From 8c4d791f011263d1867f5b5c14f11ed11a0d00b8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Mar 2016 08:08:17 -0800 Subject: [PATCH 1/4] use std::vector per Nuno's analysis to fix #420 Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_sym_mux.h | 3 ++- src/test/model_evaluator.cpp | 26 ++++++++++++++++---------- 2 files changed, 18 insertions(+), 11 deletions(-) diff --git a/src/muz/pdr/pdr_sym_mux.h b/src/muz/pdr/pdr_sym_mux.h index bc1819539..78025f26b 100644 --- a/src/muz/pdr/pdr_sym_mux.h +++ b/src/muz/pdr/pdr_sym_mux.h @@ -23,6 +23,7 @@ Revision History: #include "ast.h" #include "map.h" #include "vector.h" +#include class model_core; @@ -46,7 +47,7 @@ private: mutable unsigned m_next_sym_suffix_idx; mutable symbols m_used_suffixes; /** Here we have default suffixes for each of the variants */ - vector m_suffixes; + std::vector m_suffixes; /** diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp index 6e3a1f441..0b509fba6 100644 --- a/src/test/model_evaluator.cpp +++ b/src/test/model_evaluator.cpp @@ -26,13 +26,19 @@ void tst_model_evaluator() { expr_ref vB0(m.mk_var(0, m.mk_bool_sort()), m); expr_ref vB1(m.mk_var(1, m.mk_bool_sort()), m); expr_ref vB2(m.mk_var(2, m.mk_bool_sort()), m); - expr_ref f01(m.mk_app(f, vI0, vB1), m); - expr_ref g01(m.mk_app(g, vI0, vB1), m); - expr_ref h01(m.mk_app(h, vI0, vB1), m); + expr* vI0p = vI0.get(); + expr* vI1p = vI1.get(); + expr* vB0p = vB0.get(); + expr* vB1p = vB1.get(); + expr* vB2p = vB2.get(); + + expr_ref f01(m.mk_app(f, vI0p, vB1p), m); + expr_ref g01(m.mk_app(g, vI0p, vB1p), m); + expr_ref h01(m.mk_app(h, vI0p, vB1p), m); func_interp* fi = alloc(func_interp, m, 2); func_interp* gi = alloc(func_interp, m, 2); func_interp* hi = alloc(func_interp, m, 2); - hi->set_else(m.mk_ite(vB1, m.mk_app(f, vI0, vB1), m.mk_app(g, vI0, vB1))); + hi->set_else(m.mk_ite(vB1p, m.mk_app(f, vI0p, vB1p), m.mk_app(g, vI0p, vB1p))); mdl.register_decl(h, hi); @@ -42,23 +48,23 @@ void tst_model_evaluator() { { symbol nI("N"); - fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(F, vI1, vB2))), vI0, a.mk_int(1))); - gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(G, vI1, vB2))), a.mk_int(2), vI0)); + fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(F, vI1p, vB2p))), vI0p, a.mk_int(1))); + gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(G, vI1p, vB2p))), a.mk_int(2), vI0p)); mdl.register_decl(g, gi); mdl.register_decl(f, fi); model_pp(std::cout, mdl); - e = m.mk_app(h, vI0, vB1); + e = m.mk_app(h, vI0p, vB1p); eval(e, v); std::cout << e << " " << v << "\n"; } { - fi->set_else(m.mk_app(F, vI0, vB1)); - gi->set_else(m.mk_app(G, vI0, vB1)); + fi->set_else(m.mk_app(F, vI0p, vB1p)); + gi->set_else(m.mk_app(G, vI0p, vB1p)); mdl.register_decl(g, gi); mdl.register_decl(h, hi); model_pp(std::cout, mdl); - e = m.mk_app(h, vI0, vB1); + e = m.mk_app(h, vI0p, vB1p); eval(e, v); std::cout << e << " " << v << "\n"; } From 49d0e2862166ac6ae588c57e8c9005e4e96193f1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Mar 2016 10:44:06 -0800 Subject: [PATCH 2/4] allow parameters to overwrite logic, fixes bug report by Nuno Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/smt_tactic.cpp | 11 +++++------ src/solver/tactic2solver.cpp | 2 +- src/util/mpn.cpp | 8 ++++++-- 3 files changed, 12 insertions(+), 9 deletions(-) diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index afa4cf98f..28300e569 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -99,7 +99,7 @@ public: m_ctx(0), m_callback(0) { updt_params_core(p); - TRACE("smt_tactic", tout << this << "\np: " << p << "\n";); + TRACE("smt_tactic", tout << "p: " << p << "\n";); } virtual tactic * translate(ast_manager & m) { @@ -120,13 +120,12 @@ public: } virtual void updt_params(params_ref const & p) { - TRACE("smt_tactic", tout << this << "\nupdt_params: " << p << "\n";); + TRACE("smt_tactic", tout << "updt_params: " << p << "\n";); updt_params_core(p); fparams().updt_params(p); - symbol logic = p.get_sym(symbol("logic"), symbol::null); - if (logic != symbol::null) { - if (m_ctx) m_ctx->set_logic(logic); - m_logic = logic; + m_logic = p.get_sym(symbol("logic"), m_logic); + if (m_logic != symbol::null && m_ctx) { + m_ctx->set_logic(m_logic); } SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config); } diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index f661ca184..5235be230 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -128,8 +128,8 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass ast_manager & m = m_assertions.m(); m_result = alloc(simple_check_sat_result, m); m_tactic->cleanup(); - m_tactic->updt_params(m_params); m_tactic->set_logic(m_logic); + m_tactic->updt_params(m_params); // parameters are allowed to overwrite logic. goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores); unsigned sz = m_assertions.size(); diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 610eee564..0c1744a09 100644 --- a/src/util/mpn.cpp +++ b/src/util/mpn.cpp @@ -226,7 +226,7 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum, mpn_sbuffer & n_denom) const { size_t d = 0; - while (((denom[lden-1] << d) & MASK_FIRST) == 0) d++; + while (lden > 0 && ((denom[lden-1] << d) & MASK_FIRST) == 0) d++; SASSERT(d < DIGIT_BITS); n_numer.resize(lnum+1); @@ -239,7 +239,8 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum, for (size_t i = 0; i < lden; i++) n_denom[i] = denom[i]; } - else { + else if (lnum != 0) { + SASSERT(lden > 0); mpn_digit q = FIRST_BITS(d, numer[lnum-1]); n_numer[lnum] = q; for (size_t i = lnum-1; i > 0; i--) @@ -249,6 +250,9 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum, n_denom[i] = denom[i] << d | FIRST_BITS(d, denom[i-1]); n_denom[0] = denom[0] << d; } + else { + d = 0; + } TRACE("mpn_norm", tout << "Normalized: n_numer="; display_raw(tout, n_numer.c_ptr(), n_numer.size()); tout << " n_denom="; display_raw(tout, n_denom.c_ptr(), n_denom.size()); tout << std::endl; ); From 589227235e415b6e1d2dd7f79f3912ad634ed599 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 7 Mar 2016 18:41:39 +0000 Subject: [PATCH 3/4] Try to improve some of the comments in ``scripts/update_api.py`` based on discussion in #461. --- scripts/update_api.py | 59 ++++++++++++++++++++++++++++++++----------- 1 file changed, 44 insertions(+), 15 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index d5cc92a7f..7603817eb 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1565,14 +1565,27 @@ def generate_files(api_files, java_package_name=None, ml_output_dir=None): """ - Scan the api files in ``api_files`` and emit - the relevant ``api_*.h`` and ``api_*.cpp`` files - for the api modules into the ``api_output_dir`` - directory. + Scan the api files in ``api_files`` and emit the relevant API files into + the output directories specified. If an output directory is set to ``None`` + then the files for that language binding or module are not emitted. - For the remaining arguments, if said argument is - not ``None`` the relevant files for that language - binding will be emitted to the specified directory. + The reason for this function interface is: + + * The CMake build system needs to control where + files are emitted. + * The CMake build system needs to be able to choose + which API files are emitted. + * This function should be as decoupled from the Python + build system as much as possible but it must be possible + for the Python build system code to use this function. + + Therefore we: + + * Do not use the ``mk_util.is_*_enabled()`` functions + to determine if certain files should be or should not be emitted. + + * Do not use the components declared in the Python build system + to determine the output directory paths. """ # FIXME: These should not be global global log_h, log_c, exe_c, core_py @@ -1629,16 +1642,32 @@ def generate_files(api_files, def main(args): logging.basicConfig(level=logging.INFO) parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("api_files", nargs="+", + parser.add_argument("api_files", + nargs="+", help="API header files to generate files from") parser.add_argument("--api_output_dir", - help="Directory to emit files for api module", - default=None) - parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) - parser.add_argument("--dotnet-output-dir", dest="dotnet_output_dir", default=None) - parser.add_argument("--java-output-dir", dest="java_output_dir", default=None) - parser.add_argument("--java-package-name", dest="java_package_name", default=None) - parser.add_argument("--ml-output-dir", dest="ml_output_dir", default=None) + default=None, + help="Directory to emit files for api module. If not specified no files are emitted.") + parser.add_argument("--z3py-output-dir", + dest="z3py_output_dir", + default=None, + help="Directory to emit z3py files. If not specified no files are emitted.") + parser.add_argument("--dotnet-output-dir", + dest="dotnet_output_dir", + default=None, + help="Directory to emit dotnet files. If not specified no files are emitted.") + parser.add_argument("--java-output-dir", + dest="java_output_dir", + default=None, + help="Directory to emit Java files. If not specified no files are emitted.") + parser.add_argument("--java-package-name", + dest="java_package_name", + default=None, + help="Name to give the Java package (e.g. ``com.microsoft.z3``).") + parser.add_argument("--ml-output-dir", + dest="ml_output_dir", + default=None, + help="Directory to emit OCaml files. If not specified no files are emitted.") pargs = parser.parse_args(args) if pargs.java_output_dir: From 5994c5a94899d732ec834888d6ccee77ef436571 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Mar 2016 16:42:29 -0800 Subject: [PATCH 4/4] fix partial model tracking over cancellation/exceptions, reported by August Shi. Fix regression test for fp-to-real, reset the pre-processor in inc_sat_solver on exceptions Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 1 + src/opt/bcd2.cpp | 3 +- src/opt/fu_malik.cpp | 2 +- src/opt/maxhs.cpp | 3 +- src/opt/maxres.cpp | 38 ++++++---- src/opt/maxres.h | 4 +- src/opt/maxsmt.cpp | 34 ++++++--- src/opt/maxsmt.h | 7 +- src/opt/mss.cpp | 11 ++- src/opt/opt_context.cpp | 80 ++++++++++++++------- src/opt/opt_context.h | 14 ++-- src/opt/optsmt.cpp | 3 +- src/opt/pb_sls.cpp | 10 +-- src/sat/sat_mus.cpp | 4 +- src/sat/sat_solver/inc_sat_solver.cpp | 91 ++++++++++++++---------- src/smt/theory_bv.cpp | 52 +++++++------- src/tactic/arith/lia2pb_tactic.cpp | 3 +- src/tactic/extension_model_converter.cpp | 62 ++++++---------- src/tactic/extension_model_converter.h | 10 +-- 19 files changed, 239 insertions(+), 193 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 24c19a27a..8f1718141 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1454,6 +1454,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions throw ex; } catch (z3_exception & ex) { + get_opt()->display_assignment(regular_stream()); throw cmd_exception(ex.msg()); } if (was_pareto && r == l_false) { diff --git a/src/opt/bcd2.cpp b/src/opt/bcd2.cpp index 50c3f7e51..a373b652b 100644 --- a/src/opt/bcd2.cpp +++ b/src/opt/bcd2.cpp @@ -233,8 +233,7 @@ namespace opt { new_assignment.reset(); s().get_model(model); for (unsigned i = 0; i < m_soft.size(); ++i) { - VERIFY(model->eval(m_soft[i], val)); - new_assignment.push_back(m.is_true(val)); + new_assignment.push_back(model->eval(m_soft[i], val) && m.is_true(val)); if (!new_assignment[i]) { new_upper += m_weights[i]; } diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 7a3f685e6..48ef50cbc 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -204,7 +204,7 @@ namespace opt { m_assignment.reset(); for (unsigned i = 0; i < m_soft.size(); ++i) { expr_ref val(m); - VERIFY(m_model->eval(m_soft[i], val)); + if (!m_model->eval(m_soft[i], val)) return l_undef; TRACE("opt", tout << val << "\n";); m_assignment.push_back(m.is_true(val)); } diff --git a/src/opt/maxhs.cpp b/src/opt/maxhs.cpp index 0e16af30e..2297bdc20 100644 --- a/src/opt/maxhs.cpp +++ b/src/opt/maxhs.cpp @@ -530,8 +530,7 @@ namespace opt { bool is_true(model_ref& mdl, expr* e) { expr_ref val(m); - VERIFY(mdl->eval(e, val)); - return m.is_true(val); + return mdl->eval(e, val) && m.is_true(val); } bool is_active(unsigned i) const { diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 204276835..7c1fad80e 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -82,6 +82,7 @@ private: memset(this, 0, sizeof(*this)); } }; + unsigned m_index; stats m_stats; expr_ref_vector m_B; expr_ref_vector m_asms; @@ -112,10 +113,11 @@ private: typedef ptr_vector exprs; public: - maxres(maxsat_context& c, + maxres(maxsat_context& c, unsigned index, weights_t& ws, expr_ref_vector const& soft, strategy_t st): maxsmt_solver_base(c, ws, soft), + m_index(index), m_B(m), m_asms(m), m_defs(m), m_mus(c.get_solver(), m), m_mss(c.get_solver(), m), @@ -189,7 +191,7 @@ public: lbool mus_solver() { lbool is_sat = l_true; - init(); + if (!init()) return l_undef; init_local(); trace(); while (m_lower < m_upper) { @@ -227,7 +229,7 @@ public: } lbool primal_dual_solver() { - init(); + if (!init()) return l_undef; init_local(); trace(); exprs cs; @@ -483,8 +485,9 @@ public: if (m_csmodel) { expr_ref val(m); SASSERT(m_csmodel.get()); - VERIFY(m_csmodel->eval(value, val)); - m_csmodel->register_decl(to_app(def)->get_decl(), val); + if (m_csmodel->eval(value, val, true)) { + m_csmodel->register_decl(to_app(def)->get_decl(), val); + } } } @@ -724,17 +727,26 @@ public: if (upper >= m_upper) { return; } + + if (!m_c.verify_model(m_index, mdl, upper)) { + return; + } + m_model = mdl; - + for (unsigned i = 0; i < m_soft.size(); ++i) { m_assignment[i] = is_true(m_soft[i]); } + + + DEBUG_CODE(verify_assignment();); m_upper = upper; trace(); add_upper_bound_block(); + } void add_upper_bound_block() { @@ -751,14 +763,12 @@ public: bool is_true(model* mdl, expr* e) { expr_ref tmp(m); - VERIFY(mdl->eval(e, tmp)); - return m.is_true(tmp); + return mdl->eval(e, tmp, true) && m.is_true(tmp); } bool is_false(model* mdl, expr* e) { expr_ref tmp(m); - VERIFY(mdl->eval(e, tmp)); - return m.is_false(tmp); + return mdl->eval(e, tmp, true) && m.is_false(tmp); } bool is_true(expr* e) { @@ -870,12 +880,12 @@ public: }; opt::maxsmt_solver_base* opt::mk_maxres( - maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) { - return alloc(maxres, c, ws, soft, maxres::s_primal); + maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) { + return alloc(maxres, c, id, ws, soft, maxres::s_primal); } opt::maxsmt_solver_base* opt::mk_primal_dual_maxres( - maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) { - return alloc(maxres, c, ws, soft, maxres::s_primal_dual); + maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) { + return alloc(maxres, c, id, ws, soft, maxres::s_primal_dual); } diff --git a/src/opt/maxres.h b/src/opt/maxres.h index d8682d4d9..f1b125e37 100644 --- a/src/opt/maxres.h +++ b/src/opt/maxres.h @@ -22,9 +22,9 @@ Notes: namespace opt { - maxsmt_solver_base* mk_maxres(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft); + maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft); - maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft); + maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft); }; diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 8f3de6693..5229fafab 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -69,13 +69,13 @@ namespace opt { s().assert_expr(tmp); } - void maxsmt_solver_base::init() { + bool maxsmt_solver_base::init() { m_lower.reset(); m_upper.reset(); m_assignment.reset(); for (unsigned i = 0; i < m_weights.size(); ++i) { expr_ref val(m); - VERIFY(m_model->eval(m_soft[i], val)); + if (!m_model->eval(m_soft[i], val)) return false; m_assignment.push_back(m.is_true(val)); if (!m_assignment.back()) { m_upper += m_weights[i]; @@ -88,6 +88,7 @@ namespace opt { tout << (m_assignment[i]?"T":"F"); } tout << "\n";); + return true; } void maxsmt_solver_base::set_mus(bool f) { @@ -137,7 +138,8 @@ namespace opt { //m_wth->reset_local(); } smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; } - + + void maxsmt_solver_base::trace_bounds(char const * solver) { IF_VERBOSE(1, rational l = m_adjust_value(m_lower); @@ -148,8 +150,8 @@ namespace opt { - maxsmt::maxsmt(maxsat_context& c): - m(c.get_manager()), m_c(c), + maxsmt::maxsmt(maxsat_context& c, unsigned index): + m(c.get_manager()), m_c(c), m_index(index), m_soft_constraints(m), m_answer(m) {} lbool maxsmt::operator()() { @@ -159,10 +161,10 @@ namespace opt { IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); TRACE("opt", tout << "maxsmt\n";); if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres")) { - m_msolver = mk_maxres(m_c, m_weights, m_soft_constraints); + m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints); } else if (maxsat_engine == symbol("pd-maxres")) { - m_msolver = mk_primal_dual_maxres(m_c, m_weights, m_soft_constraints); + m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints); } else if (maxsat_engine == symbol("bcd2")) { m_msolver = mk_bcd2(m_c, m_weights, m_soft_constraints); @@ -188,7 +190,13 @@ namespace opt { if (m_msolver) { m_msolver->updt_params(m_params); m_msolver->set_adjust_value(m_adjust_value); - is_sat = (*m_msolver)(); + is_sat = l_undef; + try { + is_sat = (*m_msolver)(); + } + catch (z3_exception&) { + is_sat = l_undef; + } if (is_sat != l_false) { m_msolver->get_model(m_model, m_labels); } @@ -205,6 +213,14 @@ namespace opt { return is_sat; } + void maxsmt::set_adjust_value(adjust_value& adj) { + m_adjust_value = adj; + if (m_msolver) { + m_msolver->set_adjust_value(m_adjust_value); + } + } + + void maxsmt::verify_assignment() { // TBD: have to use a different solver // because we don't push local scope any longer. @@ -233,7 +249,7 @@ namespace opt { rational r = m_upper; if (m_msolver) { rational q = m_msolver->get_upper(); - if (q < r) r = q; + if (q < r) r = q; } return m_adjust_value(r); } diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 0e1e75a84..57fe12b59 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -82,7 +82,7 @@ namespace opt { void set_model() { s().get_model(m_model); s().get_labels(m_labels); } virtual void updt_params(params_ref& p); solver& s(); - void init(); + bool init(); void set_mus(bool f); app* mk_fresh_bool(char const* name); @@ -111,6 +111,7 @@ namespace opt { class maxsmt { ast_manager& m; maxsat_context& m_c; + unsigned m_index; scoped_ptr m_msolver; expr_ref_vector m_soft_constraints; expr_ref_vector m_answer; @@ -122,11 +123,11 @@ namespace opt { svector m_labels; params_ref m_params; public: - maxsmt(maxsat_context& c); + maxsmt(maxsat_context& c, unsigned id); lbool operator()(); void updt_params(params_ref& p); void add(expr* f, rational const& w); - void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; } + void set_adjust_value(adjust_value& adj); unsigned size() const { return m_soft_constraints.size(); } expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; } rational weight(unsigned idx) const { return m_weights[idx]; } diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp index 8c3a70e9e..863834b85 100644 --- a/src/opt/mss.cpp +++ b/src/opt/mss.cpp @@ -73,8 +73,7 @@ namespace opt { expr* n = core[j]; if (!core_lits.contains(n)) { core_lits.insert(n); - VERIFY(m_model->eval(n, tmp)); - if (m.is_true(tmp)) { + if (m_model->eval(n, tmp) && m.is_true(tmp)) { add_mss(n); } else { @@ -86,8 +85,7 @@ namespace opt { for (unsigned i = 0; i < literals.size(); ++i) { expr* n = literals[i]; if (!core_lits.contains(n)) { - VERIFY(m_model->eval(n, tmp)); - if (m.is_true(tmp)) { + if (m_model->eval(n, tmp) && m.is_true(tmp)) { m_mss.push_back(n); } else { @@ -130,8 +128,7 @@ namespace opt { if (m_mcs.contains(n)) { continue; // remove from cores. } - VERIFY(m_model->eval(n, tmp)); - if (m.is_true(tmp)) { + if (m_model->eval(n, tmp) && m.is_true(tmp)) { add_mss(n); } else { @@ -275,7 +272,7 @@ namespace opt { expr_ref tmp(m); for (unsigned i = 0; i < m_mss.size(); ++i) { expr* n = m_mss[i]; - VERIFY(m_model->eval(n, tmp)); + if (!m_model->eval(n, tmp)) return true; CTRACE("opt", !m.is_true(tmp), tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";); SASSERT(!m.is_false(tmp)); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 3c305723b..307dbfda4 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -203,7 +203,7 @@ namespace opt { objective& obj = s.m_objectives[i]; m_objectives.push_back(obj); if (obj.m_type == O_MAXSMT) { - add_maxsmt(obj.m_id); + add_maxsmt(obj.m_id, i); } } m_hard_constraints.append(s.m_hard); @@ -311,7 +311,9 @@ namespace opt { maxsmt& ms = *m_maxsmts.find(id); if (scoped) get_solver().push(); lbool result = ms(); - if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) ms.get_model(m_model, m_labels); + 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; @@ -414,12 +416,16 @@ namespace opt { case O_MINIMIZE: is_ge = !is_ge; case O_MAXIMIZE: - VERIFY(mdl->eval(obj.m_term, val) && is_numeral(val, k)); - if (is_ge) { - result = mk_ge(obj.m_term, val); + if (mdl->eval(obj.m_term, val) && is_numeral(val, k)) { + if (is_ge) { + result = mk_ge(obj.m_term, val); + } + else { + result = mk_ge(val, obj.m_term); + } } else { - result = mk_ge(val, obj.m_term); + result = m.mk_true(); } break; case O_MAXSMT: { @@ -430,8 +436,7 @@ namespace opt { for (unsigned i = 0; i < sz; ++i) { terms.push_back(obj.m_terms[i]); coeffs.push_back(obj.m_weights[i]); - VERIFY(mdl->eval(obj.m_terms[i], val)); - if (m.is_true(val)) { + if (mdl->eval(obj.m_terms[i], val) && m.is_true(val)) { k += obj.m_weights[i]; } } @@ -469,8 +474,7 @@ namespace opt { update_bound(false); } - lbool context::execute_pareto() { - + lbool context::execute_pareto() { if (!m_pareto) { set_pareto(alloc(gia_pareto, m, *this, m_solver.get(), m_params)); } @@ -642,8 +646,8 @@ namespace opt { } - void context::add_maxsmt(symbol const& id) { - maxsmt* ms = alloc(maxsmt, *this); + void context::add_maxsmt(symbol const& id, unsigned index) { + maxsmt* ms = alloc(maxsmt, *this, index); ms->updt_params(m_params); #pragma omp critical (opt_context) { @@ -708,7 +712,7 @@ namespace opt { } } - bool context::is_maximize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index) { + bool context::is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index) { if (is_app(fml) && m_objective_fns.find(to_app(fml)->get_decl(), index) && m_objectives[index].m_type == O_MAXIMIZE) { term = to_app(to_app(fml)->get_arg(0)); @@ -718,7 +722,7 @@ namespace opt { return false; } - bool context::is_minimize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index) { + bool context::is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index) { if (is_app(fml) && m_objective_fns.find(to_app(fml)->get_decl(), index) && m_objectives[index].m_type == O_MINIMIZE) { term = to_app(to_app(fml)->get_arg(0)); @@ -730,7 +734,7 @@ namespace opt { bool context::is_maxsat(expr* fml, expr_ref_vector& terms, vector& weights, rational& offset, - bool& neg, symbol& id, unsigned& index) { + bool& neg, symbol& id, expr_ref& orig_term, unsigned& index) { if (!is_app(fml)) return false; neg = false; app* a = to_app(fml); @@ -752,7 +756,6 @@ namespace opt { return true; } app_ref term(m); - expr* orig_term; offset = rational::zero(); bool is_max = is_maximize(fml, term, orig_term, index); bool is_min = !is_max && is_minimize(fml, term, orig_term, index); @@ -773,7 +776,7 @@ namespace opt { } } TRACE("opt", - tout << "Convert minimization " << mk_pp(orig_term, m) << "\n"; + tout << "Convert minimization " << orig_term << "\n"; tout << "to maxsat: " << term << "\n"; for (unsigned i = 0; i < weights.size(); ++i) { tout << mk_pp(terms[i].get(), m) << ": " << weights[i] << "\n"; @@ -781,7 +784,7 @@ namespace opt { tout << "offset: " << offset << "\n"; ); std::ostringstream out; - out << mk_pp(orig_term, m) << ":" << index; + out << orig_term << ":" << index; id = symbol(out.str().c_str()); return true; } @@ -804,7 +807,7 @@ namespace opt { } neg = true; std::ostringstream out; - out << mk_pp(orig_term, m) << ":" << index; + out << orig_term << ":" << index; id = symbol(out.str().c_str()); return true; } @@ -823,7 +826,7 @@ namespace opt { } neg = is_max; std::ostringstream out; - out << mk_pp(orig_term, m) << ":" << index; + out << orig_term << ":" << index; id = symbol(out.str().c_str()); return true; } @@ -871,7 +874,7 @@ namespace opt { tout << mk_pp(fmls[i], m) << "\n"; }); m_hard_constraints.reset(); - expr* orig_term; + expr_ref orig_term(m); for (unsigned i = 0; i < fmls.size(); ++i) { expr* fml = fmls[i]; app_ref tr(m); @@ -881,7 +884,7 @@ namespace opt { unsigned index; symbol id; bool neg; - if (is_maxsat(fml, terms, weights, offset, neg, id, index)) { + if (is_maxsat(fml, terms, weights, offset, neg, id, orig_term, index)) { objective& obj = m_objectives[index]; if (obj.m_type != O_MAXSMT) { @@ -889,10 +892,11 @@ namespace opt { obj.m_id = id; obj.m_type = O_MAXSMT; SASSERT(!m_maxsmts.contains(id)); - add_maxsmt(id); + add_maxsmt(id, index); } mk_atomic(terms); SASSERT(obj.m_id == id); + obj.m_term = to_app(orig_term); obj.m_terms.reset(); obj.m_terms.append(terms); obj.m_weights.reset(); @@ -933,6 +937,32 @@ namespace opt { } } + bool context::verify_model(unsigned index, model* md, rational const& _v) { + rational r; + app_ref term = m_objectives[index].m_term; + rational v = m_objectives[index].m_adjust_value(_v); + expr_ref val(m); + model_ref mdl = md; + fix_model(mdl); + + if (!mdl->eval(term, val)) { + TRACE("opt", tout << "Term does not evaluate " << term << "\n";); + return false; + } + if (!m_arith.is_numeral(val, r)) { + TRACE("opt", tout << "model does not evaluate objective to a value\n";); + return false; + } + if (r != v) { + TRACE("opt", tout << "Out of bounds: " << term << " " << val << " != " << v << "\n";); + return false; + } + else { + TRACE("opt", tout << "validated: " << term << " = " << val << "\n";); + } + return true; + } + void context::purify(app_ref& term) { filter_model_converter_ref fm; if (m_arith.is_add(term)) { @@ -1395,8 +1425,8 @@ namespace opt { case O_MAXSMT: { rational value(0); for (unsigned i = 0; i < obj.m_terms.size(); ++i) { - VERIFY(m_model->eval(obj.m_terms[i], val)); - if (!m.is_true(val)) { + bool evaluated = m_model->eval(obj.m_terms[i], val); + if (evaluated && !m.is_true(val)) { value += obj.m_weights[i]; } // TBD: check that optimal was not changed. diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 24051f7cb..5ddd3be99 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -55,6 +55,8 @@ namespace opt { virtual void get_base_model(model_ref& _m) = 0; // retrieve model from initial satisfiability call. virtual smt::context& smt_context() = 0; // access SMT context for SMT based MaxSMT solver (wmax requires SMT core) virtual unsigned num_objectives() = 0; + virtual bool verify_model(unsigned id, model* mdl, rational const& v) = 0; + virtual void set_model(model_ref& _m) = 0; }; /** @@ -132,6 +134,7 @@ namespace opt { bool set(ptr_vector & hard); unsigned add(expr* soft, rational const& weight, symbol const& id); unsigned add(app* obj, bool is_max); + unsigned get_index(symbol const& id) { return m_indices[id]; } }; ast_manager& m; @@ -178,6 +181,7 @@ namespace opt { virtual void set_hard_constraints(ptr_vector & hard); virtual lbool optimize(); virtual bool print_model() const; + virtual void set_model(model_ref& _m) { m_model = _m; } virtual void get_model(model_ref& _m); virtual void fix_model(model_ref& _m); virtual void collect_statistics(statistics& stats) const; @@ -219,6 +223,8 @@ namespace opt { virtual void get_base_model(model_ref& _m); + virtual bool verify_model(unsigned id, model* mdl, rational const& v); + private: void validate_feasibility(maxsmt& ms); @@ -236,11 +242,11 @@ namespace opt { void import_scoped_state(); void normalize(); void internalize(); - bool is_maximize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index); - bool is_minimize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index); + bool is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index); + bool is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index); bool is_maxsat(expr* fml, expr_ref_vector& terms, vector& weights, rational& offset, bool& neg, - symbol& id, unsigned& index); + symbol& id, expr_ref& orig_term, unsigned& index); void purify(app_ref& term); app* purify(filter_model_converter_ref& fm, expr* e); bool is_mul_const(expr* e); @@ -269,7 +275,7 @@ namespace opt { void init_solver(); void update_solver(); void setup_arith_solver(); - void add_maxsmt(symbol const& id); + void add_maxsmt(symbol const& id, unsigned index); void set_simplify(tactic *simplify); void set_pareto(pareto_base* p); void clear_state(); diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index b692cb18c..e92ab4f97 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -156,8 +156,7 @@ namespace opt { 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); - if (m.is_true(tmp)) { + if (m_model->eval(ors[i].get(), tmp) && m.is_true(tmp)) { m_lower[i] = m_upper[i]; ors[i] = m.mk_false(); disj[i] = m.mk_false(); diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index 098af68ee..95b489394 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -139,8 +139,7 @@ namespace smt { m_orig_model = mdl; for (unsigned i = 0; i < m_var2decl.size(); ++i) { expr_ref tmp(m); - VERIFY(mdl->eval(m_var2decl[i], tmp)); - m_assignment[i] = m.is_true(tmp); + m_assignment[i] = mdl->eval(m_var2decl[i], tmp) && m.is_true(tmp); } } @@ -305,7 +304,9 @@ namespace smt { if (!eval(m_clauses[i])) { m_hard_false.insert(i); expr_ref tmp(m); - VERIFY(m_orig_model->eval(m_orig_clauses[i].get(), tmp)); + if (!m_orig_model->eval(m_orig_clauses[i].get(), tmp)) { + return; + } IF_VERBOSE(0, verbose_stream() << "original evaluation: " << tmp << "\n"; verbose_stream() << mk_pp(m_orig_clauses[i].get(), m) << "\n"; @@ -487,8 +488,7 @@ namespace smt { SASSERT(m_soft_occ.size() == var); m_hard_occ.push_back(unsigned_vector()); m_soft_occ.push_back(unsigned_vector()); - VERIFY(m_orig_model->eval(f, tmp)); - m_assignment.push_back(m.is_true(tmp)); + m_assignment.push_back(m_orig_model->eval(f, tmp) && m.is_true(tmp)); m_decl2var.insert(f, var); m_var2decl.push_back(f); } diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index b5abc7544..9c7c8c7bb 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -97,7 +97,7 @@ namespace sat { break; } if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { - IF_VERBOSE(1, verbose_stream() << "restart budget exceeded\n";); + IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";); set_core(); return l_true; } @@ -173,7 +173,7 @@ namespace sat { lbool mus::qx(literal_set& assignment, literal_set& support, bool has_support) { lbool is_sat = l_true; if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { - IF_VERBOSE(1, verbose_stream() << "restart budget exceeded\n";); + IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";); return l_true; } if (has_support) { diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 7feed9fb1..c80ab29ac 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -50,14 +50,14 @@ class inc_sat_solver : public solver { expr_ref_vector m_core; atom2bool_var m_map; model_ref m_model; - model_converter_ref m_mc; - bit_blaster_rewriter m_bb_rewriter; + scoped_ptr m_bb_rewriter; tactic_ref m_preprocess; unsigned m_num_scopes; sat::literal_vector m_asms; goal_ref_buffer m_subgoals; proof_converter_ref m_pc; - model_converter_ref m_mc2; + model_converter_ref m_mc; + model_converter_ref m_mc0; expr_dependency_ref m_dep_core; svector m_weights; std::string m_unknown; @@ -72,29 +72,13 @@ public: m_asmsf(m), m_fmls_head(0), m_core(m), - m_map(m), - m_bb_rewriter(m, p), + m_map(m), m_num_scopes(0), m_dep_core(m), m_unknown("no reason given") { m_params.set_bool("elim_vars", false); m_solver.updt_params(m_params); - params_ref simp2_p = p; - simp2_p.set_bool("som", true); - simp2_p.set_bool("pull_cheap_ite", true); - simp2_p.set_bool("push_ite_bv", false); - simp2_p.set_bool("local_ctx", true); - simp2_p.set_uint("local_ctx_limit", 10000000); - simp2_p.set_bool("flat", true); // required by som - simp2_p.set_bool("hoist_mul", false); // required by som - simp2_p.set_bool("elim_and", true); - m_preprocess = - and_then(mk_card2bv_tactic(m, m_params), - using_params(mk_simplify_tactic(m), simp2_p), - mk_max_bv_sharing_tactic(m), - mk_bit_blaster_tactic(m, &m_bb_rewriter), - //mk_aig_tactic(), - using_params(mk_simplify_tactic(m), simp2_p)); + init_preprocess(); } virtual ~inc_sat_solver() {} @@ -179,14 +163,14 @@ public: m_fmls_lim.push_back(m_fmls.size()); m_asms_lim.push_back(m_asmsf.size()); m_fmls_head_lim.push_back(m_fmls_head); - m_bb_rewriter.push(); + m_bb_rewriter->push(); m_map.push(); } virtual void pop(unsigned n) { if (n > m_num_scopes) { // allow inc_sat_solver to n = m_num_scopes; // take over for another solver. } - m_bb_rewriter.pop(n); + m_bb_rewriter->pop(n); m_map.pop(n); SASSERT(n <= m_num_scopes); m_solver.user_pop(n); @@ -269,30 +253,58 @@ public: return m_asmsf[idx]; } + void init_preprocess() { + if (m_preprocess) { + m_preprocess->reset(); + } + params_ref simp2_p = m_params; + m_bb_rewriter = alloc(bit_blaster_rewriter, m, m_params); + simp2_p.set_bool("som", true); + simp2_p.set_bool("pull_cheap_ite", true); + simp2_p.set_bool("push_ite_bv", false); + simp2_p.set_bool("local_ctx", true); + simp2_p.set_uint("local_ctx_limit", 10000000); + simp2_p.set_bool("flat", true); // required by som + simp2_p.set_bool("hoist_mul", false); // required by som + simp2_p.set_bool("elim_and", true); + m_preprocess = + and_then(mk_card2bv_tactic(m, m_params), + using_params(mk_simplify_tactic(m), simp2_p), + mk_max_bv_sharing_tactic(m), + mk_bit_blaster_tactic(m, m_bb_rewriter.get()), + //mk_aig_tactic(), + using_params(mk_simplify_tactic(m), simp2_p)); + for (unsigned i = 0; i < m_num_scopes; ++i) { + m_bb_rewriter->push(); + } + m_preprocess->reset(); + } + private: lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm) { - m_mc2.reset(); + m_mc.reset(); m_pc.reset(); m_dep_core.reset(); m_subgoals.reset(); - m_preprocess->reset(); + init_preprocess(); SASSERT(g->models_enabled()); SASSERT(!g->proofs_enabled()); TRACE("sat", g->display(tout);); try { - (*m_preprocess)(g, m_subgoals, m_mc2, m_pc, m_dep_core); + (*m_preprocess)(g, m_subgoals, m_mc, m_pc, m_dep_core); } catch (tactic_exception & ex) { IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";); + m_preprocess = 0; + m_bb_rewriter = 0; return l_undef; } if (m_subgoals.size() != 1) { IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n";); return l_undef; } - CTRACE("sat", m_mc.get(), m_mc->display(tout); ); g = m_subgoals[0]; TRACE("sat", g->display_with_dependencies(tout);); m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true); @@ -416,24 +428,25 @@ private: } } m_model = md; - if (m_mc || !m_bb_rewriter.const2bits().empty()) { - model_converter_ref mc = m_mc; - if (!m_bb_rewriter.const2bits().empty()) { - mc = concat(mc.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter.const2bits())); - } - (*mc)(m_model); + + if (!m_bb_rewriter->const2bits().empty()) { + m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits())); + } + if (m_mc0) { + (*m_mc0)(m_model); } SASSERT(m_model); DEBUG_CODE( for (unsigned i = 0; i < m_fmls.size(); ++i) { expr_ref tmp(m); - VERIFY(m_model->eval(m_fmls[i].get(), tmp, true)); - CTRACE("sat", !m.is_true(tmp), - tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m) - << " to " << tmp << "\n"; - model_smt2_pp(tout, m, *(m_model.get()), 0);); - SASSERT(m.is_true(tmp)); + if (m_model->eval(m_fmls[i].get(), tmp, true)) { + CTRACE("sat", !m.is_true(tmp), + tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m) + << " to " << tmp << "\n"; + model_smt2_pp(tout, m, *(m_model.get()), 0);); + SASSERT(m.is_true(tmp)); + } }); } }; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 94566c52b..3d6e341fa 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -95,10 +95,9 @@ namespace smt { enode * first_arg_enode = ctx.get_enode(first_arg); get_var(first_arg_enode); // numerals are not blasted into bit2bool, so we do this directly. - if (!ctx.b_internalized(n)) { - rational val; - unsigned sz; - VERIFY(m_util.is_numeral(first_arg, val, sz)); + rational val; + unsigned sz; + if (!ctx.b_internalized(n) && m_util.is_numeral(first_arg, val, sz)) { theory_var v = first_arg_enode->get_th_var(get_id()); app* owner = first_arg_enode->get_owner(); for (unsigned i = 0; i < sz; ++i) { @@ -113,29 +112,28 @@ namespace smt { } } } - else { - enode * arg = ctx.get_enode(first_arg); - // The argument was already internalized, but it may not have a theory variable associated with it. - // For example, for ite-terms the method apply_sort_cnstr is not invoked. - // See comment in the then-branch. - theory_var v_arg = arg->get_th_var(get_id()); - if (v_arg == null_theory_var) { - // The method get_var will create a theory variable for arg. - // As a side-effect the bits for arg will also be created. - get_var(arg); - SASSERT(ctx.b_internalized(n)); - } - else { - SASSERT(v_arg != null_theory_var); - bool_var bv = ctx.mk_bool_var(n); - ctx.set_var_theory(bv, get_id()); - bit_atom * a = new (get_region()) bit_atom(); - insert_bv2a(bv, a); - m_trail_stack.push(mk_atom_trail(bv)); - unsigned idx = n->get_decl()->get_parameter(0).get_int(); - SASSERT(a->m_occs == 0); - a->m_occs = new (get_region()) var_pos_occ(v_arg, idx); - } + + enode * arg = ctx.get_enode(first_arg); + // The argument was already internalized, but it may not have a theory variable associated with it. + // For example, for ite-terms the method apply_sort_cnstr is not invoked. + // See comment in the then-branch. + theory_var v_arg = arg->get_th_var(get_id()); + if (v_arg == null_theory_var) { + // The method get_var will create a theory variable for arg. + // As a side-effect the bits for arg will also be created. + get_var(arg); + SASSERT(ctx.b_internalized(n)); + } + else if (!ctx.b_internalized(n)) { + SASSERT(v_arg != null_theory_var); + bool_var bv = ctx.mk_bool_var(n); + ctx.set_var_theory(bv, get_id()); + bit_atom * a = new (get_region()) bit_atom(); + insert_bv2a(bv, a); + m_trail_stack.push(mk_atom_trail(bv)); + unsigned idx = n->get_decl()->get_parameter(0).get_int(); + SASSERT(a->m_occs == 0); + a->m_occs = new (get_region()) var_pos_occ(v_arg, idx); } } diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 1ad662218..8d637bada 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -272,8 +272,9 @@ class lia2pb_tactic : public tactic { } TRACE("lia2pb", tout << mk_ismt2_pp(x, m) << " -> " << dep << "\n";); subst.insert(x, def, 0, dep); - if (m_produce_models) + if (m_produce_models) { mc1->insert(to_app(x)->get_decl(), def); + } } } diff --git a/src/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp index 0f40578a2..89c1bb4f5 100644 --- a/src/tactic/extension_model_converter.cpp +++ b/src/tactic/extension_model_converter.cpp @@ -25,25 +25,6 @@ Notes: extension_model_converter::~extension_model_converter() { } -struct extension_model_converter::set_eval { - extension_model_converter * m_owner; - model_evaluator * m_old; - set_eval(extension_model_converter * owner, model_evaluator * ev) { - m_owner = owner; - m_old = owner->m_eval; - #pragma omp critical (extension_model_converter) - { - owner->m_eval = ev; - } - } - ~set_eval() { - #pragma omp critical (extension_model_converter) - { - m_owner->m_eval = m_old; - } - } - -}; static void display_decls_info(std::ostream & out, model_ref & md) { ast_manager & m = md->get_manager(); @@ -68,36 +49,38 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { model_evaluator ev(*(md.get())); ev.set_model_completion(true); expr_ref val(m()); - { - set_eval setter(this, &ev); - unsigned i = m_vars.size(); - while (i > 0) { - --i; - expr * def = m_defs.get(i); - ev(def, val); - TRACE("extension_mc", tout << m_vars.get(i)->get_name() << " ->\n" << mk_ismt2_pp(def, m()) << "\n==>\n" << mk_ismt2_pp(val, m()) << "\n";); - func_decl * f = m_vars.get(i); - unsigned arity = f->get_arity(); - if (arity == 0) { - md->register_decl(f, val); - } - else { - func_interp * new_fi = alloc(func_interp, m(), arity); - new_fi->set_else(val); - md->register_decl(f, new_fi); - } + unsigned i = m_vars.size(); + while (i > 0) { + --i; + expr * def = m_defs.get(i); + ev(def, val); + TRACE("extension_mc", tout << m_vars.get(i)->get_name() << " ->\n" << mk_ismt2_pp(def, m()) << "\n==>\n" << mk_ismt2_pp(val, m()) << "\n";); + func_decl * f = m_vars.get(i); + unsigned arity = f->get_arity(); + if (arity == 0) { + md->register_decl(f, val); + } + else { + func_interp * new_fi = alloc(func_interp, m(), arity); + new_fi->set_else(val); + md->register_decl(f, new_fi); } } TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md);); } +void extension_model_converter::insert(func_decl * v, expr * def) { + m_vars.push_back(v); + m_defs.push_back(def); +} + + void extension_model_converter::display(std::ostream & out) { - ast_manager & m = m_vars.get_manager(); out << "(extension-model-converter"; for (unsigned i = 0; i < m_vars.size(); i++) { out << "\n (" << m_vars.get(i)->get_name() << " "; unsigned indent = m_vars.get(i)->get_name().size() + 4; - out << mk_ismt2_pp(m_defs.get(i), m, indent) << ")"; + out << mk_ismt2_pp(m_defs.get(i), m(), indent) << ")"; } out << ")" << std::endl; } @@ -108,6 +91,5 @@ model_converter * extension_model_converter::translate(ast_translation & transla res->m_vars.push_back(translator(m_vars[i].get())); for (unsigned i = 0; i < m_defs.size(); i++) res->m_defs.push_back(translator(m_defs[i].get())); - // m_eval is a transient object. So, it doesn't need to be translated. return res; } diff --git a/src/tactic/extension_model_converter.h b/src/tactic/extension_model_converter.h index ba113c7ab..7124c3bee 100644 --- a/src/tactic/extension_model_converter.h +++ b/src/tactic/extension_model_converter.h @@ -23,15 +23,12 @@ Notes: #include"ast.h" #include"model_converter.h" -class model_evaluator; class extension_model_converter : public model_converter { func_decl_ref_vector m_vars; expr_ref_vector m_defs; - model_evaluator * m_eval; - struct set_eval; public: - extension_model_converter(ast_manager & m):m_vars(m), m_defs(m), m_eval(0) { + extension_model_converter(ast_manager & m):m_vars(m), m_defs(m) { } virtual ~extension_model_converter(); @@ -43,10 +40,7 @@ public: virtual void display(std::ostream & out); // register a variable that was eliminated - void insert(func_decl * v, expr * def) { - m_vars.push_back(v); - m_defs.push_back(def); - } + void insert(func_decl * v, expr * def); virtual model_converter * translate(ast_translation & translator); };