From 4bbece661600c891672d3b2d8197db8368588bc0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 18 Nov 2017 16:33:54 -0800 Subject: [PATCH] re-organize proof and model converters to be associated with goals instead of external Signed-off-by: Nikolaj Bjorner --- .../ackermannize_bv_tactic.cpp | 5 +- src/api/api_goal.cpp | 15 + src/api/api_tactic.cpp | 41 +-- src/api/c++/z3++.h | 17 +- src/api/dotnet/ApplyResult.cs | 13 - src/api/dotnet/Goal.cs | 15 + src/api/java/ApplyResult.java | 13 - src/api/java/Goal.java | 15 + src/api/python/z3/z3.py | 65 ++-- src/api/z3_api.h | 17 +- src/cmd_context/echo_tactic.cpp | 6 +- src/cmd_context/tactic_cmds.cpp | 10 +- .../subpaving/tactic/subpaving_tactic.cpp | 2 - src/muz/base/dl_util.cpp | 15 +- src/muz/fp/horn_tactic.cpp | 10 +- src/muz/pdr/pdr_context.cpp | 5 +- src/muz/pdr/pdr_farkas_learner.cpp | 3 +- src/muz/pdr/pdr_manager.cpp | 2 +- src/muz/spacer/spacer_context.cpp | 7 +- src/muz/spacer/spacer_legacy_frames.cpp | 3 +- src/muz/spacer/spacer_manager.cpp | 2 +- src/muz/spacer/spacer_util.cpp | 6 +- src/muz/tab/tab_context.cpp | 2 +- src/muz/transforms/dl_mk_slice.cpp | 15 +- src/nlsat/tactic/nlsat_tactic.cpp | 12 +- src/opt/opt_context.cpp | 9 +- src/qe/nlqsat.cpp | 8 +- src/qe/qe_lite.cpp | 6 +- src/qe/qe_sat_tactic.cpp | 11 +- src/qe/qe_tactic.cpp | 6 +- src/qe/qsat.cpp | 5 +- src/sat/sat_solver/inc_sat_solver.cpp | 3 +- src/sat/tactic/goal2sat.cpp | 3 +- src/sat/tactic/sat_tactic.cpp | 10 +- src/smt/smt_solver.cpp | 2 +- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 3 +- src/smt/tactic/smt_tactic.cpp | 7 +- src/smt/tactic/unit_subsumption_tactic.cpp | 1 - src/solver/solver2tactic.cpp | 7 +- src/solver/tactic2solver.cpp | 3 +- src/tactic/aig/aig_tactic.cpp | 3 +- src/tactic/arith/add_bounds_tactic.cpp | 6 +- src/tactic/arith/arith_bounds_tactic.cpp | 1 - src/tactic/arith/card2bv_tactic.cpp | 9 +- src/tactic/arith/degree_shift_tactic.cpp | 8 +- src/tactic/arith/diff_neq_tactic.cpp | 11 +- src/tactic/arith/elim01_tactic.cpp | 17 +- src/tactic/arith/eq2bv_tactic.cpp | 5 +- src/tactic/arith/factor_tactic.cpp | 6 +- src/tactic/arith/fix_dl_var_tactic.cpp | 12 +- src/tactic/arith/fm_tactic.cpp | 10 +- src/tactic/arith/lia2card_tactic.cpp | 11 +- src/tactic/arith/lia2pb_tactic.cpp | 10 +- src/tactic/arith/nla2bv_tactic.cpp | 6 +- src/tactic/arith/normalize_bounds_tactic.cpp | 13 +- src/tactic/arith/pb2bv_model_converter.cpp | 63 ++-- src/tactic/arith/pb2bv_model_converter.h | 7 +- src/tactic/arith/pb2bv_tactic.cpp | 10 +- src/tactic/arith/propagate_ineqs_tactic.cpp | 5 +- src/tactic/arith/purify_arith_tactic.cpp | 9 +- src/tactic/arith/recover_01_tactic.cpp | 25 +- src/tactic/bv/bit_blaster_model_converter.cpp | 7 +- src/tactic/bv/bit_blaster_tactic.cpp | 12 +- src/tactic/bv/bv1_blaster_tactic.cpp | 8 +- src/tactic/bv/bv_bound_chk_tactic.cpp | 4 +- src/tactic/bv/bv_size_reduction_tactic.cpp | 7 +- src/tactic/bv/bvarray2uf_tactic.cpp | 8 +- src/tactic/bv/dt2bv_tactic.cpp | 5 +- src/tactic/bv/elim_small_bv_tactic.cpp | 8 +- src/tactic/bv/max_bv_sharing_tactic.cpp | 6 +- src/tactic/core/blast_term_ite_tactic.cpp | 6 +- src/tactic/core/cofactor_term_ite_tactic.cpp | 3 +- src/tactic/core/collect_statistics_tactic.cpp | 8 +- src/tactic/core/ctx_simplify_tactic.cpp | 3 +- src/tactic/core/ctx_simplify_tactic.h | 1 - src/tactic/core/der_tactic.cpp | 3 +- src/tactic/core/distribute_forall_tactic.cpp | 3 +- src/tactic/core/dom_simplify_tactic.cpp | 3 +- src/tactic/core/dom_simplify_tactic.h | 1 - src/tactic/core/elim_term_ite_tactic.cpp | 8 +- src/tactic/core/elim_uncnstr_tactic.cpp | 18 +- src/tactic/core/injectivity_tactic.cpp | 6 +- src/tactic/core/nnf_tactic.cpp | 5 +- src/tactic/core/occf_tactic.cpp | 8 +- src/tactic/core/pb_preprocess_tactic.cpp | 6 +- src/tactic/core/propagate_values_tactic.cpp | 6 +- src/tactic/core/reduce_args_tactic.cpp | 13 +- src/tactic/core/simplify_tactic.cpp | 3 +- src/tactic/core/simplify_tactic.h | 1 - src/tactic/core/solve_eqs_tactic.cpp | 9 +- src/tactic/core/split_clause_tactic.cpp | 52 ++- src/tactic/core/symmetry_reduce_tactic.cpp | 4 +- src/tactic/core/tseitin_cnf_tactic.cpp | 10 +- src/tactic/equiv_proof_converter.h | 8 +- src/tactic/fpa/fpa2bv_model_converter.h | 10 +- src/tactic/fpa/fpa2bv_tactic.cpp | 10 +- src/tactic/generic_model_converter.cpp | 5 +- src/tactic/generic_model_converter.h | 14 +- src/tactic/model_converter.cpp | 92 +---- src/tactic/model_converter.h | 27 +- .../portfolio/bounded_int2bv_solver.cpp | 4 +- src/tactic/portfolio/enum2bv_solver.cpp | 4 +- src/tactic/portfolio/parallel_tactic.cpp | 5 +- src/tactic/portfolio/pb2bv_solver.cpp | 2 +- src/tactic/proof_converter.cpp | 100 ++--- src/tactic/proof_converter.h | 23 +- src/tactic/replace_proof_converter.cpp | 9 +- src/tactic/replace_proof_converter.h | 6 +- src/tactic/sine_filter.cpp | 5 +- src/tactic/sls/sls_tactic.cpp | 6 +- src/tactic/smtlogics/qfufbv_tactic.cpp | 4 +- src/tactic/tactic.cpp | 54 ++- src/tactic/tactic.h | 27 +- src/tactic/tactical.cpp | 343 +++++------------- src/tactic/ufbv/macro_finder_tactic.cpp | 9 +- src/tactic/ufbv/quasi_macros_tactic.cpp | 9 +- src/tactic/ufbv/ufbv_rewriter_tactic.cpp | 9 +- src/test/horn_subsume_model_converter.cpp | 10 +- 118 files changed, 617 insertions(+), 1070 deletions(-) diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index b9cdc706c..a38b19c7d 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -31,9 +31,7 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; tactic_report report("ackermannize", *g); fail_if_unsat_core_generation("ackermannize", g); fail_if_proof_generation("ackermannize", g); @@ -51,14 +49,13 @@ public: TRACE("ackermannize", tout << "ackermannize not run due to limit" << std::endl;); result.reset(); result.push_back(g.get()); - mc = 0; core = 0; return; } result.push_back(resg.get()); // report model if (g->models_enabled()) { - mc = mk_ackermannize_bv_model_converter(m, lackr.get_info()); + g->add(mk_ackermannize_bv_model_converter(m, lackr.get_info())); } resg->inc_depth(); diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index cf248c10e..cfda3e87c 100644 --- a/src/api/api_goal.cpp +++ b/src/api/api_goal.cpp @@ -21,6 +21,7 @@ Revision History: #include "api/api_context.h" #include "api/api_goal.h" #include "ast/ast_translation.h" +#include "api/api_model.h" extern "C" { @@ -151,6 +152,20 @@ extern "C" { Z3_CATCH_RETURN(Z3_FALSE); } + Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m) { + Z3_TRY; + LOG_Z3_goal_convert_model(c, g, m); + RESET_ERROR_CODE(); + model_ref new_m; + Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); + mk_c(c)->save_object(m_ref); + if (m) m_ref->m_model = to_model_ref(m)->copy(); + if (to_goal_ref(g)->mc()) + (*to_goal_ref(g)->mc())(m_ref->m_model); + RETURN_Z3(of_model(m_ref)); + Z3_CATCH_RETURN(0); + } + Z3_goal Z3_API Z3_goal_translate(Z3_context c, Z3_goal g, Z3_context target) { Z3_TRY; LOG_Z3_goal_translate(c, g, target); diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 3ee65ba36..2d9a47863 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -30,20 +30,20 @@ Z3_apply_result_ref::Z3_apply_result_ref(api::context& c, ast_manager & m): api: extern "C" { -#define RETURN_TACTIC(_t_) { \ +#define RETURN_TACTIC(_t_) { \ Z3_tactic_ref * _ref_ = alloc(Z3_tactic_ref, *mk_c(c)); \ - _ref_->m_tactic = _t_; \ - mk_c(c)->save_object(_ref_); \ - Z3_tactic _result_ = of_tactic(_ref_); \ - RETURN_Z3(_result_); \ + _ref_->m_tactic = _t_; \ + mk_c(c)->save_object(_ref_); \ + Z3_tactic _result_ = of_tactic(_ref_); \ + RETURN_Z3(_result_); \ } -#define RETURN_PROBE(_t_) { \ +#define RETURN_PROBE(_t_) { \ Z3_probe_ref * _ref_ = alloc(Z3_probe_ref, *mk_c(c)); \ - _ref_->m_probe = _t_; \ - mk_c(c)->save_object(_ref_); \ - Z3_probe _result_ = of_probe(_ref_); \ - RETURN_Z3(_result_); \ + _ref_->m_probe = _t_; \ + mk_c(c)->save_object(_ref_); \ + Z3_probe _result_ = of_probe(_ref_); \ + RETURN_Z3(_result_); \ } Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name) { @@ -418,8 +418,9 @@ 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_core); + exec(*to_tactic_ref(t), new_goal, ref->m_subgoals, ref->m_core); ref->m_pc = new_goal->pc(); + ref->m_mc = new_goal->mc(); return of_apply_result(ref); } catch (z3_exception & ex) { @@ -514,22 +515,4 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m) { - Z3_TRY; - LOG_Z3_apply_result_convert_model(c, r, i, m); - RESET_ERROR_CODE(); - if (i > to_apply_result(r)->m_subgoals.size()) { - SET_ERROR_CODE(Z3_IOB); - RETURN_Z3(0); - } - model_ref new_m = to_model_ref(m)->copy(); - if (to_apply_result(r)->m_mc) - to_apply_result(r)->m_mc->operator()(new_m, i); - Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); - m_ref->m_model = new_m; - mk_c(c)->save_object(m_ref); - RETURN_Z3(of_model(m_ref)); - Z3_CATCH_RETURN(0); - } - }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index a2937cb8e..428f210ee 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2104,6 +2104,17 @@ namespace z3 { unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); } bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; } bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; } + model convert_model(model const & m) const { + check_context(*this, m); + Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m); + check_error(); + return model(ctx(), new_m); + } + model get_model() const { + Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0); + check_error(); + return model(ctx(), new_m); + } expr as_expr() const { unsigned n = size(); if (n == 0) @@ -2142,12 +2153,6 @@ namespace z3 { } unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); } goal operator[](int i) const { assert(0 <= i); Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); } - model convert_model(model const & m, unsigned i = 0) const { - check_context(*this, m); - Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m); - check_error(); - return model(ctx(), new_m); - } friend std::ostream & operator<<(std::ostream & out, apply_result const & r); }; inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; } diff --git a/src/api/dotnet/ApplyResult.cs b/src/api/dotnet/ApplyResult.cs index 608be7080..db2922460 100644 --- a/src/api/dotnet/ApplyResult.cs +++ b/src/api/dotnet/ApplyResult.cs @@ -55,19 +55,6 @@ namespace Microsoft.Z3 } } - /// - /// Convert a model for the subgoal into a model for the original - /// goal g, that the ApplyResult was obtained from. - /// - /// A model for g - public Model ConvertModel(uint i, Model m) - { - Contract.Requires(m != null); - Contract.Ensures(Contract.Result() != null); - - return new Model(Context, Native.Z3_apply_result_convert_model(Context.nCtx, NativeObject, i, m.NativeObject)); - } - /// /// A string representation of the ApplyResult. /// diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index 25aeba741..03e573538 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -174,6 +174,21 @@ namespace Microsoft.Z3 get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; } } + /// + /// Convert a model for the goal into a model of the + /// original goal from which this goal was derived. + /// + /// A model for g + public Model ConvertModel(Model m) + { + Contract.Ensures(Contract.Result() != null); + if (m != null) + return new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, m.NativeObject)); + else + return new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, IntPtr.Zero)); + } + + /// /// Translates (copies) the Goal to the target Context . /// diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index 6fafbd888..6cfedd404 100644 --- a/src/api/java/ApplyResult.java +++ b/src/api/java/ApplyResult.java @@ -46,19 +46,6 @@ public class ApplyResult extends Z3Object { return res; } - /** - * Convert a model for the subgoal {@code i} into a model for the - * original goal {@code g}, that the ApplyResult was obtained from. - * - * @return A model for {@code g} - * @throws Z3Exception - **/ - public Model convertModel(int i, Model m) - { - return new Model(getContext(), - Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject())); - } - /** * A string representation of the ApplyResult. **/ diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index 25b1fe511..903325850 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -240,6 +240,21 @@ public class Goal extends Z3Object { (unsatCores), (proofs))); } + /** + * Convert a model for the goal into a model of the + * original goal from which this goal was derived. + * + * @return A model for {@code g} + * @throws Z3Exception + **/ + public Model convertModel(Model m) + { + return new Model(getContext(), + Native.goalConvertModel(getContext().nCtx(), getNativeObject(), m.getNativeObject())); + } + + + @Override void incRef() { Native.goalIncRef(getContext().nCtx(), getNativeObject()); diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index e281a1273..f911732ef 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4964,6 +4964,35 @@ class Goal(Z3PPObject): """ self.assert_exprs(*args) + def convert_model(self, model): + """Retrieve model from a satisfiable goal + >>> a, b = Ints('a b') + >>> g = Goal() + >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) + >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs')) + >>> r = t(g) + >>> r[0] + [Or(b == 0, b == 1), Not(0 <= b)] + >>> r[1] + [Or(b == 0, b == 1), Not(1 <= b)] + >>> # Remark: the subgoal r[0] is unsatisfiable + >>> # Creating a solver for solving the second subgoal + >>> s = Solver() + >>> s.add(r[1]) + >>> s.check() + sat + >>> s.model() + [b = 0] + >>> # Model s.model() does not assign a value to `a` + >>> # It is a model for subgoal `r[1]`, but not for goal `g` + >>> # The method convert_model creates a model for `g` from a model for `r[1]`. + >>> r[1].convert_model(s.model()) + [b = 0, a = 1] + """ + if __debug__: + _z3_assert(isinstance(model, ModelRef), "Z3 Model expected") + return ModelRef(Z3_goal_convert_model(self.ctx.ref(), self.goal, model.model), self.ctx) + def __repr__(self): return obj_to_string(self) @@ -7072,36 +7101,6 @@ class ApplyResult(Z3PPObject): """Return a textual representation of the s-expression representing the set of subgoals in `self`.""" return Z3_apply_result_to_string(self.ctx.ref(), self.result) - def convert_model(self, model, idx=0): - """Convert a model for a subgoal into a model for the original goal. - - >>> a, b = Ints('a b') - >>> g = Goal() - >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) - >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs')) - >>> r = t(g) - >>> r[0] - [Or(b == 0, b == 1), Not(0 <= b)] - >>> r[1] - [Or(b == 0, b == 1), Not(1 <= b)] - >>> # Remark: the subgoal r[0] is unsatisfiable - >>> # Creating a solver for solving the second subgoal - >>> s = Solver() - >>> s.add(r[1]) - >>> s.check() - sat - >>> s.model() - [b = 0] - >>> # Model s.model() does not assign a value to `a` - >>> # It is a model for subgoal `r[1]`, but not for goal `g` - >>> # The method convert_model creates a model for `g` from a model for `r[1]`. - >>> r.convert_model(s.model(), 1) - [b = 0, a = 1] - """ - if __debug__: - _z3_assert(idx < len(self), "index out of bounds") - _z3_assert(isinstance(model, ModelRef), "Z3 Model expected") - return ModelRef(Z3_apply_result_convert_model(self.ctx.ref(), self.result, idx, model.model), self.ctx) def as_expr(self): """Return a Z3 expression consisting of all subgoals. @@ -8057,13 +8056,13 @@ def parse_smt2_string(s, sorts={}, decls={}, ctx=None): the symbol table used for the SMT 2.0 parser. >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') - And(x > 0, x < 10) + [x > 0, x < 10] >>> x, y = Ints('x y') >>> f = Function('f', IntSort(), IntSort()) >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) - x + f(y) > 0 + [x + f(y) > 0] >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) - a > 0 + [a > 0] """ ctx = _get_ctx(ctx) ssz, snames, ssorts = _dict2sarray(sorts, ctx) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 67fc0c903..c9603c018 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5561,6 +5561,15 @@ extern "C" { */ Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target); + /** + \brief Convert a model of the formulas of a goal to a model of an original goal. + The model may be null, in which case the returned model is valid if the goal was + established satisfiable. + + def_API('Z3_goal_convert_model', MODEL, (_in(CONTEXT), _in(GOAL), _in(MODEL))) + */ + Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m); + /** \brief Convert a goal into a string. @@ -5927,14 +5936,6 @@ extern "C" { */ Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i); - /** - \brief Convert a model for the subgoal \c Z3_apply_result_get_subgoal(c, r, i) into a model for the original goal \c g. - Where \c g is the goal used to create \c r using \c Z3_tactic_apply(c, t, g). - - def_API('Z3_apply_result_convert_model', MODEL, (_in(CONTEXT), _in(APPLY_RESULT), _in(UINT), _in(MODEL))) - */ - Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m); - /*@}*/ /** @name Solvers*/ diff --git a/src/cmd_context/echo_tactic.cpp b/src/cmd_context/echo_tactic.cpp index 3b4f8962f..37dcc0a29 100644 --- a/src/cmd_context/echo_tactic.cpp +++ b/src/cmd_context/echo_tactic.cpp @@ -29,7 +29,6 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { #pragma omp critical (echo_tactic) { @@ -37,7 +36,7 @@ public: if (m_newline) m_ctx.regular_stream() << std::endl; } - skip_tactic::operator()(in, result, mc, core); + skip_tactic::operator()(in, result, core); } }; @@ -62,7 +61,6 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { double val = (*m_p)(*(in.get())).get_value(); #pragma omp critical (probe_value_tactic) @@ -73,7 +71,7 @@ public: if (m_newline) m_ctx.diagnostic_stream() << std::endl; } - skip_tactic::operator()(in, result, mc, core); + skip_tactic::operator()(in, result, core); } }; diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 1cdde738e..20f6fc632 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -213,7 +213,6 @@ public: assert_exprs_from(ctx, *g); TRACE("check_sat_using", g->display(tout);); model_ref md; - model_converter_ref mc; proof_ref pr(m); expr_dependency_ref core(m); std::string reason_unknown; @@ -229,7 +228,7 @@ public: cmd_context::scoped_watch sw(ctx); lbool r = l_undef; try { - r = check_sat(t, g, md, mc, result->labels, pr, core, reason_unknown); + r = check_sat(t, g, md, result->labels, pr, core, reason_unknown); ctx.display_sat_result(r); result->set_status(r); if (r == l_undef) { @@ -327,7 +326,6 @@ public: unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit); goal_ref_buffer result_goals; - model_converter_ref mc; expr_dependency_ref core(m); std::string reason_unknown; @@ -339,7 +337,7 @@ public: scoped_timer timer(timeout, &eh); cmd_context::scoped_watch sw(ctx); try { - exec(t, g, result_goals, mc, core); + exec(t, g, result_goals, core); } catch (tactic_exception & ex) { ctx.regular_stream() << "(error \"tactic failed: " << ex.msg() << "\")" << std::endl; @@ -398,8 +396,8 @@ public: } } - if (!failed && mc && p.get_bool("print_model_converter", false)) - mc->display(ctx.regular_stream()); + if (!failed && g->mc() && p.get_bool("print_model_converter", false)) + g->mc()->display(ctx.regular_stream()); if (p.get_bool("print_statistics", false)) display_statistics(ctx, tref.get()); diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp index cb5cf9703..5940dcbfc 100644 --- a/src/math/subpaving/tactic/subpaving_tactic.cpp +++ b/src/math/subpaving/tactic/subpaving_tactic.cpp @@ -243,14 +243,12 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { m_imp->process(*in); m_imp->collect_statistics(m_stats); result.reset(); result.push_back(in.get()); - mc = 0; core = 0; } catch (z3_exception & ex) { diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp index 463b78c4a..b781a8640 100644 --- a/src/muz/base/dl_util.cpp +++ b/src/muz/base/dl_util.cpp @@ -380,26 +380,29 @@ namespace datalog { public: skip_model_converter() {} - virtual model_converter * translate(ast_translation & translator) { + model_converter * translate(ast_translation & translator) override { return alloc(skip_model_converter); } - virtual void display(std::ostream & out) { } + void operator()(model_ref&) override {} + + void display(std::ostream & out) override { } }; model_converter* mk_skip_model_converter() { return alloc(skip_model_converter); } class skip_proof_converter : public proof_converter { - virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) { + + proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override { SASSERT(num_source == 1); - result = source[0]; + return proof_ref(source[0], m); } - virtual proof_converter * translate(ast_translation & translator) { + proof_converter * translate(ast_translation & translator) override { return alloc(skip_proof_converter); } - virtual void display(std::ostream & out) { out << "(skip-proof-converter)\n"; } + void display(std::ostream & out) override { out << "(skip-proof-converter)\n"; } }; proof_converter* mk_skip_proof_converter() { return alloc(skip_proof_converter); } diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 5fd41facc..4802bbb33 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -178,10 +178,9 @@ class horn_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("horn", *g); bool produce_proofs = g->proofs_enabled(); @@ -230,11 +229,12 @@ class horn_tactic : public tactic { queries.push_back(q); generic_model_converter* mc1 = alloc(generic_model_converter, m); mc1->hide(q); - mc = mc1; + g->add(mc1); } SASSERT(queries.size() == 1); q = queries[0].get(); proof_converter_ref pc = g->pc(); + model_converter_ref mc; if (m_is_simplify) { simplify(q, g, result, mc, pc); } @@ -242,6 +242,7 @@ class horn_tactic : public tactic { verify(q, g, result, mc, pc); } g->set(pc.get()); + g->set(mc.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, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, 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 e3681d366..452be8914 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -202,10 +202,9 @@ namespace pdr { void pred_transformer::simplify_formulas(tactic& tac, expr_ref_vector& v) { 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; expr_dependency_ref core(m); goal_ref_buffer result; - tac(g, result, mc, core); + tac(g, result, core); SASSERT(result.size() == 1); goal* r = result[0]; v.reset(); @@ -390,7 +389,7 @@ namespace pdr { md->register_decl(m_head, fi); } model_converter_ref mc = ctx.get_model_converter(); - apply(mc, md, 0); + apply(mc, md); if (p_orig->get_arity() == 0) { result = md->get_const_interp(p_orig); } diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp index 83b0d2c00..68a9db2ef 100644 --- a/src/muz/pdr/pdr_farkas_learner.cpp +++ b/src/muz/pdr/pdr_farkas_learner.cpp @@ -520,11 +520,10 @@ namespace pdr { g->assert_expr(lemmas[i].get()); } expr_ref tmp(m); - model_converter_ref mc; expr_dependency_ref core(m); goal_ref_buffer result; tactic_ref simplifier = mk_arith_bounds_tactic(m); - (*simplifier)(g, result, mc, core); + (*simplifier)(g, result, core); lemmas.reset(); SASSERT(result.size() == 1); goal* r = result[0]; diff --git a/src/muz/pdr/pdr_manager.cpp b/src/muz/pdr/pdr_manager.cpp index 077d27427..da15bf094 100644 --- a/src/muz/pdr/pdr_manager.cpp +++ b/src/muz/pdr/pdr_manager.cpp @@ -107,7 +107,7 @@ namespace pdr { } } TRACE("pdr", model_smt2_pp(tout, m, *md, 0);); - apply(const_cast(m_mc), md, 0); + apply(const_cast(m_mc), md); } expr_ref inductive_property::to_expr() const { diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 484456640..d1350d29a 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -528,7 +528,7 @@ expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level) md->register_decl(m_head, fi); } model_converter_ref mc = ctx.get_model_converter(); - apply(mc, md, 0); + apply(mc, md); if (p_orig->get_arity() == 0) { result = md->get_const_interp(p_orig); } else { @@ -1367,7 +1367,6 @@ void pred_transformer::frames::simplify_formulas () // normalize level unsigned level = i < m_size ? i : infty_level (); - model_converter_ref mc; expr_dependency_ref core(m); goal_ref_buffer result; @@ -1394,7 +1393,7 @@ void pred_transformer::frames::simplify_formulas () } // more than one lemma at current level. simplify. - (*simplifier)(g, result, mc, core); + (*simplifier)(g, result, core); SASSERT(result.size () == 1); goal *r = result[0]; @@ -2062,8 +2061,8 @@ bool context::validate() expr_ref_vector refs(m); expr_ref tmp(m); model_ref model; - vector rs; model_converter_ref mc; + vector rs; get_level_property(m_inductive_lvl, refs, rs); inductive_property ex(m, mc, rs); ex.to_model(model); diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp index 5c7fae9ac..176e0101b 100644 --- a/src/muz/spacer/spacer_legacy_frames.cpp +++ b/src/muz/spacer/spacer_legacy_frames.cpp @@ -46,10 +46,9 @@ void pred_transformer::legacy_frames::simplify_formulas(tactic& tac, ast_manager &m = m_pt.get_ast_manager(); 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; expr_dependency_ref core(m); goal_ref_buffer result; - tac(g, result, mc, core); + tac(g, result, core); SASSERT(result.size() == 1); goal* r = result[0]; v.reset(); diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index 4ad3e0d7f..ba4ca0da7 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -113,7 +113,7 @@ void inductive_property::to_model(model_ref& md) const } } TRACE("spacer", model_smt2_pp(tout, m, *md, 0);); - apply(const_cast(m_mc), md, 0); + apply(const_cast(m_mc), md); } expr_ref inductive_property::to_expr() const diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 05c26b923..726ff86c8 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -929,11 +929,10 @@ void simplify_bounds_old(expr_ref_vector& cube) { } expr_ref tmp(m); - model_converter_ref mc; expr_dependency_ref core(m); goal_ref_buffer result; tactic_ref simplifier = mk_arith_bounds_tactic(m); - (*simplifier)(g, result, mc, core); + (*simplifier)(g, result, core); SASSERT(result.size() == 1); goal* r = result[0]; @@ -954,14 +953,13 @@ void simplify_bounds_new (expr_ref_vector &cube) { g->assert_expr(cube.get(i)); } - model_converter_ref mc; 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, dep); + (*t)(g, goals, dep); SASSERT(goals.size() == 1); g = goals[0]; diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index 8809c0dc7..ad3006508 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -1602,7 +1602,7 @@ namespace datalog { pc.invert(); prs.push_back(m.mk_asserted(root)); - pc(m, 1, prs.c_ptr(), pr); + pr = pc(m, 1, prs.c_ptr()); return pr; } diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index 8b38335e0..ce1b8e582 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -271,20 +271,21 @@ namespace datalog { m_renaming.insert(orig_rule, unsigned_vector(sz, renaming)); } - virtual void operator()(ast_manager& m, unsigned num_source, proof * const * source, proof_ref & result) { + proof_ref operator()(ast_manager& m, unsigned num_source, proof * const * source) override { SASSERT(num_source == 1); - result = source[0]; + proof_ref result(source[0], m); init_form2rule(); translate_proof(result); + return result; } - virtual proof_converter * translate(ast_translation & translator) { + proof_converter * translate(ast_translation & translator) override { UNREACHABLE(); // this would require implementing translation for the dl_context. return 0; } - virtual void display(std::ostream& out) { out << "(slice-proof-converter)\n"; } + void display(std::ostream& out) override { out << "(slice-proof-converter)\n"; } }; class mk_slice::slice_model_converter : public model_converter { @@ -307,7 +308,7 @@ namespace datalog { m_sliceable.insert(f, bv); } - virtual void operator()(model_ref & md) { + void operator()(model_ref & md) override { if (m_slice2old.empty()) { return; } @@ -393,12 +394,12 @@ namespace datalog { TRACE("dl", model_smt2_pp(tout, m, *md, 0); ); } - virtual model_converter * translate(ast_translation & translator) { + model_converter * translate(ast_translation & translator) override { UNREACHABLE(); return 0; } - virtual void display(std::ostream& out) { out << "(slice-model-converter)\n"; } + void display(std::ostream& out) override { out << "(slice-model-converter)\n"; } }; diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 5757220b4..bedd7c655 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -130,10 +130,9 @@ class nlsat_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("nlsat", *g); if (g->is_decided()) { @@ -165,9 +164,11 @@ class nlsat_tactic : public tactic { if (!contains_unsupported(b2a, x2t)) { // If mk_model is false it means that the model produced by nlsat // assigns noninteger values to integer variables + model_converter_ref mc; if (mk_model(*g.get(), b2a, x2t, mc)) { // result goal is trivially SAT g->reset(); + g->add(mc.get()); } } } @@ -176,8 +177,8 @@ class nlsat_tactic : public tactic { if (g->unsat_core_enabled()) { vector assumptions; m_solver.get_core(assumptions); - for (unsigned i = 0; i < assumptions.size(); ++i) { - expr_dependency* d = static_cast(assumptions[i]); + for (nlsat::assumption a : assumptions) { + expr_dependency* d = static_cast(a); lcore = m.mk_join(lcore, d); } } @@ -233,12 +234,11 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { imp local_imp(in->m(), m_params); scoped_set_imp setter(*this, local_imp); - local_imp(in, result, mc, core); + local_imp(in, result, core); } catch (z3_error & ex) { throw ex; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 19cfc4b9c..edcdb64e0 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -324,10 +324,8 @@ namespace opt { void context::fix_model(model_ref& mdl) { if (mdl) { - if (m_model_converter) { - (*m_model_converter)(mdl, 0); - } - m_fm(mdl, 0); + apply(m_model_converter, mdl); + m_fm(mdl); } } @@ -749,9 +747,10 @@ namespace opt { } expr_dependency_ref core(m); goal_ref_buffer result; - (*m_simplify)(g, result, m_model_converter, core); + (*m_simplify)(g, result, core); SASSERT(result.size() == 1); goal* r = result[0]; + m_model_converter = r->mc(); fmls.reset(); expr_ref tmp(m); for (unsigned i = 0; i < r->size(); ++i) { diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index e593e6627..87e713efc 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -659,9 +659,8 @@ namespace qe { goal_ref g = alloc(goal, m); g->assert_expr(fml); expr_dependency_ref core(m); - model_converter_ref mc; goal_ref_buffer result; - (*m_nftactic)(g, result, mc, core); + (*m_nftactic)(g, result, core); SASSERT(result.size() == 1); TRACE("qe", result[0]->display(tout);); g2s(*result[0], m_params, m_solver, m_a2b, m_t2x); @@ -812,14 +811,13 @@ namespace qe { void operator()(/* in */ goal_ref const & in, /* out */ goal_ref_buffer & result, - /* out */ model_converter_ref & mc, /* out */ expr_dependency_ref & core) { tactic_report report("nlqsat-tactic", *in); ptr_vector fmls; expr_ref fml(m); - mc = 0; core = 0; + core = 0; in->get_formulas(fmls); fml = mk_and(m, fmls.size(), fmls.c_ptr()); if (m_mode == elim_t) { @@ -850,7 +848,9 @@ namespace qe { in->inc_depth(); result.push_back(in.get()); if (in->models_enabled()) { + model_converter_ref mc; VERIFY(mk_model(mc)); + in->add(mc.get()); } break; case l_undef: diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index c7b16417c..51e5c1b78 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -2533,10 +2533,9 @@ class qe_lite_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("qe-lite", *g); proof_ref new_pr(m); expr_ref new_f(m); @@ -2603,9 +2602,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp index 6f09df5b6..28bc78f84 100644 --- a/src/qe/qe_sat_tactic.cpp +++ b/src/qe/qe_sat_tactic.cpp @@ -234,7 +234,6 @@ namespace qe { virtual void operator()( goal_ref const& goal, goal_ref_buffer& result, - model_converter_ref& mc, expr_dependency_ref& core) { try { @@ -259,7 +258,7 @@ namespace qe { else { goal->reset(); // equi-satisfiable. What to do with model? - mc = model2model_converter(&*model); + goal->add(model2model_converter(&*model)); } result.push_back(goal.get()); } @@ -269,16 +268,16 @@ namespace qe { } virtual void collect_statistics(statistics & st) const { - for (unsigned i = 0; i < m_solvers.size(); ++i) { - m_solvers[i]->collect_statistics(st); + for (auto const * s : m_solvers) { + s->collect_statistics(st); } m_solver.collect_statistics(st); m_ctx_rewriter.collect_statistics(st); } virtual void reset_statistics() { - for (unsigned i = 0; i < m_solvers.size(); ++i) { - m_solvers[i]->reset_statistics(); + for (auto * s : m_solvers) { + s->reset_statistics(); } m_solver.reset_statistics(); m_ctx_rewriter.reset_statistics(); diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp index ce1b3003a..131d0d3fb 100644 --- a/src/qe/qe_tactic.cpp +++ b/src/qe/qe_tactic.cpp @@ -51,10 +51,9 @@ class qe_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("qe", *g); m_fparams.m_model = g->models_enabled(); proof_ref new_pr(m); @@ -121,9 +120,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); m_st.reset(); m_imp->collect_statistics(m_st); diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 3040a68fe..ca8a36844 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1212,13 +1212,12 @@ namespace qe { void operator()(/* in */ goal_ref const & in, /* out */ goal_ref_buffer & result, - /* out */ model_converter_ref & mc, /* 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; core = 0; + core = 0; in->get_formulas(fmls); @@ -1271,8 +1270,10 @@ namespace qe { in->inc_depth(); result.push_back(in.get()); if (in->models_enabled()) { + model_converter_ref mc; mc = model2model_converter(m_model.get()); mc = concat(m_pred_abs.fmc(), mc.get()); + in->add(mc.get()); } break; case l_undef: diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 29de5f107..d391eddd0 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_dep_core); + (*m_preprocess)(g, m_subgoals, m_dep_core); } catch (tactic_exception & ex) { IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";); @@ -521,6 +521,7 @@ private: g = m_subgoals[0]; expr_ref_vector atoms(m); m_pc = g->pc(); + m_mc = g->mc(); 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/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index d730ea0ee..7c703653c 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -922,8 +922,7 @@ struct sat2goal::imp { } } - virtual void operator()(model_ref & md, unsigned goal_idx) { - SASSERT(goal_idx == 0); + virtual void operator()(model_ref & md) { TRACE("sat_mc", tout << "before sat_mc\n"; model_v2_pp(tout, *md); display(tout);); // REMARK: potential problem // model_evaluator can't evaluate quantifiers. Then, diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index ba6b53e17..413dfa9bf 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -40,9 +40,8 @@ class sat_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; core = 0; + core = 0; fail_if_proof_generation("sat", g); bool produce_models = g->models_enabled(); bool produce_core = g->unsat_core_enabled(); @@ -102,7 +101,7 @@ class sat_tactic : public tactic { } } TRACE("sat_tactic", model_v2_pp(tout, *md);); - mc = model2model_converter(md.get()); + g->add(model2model_converter(md.get())); } } else { @@ -111,7 +110,9 @@ class sat_tactic : public tactic { IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constains interpreted atoms, recovering formula from sat solver...\"\n";); #endif m_solver.pop_to_base_level(); + model_converter_ref mc; m_sat2goal(m_solver, map, m_params, *(g.get()), mc); + g->add(mc.get()); } g->inc_depth(); result.push_back(g.get()); @@ -175,12 +176,11 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { imp proc(g->m(), m_params); scoped_set_imp set(this, &proc); try { - proc(g, result, mc, core); + proc(g, result, core); proc.m_solver.collect_statistics(m_stats); } catch (sat::solver_exception & ex) { diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 7866f15e9..68312c6a9 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -109,7 +109,7 @@ namespace smt { if (m_name2assertion.contains(a)) { throw default_exception("named assertion defined twice"); } - solver_na2as::assert_expr(t, a); + solver_na2as::assert_expr_core(t, a); get_manager().inc_ref(t); m_name2assertion.insert(a, t); } diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 5b2537b9b..d504a63b2 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -71,10 +71,9 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; core = 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 08ce9bded..2bb68d590 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -146,11 +146,10 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { IF_VERBOSE(10, verbose_stream() << "(smt.tactic start)\n";); - mc = 0; core = 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 << " " @@ -220,8 +219,10 @@ public: m_ctx->get_model(md); buffer r; m_ctx->get_relevant_labels(0, r); + model_converter_ref mc; mc = model_and_labels2model_converter(md.get(), r); mc = concat(fmc.get(), mc.get()); + in->add(mc.get()); } return; } @@ -269,7 +270,7 @@ public: m_ctx->get_model(md); buffer r; m_ctx->get_relevant_labels(0, r); - mc = model_and_labels2model_converter(md.get(), r); + in->add(model_and_labels2model_converter(md.get(), r)); } return; default: diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp index f02829af0..0b900426b 100644 --- a/src/smt/tactic/unit_subsumption_tactic.cpp +++ b/src/smt/tactic/unit_subsumption_tactic.cpp @@ -41,7 +41,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 */ expr_dependency_ref & core) { reduce_core(in, result); } diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index 7d3076643..60a7404b6 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -103,9 +103,8 @@ public: virtual void operator()(/* in */ goal_ref const & in, /* out */ goal_ref_buffer & result, - /* out */ model_converter_ref & mc, /* out */ expr_dependency_ref & core) { - mc = 0; core = 0; + core = 0; expr_ref_vector clauses(m); expr2expr_map bool2dep; ptr_vector assumptions; @@ -119,9 +118,11 @@ public: if (in->models_enabled()) { model_ref mdl; local_solver->get_model(mdl); + model_converter_ref mc; mc = model2model_converter(mdl.get()); mc = concat(fmc.get(), mc.get()); mc = concat(local_solver->mc0(), mc.get()); + in->add(mc.get()); } in->reset(); result.push_back(in.get()); @@ -150,9 +151,11 @@ public: if (m.canceled()) { throw tactic_exception(Z3_CANCELED_MSG); } + model_converter_ref mc; mc = local_solver->get_model_converter(); mc = concat(fmc.get(), mc.get()); in->reset(); + in->add(mc.get()); unsigned sz = local_solver->get_num_assertions(); for (unsigned i = 0; i < sz; ++i) { in->assert_expr(local_solver->get_assertion(i)); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 35fe9cf8e..4585af65e 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -159,7 +159,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass std::string reason_unknown = "unknown"; labels_vec labels; try { - switch (::check_sat(*m_tactic, g, md, m_mc, labels, pr, core, reason_unknown)) { + switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) { case l_true: m_result->set_status(l_true); break; @@ -176,6 +176,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass } break; } + m_mc = g->mc(); } catch (z3_error & ex) { TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";); diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp index e51dc527c..6de44c654 100644 --- a/src/tactic/aig/aig_tactic.cpp +++ b/src/tactic/aig/aig_tactic.cpp @@ -92,10 +92,9 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { fail_if_proof_generation("aig", g); - mc = 0; core = 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 50a30b0ef..852eb9cc0 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -112,9 +112,8 @@ class add_bounds_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; core = 0; + core = 0; tactic_report report("add-bounds", *g); bound_manager bm(m); expr_fast_mark1 visited; @@ -161,9 +160,8 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(g, result, mc, core); + (*m_imp)(g, result, core); } virtual void cleanup() { diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp index bc7d4b51f..d86d8dd8f 100644 --- a/src/tactic/arith/arith_bounds_tactic.cpp +++ b/src/tactic/arith/arith_bounds_tactic.cpp @@ -25,7 +25,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 */ 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 c2715da7a..ec9f92a35 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -54,11 +54,10 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { TRACE("card2bv-before", g->display(tout);); SASSERT(g->is_well_sorted()); - mc = 0; core = 0; result.reset(); + core = 0; result.reset(); tactic_report report("card2bv", *g); th_rewriter rw1(m, m_params); pb2bv_rewriter rw2(m, m_params); @@ -89,10 +88,8 @@ public: func_decl_ref_vector const& fns = rw2.fresh_constants(); if (!fns.empty()) { generic_model_converter* filter = alloc(generic_model_converter, m); - for (unsigned i = 0; i < fns.size(); ++i) { - filter->hide(fns[i]); - } - mc = filter; + for (func_decl* f : fns) filter->hide(f); + g->add(filter); } g->inc_depth(); diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index 06e81bc68..62b030706 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -224,14 +224,14 @@ class degree_shift_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; m_produce_proofs = g->proofs_enabled(); m_produce_models = g->models_enabled(); tactic_report report("degree_shift", *g); collect(*g); + model_converter_ref mc; discard_non_candidates(); if (!m_var2degree.empty()) { prepare_substitution(mc); @@ -269,6 +269,7 @@ class degree_shift_tactic : public tactic { } } g->inc_depth(); + g->add(mc.get()); result.push_back(g.get()); TRACE("degree_shift", g->display(tout); if (mc) mc->display(tout);); SASSERT(g->is_well_sorted()); @@ -291,9 +292,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } virtual void cleanup() { diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index 1bc1c4b73..06966178f 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -314,11 +314,10 @@ class diff_neq_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); m_produce_models = g->models_enabled(); - mc = 0; core = 0; result.reset(); + 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); @@ -331,8 +330,9 @@ class diff_neq_tactic : public tactic { bool r = search(); report_tactic_progress(":conflicts", m_num_conflicts); if (r) { - if (m_produce_models) - mc = model2model_converter(mk_model()); + if (m_produce_models) { + g->add(model2model_converter(mk_model())); + } g->reset(); } else { @@ -384,9 +384,8 @@ public: */ virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } virtual void cleanup() { diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp index dd1dfbd7e..731ca4b5d 100644 --- a/src/tactic/arith/elim01_tactic.cpp +++ b/src/tactic/arith/elim01_tactic.cpp @@ -41,8 +41,7 @@ public: m_refs(m) {} - virtual void operator()(model_ref & old_model, unsigned goal_idx) { - SASSERT(goal_idx == 0); + virtual void operator()(model_ref & old_model) { model * new_model = alloc(model, m); unsigned num = old_model->get_num_constants(); for (unsigned i = 0; i < m_nums_as_int.size(); ++i) { @@ -154,16 +153,14 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("elim01", *g); expr_safe_replace sub(m); - bool2int_model_converter* b2i = alloc(bool2int_model_converter, m); - mc = b2i; + ref b2i = alloc(bool2int_model_converter, m); bound_manager bounds(m); expr_ref_vector axioms(m); bounds(*g); @@ -178,7 +175,7 @@ public: if (a.is_int(x) && bounds.has_lower(x, lo, s1) && !s1 && zero <= lo && bounds.has_upper(x, hi, s2) && !s2 && hi <= m_max_hi && lo <= hi) { - add_variable(b2i, sub, x, lo.get_unsigned(), hi.get_unsigned(), axioms); + add_variable(b2i.get(), sub, x, lo.get_unsigned(), hi.get_unsigned(), axioms); } else if (a.is_int(x)) { TRACE("pb", tout << "Not adding variable " << mk_pp(x, m) << " has lower: " @@ -204,9 +201,9 @@ public: } g->update(i, new_curr, new_pr, g->dep(i)); } - for (unsigned i = 0; i < axioms.size(); ++i) { - g->assert_expr(axioms[i].get()); - } + for (expr* a : axioms) + g->assert_expr(a); + g->add(b2i.get()); g->inc_depth(); result.push_back(g.get()); TRACE("pb", g->display(tout);); diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index 819b8cb94..74bc9a5ef 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -152,10 +152,9 @@ public: virtual void operator()( goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; m_trail.reset(); m_fd.reset(); m_max.reset(); @@ -211,7 +210,7 @@ public: } } g->inc_depth(); - mc = mc1.get(); + g->add(mc1.get()); result.push_back(g.get()); TRACE("pb", g->display(tout);); SASSERT(g->is_well_sorted()); diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index e4ab1ca05..1233ddf9d 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -258,10 +258,9 @@ class factor_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("factor", *g); bool produce_proofs = g->proofs_enabled(); @@ -313,10 +312,9 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, 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 68d31621f..16288f7ad 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -250,10 +250,9 @@ class fix_dl_var_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("fix-dl-var", *g); bool produce_proofs = g->proofs_enabled(); m_produce_models = g->models_enabled(); @@ -269,9 +268,9 @@ class fix_dl_var_tactic : public tactic { m_rw.set_substitution(&subst); if (m_produce_models) { - generic_model_converter * _mc = alloc(generic_model_converter, m); - _mc->add(var, zero); - mc = _mc; + generic_model_converter * mc = alloc(generic_model_converter, m); + mc->add(var, zero); + g->add(mc); } expr_ref new_curr(m); @@ -321,10 +320,9 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, 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 c53ef7274..92e6ee530 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -180,7 +180,7 @@ class fm_tactic : public tactic { m_clauses.back().swap(c); } - virtual void operator()(model_ref & md, unsigned goal_idx) { + virtual void operator()(model_ref & md) { TRACE("fm_mc", model_v2_pp(tout, *md); display(tout);); model_evaluator ev(*(md.get())); ev.set_model_completion(true); @@ -1551,10 +1551,9 @@ class fm_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("fm", *g); fail_if_proof_generation("fm", g); m_produce_models = g->models_enabled(); @@ -1602,7 +1601,7 @@ class fm_tactic : public tactic { report_tactic_progress(":fm-cost", m_counter); if (!m_inconsistent) { copy_remaining(); - mc = m_mc.get(); + m_new_goal->add(concat(g->mc(), m_mc.get())); } } reset_constraints(); @@ -1675,9 +1674,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } }; diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index dfe7037f4..dfff44526 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -160,10 +160,9 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; m_01s->reset(); tactic_report report("cardinality-intro", *g); @@ -172,9 +171,7 @@ public: bounds(*g); - bound_manager::iterator bit = bounds.begin(), bend = bounds.end(); - for (; bit != bend; ++bit) { - expr* x = *bit; + for (expr* x : bounds) { bool s1 = false, s2 = false; rational lo, hi; if (a.is_int(x) && @@ -196,9 +193,7 @@ public: g->update(i, new_curr, new_pr, g->dep(i)); mark_rec(subfmls, new_curr); } - expr_set::iterator it = m_01s->begin(), end = m_01s->end(); - for (; it != end; ++it) { - expr* v = *it; + for (expr* v : *m_01s) { if (subfmls.is_marked(v)) { g->assert_expr(a.mk_le(v, a.mk_numeral(rational(1), true))); g->assert_expr(a.mk_le(a.mk_numeral(rational(0), true), v)); diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index a1834a73a..cc339f74a 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -189,13 +189,12 @@ class lia2pb_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, 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; core = 0; result.reset(); + core = 0; result.reset(); tactic_report report("lia2pb", *g); m_bm.reset(); m_rw.reset(); m_new_deps.reset(); @@ -222,10 +221,9 @@ class lia2pb_tactic : public tactic { if (!check_num_bits()) throw tactic_exception("lia2pb failed, number of necessary bits exceeds specified threshold (use option :lia2pb-total-bits to increase threshold)"); - generic_model_converter * gmc = 0; + ref gmc; if (m_produce_models) { gmc = alloc(generic_model_converter, m); - mc = gmc; } expr_ref zero(m); @@ -295,6 +293,7 @@ class lia2pb_tactic : public tactic { g->update(idx, new_curr, new_pr, dep); } g->inc_depth(); + g->add(gmc.get()); result.push_back(g.get()); TRACE("lia2pb", g->display(tout);); SASSERT(g->is_well_sorted()); @@ -330,10 +329,9 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, 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 65ed8ffbe..2b4783c6f 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -441,17 +441,17 @@ public: */ virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); fail_if_proof_generation("nla2bv", g); fail_if_unsat_core_generation("nla2bv", g); - mc = 0; core = 0; result.reset(); + core = 0; result.reset(); imp proc(g->m(), m_params); scoped_set_imp setter(*this, proc); + model_converter_ref mc; proc(*(g.get()), mc); - + g->add(mc.get()); result.push_back(g.get()); SASSERT(g->is_well_sorted()); } diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index afc165866..955e92f1a 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -81,9 +81,8 @@ class normalize_bounds_tactic : public tactic { void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; core = 0; + core = 0; bool produce_models = in->models_enabled(); bool produce_proofs = in->proofs_enabled(); tactic_report report("normalize-bounds", *in); @@ -99,16 +98,13 @@ class normalize_bounds_tactic : public tactic { generic_model_converter * gmc = 0; if (produce_models) { gmc = alloc(generic_model_converter, m); - mc = gmc; + in->add(gmc); } unsigned num_norm_bounds = 0; expr_substitution subst(m); rational val; - bound_manager::iterator it = m_bm.begin(); - bound_manager::iterator end = m_bm.end(); - for (; it != end; ++it) { - expr * x = *it; + for (expr * x : m_bm) { if (is_target(x, val)) { num_norm_bounds++; sort * s = m.get_sort(x); @@ -171,10 +167,9 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } catch (rewriter_exception & ex) { throw tactic_exception(ex.msg()); diff --git a/src/tactic/arith/pb2bv_model_converter.cpp b/src/tactic/arith/pb2bv_model_converter.cpp index df5bd5745..16deb7cd7 100644 --- a/src/tactic/arith/pb2bv_model_converter.cpp +++ b/src/tactic/arith/pb2bv_model_converter.cpp @@ -27,17 +27,12 @@ pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m) : m(_m) { pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m, obj_map const & c2bit, bound_manager const & bm): m(_m) { - obj_map::iterator it = c2bit.begin(); - obj_map::iterator end = c2bit.end(); - for ( ; it != end; it++) { - m_c2bit.push_back(func_decl_pair(it->m_key, to_app(it->m_value)->get_decl())); - m.inc_ref(it->m_key); - m.inc_ref(to_app(it->m_value)->get_decl()); + for (auto const& kv : c2bit) { + m_c2bit.push_back(func_decl_pair(kv.m_key, to_app(kv.m_value)->get_decl())); + m.inc_ref(kv.m_key); + m.inc_ref(to_app(kv.m_value)->get_decl()); } - bound_manager::iterator it2 = bm.begin(); - bound_manager::iterator end2 = bm.end(); - for (; it2 != end2; ++it2) { - expr * c = *it2; + for (expr* c : bm) { SASSERT(is_uninterp_const(c)); func_decl * d = to_app(c)->get_decl(); if (!c2bit.contains(d)) { @@ -49,53 +44,43 @@ pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m, obj_map::const_iterator it = m_c2bit.begin(); - svector::const_iterator end = m_c2bit.end(); - for (; it != end; ++it) { - m.dec_ref(it->first); - m.dec_ref(it->second); + for (auto const& kv : m_c2bit) { + m.dec_ref(kv.first); + m.dec_ref(kv.second); } } -void pb2bv_model_converter::operator()(model_ref & md) { - (*this)(md, 0); -} -void pb2bv_model_converter::operator()(model_ref & md, unsigned goal_idx) { - SASSERT(goal_idx == 0); +void pb2bv_model_converter::operator()(model_ref & md) { TRACE("pb2bv", tout << "converting model:\n"; model_v2_pp(tout, *md); display(tout);); arith_util a_util(m); - svector::const_iterator it = m_c2bit.begin(); - svector::const_iterator end = m_c2bit.end(); - for (; it != end; ++it) { - if (it->second) { - expr * val = md->get_const_interp(it->second); + for (auto const& kv : m_c2bit) { + if (kv.second) { + expr * val = md->get_const_interp(kv.second); if (val == 0 || m.is_false(val)) { /* false's and don't cares get the integer 0 solution*/ - md->register_decl(it->first, a_util.mk_numeral(rational(0), true)); + md->register_decl(kv.first, a_util.mk_numeral(rational(0), true)); } else { - md->register_decl(it->first, a_util.mk_numeral(rational(1), true)); + md->register_decl(kv.first, a_util.mk_numeral(rational(1), true)); } } else { - // it->first is a don't care. - md->register_decl(it->first, a_util.mk_numeral(rational(0), true)); + // kv.first is a don't care. + md->register_decl(kv.first, a_util.mk_numeral(rational(0), true)); } } } void pb2bv_model_converter::display(std::ostream & out) { out << "(pb2bv-model-converter"; - svector::const_iterator it = m_c2bit.begin(); - svector::const_iterator end = m_c2bit.end(); - for (; it != end; ++it) { - out << "\n (" << it->first->get_name() << " "; - if (it->second == 0) + for (auto const& kv : m_c2bit) { + out << "\n (" << kv.first->get_name() << " "; + if (kv.second == 0) out << "0"; else - out << it->second->get_name(); + out << kv.second->get_name(); out << ")"; } out << ")\n"; @@ -104,11 +89,9 @@ void pb2bv_model_converter::display(std::ostream & out) { model_converter * pb2bv_model_converter::translate(ast_translation & translator) { ast_manager & to = translator.to(); pb2bv_model_converter * res = alloc(pb2bv_model_converter, to); - svector::iterator it = m_c2bit.begin(); - svector::iterator end = m_c2bit.end(); - for (; it != end; it++) { - func_decl * f1 = translator(it->first); - func_decl * f2 = translator(it->second); + for (auto const& kv : m_c2bit) { + func_decl * f1 = translator(kv.first); + func_decl * f2 = translator(kv.second); res->m_c2bit.push_back(func_decl_pair(f1, f2)); to.inc_ref(f1); to.inc_ref(f2); diff --git a/src/tactic/arith/pb2bv_model_converter.h b/src/tactic/arith/pb2bv_model_converter.h index 0c2826573..59825b10f 100644 --- a/src/tactic/arith/pb2bv_model_converter.h +++ b/src/tactic/arith/pb2bv_model_converter.h @@ -31,10 +31,9 @@ public: pb2bv_model_converter(ast_manager & _m); pb2bv_model_converter(ast_manager & _m, obj_map const & c2bit, bound_manager const & bm); virtual ~pb2bv_model_converter(); - virtual void operator()(model_ref & md); - virtual void operator()(model_ref & md, unsigned goal_idx); - virtual void display(std::ostream & out); - virtual model_converter * translate(ast_translation & translator); + void operator()(model_ref & md) override; + void display(std::ostream & out) override; + model_converter * translate(ast_translation & translator) override; }; #endif diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 76f003737..e06c44110 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -887,14 +887,13 @@ private: void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, 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; core = 0; result.reset(); + core = 0; result.reset(); tactic_report report("pb2bv", *g); m_bm.reset(); m_rw.reset(); m_new_deps.reset(); @@ -948,6 +947,7 @@ private: g->update(idx, new_exprs[idx].get(), 0, (m_produce_unsat_cores) ? new_deps[idx].get() : g->dep(idx)); if (m_produce_models) { + model_converter_ref mc; generic_model_converter * mc1 = alloc(generic_model_converter, m); for (auto const& kv : m_const2bit) mc1->hide(kv.m_value); @@ -956,7 +956,8 @@ private: for (unsigned i = 0; i < num_temps; i++) mc1->hide(m_temporary_ints.get(i)); pb2bv_model_converter * mc2 = alloc(pb2bv_model_converter, m, m_const2bit, m_bm); - mc = concat(mc1, mc2); + mc = concat(mc1, mc2); + g->add(mc.get()); } g->inc_depth(); @@ -999,9 +1000,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } virtual void cleanup() { diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp index e52668f33..58fdf14ca 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, expr_dependency_ref & core); + virtual void operator()(goal_ref const & g, goal_ref_buffer & result, expr_dependency_ref & core); virtual void cleanup(); }; @@ -528,12 +528,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, 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; core = 0; result.reset(); + 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 2affd8012..0caa0194d 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -822,11 +822,10 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("purify-arith", *g); TRACE("purify_arith", g->display(tout);); bool produce_proofs = g->proofs_enabled(); @@ -834,10 +833,10 @@ public: bool elim_root_objs = m_params.get_bool("elim_root_objects", true); bool elim_inverses = m_params.get_bool("elim_inverses", true); bool complete = m_params.get_bool("complete", true); - purify_arith_proc proc(*(g.get()), m_util, produce_proofs, elim_root_objs, elim_inverses, complete); - + purify_arith_proc proc(*(g.get()), m_util, produce_proofs, elim_root_objs, elim_inverses, complete); + model_converter_ref mc; proc(mc, produce_models); - + g->add(mc.get()); g->inc_depth(); result.push_back(g.get()); TRACE("purify_arith", g->display(tout);); diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index 11144c89b..2fde96caf 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -293,13 +293,12 @@ class recover_01_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, 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; core = 0; result.reset(); + core = 0; result.reset(); tactic_report report("recover-01", *g); bool saved = false; @@ -307,7 +306,9 @@ class recover_01_tactic : public tactic { SASSERT(new_goal->depth() == g->depth()); SASSERT(new_goal->prec() == g->prec()); new_goal->inc_depth(); - + new_goal->add(g->mc()); + new_goal->add(g->pc()); + unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) { expr * f = g->form(i); @@ -326,7 +327,7 @@ class recover_01_tactic : public tactic { if (m_produce_models) { gmc = alloc(generic_model_converter, m); - mc = gmc; + new_goal->add(gmc); } dec_ref_key_values(m, bool2int); @@ -335,25 +336,20 @@ class recover_01_tactic : public tactic { bool recovered = false; expr_substitution _subst(m); subst = &_subst; - var2clauses::iterator it = m_var2clauses.begin(); - var2clauses::iterator end = m_var2clauses.end(); - for (; it != end; ++it) { - if (process(it->m_key, it->m_value)) { + for (auto& kv : m_var2clauses) { + if (process(kv.m_key, kv.m_value)) { recovered = true; counter++; } else { - ptr_vector::iterator it2 = it->m_value.begin(); - ptr_vector::iterator end2 = it->m_value.end(); - for (; it2 != end2; ++it2) { - new_goal->assert_expr(*it2); + for (app* a : kv.m_value) { + new_goal->assert_expr(a); } } } if (!recovered) { result.push_back(g.get()); - mc = 0; return; } @@ -406,10 +402,9 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { - (*m_imp)(g, result, mc, core); + (*m_imp)(g, result, core); } catch (rewriter_exception & ex) { throw tactic_exception(ex.msg()); diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp index cdcc486a6..3ead0876a 100644 --- a/src/tactic/bv/bit_blaster_model_converter.cpp +++ b/src/tactic/bv/bit_blaster_model_converter.cpp @@ -172,8 +172,7 @@ struct bit_blaster_model_converter : public model_converter { return result; } - void operator()(model_ref & md, unsigned goal_idx) override { - SASSERT(goal_idx == 0); + void operator()(model_ref & md) override { model * new_model = alloc(model, m()); obj_hashtable bits; collect_bits(bits); @@ -182,10 +181,6 @@ struct bit_blaster_model_converter : public model_converter { md = new_model; } - void operator()(model_ref & md) override { - operator()(md, 0); - } - /** \brief simplisic expansion operator for formulas. It just adds back bit-vector definitions to the formula whether they are used or not. diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index d7df2e1c4..7928185b3 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -52,9 +52,8 @@ class bit_blaster_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; core = 0; + core = 0; bool proofs_enabled = g->proofs_enabled(); if (proofs_enabled && m_blast_quant) @@ -87,12 +86,10 @@ class bit_blaster_tactic : public tactic { } if (change && g->models_enabled()) - mc = mk_bit_blaster_model_converter(m(), m_rewriter->const2bits()); - else - mc = 0; + g->add(mk_bit_blaster_model_converter(m(), m_rewriter->const2bits())); g->inc_depth(); result.push_back(g.get()); - TRACE("after_bit_blaster", g->display(tout); if (mc) mc->display(tout); tout << "\n";); + TRACE("after_bit_blaster", g->display(tout); if (g->mc()) g->mc()->display(tout); tout << "\n";); m_rewriter->cleanup(); } @@ -135,10 +132,9 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { - (*m_imp)(g, result, mc, core); + (*m_imp)(g, result, 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 9dc247455..9e31330fd 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -380,9 +380,8 @@ class bv1_blaster_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; core = 0; + core = 0; if (!is_target(*g)) throw tactic_exception("bv1 blaster cannot be applied to goal"); @@ -408,7 +407,7 @@ class bv1_blaster_tactic : public tactic { } if (g->models_enabled()) - mc = mk_bv1_blaster_model_converter(m(), m_rw.cfg().m_const2bits); + g->add(mk_bv1_blaster_model_converter(m(), m_rw.cfg().m_const2bits)); g->inc_depth(); result.push_back(g.get()); m_rw.cfg().cleanup(); @@ -455,9 +454,8 @@ public: */ virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(g, result, mc, core); + (*m_imp)(g, result, 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 487bbb762..151b00f50 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -138,7 +138,6 @@ public: virtual ~bv_bound_chk_tactic(); void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core); virtual tactic * translate(ast_manager & m); virtual void updt_params(params_ref const & p); @@ -198,13 +197,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, 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; core = 0; result.reset(); + 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 e3a5edd84..e7cda8a2f 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, expr_dependency_ref & core); + virtual void operator()(goal_ref const & g, goal_ref_buffer & result, expr_dependency_ref & core); virtual void cleanup(); }; @@ -383,14 +383,15 @@ 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, 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; core = 0; result.reset(); + core = 0; result.reset(); + model_converter_ref mc; m_imp->operator()(*(g.get()), mc); g->inc_depth(); + g->add(mc.get()); result.push_back(g.get()); SASSERT(g->is_well_sorted()); } diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index 3aba9a073..421b3e1e7 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -54,16 +54,16 @@ class bvarray2uf_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); tactic_report report("bvarray2uf", *g); - mc = 0; core = 0; result.reset(); + core = 0; result.reset(); fail_if_unsat_core_generation("bvarray2uf", g); TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); ); m_produce_models = g->models_enabled(); + model_converter_ref mc; if (m_produce_models) { generic_model_converter * fmc = alloc(generic_model_converter, m_manager); @@ -92,6 +92,7 @@ class bvarray2uf_tactic : public tactic { g->assert_expr(m_rw.m_cfg.extra_assertions[i].get()); g->inc_depth(); + g->add(mc.get()); result.push_back(g.get()); TRACE("bvarray2uf", tout << "After: " << std::endl; g->display(tout);); SASSERT(g->is_well_sorted()); @@ -129,9 +130,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } virtual void cleanup() { diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 722d2d359..a50658b5a 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -118,9 +118,8 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; core = 0; + core = 0; bool produce_proofs = g->proofs_enabled(); tactic_report report("dt2bv", *g); unsigned size = g->size(); @@ -154,7 +153,7 @@ public: for (auto const& kv : rw.enum2def()) filter->add(kv.m_key, kv.m_value); - mc = filter.get(); + g->add(filter.get()); report_tactic_progress(":fd-num-translated", rw.num_translated()); } g->inc_depth(); diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index a86b41dcc..2d8224f42 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -226,10 +226,9 @@ class elim_small_bv_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("elim-small-bv", *g); bool produce_proofs = g->proofs_enabled(); fail_if_proof_generation("elim-small-bv", g); @@ -249,7 +248,7 @@ class elim_small_bv_tactic : public tactic { } g->update(idx, new_curr, new_pr, g->dep(idx)); } - mc = m_rw.m_cfg.m_mc.get(); + g->add(m_rw.m_cfg.m_mc.get()); report_tactic_progress(":elim-small-bv-num-eliminated", m_rw.m_cfg.m_num_eliminated); g->inc_depth(); @@ -288,9 +287,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, 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 8a6090ca3..e9452dbbc 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -238,10 +238,9 @@ class max_bv_sharing_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("max-bv-sharing", *g); bool produce_proofs = g->proofs_enabled(); @@ -299,9 +298,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, 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 7a6643568..e24ae0eb2 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -115,10 +115,9 @@ class blast_term_ite_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("blast-term-ite", *g); bool produce_proofs = g->proofs_enabled(); @@ -172,9 +171,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, 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 d139d60e9..e43d0c1ef 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ b/src/tactic/core/cofactor_term_ite_tactic.cpp @@ -56,13 +56,12 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, 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; core = 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 b71c566d6..faba93dc5 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -64,9 +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, expr_dependency_ref & core) { - mc = 0; tactic_report report("collect-statistics", *g); collect_proc cp(m, m_stats); @@ -76,10 +74,8 @@ public: for_each_expr(cp, visited, g->form(i)); std::cout << "(" << std::endl; - stats_type::iterator it = m_stats.begin(); - stats_type::iterator end = m_stats.end(); - for (; it != end; it++) - std::cout << " :" << it->first << " " << it->second << std::endl; + for (auto const& kv : m_stats) + std::cout << " :" << kv.first << " " << kv.second << std::endl; std::cout << ")" << std::endl; g->inc_depth(); diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 43371235c..1216a7556 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -622,9 +622,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, expr_dependency_ref & core) { - mc = 0; core = 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 2ad6e9243..21468d6da 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -56,7 +56,6 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core); virtual void cleanup(); diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp index 1151d6770..1b51c92e6 100644 --- a/src/tactic/core/der_tactic.cpp +++ b/src/tactic/core/der_tactic.cpp @@ -75,9 +75,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; core = 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 16e2c5f78..dd887a0e1 100644 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ b/src/tactic/core/distribute_forall_tactic.cpp @@ -101,14 +101,13 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, 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; core = 0; result.reset(); + 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 d175ba0c4..c18f6cd29 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -186,9 +186,8 @@ tactic * dom_simplify_tactic::translate(ast_manager & m) { void dom_simplify_tactic::operator()( goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; core = 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 fd4e9e49b..10a56a979 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -139,7 +139,6 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, 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 3f65f4b9d..3035a8582 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -101,10 +101,9 @@ class elim_term_ite_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 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(); @@ -123,7 +122,7 @@ class elim_term_ite_tactic : public tactic { } g->update(idx, new_curr, new_pr, g->dep(idx)); } - mc = m_rw.m_cfg.m_mc.get(); + g->add(m_rw.m_cfg.m_mc.get()); report_tactic_progress(":elim-term-ite-consts", m_rw.m_cfg.m_num_fresh); g->inc_depth(); result.push_back(g.get()); @@ -162,9 +161,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } virtual void cleanup() { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 3660fdccb..a3bb482f1 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -816,10 +816,9 @@ class elim_uncnstr_tactic : public tactic { } void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - expr_dependency_ref & core) { - mc = 0; core = 0; + goal_ref_buffer & result, + expr_dependency_ref & core) { + core = 0; bool produce_models = g->models_enabled(); bool produce_proofs = g->proofs_enabled(); @@ -864,8 +863,7 @@ class elim_uncnstr_tactic : public tactic { g->update(idx, new_f, new_pr, g->dep(idx)); } if (!modified) { - if (round == 0) { - mc = 0; + if (round == 0) { } else { app_ref_vector & fresh_vars = m_rw->cfg().m_fresh_vars; @@ -874,15 +872,14 @@ class elim_uncnstr_tactic : public tactic { generic_model_converter * fmc = alloc(generic_model_converter, m()); for (app * f : fresh_vars) fmc->hide(f); - mc = concat(fmc, m_mc.get()); + g->add(concat(fmc, m_mc.get())); } else { - mc = 0; + g->set((model_converter*)nullptr); } } m_mc = 0; m_rw = 0; - TRACE("elim_uncnstr", if (mc) mc->display(tout);); result.push_back(g.get()); g->inc_depth(); return; @@ -933,9 +930,8 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(g, result, mc, core); + (*m_imp)(g, result, 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 4c03254c4..9c233ac1c 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -145,10 +145,9 @@ class injectivity_tactic : public tactic { void operator()(goal_ref const & goal, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(goal->is_well_sorted()); - mc = 0; core = 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); @@ -271,9 +270,8 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_finder)(g, result, mc, core); + (*m_finder)(g, result, 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 080fc0bec..37251b8e9 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -55,11 +55,10 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { TRACE("nnf", tout << "params: " << m_params << "\n"; g->display(tout);); SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("nnf", *g); bool produce_proofs = g->proofs_enabled(); @@ -97,7 +96,7 @@ public: unsigned num_extra_names = dnames.get_num_names(); if (num_extra_names > 0) { generic_model_converter * fmc = alloc(generic_model_converter, m); - mc = fmc; + g->add(fmc); for (unsigned i = 0; i < num_extra_names; i++) fmc->hide(dnames.get_name_decl(i)); } diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index 8ce514401..a1cf0931a 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -129,10 +129,9 @@ class occf_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; fail_if_proof_generation("occf", g); @@ -157,7 +156,7 @@ class occf_tactic : public tactic { continue; if (produce_models && !m_mc) { m_mc = alloc(generic_model_converter, m); - mc = m_mc; + g->add(m_mc); } expr * keep = 0; new_lits.reset(); @@ -211,9 +210,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } virtual void cleanup() { diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 897d560cf..e622eb9a3 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -48,8 +48,7 @@ class pb_preproc_model_converter : public model_converter { public: pb_preproc_model_converter(ast_manager& m):m(m), pb(m), m_refs(m) {} - virtual void operator()(model_ref & mdl, unsigned goal_idx) { - SASSERT(goal_idx == 0); + virtual void operator()(model_ref & mdl) { for (auto const& kv : m_const) { mdl->register_decl(kv.first->get_decl(), kv.second); } @@ -151,7 +150,6 @@ public: virtual void operator()( goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); core = 0; @@ -161,7 +159,7 @@ public: } pb_preproc_model_converter* pp = alloc(pb_preproc_model_converter, m); - mc = pp; + g->add(pp); g->inc_depth(); result.push_back(g.get()); diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 61804d336..12a14f5a6 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -137,10 +137,9 @@ class propagate_values_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("propagate-values", *g); m_goal = g.get(); @@ -241,10 +240,9 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, 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 aa53cd9cc..25f0a8f36 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, expr_dependency_ref & core); + virtual void operator()(goal_ref const & g, goal_ref_buffer & result, expr_dependency_ref & core); virtual void cleanup(); }; @@ -439,7 +439,7 @@ struct reduce_args_tactic::imp { return f_mc; } - void operator()(goal & g, model_converter_ref & mc) { + void operator()(goal & g) { if (g.inconsistent()) return; TRACE("reduce_args", g.display(tout);); @@ -468,9 +468,9 @@ struct reduce_args_tactic::imp { report_tactic_progress(":reduced-funcs", decl2args.size()); if (g.models_enabled()) - mc = mk_mc(decl2args, ctx.m_decl2arg2funcs); + g.add(mk_mc(decl2args, ctx.m_decl2arg2funcs)); - TRACE("reduce_args", g.display(tout); if (mc) mc->display(tout);); + TRACE("reduce_args", g.display(tout); if (g.mc()) g.mc()->display(tout);); } }; @@ -484,13 +484,12 @@ reduce_args_tactic::~reduce_args_tactic() { void reduce_args_tactic::operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, 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; core = 0; result.reset(); - m_imp->operator()(*(g.get()), mc); + core = 0; result.reset(); + m_imp->operator()(*(g.get())); g->inc_depth(); result.push_back(g.get()); SASSERT(g->is_well_sorted()); diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index 84ade7ba3..a8278c383 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -94,13 +94,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, expr_dependency_ref & core) { try { (*m_imp)(*(in.get())); in->inc_depth(); result.push_back(in.get()); - mc = 0; core = 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 f14f219d4..282feda0f 100644 --- a/src/tactic/core/simplify_tactic.h +++ b/src/tactic/core/simplify_tactic.h @@ -36,7 +36,6 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, 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 6fbefcba3..fec0edd81 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -668,10 +668,10 @@ class solve_eqs_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; + model_converter_ref mc; tactic_report report("solve_eqs", *g); m_produce_models = g->models_enabled(); m_produce_proofs = g->proofs_enabled(); @@ -691,7 +691,6 @@ class solve_eqs_tactic : public tactic { normalize(); substitute(*(g.get())); if (g->inconsistent()) { - mc = 0; break; } save_elim_vars(mc); @@ -699,6 +698,7 @@ class solve_eqs_tactic : public tactic { } } g->inc_depth(); + g->add(mc.get()); result.push_back(g.get()); TRACE("solve_eqs", g->display(tout);); SASSERT(g->is_well_sorted()); @@ -734,9 +734,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, 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 f383036f7..60dbdd568 100644 --- a/src/tactic/core/split_clause_tactic.cpp +++ b/src/tactic/core/split_clause_tactic.cpp @@ -46,21 +46,16 @@ class split_clause_tactic : public tactic { } class split_pc : public proof_converter { - ast_manager & m_manager; - app * m_clause; - proof * m_clause_pr; + ast_manager & m; + app_ref m_clause; + proof_ref m_clause_pr; public: - split_pc(ast_manager & m, app * cls, proof * pr):m_manager(m), m_clause(cls), m_clause_pr(pr) { - m.inc_ref(cls); - m.inc_ref(pr); + split_pc(ast_manager & m, app * cls, proof * pr):m(m), m_clause(cls, m), m_clause_pr(pr, m) { } - ~split_pc() { - m_manager.dec_ref(m_clause); - m_manager.dec_ref(m_clause_pr); - } + virtual ~split_pc() { } - virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) { + proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override { // Let m_clause be of the form (l_0 or ... or l_{num_source - 1}) // Each source[i] proof is a proof for "false" using l_i as a hypothesis // So, I use lemma for producing a proof for (not l_i) that does not contain the hypothesis, @@ -73,14 +68,14 @@ class split_clause_tactic : public tactic { expr * not_li = m.mk_not(m_clause->get_arg(i)); prs.push_back(m.mk_lemma(pr_i, not_li)); } - result = m.mk_unit_resolution(prs.size(), prs.c_ptr()); + return proof_ref(m.mk_unit_resolution(prs.size(), prs.c_ptr()), m); } - virtual proof_converter * translate(ast_translation & translator) { - return alloc(split_pc, translator.to(), translator(m_clause), translator(m_clause_pr)); + proof_converter * translate(ast_translation & translator) override { + return alloc(split_pc, translator.to(), translator(m_clause.get()), translator(m_clause_pr.get())); } - virtual void display(std::ostream & out) { out << "(split-clause-pc)\n"; } + void display(std::ostream & out) override { out << "(split-clause-pc)\n"; } }; public: @@ -97,22 +92,21 @@ public: virtual ~split_clause_tactic() { } - virtual void updt_params(params_ref const & p) { + void updt_params(params_ref const & p) override { m_largest_clause = p.get_bool("split_largest_clause", false); } - virtual void collect_param_descrs(param_descrs & r) { + void collect_param_descrs(param_descrs & r) override { r.insert("split_largest_clause", CPK_BOOL, "(default: false) split the largest clause in the goal."); } - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - expr_dependency_ref & core) { + void operator()(goal_ref const & in, + goal_ref_buffer & result, + expr_dependency_ref & core) override { SASSERT(in->is_well_sorted()); tactic_report report("split-clause", *in); TRACE("before_split_clause", in->display(tout);); - mc = 0; core = 0; + core = 0; ast_manager & m = in->m(); unsigned cls_pos = select_clause(m, in); if (cls_pos == UINT_MAX) { @@ -123,15 +117,10 @@ public: expr_dependency * cls_dep = in->dep(cls_pos); if (produce_proofs) 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++) { - goal * subgoal_i; - if (i == cls_sz - 1) - subgoal_i = in.get(); - else - subgoal_i = alloc(goal, *in); - expr * lit_i = cls->get_arg(i); + report_tactic_progress(":num-new-branches", cls->get_num_args()); + for (expr* lit_i : *cls) { + goal * subgoal_i = alloc(goal, *in); + subgoal_i->set(in->mc()); proof * pr_i = 0; if (produce_proofs) pr_i = m.mk_hypothesis(lit_i); @@ -139,6 +128,7 @@ public: subgoal_i->inc_depth(); result.push_back(subgoal_i); } + in->set(concat(in->pc(), result.size(), result.c_ptr())); } virtual void cleanup() { diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index 89013a6da..920521e0c 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/src/tactic/core/symmetry_reduce_tactic.cpp @@ -40,7 +40,6 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core); virtual void cleanup(); }; @@ -635,11 +634,10 @@ symmetry_reduce_tactic::~symmetry_reduce_tactic() { void symmetry_reduce_tactic::operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { fail_if_proof_generation("symmetry_reduce", g); fail_if_unsat_core_generation("symmetry_reduce", g); - mc = 0; core = 0; result.reset(); + 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 22a2dc500..11b7ceb8c 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -800,10 +800,9 @@ class tseitin_cnf_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("tseitin-cnf", *g); fail_if_proof_generation("tseitin-cnf", g); m_produce_models = g->models_enabled(); @@ -842,9 +841,7 @@ class tseitin_cnf_tactic : public tactic { g->assert_expr(cls); } if (m_produce_models && !m_fresh_vars.empty()) - mc = m_mc.get(); - else - mc = 0; + g->add(m_mc.get()); g->inc_depth(); result.push_back(g.get()); TRACE("tseitin_cnf", g->display(tout);); @@ -884,9 +881,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); report_tactic_progress(":cnf-aux-vars", m_imp->m_num_aux_vars); } diff --git a/src/tactic/equiv_proof_converter.h b/src/tactic/equiv_proof_converter.h index 0ee44aec2..1afd6e610 100644 --- a/src/tactic/equiv_proof_converter.h +++ b/src/tactic/equiv_proof_converter.h @@ -35,11 +35,11 @@ public: virtual ~equiv_proof_converter() {} - virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) { - m_replace(m, num_source, source, result); + proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override { + return m_replace(m, num_source, source); } - virtual proof_converter * translate(ast_translation & translator) { + proof_converter * translate(ast_translation & translator) override { return m_replace.translate(translator); } @@ -47,7 +47,7 @@ public: ast_manager& get_manager() { return m; } - virtual void display(std::ostream & out) {} + void display(std::ostream & out) override {} }; #endif diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 989caaa58..462bf28bd 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -37,20 +37,16 @@ public: dealloc(m_bv2fp); } - virtual void operator()(model_ref & md, unsigned goal_idx) { - SASSERT(goal_idx == 0); + void operator()(model_ref & md) override { model * new_model = alloc(model, m); convert(md.get(), new_model); md = new_model; } - virtual void operator()(model_ref & md) { - operator()(md, 0); - } - void display(std::ostream & out); + void display(std::ostream & out) override; - virtual model_converter * translate(ast_translation & translator); + model_converter * translate(ast_translation & translator) override; protected: fpa2bv_model_converter(ast_manager & m) : diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 99b50429c..3ed9f9cb0 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -48,14 +48,13 @@ class fpa2bv_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, 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; core = 0; result.reset(); + core = 0; result.reset(); tactic_report report("fpa2bv", *g); m_rw.reset(); @@ -99,7 +98,7 @@ class fpa2bv_tactic : public tactic { } if (g->models_enabled()) - mc = mk_fpa2bv_model_converter(m, m_conv); + g->add(mk_fpa2bv_model_converter(m, m_conv)); g->inc_depth(); result.push_back(g.get()); @@ -109,7 +108,7 @@ class fpa2bv_tactic : public tactic { SASSERT(g->is_well_sorted()); TRACE("fpa2bv", tout << "AFTER: " << std::endl; g->display(tout); - if (mc) mc->display(tout); tout << std::endl; ); + if (g->mc()) g->mc()->display(tout); tout << std::endl; ); } }; @@ -140,10 +139,9 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { try { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } catch (rewriter_exception & ex) { throw tactic_exception(ex.msg()); diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index 03361cac1..3993f20c9 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -23,8 +23,7 @@ Notes: #include "model/model_evaluator.h" -void generic_model_converter::operator()(model_ref & md, unsigned goal_idx) { - std::cout << "model converter\n"; +void generic_model_converter::operator()(model_ref & md) { TRACE("model_converter", tout << "before generic_model_converter\n"; model_v2_pp(tout, *md); display(tout);); model_evaluator ev(*(md.get())); ev.set_model_completion(true); @@ -35,12 +34,10 @@ void generic_model_converter::operator()(model_ref & md, unsigned goal_idx) { entry const& e = m_entries[i]; switch (e.m_instruction) { case HIDE: - std::cout << "hide " << e.m_f << "\n"; md->unregister_decl(e.m_f); break; case ADD: ev(e.m_def, val); - std::cout << e.m_f << " " << e.m_def << " " << val << "\n"; TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";); arity = e.m_f->get_arity(); if (arity == 0) { diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index 014725bb0..affafb0c1 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -46,19 +46,17 @@ public: void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); m_entries.push_back(entry(to_app(d)->get_decl(), e, m, ADD)); } - virtual void operator()(model_ref & md, unsigned goal_idx); - - virtual void operator()(svector & labels, unsigned goal_idx) {} + void operator()(labels_vec & labels) override {} - virtual void operator()(model_ref & md) { operator()(md, 0); } + void operator()(model_ref & md) override; - virtual void cancel() {} + void cancel() override {} - virtual void display(std::ostream & out); + void display(std::ostream & out) override; - virtual model_converter * translate(ast_translation & translator); + model_converter * translate(ast_translation & translator) override; - virtual void collect(ast_pp_util& visitor); + void collect(ast_pp_util& visitor) override; void operator()(expr_ref& fml) override; }; diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index ab1e2a9bc..da6a0dcf8 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -68,14 +68,9 @@ public: this->m_c2->operator()(fml); } - void operator()(model_ref & m, unsigned goal_idx) override { - this->m_c2->operator()(m, goal_idx); - this->m_c1->operator()(m, 0); - } - - void operator()(labels_vec & r, unsigned goal_idx) override { - this->m_c2->operator()(r, goal_idx); - this->m_c1->operator()(r, 0); + void operator()(labels_vec & r) override { + this->m_c2->operator()(r); + this->m_c1->operator()(r); } char const * get_name() const override { return "concat-model-converter"; } @@ -98,75 +93,6 @@ model_converter * concat(model_converter * mc1, model_converter * mc2) { return alloc(concat_model_converter, mc1, mc2); } -class concat_star_model_converter : public concat_star_converter { -public: - concat_star_model_converter(model_converter * mc1, unsigned num, model_converter * const * mc2s, unsigned * szs): - concat_star_converter(mc1, num, mc2s, szs) { - } - - void operator()(model_ref & m) override { - // TODO: delete method after conversion is complete - UNREACHABLE(); - } - - void operator()(model_ref & m, unsigned goal_idx) override { - unsigned num = this->m_c2s.size(); - for (unsigned i = 0; i < num; i++) { - if (goal_idx < this->m_szs[i]) { - // found the model converter that should be used - model_converter * c2 = this->m_c2s[i]; - if (c2) - c2->operator()(m, goal_idx); - if (m_c1) - this->m_c1->operator()(m, i); - return; - } - // invalid goal - goal_idx -= this->m_szs[i]; - } - UNREACHABLE(); - } - - void operator()(labels_vec & r, unsigned goal_idx) override { - unsigned num = this->m_c2s.size(); - for (unsigned i = 0; i < num; i++) { - if (goal_idx < this->m_szs[i]) { - // found the model converter that should be used - model_converter * c2 = this->m_c2s[i]; - if (c2) - c2->operator()(r, goal_idx); - if (m_c1) - this->m_c1->operator()(r, i); - return; - } - // invalid goal - goal_idx -= this->m_szs[i]; - } - UNREACHABLE(); - } - - char const * get_name() const override { return "concat-star-model-converter"; } - - model_converter * translate(ast_translation & translator) override { - return this->translate_core(translator); - } -}; - -model_converter * concat(model_converter * mc1, unsigned num, model_converter * const * mc2s, unsigned * szs) { - SASSERT(num > 0); - if (num == 1) - return concat(mc1, mc2s[0]); - unsigned i; - for (i = 0; i < num; i++) { - if (mc2s[i] != 0) - break; - } - if (i == num) { - // all mc2s are 0 - return mc1; - } - return alloc(concat_star_model_converter, mc1, num, mc2s, szs); -} class model2mc : public model_converter { model_ref m_model; @@ -182,11 +108,7 @@ public: m = m_model; } - void operator()(model_ref & m, unsigned goal_idx) override { - m = m_model; - } - - void operator()(labels_vec & r, unsigned goal_idx) { + void operator()(labels_vec & r) { r.append(m_labels.size(), m_labels.c_ptr()); } @@ -227,13 +149,13 @@ model_converter * model_and_labels2model_converter(model * m, buffer & r void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m) { if (mc) { m = alloc(model, mng); - (*mc)(m, 0); + (*mc)(m); } } -void apply(model_converter_ref & mc, model_ref & m, unsigned gidx) { +void apply(model_converter_ref & mc, model_ref & m) { if (mc) { - (*mc)(m, gidx); + (*mc)(m); } } diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h index 720ae1916..7069e868e 100644 --- a/src/tactic/model_converter.h +++ b/src/tactic/model_converter.h @@ -19,10 +19,10 @@ Notes: #ifndef MODEL_CONVERTER_H_ #define MODEL_CONVERTER_H_ +#include "util/ref.h" #include "ast/ast_pp_util.h" #include "model/model.h" #include "tactic/converter.h" -#include "util/ref.h" class labels_vec : public svector {}; class smt2_pp_environment; @@ -36,17 +36,11 @@ protected: public: - model_converter(): m_env(0) {} + model_converter(): m_env(nullptr) {} - virtual void operator()(model_ref & m) {} // TODO: delete + virtual void operator()(model_ref & m) = 0; - virtual void operator()(model_ref & m, unsigned goal_idx) { - // TODO: make it virtual after the transition to goal/tactic/tactical is complete - SASSERT(goal_idx == 0); - operator()(m); - } - - virtual void operator()(labels_vec & r, unsigned goal_idx) {} + virtual void operator()(labels_vec & r) {} virtual model_converter * translate(ast_translation & translator) = 0; @@ -61,25 +55,18 @@ public: }; typedef ref model_converter_ref; +typedef sref_vector model_converter_ref_vector; +typedef sref_buffer model_converter_ref_buffer; model_converter * concat(model_converter * mc1, model_converter * mc2); -/** - \brief \c mc1 is the model converter for a sequence of subgoals of size \c num. - Given an i in [0, num), mc2s[i] is the model converter for subgoal i, - and num_subgoals[i] is the number of subgoals of subgoals[i]. -*/ -model_converter * concat(model_converter * mc1, unsigned num, model_converter * const * mc2s, unsigned * num_subgoals); - model_converter * model2model_converter(model * m); model_converter * model_and_labels2model_converter(model * m, buffer &r); void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m); -void apply(model_converter_ref & mc, model_ref & m, unsigned gidx); +void apply(model_converter_ref & mc, model_ref & m); -typedef sref_vector model_converter_ref_vector; -typedef sref_buffer model_converter_ref_buffer; #endif diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index bc7c5d49c..7a8a0930c 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -210,7 +210,7 @@ private: } generic_model_converter filter(m); for (func_decl* f : m_bv_fns) filter.hide(f); - filter(mdl, 0); + filter(mdl); } void extend_model(model_ref& mdl) { @@ -225,7 +225,7 @@ private: TRACE("int2bv", tout << mk_pp(kv.m_key, m) << " " << value << "\n";); ext.add(kv.m_key, value); } - ext(mdl, 0); + ext(mdl); } void accumulate_sub(expr_safe_replace& sub) const { diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 50fb7d925..4feaa622b 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -167,14 +167,14 @@ public: for (auto const& kv : m_rewriter.enum2bv()) { filter.hide(kv.m_value); } - filter(mdl, 0); + filter(mdl); } void extend_model(model_ref& mdl) { generic_model_converter ext(m); for (auto const& kv : m_rewriter.enum2def()) ext.add(kv.m_key, kv.m_value); - ext(mdl, 0); + ext(mdl); } virtual unsigned get_num_assertions() const { diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 16eb2b4a7..abb8df188 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, expr_dependency_ref & dep) { + void operator ()(const goal_ref & g,goal_ref_buffer & result, 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); @@ -560,8 +560,7 @@ public: switch (is_sat) { case l_true: if (g->models_enabled()) { - mc = model2model_converter(mdl.get()); - mc = concat(fmc.get(), mc.get()); + g->add(concat(fmc.get(), model2model_converter(mdl.get()))); } g->reset(); break; diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index 334d14d86..9b8eed98d 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -118,7 +118,7 @@ public: for (func_decl* f : fns) { filter.hide(f); } - filter(mdl, 0); + filter(mdl); } virtual unsigned get_num_assertions() const { diff --git a/src/tactic/proof_converter.cpp b/src/tactic/proof_converter.cpp index 095488415..a8d3ff578 100644 --- a/src/tactic/proof_converter.cpp +++ b/src/tactic/proof_converter.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "tactic/proof_converter.h" +#include "tactic/goal.h" #include "ast/ast_smt2_pp.h" class concat_proof_converter : public concat_converter { @@ -25,14 +26,14 @@ public: virtual char const * get_name() const { return "concat-proof-converter"; } - virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) { + proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override { proof_ref tmp(m); - this->m_c2->operator()(m, num_source, source, tmp); + tmp = this->m_c2->operator()(m, num_source, source); proof * new_source = tmp.get(); - this->m_c1->operator()(m, 1, &new_source, result); + return this->m_c1->operator()(m, 1, &new_source); } - virtual proof_converter * translate(ast_translation & translator) { + proof_converter * translate(ast_translation & translator) override { return this->translate_core(translator); } }; @@ -45,66 +46,39 @@ proof_converter * concat(proof_converter * pc1, proof_converter * pc2) { return alloc(concat_proof_converter, pc1, pc2); } -class concat_star_proof_converter : public concat_star_converter { +class subgoal_proof_converter : public proof_converter { + proof_converter_ref m_pc; + goal_ref_buffer m_goals; public: - concat_star_proof_converter(proof_converter * pc1, unsigned num, proof_converter * const * pc2s, unsigned * szs): - concat_star_converter(pc1, num, pc2s, szs) { + subgoal_proof_converter(proof_converter* pc, unsigned n, goal * const* goals): + m_pc(pc) + { + for (unsigned i = 0; i < n; ++i) m_goals.push_back(goals[i]); } - virtual char const * get_name() const { return "concat-star-proof-converter"; } - - virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) { - unsigned num = this->m_szs.size(); -#ifdef Z3DEBUG - unsigned sum = 0; - for (unsigned i = 0; i < num; i++) { - sum += this->m_szs[i]; - } - SASSERT(sum == num_source); -#endif - proof_ref_buffer tmp_prs(m); - for (unsigned i = 0; i < num; i++) { - unsigned sz = m_szs[i]; - proof_converter * c2 = m_c2s[i]; - proof_ref pr(m); - if (c2) { - (*c2)(m, sz, source, pr); - } - else { - SASSERT(sz == 1); - pr = *source; - } - source += sz; - tmp_prs.push_back(pr.get()); - } - if (m_c1) { - (*m_c1)(m, tmp_prs.size(), tmp_prs.c_ptr(), result); - } - else { - SASSERT(tmp_prs.size() == 1); - result = tmp_prs[0]; + proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override { + // ignore the proofs from the arguments, instead obtain the proofs fromt he subgoals. + SASSERT(num_source == 0); + proof_converter_ref_buffer pc_buffer; + for (goal_ref g : m_goals) { + pc_buffer.push_back(g->pc()); } + return apply(m, m_pc, pc_buffer); } - virtual proof_converter * translate(ast_translation & translator) { - return this->translate_core(translator); + proof_converter* translate(ast_translation& tr) override { + proof_converter_ref pc1 = m_pc->translate(tr); + goal_ref_buffer goals; + for (goal_ref g : m_goals) goals.push_back(g->translate(tr)); + return alloc(subgoal_proof_converter, pc1.get(), goals.size(), goals.c_ptr()); } + + void display(std::ostream& out) override {} + }; -proof_converter * concat(proof_converter * pc1, unsigned num, proof_converter * const * pc2s, unsigned * szs) { - SASSERT(num > 0); - if (num == 1) - return concat(pc1, pc2s[0]); - unsigned i; - for (i = 0; i < num; i++) { - if (pc2s[i] != 0) - break; - } - if (i == num) { - // all pc2s are 0 - return pc1; - } - return alloc(concat_star_proof_converter, pc1, num, pc2s, szs); +proof_converter * concat(proof_converter *pc, unsigned n, goal* const* goals) { + return alloc(subgoal_proof_converter, pc, n, goals); } class proof2pc : public proof_converter { @@ -113,16 +87,16 @@ public: proof2pc(ast_manager & m, proof * pr):m_pr(pr, m) {} virtual ~proof2pc() {} - virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) { + proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override { SASSERT(num_source == 0); - result = m_pr; + return m_pr; } - virtual proof_converter * translate(ast_translation & translator) { + proof_converter * translate(ast_translation & translator) override { return alloc(proof2pc, translator.to(), translator(m_pr.get())); } - virtual void display(std::ostream & out) { + void display(std::ostream & out) override { out << "(proof->proof-converter-wrapper\n" << mk_ismt2_pp(m_pr.get(), m_pr.get_manager()) << ")\n"; } }; @@ -136,7 +110,7 @@ proof_converter * proof2proof_converter(ast_manager & m, proof * pr) { void apply(ast_manager & m, proof_converter * pc, proof_ref & pr) { if (pc) { proof * _pr = pr.get(); - (*pc)(m, 1, &_pr, pr); + pr = (*pc)(m, 1, &_pr); } } @@ -148,15 +122,15 @@ void apply(ast_manager & m, proof_converter * pc, proof_ref & pr) { pc1 and pc2s must be different from 0. */ -void apply(ast_manager & m, proof_converter_ref & pc1, proof_converter_ref_buffer & pc2s, proof_ref & result) { +proof_ref apply(ast_manager & m, proof_converter_ref & pc1, proof_converter_ref_buffer & pc2s) { SASSERT(pc1); proof_ref_buffer prs(m); unsigned sz = pc2s.size(); for (unsigned i = 0; i < sz; i++) { proof_ref pr(m); SASSERT(pc2s[i]); // proof production is enabled - pc2s[i]->operator()(m, 0, 0, pr); + pr = pc2s[i]->operator()(m, 0, 0); prs.push_back(pr); } - (*pc1)(m, sz, prs.c_ptr(), result); + return (*pc1)(m, sz, prs.c_ptr()); } diff --git a/src/tactic/proof_converter.h b/src/tactic/proof_converter.h index e925436d2..162623da9 100644 --- a/src/tactic/proof_converter.h +++ b/src/tactic/proof_converter.h @@ -20,33 +20,34 @@ Notes: #define PROOF_CONVERTER_H_ #include "ast/ast.h" -#include "tactic/converter.h" #include "util/ref.h" +#include "tactic/converter.h" +class goal; class proof_converter : public converter { public: virtual ~proof_converter() { } - virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) = 0; + virtual proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) = 0; virtual proof_converter * translate(ast_translation & translator) = 0; }; typedef ref proof_converter_ref; +typedef sref_vector proof_converter_ref_vector; +typedef sref_buffer proof_converter_ref_buffer; + proof_converter * concat(proof_converter * pc1, proof_converter * pc2); /** - \brief \c pc1 is the proof converter for a sequence of subgoals of size \c num. - Given an i in [0, num), pc2s[i] is the proof converter for subgoal i, - and num_subgoals[i] is the number of subgoals of subgoals[i]. -*/ -proof_converter * concat(proof_converter * pc1, unsigned num, proof_converter * const * pc2s, unsigned * num_subgoals); + \brief create a proof converter that takes a set of subgoals and converts their proofs to a proof of + the goal they were derived from. + */ +proof_converter * concat(proof_converter *pc1, unsigned n, goal* const* goals); proof_converter * proof2proof_converter(ast_manager & m, proof * pr); -typedef sref_vector proof_converter_ref_vector; -typedef sref_buffer proof_converter_ref_buffer; - -void apply(ast_manager & m, proof_converter_ref & pc1, proof_converter_ref_buffer & pc2s, proof_ref & result); void apply(ast_manager & m, proof_converter * pc, proof_ref & pr); +proof_ref apply(ast_manager & m, proof_converter_ref & pc1, proof_converter_ref_buffer & pc2s); + #endif diff --git a/src/tactic/replace_proof_converter.cpp b/src/tactic/replace_proof_converter.cpp index 98f28bb1b..9ef49dd5f 100644 --- a/src/tactic/replace_proof_converter.cpp +++ b/src/tactic/replace_proof_converter.cpp @@ -53,8 +53,7 @@ public: }; -void replace_proof_converter::operator()(ast_manager & m, unsigned num_source, - proof * const * source, proof_ref & result) { +proof_ref replace_proof_converter::operator()(ast_manager & m, unsigned num_source, proof * const * source) { SASSERT(num_source == 1); replace_map replace(m); proof_ref p(m); @@ -73,14 +72,12 @@ void replace_proof_converter::operator()(ast_manager & m, unsigned num_source, replace.apply(tmp); TRACE("proof_converter", tout << mk_pp(source[0], m) << "\n"; tout << mk_pp(tmp.get(), m) << "\n";); - result = to_app(tmp); + return proof_ref(to_app(tmp), m); } proof_converter * replace_proof_converter::translate(ast_translation & translator) { replace_proof_converter* rp = alloc(replace_proof_converter, m); - for (unsigned i = 0; i < m_proofs.size(); ++i) { - rp->insert(translator(m_proofs[i].get())); - } + for (proof* p : m_proofs) rp->insert(translator(p)); return rp; } diff --git a/src/tactic/replace_proof_converter.h b/src/tactic/replace_proof_converter.h index d5cf7dc31..91bbc4813 100644 --- a/src/tactic/replace_proof_converter.h +++ b/src/tactic/replace_proof_converter.h @@ -34,9 +34,9 @@ public: virtual ~replace_proof_converter() {} - virtual void operator()(ast_manager & _m, unsigned num_source, proof * const * source, proof_ref & result); + proof_ref operator()(ast_manager & _m, unsigned num_source, proof * const * source) override; - virtual proof_converter * translate(ast_translation & translator); + proof_converter * translate(ast_translation & translator) override; void insert(proof* p) { m_proofs.push_back(p); } @@ -45,7 +45,7 @@ public: // run the replacements the inverse direction. void invert() { m_proofs.reverse(); } - virtual void display(std::ostream & out) {} + void display(std::ostream & out) override {} }; diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 4e4efeb8f..532169d46 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -48,9 +48,8 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; core = 0; + core = 0; TRACE("sine", g->display(tout);); TRACE("sine", tout << g->size();); @@ -66,8 +65,6 @@ public: result.push_back(g.get()); TRACE("sine", result[0]->display(tout);); SASSERT(g->is_well_sorted()); - generic_model_converter * fmc = alloc(generic_model_converter, m); - mc = fmc; } virtual void cleanup() { diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index a96cf117a..18328f0b8 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -61,16 +61,16 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; result.reset(); + core = 0; result.reset(); TRACE("sls", g->display(tout);); tactic_report report("sls", *g); + model_converter_ref mc; m_engine->operator()(g, mc); - + g->add(mc.get()); g->inc_depth(); result.push_back(g.get()); TRACE("sls", g->display(tout);); diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index a4995535e..84d445f45 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -55,9 +55,7 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; ast_manager& m(g->m()); tactic_report report("qfufbv_ackr", *g); fail_if_unsat_core_generation("qfufbv_ackr", g); @@ -79,7 +77,7 @@ public: // report model if (g->models_enabled() && (o == l_true)) { model_ref abstr_model = imp->get_model(); - mc = mk_qfufbv_ackr_model_converter(m, imp->get_info(), abstr_model); + g->add(mk_qfufbv_ackr_model_converter(m, imp->get_info(), abstr_model)); } } diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 3a8e128ec..ed78f229d 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -69,11 +69,9 @@ 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, expr_dependency_ref & core) { result.reset(); result.push_back(in.get()); - mc = 0; core = 0; } @@ -85,14 +83,13 @@ class fail_tactic : public tactic { public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { throw tactic_exception("fail tactic"); } - virtual void cleanup() {} + void cleanup() override {} - virtual tactic * translate(ast_manager & m) { return this; } + tactic * translate(ast_manager & m) override { return this; } }; tactic * mk_fail_tactic() { @@ -105,12 +102,11 @@ class report_verbose_tactic : public skip_tactic { public: report_verbose_tactic(char const * msg, unsigned lvl) : m_msg(msg), m_lvl(lvl) {} - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - expr_dependency_ref & core) { + void operator()(goal_ref const & in, + goal_ref_buffer & result, + expr_dependency_ref & core) override { IF_VERBOSE(m_lvl, verbose_stream() << m_msg << "\n";); - skip_tactic::operator()(in, result, mc, core); + skip_tactic::operator()(in, result, core); } }; @@ -123,13 +119,12 @@ class trace_tactic : public skip_tactic { public: trace_tactic(char const * tag): m_tag(tag) {} - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - expr_dependency_ref & core) { + void operator()(goal_ref const & in, + goal_ref_buffer & result, + expr_dependency_ref & core) override { TRACE(m_tag, in->display(tout);); (void)m_tag; - skip_tactic::operator()(in, result, mc, core); + skip_tactic::operator()(in, result, core); } }; @@ -141,13 +136,12 @@ class fail_if_undecided_tactic : public skip_tactic { public: fail_if_undecided_tactic() {} - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - expr_dependency_ref & core) { + void operator()(goal_ref const & in, + goal_ref_buffer & result, + expr_dependency_ref & core) override { if (!in->is_decided()) throw tactic_exception("undecided"); - skip_tactic::operator()(in, result, mc, core); + skip_tactic::operator()(in, result, core); } }; @@ -155,10 +149,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, expr_dependency_ref & core) { +void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, expr_dependency_ref & core) { t.reset_statistics(); try { - t(in, result, mc, core); + t(in, result, core); t.cleanup(); } catch (tactic_exception & ex) { @@ -169,7 +163,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_conve } -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) { +lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { bool models_enabled = g->models_enabled(); bool proofs_enabled = g->proofs_enabled(); bool cores_enabled = g->unsat_core_enabled(); @@ -179,21 +173,20 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, model_converter_ref& m ast_manager & m = g->m(); goal_ref_buffer r; try { - exec(t, g, r, mc, core); + exec(t, g, r, core); } catch (tactic_exception & ex) { reason_unknown = ex.msg(); return l_undef; } - TRACE("tactic_mc", mc->display(tout);); TRACE("tactic_check_sat", tout << "r.size(): " << r.size() << "\n"; for (unsigned i = 0; i < r.size(); i++) r[i]->display(tout);); if (is_decided_sat(r)) { - if (models_enabled) { - if (mc) - (*mc)(labels, 0); + model_converter_ref mc = r[0]->mc(); + if (mc.get()) { + (*mc)(labels); model_converter2model(m, mc.get(), md); if (!md) { // create empty model. @@ -210,10 +203,11 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, model_converter_ref& m return l_false; } else { - if (models_enabled) { + if (models_enabled && r.size() >= 1) { + model_converter_ref mc = r[0]->mc(); model_converter2model(m, mc.get(), md); if (mc) - (*mc)(labels, 0); + (*mc)(labels); } reason_unknown = "incomplete"; return l_undef; diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 3b8110fd2..98c57f12c 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -24,8 +24,6 @@ Notes: #include "tactic/goal.h" #include "util/params.h" #include "util/statistics.h" -#include "tactic/model_converter.h" -#include "tactic/proof_converter.h" #include "tactic/tactic_exception.h" #include "util/lbool.h" @@ -50,19 +48,7 @@ public: The list of resultant subgoals is stored in \c result. The content of \c in may be destroyed during the operation. - - The resultant model converter \c mc can be used to convert a model for one of the returned subgoals - into a model for \in. If mc == 0, then model construction is disabled or any model for a subgoal - of \c in is also a model for \c in. - If \c result is decided_sat (i.e., it contains a single empty subgoal), then - the model converter is just wrapping the model. - - The resultant proof converter \c pc can be used to convert proofs for each subgoal in \c result - into a proof for \c in. If pc == 0, then one of the following conditions should hold: - 1- proof construction is disabled, - 2- result contains a single subgoal, and any proof of unsatisfiability for this subgoal is a proof for \c in. - 3- result is an decided_unsat (i.e., it contains a single unsat subgoal). The actual proof can be extracted from this goal. - + The output parameter \c core is used to accumulate the unsat core of closed subgoals. It must be 0 if dependency tracking is disabled, or the result is decided unsat, or no tagged assertions were used to close any subgoal. @@ -77,7 +63,6 @@ public: */ virtual void operator()(/* in */ goal_ref const & in, /* out */ goal_ref_buffer & result, - /* out */ model_converter_ref & mc, /* out */ expr_dependency_ref & core) = 0; virtual void collect_statistics(statistics & st) const {} @@ -118,9 +103,9 @@ 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, expr_dependency_ref & core); - virtual void cleanup() {} - virtual tactic * translate(ast_manager & m) { return this; } + void operator()(goal_ref const & in, goal_ref_buffer & result, expr_dependency_ref & core) override; + void cleanup() override {} + tactic * translate(ast_manager & m) override { return this; } }; tactic * mk_skip_tactic(); @@ -151,8 +136,8 @@ 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, 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); +void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, expr_dependency_ref & core); +lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown); // Throws an exception if goal \c in requires proof generation. void fail_if_proof_generation(char const * tactic_name, goal_ref const & in); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 3f94908b3..5003a4f9d 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -16,33 +16,28 @@ Author: Notes: --*/ -#include "tactic/tactical.h" #include "util/scoped_timer.h" #include "util/cancel_eh.h" #include "util/cooperate.h" #include "util/scoped_ptr_vector.h" #include "util/z3_omp.h" +#include "tactic/tactical.h" class binary_tactical : public tactic { protected: - tactic * m_t1; - tactic * m_t2; - + tactic_ref m_t1; + tactic_ref m_t2; public: + binary_tactical(tactic * t1, tactic * t2): m_t1(t1), m_t2(t2) { SASSERT(m_t1); SASSERT(m_t2); - m_t1->inc_ref(); - m_t2->inc_ref(); } - virtual ~binary_tactical() { - m_t1->dec_ref(); - m_t2->dec_ref(); - } + virtual ~binary_tactical() {} virtual void updt_params(params_ref const & p) { m_t1->updt_params(p); @@ -108,7 +103,6 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { bool models_enabled = in->models_enabled(); @@ -117,50 +111,35 @@ public: ast_manager & m = in->m(); goal_ref_buffer r1; - model_converter_ref mc1; expr_dependency_ref core1(m); result.reset(); - mc = 0; core = 0; - m_t1->operator()(in, r1, mc1, core1); + m_t1->operator()(in, r1, 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) { if (r1[0]->is_decided()) { - result.push_back(r1[0]); - if (models_enabled) mc = mc1; + result.push_back(r1[0]); return; } goal_ref r1_0 = r1[0]; - m_t2->operator()(r1_0, result, mc, core); - if (models_enabled) mc = concat(mc1.get(), mc.get()); + m_t2->operator()(r1_0, result, core); if (cores_enabled) core = m.mk_join(core1.get(), core); } else { if (cores_enabled) core = core1; - 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; + r2.reset(); expr_dependency_ref core2(m); - m_t2->operator()(g, r2, mc2, core2); + m_t2->operator()(g, r2, core2); if (is_decided(r2)) { SASSERT(r2.size() == 1); if (is_decided_sat(r2)) { // found solution... result.push_back(r2[0]); - if (models_enabled) { - // mc2 contains the actual model - model_ref md; - md = alloc(model, m); - apply(mc2, md, 0); - apply(mc1, md, i); - mc = model2model_converter(md.get()); - } SASSERT(!core); return; } @@ -169,45 +148,30 @@ public: // the proof and unsat core of a decided_unsat goal are stored in the node itself. // core2 must be 0. SASSERT(!core2); - if (models_enabled) mc_buffer.push_back(0); - if (models_enabled || proofs_enabled) sz_buffer.push_back(0); if (cores_enabled) core = m.mk_join(core.get(), r2[0]->dep(0)); } } else { result.append(r2.size(), r2.c_ptr()); - if (models_enabled) mc_buffer.push_back(mc2.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, pc, pc_buffer, pr); - in->set(proof2proof_converter(m, pr)); + apply(m, in->pc(), pr); } SASSERT(cores_enabled || core == 0); in->assert_expr(m.mk_false(), pr, core); core = 0; result.push_back(in.get()); - SASSERT(!mc); SASSERT(!core); + SASSERT(!core); } else { - if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_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); } } @@ -272,92 +236,58 @@ tactic * and_then(unsigned num, tactic * const * ts) { class nary_tactical : public tactic { protected: - ptr_vector m_ts; + sref_vector m_ts; public: nary_tactical(unsigned num, tactic * const * ts) { for (unsigned i = 0; i < num; i++) { SASSERT(ts[i]); m_ts.push_back(ts[i]); - ts[i]->inc_ref(); } } - virtual ~nary_tactical() { - unsigned sz = m_ts.size(); - for (unsigned i = 0; i < sz; i++) { - m_ts[i]->dec_ref(); - } - } + virtual ~nary_tactical() {} - virtual void updt_params(params_ref const & p) { + void updt_params(params_ref const & p) override { TRACE("nary_tactical_updt_params", tout << "updt_params: " << p << "\n";); - ptr_vector::iterator it = m_ts.begin(); - ptr_vector::iterator end = m_ts.end(); - for (; it != end; ++it) - (*it)->updt_params(p); + for (tactic* t : m_ts) t->updt_params(p); } - virtual void collect_param_descrs(param_descrs & r) { - ptr_vector::iterator it = m_ts.begin(); - ptr_vector::iterator end = m_ts.end(); - for (; it != end; ++it) - (*it)->collect_param_descrs(r); + void collect_param_descrs(param_descrs & r) override { + for (tactic* t : m_ts) t->collect_param_descrs(r); } - virtual void collect_statistics(statistics & st) const { - ptr_vector::const_iterator it = m_ts.begin(); - ptr_vector::const_iterator end = m_ts.end(); - for (; it != end; ++it) - (*it)->collect_statistics(st); + void collect_statistics(statistics & st) const override { + for (tactic const* t : m_ts) t->collect_statistics(st); } - virtual void reset_statistics() { - ptr_vector::const_iterator it = m_ts.begin(); - ptr_vector::const_iterator end = m_ts.end(); - for (; it != end; ++it) - (*it)->reset_statistics(); + void reset_statistics() override { + for (tactic* t : m_ts) t->reset_statistics(); } - virtual void cleanup() { - ptr_vector::iterator it = m_ts.begin(); - ptr_vector::iterator end = m_ts.end(); - for (; it != end; ++it) - (*it)->cleanup(); + void cleanup() override { + for (tactic* t : m_ts) t->cleanup(); } - virtual void reset() { - ptr_vector::iterator it = m_ts.begin(); - ptr_vector::iterator end = m_ts.end(); - for (; it != end; ++it) - (*it)->reset(); + void reset() override { + for (tactic* t : m_ts) t->reset(); } - virtual void set_logic(symbol const & l) { - ptr_vector::iterator it = m_ts.begin(); - ptr_vector::iterator end = m_ts.end(); - for (; it != end; ++it) - (*it)->set_logic(l); + void set_logic(symbol const & l) override { + for (tactic* t : m_ts) t->set_logic(l); } - virtual void set_progress_callback(progress_callback * callback) { - ptr_vector::iterator it = m_ts.begin(); - ptr_vector::iterator end = m_ts.end(); - for (; it != end; ++it) - (*it)->set_progress_callback(callback); + void set_progress_callback(progress_callback * callback) override { + for (tactic* t : m_ts) t->set_progress_callback(callback); } protected: template tactic * translate_core(ast_manager & m) { - ptr_buffer new_ts; - ptr_vector::iterator it = m_ts.begin(); - ptr_vector::iterator end = m_ts.end(); - for (; it != end; ++it) { - tactic * curr = *it; - tactic * new_curr = curr->translate(m); - new_ts.push_back(new_curr); + sref_vector new_ts; + for (tactic* curr : m_ts) { + new_ts.push_back(curr->translate(m)); } return alloc(T, new_ts.size(), new_ts.c_ptr()); } @@ -372,7 +302,6 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { goal orig(*(in.get())); proof_converter_ref pc = in->pc(); @@ -381,13 +310,12 @@ public: for (i = 0; i < sz; i++) { tactic * t = m_ts[i]; result.reset(); - mc = 0; pc = 0; core = 0; SASSERT(sz > 0); if (i < sz - 1) { try { - t->operator()(in, result, mc, core); + t->operator()(in, result, core); return; } catch (tactic_exception &) { @@ -395,7 +323,7 @@ public: } } else { - t->operator()(in, result, mc, core); + t->operator()(in, result, core); return; } in->reset_all(); @@ -472,7 +400,6 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { bool use_seq; #ifdef _NO_OMP_ @@ -482,7 +409,7 @@ public: #endif if (use_seq) { // execute tasks sequentially - or_else_tactical::operator()(in, result, mc, core); + or_else_tactical::operator()(in, result, core); return; } @@ -510,14 +437,13 @@ public: #pragma omp parallel for for (int i = 0; i < static_cast(sz); i++) { goal_ref_buffer _result; - model_converter_ref _mc; expr_dependency_ref _core(*(managers[i])); goal_ref in_copy = in_copies[i]; tactic & t = *(ts.get(i)); try { - t(in_copy, _result, _mc, _core); + t(in_copy, _result, _core); bool first = false; #pragma omp critical (par_tactical) { @@ -533,10 +459,9 @@ public: } } ast_translation translator(*(managers[i]), m, false); - for (unsigned k = 0; k < _result.size(); k++) { - result.push_back(_result[k]->translate(translator)); + for (goal* g : _result) { + result.push_back(g->translate(translator)); } - mc = _mc ? _mc->translate(translator) : 0; expr_dependency_translation td(translator); core = td(_core); } @@ -561,7 +486,6 @@ public: } } if (finished_id == UINT_MAX) { - mc = 0; switch (ex_kind) { case ERROR_EX: throw z3_error(error_code); case TACTIC_EX: throw tactic_exception(ex_msg.c_str()); @@ -600,7 +524,6 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { bool use_seq; #ifdef _NO_OMP_ @@ -610,22 +533,22 @@ public: #endif if (use_seq) { // execute tasks sequentially - and_then_tactical::operator()(in, result, mc, core); + and_then_tactical::operator()(in, result, core); return; } + // enabling proofs is possible, but requires translating subgoals back. + fail_if_proof_generation("par_and_then", in); bool models_enabled = in->models_enabled(); bool proofs_enabled = in->proofs_enabled(); bool cores_enabled = in->unsat_core_enabled(); ast_manager & m = in->m(); goal_ref_buffer r1; - model_converter_ref mc1; expr_dependency_ref core1(m); result.reset(); - mc = 0; core = 0; - m_t1->operator()(in, r1, mc1, core1); + m_t1->operator()(in, r1, core1); SASSERT(!is_decided(r1) || !core1); // the core of decided goals is 0 unsigned r1_size = r1.size(); SASSERT(r1_size > 0); @@ -633,13 +556,11 @@ public: // Only one subgoal created... no need for parallelism if (r1[0]->is_decided()) { result.push_back(r1[0]); - if (models_enabled) mc = mc1; SASSERT(!core); return; } goal_ref r1_0 = r1[0]; - m_t2->operator()(r1_0, result, mc, core); - if (models_enabled) mc = concat(mc1.get(), mc.get()); + m_t2->operator()(r1_0, result, core); if (cores_enabled) core = m.mk_join(core1.get(), core); } else { @@ -657,15 +578,11 @@ public: ts2.push_back(m_t2->translate(*new_m)); } - model_converter_ref_buffer mc_buffer; - proof_converter_ref_buffer pc_buffer; scoped_ptr_vector core_buffer; scoped_ptr_vector goals_vect; - 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; @@ -679,13 +596,12 @@ public: goal_ref new_g = g_copies[i]; goal_ref_buffer r2; - model_converter_ref mc2; expr_dependency_ref core2(new_m); bool curr_failed = false; try { - ts2[i]->operator()(new_g, r2, mc2, core2); + ts2[i]->operator()(new_g, r2, core2); } catch (tactic_exception & ex) { #pragma omp critical (par_and_then_tactical) @@ -750,30 +666,16 @@ public: } ast_translation translator(new_m, m, false); SASSERT(r2.size() == 1); - result.push_back(r2[0]->translate(translator)); - if (models_enabled) { - // mc2 contains the actual model - mc2 = mc2 ? mc2->translate(translator) : 0; - model_ref md; - md = alloc(model, m); - apply(mc2, md, 0); - apply(mc1, md, i); - mc = model2model_converter(md.get()); - } + result.push_back(r2[0]->translate(translator)); 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. + // core2 must be 0. SASSERT(!core2); - if (models_enabled) mc_buffer.set(i, 0); - if (proofs_enabled) { - proof * pr = r2[0]->pr(0); - pc_buffer.push_back(proof2proof_converter(m, pr)); - } if (cores_enabled && r2[0]->dep(0) != 0) { expr_dependency_ref * new_dep = alloc(expr_dependency_ref, new_m); *new_dep = r2[0]->dep(0); @@ -785,8 +687,6 @@ public: goal_ref_buffer * new_r2 = alloc(goal_ref_buffer); goals_vect.set(i, new_r2); new_r2->append(r2.size(), r2.c_ptr()); - mc_buffer.set(i, mc2.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; @@ -809,23 +709,20 @@ public: return; core = 0; - sbuffer sz_buffer; for (unsigned i = 0; i < r1_size; i++) { ast_translation translator(*(managers[i]), m, false); goal_ref_buffer * r = goals_vect[i]; + unsigned j = result.size(); if (r != 0) { for (unsigned k = 0; k < r->size(); k++) { result.push_back((*r)[k]->translate(translator)); } - sz_buffer.push_back(r->size()); } - else { - sz_buffer.push_back(0); + if (proofs_enabled) { + // update proof converter of r1[i] + r1[i]->set(concat(r1[i]->pc(), result.size() - j, result.c_ptr() + j)); } - if (mc_buffer[i] != 0) - mc_buffer.set(i, mc_buffer[i]->translate(translator)); - if (pc_buffer[i] != 0) - pc_buffer.set(i, pc_buffer[i]->translate(translator)); + expr_dependency_translation td(translator); if (core_buffer[i] != 0) { expr_dependency_ref curr_core(m); @@ -841,23 +738,15 @@ public: in->reset_all(); proof_ref pr(m); 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)); + apply(m, in->pc(), pr); } SASSERT(cores_enabled || core == 0); in->assert_expr(m.mk_false(), pr, core); core = 0; result.push_back(in.get()); - SASSERT(!mc); SASSERT(!core); + SASSERT(!core); } else { - if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_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); } } @@ -886,25 +775,21 @@ tactic * par_and_then(unsigned num, tactic * const * ts) { class unary_tactical : public tactic { protected: - tactic * m_t; + tactic_ref m_t; public: unary_tactical(tactic * t): m_t(t) { - SASSERT(t); - t->inc_ref(); + SASSERT(t); } - virtual ~unary_tactical() { - m_t->dec_ref(); - } + virtual ~unary_tactical() { } virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - m_t->operator()(in, result, mc, core); + m_t->operator()(in, result, core); } virtual void cleanup(void) { m_t->cleanup(); } @@ -930,12 +815,10 @@ class repeat_tactical : public unary_tactical { void operator()(unsigned depth, goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { // TODO: implement a non-recursive version. if (depth > m_max_depth) { result.push_back(in.get()); - mc = 0; core = 0; return; } @@ -945,20 +828,17 @@ class repeat_tactical : public unary_tactical { bool cores_enabled = in->unsat_core_enabled(); ast_manager & m = in->m(); - goal_ref_buffer r1; - model_converter_ref mc1; + goal_ref_buffer r1; expr_dependency_ref core1(m); result.reset(); - mc = 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, core1); - if (is_equal(orig_in, *(in.get()))) { - result.push_back(r1[0]); - if (models_enabled) mc = mc1; - if (cores_enabled) core = core1; + m_t->operator()(in, r1, core1); + if (r1.size() == 1 && is_equal(orig_in, *(r1[0]))) { + result.push_back(r1[0]); + if (cores_enabled) core = core1; return; } } @@ -966,62 +846,41 @@ class repeat_tactical : public unary_tactical { SASSERT(r1_size > 0); if (r1_size == 1) { if (r1[0]->is_decided()) { - result.push_back(r1[0]); - if (models_enabled) mc = mc1; + result.push_back(r1[0]); SASSERT(!core); return; } goal_ref r1_0 = r1[0]; - operator()(depth+1, r1_0, result, mc, core); - if (models_enabled) mc = concat(mc.get(), mc1.get()); - if (cores_enabled) core = m.mk_join(core1.get(), core); + operator()(depth+1, r1_0, result, core); + if (cores_enabled) core = m.mk_join(core1.get(), core); } else { if (cores_enabled) core = core1; - 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; + r2.reset(); expr_dependency_ref core2(m); - operator()(depth+1, g, r2, mc2, core2); + operator()(depth+1, g, r2, core2); if (is_decided(r2)) { SASSERT(r2.size() == 1); if (is_decided_sat(r2)) { // found solution... result.push_back(r2[0]); - if (models_enabled) { - // mc2 contains the actual model - model_ref md; - if (mc2) (*mc2)(md, 0); - if (mc1) (*mc1)(md, i); - mc = model2model_converter(md.get()); - } SASSERT(!core); return; } else { SASSERT(is_decided_unsat(r2)); SASSERT(!core2); - if (models_enabled) mc_buffer.push_back(0); - if (models_enabled || proofs_enabled) sz_buffer.push_back(0); if (cores_enabled) core = m.mk_join(core.get(), r2[0]->dep(0)); } } else { - result.append(r2.size(), r2.c_ptr()); - if (models_enabled) mc_buffer.push_back(mc2.get()); - if (models_enabled || proofs_enabled) sz_buffer.push_back(r2.size()); + result.append(r2.size(), r2.c_ptr()); 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. @@ -1029,19 +888,15 @@ class repeat_tactical : public unary_tactical { in->reset_all(); proof_ref pr(m); if (proofs_enabled) { - proof_converter_ref pc = in->pc(); - apply(m, pc, pc_buffer, pr); - in->set(proof2proof_converter(m, pr)); + apply(m, in->pc(), pr); } SASSERT(cores_enabled || core == 0); in->assert_expr(m.mk_false(), pr, core); core = 0; result.push_back(in.get()); - SASSERT(!mc); SASSERT(!core); + SASSERT(!core); } else { - if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_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); } } @@ -1055,9 +910,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - operator()(0, in, result, mc, core); + operator()(0, in, result, core); } virtual tactic * translate(ast_manager & m) { @@ -1077,12 +931,10 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - m_t->operator()(in, result, mc, core); + m_t->operator()(in, result, core); if (result.size() > m_threshold) { result.reset(); - mc = 0; core = 0; throw tactic_exception("failed-if-branching tactical"); } @@ -1104,9 +956,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - m_t->operator()(in, result, mc, core); + m_t->operator()(in, result, core); m_t->cleanup(); } @@ -1127,13 +978,12 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, 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, core); + m_t->operator()(in, result, core); } } @@ -1196,10 +1046,9 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { scope _scope(m_name); - m_t->operator()(in, result, mc, core); + m_t->operator()(in, result, core); } virtual tactic * translate(ast_manager & m) { @@ -1214,33 +1063,29 @@ tactic * annotate_tactic(char const* name, tactic * t) { } class cond_tactical : public binary_tactical { - probe * m_p; + probe_ref m_p; public: cond_tactical(probe * p, tactic * t1, tactic * t2): binary_tactical(t1, t2), m_p(p) { SASSERT(m_p); - m_p->inc_ref(); } - ~cond_tactical() { - m_p->dec_ref(); - } + virtual ~cond_tactical() {} virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { if (m_p->operator()(*(in.get())).is_true()) - m_t1->operator()(in, result, mc, core); + m_t1->operator()(in, result, core); else - m_t2->operator()(in, result, mc, core); + m_t2->operator()(in, result, core); } virtual tactic * translate(ast_manager & m) { tactic * new_t1 = m_t1->translate(m); tactic * new_t2 = m_t2->translate(m); - return alloc(cond_tactical, m_p, new_t1, new_t2); + return alloc(cond_tactical, m_p.get(), new_t1, new_t2); } }; @@ -1253,25 +1098,20 @@ tactic * when(probe * p, tactic * t) { } class fail_if_tactic : public tactic { - probe * m_p; + probe_ref m_p; public: fail_if_tactic(probe * p): m_p(p) { SASSERT(m_p); - m_p->inc_ref(); } - ~fail_if_tactic() { - m_p->dec_ref(); - } + virtual ~fail_if_tactic() {} void cleanup() {} virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - mc = 0; core = 0; if (m_p->operator()(*(in.get())).is_true()) { throw tactic_exception("fail-if tactic"); @@ -1298,15 +1138,14 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { if (in->proofs_enabled()) { - mc = 0; core = 0; + core = 0; result.reset(); result.push_back(in.get()); } else { - m_t->operator()(in, result, mc, core); + m_t->operator()(in, result, core); } } @@ -1319,15 +1158,14 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { if (in->unsat_core_enabled()) { - mc = 0; core = 0; + core = 0; result.reset(); result.push_back(in.get()); } else { - m_t->operator()(in, result, mc, core); + m_t->operator()(in, result, core); } } @@ -1340,15 +1178,14 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { if (in->models_enabled()) { - mc = 0; core = 0; + core = 0; result.reset(); result.push_back(in.get()); } else { - m_t->operator()(in, result, mc, core); + m_t->operator()(in, result, core); } } diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 71034b2b1..fb5c7d458 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -39,10 +39,9 @@ class macro_finder_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("macro-finder", *g); bool produce_proofs = g->proofs_enabled(); @@ -75,8 +74,7 @@ class macro_finder_tactic : public tactic { func_decl * f = mm.get_macro_interpretation(i, f_interp); evmc->add(f, f_interp); } - mc = evmc; - + g->add(evmc); g->inc_depth(); result.push_back(g.get()); TRACE("macro-finder", g->display(tout);); @@ -118,9 +116,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } virtual void cleanup() { diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index c8c1f2b0f..61dbcaf01 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -37,10 +37,9 @@ class quasi_macros_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("quasi-macros", *g); bool produce_proofs = g->proofs_enabled(); @@ -87,8 +86,7 @@ class quasi_macros_tactic : public tactic { func_decl * f = mm.get_macro_interpretation(i, f_interp); evmc->add(f, f_interp); } - mc = evmc; - + g->add(evmc); g->inc_depth(); result.push_back(g.get()); TRACE("quasi-macros", g->display(tout);); @@ -129,9 +127,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } virtual void cleanup() { diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index e4ba71ad7..6b9882e29 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -33,10 +33,9 @@ class ufbv_rewriter_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - mc = 0; core = 0; + core = 0; tactic_report report("ufbv-rewriter", *g); fail_if_unsat_core_generation("ufbv-rewriter", g); @@ -59,7 +58,8 @@ class ufbv_rewriter_tactic : public tactic { for (unsigned i = 0; i < new_forms.size(); i++) g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0); - mc = 0; // CMW: Remark: The demodulator could potentially remove all references to a variable. + // CMW: Remark: The demodulator could potentially + // remove all references to a variable. g->inc_depth(); result.push_back(g.get()); @@ -101,9 +101,8 @@ public: virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, core); + (*m_imp)(in, result, core); } virtual void cleanup() { diff --git a/src/test/horn_subsume_model_converter.cpp b/src/test/horn_subsume_model_converter.cpp index a361cfb2a..3e493d408 100644 --- a/src/test/horn_subsume_model_converter.cpp +++ b/src/test/horn_subsume_model_converter.cpp @@ -31,17 +31,17 @@ void tst_horn_subsume_model_converter() { mc->insert(p, m.mk_app(q, a.mk_numeral(rational(1), true), a.mk_numeral(rational(2), true))); model_converter_ref mcr = mc.get(); - apply(mcr, mr, 0); + apply(mcr, mr); model_smt2_pp(std::cout, m, *mr.get(), 0); mr = alloc(model, m); mc->insert(p, m.mk_app(q, a.mk_numeral(rational(3), true), a.mk_numeral(rational(5), true))); - apply(mcr, mr, 0); + apply(mcr, mr); model_smt2_pp(std::cout, m, *mr.get(), 0); mr = alloc(model, m); mc->insert(p, m.mk_app(r, m.mk_var(0,a.mk_int()), m.mk_var(1, a.mk_int()))); - apply(mcr, mr, 0); + apply(mcr, mr); model_smt2_pp(std::cout, m, *mr.get(), 0); mr = alloc(model, m); @@ -52,7 +52,7 @@ void tst_horn_subsume_model_converter() { body1 = m.mk_app(q, m.mk_var(1, a.mk_int()), m.mk_var(2, a.mk_int())); VERIFY(mc->mk_horn(head1, body1, pred, body2)); mc->insert(pred, body2); - apply(mcr, mr, 0); + apply(mcr, mr); model_smt2_pp(std::cout, m, *mr.get(), 0); mr = alloc(model, m); @@ -60,7 +60,7 @@ void tst_horn_subsume_model_converter() { body1 = m.mk_app(q, m.mk_var(1, a.mk_int()), m.mk_var(0, a.mk_int())); VERIFY(mc->mk_horn(head1, body1, pred, body2)); mc->insert(pred, body2); - apply(mcr, mr, 0); + apply(mcr, mr); model_smt2_pp(std::cout, m, *mr.get(), 0);