From 4b1a730f4612bc8d123ddf1a2000e1dd05ca81a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Oct 2015 12:47:16 -0700 Subject: [PATCH 1/6] API method for translating context Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 605d23876..be496f6bf 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1338,6 +1338,11 @@ namespace smt { */ context * mk_fresh(symbol const * l = 0, smt_params * p = 0); + /** + \brief Translate context to use new manager m. + */ + context * translate(ast_manager& m); + app * mk_eq_atom(expr * lhs, expr * rhs); bool set_logic(symbol logic) { return m_setup.set_logic(logic); } From 9acaa49a05787597abc1d75e626f0f0a17db2a13 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Oct 2015 14:28:21 -0700 Subject: [PATCH 2/6] adding translation routine to context to address enhancement request #209 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 116 ++++++++++++++++++++++++++++++++++------ src/smt/smt_context.h | 4 ++ 2 files changed, 105 insertions(+), 15 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 43757b432..bd1bfc52d 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 { @@ -102,34 +103,119 @@ namespace smt { flush(); } - 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); + 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 & 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(); + 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 (new_s.get_plugin(p->get_family_id()) == 0) { - new_ctx->register_plugin(p->mk_fresh()); + if (dst_s.get_plugin(p->get_family_id()) == 0) { + dst.register_plugin(p->mk_fresh()); } - SASSERT(new_s.get_plugin(p->get_family_id()) != 0); + SASSERT(dst_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(); + 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(new_ctx); - new_ctx->register_plugin(new_th); + theory * new_th = (*it2)->mk_fresh(&dst); + dst.register_plugin(new_th); } - new_ctx->m_setup.mark_already_configured(); + dst.m_setup.mark_already_configured(); + } + + 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_plugins(*this, *new_ctx); return new_ctx; } + context* context::translate(ast_manager& m) { + pop_to_base_lvl(); + + if (m_base_lvl > 0) { + throw default_exception("Cloning contexts within a user-scope is not allowed"); + } + reduce_assertions(); + + context * new_ctx = alloc(context, m, m_fparams); + ast_manager& dst_m = new_ctx->get_manager(); + new_ctx->set_logic(m_setup.get_logic()); + copy_plugins(*this, *new_ctx); + + asserted_formulas& src_af = m_asserted_formulas; + asserted_formulas& dst_af = new_ctx->m_asserted_formulas; + + SASSERT(m_base_lvl == 0); // please don't clone me + SASSERT(src_af.get_qhead() == src_af.get_num_formulas()); // should be the same. + + // Copy asserted formulas. + for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) { + expr_ref fml(dst_m), pr(dst_m); + fml = ::translate(src_af.get_formula(i), get_manager(), dst_m); + pr = ::translate(src_af.get_formula_proof(i), get_manager(), dst_m); + dst_af.assert_expr(fml, to_app(pr)); + } + dst_af.reduce(); + for (unsigned i = 0; i < dst_af.get_num_formulas(); ++i) { + expr* f = dst_af.get_formula(i); + proof* pr = dst_af.get_formula_proof(i); + new_ctx->internalize_assertion(f, pr, 0); + } + + // Copy learned lemmas, but internalize them as axioms. + // ignore jusification. + for (unsigned i = 0; i < m_lemmas.size(); ++i) { + expr_ref_vector new_clause(dst_m); + clause& src_cls = *m_lemmas[i]; + unsigned sz = src_cls.get_num_literals(); + bool internalized = true; + for (unsigned j = 0; internalized && j < sz; ++j) { + literal src_lit = src_cls.get_literal(j); + expr_ref r = translate(src_lit, *new_ctx); + internalized = r != 0; + new_clause.push_back(r); + } + if (internalized) { + app_ref cls(dst_m); + cls = dst_m.mk_or(new_clause.size(), new_clause.c_ptr()); + new_ctx->internalize_assertion(cls, 0, 0); + } + else { + TRACE("smt_context", display_clause_detail(tout << "Clause not interalized\n", &src_cls);); + } + } + + return new_ctx; + } + + + expr_ref context::translate(literal lit, context& dst) { + ast_manager& m = dst.get_manager(); + expr_ref result(m); + expr * e; + if (lit == true_literal) { + result = m.mk_true(); + } + else if (lit == false_literal) { + result = m.mk_false(); + } + else if (e = m_bool_var2expr.get(lit.var(), 0)) { + result = ::translate(e, m_manager, m); + if (lit.sign()) { + result = dst.get_manager().mk_not(result); + } + } + return result; + } + + 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 be496f6bf..ed1968a11 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1324,6 +1324,10 @@ namespace smt { // ----------------------------------- void assert_expr_core(expr * e, proof * pr); + // copy plugins into a fresh context. + void copy_plugins(context& src, context& dst); + expr_ref translate(literal lit, context& dst); + public: context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); From 32f3bd17fb5ef7e7195d69351baf48b0a6466c08 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Oct 2015 14:30:54 -0700 Subject: [PATCH 3/6] adding translation routine to context to address enhancement request #209 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index bd1bfc52d..6149dc671 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -152,7 +152,7 @@ namespace smt { asserted_formulas& src_af = m_asserted_formulas; asserted_formulas& dst_af = new_ctx->m_asserted_formulas; - SASSERT(m_base_lvl == 0); // please don't clone me + SASSERT(m_base_lvl == 0); SASSERT(src_af.get_qhead() == src_af.get_num_formulas()); // should be the same. // Copy asserted formulas. @@ -209,7 +209,7 @@ namespace smt { else if (e = m_bool_var2expr.get(lit.var(), 0)) { result = ::translate(e, m_manager, m); if (lit.sign()) { - result = dst.get_manager().mk_not(result); + result = m.mk_not(result); } } return result; From b4cb51cdb3248a5c98285d867083376b7c041eba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Nov 2015 17:29:24 -0800 Subject: [PATCH 4/6] working on Forking/Serializing a z3 Solver #209 Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 13 ++ src/api/c++/z3++.h | 4 + src/api/python/z3.py | 13 ++ src/api/z3_api.h | 8 ++ src/ast/array_decl_plugin.cpp | 1 + src/ast/ast_translation.cpp | 1 + src/ast/ast_translation.h | 4 +- src/opt/opt_solver.cpp | 5 + src/opt/opt_solver.h | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 7 +- src/smt/smt_context.cpp | 187 +++++++++++++++----------- src/smt/smt_context.h | 5 +- src/smt/smt_kernel.cpp | 9 ++ src/smt/smt_kernel.h | 3 + src/smt/smt_solver.cpp | 6 + src/smt/theory_arith.h | 2 +- src/smt/theory_arith_core.h | 5 + src/smt/theory_array.h | 2 +- src/smt/theory_array_full.h | 2 +- src/smt/theory_bv.cpp | 5 + src/smt/theory_bv.h | 2 +- src/smt/theory_datatype.h | 2 +- src/smt/theory_dense_diff_logic.h | 2 +- src/smt/theory_diff_logic.h | 2 +- src/smt/theory_dl.cpp | 2 +- src/smt/theory_fpa.h | 2 +- src/smt/theory_seq_empty.h | 2 +- src/smt/theory_utvpi.h | 2 +- src/solver/combined_solver.cpp | 11 ++ src/solver/solver.h | 8 ++ src/solver/tactic2solver.cpp | 19 +++ 31 files changed, 241 insertions(+), 96 deletions(-) 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/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..4f3e1f7db 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -93,7 +93,12 @@ public: } virtual ~inc_sat_solver() {} - + + virtual solver* translate(ast_manager& m, params_ref const& p) { + UNREACHABLE(); + return 0; + } + 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 6149dc671..b75aea2ca 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -99,6 +99,112 @@ namespace smt { m_model_generator->set_context(this); } + 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; + expr_ref dst_f(dst_m); + +#define TRANSLATE(_lin, _lout) { \ + SASSERT(_lin != false_literal && _lin != true_literal); \ + bool_var v = b2v.get(_lin.var(), null_bool_var); \ + if (v == null_bool_var) { \ + expr* e = src_ctx.m_bool_var2expr.get(_lin.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(_lin.var(), v, null_bool_var); \ + } \ + _lout = literal(v, _lin.sign()); \ + } \ + + for (unsigned i = 0; i < src_ctx.m_assigned_literals.size(); ++i) { + literal lit; + TRANSLATE(src_ctx.m_assigned_literals[i], lit); + dst_ctx.mk_clause(1, &lit, 0, CLS_AUX, 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 = src_cls.get_literal(j), lout; + TRANSLATE(lit, lout); + lits.push_back(lout); + } + 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()) { + TRANSLATE(neg_l1, ls[0]); + TRANSLATE(l2, ls[1]); + dst_ctx.mk_clause(2, ls, 0, CLS_AUX, 0); + } + } + } + + TRACE("smt_context", + src_ctx.display(tout); + dst_ctx.display(tout);); + } + + context::~context() { flush(); } @@ -126,7 +232,6 @@ namespace smt { theory * new_th = (*it2)->mk_fresh(&dst); dst.register_plugin(new_th); } - dst.m_setup.mark_already_configured(); } context * context::mk_fresh(symbol const * l, smt_params * p) { @@ -136,85 +241,7 @@ namespace smt { return new_ctx; } - context* context::translate(ast_manager& m) { - pop_to_base_lvl(); - - if (m_base_lvl > 0) { - throw default_exception("Cloning contexts within a user-scope is not allowed"); - } - reduce_assertions(); - - context * new_ctx = alloc(context, m, m_fparams); - ast_manager& dst_m = new_ctx->get_manager(); - new_ctx->set_logic(m_setup.get_logic()); - copy_plugins(*this, *new_ctx); - - asserted_formulas& src_af = m_asserted_formulas; - asserted_formulas& dst_af = new_ctx->m_asserted_formulas; - - SASSERT(m_base_lvl == 0); - SASSERT(src_af.get_qhead() == src_af.get_num_formulas()); // should be the same. - - // Copy asserted formulas. - for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) { - expr_ref fml(dst_m), pr(dst_m); - fml = ::translate(src_af.get_formula(i), get_manager(), dst_m); - pr = ::translate(src_af.get_formula_proof(i), get_manager(), dst_m); - dst_af.assert_expr(fml, to_app(pr)); - } - dst_af.reduce(); - for (unsigned i = 0; i < dst_af.get_num_formulas(); ++i) { - expr* f = dst_af.get_formula(i); - proof* pr = dst_af.get_formula_proof(i); - new_ctx->internalize_assertion(f, pr, 0); - } - - // Copy learned lemmas, but internalize them as axioms. - // ignore jusification. - for (unsigned i = 0; i < m_lemmas.size(); ++i) { - expr_ref_vector new_clause(dst_m); - clause& src_cls = *m_lemmas[i]; - unsigned sz = src_cls.get_num_literals(); - bool internalized = true; - for (unsigned j = 0; internalized && j < sz; ++j) { - literal src_lit = src_cls.get_literal(j); - expr_ref r = translate(src_lit, *new_ctx); - internalized = r != 0; - new_clause.push_back(r); - } - if (internalized) { - app_ref cls(dst_m); - cls = dst_m.mk_or(new_clause.size(), new_clause.c_ptr()); - new_ctx->internalize_assertion(cls, 0, 0); - } - else { - TRACE("smt_context", display_clause_detail(tout << "Clause not interalized\n", &src_cls);); - } - } - - return new_ctx; - } - - - expr_ref context::translate(literal lit, context& dst) { - ast_manager& m = dst.get_manager(); - expr_ref result(m); - expr * e; - if (lit == true_literal) { - result = m.mk_true(); - } - else if (lit == false_literal) { - result = m.mk_false(); - } - else if (e = m_bool_var2expr.get(lit.var(), 0)) { - result = ::translate(e, m_manager, m); - if (lit.sign()) { - result = m.mk_not(result); - } - } - return result; - } - + void context::init() { app * t = m_manager.mk_true(); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index ed1968a11..7f13efa9f 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1326,11 +1326,11 @@ namespace smt { // copy plugins into a fresh context. void copy_plugins(context& src, context& dst); - expr_ref translate(literal lit, context& dst); public: context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); + virtual ~context(); /** @@ -1342,10 +1342,11 @@ 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. */ - context * translate(ast_manager& m); app * mk_eq_atom(expr * lhs, expr * rhs); 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..b2d880532 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -45,11 +45,14 @@ namespace smt { class kernel { struct imp; imp * m_imp; + kernel(): m_imp(0) {} public: kernel(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); ~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 9c391ca1a..661e7ab5b 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -1000,7 +1000,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 c47585606..8b2f9b780 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1544,6 +1544,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); From 1758799ef49403c7edf5c95d66ccfea9863057d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Nov 2015 10:00:14 -0800 Subject: [PATCH 5/6] add translate facility to inc_sat_solver. Limit lemma copying to unit lemmas Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 20 ++++++-- src/smt/smt_context.cpp | 67 +++++++++++++++------------ src/smt/smt_context.h | 5 ++ src/smt/smt_kernel.h | 1 - 4 files changed, 60 insertions(+), 33 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 4f3e1f7db..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 { @@ -94,9 +95,22 @@ public: virtual ~inc_sat_solver() {} - virtual solver* translate(ast_manager& m, params_ref const& p) { - UNREACHABLE(); - return 0; + 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) {} diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c55243cfd..39ccbdbb2 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -99,6 +99,36 @@ 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(); @@ -136,36 +166,15 @@ namespace smt { dst_ctx.internalize_assertions(); vector b2v; - expr_ref dst_f(dst_m); -#define TRANSLATE(_lin, _lout) { \ - SASSERT(_lin != false_literal && _lin != true_literal); \ - bool_var v = b2v.get(_lin.var(), null_bool_var); \ - if (v == null_bool_var) { \ - expr* e = src_ctx.m_bool_var2expr.get(_lin.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(_lin.var(), v, null_bool_var); \ - } \ - _lout = literal(v, _lin.sign()); \ - } \ +#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; - TRANSLATE(src_ctx.m_assigned_literals[i], 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) { @@ -174,9 +183,8 @@ namespace smt { clause& src_cls = *src_ctx.m_lemmas[i]; unsigned sz = src_cls.get_num_literals(); for (unsigned j = 0; j < sz; ++j) { - literal lit = src_cls.get_literal(j), lout; - TRANSLATE(lit, lout); - lits.push_back(lout); + 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); } @@ -192,12 +200,13 @@ namespace smt { for (; it2 != end2; ++it2) { literal l2 = *it2; if (l1.index() < l2.index()) { - TRANSLATE(neg_l1, ls[0]); - TRANSLATE(l2, ls[1]); + 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); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 8fb3504ad..08d68c723 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1329,6 +1329,11 @@ namespace smt { // 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()); diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index b2d880532..a7a467964 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -45,7 +45,6 @@ namespace smt { class kernel { struct imp; imp * m_imp; - kernel(): m_imp(0) {} public: kernel(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); From 13b19eb35120a59da2abd80112985174af031ea8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Nov 2015 10:10:21 -0800 Subject: [PATCH 6/6] add translate facility to Java/C# APIs, request #209 Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Solver.cs | 11 +++++++++++ src/api/java/Solver.java | 8 ++++++++ 2 files changed, 19 insertions(+) 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. *