diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5961b2a65..484d3e9f5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -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) diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 82ef19274..b9cdc706c 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -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()); diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index ccb1ce597..3ee65ba36 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -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) { diff --git a/src/cmd_context/echo_tactic.cpp b/src/cmd_context/echo_tactic.cpp index 848ae5429..3b4f8962f 100644 --- a/src/cmd_context/echo_tactic.cpp +++ b/src/cmd_context/echo_tactic.cpp @@ -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); } }; diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index cd5eff9a6..1cdde738e 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -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; diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp index 6a7bc11e8..cb5cf9703 100644 --- a/src/math/subpaving/tactic/subpaving_tactic.cpp +++ b/src/math/subpaving/tactic/subpaving_tactic.cpp @@ -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) { diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index ded33bb0d..5fd41facc 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -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 { diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 37d80e2d6..e3681d366 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -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(); diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp index 4a77d2f5f..83b0d2c00 100644 --- a/src/muz/pdr/pdr_farkas_learner.cpp +++ b/src/muz/pdr/pdr_farkas_learner.cpp @@ -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]; diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index b057730d8..484456640 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -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]; diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp index 679736add..5c7fae9ac 100644 --- a/src/muz/spacer/spacer_legacy_frames.cpp +++ b/src/muz/spacer/spacer_legacy_frames.cpp @@ -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(); diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 83042cd6d..05c26b923 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -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]; diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 510f503e7..5757220b4 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -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; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 2ab6abd79..19cfc4b9c 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -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(); diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 1f9c89f89..e593e6627 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -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 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) { diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 257331161..c7b16417c 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -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); } diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp index 69ebc1a42..6f09df5b6 100644 --- a/src/qe/qe_sat_tactic.cpp +++ b/src/qe/qe_sat_tactic.cpp @@ -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 { diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp index e198542c1..ce1b3003a 100644 --- a/src/qe/qe_tactic.cpp +++ b/src/qe/qe_tactic.cpp @@ -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); diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 56f2ff985..3040a68fe 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -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 fmls; expr_ref_vector defs(m); expr_ref fml(m); - mc = 0; pc = 0; core = 0; + mc = 0; core = 0; in->get_formulas(fmls); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 37f8b5d16..29de5f107 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -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); diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 7b48986c5..ba6b53e17 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -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) { diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index edc4b4ff5..5b2537b9b 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -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()); diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 77024dba6..08ce9bded 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -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 << " " diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp index 68a34cea8..f02829af0 100644 --- a/src/smt/tactic/unit_subsumption_tactic.cpp +++ b/src/smt/tactic/unit_subsumption_tactic.cpp @@ -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) { diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index a44463a75..7d3076643 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -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 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 core; diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp index 37ffc6124..e51dc527c 100644 --- a/src/tactic/aig/aig_tactic.cpp +++ b/src/tactic/aig/aig_tactic.cpp @@ -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()); diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index ac105eb06..50a30b0ef 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -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() { diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp index b750689b1..bc7d4b51f 100644 --- a/src/tactic/arith/arith_bounds_tactic.cpp +++ b/src/tactic/arith/arith_bounds_tactic.cpp @@ -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); } diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 2e4782b2c..c2715da7a 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -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); diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index 519fec742..06e81bc68 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -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() { diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index 651000297..1bc1c4b73 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -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() { diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp index 68534c60b..dd1dfbd7e 100644 --- a/src/tactic/arith/elim01_tactic.cpp +++ b/src/tactic/arith/elim01_tactic.cpp @@ -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); diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index 492b12fcf..819b8cb94 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -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(); diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index d187c0078..e4ab1ca05 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -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; diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 2abfc32ea..68d31621f 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -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()); diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 48f584169..c53ef7274 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -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); } }; diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index ec41f5845..dfe7037f4 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -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); diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 89c43e647..a1834a73a 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -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()); diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index 547af63bf..65ed8ffbe 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -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); diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index 8f95dac8a..afc165866 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -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()); diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index f391e2a17..76f003737 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -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() { diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp index d7209740f..e52668f33 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.cpp +++ b/src/tactic/arith/propagate_ineqs_tactic.cpp @@ -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()); diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index af2b3581f..2affd8012 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -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(); diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index 9425b90ef..11144c89b 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -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()); diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index 308b775a4..d7df2e1c4 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -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()); diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index e7e374184..9dc247455 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -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() { diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index b71b44bd0..487bbb762 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -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()); diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 4435bf6a3..e3a5edd84 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -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()); diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index 3598a767c..3aba9a073 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -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() { diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 0d83e313a..722d2d359 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -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(); diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index a0f78154f..a86b41dcc 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -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() { diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index b0affeb4b..8a6090ca3 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -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() { diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index 698da8498..7a6643568 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -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() { diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp index 65cdef147..d139d60e9 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ b/src/tactic/core/cofactor_term_ite_tactic.cpp @@ -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()); diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index 26f6842e3..b71c566d6 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -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); diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 5bb54073d..43371235c 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -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()); diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index 9efa7e7db..2ad6e9243 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -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(); diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp index 5df009969..1151d6770 100644 --- a/src/tactic/core/der_tactic.cpp +++ b/src/tactic/core/der_tactic.cpp @@ -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()); diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp index 3ee2697c4..16e2c5f78 100644 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ b/src/tactic/core/distribute_forall_tactic.cpp @@ -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); diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 2099eebf0..d175ba0c4 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -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())); diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 56eea8d9a..fd4e9e49b 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -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(); diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index d6fb8a091..3f65f4b9d 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -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() { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index aa5d55a8c..3660fdccb 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -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()); } diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 7d90a2155..4c03254c4 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -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); diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index 9750ad29c..080fc0bec 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -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(); diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index 66143b6b5..8ce514401 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -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() { diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index c52f0526b..897d560cf 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -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"); diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 7baac0b99..61804d336 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -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()); diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index a7a73ae61..aa53cd9cc 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -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()); diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index 9deff968e..84ade7ba3 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -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()); diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h index 1e8420c62..f14f219d4 100644 --- a/src/tactic/core/simplify_tactic.h +++ b/src/tactic/core/simplify_tactic.h @@ -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(); diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index c4f315985..6fbefcba3 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -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()); } diff --git a/src/tactic/core/split_clause_tactic.cpp b/src/tactic/core/split_clause_tactic.cpp index a120f2910..f383036f7 100644 --- a/src/tactic/core/split_clause_tactic.cpp +++ b/src/tactic/core/split_clause_tactic.cpp @@ -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++) { diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index 8e87a6741..89013a6da 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/src/tactic/core/symmetry_reduce_tactic.cpp @@ -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()); diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index 4791b5ce6..22a2dc500 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -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); } diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 6d90b46ea..99b50429c 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -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()); diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 311c9838b..7a98be3f1 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -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::iterator it = deps.begin(); - ptr_vector::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::iterator it = to_pp.begin(); - obj_hashtable::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::iterator it = deps.begin(); - ptr_vector::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; } diff --git a/src/tactic/goal.h b/src/tactic/goal.h index 599fae14f..275c80060 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -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; }; diff --git a/src/tactic/nlsat_smt/CMakeLists.txt b/src/tactic/nlsat_smt/CMakeLists.txt deleted file mode 100644 index ccfc0e3ef..000000000 --- a/src/tactic/nlsat_smt/CMakeLists.txt +++ /dev/null @@ -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 -) diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp deleted file mode 100644 index e389c960c..000000000 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ /dev/null @@ -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 m_fmc; - tactic_ref m_nl_tac; // nlsat tactic - goal_ref m_nl_g; // nlsat goal - ref m_solver; // SMT solver - expr_ref_vector m_eq_preds; // predicates for equality between pairs of interface variables - svector 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 m_ctx_asms; // assumptions passed by context - obj_hashtable m_ctx_asms_set; // assumptions passed by context - obj_hashtable m_used_asms; - obj_map m_bool2dep; - obj_pair_map m_eq_pairs; // map pairs of interface variables to auxiliary predicates - obj_map m_interface_cache; // map of compound real expression to interface variable. - obj_map 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& m_polarities; - obj_map& 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 m_cfg; - public: - rw(nl_purify_tactic & o): - rewriter_tpl(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 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& core, ptr_vector& 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::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 num2var; - obj_map::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 forms; - svector 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 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& is_pure, expr* e0) { - ptr_vector 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); -} diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.h b/src/tactic/nlsat_smt/nl_purify_tactic.h deleted file mode 100644 index 85d033921..000000000 --- a/src/tactic/nlsat_smt/nl_purify_tactic.h +++ /dev/null @@ -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 - diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index e9c6d76aa..16eb2b4a7 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -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); diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 64689602c..4e4efeb8f 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -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();); diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 19937e8b0..a96cf117a 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -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); diff --git a/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt index c90fd7468..2741334b4 100644 --- a/src/tactic/smtlogics/CMakeLists.txt +++ b/src/tactic/smtlogics/CMakeLists.txt @@ -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 ) diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index e89da3631..a4995535e 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -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()); diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 7610c420a..3a8e128ec 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -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(); diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 93da52366..3b8110fd2 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -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. diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index c5a70c0db..3f94908b3 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -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 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(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 core_buffer; scoped_ptr_vector 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 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 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); } } diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 7a1838452..71034b2b1 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -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() { diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index ee3cd14ec..c8c1f2b0f 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -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() { diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index 615593317..e4ba71ad7 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -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() { diff --git a/src/util/ref_buffer.h b/src/util/ref_buffer.h index 612dde2da..4768c3f28 100644 --- a/src/util/ref_buffer.h +++ b/src/util/ref_buffer.h @@ -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]);