merge

Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>

src/CMakeLists.txt

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

src/ackermannization/ackermannize_bv_tactic.cpp

@@ -29,12 +29,7 @@ public:
 
     virtual ~ackermannize_bv_tactic() { }
 
-    virtual void operator()(goal_ref const & g,
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result) {
-        goal_ref_buffer & result,
-        model_converter_ref & mc,
-        proof_converter_ref & pc,
-        expr_dependency_ref & core) {
-        mc = 0;
         tactic_report report("ackermannize", *g);
         fail_if_unsat_core_generation("ackermannize", g);
         fail_if_proof_generation("ackermannize", g);
@@ -52,17 +47,14 @@ public:
             TRACE("ackermannize", tout << "ackermannize not run due to limit" << std::endl;);
             result.reset();
             result.push_back(g.get());
-            mc = 0;
-            pc = 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();
         TRACE("ackermannize", resg->display(tout << "out\n"););
         SASSERT(resg->is_well_sorted());

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);

src/api/api_opt.cpp

@@ -16,6 +16,9 @@ Revision History:
 
 --*/
 #include<iostream>
+#include "util/cancel_eh.h"
+#include "util/scoped_timer.h"
+#include "util/file_path.h"
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_stats.h"
@@ -24,11 +27,11 @@ Revision History:
 #include "api/api_model.h"
 #include "opt/opt_context.h"
 #include "opt/opt_cmds.h"
-#include "util/cancel_eh.h"
+#include "opt/opt_parse.h"
-#include "util/scoped_timer.h"
 #include "parsers/smt2/smt2parser.h"
 #include "api/api_ast_vector.h"
 
+
 extern "C" {
 
     struct Z3_optimize_ref : public api::object {
@@ -286,8 +289,19 @@ extern "C" {
     static void Z3_optimize_from_stream(
         Z3_context    c,
         Z3_optimize opt,
-        std::istream& s) {
+        std::istream& s, 
-        ast_manager& m = mk_c(c)->m();
+        char const* ext) {
+        ast_manager& m = mk_c(c)->m();        
+        if (ext && std::string("opb") == ext) {
+            unsigned_vector h;
+            parse_opb(*to_optimize_ptr(opt), s, h);
+            return;
+        }
+        if (ext && std::string("wcnf") == ext) {
+            unsigned_vector h;
+            parse_wcnf(*to_optimize_ptr(opt), s, h);
+            return;
+        }
         scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &m);
         install_opt_cmds(*ctx.get(), to_optimize_ptr(opt));
         ctx->set_ignore_check(true);
@@ -311,7 +325,7 @@ extern "C" {
         //LOG_Z3_optimize_from_string(c, d, s);
         std::string str(s);
         std::istringstream is(str);
-        Z3_optimize_from_stream(c, d, is);
+        Z3_optimize_from_stream(c, d, is, nullptr);
         Z3_CATCH;
     }
 
@@ -327,7 +341,7 @@ extern "C" {
             strm << "Could not open file " << s;
             throw default_exception(strm.str());
         }
-        Z3_optimize_from_stream(c, d, is);
+        Z3_optimize_from_stream(c, d, is, get_extension(s));
         Z3_CATCH;
     }
 

src/api/api_solver.cpp

@@ -29,12 +29,16 @@ Revision History:
 #include "util/scoped_ctrl_c.h"
 #include "util/cancel_eh.h"
 #include "util/scoped_timer.h"
+#include "util/file_path.h"
 #include "tactic/portfolio/smt_strategic_solver.h"
 #include "smt/smt_solver.h"
 #include "smt/smt_implied_equalities.h"
 #include "solver/smt_logics.h"
 #include "cmd_context/cmd_context.h"
 #include "parsers/smt2/smt2parser.h"
+#include "sat/dimacs.h"
+#include "sat/sat_solver.h"
+#include "sat/tactic/goal2sat.h"
 
 
 extern "C" {
@@ -127,13 +131,30 @@ extern "C" {
     void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name) {
         Z3_TRY;
         LOG_Z3_solver_from_file(c, s, file_name);
-        scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
+        char const* ext = get_extension(file_name);
-        ctx->set_ignore_check(true);
         std::ifstream is(file_name);
         if (!is) {
             SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR);
             return;
         }
+        if (ext && std::string("dimacs") == ext) {
+            ast_manager& m = to_solver_ref(s)->get_manager();
+            sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
+            parse_dimacs(is, solver);
+            sat2goal s2g;
+            model_converter_ref mc;
+            atom2bool_var a2b(m);
+            goal g(m);            
+            s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc);
+            for (unsigned i = 0; i < g.size(); ++i) {
+                to_solver_ref(s)->assert_expr(g.form(i));
+            }
+            return;
+        }
+
+        scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
+        ctx->set_ignore_check(true);
+
         if (!parse_smt2_commands(*ctx.get(), is)) {
             ctx = nullptr;
             SET_ERROR_CODE(Z3_PARSER_ERROR);

src/api/api_tactic.cpp

@@ -25,25 +25,25 @@ Revision History:
 #include "util/cancel_eh.h"
 #include "util/scoped_timer.h"
 
-Z3_apply_result_ref::Z3_apply_result_ref(api::context& c, ast_manager & m): api::object(c), m_core(m) {
+Z3_apply_result_ref::Z3_apply_result_ref(api::context& c, ast_manager & m): api::object(c) {
 }
 
 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_;                            \
+        _ref_->m_tactic   = _t_;                                \
-    mk_c(c)->save_object(_ref_);                        \
+        mk_c(c)->save_object(_ref_);                            \
-    Z3_tactic _result_  = of_tactic(_ref_);             \
+        Z3_tactic _result_  = of_tactic(_ref_);                 \
-    RETURN_Z3(_result_);                                \
+        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_;                     \
+        _ref_->m_probe   = _t_;                                 \
-    mk_c(c)->save_object(_ref_);                \
+        mk_c(c)->save_object(_ref_);                            \
-    Z3_probe _result_  = of_probe(_ref_);       \
+        Z3_probe _result_  = of_probe(_ref_);                   \
-    RETURN_Z3(_result_);                        \
+        RETURN_Z3(_result_);                                    \
 }
 
     Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name) {
@@ -418,7 +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_pc, ref->m_core);
+                exec(*to_tactic_ref(t), new_goal, ref->m_subgoals);
+                ref->m_pc = new_goal->pc();
+                ref->m_mc = new_goal->mc();
                 return of_apply_result(ref);
             }
             catch (z3_exception & ex) {
@@ -513,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);
-    }
-
 };

src/api/api_tactic.h

@@ -50,7 +50,6 @@ struct Z3_apply_result_ref : public api::object {
     goal_ref_buffer      m_subgoals;
     model_converter_ref  m_mc;
     proof_converter_ref  m_pc;
-    expr_dependency_ref  m_core;
     Z3_apply_result_ref(api::context& c, ast_manager & m);
     virtual ~Z3_apply_result_ref() {}
 };

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; }

src/api/dotnet/ApplyResult.cs

@@ -55,19 +55,6 @@ namespace Microsoft.Z3
             }
         }
 
-        /// <summary>
-        /// Convert a model for the subgoal <paramref name="i"/> into a model for the original 
-        /// goal <c>g</c>, that the ApplyResult was obtained from. 
-        /// </summary>
-        /// <returns>A model for <c>g</c></returns>
-        public Model ConvertModel(uint i, Model m)
-        {
-            Contract.Requires(m != null);
-            Contract.Ensures(Contract.Result<Model>() != null);
-
-            return new Model(Context, Native.Z3_apply_result_convert_model(Context.nCtx, NativeObject, i, m.NativeObject));
-        }
-
         /// <summary>
         /// A string representation of the ApplyResult.
         /// </summary>

src/api/dotnet/Goal.cs

@@ -174,6 +174,21 @@ namespace Microsoft.Z3
             get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
         }
 
+	/// <summary>
+	/// Convert a model for the goal into a model of the
+        /// original goal from which this goal was derived.
+        /// </summary>
+        /// <returns>A model for <c>g</c></returns>
+        public Model ConvertModel(Model m)
+        {
+            Contract.Ensures(Contract.Result<Model>() != 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));
+        }
+
+
         /// <summary>
         /// Translates (copies) the Goal to the target Context <paramref name="ctx"/>.
         /// </summary>

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.
      **/

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());

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)

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*/

src/cmd_context/echo_tactic.cpp

@@ -28,17 +28,14 @@ public:
     echo_tactic(cmd_context & ctx, char const * msg, bool newline):m_ctx(ctx), m_msg(msg), m_newline(newline) {}
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         #pragma omp critical (echo_tactic)
         {
             m_ctx.regular_stream() << m_msg;
             if (m_newline)
                 m_ctx.regular_stream() << std::endl;
         }
-        skip_tactic::operator()(in, result, mc, pc, core);
+        skip_tactic::operator()(in, result);
     }
 };
 
@@ -62,10 +59,7 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         double val = (*m_p)(*(in.get())).get_value();
         #pragma omp critical (probe_value_tactic)
         {
@@ -75,7 +69,7 @@ public:
             if (m_newline)
                 m_ctx.diagnostic_stream() << std::endl;
         }
-        skip_tactic::operator()(in, result, mc, pc, core);
+        skip_tactic::operator()(in, result);
     }
 };
 

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,9 +326,6 @@ public:
             unsigned rlimit  =   p.get_uint("rlimit", ctx.params().m_rlimit);
 
             goal_ref_buffer     result_goals;
-            model_converter_ref mc;
-            proof_converter_ref pc;
-            expr_dependency_ref core(m);
 
             std::string reason_unknown;
             bool failed = false;
@@ -340,7 +336,7 @@ public:
                 scoped_timer timer(timeout, &eh);
                 cmd_context::scoped_watch sw(ctx);
                 try {
-                    exec(t, g, result_goals, mc, pc, core);
+                    exec(t, g, result_goals);
                 }
                 catch (tactic_exception & ex) {
                     ctx.regular_stream() << "(error \"tactic failed: " << ex.msg() << "\")" << std::endl;
@@ -399,8 +395,8 @@ public:
                 }
             }
 
-            if (!failed && mc && p.get_bool("print_model_converter", false))
+            if (!failed && g->mc() && p.get_bool("print_model_converter", false))
-                mc->display(ctx.regular_stream());
+                g->mc()->display(ctx.regular_stream());
 
             if (p.get_bool("print_statistics", false))
                 display_statistics(ctx, tref.get());

src/math/subpaving/tactic/subpaving_tactic.cpp

@@ -242,18 +242,12 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         try {
             m_imp->process(*in);
             m_imp->collect_statistics(m_stats);
             result.reset();
             result.push_back(in.get());
-            mc   = 0;
-            pc   = 0;
-            core = 0;
         }
         catch (z3_exception & ex) {
             // convert all Z3 exceptions into tactic exceptions

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); }

src/muz/fp/horn_tactic.cpp

@@ -177,12 +177,8 @@ class horn_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("horn", *g);
             bool produce_proofs = g->proofs_enabled();
 
@@ -231,16 +227,20 @@ 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);
             }
             else {
                 verify(q, g, result, mc, pc);
             }
+            g->set(pc.get());
+            g->set(mc.get());
         }
 
         void verify(expr* q, 
@@ -384,11 +384,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
     }
     
     virtual void collect_statistics(statistics & st) const {

src/muz/pdr/pdr_context.cpp

@@ -202,11 +202,8 @@ 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;
-        proof_converter_ref pc;
-        expr_dependency_ref core(m);
         goal_ref_buffer result;
-        tac(g, result, mc, pc, core);
+        tac(g, result);
         SASSERT(result.size() == 1);
         goal* r = result[0];
         v.reset();
@@ -391,7 +388,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);
         }

src/muz/pdr/pdr_farkas_learner.cpp

@@ -520,12 +520,9 @@ namespace pdr {
             g->assert_expr(lemmas[i].get()); 
         }
         expr_ref tmp(m);
-        model_converter_ref mc;
-        proof_converter_ref pc;
-        expr_dependency_ref core(m);
         goal_ref_buffer result;
         tactic_ref simplifier = mk_arith_bounds_tactic(m);
-        (*simplifier)(g, result, mc, pc, core);
+        (*simplifier)(g, result);
         lemmas.reset();
         SASSERT(result.size() == 1);
         goal* r = result[0];

src/muz/pdr/pdr_manager.cpp

@@ -107,7 +107,7 @@ namespace pdr {
             }
         }
         TRACE("pdr", model_smt2_pp(tout, m, *md, 0););
-        apply(const_cast<model_converter_ref&>(m_mc), md, 0);
+        apply(const_cast<model_converter_ref&>(m_mc), md);
     }
 
     expr_ref inductive_property::to_expr() const {

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,9 +1367,6 @@ void pred_transformer::frames::simplify_formulas ()
         // normalize level
         unsigned level = i < m_size ? i : infty_level ();
 
-        model_converter_ref mc;
-        proof_converter_ref pc;
-        expr_dependency_ref core(m);
         goal_ref_buffer result;
 
         // simplify lemmas of the current level
@@ -1395,7 +1392,7 @@ void pred_transformer::frames::simplify_formulas ()
         }
 
         // more than one lemma at current level. simplify.
-        (*simplifier)(g, result, mc, pc, core);
+        (*simplifier)(g, result);
         SASSERT(result.size () == 1);
         goal *r = result[0];
 
@@ -2063,8 +2060,8 @@ bool context::validate()
         expr_ref_vector refs(m);
         expr_ref tmp(m);
         model_ref model;
-        vector<relation_info> rs;
         model_converter_ref mc;
+        vector<relation_info> rs;
         get_level_property(m_inductive_lvl, refs, rs);
         inductive_property ex(m, mc, rs);
         ex.to_model(model);

src/muz/spacer/spacer_legacy_frames.cpp

@@ -46,11 +46,8 @@ 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;
-    proof_converter_ref pc;
-    expr_dependency_ref core(m);
     goal_ref_buffer result;
-    tac(g, result, mc, pc, core);
+    tac(g, result);
     SASSERT(result.size() == 1);
     goal* r = result[0];
     v.reset();

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<model_converter_ref&>(m_mc), md, 0);
+    apply(const_cast<model_converter_ref&>(m_mc), md);
 }
 
 expr_ref inductive_property::to_expr() const

src/muz/spacer/spacer_util.cpp

@@ -929,12 +929,9 @@ void simplify_bounds_old(expr_ref_vector& cube) {
     }
 
     expr_ref tmp(m);
-    model_converter_ref mc;
-    proof_converter_ref pc;
-    expr_dependency_ref core(m);
     goal_ref_buffer result;
     tactic_ref simplifier = mk_arith_bounds_tactic(m);
-    (*simplifier)(g, result, mc, pc, core);
+    (*simplifier)(g, result);
     SASSERT(result.size() == 1);
     goal* r = result[0];
 
@@ -955,15 +952,12 @@ void simplify_bounds_new (expr_ref_vector &cube) {
         g->assert_expr(cube.get(i));
     }
 
-    model_converter_ref mc;
-    proof_converter_ref pc;
-    expr_dependency_ref dep(m);
     goal_ref_buffer goals;
     tactic_ref prop_values = mk_propagate_values_tactic(m);
     tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m);
     tactic_ref t = and_then(prop_values.get(), prop_bounds.get());
 
-    (*t)(g, goals, mc, pc, dep);
+    (*t)(g, goals);
     SASSERT(goals.size() == 1);
 
     g = goals[0];

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;
         }
 

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"; }
 
     };
    

src/nlsat/tactic/nlsat_tactic.cpp

@@ -129,12 +129,8 @@ class nlsat_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("nlsat", *g);
             
             if (g->is_decided()) {
@@ -166,9 +162,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());
                     }
                 }
             }
@@ -177,8 +175,8 @@ class nlsat_tactic : public tactic {
                 if (g->unsat_core_enabled()) {
                     vector<nlsat::assumption, false> assumptions;
                     m_solver.get_core(assumptions);
-                    for (unsigned i = 0; i < assumptions.size(); ++i) {
+                    for (nlsat::assumption a : assumptions) {
-                        expr_dependency* d = static_cast<expr_dependency*>(assumptions[i]);
+                        expr_dependency* d = static_cast<expr_dependency*>(a);
                         lcore = m.mk_join(lcore, d);
                     }
                 }
@@ -233,14 +231,11 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         try {
             imp local_imp(in->m(), m_params);
             scoped_set_imp setter(*this, local_imp);
-            local_imp(in, result, mc, pc, core);
+            local_imp(in, result);
         }
         catch (z3_error & ex) {
             throw ex;

src/opt/CMakeLists.txt

@@ -6,6 +6,7 @@ z3_add_component(opt
     opt_cmds.cpp
     opt_context.cpp
     opt_pareto.cpp
+    opt_parse.cpp
     optsmt.cpp
     opt_solver.cpp
     pb_sls.cpp

src/opt/opt_context.cpp

@@ -324,10 +324,8 @@ namespace opt {
 
     void context::fix_model(model_ref& mdl) {
         if (mdl) {
-            if (m_model_converter) {
+            apply(m_model_converter, mdl);
-                (*m_model_converter)(mdl, 0);
+            m_fm(mdl);
-            }
-            m_fm(mdl, 0);
         }
     }
 
@@ -747,12 +745,11 @@ namespace opt {
         else {
             set_simplify(tac0.get());
         }
-        proof_converter_ref pc;
-        expr_dependency_ref core(m);
         goal_ref_buffer result;
-        (*m_simplify)(g, result, m_model_converter, pc, core); 
+        (*m_simplify)(g, result); 
         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) {

src/opt/opt_parse.cpp

@@ -0,0 +1,317 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    opt_parse.cpp
+
+Abstract:
+
+    Parse utilities for optimization.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-11-19
+
+Revision History:
+
+--*/
+#include "opt/opt_context.h"
+#include "opt/opt_parse.h"
+
+
+class opt_stream_buffer {
+    std::istream & m_stream;
+    int            m_val;
+    unsigned       m_line;
+public:    
+    opt_stream_buffer(std::istream & s):
+        m_stream(s),
+        m_line(0) {
+        m_val = m_stream.get();
+    }
+    int  operator *() const { return m_val;}
+    void operator ++() { m_val = m_stream.get(); }
+    int ch() const { return m_val; }
+    void next() { m_val = m_stream.get(); }
+    bool eof() const { return ch() == EOF; }
+    unsigned line() const { return m_line; }
+    void skip_whitespace();
+    void skip_space();
+    void skip_line();
+    bool parse_token(char const* token);
+    int parse_int();
+    unsigned parse_unsigned();
+};
+
+
+void opt_stream_buffer::skip_whitespace() {
+    while ((ch() >= 9 && ch() <= 13) || ch() == 32) {
+        if (ch() == 10) ++m_line;
+        next(); 
+    }
+}
+
+void opt_stream_buffer::skip_space() {
+    while (ch() != 10 && ((ch() >= 9 && ch() <= 13) || ch() == 32)) {
+        next(); 
+    }
+}
+void opt_stream_buffer::skip_line() {
+    while(true) {
+        if (eof()) {
+            return;
+        }
+        if (ch() == '\n') { 
+            ++m_line;
+            next();
+            return; 
+        }
+        next();
+    } 
+}
+
+bool opt_stream_buffer::parse_token(char const* token) {
+    skip_whitespace();
+    char const* t = token;
+    while (ch() == *t) {
+        next();
+        ++t;
+    }
+    return 0 == *t;
+}
+
+unsigned opt_stream_buffer::parse_unsigned() {
+    skip_space();
+    if (ch() == '\n') {
+        return UINT_MAX;
+    }
+    unsigned val = 0;
+    while (ch() >= '0' && ch() <= '9') {
+        val = val*10 + (ch() - '0');
+        next();
+    }
+    return val;
+}
+
+int opt_stream_buffer::parse_int() {
+    int     val = 0;
+    bool    neg = false;
+    skip_whitespace();
+    
+    if (ch() == '-') {
+        neg = true;
+        next();
+    }
+    else if (ch() == '+') {
+        next();
+    }        
+    if (ch() < '0' || ch() > '9') {
+        std::cerr << "(error line " << line() << " \"unexpected char: " << ((char)ch()) << "\" )\n";
+        exit(3);
+    }        
+    while (ch() >= '0' && ch() <= '9') {
+        val = val*10 + (ch() - '0');
+        next();
+    }
+    return neg ? -val : val; 
+}
+
+
+class wcnf {
+    opt::context&  opt;
+    ast_manager&   m;
+    opt_stream_buffer& in;
+    unsigned_vector& m_handles;
+
+    app_ref read_clause(unsigned& weight) {
+        int     parsed_lit;
+        int     var;    
+        weight = in.parse_unsigned();
+        app_ref result(m), p(m);
+        expr_ref_vector ors(m);
+        while (true) { 
+            parsed_lit = in.parse_int();
+            if (parsed_lit == 0)
+                break;
+            var = abs(parsed_lit);
+            p = m.mk_const(symbol(var), m.mk_bool_sort());
+            if (parsed_lit < 0) p = m.mk_not(p);
+            ors.push_back(p);
+        }
+        result = to_app(mk_or(m, ors.size(), ors.c_ptr()));
+        return result;
+    }
+    
+    void parse_spec(unsigned& num_vars, unsigned& num_clauses, unsigned& max_weight) {
+        in.parse_token("wcnf");
+        num_vars = in.parse_unsigned();
+        num_clauses = in.parse_unsigned();
+        max_weight = in.parse_unsigned();
+    }
+
+public:
+    
+    wcnf(opt::context& opt, opt_stream_buffer& in, unsigned_vector& h): opt(opt), m(opt.get_manager()), in(in), m_handles(h) {
+        opt.set_clausal(true);
+    }
+    
+    void parse() {
+        unsigned num_vars = 0, num_clauses = 0, max_weight = 0;
+        while (true) {
+            in.skip_whitespace();
+            if (in.eof()) {
+                break;
+            }
+            else if (*in == 'c') {
+                in.skip_line();
+            }
+            else if (*in == 'p') {
+                ++in;
+                parse_spec(num_vars, num_clauses, max_weight);
+            }
+            else {
+                unsigned weight = 0;
+                app_ref cls = read_clause(weight);
+                if (weight >= max_weight) {
+                    opt.add_hard_constraint(cls);
+                }
+                else {
+                    unsigned id = opt.add_soft_constraint(cls, rational(weight), symbol::null);
+                    if (m_handles.empty()) {
+                        m_handles.push_back(id);
+                    }
+                }
+            }
+        }
+    }    
+};
+
+
+class opb {
+    opt::context&  opt;
+    ast_manager&   m;    
+    opt_stream_buffer& in;
+    unsigned_vector& m_handles;
+    arith_util     arith;
+
+    app_ref parse_id() {
+        bool negated = in.parse_token("~");
+        if (!in.parse_token("x")) {
+            std::cerr << "(error line " << in.line() << " \"unexpected char: " << ((char)in.ch()) << "\" expected \"x\")\n";
+            exit(3);
+        }
+        app_ref p(m);
+        int id = in.parse_int();
+        p = m.mk_const(symbol(id), m.mk_bool_sort());
+        if (negated) p = m.mk_not(p);
+        in.skip_whitespace();
+        return p;
+    }
+
+    app_ref parse_ids() {
+        app_ref result = parse_id();
+        while (*in == '~' || *in == 'x') {            
+            result = m.mk_and(result, parse_id());
+        }
+        return result;
+    }
+
+    rational parse_coeff_r() {
+        in.skip_whitespace();
+        svector<char> num;
+        bool pos = true;
+        if (*in == '-') pos = false, ++in;
+        if (*in == '+') ++in;
+        if (!pos) num.push_back('-');
+        in.skip_whitespace();
+        while ('0' <= *in && *in <='9') num.push_back(*in), ++in;
+        num.push_back(0);
+        return rational(num.c_ptr());
+    }
+
+    app_ref parse_coeff() {
+        return app_ref(arith.mk_numeral(parse_coeff_r(), true), m);
+    }
+    
+    app_ref parse_term() {        
+        app_ref c = parse_coeff();
+        app_ref e = parse_ids();
+        return app_ref(m.mk_ite(e, c, arith.mk_numeral(rational(0), true)), m);
+    }
+
+    void parse_objective(bool is_min) {
+        app_ref t = parse_term();
+        while (!in.parse_token(";") && !in.eof()) {
+            if (is_min) {
+                t = arith.mk_add(t, parse_term());
+            }
+            else {
+                t = arith.mk_sub(t, parse_term());
+            }
+        }
+        m_handles.push_back(opt.add_objective(t, false));
+    }
+
+    void parse_constraint() {
+        app_ref t = parse_term();
+        while (!in.eof()) {
+            if (in.parse_token(">=")) {    
+                t = arith.mk_ge(t, parse_coeff());
+                in.parse_token(";");
+                break;
+            }
+            if (in.parse_token("=")) {
+                t = m.mk_eq(t, parse_coeff());
+                in.parse_token(";");
+                break;
+            }            
+            if (in.parse_token("<=")) {
+                t = arith.mk_le(t, parse_coeff());
+                in.parse_token(";");
+                break;
+            }            
+            t = arith.mk_add(t, parse_term());
+        }        
+        opt.add_hard_constraint(t);
+    }
+public:
+    opb(opt::context& opt, opt_stream_buffer& in, unsigned_vector& h): 
+        opt(opt), m(opt.get_manager()), 
+        in(in), m_handles(h), arith(m) {}
+
+    void parse() {
+        while (true) {
+            in.skip_whitespace();
+            if (in.eof()) {
+                break;
+            }
+            else if (*in == '*') {
+                in.skip_line();
+            }
+            else if (in.parse_token("min:")) {
+                parse_objective(true);
+            }
+            else if (in.parse_token("max:")) {
+                parse_objective(false);
+            }
+            else {
+                parse_constraint();
+            }
+        }
+    }
+};
+
+void parse_wcnf(opt::context& opt, std::istream& is, unsigned_vector& h) {
+    opt_stream_buffer _is(is);
+    wcnf w(opt, _is, h);
+    w.parse();
+}
+
+void parse_opb(opt::context& opt, std::istream& is, unsigned_vector& h) {
+    opt_stream_buffer _is(is);
+    opb opb(opt, _is, h);
+    opb.parse();
+}
+
+

src/opt/opt_parse.h

@@ -0,0 +1,28 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    opt_parse.h
+
+Abstract:
+
+    Parse utilities for optimization.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-11-19
+
+Revision History:
+
+--*/
+#ifndef OPT_PARSE_H_
+#define OPT_PARSE_H_
+
+void parse_wcnf(opt::context& opt, std::istream& is, unsigned_vector& h);
+
+void parse_opb(opt::context& opt, std::istream& is, unsigned_vector& h);
+
+#endif /* OPT_PARSE_H_ */
+
+

src/qe/nlqsat.cpp

@@ -658,11 +658,9 @@ namespace qe {
             fml = m.mk_iff(is_true, fml);
             goal_ref g = alloc(goal, m);
             g->assert_expr(fml);
-            proof_converter_ref pc;
             expr_dependency_ref core(m);
-            model_converter_ref mc;
             goal_ref_buffer result;
-            (*m_nftactic)(g, result, mc, pc, core);
+            (*m_nftactic)(g, result);
             SASSERT(result.size() == 1);
             TRACE("qe", result[0]->display(tout););
             g2s(*result[0], m_params, m_solver, m_a2b, m_t2x);
@@ -812,16 +810,12 @@ namespace qe {
 
         
         void operator()(/* in */  goal_ref const & in, 
-                        /* out */ goal_ref_buffer & result, 
+                        /* out */ goal_ref_buffer & result) {
-                        /* out */ model_converter_ref & mc, 
-                        /* out */ proof_converter_ref & pc,
-                        /* out */ expr_dependency_ref & core) {
 
             tactic_report report("nlqsat-tactic", *in);
 
             ptr_vector<expr> fmls;
             expr_ref fml(m);
-            mc = 0; pc = 0; core = 0;
             in->get_formulas(fmls);
             fml = mk_and(m, fmls.size(), fmls.c_ptr());
             if (m_mode == elim_t) {
@@ -852,7 +846,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:

src/qe/qe_lite.cpp

@@ -2532,12 +2532,8 @@ class qe_lite_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g,
-                        goal_ref_buffer & result,
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc,
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("qe-lite", *g);
             proof_ref new_pr(m);
             expr_ref new_f(m);
@@ -2603,11 +2599,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc,
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
     }
 
 

src/qe/qe_sat_tactic.cpp

@@ -233,10 +233,7 @@ namespace qe {
 
         virtual void operator()(
             goal_ref const& goal,  
-            goal_ref_buffer& result, 
+            goal_ref_buffer& result) 
-            model_converter_ref& mc, 
-            proof_converter_ref & pc, 
-            expr_dependency_ref& core) 
         {
             try {
                 checkpoint();
@@ -260,7 +257,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());
             }
@@ -270,16 +267,16 @@ namespace qe {
         }
 
         virtual void collect_statistics(statistics & st) const {
-            for (unsigned i = 0; i < m_solvers.size(); ++i) {
+            for (auto const * s : m_solvers) {
-                m_solvers[i]->collect_statistics(st);
+                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) {
+            for (auto * s : m_solvers) {
-                m_solvers[i]->reset_statistics();
+                s->reset_statistics();
             }            
             m_solver.reset_statistics();
             m_ctx_rewriter.reset_statistics();

src/qe/qe_tactic.cpp

@@ -50,12 +50,8 @@ class qe_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("qe", *g);
             m_fparams.m_model = g->models_enabled();
             proof_ref new_pr(m);
@@ -121,11 +117,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
         m_st.reset();
         m_imp->collect_statistics(m_st);
         

src/qe/qsat.cpp

@@ -1211,18 +1211,12 @@ namespace qe {
 
         
         void operator()(/* in */  goal_ref const & in, 
-                        /* out */ goal_ref_buffer & result, 
+                        /* out */ goal_ref_buffer & result) {
-                        /* out */ model_converter_ref & mc, 
-                        /* out */ proof_converter_ref & pc,
-                        /* out */ expr_dependency_ref & core) {
             tactic_report report("qsat-tactic", *in);
             ptr_vector<expr> fmls;
             expr_ref_vector defs(m);
             expr_ref fml(m);
-            mc = 0; pc = 0; core = 0;
             in->get_formulas(fmls);
-
-
             fml = mk_and(m, fmls.size(), fmls.c_ptr());
             
             // for now:
@@ -1272,8 +1266,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:

src/sat/sat_solver/inc_sat_solver.cpp

@@ -61,7 +61,6 @@ class inc_sat_solver : public solver {
     model_converter_ref m_mc;
     model_converter_ref m_mc0;
     model_converter_ref m_sat_mc;
-    expr_dependency_ref m_dep_core;
     svector<double>     m_weights;
     std::string         m_unknown;
     // access formulas after they have been pre-processed and handled by the sat solver.
@@ -82,7 +81,6 @@ public:
         m_core(m),
         m_map(m),
         m_num_scopes(0),
-        m_dep_core(m),
         m_unknown("no reason given"),
         m_internalized(false), 
         m_internalized_converted(false), 
@@ -495,7 +493,6 @@ private:
     lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
         m_mc.reset();
         m_pc.reset();
-        m_dep_core.reset();
         m_subgoals.reset();
         init_preprocess();
         SASSERT(g->models_enabled());
@@ -505,7 +502,7 @@ private:
         SASSERT(!g->proofs_enabled());
         TRACE("sat", g->display(tout););
         try {
-            (*m_preprocess)(g, m_subgoals, m_mc, m_pc, m_dep_core);
+            (*m_preprocess)(g, m_subgoals);
         }
         catch (tactic_exception & ex) {
             IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
@@ -520,6 +517,8 @@ 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);

src/sat/tactic/goal2sat.cpp

@@ -922,8 +922,7 @@ struct sat2goal::imp {
             }
         }
         
-        virtual void operator()(model_ref & md, unsigned goal_idx) {
+        virtual void operator()(model_ref & md) {
-            SASSERT(goal_idx == 0);
             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,

src/sat/tactic/sat_tactic.cpp

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

src/shell/main.cpp

@@ -33,6 +33,7 @@ Revision History:
 #include "util/timeout.h"
 #include "util/z3_exception.h"
 #include "util/error_codes.h"
+#include "util/file_path.h"
 #include "util/gparams.h"
 #include "util/env_params.h"
 #include "shell/lp_frontend.h"
@@ -289,19 +290,6 @@ void parse_cmd_line_args(int argc, char ** argv) {
     }
 }
 
-char const * get_extension(char const * file_name) {
-    if (file_name == 0)
-        return 0;
-    char const * last_dot = 0;
-    for (;;) {
-        char const * tmp = strchr(file_name, '.');
-        if (tmp == 0) {
-            return last_dot;
-        }
-        last_dot  = tmp + 1;
-        file_name = last_dot;
-    }
-}
 
 int STD_CALL main(int argc, char ** argv) {
     try{

src/shell/opt_frontend.cpp

@@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/gparams.h"
 #include "util/timeout.h"
 #include "ast/reg_decl_plugins.h"
+#include "opt/opt_parse.h"
 
 extern bool g_display_statistics;
 static bool g_first_interrupt = true;
@@ -20,275 +21,6 @@ static opt::context* g_opt = 0;
 static double g_start_time = 0;
 static unsigned_vector g_handles;
 
-class opt_stream_buffer {
-    std::istream & m_stream;
-    int            m_val;
-    unsigned       m_line;
-public:    
-    opt_stream_buffer(std::istream & s):
-        m_stream(s),
-        m_line(0) {
-        m_val = m_stream.get();
-    }
-    int  operator *() const { return m_val;}
-    void operator ++() { m_val = m_stream.get(); }
-    int ch() const { return m_val; }
-    void next() { m_val = m_stream.get(); }
-    bool eof() const { return ch() == EOF; }
-    unsigned line() const { return m_line; }
-    void skip_whitespace() {
-        while ((ch() >= 9 && ch() <= 13) || ch() == 32) {
-            if (ch() == 10) ++m_line;
-            next(); 
-        }
-    }
-    void skip_space() {
-        while (ch() != 10 && ((ch() >= 9 && ch() <= 13) || ch() == 32)) {
-            next(); 
-        }
-    }
-    void skip_line() {
-        while(true) {
-            if (eof()) {
-                return;
-            }
-            if (ch() == '\n') { 
-                ++m_line;
-                next();
-                return; 
-            }
-            next();
-        } 
-    }
-
-    bool parse_token(char const* token) {
-        skip_whitespace();
-        char const* t = token;
-        while (ch() == *t) {
-            next();
-            ++t;
-        }
-        return 0 == *t;
-   }
-
-    int parse_int() {
-        int     val = 0;
-        bool    neg = false;
-        skip_whitespace();
-        
-        if (ch() == '-') {
-            neg = true;
-            next();
-        }
-        else if (ch() == '+') {
-            next();
-        }        
-        if (ch() < '0' || ch() > '9') {
-            std::cerr << "(error line " << line() << " \"unexpected char: " << ((char)ch()) << "\" )\n";
-            exit(3);
-        }        
-        while (ch() >= '0' && ch() <= '9') {
-            val = val*10 + (ch() - '0');
-            next();
-        }
-        return neg ? -val : val; 
-    }
-
-    unsigned parse_unsigned() {
-        skip_space();
-        if (ch() == '\n') {
-            return UINT_MAX;
-        }
-        unsigned val = 0;
-        while (ch() >= '0' && ch() <= '9') {
-            val = val*10 + (ch() - '0');
-            next();
-        }
-        return val;
-    }
-};
-
-class wcnf {
-    opt::context&  opt;
-    ast_manager&   m;
-    opt_stream_buffer& in;
-
-    app_ref read_clause(unsigned& weight) {
-        int     parsed_lit;
-        int     var;    
-        weight = in.parse_unsigned();
-        app_ref result(m), p(m);
-        expr_ref_vector ors(m);
-        while (true) { 
-            parsed_lit = in.parse_int();
-            if (parsed_lit == 0)
-                break;
-            var = abs(parsed_lit);
-            p = m.mk_const(symbol(var), m.mk_bool_sort());
-            if (parsed_lit < 0) p = m.mk_not(p);
-            ors.push_back(p);
-        }
-        result = to_app(mk_or(m, ors.size(), ors.c_ptr()));
-        return result;
-    }
-    
-    void parse_spec(unsigned& num_vars, unsigned& num_clauses, unsigned& max_weight) {
-        in.parse_token("wcnf");
-        num_vars = in.parse_unsigned();
-        num_clauses = in.parse_unsigned();
-        max_weight = in.parse_unsigned();
-    }
-
-public:
-    
-    wcnf(opt::context& opt, opt_stream_buffer& in): opt(opt), m(opt.get_manager()), in(in) {
-        opt.set_clausal(true);
-    }
-    
-    void parse() {
-        unsigned num_vars = 0, num_clauses = 0, max_weight = 0;
-        while (true) {
-            in.skip_whitespace();
-            if (in.eof()) {
-                break;
-            }
-            else if (*in == 'c') {
-                in.skip_line();
-            }
-            else if (*in == 'p') {
-                ++in;
-                parse_spec(num_vars, num_clauses, max_weight);
-            }
-            else {
-                unsigned weight = 0;
-                app_ref cls = read_clause(weight);
-                if (weight >= max_weight) {
-                    opt.add_hard_constraint(cls);
-                }
-                else {
-                    unsigned id = opt.add_soft_constraint(cls, rational(weight), symbol::null);
-                    if (g_handles.empty()) {
-                        g_handles.push_back(id);
-                    }
-                }
-            }
-        }
-    }    
-};
-
-
-class opb {
-    opt::context&  opt;
-    ast_manager&   m;
-    opt_stream_buffer& in;
-    arith_util     arith;
-
-    app_ref parse_id() {
-        bool negated = in.parse_token("~");
-        if (!in.parse_token("x")) {
-            std::cerr << "(error line " << in.line() << " \"unexpected char: " << ((char)in.ch()) << "\" expected \"x\")\n";
-            exit(3);
-        }
-        app_ref p(m);
-        int id = in.parse_int();
-        p = m.mk_const(symbol(id), m.mk_bool_sort());
-        if (negated) p = m.mk_not(p);
-        in.skip_whitespace();
-        return p;
-    }
-
-    app_ref parse_ids() {
-        app_ref result = parse_id();
-        while (*in == '~' || *in == 'x') {            
-            result = m.mk_and(result, parse_id());
-        }
-        return result;
-    }
-
-    rational parse_coeff_r() {
-        in.skip_whitespace();
-        svector<char> num;
-        bool pos = true;
-        if (*in == '-') pos = false, ++in;
-        if (*in == '+') ++in;
-        if (!pos) num.push_back('-');
-        in.skip_whitespace();
-        while ('0' <= *in && *in <='9') num.push_back(*in), ++in;
-        num.push_back(0);
-        return rational(num.c_ptr());
-    }
-
-    app_ref parse_coeff() {
-        return app_ref(arith.mk_numeral(parse_coeff_r(), true), m);
-    }
-    
-    app_ref parse_term() {        
-        app_ref c = parse_coeff();
-        app_ref e = parse_ids();
-        return app_ref(m.mk_ite(e, c, arith.mk_numeral(rational(0), true)), m);
-    }
-
-    void parse_objective(bool is_min) {
-        app_ref t = parse_term();
-        while (!in.parse_token(";") && !in.eof()) {
-            if (is_min) {
-                t = arith.mk_add(t, parse_term());
-            }
-            else {
-                t = arith.mk_sub(t, parse_term());
-            }
-        }
-        g_handles.push_back(opt.add_objective(t, false));
-    }
-
-    void parse_constraint() {
-        app_ref t = parse_term();
-        while (!in.eof()) {
-            if (in.parse_token(">=")) {    
-                t = arith.mk_ge(t, parse_coeff());
-                in.parse_token(";");
-                break;
-            }
-            if (in.parse_token("=")) {
-                t = m.mk_eq(t, parse_coeff());
-                in.parse_token(";");
-                break;
-            }            
-            if (in.parse_token("<=")) {
-                t = arith.mk_le(t, parse_coeff());
-                in.parse_token(";");
-                break;
-            }            
-            t = arith.mk_add(t, parse_term());
-        }        
-        opt.add_hard_constraint(t);
-    }
-public:
-    opb(opt::context& opt, opt_stream_buffer& in): 
-        opt(opt), m(opt.get_manager()), 
-        in(in), arith(m) {}
-
-    void parse() {
-        while (true) {
-            in.skip_whitespace();
-            if (in.eof()) {
-                break;
-            }
-            else if (*in == '*') {
-                in.skip_line();
-            }
-            else if (in.parse_token("min:")) {
-                parse_objective(true);
-            }
-            else if (in.parse_token("max:")) {
-                parse_objective(false);
-            }
-            else {
-                parse_constraint();
-            }
-        }
-    }
-};
 
 
 static void display_results() {
@@ -348,14 +80,11 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) {
     g_opt = &opt;
     params_ref p = gparams::get_module("opt");
     opt.updt_params(p);
-    opt_stream_buffer _in(in);
     if (is_wcnf) {
-        wcnf wcnf(opt, _in);
+        parse_wcnf(opt, in, g_handles);
-        wcnf.parse();
     }
     else {
-        opb opb(opt, _in);
+        parse_opb(opt, in, g_handles);
-        opb.parse();
     }
     try {
         lbool r = opt.optimize();

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);
         }

src/smt/tactic/ctx_solver_simplify_tactic.cpp

@@ -70,12 +70,8 @@ public:
     virtual void reset_statistics() { m_num_steps = 0; }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         
-        mc = 0; pc = 0; core = 0;
         reduce(*(in.get()));
         in->inc_depth();
         result.push_back(in.get());

src/smt/tactic/smt_tactic.cpp

@@ -145,13 +145,9 @@ public:
 
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc,
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         try {
             IF_VERBOSE(10, verbose_stream() << "(smt.tactic start)\n";);
-            mc = 0; pc = 0; core = 0;
             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 << " "
@@ -221,8 +217,10 @@ public:
                     m_ctx->get_model(md);
                     buffer<symbol> 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;
             }
@@ -270,7 +268,7 @@ public:
                             m_ctx->get_model(md);
                             buffer<symbol> 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:

src/smt/tactic/unit_subsumption_tactic.cpp

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

src/solver/solver2tactic.cpp

@@ -102,11 +102,7 @@ public:
     }
 
     virtual void operator()(/* in */  goal_ref const & in, 
-                            /* out */ goal_ref_buffer & result, 
+                            /* out */ goal_ref_buffer & result) {
-                            /* out */ model_converter_ref & mc, 
-                            /* out */ proof_converter_ref & pc,
-                            /* out */ expr_dependency_ref & core) {
-        pc = 0; mc = 0; core = 0;
         expr_ref_vector clauses(m);
         expr2expr_map               bool2dep;
         ptr_vector<expr>            assumptions;
@@ -120,9 +116,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());
@@ -130,30 +128,32 @@ public:
         case l_false: {
             in->reset();
             proof* pr = 0;
-            expr_dependency* lcore = 0;
+            expr_dependency_ref lcore(m);
             if (in->proofs_enabled()) {
                 pr = local_solver->get_proof();
-                pc = proof2proof_converter(m, pr);
+                in->set(proof2proof_converter(m, pr));
             }
             if (in->unsat_core_enabled()) {
                 ptr_vector<expr> core;
                 local_solver->get_unsat_core(core);
-                for (unsigned i = 0; i < core.size(); ++i) {
+                for (expr* c : core) {
-                    lcore = m.mk_join(lcore, m.mk_leaf(bool2dep.find(core[i])));
+                    lcore = m.mk_join(lcore, m.mk_leaf(bool2dep.find(c)));
                 }
             }
             in->assert_expr(m.mk_false(), pr, lcore);
             result.push_back(in.get());
-            core = lcore;
+            in->set(dependency_converter::unit(lcore));
             break;
         }
         case l_undef:
             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));

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";);

src/tactic/CMakeLists.txt

@@ -1,5 +1,6 @@
 z3_add_component(tactic
   SOURCES
+    dependency_converter.cpp
     equiv_proof_converter.cpp
     generic_model_converter.cpp
     goal.cpp

src/tactic/aig/aig_tactic.cpp

@@ -90,13 +90,8 @@ public:
         SASSERT(g->is_well_sorted());
     }
     
-    virtual void operator()(goal_ref const & g, 
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result) {
-                            goal_ref_buffer & result, 
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         fail_if_proof_generation("aig", g);
-        mc = 0; pc = 0; core = 0;
         operator()(g);
         g->inc_depth();
         result.push_back(g.get());

src/tactic/arith/add_bounds_tactic.cpp

@@ -111,11 +111,7 @@ class add_bounds_tactic : public tactic {
         };
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
-            mc = 0; pc = 0; core = 0;
             tactic_report report("add-bounds", *g);
             bound_manager bm(m);
             expr_fast_mark1 visited;
@@ -161,11 +157,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(g, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(g, result, mc, pc, core);
     }
     
     virtual void cleanup() {

src/tactic/arith/arith_bounds_tactic.cpp

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

src/tactic/arith/card2bv_tactic.cpp

@@ -53,13 +53,10 @@ public:
 
     
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         TRACE("card2bv-before", g->display(tout););
         SASSERT(g->is_well_sorted());
-        mc = 0; pc = 0; core = 0; result.reset();
+        result.reset();
         tactic_report report("card2bv", *g);
         th_rewriter rw1(m, m_params);
         pb2bv_rewriter rw2(m, m_params);
@@ -90,10 +87,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) {
+            for (func_decl* f : fns) filter->hide(f);
-                filter->hide(fns[i]);
+            g->add(filter);
-            }
-            mc = filter;
         }
 
         g->inc_depth();

src/tactic/arith/degree_shift_tactic.cpp

@@ -223,16 +223,13 @@ class degree_shift_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             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);
@@ -270,6 +267,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,11 +289,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
     }
     
     virtual void cleanup() {

src/tactic/arith/diff_neq_tactic.cpp

@@ -313,13 +313,10 @@ class diff_neq_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
             m_produce_models = g->models_enabled();
-            mc = 0; pc = 0; core = 0; result.reset();
+            result.reset();
             tactic_report report("diff-neq", *g);
             fail_if_proof_generation("diff-neq", g);
             fail_if_unsat_core_generation("diff-neq", g);
@@ -332,8 +329,9 @@ class diff_neq_tactic : public tactic {
             bool r = search();
             report_tactic_progress(":conflicts", m_num_conflicts);
             if (r) {
-                if (m_produce_models)
+                if (m_produce_models) {
-                    mc = model2model_converter(mk_model());
+                    g->add(model2model_converter(mk_model()));
+                }
                 g->reset();
             }
             else {
@@ -384,11 +382,8 @@ public:
        If s is not really in the difference logic fragment, then this is a NOOP.
     */
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
     }
     
     virtual void cleanup() {

src/tactic/arith/elim01_tactic.cpp

@@ -41,8 +41,7 @@ public:
         m_refs(m)
     {}
 
-    virtual void operator()(model_ref & old_model, unsigned goal_idx) {
+    virtual void operator()(model_ref & old_model) {
-        SASSERT(goal_idx == 0);
         model * new_model = alloc(model, m);
         unsigned num = old_model->get_num_constants();
         for (unsigned i = 0; i < m_nums_as_int.size(); ++i) {
@@ -153,18 +152,13 @@ public:
 
     
     virtual void operator()(goal_ref const & g, 
-                    goal_ref_buffer & result, 
+                    goal_ref_buffer & result) {
-                    model_converter_ref & mc, 
-                    proof_converter_ref & pc,
-                    expr_dependency_ref & core) {
         SASSERT(g->is_well_sorted());
-        mc = 0; pc = 0; core = 0;
         
         tactic_report report("elim01", *g);
         
         expr_safe_replace sub(m);
-        bool2int_model_converter* b2i = alloc(bool2int_model_converter, m);
+        ref<bool2int_model_converter> b2i = alloc(bool2int_model_converter, m);
-        mc = b2i;
         bound_manager bounds(m);
         expr_ref_vector axioms(m);
         bounds(*g);
@@ -179,7 +173,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: " 
@@ -205,9 +199,9 @@ public:
             }
             g->update(i, new_curr, new_pr, g->dep(i));
         }
-        for (unsigned i = 0; i < axioms.size(); ++i) {
+        for (expr* a : axioms) 
-            g->assert_expr(axioms[i].get());
+            g->assert_expr(a);
-        }
+        g->add(b2i.get());
         g->inc_depth();
         result.push_back(g.get());
         TRACE("pb", g->display(tout););

src/tactic/arith/eq2bv_tactic.cpp

@@ -149,14 +149,8 @@ public:
     void updt_params(params_ref const & p) {
     }
     
-    virtual void operator()(
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result) {
-        goal_ref const & g, 
-        goal_ref_buffer & result, 
-        model_converter_ref & mc, 
-        proof_converter_ref & pc,
-        expr_dependency_ref & core) {
         SASSERT(g->is_well_sorted());
-        mc = 0; pc = 0; core = 0;
         m_trail.reset();
         m_fd.reset();
         m_max.reset();
@@ -212,7 +206,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());        

src/tactic/arith/factor_tactic.cpp

@@ -257,12 +257,8 @@ class factor_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g,
-                        goal_ref_buffer & result,
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc,
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("factor", *g);
             bool produce_proofs = g->proofs_enabled();
 
@@ -313,12 +309,9 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc,
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         try {
-            (*m_imp)(in, result, mc, pc, core);
+            (*m_imp)(in, result);
         }
         catch (z3_error & ex) {
             throw ex;

src/tactic/arith/fix_dl_var_tactic.cpp

@@ -249,12 +249,8 @@ class fix_dl_var_tactic : public tactic {
         }
                 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("fix-dl-var", *g);
             bool produce_proofs = g->proofs_enabled();
             m_produce_models    = g->models_enabled();
@@ -270,9 +266,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);
+                    generic_model_converter * mc = alloc(generic_model_converter, m);
-                    _mc->add(var, zero);
+                    mc->add(var, zero);
-                    mc = _mc;
+                    g->add(mc);
                 }
                 
                 expr_ref   new_curr(m);
@@ -321,12 +317,9 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         try {
-            (*m_imp)(in, result, mc, pc, core);
+            (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());

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);
@@ -1550,12 +1550,8 @@ class fm_tactic : public tactic {
         }
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("fm", *g);
             fail_if_proof_generation("fm", g);
             m_produce_models = g->models_enabled();
@@ -1603,7 +1599,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,11 +1671,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
     }
 };
 

src/tactic/arith/lia2card_tactic.cpp

@@ -159,12 +159,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & g, 
-                    goal_ref_buffer & result, 
+                    goal_ref_buffer & result) {
-                    model_converter_ref & mc, 
-                    proof_converter_ref & pc,
-                    expr_dependency_ref & core) {
         SASSERT(g->is_well_sorted());
-        mc = 0; pc = 0; core = 0;
         m_01s->reset();
         
         tactic_report report("cardinality-intro", *g);
@@ -173,9 +169,7 @@ public:
         bounds(*g);
 
         
-        bound_manager::iterator bit = bounds.begin(), bend = bounds.end();
+        for (expr* x : bounds) {
-        for (; bit != bend; ++bit) {
-            expr* x = *bit;
             bool s1 = false, s2 = false;
             rational lo, hi;
             if (a.is_int(x) && 
@@ -197,9 +191,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 (expr* v : *m_01s) {
-        for (; it != end; ++it) {
-            expr* v = *it;
             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));

src/tactic/arith/lia2pb_tactic.cpp

@@ -188,15 +188,12 @@ class lia2pb_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
             fail_if_proof_generation("lia2pb", g);
             m_produce_models      = g->models_enabled();
             m_produce_unsat_cores = g->unsat_core_enabled();
-            mc = 0; pc = 0; core = 0; result.reset();
+            result.reset();
             tactic_report report("lia2pb", *g);
             m_bm.reset(); m_rw.reset(); m_new_deps.reset();
 
@@ -223,10 +220,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<generic_model_converter> gmc;
             if (m_produce_models) {
                 gmc = alloc(generic_model_converter, m);
-                mc  = gmc;
             }
             
             expr_ref zero(m);
@@ -296,6 +292,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,12 +327,9 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         try {
-            (*m_imp)(in, result, mc, pc, core);
+            (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());

src/tactic/arith/nla2bv_tactic.cpp

@@ -440,19 +440,17 @@ public:
        \return false if transformation is not possible.
     */
     virtual void operator()(goal_ref const & g,
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         SASSERT(g->is_well_sorted());
         fail_if_proof_generation("nla2bv", g);
         fail_if_unsat_core_generation("nla2bv", g);
-        mc = 0; pc = 0; core = 0; result.reset();
+        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());
     }

src/tactic/arith/normalize_bounds_tactic.cpp

@@ -79,12 +79,7 @@ class normalize_bounds_tactic : public tactic {
             return false;
         }
         
-        void operator()(goal_ref const & in, 
+        void operator()(goal_ref const & in, goal_ref_buffer & result) {
-                        goal_ref_buffer & result, 
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
-            mc = 0; pc = 0; core = 0;
             bool produce_models = in->models_enabled();
             bool produce_proofs = in->proofs_enabled();
             tactic_report report("normalize-bounds", *in);
@@ -100,16 +95,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();
+            for (expr * x : m_bm) {
-            bound_manager::iterator end = m_bm.end();
-            for (; it != end; ++it) {
-                expr * x = *it;
                 if (is_target(x, val)) {
                     num_norm_bounds++;
                     sort * s = m.get_sort(x);
@@ -171,12 +163,9 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         try {
-            (*m_imp)(in, result, mc, pc, core);
+            (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());

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<func_decl, expr*> const & c2bit, bound_manager const & bm):
     m(_m) {
-    obj_map<func_decl, expr*>::iterator it  = c2bit.begin();
+    for (auto const& kv : c2bit) {
-    obj_map<func_decl, expr*>::iterator end = c2bit.end();
+        m_c2bit.push_back(func_decl_pair(kv.m_key, to_app(kv.m_value)->get_decl()));
-    for ( ; it != end; it++) {
+        m.inc_ref(kv.m_key);
-        m_c2bit.push_back(func_decl_pair(it->m_key, to_app(it->m_value)->get_decl()));
+        m.inc_ref(to_app(kv.m_value)->get_decl());
-        m.inc_ref(it->m_key);
-        m.inc_ref(to_app(it->m_value)->get_decl());
     }      
-    bound_manager::iterator it2  = bm.begin();
+    for (expr* c : bm) {
-    bound_manager::iterator end2 = bm.end();
-    for (; it2 != end2; ++it2) {
-        expr * c = *it2;
         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<func_decl
 }
     
 pb2bv_model_converter::~pb2bv_model_converter() {
-    svector<func_decl_pair>::const_iterator it  = m_c2bit.begin();
+    for (auto const& kv : m_c2bit) {
-    svector<func_decl_pair>::const_iterator end = m_c2bit.end();
+        m.dec_ref(kv.first);
-    for (; it != end; ++it) {
+        m.dec_ref(kv.second);
-        m.dec_ref(it->first);
-        m.dec_ref(it->second);
     }
 }
 
-void pb2bv_model_converter::operator()(model_ref & md) {
-    (*this)(md, 0);
-}
 
-void pb2bv_model_converter::operator()(model_ref & md, unsigned goal_idx) {
+void pb2bv_model_converter::operator()(model_ref & md) {
-    SASSERT(goal_idx == 0);
     TRACE("pb2bv", tout << "converting model:\n"; model_v2_pp(tout, *md); display(tout););
     arith_util a_util(m);
 
-    svector<func_decl_pair>::const_iterator it  = m_c2bit.begin();
+    for (auto const& kv : m_c2bit) {
-    svector<func_decl_pair>::const_iterator end = m_c2bit.end();
+        if (kv.second) {
-    for (; it != end; ++it) {
+            expr * val = md->get_const_interp(kv.second);
-        if (it->second) {
-            expr * val = md->get_const_interp(it->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.
+            // kv.first is a don't care.
-            md->register_decl(it->first, a_util.mk_numeral(rational(0), true));
+            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<func_decl_pair>::const_iterator it  = m_c2bit.begin();
+    for (auto const& kv : m_c2bit) {
-    svector<func_decl_pair>::const_iterator end = m_c2bit.end();
+        out << "\n  (" << kv.first->get_name() << " ";            
-    for (; it != end; ++it) {
+        if (kv.second == 0)
-        out << "\n  (" << it->first->get_name() << " ";            
-        if (it->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<func_decl_pair>::iterator it = m_c2bit.begin();
+    for (auto const& kv : m_c2bit) {
-    svector<func_decl_pair>::iterator end = m_c2bit.end();
+        func_decl * f1 = translator(kv.first);
-    for (; it != end; it++) {
+        func_decl * f2 = translator(kv.second);
-        func_decl * f1 = translator(it->first);
-        func_decl * f2 = translator(it->second);
         res->m_c2bit.push_back(func_decl_pair(f1, f2));
         to.inc_ref(f1);
         to.inc_ref(f2);

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<func_decl, expr*> const & c2bit, bound_manager const & bm);
     virtual ~pb2bv_model_converter();
-    virtual void operator()(model_ref & md);
+    void operator()(model_ref & md) override;
-    virtual void operator()(model_ref & md, unsigned goal_idx);
+    void display(std::ostream & out) override;
-    virtual void display(std::ostream & out);
+    model_converter * translate(ast_translation & translator) override;
-    virtual model_converter * translate(ast_translation & translator);
 };
 
 #endif

src/tactic/arith/pb2bv_tactic.cpp

@@ -886,16 +886,13 @@ private:
         }
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             TRACE("pb2bv", g->display(tout););
             SASSERT(g->is_well_sorted());
             fail_if_proof_generation("pb2bv", g);
             m_produce_models      = g->models_enabled();
             m_produce_unsat_cores = g->unsat_core_enabled();
-            mc = 0; pc = 0; core = 0; result.reset();
+            result.reset();
             tactic_report report("pb2bv", *g);
             m_bm.reset(); m_rw.reset(); m_new_deps.reset();
 
@@ -949,6 +946,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);
@@ -957,7 +955,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,11 +998,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
     }
     
     virtual void cleanup() {

src/tactic/arith/propagate_ineqs_tactic.cpp

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

src/tactic/arith/purify_arith_tactic.cpp

@@ -821,13 +821,9 @@ public:
     }
     
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         try {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("purify-arith", *g);
             TRACE("purify_arith", g->display(tout););
             bool produce_proofs = g->proofs_enabled();
@@ -835,10 +831,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););

src/tactic/arith/recover_01_tactic.cpp

@@ -292,15 +292,12 @@ class recover_01_tactic : public tactic {
         }
     
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
             fail_if_proof_generation("recover-01", g);
             fail_if_unsat_core_generation("recover-01", g);
             m_produce_models      = g->models_enabled();
-            mc = 0; pc = 0; core = 0; result.reset();
+            result.reset();
             tactic_report report("recover-01", *g);
             
             bool saved = false;
@@ -308,7 +305,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);
@@ -327,7 +326,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);
@@ -336,25 +335,20 @@ class recover_01_tactic : public tactic {
             bool recovered = false;
             expr_substitution _subst(m);
             subst = &_subst;
-            var2clauses::iterator it  = m_var2clauses.begin();
+            for (auto& kv : m_var2clauses) {
-            var2clauses::iterator end = m_var2clauses.end();
+                if (process(kv.m_key, kv.m_value)) {
-            for (; it != end; ++it) {
-                if (process(it->m_key, it->m_value)) {
                     recovered = true;
                     counter++;
                 }
                 else {
-                    ptr_vector<app>::iterator it2   = it->m_value.begin();
+                    for (app* a : kv.m_value) {
-                    ptr_vector<app>::iterator end2  = it->m_value.end();
+                        new_goal->assert_expr(a);
-                    for (; it2 != end2; ++it2) {
-                        new_goal->assert_expr(*it2);
                     }
                 }
             }
             
             if (!recovered) {
                 result.push_back(g.get());
-                mc = 0;
                 return;
             }
             
@@ -406,12 +400,9 @@ public:
     }
 
     void operator()(goal_ref const & g, 
-                    goal_ref_buffer & result, 
+                    goal_ref_buffer & result) {
-                    model_converter_ref & mc, 
-                    proof_converter_ref & pc,
-                    expr_dependency_ref & core) {
         try {
-            (*m_imp)(g, result, mc, pc, core);
+            (*m_imp)(g, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());

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 {
+    void operator()(model_ref & md) override {
-        SASSERT(goal_idx == 0);
         model * new_model = alloc(model, m());
         obj_hashtable<func_decl> 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.

src/tactic/bv/bit_blaster_tactic.cpp

@@ -51,11 +51,7 @@ class bit_blaster_tactic : public tactic {
         
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
-            mc = 0; pc = 0; core = 0;
             bool proofs_enabled = g->proofs_enabled();
 
             if (proofs_enabled && m_blast_quant)
@@ -88,12 +84,10 @@ class bit_blaster_tactic : public tactic {
             }
             
             if (change && g->models_enabled())  
-                mc = mk_bit_blaster_model_converter(m(), m_rewriter->const2bits());
+                g->add(mk_bit_blaster_model_converter(m(), m_rewriter->const2bits()));
-            else
-                mc = 0;
             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,12 +129,9 @@ public:
     }
      
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         try {
-            (*m_imp)(g, result, mc, pc, core);
+            (*m_imp)(g, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());

src/tactic/bv/bv1_blaster_tactic.cpp

@@ -379,11 +379,7 @@ class bv1_blaster_tactic : public tactic {
         
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
-            mc = 0; pc = 0; core = 0;
             
             if (!is_target(*g))
                 throw tactic_exception("bv1 blaster cannot be applied to goal");
@@ -409,7 +405,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,11 +451,8 @@ public:
        Return a model_converter that converts any model for the updated set into a model for the old set.
     */
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(g, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(g, result, mc, pc, core);
     }
     
     virtual void cleanup() {

src/tactic/bv/bv_bound_chk_tactic.cpp

@@ -136,11 +136,7 @@ class bv_bound_chk_tactic : public tactic {
 public:
     bv_bound_chk_tactic(ast_manager & m, params_ref const & p);
     virtual ~bv_bound_chk_tactic();
-    void operator()(goal_ref const & g,
+    void operator()(goal_ref const & g, goal_ref_buffer & result) override;
-        goal_ref_buffer & result,
-        model_converter_ref & mc,
-        proof_converter_ref & pc,
-        expr_dependency_ref & core);
     virtual tactic * translate(ast_manager & m);
     virtual void updt_params(params_ref const & p);
     void cleanup();
@@ -197,16 +193,12 @@ bv_bound_chk_tactic::~bv_bound_chk_tactic() {
     dealloc(m_imp);
 }
 
-void bv_bound_chk_tactic::operator()(goal_ref const & g,
+void bv_bound_chk_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) {
-        goal_ref_buffer & result,
-        model_converter_ref & mc,
-        proof_converter_ref & pc,
-        expr_dependency_ref & core) {
     SASSERT(g->is_well_sorted());
     fail_if_proof_generation("bv-bound-chk", g);
     fail_if_unsat_core_generation("bv-bound-chk", g);
     TRACE("bv-bound-chk", g->display(tout << "before:"); tout << std::endl;);
-    mc = 0; pc = 0; core = 0; result.reset();
+    result.reset();
     m_imp->operator()(g);
     g->inc_depth();
     result.push_back(g.get());

src/tactic/bv/bv_size_reduction_tactic.cpp

@@ -39,7 +39,7 @@ public:
 
     virtual ~bv_size_reduction_tactic();
 
-    virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result);
 
     virtual void cleanup();
 };
@@ -382,16 +382,15 @@ bv_size_reduction_tactic::~bv_size_reduction_tactic() {
 }
 
 void bv_size_reduction_tactic::operator()(goal_ref const & g, 
-                                          goal_ref_buffer & result, 
+                                          goal_ref_buffer & result) {
-                                          model_converter_ref & mc, 
-                                          proof_converter_ref & pc,
-                                          expr_dependency_ref & core) {
     SASSERT(g->is_well_sorted());
     fail_if_proof_generation("bv-size-reduction", g);
     fail_if_unsat_core_generation("bv-size-reduction", g);
-    mc = 0; pc = 0; core = 0; result.reset();
+    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());
 }

src/tactic/bv/bvarray2uf_tactic.cpp

@@ -53,18 +53,16 @@ class bvarray2uf_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g,
-                        goal_ref_buffer & result,
+                        goal_ref_buffer & result)
-                        model_converter_ref & mc,
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core)
         {
             SASSERT(g->is_well_sorted());
             tactic_report report("bvarray2uf", *g);
-            mc = 0; pc = 0; core = 0; result.reset();
+            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);
@@ -93,6 +91,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,11 +128,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc,
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
     }
 
     virtual void cleanup() {

src/tactic/bv/dt2bv_tactic.cpp

@@ -116,12 +116,7 @@ public:
     virtual void collect_param_descrs(param_descrs & r) {
     }
 
-    virtual void operator()(goal_ref const & g,
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result) {
-                            goal_ref_buffer & result,
-                            model_converter_ref & mc,
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        mc = 0; pc = 0; core = 0;
         bool produce_proofs = g->proofs_enabled();
         tactic_report report("dt2bv", *g);
         unsigned   size = g->size();
@@ -155,7 +150,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();

src/tactic/bv/elim_small_bv_tactic.cpp

@@ -224,13 +224,8 @@ class elim_small_bv_tactic : public tactic {
             m_rw.cfg().updt_params(p);
         }
 
-        void operator()(goal_ref const & g,
+        void operator()(goal_ref const & g, goal_ref_buffer & result) {
-            goal_ref_buffer & result,
-            model_converter_ref & mc,
-            proof_converter_ref & pc,
-            expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("elim-small-bv", *g);
             bool produce_proofs = g->proofs_enabled();
             fail_if_proof_generation("elim-small-bv", g);
@@ -250,7 +245,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,11 +283,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-        goal_ref_buffer & result,
+        goal_ref_buffer & result) {
-        model_converter_ref & mc,
+        (*m_imp)(in, result);
-        proof_converter_ref & pc,
-        expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
     }
 
     virtual void cleanup() {

src/tactic/bv/max_bv_sharing_tactic.cpp

@@ -237,12 +237,8 @@ class max_bv_sharing_tactic : public tactic {
         ast_manager & m() const { return m_rw.m(); }
                 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("max-bv-sharing", *g);
             bool produce_proofs = g->proofs_enabled();
             
@@ -299,11 +295,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
     }
     
     virtual void cleanup() {

src/tactic/core/blast_term_ite_tactic.cpp

@@ -113,13 +113,8 @@ class blast_term_ite_tactic : public tactic {
             m_rw.cfg().updt_params(p);
         }
         
-        void operator()(goal_ref const & g, 
+        void operator()(goal_ref const & g, goal_ref_buffer & result) {
-                        goal_ref_buffer & result, 
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("blast-term-ite", *g);
             bool produce_proofs = g->proofs_enabled();
 
@@ -172,11 +167,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
     }
     
     virtual void cleanup() {

src/tactic/core/cofactor_term_ite_tactic.cpp

@@ -54,16 +54,11 @@ public:
     virtual void updt_params(params_ref const & p) { m_params = p; m_elim_ite.updt_params(p); }
     virtual void collect_param_descrs(param_descrs & r) { m_elim_ite.collect_param_descrs(r); }
     
-    virtual void operator()(goal_ref const & g, 
+    void  operator()(goal_ref const & g, goal_ref_buffer& result) override {
-                            goal_ref_buffer & result, 
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         SASSERT(g->is_well_sorted());
         fail_if_proof_generation("cofactor-term-ite", g);
         fail_if_unsat_core_generation("cofactor-term-ite", g);
         tactic_report report("cofactor-term-ite", *g);
-        mc = 0; pc = 0; core = 0;
         process(*(g.get()));
         g->inc_depth();
         result.push_back(g.get());

src/tactic/core/collect_statistics_tactic.cpp

@@ -63,10 +63,7 @@ public:
 
     virtual void collect_param_descrs(param_descrs & r) {}
 
-    virtual void operator()(goal_ref const & g, goal_ref_buffer & result,
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result) {
-                            model_converter_ref & mc, proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        mc = 0;
         tactic_report report("collect-statistics", *g);
 
         collect_proc cp(m, m_stats);
@@ -76,10 +73,8 @@ public:
             for_each_expr(cp, visited, g->form(i));
 
         std::cout << "(" << std::endl;
-        stats_type::iterator it = m_stats.begin();
+        for (auto const& kv : m_stats) 
-        stats_type::iterator end = m_stats.end();
+            std::cout << " :" << kv.first << "    " << kv.second << std::endl;
-        for (; it != end; it++)
-            std::cout << " :" << it->first << "    " << it->second << std::endl;
         std::cout << ")" << std::endl;
 
         g->inc_depth();

src/tactic/core/ctx_simplify_tactic.cpp

@@ -621,11 +621,7 @@ void ctx_simplify_tactic::get_param_descrs(param_descrs & r) {
 }
 
 void ctx_simplify_tactic::operator()(goal_ref const & in,
-                                     goal_ref_buffer & result,
+                                     goal_ref_buffer & result) {
-                                     model_converter_ref & mc,
-                                     proof_converter_ref & pc,
-                                     expr_dependency_ref & core) {
-    mc = 0; pc = 0; core = 0;
     (*m_imp)(*(in.get()));
     in->inc_depth();
     result.push_back(in.get());

src/tactic/core/ctx_simplify_tactic.h

@@ -55,10 +55,7 @@ public:
     virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result);
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core);
 
     virtual void cleanup();
 };

src/tactic/core/der_tactic.cpp

@@ -74,11 +74,7 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        mc = 0; pc = 0; core = 0;
         (*m_imp)(*(in.get()));
         in->inc_depth();
         result.push_back(in.get());

src/tactic/core/distribute_forall_tactic.cpp

@@ -100,16 +100,13 @@ public:
     }
 
     virtual void operator()(goal_ref const & g,
-                            goal_ref_buffer & result,
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc,
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         SASSERT(g->is_well_sorted());
         ast_manager & m = g->m();
         bool produce_proofs = g->proofs_enabled();
         rw r(m, produce_proofs);
         m_rw = &r;
-        mc = 0; pc = 0; core = 0; result.reset();
+        result.reset();
         tactic_report report("distribute-forall", *g);
 
         expr_ref   new_curr(m);

src/tactic/core/dom_simplify_tactic.cpp

@@ -183,19 +183,11 @@ tactic * dom_simplify_tactic::translate(ast_manager & m) {
     return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params);
 }
 
-void dom_simplify_tactic::operator()(
+void dom_simplify_tactic::operator()(goal_ref const & in, goal_ref_buffer & result) {
-    goal_ref const & in,
-    goal_ref_buffer & result,
-    model_converter_ref & mc,
-    proof_converter_ref & pc,
-    expr_dependency_ref & core) {
-    mc = 0; pc = 0; core = 0;
-
     tactic_report report("dom-simplify", *in.get());
     simplify_goal(*(in.get()));
     in->inc_depth();
     result.push_back(in.get());
-
 }
 
 void dom_simplify_tactic::cleanup() {

src/tactic/core/dom_simplify_tactic.h

@@ -137,11 +137,7 @@ public:
     static  void get_param_descrs(param_descrs & r) {}
     virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
     
-    virtual void operator()(goal_ref const & in, 
+    void operator()(goal_ref const & in, goal_ref_buffer & result) override;
-                            goal_ref_buffer & result, 
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core);
 
     virtual void cleanup();
 };

src/tactic/core/elim_term_ite_tactic.cpp

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

src/tactic/core/elim_uncnstr_tactic.cpp

@@ -816,11 +816,7 @@ class elim_uncnstr_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                                goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                                model_converter_ref & mc, 
-                                proof_converter_ref & pc,
-                                expr_dependency_ref & core) {
-            mc = 0; pc = 0; core = 0;
             bool produce_models = g->models_enabled();
             bool produce_proofs = g->proofs_enabled();
 
@@ -865,8 +861,7 @@ class elim_uncnstr_tactic : public tactic {
                     g->update(idx, new_f, new_pr, g->dep(idx));
                 }
                 if (!modified) {
-                    if (round == 0) {
+                    if (round == 0) {                        
-                        mc   = 0;
                     }
                     else {
                         app_ref_vector & fresh_vars = m_rw->cfg().m_fresh_vars;
@@ -875,15 +870,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,11 +927,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(g, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(g, result, mc, pc, core);
         report_tactic_progress(":num-elim-apps", get_num_elim_apps());
     }
     

src/tactic/core/injectivity_tactic.cpp

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

src/tactic/core/nnf_tactic.cpp

@@ -54,13 +54,9 @@ public:
     virtual void collect_param_descrs(param_descrs & r) { nnf::get_param_descrs(r); }
 
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         TRACE("nnf", tout << "params: " << m_params << "\n"; g->display(tout););
         SASSERT(g->is_well_sorted());
-        mc = 0; pc = 0; core = 0;
         tactic_report report("nnf", *g);
         bool produce_proofs = g->proofs_enabled();
 
@@ -98,7 +94,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));
         }

src/tactic/core/occf_tactic.cpp

@@ -128,13 +128,9 @@ class occf_tactic : public tactic {
         }
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
+            
-
             fail_if_proof_generation("occf", g);
 
             bool produce_models = g->models_enabled();
@@ -158,7 +154,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,11 +207,8 @@ public:
     virtual void collect_param_descrs(param_descrs & r) {}
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) {
-                            model_converter_ref & mc, 
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
     }
     
     virtual void cleanup() {

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) {
+    virtual void operator()(model_ref & mdl) {
-        SASSERT(goal_idx == 0);
         for (auto const& kv : m_const) {
             mdl->register_decl(kv.first->get_decl(), kv.second);
         }
@@ -148,21 +147,17 @@ public:
         return alloc(pb_preprocess_tactic, m);
     }
     
-    virtual void operator()(
+    void operator()(
         goal_ref const & g, 
-        goal_ref_buffer & result, 
+        goal_ref_buffer & result) override {
-        model_converter_ref & mc, 
-        proof_converter_ref & pc,
-        expr_dependency_ref & core) {
         SASSERT(g->is_well_sorted());
-        pc = 0; core = 0;
 
         if (g->proofs_enabled()) {
             throw tactic_exception("pb-preprocess does not support proofs");
         }
 
         pb_preproc_model_converter* pp = alloc(pb_preproc_model_converter, m);
-        mc = pp;
+        g->add(pp);
 
         g->inc_depth();        
         result.push_back(g.get());       

src/tactic/core/propagate_values_tactic.cpp

@@ -136,12 +136,8 @@ class propagate_values_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
+                        goal_ref_buffer & result) {
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
             tactic_report report("propagate-values", *g);
             m_goal = g.get();
 
@@ -240,13 +236,9 @@ public:
         r.insert("max_rounds", CPK_UINT, "(default: 2) maximum number of rounds.");
     }
     
-    virtual void operator()(goal_ref const & in, 
+    void operator()(goal_ref const & in, goal_ref_buffer & result) override {
-                            goal_ref_buffer & result, 
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
         try {
-            (*m_imp)(in, result, mc, pc, core);
+            (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());

src/tactic/core/reduce_args_tactic.cpp

@@ -73,8 +73,8 @@ public:
 
     virtual ~reduce_args_tactic();
     
-    virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
+    void operator()(goal_ref const & g, goal_ref_buffer & result) override;
-    virtual void cleanup();
+    void cleanup() override;
 };
 
 tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) {
@@ -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););
     }
 };
 
@@ -483,15 +483,12 @@ reduce_args_tactic::~reduce_args_tactic() {
 }
 
 void reduce_args_tactic::operator()(goal_ref const & g, 
-                                    goal_ref_buffer & result, 
+                                    goal_ref_buffer & result) {
-                                    model_converter_ref & mc, 
-                                    proof_converter_ref & pc,
-                                    expr_dependency_ref & core) {
     SASSERT(g->is_well_sorted());
     fail_if_proof_generation("reduce-args", g);
     fail_if_unsat_core_generation("reduce-args", g);
-    mc = 0; pc = 0; core = 0; result.reset();
+    result.reset();
-    m_imp->operator()(*(g.get()), mc);
+    m_imp->operator()(*(g.get()));
     g->inc_depth();
     result.push_back(g.get());
     SASSERT(g->is_well_sorted());

src/tactic/core/simplify_tactic.cpp

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

src/tactic/core/simplify_tactic.h

@@ -30,21 +30,19 @@ public:
     simplify_tactic(ast_manager & m, params_ref const & ref = params_ref());
     virtual ~simplify_tactic();
 
-    virtual void updt_params(params_ref const & p);
+    void updt_params(params_ref const & p) override;
+
     static void get_param_descrs(param_descrs & r);
-    virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
     
-    virtual void operator()(goal_ref const & in, 
+    void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); }
-                            goal_ref_buffer & result, 
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core);
     
-    virtual void cleanup();
+    void operator()(goal_ref const & in, goal_ref_buffer & result) override;
+    
+    void cleanup() override;
 
     unsigned get_num_steps() const;
 
-    virtual tactic * translate(ast_manager & m) { return alloc(simplify_tactic, m, m_params); }
+    tactic * translate(ast_manager & m) override { return alloc(simplify_tactic, m, m_params); }
 
 };
 

src/tactic/core/solve_eqs_tactic.cpp

@@ -666,13 +666,9 @@ class solve_eqs_tactic : public tactic {
             return m_num_eliminated_vars;
         }
         
-        void operator()(goal_ref const & g, 
+        void operator()(goal_ref const & g, goal_ref_buffer & result) {
-                        goal_ref_buffer & result, 
-                        model_converter_ref & mc, 
-                        proof_converter_ref & pc,
-                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            mc = 0; pc = 0; core = 0;
+            model_converter_ref mc;
             tactic_report report("solve_eqs", *g);
             m_produce_models = g->models_enabled();
             m_produce_proofs = g->proofs_enabled();
@@ -692,7 +688,6 @@ class solve_eqs_tactic : public tactic {
                     normalize();
                     substitute(*(g.get()));
                     if (g->inconsistent()) {
-                        mc   = 0;
                         break;
                     }
                     save_elim_vars(mc);
@@ -700,6 +695,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());
@@ -733,12 +729,9 @@ public:
         r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver.");
     }
     
-    virtual void operator()(goal_ref const & in, 
+    void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
+                            goal_ref_buffer & result) override {
-                            model_converter_ref & mc, 
+        (*m_imp)(in, result);
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, mc, pc, core);
         report_tactic_progress(":num-elim-vars", m_imp->get_num_eliminated_vars());
     }