本文整理汇总了C++中goal_ref类的典型用法代码示例。如果您正苦于以下问题：C++ goal_ref类的具体用法？C++ goal_ref怎么用？C++ goal_ref使用的例子？那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
在下文中一共展示了goal_ref类的20个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: operator
void operator()(goal_ref const & g, goal_ref_buffer & result) override {
ast_manager& m(g->m());
tactic_report report("qfufbv_ackr", *g);
fail_if_unsat_core_generation("qfufbv_ackr", g);
fail_if_proof_generation("qfufbv_ackr", g);
TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n"););
开发者ID:bishoksan，项目名称:z3，代码行数:7，代码来源:qfufbv_tactic.cpp
示例2: operator
void operator()(goal_ref const & g,
goal_ref_buffer & result) {
SASSERT(g->is_well_sorted());
fail_if_proof_generation("occf", g);
bool produce_models = g->models_enabled();
tactic_report report("occf", *g);
m_mc = nullptr;
ptr_vector<expr> new_lits;
cnstr2bvar c2b;
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
checkpoint();
expr * f = g->form(i);
expr_dependency * d = g->dep(i);
if (!m.is_or(f))
continue;
app * cls = to_app(f);
if (!is_target(cls))
continue;
if (produce_models && !m_mc) {
m_mc = alloc(generic_model_converter, m, "occf");
g->add(m_mc);
}
expr * keep = nullptr;
new_lits.reset();
unsigned num = cls->get_num_args();
for (unsigned j = 0; j < num; j++) {
expr * l = cls->get_arg(j);
if (is_constraint(l)) {
expr * new_l = get_aux_lit(c2b, l, g);
if (new_l != nullptr) {
new_lits.push_back(new_l);
}
else if (keep == nullptr) {
keep = l;
}
else {
new_l = mk_aux_lit(c2b, l, produce_models, g);
new_lits.push_back(new_l);
}
}
else {
new_lits.push_back(l);
}
}
if (keep != nullptr)
new_lits.push_back(keep);
g->update(i, m.mk_or(new_lits.size(), new_lits.c_ptr()), nullptr, d);
}
g->inc_depth();
result.push_back(g.get());
TRACE("occf", g->display(tout););
开发者ID:NikolajBjorner，项目名称:z3，代码行数:57，代码来源:occf_tactic.cpp
示例3: operator
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0; result.reset();
TRACE("sls", g->display(tout););
开发者ID:AleksandarZeljic，项目名称:z3，代码行数:9，代码来源:sls_tactic.cpp
示例4: operator
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
fail_if_proof_generation("aig", g);
mc = 0; pc = 0; core = 0;
operator()(g);
g->inc_depth();
result.push_back(g.get());
}
开发者ID:AleksandarZeljic，项目名称:z3，代码行数:11，代码来源:aig_tactic.cpp
示例5: operator
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
mc = 0; pc = 0; core = 0;
reduce(*(in.get()));
in->inc_depth();
result.push_back(in.get());
}
开发者ID:sukwon0709，项目名称:byterun，代码行数:11，代码来源:ctx_solver_simplify_tactic.cpp
示例6: extract_clauses_and_dependencies
void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, expr2expr_map& bool2dep, ref<filter_model_converter>& fmc) {
expr2expr_map dep2bool;
ptr_vector<expr> deps;
ast_manager& m = g->m();
expr_ref_vector clause(m);
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
expr * f = g->form(i);
expr_dependency * d = g->dep(i);
if (d == 0 || !g->unsat_core_enabled()) {
clauses.push_back(f);
}
else {
// create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
clause.reset();
clause.push_back(f);
deps.reset();
m.linearize(d, deps);
SASSERT(!deps.empty()); // d != 0, then deps must not be empty
ptr_vector<expr>::iterator it = deps.begin();
ptr_vector<expr>::iterator end = deps.end();
for (; it != end; ++it) {
expr * d = *it;
if (is_uninterp_const(d) && m.is_bool(d)) {
// no need to create a fresh boolean variable for d
if (!bool2dep.contains(d)) {
assumptions.push_back(d);
bool2dep.insert(d, d);
}
clause.push_back(m.mk_not(d));
}
else {
// must normalize assumption
expr * b = 0;
if (!dep2bool.find(d, b)) {
b = m.mk_fresh_const(0, m.mk_bool_sort());
dep2bool.insert(d, b);
bool2dep.insert(b, d);
assumptions.push_back(b);
if (!fmc) {
fmc = alloc(filter_model_converter, m);
}
fmc->insert(to_app(b)->get_decl());
}
clause.push_back(m.mk_not(b));
}
}
SASSERT(clause.size() > 1);
expr_ref cls(m);
cls = mk_or(m, clause.size(), clause.c_ptr());
clauses.push_back(cls);
}
}
}
开发者ID:ForwardFunk，项目名称:SynTree，代码行数:54，代码来源:smt_tactic.cpp
示例7: operator
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
mc = 0;
ast_manager& m(g->m());
tactic_report report("qfufbv_ackr", *g);
fail_if_unsat_core_generation("qfufbv_ackr", g);
fail_if_proof_generation("qfufbv_ackr", g);
TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n"););
开发者ID:mseve，项目名称:z3，代码行数:12，代码来源:qfufbv_tactic.cpp
示例8: operator
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
mc = 0; pc = 0; core = 0;
bool proofs_enabled = g->proofs_enabled();
if (proofs_enabled && m_blast_quant)
throw tactic_exception("quantified variable blasting does not support proof generation");
tactic_report report("bit-blaster", *g);
TRACE("before_bit_blaster", g->display(tout););
开发者ID:CHolmes3，项目名称:z3，代码行数:14，代码来源:bit_blaster_tactic.cpp
示例9: full_eval
bool full_eval(goal_ref const & g, model & mdl) {
bool res = true;
unsigned sz = g->size();
for (unsigned i = 0; i < sz && res; i++) {
checkpoint();
expr_ref o(m_manager);
if (!mdl.eval(g->form(i), o, true))
exit(ERR_INTERNAL_FATAL);
res = m_manager.is_true(o.get());
}
TRACE("sls", tout << "Evaluation: " << res << std::endl;);
开发者ID:Jornason，项目名称:z3，代码行数:15，代码来源:sls_tactic.cpp
示例10: operator
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
m_proofs_enabled = g->proofs_enabled();
m_produce_models = g->models_enabled();
m_produce_unsat_cores = g->unsat_core_enabled();
mc = 0; pc = 0; core = 0; result.reset();
tactic_report report("fpa2bv", *g);
m_rw.reset();
TRACE("fpa2bv", tout << "BEFORE: " << std::endl; g->display(tout););
开发者ID:AleksandarZeljic，项目名称:z3，代码行数:15，代码来源:fpa2bv_tactic.cpp
示例11: simplify
bool simplify(goal_ref const& g, pb_preproc_model_converter& mc) {
reset();
normalize(g);
if (g->inconsistent()) {
return false;
}
for (unsigned i = 0; i < g->size(); ++i) {
process_vars(i, g);
}
if (m_ge.empty()) {
return false;
}
for (unsigned i = 0; i < m_ge.size(); ++i) {
classify_vars(i, to_app(g->form(m_ge[i])));
}
declassifier dcl(m_vars);
expr_mark visited;
for (unsigned i = 0; !m_vars.empty() && i < m_other.size(); ++i) {
for_each_expr(dcl, visited, g->form(m_other[i]));
}
if (m_vars.empty()) {
return false;
}
// display_annotation(tout, g);
m_progress = false;
// first eliminate variables
var_map::iterator it = next_resolvent(m_vars.begin());
while (it != m_vars.end()) {
app * e = it->m_key;
rec const& r = it->m_value;
TRACE("pb", tout << mk_pp(e, m) << " " << r.pos.size() << " " << r.neg.size() << "\n";);
if (r.pos.empty()) {
replace(r.neg, e, m.mk_false(), g);
mc.set_value(e, false);
}
else if (r.neg.empty()) {
replace(r.pos, e, m.mk_true(), g);
mc.set_value(e, true);
}
if (g->inconsistent()) return false;
++it;
it = next_resolvent(it);
}
开发者ID:AleksandarZeljic，项目名称:z3，代码行数:48，代码来源:pb_preprocess_tactic.cpp
示例12: operator
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
tactic_report report("horn", *g);
bool produce_proofs = g->proofs_enabled();
if (produce_proofs) {
if (!m_ctx.get_params().generate_proof_trace()) {
params_ref params = m_ctx.get_params().p;
params.set_bool("generate_proof_trace", true);
updt_params(params);
}
}
unsigned sz = g->size();
expr_ref q(m), f(m);
expr_ref_vector queries(m);
std::stringstream msg;
m_ctx.reset();
m_ctx.ensure_opened();
for (unsigned i = 0; i < sz; i++) {
f = g->form(i);
formula_kind k = get_formula_kind(f);
switch(k) {
case IS_RULE:
m_ctx.add_rule(f, symbol::null);
break;
case IS_QUERY:
queries.push_back(f);
break;
default:
msg << "formula is not in Horn fragment: " << mk_pp(g->form(i), m) << "\n";
TRACE("horn", tout << msg.str(););
throw tactic_exception(msg.str().c_str());
}
}
开发者ID:CHolmes3，项目名称:z3，代码行数:42，代码来源:horn_tactic.cpp
示例13: reduce_core
void reduce_core(goal_ref const& g, goal_ref_buffer& result) {
init(g);
m_context.push();
assert_clauses(g);
m_context.push(); // internalize assertions.
prune_clauses();
goal_ref r(g);
insert_result(r);
r->elim_true();
result.push_back(r.get());
m_context.pop(2);
TRACE("unit_subsumption_tactic", g->display(tout); r->display(tout););
开发者ID:sukwon0709，项目名称:byterun，代码行数:12，代码来源:unit_subsumption_tactic.cpp
示例14: operator
virtual void operator()(
goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
pc = 0; core = 0;
if (g->proofs_enabled()) {
throw tactic_exception("pb-preprocess does not support proofs");
}
pb_preproc_model_converter* pp = alloc(pb_preproc_model_converter, m);
mc = pp;
g->inc_depth();
result.push_back(g.get());
while (simplify(g, *pp));
// decompose(g);
}
开发者ID:AleksandarZeljic，项目名称:z3，代码行数:21，代码来源:pb_preprocess_tactic.cpp
示例15: operator
void operator()(goal_ref const & g, goal_ref_buffer & result,
model_converter_ref & mc, proof_converter_ref & pc,
expr_dependency_ref & core) override {
mc = nullptr;
tactic_report report("collect-statistics", *g);
collect_proc cp(m, m_stats);
expr_mark visited;
const unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++)
for_each_expr(cp, visited, g->form(i));
std::cout << "(" << std::endl;
stats_type::iterator it = m_stats.begin();
stats_type::iterator end = m_stats.end();
for (; it != end; it++)
std::cout << " :" << it->first << " " << it->second << std::endl;
std::cout << ")" << std::endl;
g->inc_depth();
result.push_back(g.get());
}
开发者ID:chadbrewbaker，项目名称:z3，代码行数:22，代码来源:collect_statistics_tactic.cpp
示例16: operator
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
mc = 0; pc = 0; core = 0;
if (!is_target(*g))
throw tactic_exception("bv1 blaster cannot be applied to goal");
tactic_report report("bv1-blaster", *g);
m_num_steps = 0;
bool proofs_enabled = g->proofs_enabled();
expr_ref new_curr(m());
proof_ref new_pr(m());
unsigned size = g->size();
for (unsigned idx = 0; idx < size; idx++) {
if (g->inconsistent())
break;
expr * curr = g->form(idx);
m_rw(curr, new_curr, new_pr);
m_num_steps += m_rw.get_num_steps();
if (proofs_enabled) {
proof * pr = g->pr(idx);
new_pr = m().mk_modus_ponens(pr, new_pr);
}
g->update(idx, new_curr, new_pr, g->dep(idx));
}
if (g->models_enabled())
mc = mk_bv1_blaster_model_converter(m(), m_rw.cfg().m_const2bits);
g->inc_depth();
result.push_back(g.get());
m_rw.cfg().cleanup();
}
开发者ID:CHolmes3，项目名称:z3，代码行数:36，代码来源:bv1_blaster_tactic.cpp
示例17: operator
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
double val = (*m_p)(*(in.get())).get_value();
#pragma omp critical (probe_value_tactic)
{
if (m_msg)
m_ctx.diagnostic_stream() << m_msg << " ";
m_ctx.diagnostic_stream() << val;
if (m_newline)
m_ctx.diagnostic_stream() << std::endl;
}
skip_tactic::operator()(in, result, mc, pc, core);
}
开发者ID:greatmazinger，项目名称:z3，代码行数:16，代码来源:echo_tactic.cpp
示例18: operator
void operator()(goal_ref const & g,
goal_ref_buffer & result) {
tactic_report report("add-bounds", *g);
bound_manager bm(m);
expr_fast_mark1 visited;
add_bound_proc proc(bm, *(g.get()), m_lower, m_upper);
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++)
quick_for_each_expr(proc, visited, g->form(i));
visited.reset();
g->inc_depth();
result.push_back(g.get());
if (proc.m_num_bounds > 0)
g->updt_prec(goal::UNDER);
report_tactic_progress(":added-bounds", proc.m_num_bounds);
TRACE("add_bounds", g->display(tout););
开发者ID:NikolajBjorner，项目名称:z3，代码行数:16，代码来源:add_bounds_tactic.cpp
示例19: operator
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) override {
mc = nullptr; pc = nullptr; core = nullptr;
bool produce_proofs = g->proofs_enabled();
tactic_report report("dt2bv", *g);
unsigned size = g->size();
expr_fast_mark1 visited;
check_fd proc(*this);
for (unsigned i = 0; i < size; ++i) {
quick_for_each_expr(proc, visited, g->form(i));
}
obj_hashtable<sort>::iterator it = m_non_fd_sorts.begin(), end = m_non_fd_sorts.end();
for (; it != end; ++it) {
m_fd_sorts.remove(*it);
}
if (!m_fd_sorts.empty()) {
ref<extension_model_converter> ext = alloc(extension_model_converter, m);
ref<filter_model_converter> filter = alloc(filter_model_converter, m);
enum2bv_rewriter rw(m, m_params);
rw.set_is_fd(&m_is_fd);
expr_ref new_curr(m);
proof_ref new_pr(m);
for (unsigned idx = 0; idx < size; idx++) {
rw(g->form(idx), new_curr, new_pr);
if (produce_proofs) {
proof * pr = g->pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
g->update(idx, new_curr, new_pr, g->dep(idx));
}
expr_ref_vector bounds(m);
rw.flush_side_constraints(bounds);
for (unsigned i = 0; i < bounds.size(); ++i) {
g->assert_expr(bounds[i].get());
}
{
obj_map<func_decl, func_decl*>::iterator it = rw.enum2bv().begin(), end = rw.enum2bv().end();
for (; it != end; ++it) {
filter->insert(it->m_value);
}
}
{
obj_map<func_decl, expr*>::iterator it = rw.enum2def().begin(), end = rw.enum2def().end();
for (; it != end; ++it) {
ext->insert(it->m_key, it->m_value);
}
}
mc = concat(filter.get(), ext.get());
report_tactic_progress(":fd-num-translated", rw.num_translated());
}
g->inc_depth();
result.push_back(g.get());
TRACE("dt2bv", g->display(tout););
开发者ID:chadbrewbaker，项目名称:z3，代码行数:57，代码来源:dt2bv_tactic.cpp
示例20: operator
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
ast_manager & m = g->m();
bool produce_proofs = g->proofs_enabled();
rw r(m, produce_proofs);
#pragma omp critical (tactic_cancel)
{
m_rw = &r;
}
mc = 0; pc = 0; core = 0; result.reset();
tactic_report report("distribute-forall", *g);
expr_ref new_curr(m);
proof_ref new_pr(m);
unsigned size = g->size();
for (unsigned idx = 0; idx < size; idx++) {
if (g->inconsistent())
break;
expr * curr = g->form(idx);
r(curr, new_curr, new_pr);
if (g->proofs_enabled()) {
proof * pr = g->pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
g->update(idx, new_curr, new_pr, g->dep(idx));
}
g->inc_depth();
result.push_back(g.get());
TRACE("distribute-forall", g->display(tout););
开发者ID:killbug2004，项目名称:Snippets，代码行数:34，代码来源:distribute_forall_tactic.cpp
注：本文中的goal_ref类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台，相关代码片段筛选自各路编程大神贡献的开源项目，源码版权归原作者所有，传播和使用请参考对应项目的License；未经允许，请勿转载。 |
客服电话
APP下载
官方微信
请发表评论