From ac732a500cb90d255f7bf4cee992a04fb5a97ef3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 May 2015 15:20:25 -0700 Subject: [PATCH 1/7] add first file Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbp.h | 51 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 src/qe/qe_mbp.h diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h new file mode 100644 index 000000000..b8a73a890 --- /dev/null +++ b/src/qe/qe_mbp.h @@ -0,0 +1,51 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qe_mbp.h + +Abstract: + + Model-based projection utilities + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-28 + +Revision History: + + +--*/ + +#ifndef __QE_MBP_H__ +#define __QE_MBP_H__ + +#include "ast.h" +#include "params.h" + +class qe_mbp { + class impl; + impl * m_impl; +public: + qe_mbp(ast_manager& m); + + ~qe_mbp(); + + /** + \brief + Apply model-based qe on constants provided as vector of variables. + Return the updated formula and updated set of variables that were not eliminated. + + */ + void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml); + + /** + \brief full rewriting based light-weight quantifier elimination round. + */ + void operator()(expr_ref& fml, proof_ref& pr); + + void set_cancel(bool f); +}; + +#endif From e47eea2c610e19e1afde2ac3df5565aca755a4d4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 May 2015 17:22:34 -0700 Subject: [PATCH 2/7] n/a Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbp.h | 43 +++++------ src/qe/qsat.cpp | 200 ++++++++++++++++++++++++++++++++++++++++++++++++ src/qe/qsat.h | 52 +++++++++++++ 3 files changed, 272 insertions(+), 23 deletions(-) create mode 100644 src/qe/qsat.cpp create mode 100644 src/qe/qsat.h diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h index b8a73a890..11bceef0b 100644 --- a/src/qe/qe_mbp.h +++ b/src/qe/qe_mbp.h @@ -24,28 +24,25 @@ Revision History: #include "ast.h" #include "params.h" -class qe_mbp { - class impl; - impl * m_impl; -public: - qe_mbp(ast_manager& m); - - ~qe_mbp(); - - /** - \brief - Apply model-based qe on constants provided as vector of variables. - Return the updated formula and updated set of variables that were not eliminated. - - */ - void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml); - - /** - \brief full rewriting based light-weight quantifier elimination round. - */ - void operator()(expr_ref& fml, proof_ref& pr); - - void set_cancel(bool f); -}; +namespace qe { + class mbp { + class impl; + impl * m_impl; + public: + mbp(ast_manager& m); + + ~mbp(); + + /** + \brief + Apply model-based qe on constants provided as vector of variables. + Return the updated formula and updated set of variables that were not eliminated. + + */ + void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml); + + void set_cancel(bool f); + }; +} #endif diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp new file mode 100644 index 000000000..6a59b40cd --- /dev/null +++ b/src/qe/qsat.cpp @@ -0,0 +1,200 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qsat.cpp + +Abstract: + + Quantifier Satisfiability Solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-28 + +Revision History: + + +--*/ + +#include "qsat.h" +#include "smt_kernel.h" +#include "qe_mbp.h" + +namespace qe; + +sturct qdef_t { + expr_ref m_pred; + expr_ref m_expr; + expr_ref_vector m_vars; + bool m_is_forall; + qdef_t(expr_ref& p, expr_ref& e, expr_ref_vector const& vars, bool is_forall): + m_pred(p), + m_expr(e), + m_vars(vars), + m_is_forall(is_forall) {} +}; + +typedef vector qdefs_t; + +struct pdef_t { + expr_ref m_pred; + expr_ref m_atom; + pdef_t(expr_ref& p, expr_ref& a): + m_pred(p), + m_atom(a) + {} +}; + +class qsat::impl { + ast_manager& m; + mbp mbp; + + /** + \brief replace quantified sub-formulas by a predicate, introduce definitions for the predicate. + */ + void remove_quantifiers(expr_ref_vector& fmls, qdefs_t& defs) { + + } + + /** + \brief create propositional abstration of formula by replacing atomic sub-formulas by fresh + propositional variables, and adding definitions for each propositional formula on the side. + Assumption is that the formula is quantifier-free. + */ + void mk_abstract(expr_ref_vector& fmls, vector& pdefs) { + expr_ref_vector todo(fmls), trail(m); + obj_map cache; + ptr_vector args; + expr_ref r(m); + while (!todo.empty()) { + expr* e = todo.back(); + if (cache.contains(e)) { + todo.pop_back(); + continue; + } + SASSERT(is_app(e)); + app* a = to_app(e); + if (a->get_family_id() == m.get_basic_family_id()) { + unsigned sz = a->get_num_args(); + args.reset(); + for (unsigned i = 0; i < sz; ++i) { + expr* f = a->get_arg(i); + if (cache.find(f, f)) { + args.push_back(f); + } + else { + todo.push_back(f); + } + } + if (args.size() == sz) { + r = m.mk_app(a->get_decl(), sz, args.c_ptr()); + cache.insert(e, r); + trail.push_back(r); + todo.pop_back(e); + } + } + else if (is_uninterpreted_const(a)) { + cache.insert(e, e); + } + else { + // TBD: nested Booleans. + r = m.mk_fresh_const("p",m.mk_bool_sort()); + trail.push_back(r); + cache.insert(e, r); + pdefs.push_back(pdef_t(e, r)); + } + } + + for (unsigned i = 0; i < fmls.size(); ++i) { + fmls[i] = cache.find(fmls[i].get()); + } + } + + /** + \brief use dual propagation to minimize model. + */ + void minimize_assignment(app_ref_vector& assignment) { + + } + +public: + impl(ast_manager& m): + m(m), + mbp(m) {} + + void updt_params(params_ref const & p) { + } + void collect_param_descrs(param_descrs & r) { + } + void operator()(/* in */ goal_ref const & in, + /* out */ goal_ref_buffer & result, + /* out */ model_converter_ref & mc, + /* out */ proof_converter_ref & pc, + /* out */ expr_dependency_ref & core) { + + } + + void collect_statistics(statistics & st) const { + + } + void reset_statistics() { + } + void cleanup() { + } + void set_logic(symbol const & l) { + } + void set_progress_callback(progress_callback * callback) { + } + tactic * translate(ast_manager & m) { + return 0; + } + +}; + +qsat::qsat(ast_manager& m) { + m_impl = alloc(impl, m); +} + +qsat::~qsat() { + dealloc(m_impl); +} + +void qsat::updt_params(params_ref const & p) { + m_impl->updt_params(p); +} +void qsat::collect_param_descrs(param_descrs & r) { + m_impl->collect_param_descrs(r); +} +void qsat::operator()(/* in */ goal_ref const & in, + /* out */ goal_ref_buffer & result, + /* out */ model_converter_ref & mc, + /* out */ proof_converter_ref & pc, + /* out */ expr_dependency_ref & core) { + (*m_impl)(in, result, mc, pc, core); +} + +void qsat::collect_statistics(statistics & st) const { + m_impl->collect_statistics(st); +} +void qsat::reset_statistics() { + m_impl->reset_statistics(); +} +void qsat::cleanup() { + m_impl->cleanup(); +} +void qsat::set_logic(symbol const & l) { + m_impl->set_logic(l); +} +void qsat::set_progress_callback(progress_callback * callback) { + m_impl->set_progress_callback(callback); +} +tactic * qsat::translate(ast_manager & m) { + return m_impl->translate(m); +} + + +}; + +#endif diff --git a/src/qe/qsat.h b/src/qe/qsat.h new file mode 100644 index 000000000..23d506294 --- /dev/null +++ b/src/qe/qsat.h @@ -0,0 +1,52 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qsat.h + +Abstract: + + Quantifier Satisfiability Solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-28 + +Revision History: + + +--*/ + +#ifndef __QE_MBP_H__ +#define __QE_MBP_H__ + +#include "tactic.h" + +namespace qe { + class qsat : public tactic { + class impl; + impl * m_impl; + public: + qsat(ast_manager& m); + ~qsat(); + + virtual void updt_params(params_ref const & p); + virtual void collect_param_descrs(param_descrs & r); + virtual void operator()(/* in */ goal_ref const & in, + /* out */ goal_ref_buffer & result, + /* out */ model_converter_ref & mc, + /* out */ proof_converter_ref & pc, + /* out */ expr_dependency_ref & core); + + virtual void collect_statistics(statistics & st) const; + virtual void reset_statistics(); + virtual void cleanup() = 0; + virtual void set_logic(symbol const & l); + virtual void set_progress_callback(progress_callback * callback); + virtual tactic * translate(ast_manager & m); + + }; +}; + +#endif From ed7e0e11a80a2d6cad4c8a11eaa0e2fbdc5ee3e8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 May 2015 20:55:13 -0700 Subject: [PATCH 3/7] n/a Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 4 ++ src/muz/base/dl_context.cpp | 4 ++ src/opt/opt_cmds.cpp | 6 +- src/opt/opt_context.cpp | 4 ++ src/qe/qsat.cpp | 131 +++++++++++++++++++++++++++------- src/qe/qsat.h | 4 +- src/smt/theory_array_full.cpp | 37 +++++----- src/smt/theory_array_full.h | 7 +- 8 files changed, 142 insertions(+), 55 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index e57050e82..ca15762f5 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -355,6 +355,10 @@ extern "C" { init_solver(c, s); Z3_stats_ref * st = alloc(Z3_stats_ref); to_solver_ref(s)->collect_statistics(st->m_stats); + unsigned long long max_mem = memory::get_max_used_memory(); + unsigned long long mem = memory::get_allocation_size(); + st->m_stats.update("max memory", static_cast(max_mem)/(1024.0*1024.0)); + st->m_stats.update("memory", static_cast(mem)/(1024.0*1024.0)); mk_c(c)->save_object(st); Z3_stats r = of_stats(st); RETURN_Z3(r); diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index bd70c06ef..3555e5bdc 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -945,6 +945,10 @@ namespace datalog { if (m_engine) { m_engine->collect_statistics(st); } + unsigned long long max_mem = memory::get_max_used_memory(); + unsigned long long mem = memory::get_allocation_size(); + st.update("max memory", static_cast(max_mem)/(1024.0*1024.0)); + st.update("memory", static_cast(mem)/(1024.0*1024.0)); } diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 537f4bf22..01324fc67 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -323,12 +323,8 @@ private: void display_statistics(cmd_context& ctx) { statistics stats; - unsigned long long max_mem = memory::get_max_used_memory(); - unsigned long long mem = memory::get_allocation_size(); - stats.update("time", ctx.get_seconds()); - stats.update("memory", static_cast(mem)/static_cast(1024*1024)); - stats.update("max memory", static_cast(max_mem)/static_cast(1024*1024)); get_opt(ctx).collect_statistics(stats); + stats.update("time", ctx.get_seconds()); stats.display_smt2(ctx.regular_stream()); } }; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 857b57296..5353d9b53 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1179,6 +1179,10 @@ namespace opt { for (; it != end; ++it) { it->m_value->collect_statistics(stats); } + unsigned long long max_mem = memory::get_max_used_memory(); + unsigned long long mem = memory::get_allocation_size(); + stats.update("memory", static_cast(mem)/static_cast(1024*1024)); + stats.update("max memory", static_cast(max_mem)/static_cast(1024*1024)); } void context::collect_param_descrs(param_descrs & r) { diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 6a59b40cd..4c736bc31 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -21,10 +21,12 @@ Revision History: #include "qsat.h" #include "smt_kernel.h" #include "qe_mbp.h" +#include "smt_params.h" +#include "ast_util.h" -namespace qe; +using namespace qe; -sturct qdef_t { +struct qdef_t { expr_ref m_pred; expr_ref m_expr; expr_ref_vector m_vars; @@ -41,15 +43,25 @@ typedef vector qdefs_t; struct pdef_t { expr_ref m_pred; expr_ref m_atom; - pdef_t(expr_ref& p, expr_ref& a): - m_pred(p), - m_atom(a) + pdef_t(expr_ref& p, expr* a): + m_pred(p), + m_atom(a, p.get_manager()) {} }; class qsat::impl { - ast_manager& m; - mbp mbp; + ast_manager& m; + qe::mbp mbp; + smt_params m_smtp; + smt::kernel m_kernel; + expr_ref m_fml_pred; // predicate that encodes top-level formula + expr_ref_vector m_atoms; // predicates that encode atomic subformulas + + + lbool check_sat() { + // TBD main procedure goes here. + return l_undef; + } /** \brief replace quantified sub-formulas by a predicate, introduce definitions for the predicate. @@ -63,11 +75,12 @@ class qsat::impl { propositional variables, and adding definitions for each propositional formula on the side. Assumption is that the formula is quantifier-free. */ - void mk_abstract(expr_ref_vector& fmls, vector& pdefs) { - expr_ref_vector todo(fmls), trail(m); + void mk_abstract(expr_ref& fml, vector& pdefs) { + expr_ref_vector todo(m), trail(m); obj_map cache; ptr_vector args; expr_ref r(m); + todo.push_back(fml); while (!todo.empty()) { expr* e = todo.back(); if (cache.contains(e)) { @@ -87,47 +100,114 @@ class qsat::impl { else { todo.push_back(f); } - } + } if (args.size() == sz) { r = m.mk_app(a->get_decl(), sz, args.c_ptr()); cache.insert(e, r); trail.push_back(r); - todo.pop_back(e); + todo.pop_back(); } } - else if (is_uninterpreted_const(a)) { + else if (is_uninterp_const(a)) { cache.insert(e, e); } else { - // TBD: nested Booleans. + // TBD: nested Booleans. + r = m.mk_fresh_const("p",m.mk_bool_sort()); trail.push_back(r); cache.insert(e, r); - pdefs.push_back(pdef_t(e, r)); + pdefs.push_back(pdef_t(r, e)); } } - - for (unsigned i = 0; i < fmls.size(); ++i) { - fmls[i] = cache.find(fmls[i].get()); - } + fml = cache.find(fml); } /** \brief use dual propagation to minimize model. */ - void minimize_assignment(app_ref_vector& assignment) { - + bool minimize_assignment(expr_ref_vector& assignment, expr* not_fml) { + bool result = false; + assignment.push_back(not_fml); + lbool res = m_kernel.check(assignment.size(), assignment.c_ptr()); + switch (res) { + case l_true: + UNREACHABLE(); + break; + case l_undef: + break; + case l_false: + result = true; + get_core(assignment, not_fml); + break; + } + return result; + } + + lbool check_sat(expr_ref_vector& assignment, expr* fml) { + assignment.push_back(fml); + lbool res = m_kernel.check(assignment.size(), assignment.c_ptr()); + switch (res) { + case l_true: { + model_ref mdl; + expr_ref tmp(m); + assignment.reset(); + m_kernel.get_model(mdl); + for (unsigned i = 0; i < m_atoms.size(); ++i) { + expr* p = m_atoms[i].get(); + if (mdl->eval(p, tmp)) { + if (m.is_true(tmp)) { + assignment.push_back(p); + } + else if (m.is_false(tmp)) { + assignment.push_back(m.mk_not(p)); + } + } + } + expr_ref not_fml = mk_not(fml); + if (!minimize_assignment(assignment, not_fml)) { + res = l_undef; + } + break; + } + case l_undef: + break; + case l_false: + get_core(assignment, fml); + break; + } + return res; + } + + void get_core(expr_ref_vector& core, expr* exclude) { + unsigned sz = m_kernel.get_unsat_core_size(); + core.reset(); + for (unsigned i = 0; i < sz; ++i) { + expr* e = m_kernel.get_unsat_core_expr(i); + if (e != exclude) { + core.push_back(e); + } + } + } + + expr_ref mk_not(expr* e) { + return expr_ref(::mk_not(m, e), m); } public: impl(ast_manager& m): m(m), - mbp(m) {} - + mbp(m), + m_kernel(m, m_smtp), + m_fml_pred(m), + m_atoms(m) {} + void updt_params(params_ref const & p) { } + void collect_param_descrs(param_descrs & r) { } + void operator()(/* in */ goal_ref const & in, /* out */ goal_ref_buffer & result, /* out */ model_converter_ref & mc, @@ -141,12 +221,16 @@ public: } void reset_statistics() { } + void cleanup() { } + void set_logic(symbol const & l) { } + void set_progress_callback(progress_callback * callback) { } + tactic * translate(ast_manager & m) { return 0; } @@ -195,6 +279,3 @@ tactic * qsat::translate(ast_manager & m) { } -}; - -#endif diff --git a/src/qe/qsat.h b/src/qe/qsat.h index 23d506294..2fc071c76 100644 --- a/src/qe/qsat.h +++ b/src/qe/qsat.h @@ -18,8 +18,8 @@ Revision History: --*/ -#ifndef __QE_MBP_H__ -#define __QE_MBP_H__ +#ifndef __QE_QSAT_H__ +#define __QE_QSAT_H__ #include "tactic.h" diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 28314c421..dd74f2871 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -208,6 +208,8 @@ namespace smt { theory_array::reset_eh(); std::for_each(m_var_data_full.begin(), m_var_data_full.end(), delete_proc()); m_var_data_full.reset(); + m_eqs.reset(); + m_eqsv.reset(); } void theory_array_full::display_var(std::ostream & out, theory_var v) const { @@ -223,7 +225,6 @@ namespace smt { } theory_var theory_array_full::mk_var(enode * n) { - theory_var r = theory_array::mk_var(n); SASSERT(r == static_cast(m_var_data_full.size())); m_var_data_full.push_back(alloc(var_data_full)); @@ -512,7 +513,7 @@ namespace smt { TRACE("array_map_bug", tout << "select-map axiom\n" << mk_ismt2_pp(sel1, m) << "\n=\n" << mk_ismt2_pp(sel2,m) << "\n";); - + return try_assign_eq(sel1, sel2); } @@ -760,36 +761,30 @@ namespace smt { r = FC_CONTINUE; } } + while (!m_eqsv.empty()) { + literal eq = m_eqsv.back(); + m_eqsv.pop_back(); + get_context().mark_as_relevant(eq); + assert_axiom(eq); + r = FC_CONTINUE; + } if (r == FC_DONE && m_found_unsupported_op) r = FC_GIVEUP; return r; } + bool theory_array_full::try_assign_eq(expr* v1, expr* v2) { context& ctx = get_context(); - enode* n1 = ctx.get_enode(v1); - enode* n2 = ctx.get_enode(v2); - if (n1->get_root() == n2->get_root()) { + if (m_eqs.contains(v1, v2)) { return false; } + m_eqs.insert(v1, v2, true); TRACE("array", tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" << mk_bounded_pp(v2, get_manager()) << "\n";); - -#if 0 - if (m.proofs_enabled()) { -#endif - literal eq(mk_eq(v1,v2,true)); - ctx.mark_as_relevant(eq); - assert_axiom(eq); -#if 0 - } - else { - ctx.mark_as_relevant(n1); - ctx.mark_as_relevant(n2); - ctx.assign_eq(n1, n2, eq_justification::mk_axiom()); - } -#endif + literal eq(mk_eq(v1, v2, true)); + m_eqsv.push_back(eq); return true; } @@ -798,6 +793,8 @@ namespace smt { theory_array::pop_scope_eh(num_scopes); std::for_each(m_var_data_full.begin() + num_old_vars, m_var_data_full.end(), delete_proc()); m_var_data_full.shrink(num_old_vars); + m_eqs.reset(); + m_eqsv.reset(); } void theory_array_full::collect_statistics(::statistics & st) const { diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h index 7c066f765..bbbf35408 100644 --- a/src/smt/theory_array_full.h +++ b/src/smt/theory_array_full.h @@ -38,12 +38,12 @@ namespace smt { ast2ast_trailmap m_sort2epsilon; simplifier* m_simp; + obj_pair_map m_eqs; + svector m_eqsv; protected: -#if 0 - virtual final_check_status final_check_eh(); -#endif + //virtual final_check_status final_check_eh(); virtual void reset_eh(); virtual void set_prop_upward(theory_var v); @@ -84,6 +84,7 @@ namespace smt { bool try_assign_eq(expr* n1, expr* n2); + void assign_eqs(); public: From a2448be0cde41a774f8321d94521373563285608 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 May 2015 08:55:44 -0700 Subject: [PATCH 4/7] print pareto model in check-sat too Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 10 ++++++++++ src/cmd_context/cmd_context.h | 1 + src/opt/opt_context.cpp | 6 ++++++ src/opt/opt_context.h | 1 + 4 files changed, 18 insertions(+) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 80aa10cde..187c7ba63 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -40,6 +40,7 @@ Notes: #include"for_each_expr.h" #include"scoped_timer.h" #include"interpolant_cmds.h" +#include"model_smt2_pp.h" func_decls::func_decls(ast_manager & m, func_decl * f): m_decls(TAG(func_decl*, f, 0)) { @@ -1402,6 +1403,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions was_pareto = true; get_opt()->display_assignment(regular_stream()); regular_stream() << "\n"; + if (get_opt()->print_model()) { + model_ref mdl; + get_opt()->get_model(mdl); + if (mdl) { + regular_stream() << "(model " << std::endl; + model_smt2_pp(regular_stream(), *this, *(mdl.get()), 2); + regular_stream() << ")" << std::endl; + } + } r = get_opt()->optimize(); } } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 148bb61d9..795b3a65a 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -124,6 +124,7 @@ public: virtual void display_assignment(std::ostream& out) = 0; virtual bool is_pareto() = 0; virtual void set_logic(symbol const& s) = 0; + virtual bool print_model() const = 0; }; class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context { diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 857b57296..f5a3b5c67 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -254,6 +254,12 @@ namespace opt { } } + + bool context::print_model() const { + opt_params optp(m_params); + return optp.print_model(); + } + void context::get_base_model(model_ref& mdl) { mdl = m_model; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 59868dd1e..eabc2550f 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -180,6 +180,7 @@ namespace opt { virtual void cancel() { set_cancel(true); } virtual void set_hard_constraints(ptr_vector & hard); 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); From f8e2fa03379d752fc400376f312a5d8115e173fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 May 2015 11:11:13 -0700 Subject: [PATCH 5/7] fixes issue #93 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array_full.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index dd74f2871..f2d1527c0 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -775,17 +775,19 @@ namespace smt { bool theory_array_full::try_assign_eq(expr* v1, expr* v2) { + TRACE("array", + tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" + << mk_bounded_pp(v2, get_manager()) << "\n";); context& ctx = get_context(); if (m_eqs.contains(v1, v2)) { return false; } - m_eqs.insert(v1, v2, true); - TRACE("array", - tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" - << mk_bounded_pp(v2, get_manager()) << "\n";); - literal eq(mk_eq(v1, v2, true)); - m_eqsv.push_back(eq); - return true; + else { + m_eqs.insert(v1, v2, true); + literal eq(mk_eq(v1, v2, true)); + m_eqsv.push_back(eq); + return true; + } } void theory_array_full::pop_scope_eh(unsigned num_scopes) { From 894d6cb11b4be3750d32ca42218f8f379f7b9e25 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 May 2015 13:38:54 -0700 Subject: [PATCH 6/7] fix build break to support new statistics items Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 16d2eb6ba..6d0c5bad0 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -5617,7 +5617,7 @@ class Statistics: sat >>> st = s.statistics() >>> len(st) - 2 + 4 """ return int(Z3_stats_size(self.ctx.ref(), self.stats)) @@ -5631,7 +5631,7 @@ class Statistics: sat >>> st = s.statistics() >>> len(st) - 2 + 4 >>> st[0] ('nlsat propagations', 2) >>> st[1] @@ -5655,7 +5655,7 @@ class Statistics: sat >>> st = s.statistics() >>> st.keys() - ['nlsat propagations', 'nlsat stages'] + ['nlsat propagations', 'nlsat stages', 'max memory', 'memory'] """ return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))] @@ -5692,7 +5692,7 @@ class Statistics: sat >>> st = s.statistics() >>> st.keys() - ['nlsat propagations', 'nlsat stages'] + ['nlsat propagations', 'nlsat stages', 'max memory', 'memory'] >>> st.nlsat_propagations 2 >>> st.nlsat_stages From 2d409c6042318e74d6d1b8adfc5c36225b53a691 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 May 2015 14:32:24 -0700 Subject: [PATCH 7/7] revert bug introduced to avoid stack overflow in arrays Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array_full.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index f2d1527c0..4e169a8be 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -785,7 +785,10 @@ namespace smt { else { m_eqs.insert(v1, v2, true); literal eq(mk_eq(v1, v2, true)); - m_eqsv.push_back(eq); + get_context().mark_as_relevant(eq); + assert_axiom(eq); + + // m_eqsv.push_back(eq); return true; } }