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