From 4b1a730f4612bc8d123ddf1a2000e1dd05ca81a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Oct 2015 12:47:16 -0700 Subject: [PATCH 01/53] 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 02/53] 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 03/53] 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 04/53] 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 396875bedfea80c23eeb9cb21d68acd7d5332e91 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Nov 2015 22:56:53 -0800 Subject: [PATCH 05/53] fix compilation problem, issue #297 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_int.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index 30ae6feac..72e1f1bc2 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -210,7 +210,7 @@ namespace smt { TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";); context & ctx = get_context(); ctx.internalize(bound, true); - ctx.mark_as_relevant(bound); + ctx.mark_as_relevant(bound.get()); } From 1758799ef49403c7edf5c95d66ccfea9863057d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Nov 2015 10:00:14 -0800 Subject: [PATCH 06/53] 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 07/53] 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. * From 8d1fa3ae50428a5b947cfa71fe0f512c0afc256d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Nov 2015 11:50:06 -0800 Subject: [PATCH 08/53] move mk_fresh to inside files that include smt_context.h directly to address build problem reported in #297 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array_full.cpp | 4 ++++ src/smt/theory_array_full.h | 2 +- src/smt/theory_datatype.cpp | 5 +++++ src/smt/theory_datatype.h | 2 +- src/smt/theory_dense_diff_logic.h | 2 +- src/smt/theory_dense_diff_logic_def.h | 5 +++++ src/smt/theory_diff_logic.h | 2 +- src/smt/theory_diff_logic_def.h | 6 ++++++ src/smt/theory_fpa.cpp | 4 ++++ src/smt/theory_fpa.h | 2 +- src/smt/theory_utvpi.cpp | 2 +- src/smt/theory_utvpi.h | 2 +- src/smt/theory_utvpi_def.h | 4 ++++ 13 files changed, 35 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 91f5b68ec..013c3c188 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -35,6 +35,10 @@ namespace smt { m_var_data_full.reset(); } + theory* theory_array_full::mk_fresh(context* new_ctx) { + return alloc(theory_array_full, new_ctx->get_manager(), m_params); + } + void theory_array_full::add_map(theory_var v, enode* s) { if (m_params.m_array_cg && !s->is_cgr()) { return; diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h index 730c325dc..1200275a2 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, new_ctx->get_manager(), m_params); } + virtual theory * mk_fresh(context * new_ctx); 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_datatype.cpp b/src/smt/theory_datatype.cpp index a004da666..cf4658c7d 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -36,6 +36,11 @@ namespace smt { virtual theory_id get_from_theory() const { return null_theory_id; } }; + + theory* theory_datatype::mk_fresh(context* new_ctx) { + return alloc(theory_datatype, new_ctx->get_manager(), m_params); + } + /** \brief Assert the axiom (antecedent => lhs = rhs) antecedent may be null_literal diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 99511665f..77b1ffc7c 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, new_ctx->get_manager(), m_params); } + virtual theory * mk_fresh(context * new_ctx); 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 cc739c8bc..1b1653eb7 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, new_ctx->get_manager(), m_params); } + virtual theory * mk_fresh(context * new_ctx); virtual char const * get_name() const { return "difference-logic"; } diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 4c35647e8..7702a1ef2 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -39,6 +39,11 @@ namespace smt { m_edges.push_back(edge()); } + template + theory* theory_dense_diff_logic::mk_fresh(context * new_ctx) { + return alloc(theory_dense_diff_logic, new_ctx->get_manager(), m_params); + } + template inline app * theory_dense_diff_logic::mk_zero_for(expr * n) { return m_autil.mk_numeral(rational(0), get_manager().get_sort(n)); diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 84735a411..390bd271d 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, new_ctx->get_manager(), m_params); } + virtual theory * mk_fresh(context * new_ctx); virtual char const * get_name() const { return "difference-logic"; } diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index c791668c3..f444fe88e 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -1384,5 +1384,11 @@ bool theory_diff_logic::internalize_objective(expr * n, rational const& m, return true; } +template +theory* theory_diff_logic::mk_fresh(context* new_ctx) { + return alloc(theory_diff_logic, new_ctx->get_manager(), m_params); +} + + #endif /* THEORY_DIFF_LOGIC_DEF_H_ */ diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 66a1a6321..8b031ff27 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -716,6 +716,10 @@ namespace smt { return; } + theory* theory_fpa::mk_fresh(context* new_ctx) { + return alloc(theory_fpa, new_ctx->get_manager()); + } + void theory_fpa::push_scope_eh() { theory::push_scope_eh(); m_trail_stack.push_scope(); diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index a62c35cd2..9db6a88a9 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* new_ctx) { return alloc(theory_fpa, new_ctx->get_manager()); } + virtual theory* mk_fresh(context* new_ctx); 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_utvpi.cpp b/src/smt/theory_utvpi.cpp index c45cfe74a..9da82c9e6 100644 --- a/src/smt/theory_utvpi.cpp +++ b/src/smt/theory_utvpi.cpp @@ -156,5 +156,5 @@ namespace smt { return true; } - + } diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h index daba28045..35ebd440b 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, new_ctx->get_manager()); } + virtual theory * mk_fresh(context * new_ctx); virtual char const * get_name() const { return "utvpi-logic"; } diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index bca24406f..22b19b0b1 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -942,6 +942,10 @@ namespace smt { } } + template + theory* theory_utvpi::mk_fresh(context* new_ctx) { + return alloc(theory_utvpi, new_ctx->get_manager()); + } }; From 4685a5f8bac97dcb600761fc2844fd4fc6fb2221 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Nov 2015 16:42:13 -0800 Subject: [PATCH 09/53] add array-ext to externally exposed functions to enable interpolants with arrays to be usable in feedback loops with Z3. Addresses one issue raised in #292 Signed-off-by: Nikolaj Bjorner --- src/api/api_array.cpp | 3 ++- src/api/api_ast.cpp | 1 + src/api/dotnet/Context.cs | 16 ++++++++++++++++ src/api/java/Context.java | 11 +++++++++++ src/api/python/z3.py | 7 +++++++ src/api/python/z3printer.py | 2 +- src/api/z3_api.h | 15 +++++++++++++++ src/ast/array_decl_plugin.cpp | 13 ++++++++----- src/ast/array_decl_plugin.h | 4 ++-- src/smt/theory_array_base.cpp | 7 ++----- src/smt/theory_array_base.h | 2 +- src/smt/theory_array_full.cpp | 6 +++++- 12 files changed, 71 insertions(+), 16 deletions(-) diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp index de4d6f4e6..d3dda5d9d 100644 --- a/src/api/api_array.cpp +++ b/src/api/api_array.cpp @@ -187,7 +187,8 @@ extern "C" { MK_BINARY(Z3_mk_set_difference, mk_c(c)->get_array_fid(), OP_SET_DIFFERENCE, SKIP); MK_UNARY(Z3_mk_set_complement, mk_c(c)->get_array_fid(), OP_SET_COMPLEMENT, SKIP); MK_BINARY(Z3_mk_set_subset, mk_c(c)->get_array_fid(), OP_SET_SUBSET, SKIP); - + MK_BINARY(Z3_mk_array_ext, mk_c(c)->get_array_fid(), OP_ARRAY_EXT, SKIP); + Z3_ast Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set) { return Z3_mk_select(c, set, elem); } diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 15a9f5bae..200b483cf 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1012,6 +1012,7 @@ extern "C" { case OP_SET_COMPLEMENT: return Z3_OP_SET_COMPLEMENT; case OP_SET_SUBSET: return Z3_OP_SET_SUBSET; case OP_AS_ARRAY: return Z3_OP_AS_ARRAY; + case OP_ARRAY_EXT: return Z3_OP_ARRAY_EXT; default: UNREACHABLE(); return Z3_OP_UNINTERPRETED; diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index b179d44a5..25c399d68 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2122,6 +2122,21 @@ namespace Microsoft.Z3 CheckContextMatch(array); return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject)); } + + /// + /// Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt. + /// + public Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2) + { + Contract.Requires(arg1 != null); + Contract.Requires(arg2 != null); + Contract.Ensures(Contract.Result() != null); + + CheckContextMatch(arg1); + CheckContextMatch(arg2); + return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject)); + } + #endregion #region Sets @@ -2268,6 +2283,7 @@ namespace Microsoft.Z3 CheckContextMatch(arg2); return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject)); } + #endregion #region Pseudo-Boolean constraints diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 4497e6970..0f9a85799 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -1717,6 +1717,17 @@ public class Context extends IDisposable Native.mkArrayDefault(nCtx(), array.getNativeObject())); } + /** + * Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt. + **/ + public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2) + { + checkContextMatch(arg1); + checkContextMatch(arg2); + return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); + } + + /** * Create a set type. **/ diff --git a/src/api/python/z3.py b/src/api/python/z3.py index acee87f54..837443e07 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -4143,6 +4143,13 @@ def K(dom, v): v = _py2expr(v, ctx) return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx) +def Ext(a, b): + """Return extensionality index for arrays. + """ + if __debug__: + _z3_assert(is_array(a) and is_array(b)) + return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast())); + def is_select(a): """Return `True` if `a` is a Z3 array select application. diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py index e8a6b992f..5116046dd 100644 --- a/src/api/python/z3printer.py +++ b/src/api/python/z3printer.py @@ -31,7 +31,7 @@ _z3_op_to_str = { Z3_OP_BASHR : '>>', Z3_OP_BSHL : '<<', Z3_OP_BLSHR : 'LShR', Z3_OP_CONCAT : 'Concat', Z3_OP_EXTRACT : 'Extract', Z3_OP_BV2INT : 'BV2Int', Z3_OP_ARRAY_MAP : 'Map', Z3_OP_SELECT : 'Select', Z3_OP_STORE : 'Store', - Z3_OP_CONST_ARRAY : 'K', + Z3_OP_CONST_ARRAY : 'K', Z3_OP_ARRAY_EXT : 'Ext', Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe' } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9887cd7f0..927aad930 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -322,6 +322,9 @@ typedef enum - Z3_OP_AS_ARRAY An array value that behaves as the function graph of the function passed as parameter. + - Z3_OP_ARRAY_EXT Array extensionality function. It takes two arrays as arguments and produces an index, such that the arrays + are different if they are different on the index. + - Z3_OP_BNUM Bit-vector numeral. - Z3_OP_BIT1 One bit bit-vector. @@ -1033,6 +1036,7 @@ typedef enum { Z3_OP_SET_COMPLEMENT, Z3_OP_SET_SUBSET, Z3_OP_AS_ARRAY, + Z3_OP_ARRAY_EXT, // Bit-vectors Z3_OP_BNUM = 0x400, @@ -3260,6 +3264,17 @@ END_MLAPI_EXCLUDE Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2); /*@}*/ + /** + \brief Create array extensionality index given two arrays with the same sort. + The meaning is given by the axiom: + (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B)) + + def_API('Z3_mk_array_ext', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + + Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2); + /*@}*/ + /** @name Numerals */ diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 0e315c38d..49b1b18c5 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -293,7 +293,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) { func_decl_info(m_family_id, OP_STORE)); } -func_decl * array_decl_plugin::mk_array_ext_skolem(unsigned arity, sort * const * domain, unsigned i) { +func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domain, unsigned i) { if (arity != 2 || domain[0] != domain[1]) { UNREACHABLE(); return 0; @@ -306,7 +306,7 @@ func_decl * array_decl_plugin::mk_array_ext_skolem(unsigned arity, sort * const } sort * r = to_sort(s->get_parameter(i).get_ast()); parameter param(s); - return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, func_decl_info(m_family_id, OP_ARRAY_EXT_SKOLEM, 1, ¶m)); + return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, func_decl_info(m_family_id, OP_ARRAY_EXT, 1, ¶m)); } @@ -463,12 +463,15 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters func_decl * f = to_func_decl(parameters[0].get_ast()); return mk_map(f, arity, domain); } - case OP_ARRAY_EXT_SKOLEM: + case OP_ARRAY_EXT: + if (num_parameters == 0) { + return mk_array_ext(arity, domain, 0); + } if (num_parameters != 1 || !parameters[0].is_int()) { UNREACHABLE(); return 0; } - return mk_array_ext_skolem(arity, domain, parameters[0].get_int()); + return mk_array_ext(arity, domain, parameters[0].get_int()); case OP_ARRAY_DEFAULT: return mk_default(arity, domain); case OP_SET_UNION: @@ -519,7 +522,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)); + op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT)); } } diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 98fd563f0..778b94c33 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -42,7 +42,7 @@ enum array_op_kind { OP_STORE, OP_SELECT, OP_CONST_ARRAY, - OP_ARRAY_EXT_SKOLEM, + OP_ARRAY_EXT, OP_ARRAY_DEFAULT, OP_ARRAY_MAP, OP_SET_UNION, @@ -80,7 +80,7 @@ class array_decl_plugin : public decl_plugin { func_decl * mk_store(unsigned arity, sort * const * domain); - func_decl * mk_array_ext_skolem(unsigned arity, sort * const * domain, unsigned i); + func_decl * mk_array_ext(unsigned arity, sort * const * domain, unsigned i); func_decl * mk_set_union(unsigned arity, sort * const * domain); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 663816a7d..29e4438c4 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -220,7 +220,7 @@ namespace smt { for (unsigned i = 0; i < dimension; ++i) { sort * ext_sk_domain[2] = { s_array, s_array }; parameter p(i); - func_decl * ext_sk_decl = m.mk_func_decl(get_id(), OP_ARRAY_EXT_SKOLEM, 1, &p, 2, ext_sk_domain); + func_decl * ext_sk_decl = m.mk_func_decl(get_id(), OP_ARRAY_EXT, 1, &p, 2, ext_sk_domain); ext_skolems->push_back(ext_sk_decl); } m_sort2skolem.insert(s_array, ext_skolems); @@ -310,10 +310,7 @@ namespace smt { func_decl_ref_vector * funcs = 0; sort * s = m.get_sort(e1); - if (!m_sort2skolem.find(s, funcs)) { - UNREACHABLE(); - return; - } + VERIFY(m_sort2skolem.find(s, funcs)); unsigned dimension = funcs->size(); diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index 03d180f8c..46cd60fd6 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -36,7 +36,7 @@ namespace smt { bool is_select(app const* n) const { return n->is_app_of(get_id(), OP_SELECT); } bool is_default(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_DEFAULT); } bool is_const(app const* n) const { return n->is_app_of(get_id(), OP_CONST_ARRAY); } - bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT_SKOLEM); } + bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT); } bool is_as_array(app const * n) const { return n->is_app_of(get_id(), OP_AS_ARRAY); } bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); } bool is_array_sort(app const* n) const { return is_array_sort(get_manager().get_sort(n)); } diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 013c3c188..a9dc657dd 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -273,7 +273,7 @@ namespace smt { } context & ctx = get_context(); - if (is_map(n)) { + if (is_map(n) || is_array_ext(n)) { for (unsigned i = 0; i < n->get_num_args(); ++i) { enode* arg = ctx.get_enode(n->get_arg(i)); if (!is_attached_to_var(arg)) { @@ -320,6 +320,10 @@ namespace smt { found_unsupported_op(n); instantiate_default_as_array_axiom(node); } + else if (is_array_ext(n)) { + SASSERT(n->get_num_args() == 2); + instantiate_extensionality(ctx.get_enode(n->get_arg(0)), ctx.get_enode(n->get_arg(1))); + } return true; } From e9315af0d90f3918a6faa0d98dc3395f239e0a19 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Nov 2015 04:22:44 -0800 Subject: [PATCH 10/53] remove tabs from z3.py to fix build Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 837443e07..214d8b687 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -1,3 +1,4 @@ + ############################################ # Copyright (c) 2012 Microsoft Corporation # @@ -4147,7 +4148,7 @@ def Ext(a, b): """Return extensionality index for arrays. """ if __debug__: - _z3_assert(is_array(a) and is_array(b)) + _z3_assert(is_array(a) and is_array(b)) return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast())); def is_select(a): @@ -6096,12 +6097,12 @@ class Solver(Z3PPObject): >>> c1 = Context() >>> c2 = Context() - >>> s1 = Solver(ctx=c1) - >>> s2 = s1.translate(c2) + >>> 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()) + solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref()) return Solver(solver, target) def sexpr(self): From 4e05e93ecbadfae5cfa39b10313687c10a567c89 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 9 Nov 2015 11:52:44 +0000 Subject: [PATCH 11/53] Bugfix for FPA model generation/conversion. Addresses #300 --- src/smt/theory_fpa.cpp | 14 ++++++++++++-- src/tactic/fpa/fpa2bv_model_converter.cpp | 5 ++--- 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 8b031ff27..65a66cf80 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -716,8 +716,8 @@ namespace smt { return; } - theory* theory_fpa::mk_fresh(context* new_ctx) { - return alloc(theory_fpa, new_ctx->get_manager()); + theory* theory_fpa::mk_fresh(context* new_ctx) { + return alloc(theory_fpa, new_ctx->get_manager()); } void theory_fpa::push_scope_eh() { @@ -863,6 +863,16 @@ namespace smt { mk_ismt2_pp(a2, m) << " eq. cls. #" << get_enode(a2)->get_root()->get_owner()->get_id() << std::endl;); res = vp; } + else if (is_app_of(owner, get_family_id(), OP_FPA_INTERNAL_RM)) { + SASSERT(to_app(owner)->get_num_args() == 1); + app_ref a0(m); + a0 = to_app(owner->get_arg(0)); + fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this); + vp->add_dependency(ctx.get_enode(a0)); + TRACE("t_fpa_detail", tout << "Depends on: " << + mk_ismt2_pp(a0, m) << " eq. cls. #" << get_enode(a0)->get_root()->get_owner()->get_id() << std::endl;); + res = vp; + } else if (ctx.e_internalized(wrapped)) { if (m_fpa_util.is_rm(owner)) { fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this); diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 62ad363fd..fdbe54c4d 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -177,7 +177,6 @@ expr_ref fpa2bv_model_converter::convert_bv2rm(expr * eval_v) const { rational bv_val(0); unsigned sz = 0; - if (bu.is_numeral(eval_v, bv_val, sz)) { SASSERT(bv_val.is_uint64()); switch (bv_val.get_uint64()) { @@ -309,9 +308,9 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { expr * bvval = to_app(val)->get_arg(0); expr_ref fv(m); fv = convert_bv2rm(bv_mdl, var, bvval); - TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << std::endl;); + TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;); float_mdl->register_decl(var, fv); - seen.insert(to_app(val)->get_decl()); + seen.insert(to_app(bvval)->get_decl()); } for (obj_map::iterator it = m_uf2bvuf.begin(); From 6625f7a749dac7d2297336978515e0dbb954e9b2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 9 Nov 2015 13:19:10 +0000 Subject: [PATCH 12/53] Added Z3_solver_translate to ML API. --- src/api/ml/z3.ml | 7 +++++-- src/api/ml/z3.mli | 3 +++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 9de20e29f..7aa28b272 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -2740,10 +2740,13 @@ struct mk_solver ctx (Some (Symbol.mk_string ctx logic)) let mk_simple_solver ( ctx : context ) = - (create ctx (Z3native.mk_simple_solver (context_gno ctx))) + create ctx (Z3native.mk_simple_solver (context_gno ctx)) let mk_solver_t ( ctx : context ) ( t : Tactic.tactic ) = - (create ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t))) + create ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t)) + + let translate ( x : solver ) ( to_ctx : context ) = + create to_ctx (Z3native.solver_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) let to_string ( x : solver ) = Z3native.solver_to_string (z3obj_gnc x) (z3obj_gno x) end diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 32ca24128..83c7b66a7 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -3122,6 +3122,9 @@ sig The solver supports the commands [Push] and [Pop], but it will always solve each check from scratch. *) val mk_solver_t : context -> Tactic.tactic -> solver + + (** Create a clone of the current solver with respect to a context. *) + val translate : solver -> context -> solver (** A string representation of the solver. *) val to_string : solver -> string From cffff1837354b1aefd19403c1759b718bd597d14 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 9 Nov 2015 13:22:33 +0000 Subject: [PATCH 13/53] -whitespace --- src/api/ml/z3.mli | 180 +++++++++++++++++++++++----------------------- 1 file changed, 90 insertions(+), 90 deletions(-) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 83c7b66a7..e97313148 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -864,7 +864,7 @@ sig (** Access the array default value. Produces the default range value, for arrays that can be represented as - finite maps with a default range value. *) + finite maps with a default range value. *) val mk_term_array : context -> Expr.expr -> Expr.expr end @@ -1185,36 +1185,36 @@ sig val mk_const_s : context -> string -> Expr.expr (** Create an expression representing [t1 mod t2]. - The arguments must have int type. *) + The arguments must have int type. *) val mk_mod : context -> Expr.expr -> Expr.expr -> Expr.expr (** Create an expression representing [t1 rem t2]. - The arguments must have int type. *) + The arguments must have int type. *) val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr (** Create an integer numeral. *) val mk_numeral_s : context -> string -> Expr.expr (** Create an integer numeral. - @return A Term with the given value and sort Integer *) + @return A Term with the given value and sort Integer *) val mk_numeral_i : context -> int -> Expr.expr - (** Coerce an integer to a real. - - There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard. - - You can take the floor of a real by creating an auxiliary integer Term [k] and - and asserting [MakeInt2Real(k) <= t1 < MkInt2Real(k)+1]. - The argument must be of integer sort. *) + (** Coerce an integer to a real. + + There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard. + + You can take the floor of a real by creating an auxiliary integer Term [k] and + and asserting [MakeInt2Real(k) <= t1 < MkInt2Real(k)+1]. + The argument must be of integer sort. *) val mk_int2real : context -> Expr.expr -> Expr.expr (** Create an n-bit bit-vector from an integer argument. - - NB. This function is essentially treated as uninterpreted. - So you cannot expect Z3 to precisely reflect the semantics of this function - when solving constraints with this function. - - The argument must be of integer sort. *) + + NB. This function is essentially treated as uninterpreted. + So you cannot expect Z3 to precisely reflect the semantics of this function + when solving constraints with this function. + + The argument must be of integer sort. *) val mk_int2bv : context -> int -> Expr.expr -> Expr.expr end @@ -1234,7 +1234,7 @@ sig val get_ratio : Expr.expr -> Ratio.ratio (** Returns a string representation in decimal notation. - The result has at most as many decimal places as indicated by the int argument.*) + The result has at most as many decimal places as indicated by the int argument.*) val to_decimal_string : Expr.expr-> int -> string (** Returns a string representation of a numeral. *) @@ -1247,16 +1247,16 @@ sig val mk_const_s : context -> string -> Expr.expr (** Create a real numeral from a fraction. - @return A Term with rational value and sort Real - {!mk_numeral_s} *) + @return A Term with rational value and sort Real + {!mk_numeral_s} *) val mk_numeral_nd : context -> int -> int -> Expr.expr (** Create a real numeral. - @return A Term with the given value and sort Real *) + @return A Term with the given value and sort Real *) val mk_numeral_s : context -> string -> Expr.expr (** Create a real numeral. - @return A Term with the given value and sort Real *) + @return A Term with the given value and sort Real *) val mk_numeral_i : context -> int -> Expr.expr (** Creates an expression that checks whether a real number is an integer. *) @@ -1264,29 +1264,29 @@ sig (** Coerce a real to an integer. - The semantics of this function follows the SMT-LIB standard for the function to_int. - The argument must be of real sort. *) + The semantics of this function follows the SMT-LIB standard for the function to_int. + The argument must be of real sort. *) val mk_real2int : context -> Expr.expr -> Expr.expr (** Algebraic Numbers *) module AlgebraicNumber : sig (** Return a upper bound for a given real algebraic number. - The interval isolating the number is smaller than 1/10^precision. - {!is_algebraic_number} - @return A numeral Expr of sort Real *) + The interval isolating the number is smaller than 1/10^precision. + {!is_algebraic_number} + @return A numeral Expr of sort Real *) val to_upper : Expr.expr -> int -> Expr.expr - + (** Return a lower bound for the given real algebraic number. - The interval isolating the number is smaller than 1/10^precision. - {!is_algebraic_number} - @return A numeral Expr of sort Real *) + The interval isolating the number is smaller than 1/10^precision. + {!is_algebraic_number} + @return A numeral Expr of sort Real *) val to_lower : Expr.expr -> int -> Expr.expr - + (** Returns a string representation in decimal notation. - The result has at most as many decimal places as the int argument provided.*) + The result has at most as many decimal places as the int argument provided.*) val to_decimal_string : Expr.expr -> int -> string - + (** Returns a string representation of a numeral. *) val numeral_to_string : Expr.expr -> string end @@ -1846,52 +1846,52 @@ end module FloatingPoint : sig - (** Rounding Modes *) + (** Rounding Modes *) module RoundingMode : sig - (** Create the RoundingMode sort. *) + (** Create the RoundingMode sort. *) val mk_sort : context -> Sort.sort - (** Indicates whether the terms is of floating-point rounding mode sort. *) + (** Indicates whether the terms is of floating-point rounding mode sort. *) val is_fprm : Expr.expr -> bool - (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) + (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) val mk_round_nearest_ties_to_even : context -> Expr.expr - - (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) + + (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) val mk_rne : context -> Expr.expr - (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *) + (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *) val mk_round_nearest_ties_to_away : context -> Expr.expr - - (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *) + + (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *) val mk_rna : context -> Expr.expr - - (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) + + (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) val mk_round_toward_positive : context -> Expr.expr - - (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) - val mk_rtp : context -> Expr.expr - - (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) + + (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) + val mk_rtp : context -> Expr.expr + + (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) val mk_round_toward_negative : context -> Expr.expr - - (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) + + (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) val mk_rtn : context -> Expr.expr - - (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *) + + (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *) val mk_round_toward_zero : context -> Expr.expr - - (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *) + + (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *) val mk_rtz : context -> Expr.expr end (** Create a FloatingPoint sort. *) val mk_sort : context -> int -> int -> Sort.sort - + (** Create the half-precision (16-bit) FloatingPoint sort.*) val mk_sort_half : context -> Sort.sort - + (** Create the half-precision (16-bit) FloatingPoint sort. *) val mk_sort_16 : context -> Sort.sort @@ -1906,7 +1906,7 @@ sig (** Create the double-precision (64-bit) FloatingPoint sort. *) val mk_sort_64 : context -> Sort.sort - + (** Create the quadruple-precision (128-bit) FloatingPoint sort. *) val mk_sort_quadruple : context -> Sort.sort @@ -1924,7 +1924,7 @@ sig (** Create an expression of FloatingPoint sort from three bit-vector expressions. - This is the operator named `fp' in the SMT FP theory definition. + This is the operator named `fp' in the SMT FP theory definition. Note that \c sign is required to be a bit-vector of size 1. Significand and exponent are required to be greater than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes @@ -1939,16 +1939,16 @@ sig (** Create a numeral of FloatingPoint sort from a signed integer. *) val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr - + (** Create a numeral of FloatingPoint sort from a sign bit and two integers. *) val mk_numeral_i_u : context -> bool -> int -> int -> Sort.sort -> Expr.expr (** Create a numeral of FloatingPoint sort from a string *) val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr - + (** Indicates whether the terms is of floating-point sort. *) val is_fp : Expr.expr -> bool - + (** Indicates whether an expression is a floating-point abs expression *) val is_abs : Expr.expr -> bool @@ -1958,7 +1958,7 @@ sig (** Indicates whether an expression is a floating-point add expression *) val is_add : Expr.expr -> bool - + (** Indicates whether an expression is a floating-point sub expression *) val is_sub : Expr.expr -> bool @@ -2015,7 +2015,7 @@ sig (** Indicates whether an expression is a floating-point is_nan expression *) val is_is_nan : Expr.expr -> bool - + (** Indicates whether an expression is a floating-point is_negative expression *) val is_is_negative : Expr.expr -> bool @@ -2070,17 +2070,17 @@ sig (** Floating-point fused multiply-add. *) val mk_fma : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr - + (** Floating-point square root *) val mk_sqrt : context -> Expr.expr -> Expr.expr -> Expr.expr (** Floating-point remainder *) val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr - + (** Floating-point roundToIntegral. - Rounds a floating-point number to the closest integer, - again represented as a floating-point number. *) + Rounds a floating-point number to the closest integer, + again represented as a floating-point number. *) val mk_round_to_integral : context -> Expr.expr -> Expr.expr -> Expr.expr (** Minimum of floating-point numbers. *) @@ -2088,16 +2088,16 @@ sig (** Maximum of floating-point numbers. *) val mk_max : context -> Expr.expr -> Expr.expr -> Expr.expr - + (** Floating-point less than or equal. *) val mk_leq : context -> Expr.expr -> Expr.expr -> Expr.expr - + (** Floating-point less than. *) val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr (** Floating-point greater than or equal. *) val mk_geq : context -> Expr.expr -> Expr.expr -> Expr.expr - + (** Floating-point greater than. *) val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr @@ -2142,19 +2142,19 @@ sig (** C1onversion of a floating-point term into an unsigned bit-vector. *) val mk_to_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr - + (** Conversion of a floating-point term into a signed bit-vector. *) val mk_to_sbv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr (** Conversion of a floating-point term into a real-numbered term. *) val mk_to_real : context -> Expr.expr -> Expr.expr - + (** Retrieves the number of bits reserved for the exponent in a FloatingPoint sort. *) val get_ebits : context -> Sort.sort -> int (** Retrieves the number of bits reserved for the significand in a FloatingPoint sort. *) val get_sbits : context -> Sort.sort -> int - + (** Retrieves the sign of a floating-point literal. *) val get_numeral_sign : context -> Expr.expr -> bool * int @@ -2162,7 +2162,7 @@ sig val get_numeral_significand_string : context -> Expr.expr -> string (** Return the significand value of a floating-point numeral as a uint64. - Remark: This function extracts the significand bits, without the + Remark: This function extracts the significand bits, without the hidden bit or normalization. Throws an exception if the significand does not fit into a uint64. *) val get_numeral_significand_uint : context -> Expr.expr -> bool * int @@ -2172,7 +2172,7 @@ sig (** Return the exponent value of a floating-point numeral as a signed integer *) val get_numeral_exponent_int : context -> Expr.expr -> bool * int - + (** Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. *) val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr @@ -2675,13 +2675,13 @@ sig (** Function interpretations entries - An Entry object represents an element in the finite map used to a function interpretation. *) + An Entry object represents an element in the finite map used to a function interpretation. *) module FuncEntry : sig type func_entry (** Return the (symbolic) value of this entry. - *) + *) val get_value : func_entry -> Expr.expr (** The number of arguments of the entry. @@ -2865,8 +2865,8 @@ sig val get_subgoal : apply_result -> int -> Goal.goal (** Convert a model for a subgoal into a model for the original - goal [g], that the ApplyResult was obtained from. - #return A model for [g] *) + goal [g], that the ApplyResult was obtained from. + #return A model for [g] *) val convert_model : apply_result -> int -> Model.model -> Model.model (** A string representation of the ApplyResult. *) @@ -2957,31 +2957,31 @@ end module Statistics : sig type statistics - + (** Statistical data is organized into pairs of \[Key, Entry\], where every - Entry is either a floating point or integer value. *) + Entry is either a floating point or integer value. *) module Entry : sig type statistics_entry - + (** The key of the entry. *) val get_key : statistics_entry -> string - + (** The int-value of the entry. *) val get_int : statistics_entry -> int - + (** The float-value of the entry. *) val get_float : statistics_entry -> float - + (** True if the entry is uint-valued. *) val is_int : statistics_entry -> bool - + (** True if the entry is float-valued. *) val is_float : statistics_entry -> bool - + (** The string representation of the the entry's value. *) val to_string_value : statistics_entry -> string - + (** The string representation of the entry (key and value) *) val to_string : statistics_entry -> string end From 689ed9fa12bbf0fc900b2affc77c7160725a550d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 9 Nov 2015 13:25:52 +0000 Subject: [PATCH 14/53] Added Z3_mk_array_ext to ML API. Relates to #292 --- src/api/ml/z3.ml | 3 +++ src/api/ml/z3.mli | 7 +++++++ 2 files changed, 10 insertions(+) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 7aa28b272..ca48a72bf 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1217,6 +1217,9 @@ struct let mk_term_array ( ctx : context ) ( arg : expr ) = expr_of_ptr ctx (Z3native.mk_array_default (context_gno ctx) (Expr.gno arg)) + + let mk_array_ext ( ctx : context) ( arg1 : expr ) ( arg2 : expr ) = + expr_of_ptr ctx (Z3native.mk_array_ext (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2)) end diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index e97313148..e69f7f576 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -866,6 +866,13 @@ sig Produces the default range value, for arrays that can be represented as finite maps with a default range value. *) val mk_term_array : context -> Expr.expr -> Expr.expr + + (** Create array extensionality index given two arrays with the same sort. + + The meaning is given by the axiom: + (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B)) *) + val mk_array_ext : context -> Expr.expr -> Expr.expr -> Expr.expr + end (** Functions to manipulate Set expressions *) From 5995c753d30c3ce12247a6a91612fed0a89d75c0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 9 Nov 2015 13:54:28 +0000 Subject: [PATCH 15/53] Bugfix for theory_fpa construction and destruction. --- src/smt/theory_fpa.cpp | 25 ++++++++++++++++++++----- src/smt/theory_fpa.h | 5 ++++- 2 files changed, 24 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 65a66cf80..0cd803cc0 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -142,7 +142,8 @@ namespace smt { m_trail_stack(*this), m_fpa_util(m_converter.fu()), m_bv_util(m_converter.bu()), - m_arith_util(m_converter.au()) + m_arith_util(m_converter.au()), + m_is_initialized(false) { params_ref p; p.set_bool("arith_lhs", true); @@ -151,10 +152,24 @@ namespace smt { theory_fpa::~theory_fpa() { - ast_manager & m = get_manager(); - dec_ref_map_values(m, m_conversions); - dec_ref_map_values(m, m_wraps); - dec_ref_map_values(m, m_unwraps); + if (m_is_initialized) { + ast_manager & m = get_manager(); + dec_ref_map_values(m, m_conversions); + dec_ref_map_values(m, m_wraps); + dec_ref_map_values(m, m_unwraps); + } + else { + SASSERT(m_conversions.empty()); + SASSERT(m_wraps.empty()); + SASSERT(m_unwraps.empty()); + } + + m_is_initialized = false; + } + + void theory_fpa::init(context * ctx) { + smt::theory::init(ctx); + m_is_initialized = true; } app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector & values) { diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 9db6a88a9..1b0fc6c54 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -148,6 +148,7 @@ namespace smt { obj_map m_wraps; obj_map m_unwraps; obj_map m_conversions; + bool m_is_initialized; virtual final_check_status final_check_eh(); virtual bool internalize_atom(app * atom, bool gate_ctx); @@ -169,9 +170,11 @@ namespace smt { virtual void finalize_model(model_generator & mg); public: - theory_fpa(ast_manager& m); + theory_fpa(ast_manager & m); virtual ~theory_fpa(); + virtual void init(context * ctx); + virtual void display(std::ostream & out) const; protected: From 84f935ae85ab9bdf79770919a484e0ca85a91488 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Nov 2015 06:38:06 -0800 Subject: [PATCH 16/53] initialize solver prior to translate. fixes build break Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 6a8a378e5..6112a8cd2 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -103,6 +103,7 @@ extern "C" { RESET_ERROR_CODE(); params_ref const& p = to_solver(s)->m_params; Z3_solver_ref * sr = alloc(Z3_solver_ref, 0); + init_solver(c, s); 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); From 1807acdf26f48a6d521d60c4a150ad23f1275da8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 9 Nov 2015 17:50:50 +0000 Subject: [PATCH 17/53] tabs, whitespace --- src/ast/rewriter/var_subst.cpp | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp index 1d01ef85c..37b335a9d 100644 --- a/src/ast/rewriter/var_subst.cpp +++ b/src/ast/rewriter/var_subst.cpp @@ -27,7 +27,7 @@ void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, exp SASSERT(is_well_sorted(result.m(), n)); m_reducer.reset(); if (m_std_order) - m_reducer.set_inv_bindings(num_args, args); + m_reducer.set_inv_bindings(num_args, args); else m_reducer.set_bindings(num_args, args); m_reducer(n, result); @@ -66,7 +66,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) { return; } - ptr_buffer used_decl_sorts; + ptr_buffer used_decl_sorts; buffer used_decl_names; for (unsigned i = 0; i < num_decls; ++i) { if (m_used.contains(num_decls - i - 1)) { @@ -74,7 +74,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) { used_decl_names.push_back(q->get_decl_name(i)); } } - + unsigned num_removed = 0; expr_ref_buffer var_mapping(m); int next_idx = 0; @@ -100,18 +100,18 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) { else var_mapping.push_back(0); } - - - // Remark: + + + // Remark: // (VAR 0) should be in the last position of var_mapping. // ... // (VAR (var_mapping.size() - 1)) should be in the first position. std::reverse(var_mapping.c_ptr(), var_mapping.c_ptr() + var_mapping.size()); expr_ref new_expr(m); - + m_subst(q->get_expr(), var_mapping.size(), var_mapping.c_ptr(), new_expr); - + if (num_removed == num_decls) { result = new_expr; return; @@ -120,7 +120,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) { expr_ref tmp(m); expr_ref_buffer new_patterns(m); expr_ref_buffer new_no_patterns(m); - + for (unsigned i = 0; i < num_patterns; i++) { m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp); new_patterns.push_back(tmp); @@ -129,7 +129,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) { m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp); new_no_patterns.push_back(tmp); } - + result = m.mk_quantifier(q->is_forall(), used_decl_sorts.size(), used_decl_sorts.c_ptr(), @@ -143,7 +143,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) { num_no_patterns, new_no_patterns.c_ptr()); to_quantifier(result)->set_no_unused_vars(); - SASSERT(is_well_sorted(m, result)); + SASSERT(is_well_sorted(m, result)); } void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) { From 746689904de6778abb6c5892a0d907f95971fb51 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 10 Nov 2015 16:23:05 +0000 Subject: [PATCH 18/53] Added elim_small_bv_tactic. --- src/tactic/bv/elim_small_bv_tactic.cpp | 332 +++++++++++++++++++++++++ src/tactic/bv/elim_small_bv_tactic.h | 32 +++ 2 files changed, 364 insertions(+) create mode 100644 src/tactic/bv/elim_small_bv_tactic.cpp create mode 100644 src/tactic/bv/elim_small_bv_tactic.h diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp new file mode 100644 index 000000000..d2c7ff5f4 --- /dev/null +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -0,0 +1,332 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + elim_small_bv.h + +Abstract: + + Tactic that eliminates small, quantified bit-vectors. + +Author: + + Christoph (cwinter) 2015-11-09 + +Revision History: + +--*/ +#include"tactical.h" +#include"rewriter_def.h" +#include"filter_model_converter.h" +#include"cooperate.h" +#include"bv_decl_plugin.h" +#include"used_vars.h" +#include"well_sorted.h" +#include"var_subst.h" +#include"simplifier.h" +#include"basic_simplifier_plugin.h" +#include"bv_simplifier_plugin.h" + +#include"elim_small_bv_tactic.h" + +class elim_small_bv_tactic : public tactic { + + struct rw_cfg : public default_rewriter_cfg { + ast_manager & m; + bv_util m_util; + simplifier m_simp; + ref m_mc; + goal * m_goal; + unsigned m_max_bits; + unsigned long long m_max_steps; + unsigned long long m_max_memory; // in bytes + bool m_produce_models; + sort_ref_vector m_bindings; + unsigned long m_num_eliminated; + + rw_cfg(ast_manager & _m, params_ref const & p) : + m(_m), + m_util(_m), + m_simp(_m), + m_bindings(_m), + m_num_eliminated(0) { + updt_params(p); + m_goal = 0; + m_max_steps = UINT_MAX; + + basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m); + // bsimp->set_eliminate_and(true); + m_simp.register_plugin(bsimp); + + bv_simplifier_params bv_params; + bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, bv_params); + m_simp.register_plugin(bvsimp); + } + + bool max_steps_exceeded(unsigned long long num_steps) const { + cooperate("elim-small-bv"); + if (num_steps > m_max_steps) + return true; + if (memory::get_allocation_size() > m_max_memory) + throw tactic_exception(TACTIC_MAX_MEMORY_MSG); + return false; + } + + bool is_small_bv(sort * s) { + return m_util.is_bv_sort(s) && m_util.get_bv_size(s) <= m_max_bits; + } + + expr_ref replace_var(used_vars & uv, + unsigned num_decls, unsigned max_var_idx_p1, + unsigned idx, sort * s, expr * e, expr * replacement) { + TRACE("elim_small_bv", tout << "replace idx " << idx << " with " << mk_ismt2_pp(replacement, m) << + " in " << mk_ismt2_pp(e, m) << std::endl;); + expr_ref res(m); + expr_ref_vector substitution(m); + + substitution.resize(num_decls, 0); + substitution[num_decls - idx - 1] = replacement; + + // (VAR 0) is in the first position of substitution; (VAR num_decls-1) is in the last position. + + for (unsigned i = 0; i < max_var_idx_p1; i++) { + sort * s = uv.get(i); + substitution.push_back(0); + } + + // (VAR num_decls) ... (VAR num_decls+sz-1); are in positions num_decls .. num_decls+sz-1 + + std::reverse(substitution.c_ptr(), substitution.c_ptr() + substitution.size()); + + // (VAR 0) should be in the last position of substitution. + + TRACE("elim_small_bv", tout << "substitution: " << std::endl; + for (unsigned k = 0; k < substitution.size(); k++) { + expr * se = substitution[k].get(); + tout << k << " = "; + if (se == 0) tout << "0"; + else tout << mk_ismt2_pp(se, m); + tout << std::endl; + }); + + var_subst vsbst(m); + vsbst(e, substitution.size(), substitution.c_ptr(), res); + SASSERT(is_well_sorted(m, res)); + + proof_ref pr(m); + m_simp(res, res, pr); + TRACE("elim_small_bv", tout << "replace done: " << mk_ismt2_pp(res, m) << std::endl;); + + return res; + } + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + result = m.mk_app(f, num, args); + TRACE("elim_small_bv_app", tout << "reduce " << mk_ismt2_pp(result, m) << std::endl; ); + return BR_FAILED; + } + + bool reduce_quantifier( + quantifier * q, + expr * old_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + TRACE("elim_small_bv", tout << "reduce_quantifier " << mk_ismt2_pp(q, m) << std::endl; ); + unsigned long long num_steps = 0; + unsigned curr_sz = m_bindings.size(); + SASSERT(q->get_num_decls() <= curr_sz); + unsigned num_decls = q->get_num_decls(); + unsigned old_sz = curr_sz - num_decls; + + used_vars uv; + uv(q); + SASSERT(is_well_sorted(m, q)); + unsigned max_var_idx_p1 = uv.get_max_found_var_idx_plus_1(); + + expr_ref body(old_body, m); + for (unsigned i = num_decls-1; i != ((unsigned)-1) && !max_steps_exceeded(num_steps); i--) { + sort * s = q->get_decl_sort(i); + symbol const & name = q->get_decl_name(i); + unsigned bv_sz = m_util.get_bv_size(s); + + if (is_small_bv(s) && !max_steps_exceeded(num_steps)) { + TRACE("elim_small_bv", tout << "eliminating " << name << + "; sort = " << mk_ismt2_pp(s, m) << + "; body = " << mk_ismt2_pp(body, m) << std::endl;); + + expr_ref_vector new_bodies(m); + for (unsigned j = 0; j < bv_sz && !max_steps_exceeded(num_steps); j ++) { + expr_ref n(m_util.mk_numeral(j, bv_sz), m); + expr_ref nb(m); + nb = replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n); + new_bodies.push_back(nb); + num_steps++; + } + + TRACE("elim_small_bv", tout << "new bodies: " << std::endl; + for (unsigned k = 0; k < new_bodies.size(); k++) + tout << mk_ismt2_pp(new_bodies[k].get(), m) << std::endl; ); + + body = q->is_forall() ? m.mk_and(new_bodies.size(), new_bodies.c_ptr()) : + m.mk_or(new_bodies.size(), new_bodies.c_ptr()); + SASSERT(is_well_sorted(m, body)); + + proof_ref pr(m); + m_simp(body, body, pr); + m_num_eliminated++; + } + } + + quantifier_ref new_q(m); + new_q = m.update_quantifier(q, body); + unused_vars_eliminator el(m); + el(new_q, result); + + TRACE("elim_small_bv", tout << "elimination result: " << mk_ismt2_pp(result, m) << std::endl; ); + + result_pr = 0; // proofs NIY + m_bindings.shrink(old_sz); + return true; + } + + bool pre_visit(expr * t) { + TRACE("elim_small_bv_pre", tout << "pre_visit: " << mk_ismt2_pp(t, m) << std::endl;); + if (is_quantifier(t)) { + quantifier * q = to_quantifier(t); + TRACE("elim_small_bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m) << std::endl;); + sort_ref_vector new_bindings(m); + for (unsigned i = 0; i < q->get_num_decls(); i++) + new_bindings.push_back(q->get_decl_sort(i)); + SASSERT(new_bindings.size() == q->get_num_decls()); + m_bindings.append(new_bindings); + } + return true; + } + + void updt_params(params_ref const & p) { + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_max_steps = p.get_uint("max_steps", UINT_MAX); + m_max_bits = p.get_uint("max_bits", 4); + } + }; + + struct rw : public rewriter_tpl { + rw_cfg m_cfg; + + rw(ast_manager & m, params_ref const & p) : + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, p) { + } + }; + + struct imp { + ast_manager & m; + rw m_rw; + + imp(ast_manager & _m, params_ref const & p) : + m(_m), + m_rw(m, p) { + } + + void set_cancel(bool f) { + m_rw.set_cancel(f); + } + + void updt_params(params_ref const & p) { + m_rw.cfg().updt_params(p); + } + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + SASSERT(g->is_well_sorted()); + mc = 0; pc = 0; core = 0; + tactic_report report("elim-small-bv", *g); + bool produce_proofs = g->proofs_enabled(); + fail_if_proof_generation("elim-small-bv", g); + fail_if_unsat_core_generation("elim-small-bv", g); + m_rw.cfg().m_produce_models = g->models_enabled(); + + m_rw.m_cfg.m_goal = g.get(); + expr_ref new_curr(m); + proof_ref new_pr(m); + unsigned size = g->size(); + for (unsigned idx = 0; idx < size; idx++) { + expr * curr = g->form(idx); + m_rw(curr, new_curr, new_pr); + if (produce_proofs) { + proof * pr = g->pr(idx); + new_pr = m.mk_modus_ponens(pr, new_pr); + } + g->update(idx, new_curr, new_pr, g->dep(idx)); + } + mc = 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(); + result.push_back(g.get()); + TRACE("elim-small-bv", g->display(tout);); + SASSERT(g->is_well_sorted()); + } + }; + + imp * m_imp; + params_ref m_params; +public: + elim_small_bv_tactic(ast_manager & m, params_ref const & p) : + m_params(p) { + m_imp = alloc(imp, m, p); + } + + virtual tactic * translate(ast_manager & m) { + return alloc(elim_small_bv_tactic, m, m_params); + } + + virtual ~elim_small_bv_tactic() { + dealloc(m_imp); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_imp->m_rw.cfg().updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + insert_max_memory(r); + insert_max_steps(r); + r.insert("max_bits", CPK_UINT, "(default: 4) maximum bit-vector size of quantified bit-vectors to be eliminated."); + } + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + (*m_imp)(in, result, mc, pc, core); + } + + virtual void cleanup() { + ast_manager & m = m_imp->m; + imp * d = alloc(imp, m, m_params); +#pragma omp critical (tactic_cancel) + { + std::swap(d, m_imp); + } + dealloc(d); + } + + virtual void set_cancel(bool f) { + if (m_imp) + m_imp->set_cancel(f); + } +}; + +tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(elim_small_bv_tactic, m, p)); +} + diff --git a/src/tactic/bv/elim_small_bv_tactic.h b/src/tactic/bv/elim_small_bv_tactic.h new file mode 100644 index 000000000..bcdd8aad6 --- /dev/null +++ b/src/tactic/bv/elim_small_bv_tactic.h @@ -0,0 +1,32 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + elim_small_bv.h + +Abstract: + + Tactic that eliminates small, quantified bit-vectors. + +Author: + + Christoph (cwinter) 2015-11-09 + +Revision History: + +--*/ +#ifndef ELIM_SMALL_BV_H_ +#define ELIM_SMALL_BV_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("elim-small-bv", "eliminate small, quantified bit-vectors by expansion.", "mk_elim_small_bv_tactic(m, p)") +*/ + +#endif From 315dc80eb0ae64f7cae14c6e5950f9ed4c2c4ac9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Nov 2015 15:09:52 -0500 Subject: [PATCH 19/53] toggle default for bv2int decision procedure support to avoid confusing users. Issue #301 Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/params/theory_bv_params.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index e84f3654c..56d393d41 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -33,7 +33,7 @@ def_module_params(module_name='smt', ('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'), ('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'), ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), - ('bv.enable_int2bv', BOOL, False, 'enable support for int2bv and bv2int operators'), + ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'), diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h index d7c9f903b..00565969e 100644 --- a/src/smt/params/theory_bv_params.h +++ b/src/smt/params/theory_bv_params.h @@ -39,7 +39,7 @@ struct theory_bv_params { m_bv_lazy_le(false), m_bv_cc(false), m_bv_blast_max_size(INT_MAX), - m_bv_enable_int2bv2int(false) { + m_bv_enable_int2bv2int(true) { updt_params(p); } From 2865f60f8c6514a9e564e23bb7651ad021072d5c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Nov 2015 11:39:34 -0500 Subject: [PATCH 20/53] deal with case of unsatisfiable context and bit-vector objectives that are not normalized to maxsmt. Issue #304 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 83d83fdb5..49b5f988f 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -902,6 +902,21 @@ namespace opt { m_hard_constraints.push_back(fml); } } + // fix types of objectives: + for (unsigned i = 0; i < m_objectives.size(); ++i) { + objective & obj = m_objectives[i]; + expr* t = obj.m_term; + switch(obj.m_type) { + case O_MINIMIZE: + case O_MAXIMIZE: + if (!m_arith.is_int(t) && !m_arith.is_real(t)) { + obj.m_term = m_arith.mk_numeral(rational(0), true); + } + break; + default: + break; + } + } } void context::purify(app_ref& term) { @@ -1000,7 +1015,10 @@ namespace opt { switch(obj.m_type) { case O_MINIMIZE: { app_ref tmp(m); - tmp = m_arith.mk_uminus(obj.m_term); + tmp = obj.m_term; + if (m_arith.is_int(tmp) || m_arith.is_real(tmp)) { + tmp = m_arith.mk_uminus(obj.m_term); + } obj.m_index = m_optsmt.add(tmp); break; } From 87ae5888ee603ec7e365700ac3eefcb98dc05938 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Nov 2015 14:48:29 +0000 Subject: [PATCH 21/53] whitespace --- src/ast/rewriter/bool_rewriter.cpp | 88 +++++++++++++++--------------- 1 file changed, 44 insertions(+), 44 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 5b0c38616..6dec03307 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -84,7 +84,7 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg ptr_buffer buffer; expr_fast_mark1 neg_lits; expr_fast_mark2 pos_lits; - + for (unsigned i = 0; i < num_args; i++) { expr * arg = args[i]; if (m().is_true(arg)) { @@ -120,9 +120,9 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg } buffer.push_back(arg); } - + unsigned sz = buffer.size(); - + switch(sz) { case 0: result = m().mk_true(); @@ -208,9 +208,9 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args } buffer.push_back(arg); } - + unsigned sz = buffer.size(); - + switch(sz) { case 0: result = m().mk_false(); @@ -222,7 +222,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args if (m_local_ctx && m_local_ctx_cost <= m_local_ctx_limit) { neg_lits.reset(); pos_lits.reset(); - if (local_ctx_simp(sz, buffer.c_ptr(), result)) + if (local_ctx_simp(sz, buffer.c_ptr(), result)) return BR_DONE; } if (s) { @@ -273,11 +273,11 @@ expr * bool_rewriter::mk_or_app(unsigned num_args, expr * const * args) { /** \brief Auxiliary method for local_ctx_simp. - + Replace args[i] by true if marked in neg_lits. Replace args[i] by false if marked in pos_lits. */ -bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args, +bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result) { ptr_buffer new_args; bool simp = false; @@ -307,13 +307,13 @@ bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args, } if (simp) { switch(new_args.size()) { - case 0: - result = m().mk_true(); + case 0: + result = m().mk_true(); return true; - case 1: - mk_not(new_args[0], result); + case 1: + mk_not(new_args[0], result); return true; - default: + default: result = m().mk_not(m().mk_or(new_args.size(), new_args.c_ptr())); return true; } @@ -358,7 +358,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul result = t; return; } - + if (m().is_false(c)) { result = e; return; @@ -368,7 +368,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul result = t; return; } - + if (m().is_bool(t)) { if (m().is_true(t)) { if (m().is_false(e)) { @@ -384,13 +384,13 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul return; } expr_ref tmp(m()); - mk_not(e, tmp); + mk_not(e, tmp); result = m().mk_not(m().mk_or(c, tmp)); return; } if (m().is_true(e)) { expr_ref tmp(m()); - mk_not(c, tmp); + mk_not(c, tmp); result = m().mk_or(tmp, t); return; } @@ -406,7 +406,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul result = m().mk_or(c, e); return; } - if (m().is_complement_core(t, e)) { // t = not(e) + if (m().is_complement_core(t, e)) { // t = not(e) mk_eq(c, t, result); return; } @@ -443,8 +443,8 @@ bool bool_rewriter::simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, exp expr * new_e = simp_arg(to_app(t)->get_arg(2), neg_lits, pos_lits, modified); if (!modified) return false; - // It is not safe to invoke mk_ite here, since it can recursively call - // local_ctx_simp by + // It is not safe to invoke mk_ite here, since it can recursively call + // local_ctx_simp by // - transforming the ITE into an OR // - and invoked mk_or, that will invoke local_ctx_simp // mk_ite(new_c, new_t, new_e, result); @@ -522,7 +522,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_ PUSH_NEW_ARG(arg); \ } \ } - + m_local_ctx_cost += 2*num_args; #if 0 static unsigned counter = 0; @@ -567,9 +567,9 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_ /** \brief Apply simplification if ite is an if-then-else tree where every leaf is a value. - - This is an efficient way to - + + This is an efficient way to + */ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) { SASSERT(m().is_ite(ite)); @@ -585,7 +585,7 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) tout << t << " " << e << " " << val << "\n";); result = m().mk_false(); return BR_DONE; - } + } if (t == val && e == val) { result = m().mk_true(); @@ -598,7 +598,7 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) } SASSERT(e == val); - + mk_not(ite->get_arg(0), result); return BR_DONE; } @@ -642,14 +642,14 @@ static bool is_ite_value_tree_neq_value(ast_manager & m, app * ite, app * val) { return true; } -#endif +#endif br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { if (lhs == rhs) { result = m().mk_true(); return BR_DONE; } - + if (m().are_distinct(lhs, rhs)) { result = m().mk_false(); return BR_DONE; @@ -662,7 +662,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { // return BR_DONE; // } r = try_ite_value(to_app(lhs), to_app(rhs), result); - CTRACE("try_ite_value", r != BR_FAILED, + CTRACE("try_ite_value", r != BR_FAILED, tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";); } else if (m().is_ite(rhs) && m().is_value(lhs)) { @@ -671,7 +671,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { // return BR_DONE; // } r = try_ite_value(to_app(rhs), to_app(lhs), result); - CTRACE("try_ite_value", r != BR_FAILED, + CTRACE("try_ite_value", r != BR_FAILED, tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";); } if (r != BR_FAILED) @@ -756,13 +756,13 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args result = m().mk_and(new_diseqs.size(), new_diseqs.c_ptr()); return BR_REWRITE3; } - + return BR_FAILED; } br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result) { bool s = false; - + // (ite (not c) a b) ==> (ite c b a) if (m().is_not(c)) { c = to_app(c)->get_arg(0); @@ -788,7 +788,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = t; return BR_DONE; } - + if (m().is_false(c)) { result = e; return BR_DONE; @@ -814,18 +814,18 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re return BR_DONE; } expr_ref tmp(m()); - mk_not(c, tmp); + mk_not(c, tmp); mk_and(tmp, e, result); return BR_DONE; } if (m().is_true(e)) { expr_ref tmp(m()); - mk_not(c, tmp); + mk_not(c, tmp); mk_or(tmp, t, result); return BR_DONE; } if (m().is_false(e)) { - mk_and(c, t, result); + mk_and(c, t, result); return BR_DONE; } if (c == e) { @@ -833,10 +833,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re return BR_DONE; } if (c == t) { - mk_or(c, e, result); + mk_or(c, e, result); return BR_DONE; } - if (m().is_complement_core(t, e)) { // t = not(e) + if (m().is_complement_core(t, e)) { // t = not(e) mk_eq(c, t, result); return BR_DONE; } @@ -863,10 +863,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = m().mk_ite(new_c, to_app(t)->get_arg(1), e); return BR_REWRITE1; } - + if (m().is_ite(e)) { // (ite c1 (ite c2 t1 t2) (ite c3 t1 t2)) ==> (ite (or (and c1 c2) (and (not c1) c3)) t1 t2) - if (to_app(t)->get_arg(1) == to_app(e)->get_arg(1) && + if (to_app(t)->get_arg(1) == to_app(e)->get_arg(1) && to_app(t)->get_arg(2) == to_app(e)->get_arg(2)) { expr_ref and1(m()); expr_ref and2(m()); @@ -879,9 +879,9 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2)); return BR_REWRITE1; } - + // (ite c1 (ite c2 t1 t2) (ite c3 t2 t1)) ==> (ite (or (and c1 c2) (and (not c1) (not c3))) t1 t2) - if (to_app(t)->get_arg(1) == to_app(e)->get_arg(2) && + if (to_app(t)->get_arg(1) == to_app(e)->get_arg(2) && to_app(t)->get_arg(2) == to_app(e)->get_arg(1)) { expr_ref and1(m()); expr_ref and2(m()); @@ -922,10 +922,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = m().mk_ite(c, t, e); return BR_DONE; } - + return BR_FAILED; } - + br_status bool_rewriter::mk_not_core(expr * t, expr_ref & result) { if (m().is_not(t)) { result = to_app(t)->get_arg(0); From 5cf2caa7e9a35705bf78a38a5076b89f3b4790d5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Nov 2015 14:48:55 +0000 Subject: [PATCH 22/53] Added check for QF_BV in QF_UFBV tactic. --- src/tactic/smtlogics/qfufbv_tactic.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index d10b7c1b4..816d69b1f 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -25,6 +25,7 @@ Notes: #include"max_bv_sharing_tactic.h" #include"bv_size_reduction_tactic.h" #include"reduce_args_tactic.h" +#include"qfbv_tactic.h" tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; @@ -41,13 +42,11 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { ); tactic * st = using_params(and_then(preamble_st, - mk_smt_tactic()), + cond(mk_is_qfbv_probe(), + mk_qfbv_tactic(m), + mk_smt_tactic())), main_p); - //cond(is_qfbv(), - // and_then(mk_bit_blaster(m), - // mk_sat_solver(m)), - // mk_smt_solver()) st->updt_params(p); return st; } From 5f8f0b128022790bc6e4402c4a5671404cd92891 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Nov 2015 14:49:21 +0000 Subject: [PATCH 23/53] Added bool rewriter case. --- src/ast/rewriter/bool_rewriter.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 6dec03307..0b8a51fb4 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -708,6 +708,19 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { result = m().mk_eq(lhs, rhs); return BR_DONE; } + + expr *la, *lb, *ra, *rb; + // fold (iff (iff a b) (iff (not a) b)) to false + if (m().is_iff(lhs, la, lb) && m().is_iff(rhs, ra, rb)) { + expr *n; + if ((la == ra && ((m().is_not(rb, n) && n == lb) || + (m().is_not(lb, n) && n == rb))) || + (lb == rb && ((m().is_not(ra, n) && n == la) || + (m().is_not(la, n) && n == ra)))) { + result = m().mk_false(); + return BR_DONE; + } + } } return BR_FAILED; } From 643dbb874b4db701b6ddbc13e5b9ddec1d819e15 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Nov 2015 15:27:33 +0000 Subject: [PATCH 24/53] Added tactic that translates BV arrays into BV UFs. --- src/ast/array_decl_plugin.h | 15 +- src/tactic/bv/bvarray2uf_rewriter.cpp | 377 ++++++++++++++++++++++++++ src/tactic/bv/bvarray2uf_rewriter.h | 87 ++++++ src/tactic/bv/bvarray2uf_tactic.cpp | 168 ++++++++++++ src/tactic/bv/bvarray2uf_tactic.h | 33 +++ 5 files changed, 675 insertions(+), 5 deletions(-) create mode 100644 src/tactic/bv/bvarray2uf_rewriter.cpp create mode 100644 src/tactic/bv/bvarray2uf_rewriter.h create mode 100644 src/tactic/bv/bvarray2uf_tactic.cpp create mode 100644 src/tactic/bv/bvarray2uf_tactic.h diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 778b94c33..60adc3ae6 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -22,7 +22,7 @@ Revision History: #include"ast.h" -inline sort* get_array_range(sort const * s) { +inline sort* get_array_range(sort const * s) { return to_sort(s->get_parameter(s->get_num_parameters() - 1).get_ast()); } @@ -104,20 +104,20 @@ class array_decl_plugin : public decl_plugin { } // - // Contract for sort: - // parameters[0] - 1st dimension + // Contract for sort: + // parameters[0] - 1st dimension // ... // parameters[n-1] - nth dimension // parameters[n] - range // virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - + // // Contract for func_decl: // parameters[0] - array sort // Contract for others: // no parameters - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); virtual void get_op_names(svector & op_names, symbol const & logic); @@ -184,6 +184,11 @@ public: sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); } sort * mk_array_sort(unsigned arity, sort* const* domain, sort* range); + + app * mk_as_array(sort * s, func_decl * f) { + parameter param(f); + return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, ¶m, 0, 0, s); + } }; diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp new file mode 100644 index 000000000..83038cfa9 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -0,0 +1,377 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + bvarray2uf_rewriter.cpp + +Abstract: + + Rewriter that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ + +#include"cooperate.h" +#include"bv_decl_plugin.h" +#include"array_decl_plugin.h" +#include"params.h" +#include"ast_pp.h" +#include"bvarray2uf_rewriter.h" + +// [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving +// Quantified Bit-Vector Formulas, in Formal Methods in System Design, +// vol. 42, no. 1, pp. 3-23, Springer, 2013. + +bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p) : + m_manager(m), + m_out(m), + m_bindings(m), + m_bv_util(m), + m_array_util(m), + m_emc(0), + m_fmc(0), + extra_assertions(m) { + updt_params(p); + // We need to make sure that the mananger has the BV and array plugins loaded. + symbol s_bv("bv"); + if (!m_manager.has_plugin(s_bv)) + m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); + symbol s_array("array"); + if (!m_manager.has_plugin(s_array)) + m_manager.register_plugin(s_array, alloc(array_decl_plugin)); +} + +bvarray2uf_rewriter_cfg::~bvarray2uf_rewriter_cfg() { + for (obj_map::iterator it = m_arrays_fs.begin(); + it != m_arrays_fs.end(); + it++) + m_manager.dec_ref(it->m_value); +} + +void bvarray2uf_rewriter_cfg::reset() {} + +sort * bvarray2uf_rewriter_cfg::get_index_sort(expr * e) { + return get_index_sort(m_manager.get_sort(e)); +} + +sort * bvarray2uf_rewriter_cfg::get_index_sort(sort * s) { + SASSERT(s->get_num_parameters() >= 2); + unsigned total_width = 0; + for (unsigned i = 0; i < s->get_num_parameters() - 1; i++) { + parameter const & p = s->get_parameter(i); + SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast()))); + SASSERT(m_bv_util.is_bv_sort(to_sort(p.get_ast()))); + total_width += m_bv_util.get_bv_size(to_sort(p.get_ast())); + } + return m_bv_util.mk_sort(total_width); +} + +sort * bvarray2uf_rewriter_cfg::get_value_sort(expr * e) { + return get_value_sort(m_manager.get_sort(e)); +} + +sort * bvarray2uf_rewriter_cfg::get_value_sort(sort * s) { + SASSERT(s->get_num_parameters() >= 2); + parameter const & p = s->get_parameter(s->get_num_parameters() - 1); + SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast()))); + return to_sort(p.get_ast()); +} + +bool bvarray2uf_rewriter_cfg::is_bv_array(expr * e) { + return is_bv_array(m_manager.get_sort(e)); +} + +bool bvarray2uf_rewriter_cfg::is_bv_array(sort * s) { + if (!m_array_util.is_array(s)) + return false; + + SASSERT(s->get_num_parameters() >= 2); + for (unsigned i = 0; i < s->get_num_parameters(); i++) { + parameter const & p = s->get_parameter(i); + if (!p.is_ast() || !is_sort(to_sort(p.get_ast())) || + !m_bv_util.is_bv_sort(to_sort(p.get_ast()))) + return false; + } + + return true; +} + +func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) { + SASSERT(is_bv_array(e)); + + if (m_array_util.is_as_array(e)) + return func_decl_ref(static_cast(to_app(e)->get_decl()->get_parameter(0).get_ast()), m_manager); + else { + app * a = to_app(e); + func_decl * bv_f = 0; + if (!m_arrays_fs.find(e, bv_f)) { + sort * domain = get_index_sort(a); + sort * range = get_value_sort(a); + bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range); + if (is_uninterp_const(e)) { + if (m_emc) + m_emc->insert(to_app(e)->get_decl(), + m_array_util.mk_as_array(m_manager.get_sort(e), bv_f)); + } + else if (m_fmc) + m_fmc->insert(bv_f); + m_arrays_fs.insert(e, bv_f); + m_manager.inc_ref(bv_f); + } + + return func_decl_ref(bv_f, m_manager); + } +} + +br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + br_status res = BR_FAILED; + + if (m_manager.is_eq(f) && is_bv_array(f->get_domain()[0])) { + SASSERT(num == 2); + // From [1]: Finally, we replace equations of the form t = s, + // where t and s are arrays, with \forall x . f_t(x) = f_s(x). + func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager); + func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager); + + sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) }; + symbol names[1] = { symbol("x") }; + var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); + + expr_ref body(m_manager); + body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get())); + + result = m_manager.mk_forall(1, sorts, names, body); + res = BR_DONE; + } + else if (m_manager.is_distinct(f) && is_bv_array(f->get_domain()[0])) { + result = m_manager.mk_distinct_expanded(num, args); + res = BR_REWRITE1; + } + else if (f->get_family_id() == null_family_id) { + TRACE("bvarray2uf_rw", tout << "UF APP: " << f->get_name() << std::endl; ); + + bool has_bv_arrays = false; + func_decl_ref f_t(m_manager); + for (unsigned i = 0; i < num; i++) { + if (is_bv_array(args[i])) { + SASSERT(m_array_util.is_as_array(args[i])); + has_bv_arrays = true; + } + } + + expr_ref t(m_manager); + t = m_manager.mk_app(f, num, args); + + if (is_bv_array(t)) { + // From [1]: For every array term t we create a fresh uninterpreted function f_t. + f_t = mk_uf_for_array(t); + result = m_array_util.mk_as_array(m_manager.get_sort(t), f_t); + res = BR_DONE; + } + else if (has_bv_arrays) { + result = t; + res = BR_DONE; + } + else + res = BR_FAILED; + } + else if (m_array_util.get_family_id() == f->get_family_id()) { + TRACE("bvarray2uf_rw", tout << "APP: " << f->get_name() << std::endl; ); + + if (m_array_util.is_select(f)) { + SASSERT(num == 2); + expr * t = args[0]; + expr * i = args[1]; + TRACE("bvarray2uf_rw", tout << + "select; array: " << mk_ismt2_pp(t, m()) << + " index: " << mk_ismt2_pp(i, m()) << std::endl;); + + if (!is_bv_array(t)) + res = BR_FAILED; + else { + // From [1]: Then, we replace terms of the form select(t, i) with f_t(i). + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + result = m_manager.mk_app(f_t, i); + res = BR_DONE; + } + } + else { + if (!is_bv_array(f->get_range())) + res = BR_FAILED; + else { + if (m_array_util.is_const(f)) { + SASSERT(num == 1); + expr_ref t(m_manager.mk_app(f, num, args), m_manager); + expr * v = args[0]; + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + + result = m_array_util.mk_as_array(f->get_range(), f_t); + res = BR_DONE; + + // Add \forall x . f_t(x) = v + sort * sorts[1] = { get_index_sort(f->get_range()) }; + symbol names[1] = { symbol("x") }; + var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); + + expr_ref body(m_manager); + body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), v); + + expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); + extra_assertions.push_back(frllx); + } + else if (m_array_util.is_as_array(f)) { + res = BR_FAILED; + } + else if (m_array_util.is_map(f)) { + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_ast()); + expr_ref t(m_manager.mk_app(f, num, args), m_manager); + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + func_decl_ref map_f(to_func_decl(f->get_parameter(0).get_ast()), m_manager); + + func_decl_ref_vector ss(m_manager); + for (unsigned i = 0; i < num; i++) { + SASSERT(m_array_util.is_array(args[i])); + func_decl_ref fd(mk_uf_for_array(args[i]), m_manager); + ss.push_back(fd); + } + + // Add \forall x . f_t(x) = map_f(a[x], b[x], ...) + sort * sorts[1] = { get_index_sort(f->get_range()) }; + symbol names[1] = { symbol("x") }; + var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); + + expr_ref_vector new_args(m_manager); + for (unsigned i = 0; i < num; i++) + new_args.push_back(m_manager.mk_app(ss[i].get(), x.get())); + + expr_ref body(m_manager); + body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), + m_manager.mk_app(map_f, num, new_args.c_ptr())); + + expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); + extra_assertions.push_back(frllx); + + result = m_array_util.mk_as_array(f->get_range(), f_t); + res = BR_DONE; + } + else if (m_array_util.is_store(f)) { + SASSERT(num == 3); + expr * s = args[0]; + expr * i = args[1]; + expr * v = args[2]; + TRACE("bvarray2uf_rw", tout << + "store; array: " << mk_ismt2_pp(s, m()) << + " index: " << mk_ismt2_pp(i, m()) << + " value: " << mk_ismt2_pp(v, m()) << std::endl;); + if (!is_bv_array(s)) + res = BR_FAILED; + else { + expr_ref t(m_manager.mk_app(f, num, args), m_manager); + // From [1]: For every term t of the form store(s, i, v), we add the universal + // formula \forall x . x = i \vee f_t(x) = f_s(x), and the ground atom f_t(i) = v. + func_decl_ref f_s(mk_uf_for_array(s), m_manager); + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + + result = m_array_util.mk_as_array(f->get_range(), f_t); + res = BR_DONE; + + sort * sorts[1] = { get_index_sort(f->get_range()) }; + symbol names[1] = { symbol("x") }; + var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); + + expr_ref body(m_manager); + body = m_manager.mk_or(m_manager.mk_eq(x, i), + m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), + m_manager.mk_app(f_s, x.get()))); + + expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); + extra_assertions.push_back(frllx); + + expr_ref ground_atom(m_manager); + ground_atom = m_manager.mk_eq(m_manager.mk_app(f_t, i), v); + extra_assertions.push_back(ground_atom); + TRACE("bvarray2uf_rw", tout << "ground atom: " << mk_ismt2_pp(ground_atom, m()) << std::endl; ); + } + } + else { + NOT_IMPLEMENTED_YET(); + res = BR_FAILED; + } + } + } + } + + CTRACE("bvarray2uf_rw", res==BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; ); + return res; +} + +bool bvarray2uf_rewriter_cfg::pre_visit(expr * t) +{ + TRACE("bvarray2uf_rw_q", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;); + + if (is_quantifier(t)) { + quantifier * q = to_quantifier(t); + TRACE("bvarray2uf_rw_q", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;); + sort_ref_vector new_bindings(m_manager); + for (unsigned i = 0; i < q->get_num_decls(); i++) + new_bindings.push_back(q->get_decl_sort(i)); + SASSERT(new_bindings.size() == q->get_num_decls()); + m_bindings.append(new_bindings); + } + return true; +} + +bool bvarray2uf_rewriter_cfg::reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + unsigned curr_sz = m_bindings.size(); + SASSERT(old_q->get_num_decls() <= curr_sz); + unsigned num_decls = old_q->get_num_decls(); + unsigned old_sz = curr_sz - num_decls; + string_buffer<> name_buffer; + ptr_buffer new_decl_sorts; + sbuffer new_decl_names; + for (unsigned i = 0; i < num_decls; i++) { + symbol const & n = old_q->get_decl_name(i); + sort * s = old_q->get_decl_sort(i); + + NOT_IMPLEMENTED_YET(); + + } + result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(), + new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(), + old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); + result_pr = 0; + m_bindings.shrink(old_sz); + TRACE("bvarray2uf_rw_q", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << + mk_ismt2_pp(old_q->get_expr(), m()) << std::endl << + " new body: " << mk_ismt2_pp(new_body, m()) << std::endl; + tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;); + return true; +} + +bool bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { + if (t->get_idx() >= m_bindings.size()) + return false; + + expr_ref new_exp(m()); + sort * s = t->get_sort(); + + NOT_IMPLEMENTED_YET(); + + result = new_exp; + result_pr = 0; + TRACE("bvarray2uf_rw_q", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;); + return true; +} diff --git a/src/tactic/bv/bvarray2uf_rewriter.h b/src/tactic/bv/bvarray2uf_rewriter.h new file mode 100644 index 000000000..e65340cc3 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_rewriter.h @@ -0,0 +1,87 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + bvarray2uf_rewriter.h + +Abstract: + + Rewriter that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ +#ifndef BVARRAY2UF_REWRITER_H_ +#define BVARRAY2UF_REWRITER_H_ + +#include"rewriter_def.h" +#include"extension_model_converter.h" +#include"filter_model_converter.h" + +class bvarray2uf_rewriter_cfg : public default_rewriter_cfg { + ast_manager & m_manager; + expr_ref_vector m_out; + sort_ref_vector m_bindings; + bv_util m_bv_util; + array_util m_array_util; + extension_model_converter * m_emc; + filter_model_converter * m_fmc; + + obj_map m_arrays_fs; + +public: + bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p); + ~bvarray2uf_rewriter_cfg(); + + ast_manager & m() const { return m_manager; } + void updt_params(params_ref const & p) {} + + void reset(); + + bool pre_visit(expr * t); + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr); + + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr); + + bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr); + + expr_ref_vector extra_assertions; + + void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_emc = emc; m_fmc = fmc; } + +protected: + sort * get_index_sort(expr * e); + sort * get_index_sort(sort * s); + sort * get_value_sort(expr * e); + sort * get_value_sort(sort * s); + bool is_bv_array(expr * e); + bool is_bv_array(sort * e); + func_decl_ref mk_uf_for_array(expr * e); +}; + +template class rewriter_tpl; + +struct bvarray2uf_rewriter : public rewriter_tpl { + bvarray2uf_rewriter_cfg m_cfg; + bvarray2uf_rewriter(ast_manager & m, params_ref const & p) : + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, p) { + } + + void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_cfg.set_mcs(emc, fmc); } +}; + +#endif + diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp new file mode 100644 index 000000000..6bf1324f1 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -0,0 +1,168 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + bvarray2uf_tactic.cpp + +Abstract: + + Tactic that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ +#include"tactical.h" +#include"bv_decl_plugin.h" +#include"expr_replacer.h" +#include"extension_model_converter.h" +#include"filter_model_converter.h" +#include"ast_smt2_pp.h" + +#include"bvarray2uf_tactic.h" +#include"bvarray2uf_rewriter.h" + +class bvarray2uf_tactic : public tactic { + + struct imp { + ast_manager & m_manager; + bool m_produce_models; + bool m_produce_proofs; + bool m_produce_cores; + volatile bool m_cancel; + bvarray2uf_rewriter m_rw; + + ast_manager & m() { return m_manager; } + + imp(ast_manager & m, params_ref const & p) : + m_manager(m), + m_produce_models(false), + m_cancel(false), + m_produce_proofs(false), + m_produce_cores(false), + m_rw(m, p) { + updt_params(p); + } + + void set_cancel(bool f) { + m_cancel = f; + } + + void checkpoint() { + if (m_cancel) + throw tactic_exception(TACTIC_CANCELED_MSG); + } + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) + { + SASSERT(g->is_well_sorted()); + tactic_report report("bvarray2uf", *g); + mc = 0; pc = 0; core = 0; result.reset(); + fail_if_proof_generation("bvarray2uf", g); + fail_if_unsat_core_generation("bvarray2uf", g); + + TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); ); + m_produce_models = g->models_enabled(); + + if (m_produce_models) { + extension_model_converter * emc = alloc(extension_model_converter, m_manager); + filter_model_converter * fmc = alloc(filter_model_converter, m_manager); + mc = concat(emc, fmc); + m_rw.set_mcs(emc, fmc); + + } + + + m_rw.reset(); + expr_ref new_curr(m_manager); + proof_ref new_pr(m_manager); + unsigned size = g->size(); + for (unsigned idx = 0; idx < size; idx++) { + if (g->inconsistent()) + break; + expr * curr = g->form(idx); + m_rw(curr, new_curr, new_pr); + //if (m_produce_proofs) { + // proof * pr = g->pr(idx); + // new_pr = m.mk_modus_ponens(pr, new_pr); + //} + g->update(idx, new_curr, new_pr, g->dep(idx)); + } + + for (unsigned i = 0; i < m_rw.m_cfg.extra_assertions.size(); i++) + g->assert_expr(m_rw.m_cfg.extra_assertions[i].get()); + + g->inc_depth(); + result.push_back(g.get()); + TRACE("bvarray2uf", tout << "After: " << std::endl; g->display(tout);); + SASSERT(g->is_well_sorted()); + } + + void updt_params(params_ref const & p) { + } + }; + + imp * m_imp; + params_ref m_params; + +public: + bvarray2uf_tactic(ast_manager & m, params_ref const & p) : + m_params(p) { + m_imp = alloc(imp, m, p); + } + + virtual tactic * translate(ast_manager & m) { + return alloc(bvarray2uf_tactic, m, m_params); + } + + virtual ~bvarray2uf_tactic() { + dealloc(m_imp); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_imp->updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + insert_produce_models(r); + } + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + (*m_imp)(in, result, mc, pc, core); + } + + virtual void cleanup() { + ast_manager & m = m_imp->m(); + imp * d = alloc(imp, m, m_params); + #pragma omp critical (tactic_cancel) + { + std::swap(d, m_imp); + } + dealloc(d); + } + + virtual void set_cancel(bool f) { + if (m_imp) + m_imp->set_cancel(f); + } + +}; + + +tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(bvarray2uf_tactic, m, p)); +} diff --git a/src/tactic/bv/bvarray2uf_tactic.h b/src/tactic/bv/bvarray2uf_tactic.h new file mode 100644 index 000000000..608a831e0 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_tactic.h @@ -0,0 +1,33 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + bvarray2ufbvarray2uf_tactic.h + +Abstract: + + Tactic that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ +#ifndef BV_ARRAY2UF_TACTIC_H_ +#define BV_ARRAY2UF_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf_tactic(m, p)") +*/ + + +#endif \ No newline at end of file From 806016c315ca8969bb34c340930337df6de34b1f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Nov 2015 14:11:39 +0000 Subject: [PATCH 25/53] build fix --- src/tactic/bv/bvarray2uf_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp index 83038cfa9..6245ed2bc 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.cpp +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -361,7 +361,7 @@ bool bvarray2uf_rewriter_cfg::reduce_quantifier(quantifier * old_q, return true; } -bool bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { +bool bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { if (t->get_idx() >= m_bindings.size()) return false; From 4cb96bfe76a1b63209f42d8186d48ea0929c0f0b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Nov 2015 15:55:01 +0000 Subject: [PATCH 26/53] Fixed assertion failure in fpa2bv_converter. Partially addresses #307 --- src/ast/fpa/fpa2bv_converter.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 4ee6366f0..19b07035f 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2648,9 +2648,8 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const SASSERT(num == 2); SASSERT(m_util.is_float(f->get_range())); - SASSERT(m_bv_util.is_bv(args[0])); - SASSERT(m_bv_util.is_bv(args[1])); SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + SASSERT(m_bv_util.is_bv(args[1])); expr_ref bv_rm(m), x(m); bv_rm = to_app(args[0])->get_arg(0); From 954400cfa27cedf508b18da146e17973e5dbbc6f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Nov 2015 16:35:08 +0000 Subject: [PATCH 27/53] whitespace --- src/api/api_solver_old.cpp | 48 +++++++++++++++++++------------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index 7e994a0e2..7fa469718 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -34,7 +34,7 @@ extern "C" { mk_c(c)->push(); Z3_CATCH; } - + void Z3_API Z3_pop(Z3_context c, unsigned num_scopes) { Z3_TRY; LOG_Z3_pop(c, num_scopes); @@ -62,7 +62,7 @@ extern "C" { Z3_TRY; LOG_Z3_assert_cnstr(c, a); RESET_ERROR_CODE(); - CHECK_FORMULA(a,); + CHECK_FORMULA(a,); mk_c(c)->assert_cnstr(to_expr(a)); Z3_CATCH; } @@ -81,11 +81,11 @@ extern "C" { result = mk_c(c)->check(_m); if (m) { if (_m) { - Z3_model_ref * m_ref = alloc(Z3_model_ref); + Z3_model_ref * m_ref = alloc(Z3_model_ref); m_ref->m_model = _m; // Must bump reference counter for backward compatibility reasons. // Don't need to invoke save_object, since the counter was bumped - m_ref->inc_ref(); + m_ref->inc_ref(); *m = of_model(m_ref); } else { @@ -100,21 +100,21 @@ extern "C" { RETURN_Z3_check_and_get_model static_cast(result); Z3_CATCH_RETURN(Z3_L_UNDEF); } - + Z3_lbool Z3_API Z3_check(Z3_context c) { Z3_TRY; - // This is just syntax sugar... - RESET_ERROR_CODE(); + // This is just syntax sugar... + RESET_ERROR_CODE(); CHECK_SEARCHING(c); Z3_lbool r = Z3_check_and_get_model(c, 0); return r; Z3_CATCH_RETURN(Z3_L_UNDEF); } - - Z3_lbool Z3_API Z3_check_assumptions(Z3_context c, - unsigned num_assumptions, Z3_ast const assumptions[], - Z3_model * m, Z3_ast* proof, + + Z3_lbool Z3_API Z3_check_assumptions(Z3_context c, + unsigned num_assumptions, Z3_ast const assumptions[], + Z3_model * m, Z3_ast* proof, unsigned* core_size, Z3_ast core[]) { Z3_TRY; LOG_Z3_check_assumptions(c, num_assumptions, assumptions, m, proof, core_size, core); @@ -130,11 +130,11 @@ extern "C" { model_ref _m; mk_c(c)->get_smt_kernel().get_model(_m); if (_m) { - Z3_model_ref * m_ref = alloc(Z3_model_ref); + Z3_model_ref * m_ref = alloc(Z3_model_ref); m_ref->m_model = _m; // Must bump reference counter for backward compatibility reasons. // Don't need to invoke save_object, since the counter was bumped - m_ref->inc_ref(); + m_ref->inc_ref(); *m = of_model(m_ref); } else { @@ -159,7 +159,7 @@ extern "C" { else if (proof) { *proof = 0; // breaks abstraction. } - RETURN_Z3_check_assumptions static_cast(result); + RETURN_Z3_check_assumptions static_cast(result); Z3_CATCH_RETURN(Z3_L_UNDEF); } @@ -185,7 +185,7 @@ extern "C" { symbol const& get_label() const { return m_label; } expr* get_literal() { return m_literal.get(); } }; - + typedef vector labels; Z3_literals Z3_API Z3_get_relevant_labels(Z3_context c) { @@ -196,7 +196,7 @@ extern "C" { ast_manager& m = mk_c(c)->m(); expr_ref_vector lits(m); mk_c(c)->get_smt_kernel().get_relevant_labels(0, labl_syms); - mk_c(c)->get_smt_kernel().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits); + mk_c(c)->get_smt_kernel().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits); labels* lbls = alloc(labels); SASSERT(labl_syms.size() == lits.size()); for (unsigned i = 0; i < lits.size(); ++i) { @@ -212,12 +212,12 @@ extern "C" { RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); expr_ref_vector lits(m); - mk_c(c)->get_smt_kernel().get_relevant_literals(lits); + mk_c(c)->get_smt_kernel().get_relevant_literals(lits); labels* lbls = alloc(labels); for (unsigned i = 0; i < lits.size(); ++i) { lbls->push_back(labeled_literal(m,lits[i].get())); } - RETURN_Z3(reinterpret_cast(lbls)); + RETURN_Z3(reinterpret_cast(lbls)); Z3_CATCH_RETURN(0); } @@ -227,12 +227,12 @@ extern "C" { RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); expr_ref_vector lits(m); - mk_c(c)->get_smt_kernel().get_guessed_literals(lits); + mk_c(c)->get_smt_kernel().get_guessed_literals(lits); labels* lbls = alloc(labels); for (unsigned i = 0; i < lits.size(); ++i) { lbls->push_back(labeled_literal(m,lits[i].get())); } - RETURN_Z3(reinterpret_cast(lbls)); + RETURN_Z3(reinterpret_cast(lbls)); Z3_CATCH_RETURN(0); } @@ -248,7 +248,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_num_literals(c, lbls); RESET_ERROR_CODE(); - return reinterpret_cast(lbls)->size(); + return reinterpret_cast(lbls)->size(); Z3_CATCH_RETURN(0); } @@ -256,7 +256,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_label_symbol(c, lbls, idx); RESET_ERROR_CODE(); - return of_symbol((*reinterpret_cast(lbls))[idx].get_label()); + return of_symbol((*reinterpret_cast(lbls))[idx].get_label()); Z3_CATCH_RETURN(0); } @@ -274,7 +274,7 @@ extern "C" { Z3_TRY; LOG_Z3_disable_literal(c, lbls, idx); RESET_ERROR_CODE(); - (*reinterpret_cast(lbls))[idx].disable(); + (*reinterpret_cast(lbls))[idx].disable(); Z3_CATCH; } @@ -348,4 +348,4 @@ void Z3_display_statistics(Z3_context c, std::ostream& s) { void Z3_display_istatistics(Z3_context c, std::ostream& s) { mk_c(c)->get_smt_kernel().display_istatistics(s); } - + From 15c48eeaf9352a73515e0b6badf042879a6f19dc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Nov 2015 16:42:46 +0000 Subject: [PATCH 28/53] Fix for timeout/rlimit in deprecated solver API. Partially fixes #307. --- src/api/api_solver_old.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index 7fa469718..fbd57ad97 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -23,6 +23,8 @@ Revision History: #include"api_context.h" #include"api_model.h" #include"cancel_eh.h" +#include"scoped_timer.h" +#include"rlimit.h" extern "C" { @@ -75,8 +77,13 @@ extern "C" { cancel_eh eh(mk_c(c)->get_smt_kernel()); api::context::set_interruptable si(*(mk_c(c)), eh); flet _model(mk_c(c)->fparams().m_model, true); + unsigned timeout = mk_c(c)->params().m_timeout; + unsigned rlimit = mk_c(c)->params().m_rlimit; lbool result; try { + scoped_timer timer(timeout, &eh); + scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); + model_ref _m; result = mk_c(c)->check(_m); if (m) { From 27dcd8c5b6bd6fdb9c2b1acd724346618bac2113 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Nov 2015 17:15:04 +0000 Subject: [PATCH 29/53] Fix for python decoding of command line output strings Fixes #302 --- scripts/mk_util.py | 2 +- scripts/update_api.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0baed2968..225a38c04 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -90,7 +90,7 @@ FPMATH="Default" FPMATH_FLAGS="-mfpmath=sse -msse -msse2" def check_output(cmd): - return (subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).decode("utf-8").rstrip('\r\n') + return (subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).decode(sys.stdout.encoding).rstrip('\r\n') def git_hash(): try: diff --git a/scripts/update_api.py b/scripts/update_api.py index 0b6ddfb32..1ad85d228 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -96,7 +96,7 @@ if sys.version < '3': return s else: def _to_pystr(s): - return s.decode('utf-8') + return s.decode(sys.stdout.encoding) def init(PATH): global _lib From 0a26bcf14c5db9697d0bba9d6e92f095a19e1285 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Nov 2015 15:12:08 -0500 Subject: [PATCH 30/53] ensure unique symbols when MaxSAT problems are extracted from linear objectives such that multiple objectives can be supported. Fixes issue #308 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 49b5f988f..1b4b1e7bc 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -770,7 +770,7 @@ namespace opt { tout << "offset: " << offset << "\n"; ); std::ostringstream out; - out << mk_pp(orig_term, m); + out << mk_pp(orig_term, m) << ":" << index; id = symbol(out.str().c_str()); return true; } @@ -793,7 +793,7 @@ namespace opt { } neg = true; std::ostringstream out; - out << mk_pp(orig_term, m); + out << mk_pp(orig_term, m) << ":" << index; id = symbol(out.str().c_str()); return true; } @@ -812,7 +812,7 @@ namespace opt { } neg = is_max; std::ostringstream out; - out << mk_pp(orig_term, m); + out << mk_pp(orig_term, m) << ":" << index; id = symbol(out.str().c_str()); return true; } From f880433a692700502f2c4f3704afbe42a529a549 Mon Sep 17 00:00:00 2001 From: "Bernhard F. Brodowsky" Date: Sat, 14 Nov 2015 15:47:47 +0100 Subject: [PATCH 31/53] Fixed typo in warning message. --- src/parsers/util/pattern_validation.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parsers/util/pattern_validation.cpp b/src/parsers/util/pattern_validation.cpp index fe3292312..3d59c2213 100644 --- a/src/parsers/util/pattern_validation.cpp +++ b/src/parsers/util/pattern_validation.cpp @@ -88,7 +88,7 @@ bool pattern_validator::process(uint_set & found_vars, unsigned num_bindings, un if (!f.m_result) return false; if (!f.m_found_a_var) { - warning_msg("pattern does contain any variable."); + warning_msg("pattern does not contain any variable."); return false; } return true; From 639dfc4b308616955adcef6828f63e9f0b35b003 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 14 Nov 2015 15:06:55 +0000 Subject: [PATCH 32/53] fix for string decoding in build scripts --- scripts/mk_util.py | 7 ++++++- scripts/update_api.py | 6 +++++- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 225a38c04..66ccb7b65 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -90,7 +90,12 @@ FPMATH="Default" FPMATH_FLAGS="-mfpmath=sse -msse -msse2" def check_output(cmd): - return (subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).decode(sys.stdout.encoding).rstrip('\r\n') + out = subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0] + if out != None: + enc = sys.stdout.encoding + if enc != None: out.decode(enc).rstrip('\r\n') + else: out.rstrip('\r\n') + else: "" def git_hash(): try: diff --git a/scripts/update_api.py b/scripts/update_api.py index 1ad85d228..85ee296e3 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -96,7 +96,11 @@ if sys.version < '3': return s else: def _to_pystr(s): - return s.decode(sys.stdout.encoding) + if s != None: + enc = sys.stdout.encoding + if enc != None: s.decode(enc) + else: s + else: "" def init(PATH): global _lib From 05eb78ccacc0a41100de91a275c165f81bdef1ac Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 14 Nov 2015 15:42:49 +0000 Subject: [PATCH 33/53] fix for string decoding in build scripts --- scripts/mk_util.py | 7 ++++--- scripts/update_api.py | 7 ++++--- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 66ccb7b65..0b924c21f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -93,9 +93,10 @@ def check_output(cmd): out = subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0] if out != None: enc = sys.stdout.encoding - if enc != None: out.decode(enc).rstrip('\r\n') - else: out.rstrip('\r\n') - else: "" + if enc != None: return out.decode(enc).rstrip('\r\n') + else: return out.rstrip('\r\n') + else: + return "" def git_hash(): try: diff --git a/scripts/update_api.py b/scripts/update_api.py index 85ee296e3..bb5935a1e 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -98,9 +98,10 @@ else: def _to_pystr(s): if s != None: enc = sys.stdout.encoding - if enc != None: s.decode(enc) - else: s - else: "" + if enc != None: return s.decode(enc) + else: return s + else: + return "" def init(PATH): global _lib From 6b5e49c4a15ff5c4ca132311e2df8a4c7c6d14c6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 14 Nov 2015 17:25:18 +0000 Subject: [PATCH 34/53] Added checks for uint parameter values in context_params --- src/cmd_context/context_params.cpp | 33 ++++++++++++++++++++++-------- src/cmd_context/context_params.h | 7 ++++--- 2 files changed, 29 insertions(+), 11 deletions(-) diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 30b5a7c4b..091207a93 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -48,7 +48,26 @@ void context_params::set_bool(bool & opt, char const * param, char const * value } else { std::stringstream strm; - strm << "invalid value '" << value << "' for Boolean parameter '" << param; + strm << "invalid value '" << value << "' for Boolean parameter '" << param << "'"; + throw default_exception(strm.str()); + } +} + +void context_params::set_uint(unsigned & opt, char const * param, char const * value) { + bool is_uint = true; + size_t sz = strlen(value); + for (unsigned i = 0; i < sz; i++) { + if (!(value[i] >= '0' && value[i] <= '9')) + is_uint = false; + } + + if (is_uint) { + long val = strtol(value, 0, 10); + opt = static_cast(val); + } + else { + std::stringstream strm; + strm << "invalid value '" << value << "' for unsigned int parameter '" << param << "'"; throw default_exception(strm.str()); } } @@ -63,12 +82,10 @@ void context_params::set(char const * param, char const * value) { p[i] = '_'; } if (p == "timeout") { - long val = strtol(value, 0, 10); - m_timeout = static_cast(val); + set_uint(m_timeout, param, value); } else if (p == "rlimit") { - long val = strtol(value, 0, 10); - m_rlimit = static_cast(val); + set_uint(m_rlimit, param, value); } else if (p == "type_check" || p == "well_sorted_check") { set_bool(m_well_sorted_check, param, value); @@ -110,7 +127,7 @@ void context_params::set(char const * param, char const * value) { strm << "unknown parameter '" << p << "'\n"; strm << "Legal parameters are:\n"; d.display(strm, 2, false, false); - throw default_exception(strm.str()); + throw default_exception(strm.str()); } } @@ -174,8 +191,8 @@ void context_params::get_solver_params(ast_manager const & m, params_ref & p, bo } ast_manager * context_params::mk_ast_manager() { - ast_manager * r = alloc(ast_manager, - m_proof ? PGM_FINE : PGM_DISABLED, + ast_manager * r = alloc(ast_manager, + m_proof ? PGM_FINE : PGM_DISABLED, m_trace ? m_trace_file_name.c_str() : 0); if (m_smtlib2_compliant) r->enable_int_real_coercions(false); diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index 2c75b5743..40b6c9482 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -25,7 +25,8 @@ class ast_manager; class context_params { void set_bool(bool & opt, char const * param, char const * value); - + void set_uint(unsigned & opt, char const * param, char const * value); + public: bool m_auto_config; bool m_proof; @@ -50,7 +51,7 @@ public: /* REG_PARAMS('context_params::collect_param_descrs') */ - + /** \brief Goodies for extracting parameters for creating a solver object. */ @@ -64,7 +65,7 @@ public: Example: auto_config */ params_ref merge_default_params(params_ref const & p); - + /** \brief Create an AST manager using this configuration. */ From c2108f74f1e5c5ab96c6e4cc189ccbc55dca339a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Nov 2015 10:35:06 -0800 Subject: [PATCH 35/53] fix uninitialized variable Signed-off-by: Nikolaj Bjorner --- src/opt/maxsmt.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 2d3a60ea8..1bb521923 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -154,7 +154,7 @@ namespace opt { m_soft_constraints(m), m_answer(m) {} lbool maxsmt::operator()() { - lbool is_sat; + lbool is_sat = l_undef; m_msolver = 0; symbol const& maxsat_engine = m_c.maxsat_engine(); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); From f537167080b52b9793e0f310ee824ac745688ca4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Nov 2015 18:41:16 -0800 Subject: [PATCH 36/53] Fix bug #311 Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 20 +++++++++++++++----- src/muz/pdr/pdr_context.h | 2 +- 2 files changed, 16 insertions(+), 6 deletions(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index d349da4ec..a55d0e648 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -738,6 +738,7 @@ namespace pdr { // model_node void model_node::set_closed() { + TRACE("pdr", tout << state() << "\n";); pt().close(state()); m_closed = true; } @@ -928,7 +929,7 @@ namespace pdr { model_node* p = n.parent(); while (p) { if (p->state() == n.state()) { - TRACE("pdr", tout << "repeated\n";); + TRACE("pdr", tout << n.state() << "repeated\n";); return true; } p = p->parent(); @@ -1018,6 +1019,11 @@ namespace pdr { SASSERT(n1->children().empty()); enqueue_leaf(n1); } + + if (!nodes.empty() && n.get_model_ptr() && backtrack) { + model_ref mr(n.get_model_ptr()); + nodes[0]->set_model(mr); + } if (nodes.empty()) { cache(n).remove(n.state()); } @@ -1149,17 +1155,21 @@ namespace pdr { ast_manager& m = n->pt().get_manager(); if (!n->get_model_ptr()) { if (models.find(n->state(), md)) { - TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";); + TRACE("pdr", tout << n->state() << "\n";); model_ref mr(md); n->set_model(mr); datalog::rule const* rule = rules.find(n->state()); n->set_rule(rule); } else { + TRACE("pdr", tout << "no model for " << n->state() << "\n";); IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0); - verbose_stream() << mk_pp(n->state(), m) << "\n";); + verbose_stream() << n->state() << "\n";); } } + else { + TRACE("pdr", tout << n->state() << "\n";); + } todo.pop_back(); todo.append(n->children().size(), n->children().c_ptr()); } @@ -2027,11 +2037,11 @@ namespace pdr { switch (expand_state(n, cube, uses_level)) { case l_true: if (n.level() == 0) { - TRACE("pdr", tout << "reachable at level 0\n";); + TRACE("pdr", n.display(tout << "reachable at level 0\n", 0);); close_node(n); } else { - TRACE("pdr", tout << "node: " << &n << "\n";); + TRACE("pdr", n.display(tout, 0);); create_children(n); } break; diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 7cba1e0c5..35b9067b2 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -240,7 +240,7 @@ namespace pdr { void check_pre_closed(); void set_closed(); void set_open(); - void set_pre_closed() { m_closed = true; } + void set_pre_closed() { TRACE("pdr", tout << state() << "\n";); m_closed = true; } void reset() { m_children.reset(); } void set_rule(datalog::rule const* r) { m_rule = r; } From 3a3e1796e299633d6cfe79795bc132820b6f8e4d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Nov 2015 18:42:11 -0800 Subject: [PATCH 37/53] Fix bug #311. update tabs Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index a55d0e648..4cdc76ede 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -1162,14 +1162,14 @@ namespace pdr { n->set_rule(rule); } else { - TRACE("pdr", tout << "no model for " << n->state() << "\n";); + TRACE("pdr", tout << "no model for " << n->state() << "\n";); IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0); verbose_stream() << n->state() << "\n";); } } - else { - TRACE("pdr", tout << n->state() << "\n";); - } + else { + TRACE("pdr", tout << n->state() << "\n";); + } todo.pop_back(); todo.append(n->children().size(), n->children().c_ptr()); } @@ -2037,11 +2037,11 @@ namespace pdr { switch (expand_state(n, cube, uses_level)) { case l_true: if (n.level() == 0) { - TRACE("pdr", n.display(tout << "reachable at level 0\n", 0);); + TRACE("pdr", n.display(tout << "reachable at level 0\n", 0);); close_node(n); } else { - TRACE("pdr", n.display(tout, 0);); + TRACE("pdr", n.display(tout, 0);); create_children(n); } break; From b8e4871d9efa8bf966cb693a00bf1c451aca5b79 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Nov 2015 10:53:00 -0800 Subject: [PATCH 38/53] disable bottom-up coi filtering when relations contain facts. bug reported by SeanMcL Signed-off-by: Nikolaj Bjorner --- src/muz/dataflow/dataflow.h | 1 + src/muz/transforms/dl_mk_coi_filter.cpp | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/muz/dataflow/dataflow.h b/src/muz/dataflow/dataflow.h index 9e100121a..1e52c5f93 100644 --- a/src/muz/dataflow/dataflow.h +++ b/src/muz/dataflow/dataflow.h @@ -87,6 +87,7 @@ namespace datalog { for (func_decl_set::iterator I = output_preds.begin(), E = output_preds.end(); I != E; ++I) { func_decl* sym = *I; + TRACE("dl", tout << sym->get_name() << "\n";); const rule_vector& output_rules = m_rules.get_predicate_rules(sym); for (unsigned i = 0; i < output_rules.size(); ++i) { m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, output_rules[i]); diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 67b88724c..c452e2611 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -41,6 +41,9 @@ namespace datalog { bool new_tail = false; bool contained = true; for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) { + if (m_context.has_facts(r->get_decl(i))) { + return 0; + } if (r->is_neg_tail(i)) { if (!engine.get_fact(r->get_decl(i)).is_reachable()) { if (!new_tail) { From 706a037bf4bc20e37f85978b6ae8912cb9f32e67 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 16 Nov 2015 15:16:50 +0100 Subject: [PATCH 39/53] Python 3.x string decoding fix --- scripts/update_api.py | 2 +- src/api/python/z3printer.py | 8 +++++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index bb5935a1e..6e7b6d5f7 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -99,7 +99,7 @@ else: if s != None: enc = sys.stdout.encoding if enc != None: return s.decode(enc) - else: return s + else: return s.decode('ascii') else: return "" diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py index 5116046dd..2a242865e 100644 --- a/src/api/python/z3printer.py +++ b/src/api/python/z3printer.py @@ -1157,7 +1157,13 @@ def set_pp_option(k, v): def obj_to_string(a): out = io.StringIO() _PP(out, _Formatter(a)) - return out.getvalue() + r = out.getvalue() + if sys.version < '3': + return r + else: + enc = sys.stdout.encoding + if enc != None: return r.decode(enc) + return r _html_out = None From e8d37dba9cce90574ed5c9ad640968c0362c5c82 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 16 Nov 2015 21:58:17 +0100 Subject: [PATCH 40/53] Added comments for quantifier constructors. Fixes #319. --- src/api/dotnet/Context.cs | 26 ++++++++++++++++-- src/api/java/Context.java | 58 +++++++++++++++++++++++---------------- 2 files changed, 57 insertions(+), 27 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 25c399d68..d56ba4af1 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2613,8 +2613,13 @@ namespace Microsoft.Z3 /// is an array of patterns, is an array /// with the sorts of the bound variables, is an array with the /// 'names' of the bound variables, and is the body of the - /// quantifier. Quantifiers are associated with weights indicating - /// the importance of using the quantifier during instantiation. + /// quantifier. Quantifiers are associated with weights indicating the importance of + /// using the quantifier during instantiation. + /// Note that the bound variables are de-Bruijn indices created using . + /// Z3 applies the convention that the last element in and + /// refers to the variable with index 0, the second to last element + /// of and refers to the variable + /// with index 1, etc. /// /// the sorts of the bound variables. /// names of the bound variables @@ -2644,6 +2649,11 @@ namespace Microsoft.Z3 /// /// Create a universal Quantifier. /// + /// + /// Creates a universal quantifier using a list of constants that will + /// form the set of bound variables. + /// + /// public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { Contract.Requires(body != null); @@ -2659,7 +2669,10 @@ namespace Microsoft.Z3 /// /// Create an existential Quantifier. /// - /// + /// + /// Creates an existential quantifier using de-Brujin indexed variables. + /// (). + /// public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { Contract.Requires(sorts != null); @@ -2678,6 +2691,11 @@ namespace Microsoft.Z3 /// /// Create an existential Quantifier. /// + /// + /// Creates an existential quantifier using a list of constants that will + /// form the set of bound variables. + /// + /// public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { Contract.Requires(body != null); @@ -2693,6 +2711,7 @@ namespace Microsoft.Z3 /// /// Create a Quantifier. /// + /// public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { Contract.Requires(body != null); @@ -2716,6 +2735,7 @@ namespace Microsoft.Z3 /// /// Create a Quantifier. /// + /// public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { Contract.Requires(body != null); diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 0f9a85799..4d8484ced 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -433,8 +433,8 @@ public class Context extends IDisposable /** * Creates a fresh function declaration with a name prefixed with * {@code prefix}. - * @see mkFuncDecl(String,Sort,Sort) - * @see mkFuncDecl(String,Sort[],Sort) + * @see #mkFuncDecl(String,Sort,Sort) + * @see #mkFuncDecl(String,Sort[],Sort) **/ public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range) @@ -1722,9 +1722,9 @@ public class Context extends IDisposable **/ public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2) { - checkContextMatch(arg1); - checkContextMatch(arg2); - return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); + checkContextMatch(arg1); + checkContextMatch(arg2); + return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); } @@ -2025,6 +2025,7 @@ public class Context extends IDisposable /** * Create a universal Quantifier. + * * @param sorts the sorts of the bound variables. * @param names names of the bound variables * @param body the body of the quantifier. @@ -2034,17 +2035,22 @@ public class Context extends IDisposable * @param quantifierID optional symbol to track quantifier. * @param skolemID optional symbol to track skolem constants. * - * Remarks: Creates a forall formula, where - * {@code weight"/> is the weight, (m_rule); } @@ -830,7 +848,7 @@ namespace pdr { } r0 = get_rule(); app_ref_vector& inst = pt().get_inst(r0); - TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";); + TRACE("pdr", tout << state() << " instance: " << inst.size() << "\n";); for (unsigned i = 0; i < inst.size(); ++i) { expr* v; if (model.find(inst[i].get(), v)) { @@ -852,7 +870,7 @@ namespace pdr { for (unsigned i = 0; i < indent; ++i) out << " "; out << m_level << " " << m_pt.head()->get_name() << " " << (m_closed?"closed":"open") << "\n"; for (unsigned i = 0; i < indent; ++i) out << " "; - out << " " << mk_pp(m_state, m_state.get_manager(), indent) << "\n"; + out << " " << mk_pp(m_state, m_state.get_manager(), indent) << " " << m_state->get_id() << "\n"; for (unsigned i = 0; i < children().size(); ++i) { children()[i]->display(out, indent + 1); } @@ -925,17 +943,6 @@ namespace pdr { } } - bool model_search::is_repeated(model_node& n) const { - model_node* p = n.parent(); - while (p) { - if (p->state() == n.state()) { - TRACE("pdr", tout << n.state() << "repeated\n";); - return true; - } - p = p->parent(); - } - return false; - } void model_search::add_leaf(model_node& n) { SASSERT(n.children().empty()); @@ -1012,11 +1019,11 @@ namespace pdr { nodes.erase(&n); bool is_goal = n.is_goal(); remove_goal(n); - if (!nodes.empty() && is_goal && backtrack) { + // TBD: siblings would also fail if n is not a goal. + if (!nodes.empty() && backtrack && nodes[0]->children().empty() && nodes[0]->is_closed()) { TRACE("pdr_verbose", for (unsigned i = 0; i < nodes.size(); ++i) n.display(tout << &n << "\n", 2);); model_node* n1 = nodes[0]; - n1->set_open(); - SASSERT(n1->children().empty()); + n1->set_open(); enqueue_leaf(n1); } @@ -1702,7 +1709,15 @@ namespace pdr { void context::validate_search() { expr_ref tr = m_search.get_trace(*this); - // TBD: tr << "\n"; + smt::kernel solver(m, get_fparams()); + solver.assert_expr(tr); + lbool res = solver.check(); + if (res != l_true) { + std::stringstream msg; + msg << "rule validation failed when checking: " << tr; + IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); + throw default_exception(msg.str()); + } } void context::validate_model() { @@ -1938,11 +1953,11 @@ namespace pdr { proof_ref proof(m); SASSERT(m_last_result == l_true); proof = m_search.get_proof_trace(*this); - TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";); + TRACE("pdr", tout << "PDR trace: " << proof << "\n";); apply(m, m_pc.get(), proof); - TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";); + TRACE("pdr", tout << "PDR trace: " << proof << "\n";); // proof_utils::push_instantiations_up(proof); - // TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";); + // TRACE("pdr", tout << "PDR up: " << proof << "\n";); return proof; } diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 35b9067b2..ad4b44d90 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -268,7 +268,6 @@ namespace pdr { void enqueue_leaf(model_node* n); // add leaf to priority queue. void update_models(); void set_leaf(model_node& n); // Set node as leaf, remove children. - bool is_repeated(model_node& n) const; unsigned num_goals() const; public: From 6e1c246454930377bb14f249e3827db29878050b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Nov 2015 23:06:04 -0800 Subject: [PATCH 43/53] avoid exception in Ratul's environment Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0b924c21f..407c78e13 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2653,6 +2653,8 @@ def mk_z3consts_py(api_files): z3consts.write('%s = %s\n' % (k, i)) z3consts.write('\n') mode = SEARCHING + elif len(words) <= 2: + pass else: if words[2] != '': if len(words[2]) > 1 and words[2][1] == 'x': From 70069e0ae1042ade02fa0a69b3400fc905d58b67 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 17 Nov 2015 13:50:11 +0000 Subject: [PATCH 44/53] Fixed regular expressions in to expect cross-platform newlines. Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 407c78e13..67b60cbaf 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2592,7 +2592,7 @@ def mk_z3consts_py(api_files): if Z3PY_SRC_DIR is None: raise MKException("You must invoke set_z3py_dir(path):") - blank_pat = re.compile("^ *$") + blank_pat = re.compile("^ *\r?$") comment_pat = re.compile("^ *//.*$") typedef_pat = re.compile("typedef enum *") typedef2_pat = re.compile("typedef enum { *") @@ -2654,7 +2654,7 @@ def mk_z3consts_py(api_files): z3consts.write('\n') mode = SEARCHING elif len(words) <= 2: - pass + assert False, "Invalid %s, line: %s" % (api_file, linenum) else: if words[2] != '': if len(words[2]) > 1 and words[2][1] == 'x': @@ -2672,7 +2672,7 @@ def mk_z3consts_py(api_files): # Extract enumeration types from z3_api.h, and add .Net definitions def mk_z3consts_dotnet(api_files): - blank_pat = re.compile("^ *$") + blank_pat = re.compile("^ *\r?$") comment_pat = re.compile("^ *//.*$") typedef_pat = re.compile("typedef enum *") typedef2_pat = re.compile("typedef enum { *") @@ -2742,6 +2742,8 @@ def mk_z3consts_dotnet(api_files): z3consts.write(' %s = %s,\n' % (k, i)) z3consts.write(' }\n\n') mode = SEARCHING + elif len(words) <= 2: + assert False, "Invalid %s, line: %s" % (api_file, linenum) else: if words[2] != '': if len(words[2]) > 1 and words[2][1] == 'x': From fc05eb65bd7195e5baef7af0b3645c63e3dbd997 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 17 Nov 2015 13:50:11 +0000 Subject: [PATCH 45/53] Fixed regular expressions in build scripts to expect cross-platform newlines. --- scripts/mk_util.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 407c78e13..67b60cbaf 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2592,7 +2592,7 @@ def mk_z3consts_py(api_files): if Z3PY_SRC_DIR is None: raise MKException("You must invoke set_z3py_dir(path):") - blank_pat = re.compile("^ *$") + blank_pat = re.compile("^ *\r?$") comment_pat = re.compile("^ *//.*$") typedef_pat = re.compile("typedef enum *") typedef2_pat = re.compile("typedef enum { *") @@ -2654,7 +2654,7 @@ def mk_z3consts_py(api_files): z3consts.write('\n') mode = SEARCHING elif len(words) <= 2: - pass + assert False, "Invalid %s, line: %s" % (api_file, linenum) else: if words[2] != '': if len(words[2]) > 1 and words[2][1] == 'x': @@ -2672,7 +2672,7 @@ def mk_z3consts_py(api_files): # Extract enumeration types from z3_api.h, and add .Net definitions def mk_z3consts_dotnet(api_files): - blank_pat = re.compile("^ *$") + blank_pat = re.compile("^ *\r?$") comment_pat = re.compile("^ *//.*$") typedef_pat = re.compile("typedef enum *") typedef2_pat = re.compile("typedef enum { *") @@ -2742,6 +2742,8 @@ def mk_z3consts_dotnet(api_files): z3consts.write(' %s = %s,\n' % (k, i)) z3consts.write(' }\n\n') mode = SEARCHING + elif len(words) <= 2: + assert False, "Invalid %s, line: %s" % (api_file, linenum) else: if words[2] != '': if len(words[2]) > 1 and words[2][1] == 'x': From 66fc873613a80c5f2935fbeb29ced4ae8ec2b405 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Nov 2015 09:00:16 -0800 Subject: [PATCH 46/53] Fix for #322: PDR engine cannot falls back on fixed size arithmetic for difference logic. It would eventually overflow and cause incorrect model construction. Enable only fixed-size arithmetic when configuration allows it Signed-off-by: Nikolaj Bjorner --- src/smt/smt_setup.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 524dbeab6..edb4f1e55 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -721,8 +721,8 @@ namespace smt { IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";); st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas()); IF_VERBOSE(1000, st.display_primitive(verbose_stream());); - bool fixnum = st.arith_k_sum_is_small(); - bool int_only = !st.m_has_rational && !st.m_has_real; + bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum; + bool int_only = !st.m_has_rational && !st.m_has_real && m_params.m_arith_int_only; switch(m_params.m_arith_mode) { case AS_NO_ARITH: m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic")); From d6d301c5ebe10c584798ddfd5f54128d4d83526f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Nov 2015 18:38:37 -0800 Subject: [PATCH 47/53] fix for mising handling of quantifiers in tactic. Bug #324 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/eq2bv_tactic.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index b84d5567c..7cba66a5a 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -305,14 +305,16 @@ public: m_nonfd.mark(f, true); expr* e1, *e2; if (m.is_eq(f, e1, e2)) { - if (is_fd(e1, e2)) { + if (is_fd(e1, e2) || is_fd(e2, e1)) { continue; - } - if (is_fd(e2, e1)) { - continue; - } + } } - m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args()); + if (is_app(f)) { + m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args()); + } + else if (is_quantifier(f)) { + m_todo.push_back(to_quantifier(f)->get_expr()); + } } } From 04b0e3c2f74c318d52de5fa7fb3324d95b89bf56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Nov 2015 18:48:52 -0800 Subject: [PATCH 48/53] add checks for cancellation inside mam to agilely not ignore Rustan's soft requests for a timeout #326 Signed-off-by: Nikolaj Bjorner --- src/smt/mam.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index d92eef5b8..d22ca88db 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -3646,6 +3646,9 @@ namespace smt { approx_set::iterator it1 = plbls1.begin(); approx_set::iterator end1 = plbls1.end(); for (; it1 != end1; ++it1) { + if (m_context.get_cancel_flag()) { + break; + } unsigned plbl1 = *it1; SASSERT(plbls1.may_contain(plbl1)); approx_set::iterator it2 = plbls2.begin(); @@ -3687,6 +3690,9 @@ namespace smt { approx_set::iterator it1 = plbls.begin(); approx_set::iterator end1 = plbls.end(); for (; it1 != end1; ++it1) { + if (m_context.get_cancel_flag()) { + break; + } unsigned plbl1 = *it1; SASSERT(plbls.may_contain(plbl1)); approx_set::iterator it2 = clbls.begin(); @@ -3706,6 +3712,9 @@ namespace smt { svector::iterator it1 = m_new_patterns.begin(); svector::iterator end1 = m_new_patterns.end(); for (; it1 != end1; ++it1) { + if (m_context.get_cancel_flag()) { + break; + } quantifier * qa = it1->first; app * mp = it1->second; SASSERT(m_ast_manager.is_pattern(mp)); From d7c3e77b66414d1d10f1df73b6b1a792496710e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Nov 2015 18:59:43 -0800 Subject: [PATCH 49/53] port test_capi.c to use mostly essentially non-deprecated APIs Signed-off-by: Nikolaj Bjorner --- examples/c/test_capi.c | 489 ++++++++++++++++++++++++----------------- 1 file changed, 291 insertions(+), 198 deletions(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 11306a98b..385035361 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -83,6 +83,18 @@ Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err) return ctx; } +Z3_solver mk_solver(Z3_context ctx) +{ + Z3_solver s = Z3_mk_solver(ctx); + Z3_solver_inc_ref(ctx, s); + return s; +} + +void del_solver(Z3_context ctx, Z3_solver s) +{ + Z3_solver_dec_ref(ctx, s); +} + /** \brief Create a logical context. @@ -184,28 +196,30 @@ Z3_ast mk_binary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x, Z3_ast y) \brief Check whether the logical context is satisfiable, and compare the result with the expected result. If the context is satisfiable, then display the model. */ -void check(Z3_context ctx, Z3_lbool expected_result) +void check(Z3_context ctx, Z3_solver s, Z3_lbool expected_result) { Z3_model m = 0; - Z3_lbool result = Z3_check_and_get_model(ctx, &m); + Z3_lbool result = Z3_solver_check(ctx, s); switch (result) { case Z3_L_FALSE: printf("unsat\n"); break; case Z3_L_UNDEF: - printf("unknown\n"); + printf("unknown\n"); + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); printf("potential model:\n%s\n", Z3_model_to_string(ctx, m)); break; case Z3_L_TRUE: + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); printf("sat\n%s\n", Z3_model_to_string(ctx, m)); break; } - if (m) { - Z3_del_model(ctx, m); - } if (result != expected_result) { exitf("unexpected result"); } + if (m) Z3_model_dec_ref(ctx, m); } /** @@ -218,20 +232,18 @@ void check(Z3_context ctx, Z3_lbool expected_result) The context \c ctx is not modified by this function. */ -void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid) +void prove(Z3_context ctx, Z3_solver s, Z3_ast f, Z3_bool is_valid) { - Z3_model m; + Z3_model m = 0; Z3_ast not_f; /* save the current state of the context */ - Z3_push(ctx); + Z3_solver_push(ctx, s); not_f = Z3_mk_not(ctx, f); - Z3_assert_cnstr(ctx, not_f); - - m = 0; - - switch (Z3_check_and_get_model(ctx, &m)) { + Z3_solver_assert(ctx, s, not_f); + + switch (Z3_solver_check(ctx, s)) { case Z3_L_FALSE: /* proved */ printf("valid\n"); @@ -242,9 +254,11 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid) case Z3_L_UNDEF: /* Z3 failed to prove/disprove f. */ printf("unknown\n"); + m = Z3_solver_get_model(ctx, s); if (m != 0) { + Z3_model_inc_ref(ctx, m); /* m should be viewed as a potential counterexample. */ - printf("potential counterexample:\n%s\n", Z3_model_to_string(ctx, m)); + printf("potential counterexample:\n%s\n", Z3_model_to_string(ctx, m)); } if (is_valid) { exitf("unexpected result"); @@ -253,7 +267,9 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid) case Z3_L_TRUE: /* disproved */ printf("invalid\n"); + m = Z3_solver_get_model(ctx, s); if (m) { + Z3_model_inc_ref(ctx, m); /* the model returned by Z3 is a counterexample */ printf("counterexample:\n%s\n", Z3_model_to_string(ctx, m)); } @@ -262,13 +278,10 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid) } break; } + if (m) Z3_model_dec_ref(ctx, m); - if (m) { - Z3_del_model(ctx, m); - } - - /* restore context */ - Z3_pop(ctx, 1); + /* restore scope */ + Z3_solver_pop(ctx, s, 1); } /** @@ -281,7 +294,7 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid) Where, \c finv is a fresh function declaration. */ -void assert_inj_axiom(Z3_context ctx, Z3_func_decl f, unsigned i) +void assert_inj_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f, unsigned i) { unsigned sz, j; Z3_sort finv_domain, finv_range; @@ -339,7 +352,7 @@ void assert_inj_axiom(Z3_context ctx, Z3_func_decl f, unsigned i) names, eq); printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q)); - Z3_assert_cnstr(ctx, q); + Z3_solver_assert(ctx, s, q); /* free temporary arrays */ free(types); @@ -352,7 +365,7 @@ void assert_inj_axiom(Z3_context ctx, Z3_func_decl f, unsigned i) This example uses the SMT-LIB parser to simplify the axiom construction. */ -void assert_comm_axiom(Z3_context ctx, Z3_func_decl f) +void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f) { Z3_sort t; Z3_symbol f_name, t_name; @@ -379,7 +392,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_func_decl f) 1, &f_name, &f); q = Z3_get_smtlib_formula(ctx, 0); printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q)); - Z3_assert_cnstr(ctx, q); + Z3_solver_assert(ctx, s, q); } /** @@ -554,42 +567,50 @@ void display_function_interpretations(Z3_context c, FILE * out, Z3_model m) fprintf(out, "function interpretations:\n"); - num_functions = Z3_get_model_num_funcs(c, m); + num_functions = Z3_model_get_num_funcs(c, m); for (i = 0; i < num_functions; i++) { Z3_func_decl fdecl; Z3_symbol name; Z3_ast func_else; - unsigned num_entries, j; + unsigned num_entries = 0, j; + Z3_func_interp_opt finterp; - fdecl = Z3_get_model_func_decl(c, m, i); + fdecl = Z3_model_get_func_decl(c, m, i); + finterp = Z3_model_get_func_interp(c, m, fdecl); + Z3_func_interp_inc_ref(c, finterp); name = Z3_get_decl_name(c, fdecl); display_symbol(c, out, name); fprintf(out, " = {"); - num_entries = Z3_get_model_func_num_entries(c, m, i); + if (finterp) + num_entries = Z3_func_interp_get_num_entries(c, finterp); for (j = 0; j < num_entries; j++) { unsigned num_args, k; + Z3_func_entry fentry = Z3_func_interp_get_entry(c, finterp, j); + Z3_func_entry_inc_ref(c, fentry); if (j > 0) { fprintf(out, ", "); } - num_args = Z3_get_model_func_entry_num_args(c, m, i, j); + num_args = Z3_func_entry_get_num_args(c, fentry); fprintf(out, "("); for (k = 0; k < num_args; k++) { if (k > 0) { fprintf(out, ", "); } - display_ast(c, out, Z3_get_model_func_entry_arg(c, m, i, j, k)); + display_ast(c, out, Z3_func_entry_get_arg(c, fentry, k)); } fprintf(out, "|->"); - display_ast(c, out, Z3_get_model_func_entry_value(c, m, i, j)); + display_ast(c, out, Z3_func_entry_get_value(c, fentry)); fprintf(out, ")"); + Z3_func_entry_dec_ref(c, fentry); } if (num_entries > 0) { fprintf(out, ", "); } fprintf(out, "(else|->"); - func_else = Z3_get_model_func_else(c, m, i); + func_else = Z3_func_interp_get_else(c, finterp); display_ast(c, out, func_else); fprintf(out, ")}\n"); + Z3_func_interp_dec_ref(c, finterp); } } @@ -601,10 +622,12 @@ void display_model(Z3_context c, FILE * out, Z3_model m) unsigned num_constants; unsigned i; - num_constants = Z3_get_model_num_constants(c, m); + if (!m) return; + + num_constants = Z3_model_get_num_consts(c, m); for (i = 0; i < num_constants; i++) { Z3_symbol name; - Z3_func_decl cnst = Z3_get_model_constant(c, m, i); + Z3_func_decl cnst = Z3_model_get_const_decl(c, m, i); Z3_ast a, v; Z3_bool ok; name = Z3_get_decl_name(c, cnst); @@ -612,7 +635,7 @@ void display_model(Z3_context c, FILE * out, Z3_model m) fprintf(out, " = "); a = Z3_mk_app(c, cnst, 0, 0); v = a; - ok = Z3_eval(c, m, a, &v); + ok = Z3_model_eval(c, m, a, 1, &v); display_ast(c, out, v); fprintf(out, "\n"); } @@ -622,10 +645,10 @@ void display_model(Z3_context c, FILE * out, Z3_model m) /** \brief Similar to #check, but uses #display_model instead of #Z3_model_to_string. */ -void check2(Z3_context ctx, Z3_lbool expected_result) +void check2(Z3_context ctx, Z3_solver s, Z3_lbool expected_result) { Z3_model m = 0; - Z3_lbool result = Z3_check_and_get_model(ctx, &m); + Z3_lbool result = Z3_solver_check(ctx, s); switch (result) { case Z3_L_FALSE: printf("unsat\n"); @@ -633,19 +656,22 @@ void check2(Z3_context ctx, Z3_lbool expected_result) case Z3_L_UNDEF: printf("unknown\n"); printf("potential model:\n"); + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); display_model(ctx, stdout, m); break; case Z3_L_TRUE: printf("sat\n"); + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); display_model(ctx, stdout, m); break; } - if (m) { - Z3_del_model(ctx, m); - } if (result != expected_result) { exitf("unexpected result"); } + if (m) Z3_model_dec_ref(ctx, m); + } /** @@ -674,9 +700,6 @@ void simple_example() ctx = mk_context(); - /* do something with the context */ - printf("CONTEXT:\n%sEND OF CONTEXT\n", Z3_context_to_string(ctx)); - /* delete logical context */ Z3_del_context(ctx); } @@ -689,6 +712,7 @@ void demorgan() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_sort bool_sort; Z3_symbol symbol_x, symbol_y; Z3_ast x, y, not_x, not_y, x_and_y, ls, rs, conjecture, negated_conjecture; @@ -719,9 +743,10 @@ void demorgan() rs = Z3_mk_or(ctx, 2, args); conjecture = Z3_mk_iff(ctx, ls, rs); negated_conjecture = Z3_mk_not(ctx, conjecture); - - Z3_assert_cnstr(ctx, negated_conjecture); - switch (Z3_check(ctx)) { + + s = mk_solver(ctx); + Z3_solver_assert(ctx, s, negated_conjecture); + switch (Z3_solver_check(ctx, s)) { case Z3_L_FALSE: /* The negated conjecture was unsatisfiable, hence the conjecture is valid */ printf("DeMorgan is valid\n"); @@ -735,6 +760,7 @@ void demorgan() printf("DeMorgan is not valid\n"); break; } + del_solver(ctx, s); Z3_del_context(ctx); } @@ -745,21 +771,24 @@ void find_model_example1() { Z3_context ctx; Z3_ast x, y, x_xor_y; + Z3_solver s; printf("\nfind_model_example1\n"); LOG_MSG("find_model_example1"); ctx = mk_context(); + s = mk_solver(ctx); x = mk_bool_var(ctx, "x"); y = mk_bool_var(ctx, "y"); x_xor_y = Z3_mk_xor(ctx, x, y); - Z3_assert_cnstr(ctx, x_xor_y); + Z3_solver_assert(ctx, s, x_xor_y); printf("model for: x xor y\n"); - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -774,11 +803,13 @@ void find_model_example2() Z3_ast x_eq_y; Z3_ast args[2]; Z3_ast c1, c2, c3; + Z3_solver s; printf("\nfind_model_example2\n"); LOG_MSG("find_model_example2"); ctx = mk_context(); + s = mk_solver(ctx); x = mk_int_var(ctx, "x"); y = mk_int_var(ctx, "y"); one = mk_int(ctx, 1); @@ -791,20 +822,21 @@ void find_model_example2() c1 = Z3_mk_lt(ctx, x, y_plus_one); c2 = Z3_mk_gt(ctx, x, two); - Z3_assert_cnstr(ctx, c1); - Z3_assert_cnstr(ctx, c2); + Z3_solver_assert(ctx, s, c1); + Z3_solver_assert(ctx, s, c2); printf("model for: x < y + 1, x > 2\n"); - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); /* assert not(x = y) */ x_eq_y = Z3_mk_eq(ctx, x, y); c3 = Z3_mk_not(ctx, x_eq_y); - Z3_assert_cnstr(ctx, c3); + Z3_solver_assert(ctx, s,c3); printf("model for: x < y + 1, x > 2, not(x = y)\n"); - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -818,6 +850,7 @@ void find_model_example2() void prove_example1() { Z3_context ctx; + Z3_solver s; Z3_symbol U_name, g_name, x_name, y_name; Z3_sort U; Z3_sort g_domain[1]; @@ -829,7 +862,8 @@ void prove_example1() LOG_MSG("prove_example1"); ctx = mk_context(); - + s = mk_solver(ctx); + /* create uninterpreted type. */ U_name = Z3_mk_string_symbol(ctx, "U"); U = Z3_mk_uninterpreted_sort(ctx, U_name); @@ -850,12 +884,12 @@ void prove_example1() /* assert x = y */ eq = Z3_mk_eq(ctx, x, y); - Z3_assert_cnstr(ctx, eq); + Z3_solver_assert(ctx, s, eq); /* prove g(x) = g(y) */ f = Z3_mk_eq(ctx, gx, gy); printf("prove: x = y implies g(x) = g(y)\n"); - prove(ctx, f, Z3_TRUE); + prove(ctx, s, f, Z3_TRUE); /* create g(g(x)) */ ggx = mk_unary_app(ctx, g, gx); @@ -863,8 +897,9 @@ void prove_example1() /* disprove g(g(x)) = g(y) */ f = Z3_mk_eq(ctx, ggx, gy); printf("disprove: x = y implies g(g(x)) = g(y)\n"); - prove(ctx, f, Z3_FALSE); + prove(ctx, s, f, Z3_FALSE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -877,6 +912,7 @@ void prove_example1() void prove_example2() { Z3_context ctx; + Z3_solver s; Z3_sort int_sort; Z3_symbol g_name; Z3_sort g_domain[1]; @@ -889,6 +925,7 @@ void prove_example2() LOG_MSG("prove_example2"); ctx = mk_context(); + s = mk_solver(ctx); /* declare function g */ int_sort = Z3_mk_int_sort(ctx); @@ -916,30 +953,31 @@ void prove_example2() ggx_gy = mk_unary_app(ctx, g, gx_gy); eq = Z3_mk_eq(ctx, ggx_gy, gz); c1 = Z3_mk_not(ctx, eq); - Z3_assert_cnstr(ctx, c1); + Z3_solver_assert(ctx, s, c1); /* assert x + z <= y */ args[0] = x; args[1] = z; x_plus_z = Z3_mk_add(ctx, 2, args); c2 = Z3_mk_le(ctx, x_plus_z, y); - Z3_assert_cnstr(ctx, c2); + Z3_solver_assert(ctx, s, c2); /* assert y <= x */ c3 = Z3_mk_le(ctx, y, x); - Z3_assert_cnstr(ctx, c3); + Z3_solver_assert(ctx, s, c3); /* prove z < 0 */ f = Z3_mk_lt(ctx, z, zero); printf("prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0\n"); - prove(ctx, f, Z3_TRUE); + prove(ctx, s, f, Z3_TRUE); /* disprove z < -1 */ minus_one = mk_int(ctx, -1); f = Z3_mk_lt(ctx, z, minus_one); printf("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1\n"); - prove(ctx, f, Z3_FALSE); + prove(ctx, s, f, Z3_FALSE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -952,6 +990,7 @@ void prove_example2() void push_pop_example1() { Z3_context ctx; + Z3_solver s; Z3_sort int_sort; Z3_symbol x_sym, y_sym; Z3_ast x, y, big_number, three; @@ -961,6 +1000,7 @@ void push_pop_example1() LOG_MSG("push_pop_example1"); ctx = mk_context(); + s = mk_solver(ctx); /* create a big number */ int_sort = Z3_mk_int_sort(ctx); @@ -976,32 +1016,32 @@ void push_pop_example1() /* assert x >= "big number" */ c1 = Z3_mk_ge(ctx, x, big_number); printf("assert: x >= 'big number'\n"); - Z3_assert_cnstr(ctx, c1); + Z3_solver_assert(ctx, s, c1); /* create a backtracking point */ printf("push\n"); - Z3_push(ctx); + Z3_solver_push(ctx, s); - printf("number of scopes: %d\n", Z3_get_num_scopes(ctx)); + printf("number of scopes: %d\n", Z3_solver_get_num_scopes(ctx, s)); /* assert x <= 3 */ c2 = Z3_mk_le(ctx, x, three); printf("assert: x <= 3\n"); - Z3_assert_cnstr(ctx, c2); + Z3_solver_assert(ctx, s, c2); /* context is inconsistent at this point */ - check2(ctx, Z3_L_FALSE); + check2(ctx, s, Z3_L_FALSE); /* backtrack: the constraint x <= 3 will be removed, since it was - asserted after the last Z3_push. */ + asserted after the last Z3_solver_push. */ printf("pop\n"); - Z3_pop(ctx, 1); + Z3_solver_pop(ctx, s, 1); - printf("number of scopes: %d\n", Z3_get_num_scopes(ctx)); + printf("number of scopes: %d\n", Z3_solver_get_num_scopes(ctx, s)); /* the context is consistent again. */ - check2(ctx, Z3_L_TRUE); + check2(ctx, s, Z3_L_TRUE); /* new constraints can be asserted... */ @@ -1012,11 +1052,12 @@ void push_pop_example1() /* assert y > x */ c3 = Z3_mk_gt(ctx, y, x); printf("assert: y > x\n"); - Z3_assert_cnstr(ctx, c3); + Z3_solver_assert(ctx, s, c3); /* the context is still consistent. */ - check2(ctx, Z3_L_TRUE); + check2(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1030,6 +1071,7 @@ void quantifier_example1() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_sort int_sort; Z3_symbol f_name; Z3_sort f_domain[2]; @@ -1052,6 +1094,7 @@ void quantifier_example1() Z3_global_param_set("smt.mbqi.max_iterations", "10"); ctx = mk_context_custom(cfg, error_handler); Z3_del_config(cfg); + s = mk_solver(ctx); /* declare function f */ int_sort = Z3_mk_int_sort(ctx); @@ -1061,7 +1104,7 @@ void quantifier_example1() f = Z3_mk_func_decl(ctx, f_name, 2, f_domain, int_sort); /* assert that f is injective in the second argument. */ - assert_inj_axiom(ctx, f, 1); + assert_inj_axiom(ctx, s, f, 1); /* create x, y, v, w, fxy, fwv */ x = mk_int_var(ctx, "x"); @@ -1073,26 +1116,23 @@ void quantifier_example1() /* assert f(x, y) = f(w, v) */ p1 = Z3_mk_eq(ctx, fxy, fwv); - Z3_assert_cnstr(ctx, p1); + Z3_solver_assert(ctx, s, p1); /* prove f(x, y) = f(w, v) implies y = v */ p2 = Z3_mk_eq(ctx, y, v); printf("prove: f(x, y) = f(w, v) implies y = v\n"); - prove(ctx, p2, Z3_TRUE); + prove(ctx, s, p2, Z3_TRUE); /* disprove f(x, y) = f(w, v) implies x = w */ /* using check2 instead of prove */ p3 = Z3_mk_eq(ctx, x, w); not_p3 = Z3_mk_not(ctx, p3); - Z3_assert_cnstr(ctx, not_p3); + Z3_solver_assert(ctx, s, not_p3); printf("disprove: f(x, y) = f(w, v) implies x = w\n"); printf("that is: not(f(x, y) = f(w, v) implies x = w) is satisfiable\n"); - check2(ctx, Z3_L_UNDEF); - printf("reason for last failure: %d (7 = quantifiers)\n", - Z3_get_search_failure(ctx)); - if (Z3_get_search_failure(ctx) != Z3_QUANTIFIERS) { - exitf("unexpected result"); - } + check2(ctx, s, Z3_L_UNDEF); + printf("reason for last failure: %s\n", Z3_solver_get_reason_unknown(ctx, s)); + del_solver(ctx, s); Z3_del_context(ctx); /* reset global parameters set by this function */ Z3_global_param_reset_all(); @@ -1105,7 +1145,8 @@ void quantifier_example1() */ void array_example1() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort int_sort, array_sort; Z3_ast a1, a2, i1, v1, i2, v2, i3; Z3_ast st1, st2, sel1, sel2; @@ -1116,7 +1157,6 @@ void array_example1() printf("\narray_example1\n"); LOG_MSG("array_example1"); - ctx = mk_context(); int_sort = Z3_mk_int_sort(ctx); array_sort = Z3_mk_array_sort(ctx, int_sort, int_sort); @@ -1148,8 +1188,9 @@ void array_example1() thm = Z3_mk_implies(ctx, antecedent, consequent); printf("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))\n"); printf("%s\n", Z3_ast_to_string(ctx, thm)); - prove(ctx, thm, Z3_TRUE); + prove(ctx, s, thm, Z3_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1163,6 +1204,7 @@ void array_example1() void array_example2() { Z3_context ctx; + Z3_solver s; Z3_sort bool_sort, array_sort; Z3_ast a[5]; Z3_ast d; @@ -1174,6 +1216,7 @@ void array_example2() for (n = 2; n <= 5; n++) { printf("n = %d\n", n); ctx = mk_context(); + s = mk_solver(ctx); bool_sort = Z3_mk_bool_sort(ctx); array_sort = Z3_mk_array_sort(ctx, bool_sort, bool_sort); @@ -1187,11 +1230,12 @@ void array_example2() /* assert distinct(a[0], ..., a[n]) */ d = Z3_mk_distinct(ctx, n, a); printf("%s\n", Z3_ast_to_string(ctx, d)); - Z3_assert_cnstr(ctx, d); + Z3_solver_assert(ctx, s, d); /* context is satisfiable if n < 5 */ - check2(ctx, n < 5 ? Z3_L_TRUE : Z3_L_FALSE); + check2(ctx, s, n < 5 ? Z3_L_TRUE : Z3_L_FALSE); + del_solver(ctx, s); Z3_del_context(ctx); } } @@ -1201,13 +1245,13 @@ void array_example2() */ void array_example3() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort bool_sort, int_sort, array_sort; Z3_sort domain, range; printf("\narray_example3\n"); LOG_MSG("array_example3"); - ctx = mk_context(); bool_sort = Z3_mk_bool_sort(ctx); int_sort = Z3_mk_int_sort(ctx); @@ -1231,6 +1275,7 @@ void array_example3() exitf("invalid array type"); } + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1239,7 +1284,8 @@ void array_example3() */ void tuple_example1() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort real_sort, pair_sort; Z3_symbol mk_tuple_name; Z3_func_decl mk_tuple_decl; @@ -1251,7 +1297,6 @@ void tuple_example1() printf("\ntuple_example1\n"); LOG_MSG("tuple_example1"); - ctx = mk_context(); real_sort = Z3_mk_real_sort(ctx); @@ -1284,13 +1329,13 @@ void tuple_example1() eq2 = Z3_mk_eq(ctx, x, one); thm = Z3_mk_implies(ctx, eq1, eq2); printf("prove: get_x(mk_pair(x, y)) = 1 implies x = 1\n"); - prove(ctx, thm, Z3_TRUE); + prove(ctx, s, thm, Z3_TRUE); /* disprove that get_x(mk_pair(x,y)) == 1 implies y = 1*/ eq3 = Z3_mk_eq(ctx, y, one); thm = Z3_mk_implies(ctx, eq1, eq3); printf("disprove: get_x(mk_pair(x, y)) = 1 implies y = 1\n"); - prove(ctx, thm, Z3_FALSE); + prove(ctx, s, thm, Z3_FALSE); } { @@ -1311,12 +1356,12 @@ void tuple_example1() consequent = Z3_mk_eq(ctx, p1, p2); thm = Z3_mk_implies(ctx, antecedent, consequent); printf("prove: get_x(p1) = get_x(p2) and get_y(p1) = get_y(p2) implies p1 = p2\n"); - prove(ctx, thm, Z3_TRUE); + prove(ctx, s, thm, Z3_TRUE); /* disprove that get_x(p1) = get_x(p2) implies p1 = p2 */ thm = Z3_mk_implies(ctx, antecedents[0], consequent); printf("disprove: get_x(p1) = get_x(p2) implies p1 = p2\n"); - prove(ctx, thm, Z3_FALSE); + prove(ctx, s, thm, Z3_FALSE); } { @@ -1335,16 +1380,17 @@ void tuple_example1() consequent = Z3_mk_eq(ctx, x, ten); thm = Z3_mk_implies(ctx, antecedent, consequent); printf("prove: p2 = update(p1, 0, 10) implies get_x(p2) = 10\n"); - prove(ctx, thm, Z3_TRUE); + prove(ctx, s, thm, Z3_TRUE); /* disprove that p2 = update(p1, 0, 10) implies get_y(p2) = 10 */ y = mk_unary_app(ctx, get_y_decl, p2); consequent = Z3_mk_eq(ctx, y, ten); thm = Z3_mk_implies(ctx, antecedent, consequent); printf("disprove: p2 = update(p1, 0, 10) implies get_y(p2) = 10\n"); - prove(ctx, thm, Z3_FALSE); + prove(ctx, s, thm, Z3_FALSE); } + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1353,14 +1399,14 @@ void tuple_example1() */ void bitvector_example1() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort bv_sort; Z3_ast x, zero, ten, x_minus_ten, c1, c2, thm; printf("\nbitvector_example1\n"); LOG_MSG("bitvector_example1"); - ctx = mk_context(); bv_sort = Z3_mk_bv_sort(ctx, 32); @@ -1373,8 +1419,9 @@ void bitvector_example1() c2 = Z3_mk_bvsle(ctx, x_minus_ten, zero); thm = Z3_mk_iff(ctx, c1, c2); printf("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers\n"); - prove(ctx, thm, Z3_FALSE); + prove(ctx, s, thm, Z3_FALSE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1384,6 +1431,7 @@ void bitvector_example1() void bitvector_example2() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); /* construct x ^ y - 103 == x * y */ Z3_sort bv_sort = Z3_mk_bv_sort(ctx, 32); @@ -1400,11 +1448,12 @@ void bitvector_example2() printf("find values of x and y, such that x ^ y - 103 == x * y\n"); /* add the constraint x ^ y - 103 == x * y<\tt> to the logical context */ - Z3_assert_cnstr(ctx, ctr); + Z3_solver_assert(ctx, s, ctr); /* find a model (i.e., values for x an y that satisfy the constraint */ - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1413,36 +1462,38 @@ void bitvector_example2() */ void eval_example1() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_ast x, y, two; Z3_ast c1, c2; - Z3_model m; + Z3_model m = 0; printf("\neval_example1\n"); LOG_MSG("eval_example1"); - ctx = mk_context(); x = mk_int_var(ctx, "x"); y = mk_int_var(ctx, "y"); two = mk_int(ctx, 2); /* assert x < y */ c1 = Z3_mk_lt(ctx, x, y); - Z3_assert_cnstr(ctx, c1); + Z3_solver_assert(ctx, s, c1); /* assert x > 2 */ c2 = Z3_mk_gt(ctx, x, two); - Z3_assert_cnstr(ctx, c2); + Z3_solver_assert(ctx, s, c2); /* find model for the constraints above */ - if (Z3_check_and_get_model(ctx, &m) == Z3_L_TRUE) { + if (Z3_solver_check(ctx, s) == Z3_L_TRUE) { Z3_ast x_plus_y; Z3_ast args[2] = {x, y}; Z3_ast v; + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); printf("MODEL:\n%s", Z3_model_to_string(ctx, m)); x_plus_y = Z3_mk_add(ctx, 2, args); printf("\nevaluating x+y\n"); - if (Z3_eval(ctx, m, x_plus_y, &v)) { + if (Z3_model_eval(ctx, m, x_plus_y, 1, &v)) { printf("result = "); display_ast(ctx, stdout, v); printf("\n"); @@ -1450,12 +1501,13 @@ void eval_example1() else { exitf("failed to evaluate: x+y"); } - Z3_del_model(ctx, m); } else { exitf("the constraints are satisfiable"); } + if (m) Z3_model_dec_ref(ctx, m); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1492,6 +1544,7 @@ void error_code_example1() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_ast x; Z3_model m; Z3_ast v; @@ -1505,16 +1558,19 @@ void error_code_example1() cfg = Z3_mk_config(); ctx = mk_context_custom(cfg, NULL); Z3_del_config(cfg); + s = mk_solver(ctx); x = mk_bool_var(ctx, "x"); x_decl = Z3_get_app_decl(ctx, Z3_to_app(ctx, x)); - Z3_assert_cnstr(ctx, x); + Z3_solver_assert(ctx, s, x); - if (Z3_check_and_get_model(ctx, &m) != Z3_L_TRUE) { + if (Z3_solver_check(ctx, s) != Z3_L_TRUE) { exitf("unexpected result"); } - if (!Z3_eval_func_decl(ctx, m, x_decl, &v)) { + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); + if (!Z3_model_eval(ctx, m, x, 1, &v)) { exitf("did not obtain value for declaration.\n"); } if (Z3_get_error_code(ctx) == Z3_OK) { @@ -1525,7 +1581,8 @@ void error_code_example1() if (Z3_get_error_code(ctx) != Z3_OK) { printf("last call failed.\n"); } - Z3_del_model(ctx, m); + if (m) Z3_model_dec_ref(ctx, m); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1558,7 +1615,7 @@ void error_code_example2() { Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg((Z3_error_code)r)); + printf("Z3 error: %s.\n", Z3_get_error_msg_ex(ctx, (Z3_error_code)r)); if (ctx != NULL) { Z3_del_context(ctx); } @@ -1570,13 +1627,13 @@ void error_code_example2() { */ void parser_example1() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); unsigned i, num_formulas; printf("\nparser_example1\n"); LOG_MSG("parser_example1"); - ctx = mk_context(); Z3_parse_smtlib_string(ctx, "(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))", @@ -1586,11 +1643,12 @@ void parser_example1() for (i = 0; i < num_formulas; i++) { Z3_ast f = Z3_get_smtlib_formula(ctx, i); printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f)); - Z3_assert_cnstr(ctx, f); + Z3_solver_assert(ctx, s, f); } - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1599,7 +1657,8 @@ void parser_example1() */ void parser_example2() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_ast x, y; Z3_symbol names[2]; Z3_func_decl decls[2]; @@ -1608,7 +1667,6 @@ void parser_example2() printf("\nparser_example2\n"); LOG_MSG("parser_example2"); - ctx = mk_context(); /* Z3_enable_arithmetic doesn't need to be invoked in this example because it will be implicitly invoked by mk_int_var. @@ -1629,9 +1687,10 @@ void parser_example2() 2, names, decls); f = Z3_get_smtlib_formula(ctx, 0); printf("formula: %s\n", Z3_ast_to_string(ctx, f)); - Z3_assert_cnstr(ctx, f); - check(ctx, Z3_L_TRUE); + Z3_solver_assert(ctx, s, f); + check(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1642,6 +1701,7 @@ void parser_example3() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_sort int_sort; Z3_symbol g_name; Z3_sort g_domain[2]; @@ -1656,6 +1716,7 @@ void parser_example3() Z3_set_param_value(cfg, "model", "true"); ctx = mk_context_custom(cfg, error_handler); Z3_del_config(cfg); + s = mk_solver(ctx); /* declare function g */ int_sort = Z3_mk_int_sort(ctx); @@ -1664,7 +1725,7 @@ void parser_example3() g_domain[1] = int_sort; g = Z3_mk_func_decl(ctx, g_name, 2, g_domain, int_sort); - assert_comm_axiom(ctx, g); + assert_comm_axiom(ctx, s, g); Z3_parse_smtlib_string(ctx, "(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (g x 0) (g 0 y)))))", @@ -1672,8 +1733,9 @@ void parser_example3() 1, &g_name, &g); thm = Z3_get_smtlib_formula(ctx, 0); printf("formula: %s\n", Z3_ast_to_string(ctx, thm)); - prove(ctx, thm, Z3_TRUE); + prove(ctx, s, thm, Z3_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1718,6 +1780,7 @@ void parser_example4() void parser_example5() { Z3_config cfg; Z3_context ctx = NULL; + Z3_solver s = NULL; int r; printf("\nparser_example5\n"); @@ -1727,6 +1790,7 @@ void parser_example5() { if (r == 0) { cfg = Z3_mk_config(); ctx = mk_context_custom(cfg, throw_z3_error); + s = mk_solver(ctx); Z3_del_config(cfg); Z3_parse_smtlib_string(ctx, @@ -1735,12 +1799,14 @@ void parser_example5() { 0, 0, 0, 0, 0, 0); unreachable(); + del_solver(ctx, s); Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg((Z3_error_code)r)); + printf("Z3 error: %s.\n", Z3_get_error_msg_ex(ctx, (Z3_error_code)r)); if (ctx != NULL) { printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx)); + del_solver(ctx, s); Z3_del_context(ctx); } } @@ -1751,24 +1817,28 @@ void parser_example5() { */ void numeral_example() { Z3_context ctx; + Z3_solver s; Z3_ast n1, n2; Z3_sort real_ty; printf("\nnumeral_example\n"); LOG_MSG("numeral_example"); ctx = mk_context(); + s = mk_solver(ctx); + real_ty = Z3_mk_real_sort(ctx); n1 = Z3_mk_numeral(ctx, "1/2", real_ty); n2 = Z3_mk_numeral(ctx, "0.5", real_ty); printf("Numerals n1:%s", Z3_ast_to_string(ctx, n1)); printf(" n2:%s\n", Z3_ast_to_string(ctx, n2)); - prove(ctx, Z3_mk_eq(ctx, n1, n2), Z3_TRUE); + prove(ctx, s, Z3_mk_eq(ctx, n1, n2), Z3_TRUE); n1 = Z3_mk_numeral(ctx, "-1/3", real_ty); n2 = Z3_mk_numeral(ctx, "-0.33333333333333333333333333333333333333333333333333", real_ty); printf("Numerals n1:%s", Z3_ast_to_string(ctx, n1)); printf(" n2:%s\n", Z3_ast_to_string(ctx, n2)); - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, n1, n2)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, n1, n2)), Z3_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1801,6 +1871,7 @@ void ite_example() */ void enum_example() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort fruit; Z3_symbol name = Z3_mk_string_symbol(ctx, "fruit"); Z3_symbol enum_names[3]; @@ -1831,14 +1902,14 @@ void enum_example() { orange = Z3_mk_app(ctx, enum_consts[2], 0, 0); /* Apples are different from oranges */ - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, apple, orange)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, apple, orange)), Z3_TRUE); /* Apples pass the apple test */ - prove(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &apple), Z3_TRUE); + prove(ctx, s, Z3_mk_app(ctx, enum_testers[0], 1, &apple), Z3_TRUE); /* Oranges fail the apple test */ - prove(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange), Z3_FALSE); - prove(ctx, Z3_mk_not(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange)), Z3_TRUE); + prove(ctx, s, Z3_mk_app(ctx, enum_testers[0], 1, &orange), Z3_FALSE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange)), Z3_TRUE); fruity = mk_var(ctx, "fruity", fruit); @@ -1847,9 +1918,10 @@ void enum_example() { ors[1] = Z3_mk_eq(ctx, fruity, banana); ors[2] = Z3_mk_eq(ctx, fruity, orange); - prove(ctx, Z3_mk_or(ctx, 3, ors), Z3_TRUE); + prove(ctx, s, Z3_mk_or(ctx, 3, ors), Z3_TRUE); /* delete logical context */ + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1858,6 +1930,7 @@ void enum_example() { */ void list_example() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort int_ty, int_list; Z3_func_decl nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl; Z3_ast nil, l1, l2, x, y, u, v, fml, fml1; @@ -1877,43 +1950,44 @@ void list_example() { l2 = mk_binary_app(ctx, cons_decl, mk_int(ctx, 2), nil); /* nil != cons(1, nil) */ - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE); /* cons(2,nil) != cons(1, nil) */ - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, l1, l2)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, l1, l2)), Z3_TRUE); /* cons(x,nil) = cons(y, nil) => x = y */ x = mk_var(ctx, "x", int_ty); y = mk_var(ctx, "y", int_ty); l1 = mk_binary_app(ctx, cons_decl, x, nil); l2 = mk_binary_app(ctx, cons_decl, y, nil); - prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE); + prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE); /* cons(x,u) = cons(x, v) => u = v */ u = mk_var(ctx, "u", int_list); v = mk_var(ctx, "v", int_list); l1 = mk_binary_app(ctx, cons_decl, x, u); l2 = mk_binary_app(ctx, cons_decl, y, v); - prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE); - prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE); + prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE); + prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE); /* is_nil(u) or is_cons(u) */ ors[0] = Z3_mk_app(ctx, is_nil_decl, 1, &u); ors[1] = Z3_mk_app(ctx, is_cons_decl, 1, &u); - prove(ctx, Z3_mk_or(ctx, 2, ors), Z3_TRUE); + prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE); /* occurs check u != cons(x,u) */ - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE); /* destructors: is_cons(u) => u = cons(head(u),tail(u)) */ fml1 = Z3_mk_eq(ctx, u, mk_binary_app(ctx, cons_decl, mk_unary_app(ctx, head_decl, u), mk_unary_app(ctx, tail_decl, u))); fml = Z3_mk_implies(ctx, Z3_mk_app(ctx, is_cons_decl, 1, &u), fml1); printf("Formula %s\n", Z3_ast_to_string(ctx, fml)); - prove(ctx, fml, Z3_TRUE); + prove(ctx, s, fml, Z3_TRUE); - prove(ctx, fml1, Z3_FALSE); + prove(ctx, s, fml1, Z3_FALSE); /* delete logical context */ + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1922,6 +1996,7 @@ void list_example() { */ void tree_example() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort cell; Z3_func_decl nil_decl, is_nil_decl, cons_decl, is_cons_decl, car_decl, cdr_decl; Z3_ast nil, l1, l2, x, y, u, v, fml, fml1; @@ -1957,7 +2032,7 @@ void tree_example() { l2 = mk_binary_app(ctx, cons_decl, l1, nil); /* nil != cons(nil, nil) */ - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE); /* cons(x,u) = cons(x, v) => u = v */ u = mk_var(ctx, "u", cell); @@ -1966,26 +2041,27 @@ void tree_example() { y = mk_var(ctx, "y", cell); l1 = mk_binary_app(ctx, cons_decl, x, u); l2 = mk_binary_app(ctx, cons_decl, y, v); - prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE); - prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE); + prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE); + prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE); /* is_nil(u) or is_cons(u) */ ors[0] = Z3_mk_app(ctx, is_nil_decl, 1, &u); ors[1] = Z3_mk_app(ctx, is_cons_decl, 1, &u); - prove(ctx, Z3_mk_or(ctx, 2, ors), Z3_TRUE); + prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE); /* occurs check u != cons(x,u) */ - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE); /* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */ fml1 = Z3_mk_eq(ctx, u, mk_binary_app(ctx, cons_decl, mk_unary_app(ctx, car_decl, u), mk_unary_app(ctx, cdr_decl, u))); fml = Z3_mk_implies(ctx, Z3_mk_app(ctx, is_cons_decl, 1, &u), fml1); printf("Formula %s\n", Z3_ast_to_string(ctx, fml)); - prove(ctx, fml, Z3_TRUE); + prove(ctx, s, fml, Z3_TRUE); - prove(ctx, fml1, Z3_FALSE); + prove(ctx, s, fml1, Z3_FALSE); /* delete logical context */ + del_solver(ctx, s); Z3_del_context(ctx); @@ -2000,6 +2076,7 @@ void tree_example() { void forest_example() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort tree, forest; Z3_func_decl nil1_decl, is_nil1_decl, cons1_decl, is_cons1_decl, car1_decl, cdr1_decl; Z3_func_decl nil2_decl, is_nil2_decl, cons2_decl, is_cons2_decl, car2_decl, cdr2_decl; @@ -2073,8 +2150,8 @@ void forest_example() { /* nil != cons(nil,nil) */ - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil1, f1)), Z3_TRUE); - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil2, t1)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil1, f1)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil2, t1)), Z3_TRUE); /* cons(x,u) = cons(x, v) => u = v */ @@ -2084,18 +2161,19 @@ void forest_example() { y = mk_var(ctx, "y", tree); l1 = mk_binary_app(ctx, cons1_decl, x, u); l2 = mk_binary_app(ctx, cons1_decl, y, v); - prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE); - prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE); + prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE); + prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE); /* is_nil(u) or is_cons(u) */ ors[0] = Z3_mk_app(ctx, is_nil1_decl, 1, &u); ors[1] = Z3_mk_app(ctx, is_cons1_decl, 1, &u); - prove(ctx, Z3_mk_or(ctx, 2, ors), Z3_TRUE); + prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE); /* occurs check u != cons(x,u) */ - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE); /* delete logical context */ + del_solver(ctx, s); Z3_del_context(ctx); } @@ -2108,6 +2186,7 @@ void forest_example() { */ void binary_tree_example() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort cell; Z3_func_decl nil_decl, /* nil : BinTree (constructor) */ @@ -2164,22 +2243,23 @@ void binary_tree_example() { Z3_ast node3 = Z3_mk_app(ctx, node_decl, 3, args3); /* prove that nil != node1 */ - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, node1)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, node1)), Z3_TRUE); /* prove that nil = left(node1) */ - prove(ctx, Z3_mk_eq(ctx, nil, mk_unary_app(ctx, left_decl, node1)), Z3_TRUE); + prove(ctx, s, Z3_mk_eq(ctx, nil, mk_unary_app(ctx, left_decl, node1)), Z3_TRUE); /* prove that node1 = right(node3) */ - prove(ctx, Z3_mk_eq(ctx, node1, mk_unary_app(ctx, right_decl, node3)), Z3_TRUE); + prove(ctx, s, Z3_mk_eq(ctx, node1, mk_unary_app(ctx, right_decl, node3)), Z3_TRUE); /* prove that !is-nil(node2) */ - prove(ctx, Z3_mk_not(ctx, mk_unary_app(ctx, is_nil_decl, node2)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, mk_unary_app(ctx, is_nil_decl, node2)), Z3_TRUE); /* prove that value(node2) >= 0 */ - prove(ctx, Z3_mk_ge(ctx, mk_unary_app(ctx, value_decl, node2), mk_int(ctx, 0)), Z3_TRUE); + prove(ctx, s, Z3_mk_ge(ctx, mk_unary_app(ctx, value_decl, node2), mk_int(ctx, 0)), Z3_TRUE); } /* delete logical context */ + del_solver(ctx, s); Z3_del_context(ctx); } @@ -2190,6 +2270,7 @@ void binary_tree_example() { */ void unsat_core_and_proof_example() { Z3_context ctx = mk_proof_context(); + Z3_solver s = mk_solver(ctx); Z3_ast pa = mk_bool_var(ctx, "PredA"); Z3_ast pb = mk_bool_var(ctx, "PredB"); Z3_ast pc = mk_bool_var(ctx, "PredC"); @@ -2210,49 +2291,53 @@ void unsat_core_and_proof_example() { Z3_ast g2[2] = { f2, p2 }; Z3_ast g3[2] = { f3, p3 }; Z3_ast g4[2] = { f4, p4 }; - Z3_ast core[4] = { 0, 0, 0, 0 }; - unsigned core_size = 4; - Z3_ast proof; - Z3_model m = 0; Z3_lbool result; + Z3_ast proof; + Z3_model m = 0; unsigned i; + Z3_ast_vector core; printf("\nunsat_core_and_proof_example\n"); LOG_MSG("unsat_core_and_proof_example"); - Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g1)); - Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g2)); - Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g3)); - Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g4)); + Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g1)); + Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g2)); + Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g3)); + Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g4)); - result = Z3_check_assumptions(ctx, 4, assumptions, &m, &proof, &core_size, core); + result = Z3_solver_check_assumptions(ctx, s, 4, assumptions); switch (result) { case Z3_L_FALSE: + core = Z3_solver_get_unsat_core(ctx, s); + proof = Z3_solver_get_proof(ctx, s); printf("unsat\n"); printf("proof: %s\n", Z3_ast_to_string(ctx, proof)); printf("\ncore:\n"); - for (i = 0; i < core_size; ++i) { - printf("%s\n", Z3_ast_to_string(ctx, core[i])); + for (i = 0; i < Z3_ast_vector_size(ctx, core); ++i) { + printf("%s\n", Z3_ast_to_string(ctx, Z3_ast_vector_get(ctx, core, i))); } printf("\n"); break; case Z3_L_UNDEF: printf("unknown\n"); printf("potential model:\n"); + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); display_model(ctx, stdout, m); break; case Z3_L_TRUE: printf("sat\n"); + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); display_model(ctx, stdout, m); break; } - if (m) { - Z3_del_model(ctx, m); - } /* delete logical context */ + if (m) Z3_model_dec_ref(ctx, m); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -2264,6 +2349,7 @@ void unsat_core_and_proof_example() { */ typedef struct { Z3_context m_context; + Z3_solver m_solver; // IMPORTANT: the fields m_answer_literals, m_retracted and m_num_answer_literals must be saved/restored // if push/pop operations are performed on m_context. Z3_ast m_answer_literals[MAX_RETRACTABLE_ASSERTIONS]; @@ -2279,6 +2365,7 @@ typedef Z3_ext_context_struct * Z3_ext_context; Z3_ext_context mk_ext_context() { Z3_ext_context ctx = (Z3_ext_context) malloc(sizeof(Z3_ext_context_struct)); ctx->m_context = mk_context(); + ctx->m_solver = mk_solver(ctx->m_context); ctx->m_num_answer_literals = 0; return ctx; } @@ -2287,6 +2374,7 @@ Z3_ext_context mk_ext_context() { \brief Delete the given logical context wrapper. */ void del_ext_context(Z3_ext_context ctx) { + del_solver(ctx->m_context, ctx->m_solver); Z3_del_context(ctx->m_context); free(ctx); } @@ -2313,7 +2401,7 @@ unsigned assert_retractable_cnstr(Z3_ext_context ctx, Z3_ast c) { // assert: c OR (not ans_lit) args[0] = c; args[1] = Z3_mk_not(ctx->m_context, ans_lit); - Z3_assert_cnstr(ctx->m_context, Z3_mk_or(ctx->m_context, 2, args)); + Z3_solver_assert(ctx->m_context, ctx->m_solver, Z3_mk_or(ctx->m_context, 2, args)); return result; } @@ -2344,10 +2432,8 @@ Z3_lbool ext_check(Z3_ext_context ctx) { Z3_lbool result; unsigned num_assumptions = 0; Z3_ast assumptions[MAX_RETRACTABLE_ASSERTIONS]; - Z3_ast core[MAX_RETRACTABLE_ASSERTIONS]; + Z3_ast_vector core; unsigned core_size; - Z3_ast dummy_proof = 0; // we don't care about the proof in this example. - Z3_model dummy_model = 0; // we don't care about the model in this example. unsigned i; for (i = 0; i < ctx->m_num_answer_literals; i++) { if (ctx->m_retracted[i] == Z3_FALSE) { @@ -2358,15 +2444,18 @@ Z3_lbool ext_check(Z3_ext_context ctx) { num_assumptions ++; } } - result = Z3_check_assumptions(ctx->m_context, num_assumptions, assumptions, &dummy_model, &dummy_proof, &core_size, core); + result = Z3_solver_check_assumptions(ctx->m_context, ctx->m_solver, num_assumptions, assumptions); if (result == Z3_L_FALSE) { // Display the UNSAT core printf("unsat core: "); + core = Z3_solver_get_unsat_core(ctx->m_context, ctx->m_solver); + core_size = Z3_ast_vector_size(ctx->m_context, core); for (i = 0; i < core_size; i++) { + // In this example, we display the core based on the assertion ids. unsigned j; for (j = 0; j < ctx->m_num_answer_literals; j++) { - if (core[i] == ctx->m_answer_literals[j]) { + if (Z3_ast_vector_get(ctx->m_context, core, i) == ctx->m_answer_literals[j]) { printf("%d ", j); break; } @@ -2378,10 +2467,6 @@ Z3_lbool ext_check(Z3_ext_context ctx) { printf("\n"); } - if (dummy_model) { - Z3_del_model(ctx->m_context, dummy_model); - } - return result; } @@ -2452,6 +2537,7 @@ void incremental_example1() { void reference_counter_example() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_sort ty; Z3_ast x, y, x_xor_y; Z3_symbol sx, sy; @@ -2465,6 +2551,8 @@ void reference_counter_example() { // Z3_ast reference counters. ctx = Z3_mk_context_rc(cfg); Z3_del_config(cfg); + s = mk_solver(ctx); + Z3_solver_inc_ref(ctx, s); ty = Z3_mk_bool_sort(ctx); Z3_inc_ref(ctx, Z3_sort_to_ast(ctx, ty)); // Z3_sort_to_ast(ty) is just syntax sugar for ((Z3_ast) ty) @@ -2482,17 +2570,19 @@ void reference_counter_example() { // x and y are not needed anymore. Z3_dec_ref(ctx, x); Z3_dec_ref(ctx, y); - Z3_assert_cnstr(ctx, x_xor_y); + Z3_solver_assert(ctx, s, x_xor_y); // x_or_y is not needed anymore. Z3_dec_ref(ctx, x_xor_y); printf("model for: x xor y\n"); - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); // Test push & pop - Z3_push(ctx); - Z3_pop(ctx, 1); + Z3_solver_push(ctx, s); + Z3_solver_pop(ctx, s, 1); + Z3_solver_dec_ref(ctx, s); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -2608,6 +2698,7 @@ void substitute_vars_example() { void fpa_example() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_sort double_sort, rm_sort; Z3_symbol s_rm, s_x, s_y, s_x_plus_y; Z3_ast rm, x, y, n, x_plus_y, c1, c2, c3, c4, c5; @@ -2618,6 +2709,7 @@ void fpa_example() { cfg = Z3_mk_config(); ctx = Z3_mk_context(cfg); + s = mk_solver(ctx); Z3_del_config(cfg); double_sort = Z3_mk_fpa_sort(ctx, 11, 53); @@ -2652,10 +2744,10 @@ void fpa_example() { c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3); printf("c4: %s\n", Z3_ast_to_string(ctx, c4)); - Z3_push(ctx); - Z3_assert_cnstr(ctx, c4); - check(ctx, Z3_L_TRUE); - Z3_pop(ctx, 1); + Z3_solver_push(ctx, s); + Z3_solver_assert(ctx, s, c4); + check(ctx, s, Z3_L_TRUE); + Z3_solver_pop(ctx, s, 1); // Show that the following are equal: // (fp #b0 #b10000000001 #xc000000000000) @@ -2663,7 +2755,7 @@ void fpa_example() { // ((_ to_fp 11 53) RTZ 1.75 2))) // ((_ to_fp 11 53) RTZ 7.0))) - Z3_push(ctx); + Z3_solver_push(ctx, s); c1 = Z3_mk_fpa_fp(ctx, Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)), Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)), @@ -2686,10 +2778,11 @@ void fpa_example() { c5 = Z3_mk_and(ctx, 3, args3); printf("c5: %s\n", Z3_ast_to_string(ctx, c5)); - Z3_assert_cnstr(ctx, c5); - check(ctx, Z3_L_TRUE); - Z3_pop(ctx, 1); + Z3_solver_assert(ctx, s, c5); + check(ctx, s, Z3_L_TRUE); + Z3_solver_pop(ctx, s, 1); + del_solver(ctx, s); Z3_del_context(ctx); } From 1575dd06a73e5dcdcdec57f41713d38126f49ab2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Nov 2015 09:42:12 -0800 Subject: [PATCH 50/53] expose labels from optimization. Move printing of objectives to after sat/unsat. Cahnge format to something that is somewhat related to how other output is created. Issue #325. Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 10 ++++++---- src/opt/opt_context.cpp | 14 ++++++++++++-- src/opt/opt_context.h | 2 +- 3 files changed, 19 insertions(+), 7 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index b018d62c5..6e443d476 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1401,9 +1401,10 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions unsigned rlimit = m_params.m_rlimit; scoped_watch sw(*this); lbool r; + bool was_pareto = false, was_opt = false; if (m_opt && !m_opt->empty()) { - bool was_pareto = false; + was_opt = true; m_check_sat_result = get_opt(); cancel_eh eh(*get_opt()); scoped_ctrl_c ctrlc(eh); @@ -1436,9 +1437,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions r = l_true; } get_opt()->set_status(r); - if (r != l_false && !was_pareto) { - get_opt()->display_assignment(regular_stream()); - } } else if (m_solver) { m_check_sat_result = m_solver.get(); // solver itself stores the result. @@ -1465,6 +1463,10 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions } display_sat_result(r); validate_check_sat_result(r); + if (was_opt && r != l_false && !was_pareto) { + get_opt()->display_assignment(regular_stream()); + } + if (r == l_true) { validate_model(); if (m_params.m_dump_models) { diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1b4b1e7bc..265e3b7c8 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -167,6 +167,12 @@ namespace opt { m_hard_constraints.reset(); } + void context::get_labels(svector & r) { + if (m_solver) { + m_solver->get_labels(r); + } + } + void context::set_hard_constraints(ptr_vector& fmls) { if (m_scoped_state.set(fmls)) { clear_state(); @@ -1121,16 +1127,20 @@ namespace opt { } void context::display_assignment(std::ostream& out) { + out << "(objectives\n"; for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) { objective const& obj = m_scoped_state.m_objectives[i]; + out << " ("; display_objective(out, obj); if (get_lower_as_num(i) != get_upper_as_num(i)) { - out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n"; + out << " (" << get_lower(i) << " " << get_upper(i) << ")"; } else { - out << " |-> " << get_lower(i) << "\n"; + out << " " << get_lower(i); } + out << ")\n"; } + out << ")\n"; } void context::display_objective(std::ostream& out, objective const& obj) const { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 735dc6905..b364fe63e 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -184,7 +184,7 @@ namespace opt { virtual void fix_model(model_ref& _m); virtual void collect_statistics(statistics& stats) const; virtual proof* get_proof() { return 0; } - virtual void get_labels(svector & r) {} + virtual void get_labels(svector & r); virtual void get_unsat_core(ptr_vector & r) {} virtual std::string reason_unknown() const; From 9cba63c31f6f1466dd4ef442bb840d1ab84539c7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Nov 2015 12:32:15 -0800 Subject: [PATCH 51/53] remove deprecated iz3 example. Remove deprecated process control Signed-off-by: Nikolaj Bjorner --- examples/interp/iz3.cpp | 458 ---------------------------------------- scripts/mk_project.py | 1 - src/api/api_context.cpp | 4 +- src/util/util.cpp | 21 -- src/util/util.h | 1 - 5 files changed, 1 insertion(+), 484 deletions(-) delete mode 100755 examples/interp/iz3.cpp diff --git a/examples/interp/iz3.cpp b/examples/interp/iz3.cpp deleted file mode 100755 index 21ea518a6..000000000 --- a/examples/interp/iz3.cpp +++ /dev/null @@ -1,458 +0,0 @@ - -/*++ -Copyright (c) 2015 Microsoft Corporation - ---*/ - -#include -#include -#include -#include -#include -#include "z3.h" - - - -int usage(const char **argv){ - std::cerr << "usage: " << argv[0] << " [options] file.smt" << std::endl; - std::cerr << std::endl; - std::cerr << "options:" << std::endl; - std::cerr << " -t,--tree tree interpolation" << std::endl; - std::cerr << " -c,--check check result" << std::endl; - std::cerr << " -p,--profile profile execution" << std::endl; - std::cerr << " -w,--weak weak interpolants" << std::endl; - std::cerr << " -f,--flat ouput flat formulas" << std::endl; - std::cerr << " -o ouput to SMT-LIB file" << std::endl; - std::cerr << " -a,--anon anonymize" << std::endl; - std::cerr << " -s,--simple simple proof mode" << std::endl; - std::cerr << std::endl; - return 1; -} - -int main(int argc, const char **argv) { - - bool tree_mode = false; - bool check_mode = false; - bool profile_mode = false; - bool incremental_mode = false; - std::string output_file; - bool flat_mode = false; - bool anonymize = false; - bool write = false; - - Z3_config cfg = Z3_mk_config(); - // Z3_interpolation_options options = Z3_mk_interpolation_options(); - // Z3_params options = 0; - - /* Parse the command line */ - int argn = 1; - while(argn < argc-1){ - std::string flag = argv[argn]; - if(flag[0] == '-'){ - if(flag == "-t" || flag == "--tree") - tree_mode = true; - else if(flag == "-c" || flag == "--check") - check_mode = true; - else if(flag == "-p" || flag == "--profile") - profile_mode = true; -#if 0 - else if(flag == "-w" || flag == "--weak") - Z3_set_interpolation_option(options,"weak","1"); - else if(flag == "--secondary") - Z3_set_interpolation_option(options,"secondary","1"); -#endif - else if(flag == "-i" || flag == "--incremental") - incremental_mode = true; - else if(flag == "-o"){ - argn++; - if(argn >= argc) return usage(argv); - output_file = argv[argn]; - } - else if(flag == "-f" || flag == "--flat") - flat_mode = true; - else if(flag == "-a" || flag == "--anon") - anonymize = true; - else if(flag == "-w" || flag == "--write") - write = true; - else if(flag == "-s" || flag == "--simple") - Z3_set_param_value(cfg,"PREPROCESS","false"); - else - return usage(argv); - } - argn++; - } - if(argn != argc-1) - return usage(argv); - const char *filename = argv[argn]; - - - /* Create a Z3 context to contain formulas */ - Z3_context ctx = Z3_mk_interpolation_context(cfg); - - if(write || anonymize) - Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT); - else if(!flat_mode) - Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB_COMPLIANT); - - /* Read an interpolation problem */ - - unsigned num; - Z3_ast *constraints; - unsigned *parents = 0; - const char *error; - bool ok; - unsigned num_theory; - Z3_ast *theory; - - ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory) != 0; - - /* If parse failed, print the error message */ - - if(!ok){ - std::cerr << error << "\n"; - return 1; - } - - /* if we get only one formula, and it is a conjunction, split it into conjuncts. */ - if(!tree_mode && num == 1){ - Z3_app app = Z3_to_app(ctx,constraints[0]); - Z3_func_decl func = Z3_get_app_decl(ctx,app); - Z3_decl_kind dk = Z3_get_decl_kind(ctx,func); - if(dk == Z3_OP_AND){ - int nconjs = Z3_get_app_num_args(ctx,app); - if(nconjs > 1){ - std::cout << "Splitting formula into " << nconjs << " conjuncts...\n"; - num = nconjs; - constraints = new Z3_ast[num]; - for(unsigned k = 0; k < num; k++) - constraints[k] = Z3_get_app_arg(ctx,app,k); - } - } - } - - /* Write out anonymized version. */ - - if(write || anonymize){ -#if 0 - Z3_anonymize_ast_vector(ctx,num,constraints); -#endif - std::string ofn = output_file.empty() ? "iz3out.smt2" : output_file; - Z3_write_interpolation_problem(ctx, num, constraints, parents, ofn.c_str(), num_theory, theory); - std::cout << "anonymized problem written to " << ofn << "\n"; - exit(0); - } - - /* Compute an interpolant, or get a model. */ - - Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast)); - Z3_model model = 0; - Z3_lbool result; - - if(!incremental_mode){ - /* In non-incremental mode, we just pass the constraints. */ - result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, constraints, parents, options, interpolants, &model, 0, false, num_theory, theory); - } - else { - - /* This is a somewhat useless demonstration of incremental mode. - Here, we assert the constraints in the context, then pass them to - iZ3 in an array, so iZ3 knows the sequence. Note it's safe to pass - "true", even though we haven't techically asserted if. */ - - Z3_push(ctx); - std::vector asserted(num); - - /* We start with nothing asserted. */ - for(unsigned i = 0; i < num; i++) - asserted[i] = Z3_mk_true(ctx); - - /* Now we assert the constrints one at a time until UNSAT. */ - - for(unsigned i = 0; i < num; i++){ - asserted[i] = constraints[i]; - Z3_assert_cnstr(ctx,constraints[i]); // assert one constraint - result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &model, 0, true, 0, 0); - if(result == Z3_L_FALSE){ - for(unsigned j = 0; j < num-1; j++) - /* Since we want the interpolant formulas to survive a "pop", we - "persist" them here. */ - Z3_persist_ast(ctx,interpolants[j],1); - break; - } - } - Z3_pop(ctx,1); - } - - switch (result) { - - /* If UNSAT, print the interpolants */ - case Z3_L_FALSE: - printf("unsat\n"); - if(output_file.empty()){ - printf("interpolant:\n"); - for(unsigned i = 0; i < num-1; i++) - printf("%s\n", Z3_ast_to_string(ctx, interpolants[i])); - } - else { -#if 0 - Z3_write_interpolation_problem(ctx,num-1,interpolants,0,output_file.c_str()); - printf("interpolant written to %s\n",output_file.c_str()); -#endif - } -#if 1 - if(check_mode){ - std::cout << "Checking interpolant...\n"; - bool chk; - chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory) != 0; - if(chk) - std::cout << "Interpolant is correct\n"; - else { - std::cout << "Interpolant is incorrect\n"; - std::cout << error; - return 1; - } - } -#endif - break; - case Z3_L_UNDEF: - printf("fail\n"); - break; - case Z3_L_TRUE: - printf("sat\n"); - printf("model:\n%s\n", Z3_model_to_string(ctx, model)); - break; - } - - if(profile_mode) - std::cout << Z3_interpolation_profile(ctx); - - /* Delete the model if there is one */ - - if (model) - Z3_del_model(ctx, model); - - /* Delete logical context. */ - - Z3_del_context(ctx); - free(interpolants); - - return 0; -} - - -#if 0 - - - -int test(){ - int i; - - /* Create a Z3 context to contain formulas */ - - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = iz3_mk_context(cfg); - - int num = 2; - - Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast)); - -#if 1 - Z3_sort arr = Z3_mk_array_sort(ctx,Z3_mk_int_sort(ctx),Z3_mk_bool_sort(ctx)); - Z3_symbol as = Z3_mk_string_symbol(ctx, "a"); - Z3_symbol bs = Z3_mk_string_symbol(ctx, "b"); - Z3_symbol xs = Z3_mk_string_symbol(ctx, "x"); - - Z3_ast a = Z3_mk_const(ctx,as,arr); - Z3_ast b = Z3_mk_const(ctx,bs,arr); - Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_int_sort(ctx)); - - Z3_ast c1 = Z3_mk_eq(ctx,a,Z3_mk_store(ctx,b,x,Z3_mk_true(ctx))); - Z3_ast c2 = Z3_mk_not(ctx,Z3_mk_select(ctx,a,x)); -#else - Z3_symbol xs = Z3_mk_string_symbol(ctx, "x"); - Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_bool_sort(ctx)); - Z3_ast c1 = Z3_mk_eq(ctx,x,Z3_mk_true(ctx)); - Z3_ast c2 = Z3_mk_eq(ctx,x,Z3_mk_false(ctx)); - -#endif - - constraints[0] = c1; - constraints[1] = c2; - - /* print out the result for grins. */ - - // Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx)); - - // Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]); - // Z3_string smtout = Z3_context_to_string(ctx); - // puts(smtout); - - iz3_print(ctx,num,constraints,"iZ3temp.smt"); - - /* Make room for interpolants. */ - - Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast)); - - /* Make room for the model. */ - - Z3_model model = 0; - - /* Call the prover */ - - Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model); - - switch (result) { - - /* If UNSAT, print the interpolants */ - case Z3_L_FALSE: - printf("unsat, interpolants:\n"); - for(i = 0; i < num-1; i++) - printf("%s\n", Z3_ast_to_string(ctx, interpolants[i])); - break; - case Z3_L_UNDEF: - printf("fail\n"); - break; - case Z3_L_TRUE: - printf("sat\n"); - printf("model:\n%s\n", Z3_model_to_string(ctx, model)); - break; - } - - /* Delete the model if there is one */ - - if (model) - Z3_del_model(ctx, model); - - /* Delete logical context (note, we call iz3_del_context, not - Z3_del_context */ - - iz3_del_context(ctx); - - return 1; -} - -struct z3_error { - Z3_error_code c; - z3_error(Z3_error_code _c) : c(_c) {} -}; - -extern "C" { - static void throw_z3_error(Z3_error_code c){ - throw z3_error(c); - } -} - -int main(int argc, const char **argv) { - - /* Create a Z3 context to contain formulas */ - - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = iz3_mk_context(cfg); - Z3_set_error_handler(ctx, throw_z3_error); - - /* Make some constraints, by parsing an smtlib formatted file given as arg 1 */ - - try { - Z3_parse_smtlib_file(ctx, argv[1], 0, 0, 0, 0, 0, 0); - } - catch(const z3_error &err){ - std::cerr << "Z3 error: " << Z3_get_error_msg(err.c) << "\n"; - std::cerr << Z3_get_smtlib_error(ctx) << "\n"; - return(1); - } - - /* Get the constraints from the parser. */ - - int num = Z3_get_smtlib_num_formulas(ctx); - - if(num == 0){ - std::cerr << "iZ3 error: File contains no formulas.\n"; - return 1; - } - - - Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast)); - - int i; - for (i = 0; i < num; i++) - constraints[i] = Z3_get_smtlib_formula(ctx, i); - - /* if we get only one formula, and it is a conjunction, split it into conjuncts. */ - if(num == 1){ - Z3_app app = Z3_to_app(ctx,constraints[0]); - Z3_func_decl func = Z3_get_app_decl(ctx,app); - Z3_decl_kind dk = Z3_get_decl_kind(ctx,func); - if(dk == Z3_OP_AND){ - int nconjs = Z3_get_app_num_args(ctx,app); - if(nconjs > 1){ - std::cout << "Splitting formula into " << nconjs << " conjuncts...\n"; - num = nconjs; - constraints = new Z3_ast[num]; - for(int k = 0; k < num; k++) - constraints[k] = Z3_get_app_arg(ctx,app,k); - } - } - } - - - /* print out the result for grins. */ - - // Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx)); - - // Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]); - // Z3_string smtout = Z3_context_to_string(ctx); - // puts(smtout); - - // iz3_print(ctx,num,constraints,"iZ3temp.smt"); - - /* Make room for interpolants. */ - - Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast)); - - /* Make room for the model. */ - - Z3_model model = 0; - - /* Call the prover */ - - Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model); - - switch (result) { - - /* If UNSAT, print the interpolants */ - case Z3_L_FALSE: - printf("unsat, interpolants:\n"); - for(i = 0; i < num-1; i++) - printf("%s\n", Z3_ast_to_string(ctx, interpolants[i])); - std::cout << "Checking interpolants...\n"; - const char *error; - if(iZ3_check_interpolant(ctx, num, constraints, 0, interpolants, &error)) - std::cout << "Interpolant is correct\n"; - else { - std::cout << "Interpolant is incorrect\n"; - std::cout << error << "\n"; - } - break; - case Z3_L_UNDEF: - printf("fail\n"); - break; - case Z3_L_TRUE: - printf("sat\n"); - printf("model:\n%s\n", Z3_model_to_string(ctx, model)); - break; - } - - /* Delete the model if there is one */ - - if (model) - Z3_del_model(ctx, model); - - /* Delete logical context (note, we call iz3_del_context, not - Z3_del_context */ - - iz3_del_context(ctx); - - return 0; -} - -#endif diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 2863de628..dfe801bdd 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -94,7 +94,6 @@ def init_project_def(): set_z3py_dir('api/python') # Examples add_cpp_example('cpp_example', 'c++') - add_cpp_example('iz3', 'interp') add_cpp_example('z3_tptp', 'tptp') add_c_example('c_example', 'c') add_c_example('maxsat') diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index f17a296fa..6749f1525 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -103,9 +103,7 @@ namespace api { m_smtlib_parser = 0; m_smtlib_parser_has_decls = false; - - z3_bound_num_procs(); - + m_error_handler = &default_error_handler; m_basic_fid = m().get_basic_family_id(); diff --git a/src/util/util.cpp b/src/util/util.cpp index c4b729adb..bfd4923a8 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -151,24 +151,3 @@ void escaped::display(std::ostream & out) const { } } -#ifdef _WINDOWS -#ifdef ARRAYSIZE -#undef ARRAYSIZE -#endif -#include -#endif - -void z3_bound_num_procs() { - -#ifdef _Z3_COMMERCIAL -#define Z3_COMMERCIAL_MAX_CORES 4 -#ifdef _WINDOWS - DWORD_PTR numProcs = (1 << Z3_COMMERCIAL_MAX_CORES) - 1; - SetProcessAffinityMask(GetCurrentProcess(), numProcs); -#endif -#else - // Not bounded: Research evaluations are - // not reasonable if run with artificial - // or hidden throttles. -#endif -} diff --git a/src/util/util.h b/src/util/util.h index f97f5c1f9..1e15b526c 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -400,7 +400,6 @@ inline size_t megabytes_to_bytes(unsigned mb) { return r; } -void z3_bound_num_procs(); #endif /* UTIL_H_ */ From c58e640563424747ecf086339aeb2f6437b46567 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Nov 2015 14:53:08 -0800 Subject: [PATCH 52/53] extract labels for optimal model. Fix to #325 Signed-off-by: Nikolaj Bjorner --- src/opt/maxsmt.cpp | 5 +++-- src/opt/maxsmt.h | 10 ++++++---- src/opt/opt_context.cpp | 16 +++++----------- src/opt/opt_context.h | 2 +- src/opt/opt_pareto.cpp | 2 ++ src/opt/opt_pareto.h | 5 +++-- src/opt/optsmt.cpp | 9 +++++++-- src/opt/optsmt.h | 3 ++- src/sat/sat_solver/inc_sat_solver.cpp | 1 - 9 files changed, 29 insertions(+), 24 deletions(-) diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 1bb521923..cb598617c 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -191,7 +191,7 @@ namespace opt { m_msolver->set_adjust_value(m_adjust_value); is_sat = (*m_msolver)(); if (is_sat != l_false) { - m_msolver->get_model(m_model); + m_msolver->get_model(m_model, m_labels); } } @@ -247,8 +247,9 @@ namespace opt { m_upper = r; } - void maxsmt::get_model(model_ref& mdl) { + void maxsmt::get_model(model_ref& mdl, svector& labels) { mdl = m_model.get(); + labels = m_labels; } void maxsmt::commit_assignment() { diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 8d290a640..7dbf763e2 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -46,7 +46,7 @@ namespace opt { virtual bool get_assignment(unsigned index) const = 0; virtual void set_cancel(bool f) = 0; virtual void collect_statistics(statistics& st) const = 0; - virtual void get_model(model_ref& mdl) = 0; + virtual void get_model(model_ref& mdl, svector& labels) = 0; virtual void updt_params(params_ref& p) = 0; void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; } @@ -67,6 +67,7 @@ namespace opt { rational m_lower; rational m_upper; model_ref m_model; + svector m_labels; svector m_assignment; // truth assignment to soft constraints params_ref m_params; // config @@ -79,9 +80,9 @@ namespace opt { virtual bool get_assignment(unsigned index) const { return m_assignment[index]; } virtual void set_cancel(bool f) { m_cancel = f; if (f) s().cancel(); else s().reset_cancel(); } virtual void collect_statistics(statistics& st) const { } - virtual void get_model(model_ref& mdl) { mdl = m_model.get(); } + virtual void get_model(model_ref& mdl, svector& labels) { mdl = m_model.get(); labels = m_labels;} virtual void commit_assignment(); - void set_model() { s().get_model(m_model); } + void set_model() { s().get_model(m_model); s().get_labels(m_labels); } virtual void updt_params(params_ref& p); solver& s(); void init(); @@ -122,6 +123,7 @@ namespace opt { rational m_upper; adjust_value m_adjust_value; model_ref m_model; + svector m_labels; params_ref m_params; public: maxsmt(maxsat_context& c); @@ -139,7 +141,7 @@ namespace opt { rational get_upper() const; void update_lower(rational const& r); void update_upper(rational const& r); - void get_model(model_ref& mdl); + void get_model(model_ref& mdl, svector& labels); bool get_assignment(unsigned index) const; void display_answer(std::ostream& out) const; void collect_statistics(statistics& st) const; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 265e3b7c8..1b33c2cf1 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -168,9 +168,7 @@ namespace opt { } void context::get_labels(svector & r) { - if (m_solver) { - m_solver->get_labels(r); - } + r.append(m_labels); } void context::set_hard_constraints(ptr_vector& fmls) { @@ -234,6 +232,7 @@ namespace opt { TRACE("opt", tout << "initial search result: " << is_sat << "\n";); if (is_sat != l_false) { s.get_model(m_model); + s.get_labels(m_labels); } if (is_sat != l_true) { return is_sat; @@ -282,11 +281,6 @@ namespace opt { } } - void context::set_model(model_ref& mdl) { - m_model = mdl; - fix_model(mdl); - } - void context::get_model(model_ref& mdl) { mdl = m_model; fix_model(mdl); @@ -295,7 +289,7 @@ namespace opt { lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) { if (scoped) get_solver().push(); lbool result = m_optsmt.lex(index, is_max); - if (result == l_true) m_optsmt.get_model(m_model); + if (result == l_true) m_optsmt.get_model(m_model, m_labels); if (scoped) get_solver().pop(1); if (result == l_true && committed) m_optsmt.commit_assignment(index); return result; @@ -306,7 +300,7 @@ namespace opt { maxsmt& ms = *m_maxsmts.find(id); if (scoped) get_solver().push(); lbool result = ms(); - if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model); + if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) ms.get_model(m_model, m_labels); if (scoped) get_solver().pop(1); if (result == l_true && committed) ms.commit_assignment(); return result; @@ -459,7 +453,7 @@ namespace opt { } void context::yield() { - m_pareto->get_model(m_model); + m_pareto->get_model(m_model, m_labels); update_bound(true); update_bound(false); } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index b364fe63e..dc180e8e6 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -162,6 +162,7 @@ namespace opt { bool m_pp_neat; symbol m_maxsat_engine; symbol m_logic; + svector m_labels; public: context(ast_manager& m); virtual ~context(); @@ -180,7 +181,6 @@ namespace opt { virtual lbool optimize(); virtual bool print_model() const; virtual void get_model(model_ref& _m); - virtual void set_model(model_ref& _m); virtual void fix_model(model_ref& _m); virtual void collect_statistics(statistics& stats) const; virtual proof* get_proof() { return 0; } diff --git a/src/opt/opt_pareto.cpp b/src/opt/opt_pareto.cpp index 5e1d4b269..dea744a72 100644 --- a/src/opt/opt_pareto.cpp +++ b/src/opt/opt_pareto.cpp @@ -38,6 +38,7 @@ namespace opt { return l_undef; } m_solver->get_model(m_model); + m_solver->get_labels(m_labels); IF_VERBOSE(1, model_ref mdl(m_model); cb.fix_model(mdl); @@ -96,6 +97,7 @@ namespace opt { } if (is_sat == l_true) { m_solver->get_model(m_model); + m_solver->get_labels(m_labels); mk_not_dominated_by(); } return is_sat; diff --git a/src/opt/opt_pareto.h b/src/opt/opt_pareto.h index 88a3ce9c1..122f29c55 100644 --- a/src/opt/opt_pareto.h +++ b/src/opt/opt_pareto.h @@ -31,7 +31,6 @@ namespace opt { virtual expr_ref mk_gt(unsigned i, model_ref& model) = 0; virtual expr_ref mk_ge(unsigned i, model_ref& model) = 0; virtual expr_ref mk_le(unsigned i, model_ref& model) = 0; - virtual void set_model(model_ref& m) = 0; virtual void fix_model(model_ref& m) = 0; }; class pareto_base { @@ -42,6 +41,7 @@ namespace opt { ref m_solver; params_ref m_params; model_ref m_model; + svector m_labels; public: pareto_base( ast_manager & m, @@ -77,8 +77,9 @@ namespace opt { } virtual lbool operator()() = 0; - virtual void get_model(model_ref& mdl) { + virtual void get_model(model_ref& mdl, svector& labels) { mdl = m_model; + labels = m_labels; } protected: diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 02effa337..c9ee61ebc 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -51,6 +51,7 @@ namespace opt { if (src[i] >= dst[i]) { dst[i] = src[i]; m_models.set(i, m_s->get_model(i)); + m_s->get_labels(m_labels); m_lower_fmls[i] = fmls[i].get(); if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already. m_lower_fmls[i] = m.mk_false(); @@ -156,7 +157,8 @@ namespace opt { if (is_sat == l_true) { disj.reset(); m_s->maximize_objectives(disj); - m_s->get_model(m_model); + m_s->get_model(m_model); + m_s->get_labels(m_labels); for (unsigned i = 0; i < ors.size(); ++i) { expr_ref tmp(m); m_model->eval(ors[i].get(), tmp); @@ -203,6 +205,7 @@ namespace opt { expr_ref optsmt::update_lower() { expr_ref_vector disj(m); m_s->get_model(m_model); + m_s->get_labels(m_labels); m_s->maximize_objectives(disj); set_max(m_lower, m_s->get_objective_values(), disj); TRACE("opt", @@ -331,6 +334,7 @@ namespace opt { m_s->maximize_objective(obj_index, block); m_s->get_model(m_model); + m_s->get_labels(m_labels); inf_eps obj = m_s->saved_objective_value(obj_index); if (obj > m_lower[obj_index]) { m_lower[obj_index] = obj; @@ -405,8 +409,9 @@ namespace opt { return m_upper[i]; } - void optsmt::get_model(model_ref& mdl) { + void optsmt::get_model(model_ref& mdl, svector & labels) { mdl = m_model.get(); + labels = m_labels; } // force lower_bound(i) <= objective_value(i) diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index 10ea9f11c..f4efa25f9 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -38,6 +38,7 @@ namespace opt { svector m_vars; symbol m_optsmt_engine; model_ref m_model; + svector m_labels; sref_vector m_models; public: optsmt(ast_manager& m): @@ -60,7 +61,7 @@ namespace opt { inf_eps get_lower(unsigned index) const; inf_eps get_upper(unsigned index) const; bool objective_is_model_valid(unsigned index) const; - void get_model(model_ref& mdl); + void get_model(model_ref& mdl, svector& labels); model* get_model(unsigned index) const { return m_models[index]; } void update_lower(unsigned idx, inf_eps const& r); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index b0d771ba8..43b2c2e3f 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -250,7 +250,6 @@ public: return "no reason given"; } virtual void get_labels(svector & r) { - UNREACHABLE(); } virtual unsigned get_num_assertions() const { return m_fmls.size(); From 5948013b1b04d8529bce366c0c7b87e1d88a1827 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Nov 2015 18:56:54 -0800 Subject: [PATCH 53/53] clear label buffer Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 8652ab7fd..d7e3c8590 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -282,6 +282,7 @@ namespace opt { } void opt_solver::get_labels(svector & r) { + r.reset(); buffer tmp; m_context.get_relevant_labels(0, tmp); r.append(tmp.size(), tmp.c_ptr());