mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

remove proof_converter from tactic application, removing nlsat_tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-17 23:32:29 -08:00
parent b3bd9b89b5
commit df6b1a707e
93 changed files with 236 additions and 1216 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/CMakeLists.txt
View file

@ -92,7 +92,6 @@ add_subdirectory(muz/ddnf)
add_subdirectory(muz/duality)
add_subdirectory(muz/spacer)
add_subdirectory(muz/fp)
add_subdirectory(tactic/nlsat_smt)
add_subdirectory(tactic/ufbv)
add_subdirectory(sat/sat_solver)
add_subdirectory(tactic/smtlogics)

4
src/ackermannization/ackermannize_bv_tactic.cpp
View file

@ -32,7 +32,6 @@ public:
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;
tactic_report report("ackermannize", *g);
@ -53,7 +52,6 @@ public:
result.reset();
result.push_back(g.get());
mc = 0;
pc = 0;
core = 0;
return;
}
@ -62,7 +60,7 @@ public:
if (g->models_enabled()) {
mc = mk_ackermannize_bv_model_converter(m, lackr.get_info());
}
resg->inc_depth();
TRACE("ackermannize", resg->display(tout << "out\n"););
SASSERT(resg->is_well_sorted());

3
src/api/api_tactic.cpp
View file

@ -418,7 +418,8 @@ extern "C" {
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_timer timer(timeout, &eh);
try {
exec(*to_tactic_ref(t), new_goal, ref->m_subgoals, ref->m_mc, ref->m_pc, ref->m_core);
exec(*to_tactic_ref(t), new_goal, ref->m_subgoals, ref->m_mc, ref->m_core);
ref->m_pc = new_goal->pc();
return of_apply_result(ref);
}
catch (z3_exception & ex) {

6
src/cmd_context/echo_tactic.cpp
View file

@ -30,7 +30,6 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
#pragma omp critical (echo_tactic)
{
@ -38,7 +37,7 @@ public:
if (m_newline)
m_ctx.regular_stream() << std::endl;
}
skip_tactic::operator()(in, result, mc, pc, core);
skip_tactic::operator()(in, result, mc, core);
}
};
@ -64,7 +63,6 @@ public:
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)
@ -75,7 +73,7 @@ public:
if (m_newline)
m_ctx.diagnostic_stream() << std::endl;
}
skip_tactic::operator()(in, result, mc, pc, core);
skip_tactic::operator()(in, result, mc, core);
}
};

3
src/cmd_context/tactic_cmds.cpp
View file

@ -328,7 +328,6 @@ public:
goal_ref_buffer result_goals;
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
std::string reason_unknown;
@ -340,7 +339,7 @@ public:
scoped_timer timer(timeout, &eh);
cmd_context::scoped_watch sw(ctx);
try {
exec(t, g, result_goals, mc, pc, core);
exec(t, g, result_goals, mc, core);
}
catch (tactic_exception & ex) {
ctx.regular_stream() << "(error \"tactic failed: " << ex.msg() << "\")" << std::endl;

2
src/math/subpaving/tactic/subpaving_tactic.cpp
View file

@ -244,7 +244,6 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
m_imp->process(*in);
@ -252,7 +251,6 @@ public:
result.reset();
result.push_back(in.get());
mc = 0;
pc = 0;
core = 0;
}
catch (z3_exception & ex) {

8
src/muz/fp/horn_tactic.cpp
View file

@ -179,10 +179,9 @@ class horn_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("horn", *g);
bool produce_proofs = g->proofs_enabled();
@ -235,12 +234,14 @@ class horn_tactic : public tactic {
}
SASSERT(queries.size() == 1);
q = queries[0].get();
proof_converter_ref pc = g->pc();
if (m_is_simplify) {
simplify(q, g, result, mc, pc);
}
else {
verify(q, g, result, mc, pc);
}
g->set(pc.get());
}
void verify(expr* q,
@ -386,9 +387,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void collect_statistics(statistics & st) const {

3
src/muz/pdr/pdr_context.cpp
View file

@ -203,10 +203,9 @@ namespace pdr {
goal_ref g(alloc(goal, m, false, false, false));
for (unsigned j = 0; j < v.size(); ++j) g->assert_expr(v[j].get());
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
tac(g, result, mc, pc, core);
tac(g, result, mc, core);
SASSERT(result.size() == 1);
goal* r = result[0];
v.reset();

3
src/muz/pdr/pdr_farkas_learner.cpp
View file

@ -521,11 +521,10 @@ namespace pdr {
}
expr_ref tmp(m);
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
tactic_ref simplifier = mk_arith_bounds_tactic(m);
(*simplifier)(g, result, mc, pc, core);
(*simplifier)(g, result, mc, core);
lemmas.reset();
SASSERT(result.size() == 1);
goal* r = result[0];

3
src/muz/spacer/spacer_context.cpp
View file

@ -1368,7 +1368,6 @@ void pred_transformer::frames::simplify_formulas ()
unsigned level = i < m_size ? i : infty_level ();
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
@ -1395,7 +1394,7 @@ void pred_transformer::frames::simplify_formulas ()
}
// more than one lemma at current level. simplify.
(*simplifier)(g, result, mc, pc, core);
(*simplifier)(g, result, mc, core);
SASSERT(result.size () == 1);
goal *r = result[0];

3
src/muz/spacer/spacer_legacy_frames.cpp
View file

@ -47,10 +47,9 @@ void pred_transformer::legacy_frames::simplify_formulas(tactic& tac,
goal_ref g(alloc(goal, m, false, false, false));
for (unsigned j = 0; j < v.size(); ++j) { g->assert_expr(v[j].get()); }
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
tac(g, result, mc, pc, core);
tac(g, result, mc, core);
SASSERT(result.size() == 1);
goal* r = result[0];
v.reset();

6
src/muz/spacer/spacer_util.cpp
View file

@ -930,11 +930,10 @@ void simplify_bounds_old(expr_ref_vector& cube) {
expr_ref tmp(m);
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
tactic_ref simplifier = mk_arith_bounds_tactic(m);
(*simplifier)(g, result, mc, pc, core);
(*simplifier)(g, result, mc, core);
SASSERT(result.size() == 1);
goal* r = result[0];
@ -956,14 +955,13 @@ void simplify_bounds_new (expr_ref_vector &cube) {
}
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref dep(m);
goal_ref_buffer goals;
tactic_ref prop_values = mk_propagate_values_tactic(m);
tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m);
tactic_ref t = and_then(prop_values.get(), prop_bounds.get());
(*t)(g, goals, mc, pc, dep);
(*t)(g, goals, mc, dep);
SASSERT(goals.size() == 1);
g = goals[0];

6
src/nlsat/tactic/nlsat_tactic.cpp
View file

@ -131,10 +131,9 @@ class nlsat_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("nlsat", *g);
if (g->is_decided()) {
@ -235,12 +234,11 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
imp local_imp(in->m(), m_params);
scoped_set_imp setter(*this, local_imp);
local_imp(in, result, mc, pc, core);
local_imp(in, result, mc, core);
}
catch (z3_error & ex) {
throw ex;

3
src/opt/opt_context.cpp
View file

@ -747,10 +747,9 @@ namespace opt {
else {
set_simplify(tac0.get());
}
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
(*m_simplify)(g, result, m_model_converter, pc, core);
(*m_simplify)(g, result, m_model_converter, core);
SASSERT(result.size() == 1);
goal* r = result[0];
fmls.reset();

6
src/qe/nlqsat.cpp
View file

@ -658,11 +658,10 @@ namespace qe {
fml = m.mk_iff(is_true, fml);
goal_ref g = alloc(goal, m);
g->assert_expr(fml);
proof_converter_ref pc;
expr_dependency_ref core(m);
model_converter_ref mc;
goal_ref_buffer result;
(*m_nftactic)(g, result, mc, pc, core);
(*m_nftactic)(g, result, mc, core);
SASSERT(result.size() == 1);
TRACE("qe", result[0]->display(tout););
g2s(*result[0], m_params, m_solver, m_a2b, m_t2x);
@ -814,14 +813,13 @@ namespace qe {
void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result,
/* out */ model_converter_ref & mc,
/* out */ proof_converter_ref & pc,
/* out */ expr_dependency_ref & core) {
tactic_report report("nlqsat-tactic", *in);
ptr_vector<expr> fmls;
expr_ref fml(m);
mc = 0; pc = 0; core = 0;
mc = 0; core = 0;
in->get_formulas(fmls);
fml = mk_and(m, fmls.size(), fmls.c_ptr());
if (m_mode == elim_t) {

6
src/qe/qe_lite.cpp
View file

@ -2534,10 +2534,9 @@ class qe_lite_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("qe-lite", *g);
proof_ref new_pr(m);
expr_ref new_f(m);
@ -2605,9 +2604,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}

1
src/qe/qe_sat_tactic.cpp
View file

@ -235,7 +235,6 @@ namespace qe {
goal_ref const& goal,
goal_ref_buffer& result,
model_converter_ref& mc,
proof_converter_ref & pc,
expr_dependency_ref& core)
{
try {

6
src/qe/qe_tactic.cpp
View file

@ -52,10 +52,9 @@ class qe_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("qe", *g);
m_fparams.m_model = g->models_enabled();
proof_ref new_pr(m);
@ -123,9 +122,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
m_st.reset();
m_imp->collect_statistics(m_st);

3
src/qe/qsat.cpp
View file

@ -1213,13 +1213,12 @@ namespace qe {
void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result,
/* out */ model_converter_ref & mc,
/* out */ proof_converter_ref & pc,
/* out */ expr_dependency_ref & core) {
tactic_report report("qsat-tactic", *in);
ptr_vector<expr> fmls;
expr_ref_vector defs(m);
expr_ref fml(m);
mc = 0; pc = 0; core = 0;
mc = 0; core = 0;
in->get_formulas(fmls);

3
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -505,7 +505,7 @@ private:
SASSERT(!g->proofs_enabled());
TRACE("sat", g->display(tout););
try {
(*m_preprocess)(g, m_subgoals, m_mc, m_pc, m_dep_core);
(*m_preprocess)(g, m_subgoals, m_mc, m_dep_core);
}
catch (tactic_exception & ex) {
IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
@ -520,6 +520,7 @@ private:
}
g = m_subgoals[0];
expr_ref_vector atoms(m);
m_pc = g->pc();
TRACE("sat", g->display_with_dependencies(tout););
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, false, is_lemma);
m_goal2sat.get_interpreted_atoms(atoms);

6
src/sat/tactic/sat_tactic.cpp
View file

@ -41,9 +41,8 @@ class sat_tactic : public tactic {
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;
mc = 0; core = 0;
fail_if_proof_generation("sat", g);
bool produce_models = g->models_enabled();
bool produce_core = g->unsat_core_enabled();
@ -177,12 +176,11 @@ public:
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
imp proc(g->m(), m_params);
scoped_set_imp set(this, &proc);
try {
proc(g, result, mc, pc, core);
proc(g, result, mc, core);
proc.m_solver.collect_statistics(m_stats);
}
catch (sat::solver_exception & ex) {

3
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -72,10 +72,9 @@ public:
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;
mc = 0; core = 0;
reduce(*(in.get()));
in->inc_depth();
result.push_back(in.get());

3
src/smt/tactic/smt_tactic.cpp
View file

@ -147,11 +147,10 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
IF_VERBOSE(10, verbose_stream() << "(smt.tactic start)\n";);
mc = 0; pc = 0; core = 0;
mc = 0; core = 0;
SASSERT(in->is_well_sorted());
ast_manager & m = in->m();
TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "

5
src/smt/tactic/unit_subsumption_tactic.cpp
View file

@ -42,7 +42,6 @@ struct unit_subsumption_tactic : public tactic {
virtual void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result,
/* out */ model_converter_ref & mc,
/* out */ proof_converter_ref & pc,
/* out */ expr_dependency_ref & core) {
reduce_core(in, result);
}
@ -109,9 +108,7 @@ struct unit_subsumption_tactic : public tactic {
}
void insert_result(goal_ref& result) {
for (unsigned i = 0; i < m_deleted.size(); ++i) {
result->update(m_deleted[i], m.mk_true()); // TBD proof?
}
for (auto d : m_deleted) result->update(d, m.mk_true()); // TBD proof?
}
void init(goal_ref const& g) {

5
src/solver/solver2tactic.cpp
View file

@ -104,9 +104,8 @@ public:
virtual void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result,
/* out */ model_converter_ref & mc,
/* out */ proof_converter_ref & pc,
/* out */ expr_dependency_ref & core) {
pc = 0; mc = 0; core = 0;
mc = 0; core = 0;
expr_ref_vector clauses(m);
expr2expr_map bool2dep;
ptr_vector<expr> assumptions;
@ -133,7 +132,7 @@ public:
expr_dependency* lcore = 0;
if (in->proofs_enabled()) {
pr = local_solver->get_proof();
pc = proof2proof_converter(m, pr);
in->set(proof2proof_converter(m, pr));
}
if (in->unsat_core_enabled()) {
ptr_vector<expr> core;

3
src/tactic/aig/aig_tactic.cpp
View file

@ -93,10 +93,9 @@ public:
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;
mc = 0; core = 0;
operator()(g);
g->inc_depth();
result.push_back(g.get());

8
src/tactic/arith/add_bounds_tactic.cpp
View file

@ -113,9 +113,8 @@ class add_bounds_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("add-bounds", *g);
bound_manager bm(m);
expr_fast_mark1 visited;
@ -162,10 +161,9 @@ public:
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
model_converter_ref & mc,
expr_dependency_ref & core) {
(*m_imp)(g, result, mc, pc, core);
(*m_imp)(g, result, mc, core);
}
virtual void cleanup() {

1
src/tactic/arith/arith_bounds_tactic.cpp
View file

@ -26,7 +26,6 @@ struct arith_bounds_tactic : public tactic {
virtual void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result,
/* out */ model_converter_ref & mc,
/* out */ proof_converter_ref & pc,
/* out */ expr_dependency_ref & core) {
bounds_arith_subsumption(in, result);
}

3
src/tactic/arith/card2bv_tactic.cpp
View file

@ -55,11 +55,10 @@ public:
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
TRACE("card2bv-before", g->display(tout););
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
tactic_report report("card2bv", *g);
th_rewriter rw1(m, m_params);
pb2bv_rewriter rw2(m, m_params);

6
src/tactic/arith/degree_shift_tactic.cpp
View file

@ -225,10 +225,9 @@ class degree_shift_tactic : public tactic {
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;
mc = 0; core = 0;
m_produce_proofs = g->proofs_enabled();
m_produce_models = g->models_enabled();
tactic_report report("degree_shift", *g);
@ -293,9 +292,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

6
src/tactic/arith/diff_neq_tactic.cpp
View file

@ -315,11 +315,10 @@ class diff_neq_tactic : public tactic {
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_produce_models = g->models_enabled();
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
tactic_report report("diff-neq", *g);
fail_if_proof_generation("diff-neq", g);
fail_if_unsat_core_generation("diff-neq", g);
@ -386,9 +385,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

3
src/tactic/arith/elim01_tactic.cpp
View file

@ -155,10 +155,9 @@ public:
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;
mc = 0; core = 0;
tactic_report report("elim01", *g);

3
src/tactic/arith/eq2bv_tactic.cpp
View file

@ -153,10 +153,9 @@ public:
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;
mc = 0; core = 0;
m_trail.reset();
m_fd.reset();
m_max.reset();

6
src/tactic/arith/factor_tactic.cpp
View file

@ -259,10 +259,9 @@ class factor_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("factor", *g);
bool produce_proofs = g->proofs_enabled();
@ -315,10 +314,9 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
catch (z3_error & ex) {
throw ex;

6
src/tactic/arith/fix_dl_var_tactic.cpp
View file

@ -251,10 +251,9 @@ class fix_dl_var_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("fix-dl-var", *g);
bool produce_proofs = g->proofs_enabled();
m_produce_models = g->models_enabled();
@ -323,10 +322,9 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.msg());

6
src/tactic/arith/fm_tactic.cpp
View file

@ -1552,10 +1552,9 @@ class fm_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("fm", *g);
fail_if_proof_generation("fm", g);
m_produce_models = g->models_enabled();
@ -1677,9 +1676,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
};

3
src/tactic/arith/lia2card_tactic.cpp
View file

@ -161,10 +161,9 @@ public:
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;
mc = 0; core = 0;
m_01s->reset();
tactic_report report("cardinality-intro", *g);

6
src/tactic/arith/lia2pb_tactic.cpp
View file

@ -190,13 +190,12 @@ class lia2pb_tactic : public tactic {
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());
fail_if_proof_generation("lia2pb", g);
m_produce_models = g->models_enabled();
m_produce_unsat_cores = g->unsat_core_enabled();
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
tactic_report report("lia2pb", *g);
m_bm.reset(); m_rw.reset(); m_new_deps.reset();
@ -332,10 +331,9 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.msg());

5
src/tactic/arith/nla2bv_tactic.cpp
View file

@ -442,13 +442,12 @@ public:
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());
fail_if_proof_generation("nla2bv", g);
fail_if_unsat_core_generation("nla2bv", g);
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
imp proc(g->m(), m_params);
scoped_set_imp setter(*this, proc);
proc(*(g.get()), mc);

6
src/tactic/arith/normalize_bounds_tactic.cpp
View file

@ -82,9 +82,8 @@ class normalize_bounds_tactic : public tactic {
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;
mc = 0; core = 0;
bool produce_models = in->models_enabled();
bool produce_proofs = in->proofs_enabled();
tactic_report report("normalize-bounds", *in);
@ -173,10 +172,9 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.msg());

6
src/tactic/arith/pb2bv_tactic.cpp
View file

@ -888,14 +888,13 @@ private:
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
TRACE("pb2bv", g->display(tout););
SASSERT(g->is_well_sorted());
fail_if_proof_generation("pb2bv", g);
m_produce_models = g->models_enabled();
m_produce_unsat_cores = g->unsat_core_enabled();
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
tactic_report report("pb2bv", *g);
m_bm.reset(); m_rw.reset(); m_new_deps.reset();
@ -1001,9 +1000,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

5
src/tactic/arith/propagate_ineqs_tactic.cpp
View file

@ -52,7 +52,7 @@ public:
virtual void updt_params(params_ref const & p);
virtual void collect_param_descrs(param_descrs & r) {}
virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, expr_dependency_ref & core);
virtual void cleanup();
};
@ -529,12 +529,11 @@ void propagate_ineqs_tactic::updt_params(params_ref const & p) {
void propagate_ineqs_tactic::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());
fail_if_proof_generation("propagate-ineqs", g);
fail_if_unsat_core_generation("propagate-ineqs", g);
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
goal_ref r;
(*m_imp)(g.get(), r);
result.push_back(r.get());

3
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -823,11 +823,10 @@ public:
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
mc = 0; core = 0;
tactic_report report("purify-arith", *g);
TRACE("purify_arith", g->display(tout););
bool produce_proofs = g->proofs_enabled();

6
src/tactic/arith/recover_01_tactic.cpp
View file

@ -294,13 +294,12 @@ class recover_01_tactic : public tactic {
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());
fail_if_proof_generation("recover-01", g);
fail_if_unsat_core_generation("recover-01", g);
m_produce_models = g->models_enabled();
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
tactic_report report("recover-01", *g);
bool saved = false;
@ -408,10 +407,9 @@ public:
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
(*m_imp)(g, result, mc, pc, core);
(*m_imp)(g, result, mc, core);
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.msg());

6
src/tactic/bv/bit_blaster_tactic.cpp
View file

@ -53,9 +53,8 @@ class bit_blaster_tactic : public tactic {
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;
mc = 0; core = 0;
bool proofs_enabled = g->proofs_enabled();
if (proofs_enabled && m_blast_quant)
@ -137,10 +136,9 @@ public:
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
(*m_imp)(g, result, mc, pc, core);
(*m_imp)(g, result, mc, core);
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.msg());

6
src/tactic/bv/bv1_blaster_tactic.cpp
View file

@ -381,9 +381,8 @@ class bv1_blaster_tactic : public tactic {
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;
mc = 0; core = 0;
if (!is_target(*g))
throw tactic_exception("bv1 blaster cannot be applied to goal");
@ -457,9 +456,8 @@ public:
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(g, result, mc, pc, core);
(*m_imp)(g, result, mc, core);
}
virtual void cleanup() {

4
src/tactic/bv/bv_bound_chk_tactic.cpp
View file

@ -139,7 +139,6 @@ public:
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core);
virtual tactic * translate(ast_manager & m);
virtual void updt_params(params_ref const & p);
@ -200,13 +199,12 @@ bv_bound_chk_tactic::~bv_bound_chk_tactic() {
void bv_bound_chk_tactic::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());
fail_if_proof_generation("bv-bound-chk", g);
fail_if_unsat_core_generation("bv-bound-chk", g);
TRACE("bv-bound-chk", g->display(tout << "before:"); tout << std::endl;);
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
m_imp->operator()(g);
g->inc_depth();
result.push_back(g.get());

5
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -39,7 +39,7 @@ public:
virtual ~bv_size_reduction_tactic();
virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, expr_dependency_ref & core);
virtual void cleanup();
};
@ -384,12 +384,11 @@ bv_size_reduction_tactic::~bv_size_reduction_tactic() {
void bv_size_reduction_tactic::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());
fail_if_proof_generation("bv-size-reduction", g);
fail_if_unsat_core_generation("bv-size-reduction", g);
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
m_imp->operator()(*(g.get()), mc);
g->inc_depth();
result.push_back(g.get());

6
src/tactic/bv/bvarray2uf_tactic.cpp
View file

@ -55,12 +55,11 @@ class bvarray2uf_tactic : public tactic {
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());
tactic_report report("bvarray2uf", *g);
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
fail_if_unsat_core_generation("bvarray2uf", g);
TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); );
@ -131,9 +130,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

3
src/tactic/bv/dt2bv_tactic.cpp
View file

@ -119,9 +119,8 @@ public:
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; pc = 0; core = 0;
mc = 0; core = 0;
bool produce_proofs = g->proofs_enabled();
tactic_report report("dt2bv", *g);
unsigned size = g->size();

6
src/tactic/bv/elim_small_bv_tactic.cpp
View file

@ -227,10 +227,9 @@ class elim_small_bv_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("elim-small-bv", *g);
bool produce_proofs = g->proofs_enabled();
fail_if_proof_generation("elim-small-bv", g);
@ -290,9 +289,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

6
src/tactic/bv/max_bv_sharing_tactic.cpp
View file

@ -239,10 +239,9 @@ class max_bv_sharing_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("max-bv-sharing", *g);
bool produce_proofs = g->proofs_enabled();
@ -301,9 +300,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

6
src/tactic/core/blast_term_ite_tactic.cpp
View file

@ -116,10 +116,9 @@ class blast_term_ite_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("blast-term-ite", *g);
bool produce_proofs = g->proofs_enabled();
@ -174,9 +173,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

3
src/tactic/core/cofactor_term_ite_tactic.cpp
View file

@ -57,13 +57,12 @@ public:
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());
fail_if_proof_generation("cofactor-term-ite", g);
fail_if_unsat_core_generation("cofactor-term-ite", g);
tactic_report report("cofactor-term-ite", *g);
mc = 0; pc = 0; core = 0;
mc = 0; core = 0;
process(*(g.get()));
g->inc_depth();
result.push_back(g.get());

2
src/tactic/core/collect_statistics_tactic.cpp
View file

@ -64,7 +64,7 @@ public:
virtual void collect_param_descrs(param_descrs & r) {}
virtual void operator()(goal_ref const & g, goal_ref_buffer & result,
model_converter_ref & mc, proof_converter_ref & pc,
model_converter_ref & mc,
expr_dependency_ref & core) {
mc = 0;
tactic_report report("collect-statistics", *g);

3
src/tactic/core/ctx_simplify_tactic.cpp
View file

@ -623,9 +623,8 @@ void ctx_simplify_tactic::get_param_descrs(param_descrs & r) {
void ctx_simplify_tactic::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;
mc = 0; core = 0;
(*m_imp)(*(in.get()));
in->inc_depth();
result.push_back(in.get());

1
src/tactic/core/ctx_simplify_tactic.h
View file

@ -57,7 +57,6 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core);
virtual void cleanup();

3
src/tactic/core/der_tactic.cpp
View file

@ -76,9 +76,8 @@ public:
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;
mc = 0; core = 0;
(*m_imp)(*(in.get()));
in->inc_depth();
result.push_back(in.get());

3
src/tactic/core/distribute_forall_tactic.cpp
View file

@ -102,14 +102,13 @@ public:
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);
m_rw = &r;
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
tactic_report report("distribute-forall", *g);
expr_ref new_curr(m);

3
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -187,9 +187,8 @@ void dom_simplify_tactic::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;
mc = 0; core = 0;
tactic_report report("dom-simplify", *in.get());
simplify_goal(*(in.get()));

1
src/tactic/core/dom_simplify_tactic.h
View file

@ -140,7 +140,6 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core);
virtual void cleanup();

6
src/tactic/core/elim_term_ite_tactic.cpp
View file

@ -102,10 +102,9 @@ class elim_term_ite_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("elim-term-ite", *g);
bool produce_proofs = g->proofs_enabled();
m_rw.cfg().m_produce_models = g->models_enabled();
@ -164,9 +163,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

8
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -818,9 +818,8 @@ class elim_uncnstr_tactic : public tactic {
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;
mc = 0; core = 0;
bool produce_models = g->models_enabled();
bool produce_proofs = g->proofs_enabled();
@ -934,10 +933,9 @@ public:
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
model_converter_ref & mc,
expr_dependency_ref & core) {
(*m_imp)(g, result, mc, pc, core);
(*m_imp)(g, result, mc, core);
report_tactic_progress(":num-elim-apps", get_num_elim_apps());
}

6
src/tactic/core/injectivity_tactic.cpp
View file

@ -146,10 +146,9 @@ class injectivity_tactic : public tactic {
void operator()(goal_ref const & goal,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(goal->is_well_sorted());
mc = 0; pc = 0; core = 0;
mc = 0; core = 0;
tactic_report report("injectivity", *goal);
fail_if_unsat_core_generation("injectivity", goal); // TODO: Support UNSAT cores
fail_if_proof_generation("injectivity", goal);
@ -273,9 +272,8 @@ public:
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_finder)(g, result, mc, pc, core);
(*m_finder)(g, result, mc, core);
for (unsigned i = 0; i < g->size(); ++i) {
expr* curr = g->form(i);

3
src/tactic/core/nnf_tactic.cpp
View file

@ -56,11 +56,10 @@ public:
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
TRACE("nnf", tout << "params: " << m_params << "\n"; g->display(tout););
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
mc = 0; core = 0;
tactic_report report("nnf", *g);
bool produce_proofs = g->proofs_enabled();

8
src/tactic/core/occf_tactic.cpp
View file

@ -130,11 +130,10 @@ class occf_tactic : public tactic {
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;
mc = 0; core = 0;
fail_if_proof_generation("occf", g);
bool produce_models = g->models_enabled();
@ -213,9 +212,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

3
src/tactic/core/pb_preprocess_tactic.cpp
View file

@ -152,10 +152,9 @@ public:
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;
core = 0;
if (g->proofs_enabled()) {
throw tactic_exception("pb-preprocess does not support proofs");

6
src/tactic/core/propagate_values_tactic.cpp
View file

@ -138,10 +138,9 @@ class propagate_values_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("propagate-values", *g);
m_goal = g.get();
@ -243,10 +242,9 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.msg());

5
src/tactic/core/reduce_args_tactic.cpp
View file

@ -73,7 +73,7 @@ public:
virtual ~reduce_args_tactic();
virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, expr_dependency_ref & core);
virtual void cleanup();
};
@ -485,12 +485,11 @@ reduce_args_tactic::~reduce_args_tactic() {
void reduce_args_tactic::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());
fail_if_proof_generation("reduce-args", g);
fail_if_unsat_core_generation("reduce-args", g);
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
m_imp->operator()(*(g.get()), mc);
g->inc_depth();
result.push_back(g.get());

3
src/tactic/core/simplify_tactic.cpp
View file

@ -95,13 +95,12 @@ void simplify_tactic::get_param_descrs(param_descrs & r) {
void simplify_tactic::operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
(*m_imp)(*(in.get()));
in->inc_depth();
result.push_back(in.get());
mc = 0; pc = 0; core = 0;
mc = 0; core = 0;
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.msg());

1
src/tactic/core/simplify_tactic.h
View file

@ -37,7 +37,6 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core);
virtual void cleanup();

6
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -669,10 +669,9 @@ class solve_eqs_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("solve_eqs", *g);
m_produce_models = g->models_enabled();
m_produce_proofs = g->proofs_enabled();
@ -736,9 +735,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
report_tactic_progress(":num-elim-vars", m_imp->get_num_eliminated_vars());
}

5
src/tactic/core/split_clause_tactic.cpp
View file

@ -108,12 +108,11 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(in->is_well_sorted());
tactic_report report("split-clause", *in);
TRACE("before_split_clause", in->display(tout););
pc = 0; mc = 0; core = 0;
mc = 0; core = 0;
ast_manager & m = in->m();
unsigned cls_pos = select_clause(m, in);
if (cls_pos == UINT_MAX) {
@ -123,7 +122,7 @@ public:
app * cls = to_app(in->form(cls_pos));
expr_dependency * cls_dep = in->dep(cls_pos);
if (produce_proofs)
pc = alloc(split_pc, m, cls, in->pr(cls_pos));
in->set(alloc(split_pc, m, cls, in->pr(cls_pos)));
unsigned cls_sz = cls->get_num_args();
report_tactic_progress(":num-new-branches", cls_sz);
for (unsigned i = 0; i < cls_sz; i++) {

4
src/tactic/core/symmetry_reduce_tactic.cpp
View file

@ -41,7 +41,6 @@ public:
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core);
virtual void cleanup();
};
@ -637,11 +636,10 @@ symmetry_reduce_tactic::~symmetry_reduce_tactic() {
void symmetry_reduce_tactic::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("symmetry_reduce", g);
fail_if_unsat_core_generation("symmetry_reduce", g);
mc = 0; pc = 0; core = 0; result.reset();
mc = 0; core = 0; result.reset();
(*m_imp)(*(g.get()));
g->inc_depth();
result.push_back(g.get());

6
src/tactic/core/tseitin_cnf_tactic.cpp
View file

@ -801,10 +801,9 @@ class tseitin_cnf_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("tseitin-cnf", *g);
fail_if_proof_generation("tseitin-cnf", g);
m_produce_models = g->models_enabled();
@ -886,9 +885,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
report_tactic_progress(":cnf-aux-vars", m_imp->m_num_aux_vars);
}

6
src/tactic/fpa/fpa2bv_tactic.cpp
View file

@ -49,14 +49,13 @@ class fpa2bv_tactic : public tactic {
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();
mc = 0; core = 0; result.reset();
tactic_report report("fpa2bv", *g);
m_rw.reset();
@ -142,10 +141,9 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.msg());

25
src/tactic/goal.cpp
View file

@ -16,11 +16,11 @@ Author:
Revision History:
--*/
#include "tactic/goal.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/for_each_expr.h"
#include "ast/well_sorted.h"
#include "tactic/goal.h"
goal::precision goal::mk_union(precision p1, precision p2) {
if (p1 == PRECISE) return p2;
@ -344,10 +344,7 @@ void goal::display_with_dependencies(ast_printer & prn, std::ostream & out) cons
out << "\n |-";
deps.reset();
m().linearize(dep(i), deps);
ptr_vector<expr>::iterator it = deps.begin();
ptr_vector<expr>::iterator end = deps.end();
for (; it != end; ++it) {
expr * d = *it;
for (expr * d : deps) {
if (is_uninterp_const(d)) {
out << " " << mk_ismt2_pp(d, m());
}
@ -361,10 +358,7 @@ void goal::display_with_dependencies(ast_printer & prn, std::ostream & out) cons
}
if (!to_pp.empty()) {
out << "\n :dependencies-definitions (";
obj_hashtable<expr>::iterator it = to_pp.begin();
obj_hashtable<expr>::iterator end = to_pp.end();
for (; it != end; ++it) {
expr * d = *it;
for (expr* d : to_pp) {
out << "\n (#" << d->get_id() << "\n ";
prn.display(out, d, 2);
out << ")";
@ -382,10 +376,7 @@ void goal::display_with_dependencies(std::ostream & out) const {
out << "\n |-";
deps.reset();
m().linearize(dep(i), deps);
ptr_vector<expr>::iterator it = deps.begin();
ptr_vector<expr>::iterator end = deps.end();
for (; it != end; ++it) {
expr * d = *it;
for (expr * d : deps) {
if (is_uninterp_const(d)) {
out << " " << mk_ismt2_pp(d, m());
}
@ -510,14 +501,12 @@ void goal::shrink(unsigned j) {
unsigned sz = size();
for (unsigned i = j; i < sz; i++)
m().pop_back(m_forms);
if (proofs_enabled()) {
if (proofs_enabled())
for (unsigned i = j; i < sz; i++)
m().pop_back(m_proofs);
}
if (unsat_core_enabled()) {
if (unsat_core_enabled())
for (unsigned i = j; i < sz; i++)
m().pop_back(m_dependencies);
}
}
/**
@ -662,6 +651,8 @@ goal * goal::translate(ast_translation & translator) const {
res->m_inconsistent = m_inconsistent;
res->m_depth = m_depth;
res->m_precision = m_precision;
res->m_pc = m_pc ? m_pc->translate(translator) : nullptr;
res->m_mc = m_mc ? m_mc->translate(translator) : nullptr;
return res;
}

11
src/tactic/goal.h
View file

@ -35,6 +35,8 @@ Revision History:
#include "util/ref.h"
#include "util/ref_vector.h"
#include "util/ref_buffer.h"
#include "tactic/model_converter.h"
#include "tactic/proof_converter.h"
class goal {
public:
@ -49,6 +51,8 @@ public:
protected:
ast_manager & m_manager;
model_converter_ref m_mc;
proof_converter_ref m_pc;
unsigned m_ref_count;
expr_array m_forms;
expr_array m_proofs;
@ -142,6 +146,13 @@ public:
bool is_decided() const;
bool is_well_sorted() const;
model_converter* mc() { return m_mc.get(); }
proof_converter* pc() { return inconsistent() ? proof2proof_converter(m(), pr(0)) : m_pc.get(); }
void add(model_converter* m) { m_mc = concat(m_mc.get(), m); }
void add(proof_converter* p) { m_pc = concat(m_pc.get(), p); }
void set(model_converter* m) { m_mc = m; }
void set(proof_converter* p) { m_pc = p; }
goal * translate(ast_translation & translator) const;
};

9
src/tactic/nlsat_smt/CMakeLists.txt
View file

@ -1,9 +0,0 @@
z3_add_component(nlsat_smt_tactic
SOURCES
nl_purify_tactic.cpp
COMPONENT_DEPENDENCIES
nlsat_tactic
smt_tactic
TACTIC_HEADERS
nl_purify_tactic.h
)

799
src/tactic/nlsat_smt/nl_purify_tactic.cpp
View file

@ -1,799 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
nl_purify_tactic.cpp
Abstract:
Tactic for purifying quantifier-free formulas that mix QF_NRA and other theories.
It is designed to allow cooprating between the nlsat solver and other theories
in a decoupled way.
Let goal be formula F.
Let NL goal be formula G.
Assume F is in NNF.
Assume F does not contain mix of real/integers.
Assume F is quantifier-free (please, otherwise we need to reprocess from instantiated satisfiable formula)
For each atomic nl formula f,
- introduce a propositional variable p
- replace f by p
- add clauses p => f to G
For each interface term t,
- introduce interface variable v (or use t if it is already a variable)
- replace t by v
Check satisfiability of G.
If satisfiable, then check assignment to p and interface equalities on F
If unsat:
Retrieve core and add core to G.
else:
For interface equalities from model of F that are not equal in G, add
For interface variables that are equal under one model, but not the other model,
create interface predicate p_vw => v = w, add to both F, G.
Add interface equations to assumptions, recheck F.
If unsat retrieve core add to G.
Author:
Nikolaj Bjorner (nbjorner) 2015-5-5.
Revision History:
--*/
#include "tactic/tactical.h"
#include "tactic/nlsat_smt/nl_purify_tactic.h"
#include "smt/tactic/smt_tactic.h"
#include "ast/rewriter/rewriter.h"
#include "nlsat/tactic/nlsat_tactic.h"
#include "tactic/generic_model_converter.h"
#include "util/obj_pair_hashtable.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_pp.h"
#include "util/trace.h"
#include "smt/smt_solver.h"
#include "solver/solver.h"
#include "model/model_smt2_pp.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/ast_util.h"
#include "solver/solver2tactic.h"
class nl_purify_tactic : public tactic {
enum polarity_t {
pol_pos,
pol_neg,
pol_dual
};
ast_manager & m;
arith_util m_util;
params_ref m_params;
bool m_produce_proofs;
ref<generic_model_converter> m_fmc;
tactic_ref m_nl_tac; // nlsat tactic
goal_ref m_nl_g; // nlsat goal
ref<solver> m_solver; // SMT solver
expr_ref_vector m_eq_preds; // predicates for equality between pairs of interface variables
svector<lbool> m_eq_values; // truth value of the equality predicates in nlsat
app_ref_vector m_new_reals; // interface real variables
app_ref_vector m_new_preds; // abstraction predicates for smt_solver (hide real constraints)
expr_ref_vector m_asms; // assumptions to pass to SMT solver
ptr_vector<expr> m_ctx_asms; // assumptions passed by context
obj_hashtable<expr> m_ctx_asms_set; // assumptions passed by context
obj_hashtable<expr> m_used_asms;
obj_map<expr, expr*> m_bool2dep;
obj_pair_map<expr,expr,expr*> m_eq_pairs; // map pairs of interface variables to auxiliary predicates
obj_map<expr,expr*> m_interface_cache; // map of compound real expression to interface variable.
obj_map<expr, polarity_t> m_polarities; // polarities of sub-expressions
public:
struct rw_cfg : public default_rewriter_cfg {
enum mode_t {
mode_interface_var,
mode_bool_preds
};
ast_manager& m;
nl_purify_tactic & m_owner;
app_ref_vector& m_new_reals;
app_ref_vector& m_new_preds;
obj_map<expr, polarity_t>& m_polarities;
obj_map<expr,expr*>& m_interface_cache;
expr_ref_vector m_args;
proof_ref_vector m_proofs;
mode_t m_mode;
rw_cfg(nl_purify_tactic & o):
m(o.m),
m_owner(o),
m_new_reals(o.m_new_reals),
m_new_preds(o.m_new_preds),
m_polarities(o.m_polarities),
m_interface_cache(o.m_interface_cache),
m_args(m),
m_proofs(m),
m_mode(mode_interface_var) {
}
virtual ~rw_cfg() {}
arith_util & u() { return m_owner.m_util; }
expr * mk_interface_var(expr* arg, proof_ref& arg_pr) {
expr* r;
if (m_interface_cache.find(arg, r)) {
return r;
}
if (is_uninterp_const(arg)) {
m_interface_cache.insert(arg, arg);
return arg;
}
r = m.mk_fresh_const(0, u().mk_real());
m_new_reals.push_back(to_app(r));
m_owner.m_fmc->hide(r);
m_interface_cache.insert(arg, r);
expr_ref eq(m);
eq = m.mk_eq(r, arg);
if (is_real_expression(arg)) {
m_owner.m_nl_g->assert_expr(eq); // m.mk_oeq(r, arg)
}
else {
m_owner.m_solver->assert_expr(eq);
}
if (m_owner.m_produce_proofs) {
arg_pr = m.mk_oeq(arg, r);
}
return r;
}
bool is_real_expression(expr* e) {
return is_app(e) && (to_app(e)->get_family_id() == u().get_family_id());
}
void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref& pr) {
expr_ref old_pred(m.mk_app(f, num, args), m);
polarity_t pol = m_polarities.find(old_pred);
result = m.mk_fresh_const(0, m.mk_bool_sort());
m_polarities.insert(result, pol);
m_new_preds.push_back(to_app(result));
m_owner.m_fmc->hide(result);
if (pol != pol_neg) {
m_owner.m_nl_g->assert_expr(m.mk_or(m.mk_not(result), old_pred));
}
if (pol != pol_pos) {
m_owner.m_nl_g->assert_expr(m.mk_or(result, m.mk_not(old_pred)));
}
if (m_owner.m_produce_proofs) {
pr = m.mk_oeq(old_pred, result);
}
TRACE("nlsat_smt", tout << old_pred << " : " << result << "\n";);
}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
throw tactic_exception("quantifiers are not supported in mixed-mode nlsat engine");
}
br_status reduce_app(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) {
if (m_mode == mode_bool_preds) {
return reduce_app_bool(f, num, args, result, pr);
}
else {
return reduce_app_real(f, num, args, result, pr);
}
}
br_status reduce_app_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) {
if (f->get_family_id() == m.get_basic_family_id()) {
if (f->get_decl_kind() == OP_EQ && u().is_real(args[0])) {
mk_interface_bool(f, num, args, result, pr);
return BR_DONE;
}
else {
return BR_FAILED;
}
}
if (f->get_family_id() == u().get_family_id()) {
switch (f->get_decl_kind()) {
case OP_LE: case OP_GE: case OP_LT: case OP_GT:
// these are the only real cases of non-linear atomic formulas besides equality.
mk_interface_bool(f, num, args, result, pr);
return BR_DONE;
default:
return BR_FAILED;
}
}
return BR_FAILED;
}
// (+ (f x) y)
// (f (+ x y))
//
bool is_arith_op(expr* e) {
return is_app(e) && to_app(e)->get_family_id() == u().get_family_id();
}
br_status reduce_app_real(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) {
bool has_interface = false;
bool is_arith = false;
if (f->get_family_id() == u().get_family_id()) {
switch (f->get_decl_kind()) {
case OP_NUM:
case OP_IRRATIONAL_ALGEBRAIC_NUM:
return BR_FAILED;
default:
is_arith = true;
break;
}
}
m_args.reset();
m_proofs.reset();
for (unsigned i = 0; i < num; ++i) {
expr* arg = args[i];
proof_ref arg_pr(m);
if (is_arith && !is_arith_op(arg)) {
has_interface = true;
m_args.push_back(mk_interface_var(arg, arg_pr));
}
else if (!is_arith && u().is_real(arg)) {
has_interface = true;
m_args.push_back(mk_interface_var(arg, arg_pr));
}
else {
m_args.push_back(arg);
}
if (arg_pr) {
m_proofs.push_back(arg_pr);
}
}
if (has_interface) {
result = m.mk_app(f, num, m_args.c_ptr());
if (m_owner.m_produce_proofs) {
pr = m.mk_oeq_congruence(m.mk_app(f, num, args), to_app(result), m_proofs.size(), m_proofs.c_ptr());
}
TRACE("nlsat_smt", tout << result << "\n";);
return BR_DONE;
}
else {
return BR_FAILED;
}
}
};
private:
class rw : public rewriter_tpl<rw_cfg> {
rw_cfg m_cfg;
public:
rw(nl_purify_tactic & o):
rewriter_tpl<rw_cfg>(o.m, o.m_produce_proofs, m_cfg),
m_cfg(o) {
}
void set_bool_mode() {
m_cfg.m_mode = rw_cfg::mode_bool_preds;
}
void set_interface_var_mode() {
m_cfg.m_mode = rw_cfg::mode_interface_var;
}
};
arith_util & u() { return m_util; }
void check_point() {
if (m.canceled()) {
throw tactic_exception(Z3_CANCELED_MSG);
}
}
void display_result(std::ostream& out, goal_ref_buffer const& result) {
for (unsigned i = 0; i < result.size(); ++i) {
result[i]->display_with_dependencies(out << "goal\n");
}
}
void update_eq_values(model_ref& mdl) {
expr_ref tmp(m);
for (unsigned i = 0; i < m_eq_preds.size(); ++i) {
expr* pred = m_eq_preds[i].get();
m_eq_values[i] = l_undef;
if (mdl->eval(pred, tmp)) {
if (m.is_true(tmp)) {
m_eq_values[i] = l_true;
}
else if (m.is_false(tmp)) {
m_eq_values[i] = l_false;
}
}
}
}
void solve(
goal_ref const& g,
goal_ref_buffer& result,
expr_dependency_ref& core,
model_converter_ref& mc) {
while (true) {
check_point();
TRACE("nlsat_smt", m_solver->display(tout << "SMT:\n"); m_nl_g->display(tout << "\nNL:\n"); );
goal_ref tmp_nl = alloc(goal, m, true, false);
model_converter_ref nl_mc;
proof_converter_ref nl_pc;
expr_dependency_ref nl_core(m);
result.reset();
tmp_nl->copy_from(*m_nl_g.get());
(*m_nl_tac)(tmp_nl, result, nl_mc, nl_pc, nl_core);
if (is_decided_unsat(result)) {
core2result(core, g, result);
TRACE("nlsat_smt", tout << "unsat\n";);
break;
}
if (!is_decided_sat(result)) {
TRACE("nlsat_smt", tout << "not a unit\n";);
break;
}
// extract evaluation on interface variables.
// assert booleans that evaluate to true.
// assert equalities between equal interface real variables.
model_ref mdl_nl, mdl_smt;
if (nl_mc.get()) {
model_converter2model(m, nl_mc.get(), mdl_nl);
update_eq_values(mdl_nl);
enforce_equalities(mdl_nl, m_nl_g);
setup_assumptions(mdl_nl);
TRACE("nlsat_smt",
model_smt2_pp(tout << "nl model\n", m, *mdl_nl.get(), 0);
m_solver->display(tout << "smt goal:\n"); tout << "\n";);
}
result.reset();
lbool r = m_solver->check_sat(m_asms.size(), m_asms.c_ptr());
if (r == l_false) {
// extract the core from the result
ptr_vector<expr> ecore, asms;
expr_ref_vector clause(m);
expr_ref fml(m);
get_unsat_core(ecore, asms);
//
// assumptions should also be used for the nlsat tactic,
// but since it does not support assumptions at this time
// we overapproximate the necessary core and accumulate
// all assumptions that are ever used.
//
for (unsigned i = 0; i < asms.size(); ++i) {
m_used_asms.insert(asms[i]);
}
if (ecore.empty()) {
core2result(core, g, result);
break;
}
for (unsigned i = 0; i < ecore.size(); ++i) {
clause.push_back(mk_not(m, ecore[i]));
}
fml = mk_or(m, clause.size(), clause.c_ptr());
m_nl_g->assert_expr(fml);
continue;
}
else if (r == l_true) {
m_solver->get_model(mdl_smt);
if (enforce_equalities(mdl_smt, m_nl_g)) {
// SMT enforced a new equality that wasn't true for nlsat.
continue;
}
TRACE("nlsat_smt",
m_fmc->display(tout << "joint state is sat\n");
nl_mc->display(tout << "nl\n"););
if (mdl_nl.get()) {
merge_models(*mdl_nl.get(), mdl_smt);
}
mc = m_fmc.get();
apply(mc, mdl_smt, 0);
mc = model2model_converter(mdl_smt.get());
result.push_back(alloc(goal, m));
}
else {
TRACE("nlsat_smt", tout << "unknown\n";);
}
break;
}
TRACE("nlsat_smt", display_result(tout, result););
}
void get_unsat_core(ptr_vector<expr>& core, ptr_vector<expr>& asms) {
m_solver->get_unsat_core(core);
for (unsigned i = 0; i < core.size(); ++i) {
if (m_ctx_asms_set.contains(core[i])) {
asms.push_back(core[i]);
core[i] = core.back();
core.pop_back();
--i;
}
}
}
void core2result(expr_dependency_ref & lcore, goal_ref const& g, goal_ref_buffer& result) {
result.reset();
proof * pr = 0;
lcore = 0;
g->reset();
obj_hashtable<expr>::iterator it = m_used_asms.begin(), end = m_used_asms.end();
for (; it != end; ++it) {
lcore = m.mk_join(lcore, m.mk_leaf(m_bool2dep.find(*it)));
}
g->assert_expr(m.mk_false(), pr, lcore);
TRACE("nlsat_smt", g->display_with_dependencies(tout););
result.push_back(g.get());
}
void setup_assumptions(model_ref& mdl) {
m_asms.reset();
m_asms.append(m_ctx_asms.size(), m_ctx_asms.c_ptr());
app_ref_vector const& fresh_preds = m_new_preds;
expr_ref tmp(m);
for (unsigned i = 0; i < fresh_preds.size(); ++i) {
expr* pred = fresh_preds[i];
if (mdl->eval(pred, tmp)) {
polarity_t pol = m_polarities.find(pred);
// if assumptinon literals are used to satisfy NL state,
// we have to assume them when satisfying SMT state
if (pol != pol_neg && m.is_false(tmp)) {
m_asms.push_back(m.mk_not(pred));
}
else if (pol != pol_pos && m.is_true(tmp)) {
m_asms.push_back(pred);
}
}
}
for (unsigned i = 0; i < m_eq_preds.size(); ++i) {
expr* pred = m_eq_preds[i].get();
switch (m_eq_values[i]) {
case l_true:
m_asms.push_back(pred);
break;
case l_false:
m_asms.push_back(m.mk_not(pred));
break;
default:
break;
}
}
TRACE("nlsat_smt",
tout << "assumptions:\n" << m_asms << "\n";);
}
bool enforce_equalities(model_ref& mdl, goal_ref const& nl_g) {
TRACE("nlsat_smt", tout << "Enforce equalities " << m_interface_cache.size() << "\n";);
bool new_equality = false;
expr_ref_vector nums(m);
obj_map<expr, expr*> num2var;
obj_map<expr, expr*>::iterator it = m_interface_cache.begin(), end = m_interface_cache.end();
for (; it != end; ++it) {
expr_ref r(m);
expr* v, *w, *pred;
w = it->m_value;
VERIFY(mdl->eval(w, r));
TRACE("nlsat_smt", tout << mk_pp(w, m) << " |-> " << r << "\n";);
nums.push_back(r);
if (num2var.find(r, v)) {
if (!m_eq_pairs.find(v, w, pred)) {
pred = m.mk_fresh_const(0, m.mk_bool_sort());
m_eq_preds.push_back(pred);
m_eq_values.push_back(l_true);
m_fmc->hide(pred);
nl_g->assert_expr(m.mk_or(m.mk_not(pred), m.mk_eq(w, v)));
nl_g->assert_expr(m.mk_or(pred, m.mk_not(m.mk_eq(w, v))));
m_solver->assert_expr(m.mk_iff(pred, m.mk_eq(w, v)));
new_equality = true;
m_eq_pairs.insert(v, w, pred);
}
else {
// interface equality is already enforced.
}
}
else {
num2var.insert(r, w);
}
}
return new_equality;
}
void merge_models(model const& mdl_nl, model_ref& mdl_smt) {
expr_safe_replace num2num(m);
expr_ref result(m), val2(m);
expr_ref_vector args(m);
unsigned sz = mdl_nl.get_num_constants();
for (unsigned i = 0; i < sz; ++i) {
func_decl* v = mdl_nl.get_constant(i);
if (u().is_real(v->get_range())) {
expr* val = mdl_nl.get_const_interp(v);
if (mdl_smt->eval(v, val2)) {
if (val != val2) {
num2num.insert(val2, val);
}
}
}
}
sz = mdl_smt->get_num_functions();
for (unsigned i = 0; i < sz; ++i) {
func_decl* f = mdl_smt->get_function(i);
if (has_real(f)) {
unsigned arity = f->get_arity();
func_interp* f1 = mdl_smt->get_func_interp(f);
func_interp* f2 = alloc(func_interp, m, f->get_arity());
for (unsigned j = 0; j < f1->num_entries(); ++j) {
args.reset();
func_entry const* entry = f1->get_entry(j);
for (unsigned k = 0; k < arity; ++k) {
translate(num2num, entry->get_arg(k), result);
args.push_back(result);
}
translate(num2num, entry->get_result(), result);
f2->insert_entry(args.c_ptr(), result);
}
translate(num2num, f1->get_else(), result);
f2->set_else(result);
mdl_smt->register_decl(f, f2);
}
}
mdl_smt->copy_const_interps(mdl_nl);
}
bool has_real(func_decl* f) {
for (unsigned i = 0; i < f->get_arity(); ++i) {
if (u().is_real(f->get_domain(i))) return true;
}
return u().is_real(f->get_range());
}
void translate(expr_safe_replace& num2num, expr* e, expr_ref& result) {
result = 0;
if (e) {
num2num(e, result);
}
}
void get_polarities(goal const& g) {
ptr_vector<expr> forms;
svector<polarity_t> pols;
unsigned sz = g.size();
for (unsigned i = 0; i < sz; ++i) {
forms.push_back(g.form(i));
pols.push_back(pol_pos);
}
polarity_t p, q;
while (!forms.empty()) {
expr* e = forms.back();
p = pols.back();
forms.pop_back();
pols.pop_back();
if (m_polarities.find(e, q)) {
if (p == q || q == pol_dual) continue;
p = pol_dual;
}
TRACE("nlsat_smt_verbose", tout << mk_pp(e, m) << "\n";);
m_polarities.insert(e, p);
if (is_quantifier(e) || is_var(e)) {
throw tactic_exception("nl-purify tactic does not support quantifiers");
}
SASSERT(is_app(e));
app* a = to_app(e);
func_decl* f = a->get_decl();
if (f->get_family_id() == m.get_basic_family_id() && p != pol_dual) {
switch(f->get_decl_kind()) {
case OP_NOT:
p = neg(p);
break;
case OP_AND:
case OP_OR:
break;
default:
p = pol_dual;
break;
}
}
else {
p = pol_dual;
}
for (unsigned i = 0; i < a->get_num_args(); ++i) {
forms.push_back(a->get_arg(i));
pols.push_back(p);
}
}
}
polarity_t neg(polarity_t p) {
switch (p) {
case pol_pos: return pol_neg;
case pol_neg: return pol_pos;
case pol_dual: return pol_dual;
}
return pol_dual;
}
polarity_t join(polarity_t p, polarity_t q) {
if (p == q) return p;
return pol_dual;
}
void rewrite_goal(rw& r, goal_ref const& g) {
r.reset();
expr_ref new_curr(m);
proof_ref new_pr(m);
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
expr * curr = g->form(i);
r(curr, new_curr, new_pr);
if (m_produce_proofs) {
proof * pr = g->pr(i);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
g->update(i, new_curr, new_pr, g->dep(i));
}
}
void remove_pure_arith(goal_ref const& g) {
obj_map<expr, bool> is_pure;
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
expr * curr = g->form(i);
if (is_pure_arithmetic(is_pure, curr)) {
m_nl_g->assert_expr(curr, g->pr(i), g->dep(i));
g->update(i, m.mk_true(), g->pr(i), g->dep(i));
}
}
}
bool is_pure_arithmetic(obj_map<expr, bool>& is_pure, expr* e0) {
ptr_vector<expr> todo;
todo.push_back(e0);
while (!todo.empty()) {
expr* e = todo.back();
if (is_pure.contains(e)) {
todo.pop_back();
continue;
}
if (!is_app(e)) {
todo.pop_back();
is_pure.insert(e, false);
continue;
}
app* a = to_app(e);
bool pure = false, all_found = true, p;
pure |= (a->get_family_id() == u().get_family_id()) && u().is_real(a);
pure |= (m.is_eq(e) && u().is_real(a->get_arg(0)));
pure |= (a->get_family_id() == u().get_family_id()) && m.is_bool(a) && u().is_real(a->get_arg(0));
pure |= (a->get_family_id() == m.get_basic_family_id());
pure |= is_uninterp_const(a) && u().is_real(a);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
if (!is_pure.find(a->get_arg(i), p)) {
todo.push_back(a->get_arg(i));
all_found = false;
}
else {
pure &= p;
}
}
if (all_found) {
is_pure.insert(e, pure);
todo.pop_back();
}
}
return is_pure.find(e0);
}
public:
nl_purify_tactic(ast_manager & m, params_ref const& p):
m(m),
m_util(m),
m_params(p),
m_fmc(0),
m_nl_tac(mk_nlsat_tactic(m, p)),
m_nl_g(0),
m_solver(mk_smt_solver(m, p, symbol::null)),
m_eq_preds(m),
m_new_reals(m),
m_new_preds(m),
m_asms(m)
{}
virtual ~nl_purify_tactic() {}
virtual void updt_params(params_ref const & p) {
m_params = p;
}
virtual tactic * translate(ast_manager& m) {
return alloc(nl_purify_tactic, m, m_params);
}
virtual void collect_statistics(statistics & st) const {
m_nl_tac->collect_statistics(st);
m_solver->collect_statistics(st);
}
virtual void reset_statistics() {
m_nl_tac->reset_statistics();
}
virtual void cleanup() {
m_solver = mk_smt_solver(m, m_params, symbol::null);
m_nl_tac->cleanup();
m_eq_preds.reset();
m_eq_values.reset();
m_new_reals.reset();
m_new_preds.reset();
m_eq_pairs.reset();
m_polarities.reset();
m_ctx_asms.reset();
m_ctx_asms_set.reset();
m_used_asms.reset();
m_bool2dep.reset();
}
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
tactic_report report("qfufnl-purify", *g);
TRACE("nlsat_smt", g->display(tout););
m_produce_proofs = g->proofs_enabled();
mc = 0; pc = 0; core = 0;
fail_if_proof_generation("qfufnra-purify", g);
// fail_if_unsat_core_generation("qfufnra-purify", g);
rw r(*this);
expr_ref_vector clauses(m);
m_nl_g = alloc(goal, m, true, false);
m_fmc = alloc(generic_model_converter, m);
// first hoist interface variables,
// then annotate subformulas by polarities,
// finally extract polynomial inequalities by
// creating a place-holder predicate inside the
// original goal and extracing pure nlsat clauses.
r.set_interface_var_mode();
rewrite_goal(r, g);
if (!g->unsat_core_enabled()) {
remove_pure_arith(g);
}
get_polarities(*g.get());
r.set_bool_mode();
rewrite_goal(r, g);
extract_clauses_and_dependencies(g, clauses, m_ctx_asms, m_bool2dep, m_fmc);
TRACE("nlsat_smt", tout << clauses << "\n";);
for (unsigned i = 0; i < m_ctx_asms.size(); ++i) {
m_ctx_asms_set.insert(m_ctx_asms[i]);
}
for (unsigned i = 0; i < clauses.size(); ++i) {
m_solver->assert_expr(clauses[i].get());
}
g->inc_depth();
solve(g, result, core, mc);
}
};
tactic * mk_nl_purify_tactic(ast_manager& m, params_ref const& p) {
return alloc(nl_purify_tactic, m, p);
}

35
src/tactic/nlsat_smt/nl_purify_tactic.h
View file

@ -1,35 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
nl_purify_tactic.h
Abstract:
Tactic for purifying quantifier-free formulas that mix QF_NRA and other theories.
It is designed to allow cooprating between the nlsat solver and other theories
in a decoubled way.
Author:
Nikolaj Bjorner (nbjorner) 2015-5-5.
Revision History:
--*/
#ifndef NL_PURIFY_TACTIC_H_
#define NL_PURIFY_TACTIC_H_
#include "util/params.h"
class ast_manager;
class tactic;
tactic * mk_nl_purify_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("nl-purify", "Decompose goal into pure NL-sat formula and formula over other theories.", "mk_nl_purify_tactic(m, p)")
*/
#endif

2
src/tactic/portfolio/parallel_tactic.cpp
View file

@ -541,7 +541,7 @@ public:
init();
}
void operator ()(const goal_ref & g,goal_ref_buffer & result,model_converter_ref & mc,proof_converter_ref & pc,expr_dependency_ref & dep) {
void operator ()(const goal_ref & g,goal_ref_buffer & result,model_converter_ref & mc, expr_dependency_ref & dep) {
ast_manager& m = g->m();
solver* s = mk_fd_solver(m, m_params);
solver_state* st = alloc(solver_state, 0, s, m_params, cube_task);

3
src/tactic/sine_filter.cpp
View file

@ -49,9 +49,8 @@ public:
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; pc = 0; core = 0;
mc = 0; core = 0;
TRACE("sine", g->display(tout););
TRACE("sine", tout << g->size(););

3
src/tactic/sls/sls_tactic.cpp
View file

@ -62,10 +62,9 @@ public:
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();
mc = 0; core = 0; result.reset();
TRACE("sls", g->display(tout););
tactic_report report("sls", *g);

3
src/tactic/smtlogics/CMakeLists.txt
View file

@ -11,7 +11,6 @@ z3_add_component(smtlogic_tactics
qfnra_tactic.cpp
qfufbv_ackr_model_converter.cpp
qfufbv_tactic.cpp
qfufnra_tactic.cpp
qfuf_tactic.cpp
quant_tactics.cpp
COMPONENT_DEPENDENCIES
@ -22,7 +21,6 @@ z3_add_component(smtlogic_tactics
fp
muz
nlsat_tactic
nlsat_smt_tactic
qe
sat_solver
smt_tactic
@ -40,6 +38,5 @@ z3_add_component(smtlogic_tactics
qfnra_tactic.h
qfuf_tactic.h
qfufbv_tactic.h
qfufnra_tactic.h
quant_tactics.h
)

1
src/tactic/smtlogics/qfufbv_tactic.cpp
View file

@ -56,7 +56,6 @@ public:
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());

19
src/tactic/tactic.cpp
View file

@ -70,12 +70,10 @@ void report_tactic_progress(char const * id, unsigned val) {
void skip_tactic::operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
result.reset();
result.push_back(in.get());
mc = 0;
pc = 0;
core = 0;
}
@ -88,7 +86,6 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
throw tactic_exception("fail tactic");
}
@ -111,10 +108,9 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
IF_VERBOSE(m_lvl, verbose_stream() << m_msg << "\n";);
skip_tactic::operator()(in, result, mc, pc, core);
skip_tactic::operator()(in, result, mc, core);
}
};
@ -130,11 +126,10 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
TRACE(m_tag, in->display(tout););
(void)m_tag;
skip_tactic::operator()(in, result, mc, pc, core);
skip_tactic::operator()(in, result, mc, core);
}
};
@ -149,11 +144,10 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
if (!in->is_decided())
throw tactic_exception("undecided");
skip_tactic::operator()(in, result, mc, pc, core);
skip_tactic::operator()(in, result, mc, core);
}
};
@ -161,10 +155,10 @@ tactic * mk_fail_if_undecided_tactic() {
return alloc(fail_if_undecided_tactic);
}
void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) {
void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, expr_dependency_ref & core) {
t.reset_statistics();
try {
t(in, result, mc, pc, core);
t(in, result, mc, core);
t.cleanup();
}
catch (tactic_exception & ex) {
@ -184,9 +178,8 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, model_converter_ref& m
core = 0;
ast_manager & m = g->m();
goal_ref_buffer r;
proof_converter_ref pc;
try {
exec(t, g, r, mc, pc, core);
exec(t, g, r, mc, core);
}
catch (tactic_exception & ex) {
reason_unknown = ex.msg();

5
src/tactic/tactic.h
View file

@ -78,7 +78,6 @@ public:
virtual void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result,
/* out */ model_converter_ref & mc,
/* out */ proof_converter_ref & pc,
/* out */ expr_dependency_ref & core) = 0;
virtual void collect_statistics(statistics & st) const {}
@ -119,7 +118,7 @@ void report_tactic_progress(char const * id, unsigned val);
class skip_tactic : public tactic {
public:
virtual void operator()(goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
virtual void operator()(goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, expr_dependency_ref & core);
virtual void cleanup() {}
virtual tactic * translate(ast_manager & m) { return this; }
};
@ -152,7 +151,7 @@ public:
#define MK_SIMPLE_TACTIC_FACTORY(NAME, ST) MK_TACTIC_FACTORY(NAME, return ST;)
void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, expr_dependency_ref & core);
lbool check_sat(tactic & t, goal_ref & g, model_ref & md, model_converter_ref& mc, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);
// Throws an exception if goal \c in requires proof generation.

181
src/tactic/tactical.cpp
View file

@ -109,7 +109,6 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
bool models_enabled = in->models_enabled();
@ -119,14 +118,12 @@ public:
ast_manager & m = in->m();
goal_ref_buffer r1;
model_converter_ref mc1;
proof_converter_ref pc1;
expr_dependency_ref core1(m);
result.reset();
mc = 0;
pc = 0;
mc = 0;
core = 0;
m_t1->operator()(in, r1, mc1, pc1, core1);
SASSERT(!is_decided(r1) || (!pc1 && !core1)); // the pc and core of decided goals is 0
m_t1->operator()(in, r1, mc1, core1);
SASSERT(!is_decided(r1) || !core1); // the pc and core of decided goals is 0
unsigned r1_size = r1.size();
SASSERT(r1_size > 0);
if (r1_size == 1) {
@ -136,24 +133,21 @@ public:
return;
}
goal_ref r1_0 = r1[0];
m_t2->operator()(r1_0, result, mc, pc, core);
m_t2->operator()(r1_0, result, mc, core);
if (models_enabled) mc = concat(mc1.get(), mc.get());
if (proofs_enabled) pc = concat(pc1.get(), pc.get());
if (cores_enabled) core = m.mk_join(core1.get(), core);
}
else {
if (cores_enabled) core = core1;
proof_converter_ref_buffer pc_buffer;
model_converter_ref_buffer mc_buffer;
sbuffer<unsigned> sz_buffer;
goal_ref_buffer r2;
for (unsigned i = 0; i < r1_size; i++) {
goal_ref g = r1[i];
r2.reset();
model_converter_ref mc2;
proof_converter_ref pc2;
expr_dependency_ref core2(m);
m_t2->operator()(g, r2, mc2, pc2, core2);
model_converter_ref mc2;
expr_dependency_ref core2(m);
m_t2->operator()(g, r2, mc2, core2);
if (is_decided(r2)) {
SASSERT(r2.size() == 1);
if (is_decided_sat(r2)) {
@ -167,17 +161,15 @@ public:
apply(mc1, md, i);
mc = model2model_converter(md.get());
}
SASSERT(!pc); SASSERT(!core);
SASSERT(!core);
return;
}
else {
SASSERT(is_decided_unsat(r2));
// the proof and unsat core of a decided_unsat goal are stored in the node itself.
// pc2 and core2 must be 0.
SASSERT(!pc2);
// core2 must be 0.
SASSERT(!core2);
if (models_enabled) mc_buffer.push_back(0);
if (proofs_enabled) pc_buffer.push_back(proof2proof_converter(m, r2[0]->pr(0)));
if (models_enabled || proofs_enabled) sz_buffer.push_back(0);
if (cores_enabled) core = m.mk_join(core.get(), r2[0]->dep(0));
}
@ -185,28 +177,37 @@ public:
else {
result.append(r2.size(), r2.c_ptr());
if (models_enabled) mc_buffer.push_back(mc2.get());
if (proofs_enabled) pc_buffer.push_back(pc2.get());
if (models_enabled || proofs_enabled) sz_buffer.push_back(r2.size());
if (cores_enabled) core = m.mk_join(core.get(), core2.get());
}
}
proof_converter_ref_buffer pc_buffer;
proof_converter_ref pc(in->pc());
if (proofs_enabled) {
for (goal* g : r1) {
pc_buffer.push_back(g->pc());
}
}
if (result.empty()) {
// all subgoals were shown to be unsat.
// create an decided_unsat goal with the proof
in->reset_all();
proof_ref pr(m);
if (proofs_enabled)
apply(m, pc1, pc_buffer, pr);
if (proofs_enabled) {
apply(m, pc, pc_buffer, pr);
in->set(proof2proof_converter(m, pr));
}
SASSERT(cores_enabled || core == 0);
in->assert_expr(m.mk_false(), pr, core);
core = 0;
result.push_back(in.get());
SASSERT(!mc); SASSERT(!pc); SASSERT(!core);
SASSERT(!mc); SASSERT(!core);
}
else {
if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_buffer.c_ptr(), sz_buffer.c_ptr());
if (proofs_enabled) pc = concat(pc1.get(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr());
if (proofs_enabled) in->set(concat(pc.get(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr()));
SASSERT(cores_enabled || core == 0);
}
}
@ -372,9 +373,9 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
goal orig(*(in.get()));
proof_converter_ref pc = in->pc();
unsigned sz = m_ts.size();
unsigned i;
for (i = 0; i < sz; i++) {
@ -386,14 +387,15 @@ public:
SASSERT(sz > 0);
if (i < sz - 1) {
try {
t->operator()(in, result, mc, pc, core);
t->operator()(in, result, mc, core);
return;
}
catch (tactic_exception &) {
in->set(pc.get());
}
}
else {
t->operator()(in, result, mc, pc, core);
t->operator()(in, result, mc, core);
return;
}
in->reset_all();
@ -471,7 +473,6 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
bool use_seq;
#ifdef _NO_OMP_
@ -481,7 +482,7 @@ public:
#endif
if (use_seq) {
// execute tasks sequentially
or_else_tactical::operator()(in, result, mc, pc, core);
or_else_tactical::operator()(in, result, mc, core);
return;
}
@ -510,14 +511,13 @@ public:
for (int i = 0; i < static_cast<int>(sz); i++) {
goal_ref_buffer _result;
model_converter_ref _mc;
proof_converter_ref _pc;
expr_dependency_ref _core(*(managers[i]));
goal_ref in_copy = in_copies[i];
tactic & t = *(ts.get(i));
try {
t(in_copy, _result, _mc, _pc, _core);
t(in_copy, _result, _mc, _core);
bool first = false;
#pragma omp critical (par_tactical)
{
@ -537,7 +537,6 @@ public:
result.push_back(_result[k]->translate(translator));
}
mc = _mc ? _mc->translate(translator) : 0;
pc = _pc ? _pc->translate(translator) : 0;
expr_dependency_translation td(translator);
core = td(_core);
}
@ -602,7 +601,6 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
bool use_seq;
#ifdef _NO_OMP_
@ -612,7 +610,7 @@ public:
#endif
if (use_seq) {
// execute tasks sequentially
and_then_tactical::operator()(in, result, mc, pc, core);
and_then_tactical::operator()(in, result, mc, core);
return;
}
@ -623,14 +621,12 @@ public:
ast_manager & m = in->m();
goal_ref_buffer r1;
model_converter_ref mc1;
proof_converter_ref pc1;
expr_dependency_ref core1(m);
result.reset();
mc = 0;
pc = 0;
core = 0;
m_t1->operator()(in, r1, mc1, pc1, core1);
SASSERT(!is_decided(r1) || (!pc1 && !core1)); // the pc and core of decided goals is 0
m_t1->operator()(in, r1, mc1, core1);
SASSERT(!is_decided(r1) || !core1); // the core of decided goals is 0
unsigned r1_size = r1.size();
SASSERT(r1_size > 0);
if (r1_size == 1) {
@ -638,13 +634,12 @@ public:
if (r1[0]->is_decided()) {
result.push_back(r1[0]);
if (models_enabled) mc = mc1;
SASSERT(!pc); SASSERT(!core);
SASSERT(!core);
return;
}
goal_ref r1_0 = r1[0];
m_t2->operator()(r1_0, result, mc, pc, core);
m_t2->operator()(r1_0, result, mc, core);
if (models_enabled) mc = concat(mc1.get(), mc.get());
if (proofs_enabled) pc = concat(pc1.get(), pc.get());
if (cores_enabled) core = m.mk_join(core1.get(), core);
}
else {
@ -662,15 +657,15 @@ public:
ts2.push_back(m_t2->translate(*new_m));
}
proof_converter_ref_buffer pc_buffer;
model_converter_ref_buffer mc_buffer;
proof_converter_ref_buffer pc_buffer;
scoped_ptr_vector<expr_dependency_ref> core_buffer;
scoped_ptr_vector<goal_ref_buffer> goals_vect;
pc_buffer.resize(r1_size);
mc_buffer.resize(r1_size);
core_buffer.resize(r1_size);
goals_vect.resize(r1_size);
pc_buffer.resize(r1_size);
bool found_solution = false;
bool failed = false;
@ -685,13 +680,12 @@ public:
goal_ref_buffer r2;
model_converter_ref mc2;
proof_converter_ref pc2;
expr_dependency_ref core2(new_m);
bool curr_failed = false;
try {
ts2[i]->operator()(new_g, r2, mc2, pc2, core2);
ts2[i]->operator()(new_g, r2, mc2, core2);
}
catch (tactic_exception & ex) {
#pragma omp critical (par_and_then_tactical)
@ -766,14 +760,13 @@ public:
apply(mc1, md, i);
mc = model2model_converter(md.get());
}
SASSERT(!pc); SASSERT(!core);
SASSERT(!core);
}
}
else {
SASSERT(is_decided_unsat(r2));
// the proof and unsat core of a decided_unsat goal are stored in the node itself.
// pc2 and core2 must be 0.
SASSERT(!pc2);
SASSERT(!core2);
if (models_enabled) mc_buffer.set(i, 0);
@ -793,7 +786,7 @@ public:
goals_vect.set(i, new_r2);
new_r2->append(r2.size(), r2.c_ptr());
mc_buffer.set(i, mc2.get());
pc_buffer.set(i, pc2.get());
pc_buffer.set(i, new_g->pc());
if (cores_enabled && core2 != 0) {
expr_dependency_ref * new_dep = alloc(expr_dependency_ref, new_m);
*new_dep = core2;
@ -841,22 +834,30 @@ public:
}
}
if (result.empty()) {
// all subgoals were shown to be unsat.
// create an decided_unsat goal with the proof
in->reset_all();
proof_ref pr(m);
if (proofs_enabled)
apply(m, pc1, pc_buffer, pr);
if (proofs_enabled) {
proof_converter_ref_buffer pc_buffer;
for (goal_ref g : r1) {
pc_buffer.push_back(g->pc());
}
proof_converter_ref pc = in->pc();
apply(m, pc, pc_buffer, pr);
in->set(proof2proof_converter(m, pr));
}
SASSERT(cores_enabled || core == 0);
in->assert_expr(m.mk_false(), pr, core);
core = 0;
result.push_back(in.get());
SASSERT(!mc); SASSERT(!pc); SASSERT(!core);
SASSERT(!mc); SASSERT(!core);
}
else {
if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_buffer.c_ptr(), sz_buffer.c_ptr());
if (proofs_enabled) pc = concat(pc1.get(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr());
if (proofs_enabled) in->set(concat(in->pc(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr()));
SASSERT(cores_enabled || core == 0);
}
}
@ -902,9 +903,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
m_t->operator()(in, result, mc, pc, core);
m_t->operator()(in, result, mc, core);
}
virtual void cleanup(void) { m_t->cleanup(); }
@ -931,13 +931,11 @@ class repeat_tactical : public unary_tactical {
goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
// TODO: implement a non-recursive version.
if (depth > m_max_depth) {
result.push_back(in.get());
mc = 0;
pc = 0;
core = 0;
return;
}
@ -949,20 +947,17 @@ class repeat_tactical : public unary_tactical {
ast_manager & m = in->m();
goal_ref_buffer r1;
model_converter_ref mc1;
proof_converter_ref pc1;
expr_dependency_ref core1(m);
result.reset();
mc = 0;
pc = 0;
core = 0;
{
goal orig_in(in->m(), proofs_enabled, models_enabled, cores_enabled);
orig_in.copy_from(*(in.get()));
m_t->operator()(in, r1, mc1, pc1, core1);
m_t->operator()(in, r1, mc1, core1);
if (is_equal(orig_in, *(in.get()))) {
result.push_back(r1[0]);
if (models_enabled) mc = mc1;
if (proofs_enabled) pc = pc1;
if (cores_enabled) core = core1;
return;
}
@ -973,28 +968,25 @@ class repeat_tactical : public unary_tactical {
if (r1[0]->is_decided()) {
result.push_back(r1[0]);
if (models_enabled) mc = mc1;
SASSERT(!pc); SASSERT(!core);
SASSERT(!core);
return;
}
goal_ref r1_0 = r1[0];
operator()(depth+1, r1_0, result, mc, pc, core);
operator()(depth+1, r1_0, result, mc, core);
if (models_enabled) mc = concat(mc.get(), mc1.get());
if (proofs_enabled) pc = concat(pc.get(), pc1.get());
if (cores_enabled) core = m.mk_join(core1.get(), core);
}
else {
if (cores_enabled) core = core1;
proof_converter_ref_buffer pc_buffer;
model_converter_ref_buffer mc_buffer;
sbuffer<unsigned> sz_buffer;
goal_ref_buffer r2;
for (unsigned i = 0; i < r1_size; i++) {
goal_ref g = r1[i];
r2.reset();
model_converter_ref mc2;
proof_converter_ref pc2;
model_converter_ref mc2;
expr_dependency_ref core2(m);
operator()(depth+1, g, r2, mc2, pc2, core2);
operator()(depth+1, g, r2, mc2, core2);
if (is_decided(r2)) {
SASSERT(r2.size() == 1);
if (is_decided_sat(r2)) {
@ -1007,15 +999,13 @@ class repeat_tactical : public unary_tactical {
if (mc1) (*mc1)(md, i);
mc = model2model_converter(md.get());
}
SASSERT(!pc); SASSERT(!core);
SASSERT(!core);
return;
}
else {
SASSERT(is_decided_unsat(r2));
SASSERT(!pc2);
SASSERT(!core2);
if (models_enabled) mc_buffer.push_back(0);
if (proofs_enabled) pc_buffer.push_back(proof2proof_converter(m, r2[0]->pr(0)));
if (models_enabled || proofs_enabled) sz_buffer.push_back(0);
if (cores_enabled) core = m.mk_join(core.get(), r2[0]->dep(0));
}
@ -1023,28 +1013,35 @@ class repeat_tactical : public unary_tactical {
else {
result.append(r2.size(), r2.c_ptr());
if (models_enabled) mc_buffer.push_back(mc2.get());
if (proofs_enabled) pc_buffer.push_back(pc2.get());
if (models_enabled || proofs_enabled) sz_buffer.push_back(r2.size());
if (cores_enabled) core = m.mk_join(core.get(), core2.get());
}
}
proof_converter_ref_buffer pc_buffer;
if (proofs_enabled) {
for (goal_ref g : r1) pc_buffer.push_back(g->pc());
}
if (result.empty()) {
// all subgoals were shown to be unsat.
// create an decided_unsat goal with the proof
in->reset_all();
proof_ref pr(m);
if (proofs_enabled)
apply(m, pc1, pc_buffer, pr);
if (proofs_enabled) {
proof_converter_ref pc = in->pc();
apply(m, pc, pc_buffer, pr);
in->set(proof2proof_converter(m, pr));
}
SASSERT(cores_enabled || core == 0);
in->assert_expr(m.mk_false(), pr, core);
core = 0;
result.push_back(in.get());
SASSERT(!mc); SASSERT(!pc); SASSERT(!core);
SASSERT(!mc); SASSERT(!core);
}
else {
if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_buffer.c_ptr(), sz_buffer.c_ptr());
if (proofs_enabled) pc = concat(pc1.get(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr());
if (proofs_enabled) in->set(concat(in->pc(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr()));
SASSERT(cores_enabled || core == 0);
}
}
@ -1059,9 +1056,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
operator()(0, in, result, mc, pc, core);
operator()(0, in, result, mc, core);
}
virtual tactic * translate(ast_manager & m) {
@ -1082,13 +1078,11 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
m_t->operator()(in, result, mc, pc, core);
m_t->operator()(in, result, mc, core);
if (result.size() > m_threshold) {
result.reset();
mc = 0;
pc = 0;
core = 0;
throw tactic_exception("failed-if-branching tactical");
}
@ -1111,9 +1105,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
m_t->operator()(in, result, mc, pc, core);
m_t->operator()(in, result, mc, core);
m_t->cleanup();
}
@ -1135,13 +1128,12 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
cancel_eh<reslimit> eh(in->m().limit());
{
// Warning: scoped_timer is not thread safe in Linux.
scoped_timer timer(m_timeout, &eh);
m_t->operator()(in, result, mc, pc, core);
m_t->operator()(in, result, mc, core);
}
}
@ -1205,10 +1197,9 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
scope _scope(m_name);
m_t->operator()(in, result, mc, pc, core);
m_t->operator()(in, result, mc, core);
}
virtual tactic * translate(ast_manager & m) {
@ -1239,12 +1230,11 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
if (m_p->operator()(*(in.get())).is_true())
m_t1->operator()(in, result, mc, pc, core);
m_t1->operator()(in, result, mc, core);
else
m_t2->operator()(in, result, mc, pc, core);
m_t2->operator()(in, result, mc, core);
}
virtual tactic * translate(ast_manager & m) {
@ -1280,10 +1270,8 @@ public:
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;
if (m_p->operator()(*(in.get())).is_true()) {
throw tactic_exception("fail-if tactic");
@ -1311,15 +1299,14 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
if (in->proofs_enabled()) {
mc = 0; pc = 0; core = 0;
mc = 0; core = 0;
result.reset();
result.push_back(in.get());
}
else {
m_t->operator()(in, result, mc, pc, core);
m_t->operator()(in, result, mc, core);
}
}
@ -1333,15 +1320,14 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
if (in->unsat_core_enabled()) {
mc = 0; pc = 0; core = 0;
mc = 0; core = 0;
result.reset();
result.push_back(in.get());
}
else {
m_t->operator()(in, result, mc, pc, core);
m_t->operator()(in, result, mc, core);
}
}
@ -1355,15 +1341,14 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
if (in->models_enabled()) {
mc = 0; pc = 0; core = 0;
mc = 0; core = 0;
result.reset();
result.push_back(in.get());
}
else {
m_t->operator()(in, result, mc, pc, core);
m_t->operator()(in, result, mc, core);
}
}

6
src/tactic/ufbv/macro_finder_tactic.cpp
View file

@ -40,10 +40,9 @@ class macro_finder_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("macro-finder", *g);
bool produce_proofs = g->proofs_enabled();
@ -120,9 +119,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

6
src/tactic/ufbv/quasi_macros_tactic.cpp
View file

@ -38,10 +38,9 @@ class quasi_macros_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("quasi-macros", *g);
bool produce_proofs = g->proofs_enabled();
@ -131,9 +130,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

6
src/tactic/ufbv/ufbv_rewriter_tactic.cpp
View file

@ -34,10 +34,9 @@ class ufbv_rewriter_tactic : public tactic {
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;
mc = 0; core = 0;
tactic_report report("ufbv-rewriter", *g);
fail_if_unsat_core_generation("ufbv-rewriter", g);
@ -103,9 +102,8 @@ public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
(*m_imp)(in, result, mc, core);
}
virtual void cleanup() {

3
src/util/ref_buffer.h
View file

@ -82,6 +82,9 @@ public:
return m_buffer[idx];
}
T* const* begin() const { return c_ptr(); }
T* const* end() const { return c_ptr() + size(); }
void set(unsigned idx, T * n) {
inc_ref(n);
dec_ref(m_buffer[idx]);