diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 4daf3956f..6a8a378e5 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -97,6 +97,19 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
+ Z3_solver Z3_API Z3_solver_translate(Z3_context c, Z3_solver s, Z3_context target) {
+ Z3_TRY;
+ LOG_Z3_solver_translate(c, s, target);
+ RESET_ERROR_CODE();
+ params_ref const& p = to_solver(s)->m_params;
+ Z3_solver_ref * sr = alloc(Z3_solver_ref, 0);
+ sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
+ mk_c(target)->save_object(sr);
+ Z3_solver r = of_solver(sr);
+ RETURN_Z3(r);
+ Z3_CATCH_RETURN(0);
+ }
+
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s) {
Z3_TRY;
LOG_Z3_solver_get_help(c, s);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 9c04ee98a..9cfad3415 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1359,9 +1359,13 @@ namespace z3 {
Z3_solver_inc_ref(ctx(), s);
}
public:
+ struct simple {};
+ struct translate {};
solver(context & c):object(c) { init(Z3_mk_solver(c)); }
+ solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); }
solver(context & c, Z3_solver s):object(c) { init(s); }
solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
+ solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
solver(solver const & s):object(s) { init(s.m_solver); }
~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
operator Z3_solver() const { return m_solver; }
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 80ca7a0cd..c9e76e68e 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -290,6 +290,17 @@ namespace Microsoft.Z3
}
}
+ ///
+ /// Create a clone of the current solver with respect to ctx.
+ ///
+ public Solver Translate(Context ctx)
+ {
+ Contract.Requires(ctx != null);
+ Contract.Ensures(Contract.Result() != null);
+ return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
+ }
+
+
///
/// Solver statistics.
///
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 4d2d9b641..f312da051 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -293,6 +293,14 @@ public class Solver extends Z3Object
getNativeObject());
}
+ /**
+ * Create a clone of the current solver with respect to ctx.
+ */
+ public Solver translate(Context ctx)
+ {
+ return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
+ }
+
/**
* Solver statistics.
*
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 3183ad693..acee87f54 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -6084,6 +6084,19 @@ class Solver(Z3PPObject):
"""Return a formatted string with all added constraints."""
return obj_to_string(self)
+ def translate(self, target):
+ """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
+
+ >>> c1 = Context()
+ >>> c2 = Context()
+ >>> s1 = Solver(ctx=c1)
+ >>> s2 = s1.translate(c2)
+ """
+ if __debug__:
+ _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
+ solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
+ return Solver(solver, target)
+
def sexpr(self):
"""Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index d0bf20188..9887cd7f0 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -7062,6 +7062,14 @@ END_MLAPI_EXCLUDE
*/
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
+ /**
+ \brief Copy a solver \c s from the context \c source to a the context \c target.
+
+ def_API('Z3_solver_translate', SOLVER, (_in(CONTEXT), _in(SOLVER), _in(CONTEXT)))
+ */
+ Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target);
+
+
/**
\brief Return a string describing all solver available parameters.
diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
index 47842ae90..0e315c38d 100644
--- a/src/ast/array_decl_plugin.cpp
+++ b/src/ast/array_decl_plugin.cpp
@@ -519,6 +519,7 @@ void array_decl_plugin::get_op_names(svector& op_names, symbol con
op_names.push_back(builtin_name("complement",OP_SET_COMPLEMENT));
op_names.push_back(builtin_name("subset",OP_SET_SUBSET));
op_names.push_back(builtin_name("as-array", OP_AS_ARRAY));
+ //op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT_SKOLEM));
}
}
diff --git a/src/ast/ast_translation.cpp b/src/ast/ast_translation.cpp
index e49edb7ab..4b1a80908 100644
--- a/src/ast/ast_translation.cpp
+++ b/src/ast/ast_translation.cpp
@@ -184,6 +184,7 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) {
}
ast * ast_translation::process(ast const * _n) {
+ if (!_n) return 0;
SASSERT(m_result_stack.empty());
SASSERT(m_frame_stack.empty());
SASSERT(m_extra_children_stack.empty());
diff --git a/src/ast/ast_translation.h b/src/ast/ast_translation.h
index b1b12c1c6..ec187110b 100644
--- a/src/ast/ast_translation.h
+++ b/src/ast/ast_translation.h
@@ -58,9 +58,9 @@ public:
template
T * operator()(T const * n) {
- SASSERT(from().contains(const_cast(n)));
+ SASSERT(!n || from().contains(const_cast(n)));
ast * r = process(n);
- SASSERT(to().contains(const_cast(r)));
+ SASSERT((!n && !r) || to().contains(const_cast(r)));
return static_cast(r);
}
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index bf7a39424..8652ab7fd 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -63,6 +63,11 @@ namespace opt {
m_context.updt_params(_p);
}
+ solver* opt_solver::translate(ast_manager& m, params_ref const& p) {
+ UNREACHABLE();
+ return 0;
+ }
+
void opt_solver::collect_param_descrs(param_descrs & r) {
m_context.collect_param_descrs(r);
}
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 9e74e9127..0e53e07c6 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -86,6 +86,7 @@ namespace opt {
opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm);
virtual ~opt_solver();
+ virtual solver* translate(ast_manager& m, params_ref const& p);
virtual void updt_params(params_ref & p);
virtual void collect_param_descrs(param_descrs & r);
virtual void collect_statistics(statistics & st) const;
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index fd1f4cfd0..b0d771ba8 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -32,6 +32,7 @@ Notes:
#include "model_smt2_pp.h"
#include "filter_model_converter.h"
#include "bit_blaster_model_converter.h"
+#include "ast_translation.h"
// incremental SAT solver.
class inc_sat_solver : public solver {
@@ -93,7 +94,25 @@ public:
}
virtual ~inc_sat_solver() {}
-
+
+ virtual solver* translate(ast_manager& dst_m, params_ref const& p) {
+ ast_translation tr(m, dst_m);
+ if (m_num_scopes > 0) {
+ throw default_exception("Cannot translate sat solver at non-base level");
+ }
+ inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p);
+ expr_ref fml(dst_m);
+ for (unsigned i = 0; i < m_fmls.size(); ++i) {
+ fml = tr(m_fmls[i].get());
+ result->m_fmls.push_back(fml);
+ }
+ for (unsigned i = 0; i < m_asmsf.size(); ++i) {
+ fml = tr(m_asmsf[i].get());
+ result->m_asmsf.push_back(fml);
+ }
+ return result;
+ }
+
virtual void set_progress_callback(progress_callback * callback) {}
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 6b3316809..39ccbdbb2 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -36,6 +36,7 @@ Revision History:
#include"smt_model_finder.h"
#include"model_pp.h"
#include"ast_smt2_pp.h"
+#include"ast_translation.h"
namespace smt {
@@ -98,38 +99,159 @@ namespace smt {
m_model_generator->set_context(this);
}
+ literal context::translate_literal(
+ literal lit, context& src_ctx, context& dst_ctx,
+ vector b2v, ast_translation& tr) {
+ ast_manager& dst_m = dst_ctx.get_manager();
+ ast_manager& src_m = src_ctx.get_manager();
+ expr_ref dst_f(dst_m);
+
+ SASSERT(lit != false_literal && lit != true_literal);
+ bool_var v = b2v.get(lit.var(), null_bool_var);
+ if (v == null_bool_var) {
+ expr* e = src_ctx.m_bool_var2expr.get(lit.var(), 0);
+ SASSERT(e);
+ dst_f = tr(e);
+ v = dst_ctx.get_bool_var_of_id_option(dst_f->get_id());
+ if (v != null_bool_var) {
+ }
+ else if (src_m.is_not(e) || src_m.is_and(e) || src_m.is_or(e) ||
+ src_m.is_iff(e) || src_m.is_ite(e)) {
+ v = dst_ctx.mk_bool_var(dst_f);
+ }
+ else {
+ dst_ctx.internalize_formula(dst_f, false);
+ v = dst_ctx.get_bool_var(dst_f);
+ }
+ b2v.setx(lit.var(), v, null_bool_var);
+ }
+ return literal(v, lit.sign());
+ }
+
+
+ void context::copy(context& src_ctx, context& dst_ctx) {
+ ast_manager& dst_m = dst_ctx.get_manager();
+ ast_manager& src_m = src_ctx.get_manager();
+ src_ctx.pop_to_base_lvl();
+
+ if (src_ctx.m_base_lvl > 0) {
+ throw default_exception("Cloning contexts within a user-scope is not allowed");
+ }
+ SASSERT(src_ctx.m_base_lvl == 0);
+
+ ast_translation tr(src_m, dst_m, false);
+
+ dst_ctx.set_logic(src_ctx.m_setup.get_logic());
+ dst_ctx.copy_plugins(src_ctx, dst_ctx);
+
+ asserted_formulas& src_af = src_ctx.m_asserted_formulas;
+ asserted_formulas& dst_af = dst_ctx.m_asserted_formulas;
+
+ // Copy asserted formulas.
+ for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) {
+ expr_ref fml(dst_m);
+ proof_ref pr(dst_m);
+ proof* pr_src = src_af.get_formula_proof(i);
+ fml = tr(src_af.get_formula(i));
+ if (pr_src) {
+ pr = tr(pr_src);
+ }
+ dst_af.assert_expr(fml, pr);
+ }
+
+ if (!src_ctx.m_setup.already_configured()) {
+ return;
+ }
+ dst_ctx.setup_context(dst_ctx.m_fparams.m_auto_config);
+ dst_ctx.internalize_assertions();
+
+ vector b2v;
+
+#define TRANSLATE(_lit) translate_literal(_lit, src_ctx, dst_ctx, b2v, tr)
+
+ for (unsigned i = 0; i < src_ctx.m_assigned_literals.size(); ++i) {
+ literal lit;
+ lit = TRANSLATE(src_ctx.m_assigned_literals[i]);
+ dst_ctx.mk_clause(1, &lit, 0, CLS_AUX, 0);
+ }
+#if 0
+ literal_vector lits;
+ expr_ref_vector cls(src_m);
+ for (unsigned i = 0; i < src_ctx.m_lemmas.size(); ++i) {
+ lits.reset();
+ cls.reset();
+ clause& src_cls = *src_ctx.m_lemmas[i];
+ unsigned sz = src_cls.get_num_literals();
+ for (unsigned j = 0; j < sz; ++j) {
+ literal lit = TRANSLATE(src_cls.get_literal(j));
+ lits.push_back(lit);
+ }
+ dst_ctx.mk_clause(lits.size(), lits.c_ptr(), 0, src_cls.get_kind(), 0);
+ }
+ vector::const_iterator it = src_ctx.m_watches.begin();
+ vector::const_iterator end = src_ctx.m_watches.end();
+ literal ls[2];
+ for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
+ literal l1 = to_literal(l_idx);
+ literal neg_l1 = ~l1;
+ watch_list const & wl = *it;
+ literal const * it2 = wl.begin_literals();
+ literal const * end2 = wl.end_literals();
+ for (; it2 != end2; ++it2) {
+ literal l2 = *it2;
+ if (l1.index() < l2.index()) {
+ ls[0] = TRANSLATE(neg_l1);
+ ls[1] = TRANSLATE(l2);
+ dst_ctx.mk_clause(2, ls, 0, CLS_AUX, 0);
+ }
+ }
+ }
+#endif
+
+ TRACE("smt_context",
+ src_ctx.display(tout);
+ dst_ctx.display(tout););
+ }
+
+
context::~context() {
flush();
}
+ void context::copy_plugins(context& src, context& dst) {
+
+ // copy missing simplifier_plugins
+ // remark: some simplifier_plugins are automatically created by the asserted_formulas class.
+ simplifier & src_s = src.get_simplifier();
+ simplifier & dst_s = dst.get_simplifier();
+ ptr_vector::const_iterator it1 = src_s.begin_plugins();
+ ptr_vector::const_iterator end1 = src_s.end_plugins();
+ for (; it1 != end1; ++it1) {
+ simplifier_plugin * p = *it1;
+ if (dst_s.get_plugin(p->get_family_id()) == 0) {
+ dst.register_plugin(p->mk_fresh());
+ }
+ SASSERT(dst_s.get_plugin(p->get_family_id()) != 0);
+ }
+
+ // copy theory plugins
+ ptr_vector::iterator it2 = src.m_theory_set.begin();
+ ptr_vector::iterator end2 = src.m_theory_set.end();
+ for (; it2 != end2; ++it2) {
+ theory * new_th = (*it2)->mk_fresh(&dst);
+ dst.register_plugin(new_th);
+ }
+ }
+
context * context::mk_fresh(symbol const * l, smt_params * p) {
context * new_ctx = alloc(context, m_manager, p == 0 ? m_fparams : *p);
new_ctx->set_logic(l == 0 ? m_setup.get_logic() : *l);
- // copy missing simplifier_plugins
- // remark: some simplifier_plugins are automatically created by the asserted_formulas class.
- simplifier & s = get_simplifier();
- simplifier & new_s = new_ctx->get_simplifier();
- ptr_vector::const_iterator it1 = s.begin_plugins();
- ptr_vector::const_iterator end1 = s.end_plugins();
- for (; it1 != end1; ++it1) {
- simplifier_plugin * p = *it1;
- if (new_s.get_plugin(p->get_family_id()) == 0) {
- new_ctx->register_plugin(p->mk_fresh());
- }
- SASSERT(new_s.get_plugin(p->get_family_id()) != 0);
- }
-
- // copy theory plugins
- ptr_vector::iterator it2 = m_theory_set.begin();
- ptr_vector::iterator end2 = m_theory_set.end();
- for (; it2 != end2; ++it2) {
- theory * new_th = (*it2)->mk_fresh(new_ctx);
- new_ctx->register_plugin(new_th);
- }
- new_ctx->m_setup.mark_already_configured();
+ copy_plugins(*this, *new_ctx);
return new_ctx;
}
+
+
void context::init() {
app * t = m_manager.mk_true();
mk_bool_var(t);
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 040054d39..08d68c723 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1326,9 +1326,18 @@ namespace smt {
// -----------------------------------
void assert_expr_core(expr * e, proof * pr);
+ // copy plugins into a fresh context.
+ void copy_plugins(context& src, context& dst);
+
+ static literal translate_literal(
+ literal lit, context& src_ctx, context& dst_ctx,
+ vector b2v, ast_translation& tr);
+
+
public:
context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref());
+
virtual ~context();
/**
@@ -1340,6 +1349,12 @@ namespace smt {
*/
context * mk_fresh(symbol const * l = 0, smt_params * p = 0);
+ static void copy(context& src, context& dst);
+
+ /**
+ \brief Translate context to use new manager m.
+ */
+
app * mk_eq_atom(expr * lhs, expr * rhs);
bool set_logic(symbol logic) { return m_setup.set_logic(logic); }
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index a4e97380b..de0f91d97 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -32,6 +32,10 @@ namespace smt {
m_params(p) {
}
+ static void copy(imp& src, imp& dst) {
+ context::copy(src.m_kernel, dst.m_kernel);
+ }
+
smt_params & fparams() {
return m_kernel.get_fparams();
}
@@ -193,6 +197,11 @@ namespace smt {
return m_imp->m();
}
+ void kernel::copy(kernel& src, kernel& dst) {
+ imp::copy(*src.m_imp, *dst.m_imp);
+ }
+
+
bool kernel::set_logic(symbol logic) {
return m_imp->set_logic(logic);
}
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index 5c02cf96f..a7a467964 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -50,6 +50,8 @@ namespace smt {
~kernel();
+ static void copy(kernel& src, kernel& dst);
+
ast_manager & m() const;
/**
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 1fbb58847..5104291e8 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -37,6 +37,12 @@ namespace smt {
if (m_logic != symbol::null)
m_context.set_logic(m_logic);
}
+
+ virtual solver* translate(ast_manager& m, params_ref const& p) {
+ solver* result = alloc(solver, m, p, m_logic);
+ smt::kernel::copy(m_context, result->m_context);
+ return result;
+ }
virtual ~solver() {
}
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 5af436919..1e0c7c5f4 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -1029,7 +1029,7 @@ namespace smt {
theory_arith(ast_manager & m, theory_arith_params & params);
virtual ~theory_arith();
- virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_arith, get_manager(), m_params); }
+ virtual theory * mk_fresh(context * new_ctx);
virtual void setup();
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 6ae146b1b..96fe2d1f8 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1538,6 +1538,11 @@ namespace smt {
theory_arith::~theory_arith() {
}
+ template
+ theory* theory_arith::mk_fresh(context* new_ctx) {
+ return alloc(theory_arith, new_ctx->get_manager(), m_params);
+ }
+
template
void theory_arith::setup() {
m_random.set_seed(m_params.m_arith_random_seed);
diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h
index ac9e0befa..9cc833d31 100644
--- a/src/smt/theory_array.h
+++ b/src/smt/theory_array.h
@@ -98,7 +98,7 @@ namespace smt {
theory_array(ast_manager & m, theory_array_params & params);
virtual ~theory_array();
- virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, get_manager(), m_params); }
+ virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, new_ctx->get_manager(), m_params); }
virtual char const * get_name() const { return "array"; }
diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h
index 870f56739..730c325dc 100644
--- a/src/smt/theory_array_full.h
+++ b/src/smt/theory_array_full.h
@@ -91,7 +91,7 @@ namespace smt {
theory_array_full(ast_manager & m, theory_array_params & params);
virtual ~theory_array_full();
- virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array_full, get_manager(), m_params); }
+ virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array_full, new_ctx->get_manager(), m_params); }
virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var);
virtual void display_var(std::ostream & out, theory_var v) const;
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index dcf06e1e5..e381e81c1 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1312,6 +1312,11 @@ namespace smt {
theory_bv::~theory_bv() {
}
+
+ theory* theory_bv::mk_fresh(context* new_ctx) {
+ return alloc(theory_bv, new_ctx->get_manager(), m_params, m_bb.get_params());
+ }
+
void theory_bv::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
TRACE("bv", tout << "merging: #" << get_enode(v1)->get_owner_id() << " #" << get_enode(v2)->get_owner_id() << "\n";);
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index 414474a89..bb0dcc907 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -253,7 +253,7 @@ namespace smt {
theory_bv(ast_manager & m, theory_bv_params const & params, bit_blaster_params const & bb_params);
virtual ~theory_bv();
- virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_bv, get_manager(), m_params, m_bb.get_params()); }
+ virtual theory * mk_fresh(context * new_ctx);
virtual char const * get_name() const { return "bit-vector"; }
diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h
index 0426613a4..99511665f 100644
--- a/src/smt/theory_datatype.h
+++ b/src/smt/theory_datatype.h
@@ -101,7 +101,7 @@ namespace smt {
public:
theory_datatype(ast_manager & m, theory_datatype_params & p);
virtual ~theory_datatype();
- virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_datatype, get_manager(), m_params); }
+ virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_datatype, new_ctx->get_manager(), m_params); }
virtual void display(std::ostream & out) const;
virtual void collect_statistics(::statistics & st) const;
virtual void init_model(model_generator & m);
diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h
index b1d1cb632..cc739c8bc 100644
--- a/src/smt/theory_dense_diff_logic.h
+++ b/src/smt/theory_dense_diff_logic.h
@@ -282,7 +282,7 @@ namespace smt {
theory_dense_diff_logic(ast_manager & m, theory_arith_params & p);
virtual ~theory_dense_diff_logic() { reset_eh(); }
- virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_dense_diff_logic, get_manager(), m_params); }
+ virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_dense_diff_logic, new_ctx->get_manager(), m_params); }
virtual char const * get_name() const { return "difference-logic"; }
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index ed96d050e..84735a411 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -243,7 +243,7 @@ namespace smt {
reset_eh();
}
- virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_diff_logic, get_manager(), m_params); }
+ virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_diff_logic, new_ctx->get_manager(), m_params); }
virtual char const * get_name() const { return "difference-logic"; }
diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp
index 3c80a5ef2..ac64db74c 100644
--- a/src/smt/theory_dl.cpp
+++ b/src/smt/theory_dl.cpp
@@ -155,7 +155,7 @@ namespace smt {
}
virtual theory * mk_fresh(context * new_ctx) {
- return alloc(theory_dl, get_manager());
+ return alloc(theory_dl, new_ctx->get_manager());
}
virtual void init_model(smt::model_generator & m) {
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index 990701c4a..a62c35cd2 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -158,7 +158,7 @@ namespace smt {
virtual void push_scope_eh();
virtual void pop_scope_eh(unsigned num_scopes);
virtual void reset_eh();
- virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); }
+ virtual theory* mk_fresh(context* new_ctx) { return alloc(theory_fpa, new_ctx->get_manager()); }
virtual char const * get_name() const { return "fpa"; }
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h
index c176d2fd1..60350017f 100644
--- a/src/smt/theory_seq_empty.h
+++ b/src/smt/theory_seq_empty.h
@@ -29,7 +29,7 @@ namespace smt {
virtual bool internalize_term(app*) { return internalize_atom(0,false); }
virtual void new_eq_eh(theory_var, theory_var) { }
virtual void new_diseq_eh(theory_var, theory_var) {}
- virtual theory* mk_fresh(context*) { return alloc(theory_seq_empty, get_manager()); }
+ virtual theory* mk_fresh(context* new_ctx) { return alloc(theory_seq_empty, new_ctx->get_manager()); }
virtual char const * get_name() const { return "seq-empty"; }
public:
theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index 8568238fa..daba28045 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -183,7 +183,7 @@ namespace smt {
virtual ~theory_utvpi();
- virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_utvpi, get_manager()); }
+ virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_utvpi, new_ctx->get_manager()); }
virtual char const * get_name() const { return "utvpi-logic"; }
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 649a79be2..85f84e26e 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -127,6 +127,17 @@ public:
m_use_solver1_results = true;
}
+ solver* translate(ast_manager& m, params_ref const& p) {
+ solver* s1 = m_solver1->translate(m, p);
+ solver* s2 = m_solver2->translate(m, p);
+ combined_solver* r = alloc(combined_solver, s1, s2, p);
+ r->m_solver2_initialized = m_solver2_initialized;
+ r->m_inc_mode = m_inc_mode;
+ r->m_check_sat_executed = m_check_sat_executed;
+ r->m_use_solver1_results = m_use_solver1_results;
+ return r;
+ }
+
virtual void updt_params(params_ref const & p) {
m_solver1->updt_params(p);
m_solver2->updt_params(p);
diff --git a/src/solver/solver.h b/src/solver/solver.h
index 63592ea3b..8b5e98433 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -46,6 +46,12 @@ public:
class solver : public check_sat_result {
public:
virtual ~solver() {}
+
+ /**
+ \brief Creates a clone of the solver.
+ */
+ virtual solver* translate(ast_manager& m, params_ref const& p) = 0;
+
/**
\brief Update the solver internal settings.
*/
@@ -135,6 +141,8 @@ public:
*/
virtual expr * get_assumption(unsigned idx) const = 0;
+
+
/**
\brief Display the content of this solver.
*/
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index d7dc3ad37..02b9bd347 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -22,6 +22,7 @@ Notes:
#include"solver_na2as.h"
#include"tactic.h"
#include"ast_pp_util.h"
+#include"ast_translation.h"
/**
\brief Simulates the incremental solver interface using a tactic.
@@ -45,6 +46,8 @@ public:
tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic);
virtual ~tactic2solver();
+ virtual solver* translate(ast_manager& m, params_ref const& p);
+
virtual void updt_params(params_ref const & p);
virtual void collect_param_descrs(param_descrs & r);
@@ -183,6 +186,22 @@ void tactic2solver::set_cancel(bool f) {
}
}
+solver* tactic2solver::translate(ast_manager& m, params_ref const& p) {
+ tactic* t = m_tactic->translate(m);
+ tactic2solver* r = alloc(tactic2solver, m, t, p, m_produce_proofs, m_produce_models, m_produce_unsat_cores, m_logic);
+ r->m_result = 0;
+ if (!m_scopes.empty()) {
+ throw default_exception("translation of contexts is only supported at base level");
+ }
+ ast_translation tr(m_assertions.get_manager(), m, false);
+
+ for (unsigned i = 0; i < get_num_assertions(); ++i) {
+ r->m_assertions.push_back(tr(get_assertion(i)));
+ }
+ return r;
+}
+
+
void tactic2solver::collect_statistics(statistics & st) const {
st.copy(m_stats);
//SASSERT(m_stats.size() > 0);