mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

working on Forking/Serializing a z3 Solver #209

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-06 17:29:24 -08:00
parent 7b72486644
commit b4cb51cdb3
31 changed files with 241 additions and 96 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/api/api_solver.cpp
View file

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

4
src/api/c++/z3++.h
View file

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

13
src/api/python/z3.py
View file

@ -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.

8
src/api/z3_api.h
View file

@ -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.

1
src/ast/array_decl_plugin.cpp
View file

@ -519,6 +519,7 @@ void array_decl_plugin::get_op_names(svector<builtin_name>& 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));
}
}

1
src/ast/ast_translation.cpp
View file

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

4
src/ast/ast_translation.h
View file

@ -58,9 +58,9 @@ public:
template<typename T>
T * operator()(T const * n) {
SASSERT(from().contains(const_cast<T*>(n)));
SASSERT(!n || from().contains(const_cast<T*>(n)));
ast * r = process(n);
SASSERT(to().contains(const_cast<ast*>(r)));
SASSERT((!n && !r) || to().contains(const_cast<ast*>(r)));
return static_cast<T*>(r);
}

5
src/opt/opt_solver.cpp
View file

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

1
src/opt/opt_solver.h
View file

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

7
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -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) {

187
src/smt/smt_context.cpp
View file

@ -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<bool_var> 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<watch_list>::const_iterator it = src_ctx.m_watches.begin();
vector<watch_list>::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();

5
src/smt/smt_context.h
View file

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

9
src/smt/smt_kernel.cpp
View file

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

3
src/smt/smt_kernel.h
View file

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

6
src/smt/smt_solver.cpp
View file

@ -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() {
}

2
src/smt/theory_arith.h
View file

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

5
src/smt/theory_arith_core.h
View file

@ -1544,6 +1544,11 @@ namespace smt {
theory_arith<Ext>::~theory_arith() {
}
template<typename Ext>
theory* theory_arith<Ext>::mk_fresh(context* new_ctx) {
return alloc(theory_arith<Ext>, new_ctx->get_manager(), m_params);
}
template<typename Ext>
void theory_arith<Ext>::setup() {
m_random.set_seed(m_params.m_arith_random_seed);

2
src/smt/theory_array.h
View file

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

2
src/smt/theory_array_full.h
View file

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

5
src/smt/theory_bv.cpp
View file

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

2
src/smt/theory_bv.h
View file

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

2
src/smt/theory_datatype.h
View file

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

2
src/smt/theory_dense_diff_logic.h
View file

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

2
src/smt/theory_diff_logic.h
View file

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

2
src/smt/theory_dl.cpp
View file

@ -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) {

2
src/smt/theory_fpa.h
View file

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

2
src/smt/theory_seq_empty.h
View file

@ -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) {}

2
src/smt/theory_utvpi.h
View file

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

11
src/solver/combined_solver.cpp
View file

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

8
src/solver/solver.h
View file

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

19
src/solver/tactic2solver.cpp
View file

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