diff --git a/src/ast/converters/generic_model_converter.cpp b/src/ast/converters/generic_model_converter.cpp index 81f24ed8a..f64e798b5 100644 --- a/src/ast/converters/generic_model_converter.cpp +++ b/src/ast/converters/generic_model_converter.cpp @@ -22,6 +22,7 @@ Notes: #include "ast/for_each_expr.h" #include "ast/ast_util.h" #include "ast/occurs.h" +#include "ast/bv_decl_plugin.h" #include "ast/rewriter/expr_safe_replace.h" #include "ast/rewriter/th_rewriter.h" #include "ast/converters/generic_model_converter.h" @@ -130,25 +131,32 @@ generic_model_converter * generic_model_converter::copy(ast_translation & transl return res; } -void generic_model_converter::convert_initialize_value(expr_ref& var, expr_ref& value) { - for (auto const& e : m_entries) { - switch (e.m_instruction) { - case HIDE: - break; - case ADD: - if (is_uninterp_const(var) && e.m_f == to_app(var)->get_decl()) - convert_initialize_value(e.m_def, var, value); - break; +void generic_model_converter::convert_initialize_value(vector> & var2value) { + if (var2value.empty() || m_entries.empty()) + return; + for (unsigned i = 0; i < var2value.size(); ++i) { + auto& [var, value] = var2value[i]; + for (auto const& e : m_entries) { + switch (e.m_instruction) { + case HIDE: + break; + case ADD: + if (is_uninterp_const(var) && e.m_f == to_app(var)->get_decl()) + convert_initialize_value(e.m_def, i, var2value); + break; + } } } } -void generic_model_converter::convert_initialize_value(expr* def, expr_ref& var, expr_ref& value) { +void generic_model_converter::convert_initialize_value(expr* def, unsigned i, vector>& var2value) { // var = if(c, th, el) = value // th = value => c = true // el = value => c = false expr* c = nullptr, *th = nullptr, *el = nullptr; + auto& [var, value] = var2value[i]; + verbose_stream() << "def " << mk_pp(def, m) << "\n"; if (m.is_ite(def, c, th, el)) { if (value == th) { var = c; @@ -164,8 +172,15 @@ void generic_model_converter::convert_initialize_value(expr* def, expr_ref& var, // var = def = value // => def = value - if (is_uninterp(def)) - var = def; + if (is_uninterp(def)) { + var = def; + return; + } + + bv_util bv(m); + if (bv.is_mkbv(def)) { + verbose_stream() << "def\n"; + } } diff --git a/src/ast/converters/generic_model_converter.h b/src/ast/converters/generic_model_converter.h index e778828cd..18ec16fe0 100644 --- a/src/ast/converters/generic_model_converter.h +++ b/src/ast/converters/generic_model_converter.h @@ -37,7 +37,7 @@ private: vector m_entries; expr_ref simplify_def(entry const& e); - void convert_initialize_value(expr* def, expr_ref& var, expr_ref& value); + void convert_initialize_value(expr* def, unsigned i, vector>& var2value); public: generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {} @@ -62,7 +62,7 @@ public: model_converter * translate(ast_translation & translator) override { return copy(translator); } - void convert_initialize_value(expr_ref& var, expr_ref& value) override; + void convert_initialize_value(vector>& var2value) override; generic_model_converter* copy(ast_translation & translator); diff --git a/src/ast/converters/model_converter.cpp b/src/ast/converters/model_converter.cpp index f03ef5327..c309bbb79 100644 --- a/src/ast/converters/model_converter.cpp +++ b/src/ast/converters/model_converter.cpp @@ -108,9 +108,9 @@ public: m_c1->get_units(fmls); } - void convert_initialize_value(expr_ref& var, expr_ref& value) override { - m_c2->convert_initialize_value(var, value); - m_c1->convert_initialize_value(var, value); + void convert_initialize_value(vector>& var2value) override { + m_c2->convert_initialize_value(var2value); + m_c1->convert_initialize_value(var2value); } diff --git a/src/ast/converters/model_converter.h b/src/ast/converters/model_converter.h index 0165cfbfc..354b51854 100644 --- a/src/ast/converters/model_converter.h +++ b/src/ast/converters/model_converter.h @@ -86,7 +86,7 @@ public: virtual void set_env(ast_pp_util* visitor); - virtual void convert_initialize_value(expr_ref& var, expr_ref& value) { } + virtual void convert_initialize_value(vector> & var2value) { } /** \brief we are adding a formula to the context of the model converter. diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 6eb1de598..c571753e9 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -311,11 +311,10 @@ namespace opt { } solver& s = get_solver(); s.assert_expr(m_hard_constraints); - for (auto & [var, value] : m_scoped_state.m_values) { - if (m_model_converter) - m_model_converter->convert_initialize_value(var, value); + if (m_model_converter) + m_model_converter->convert_initialize_value(m_scoped_state.m_values); + for (auto & [var, value] : m_scoped_state.m_values) s.user_propagate_initialize_value(var, value); - } opt_params optp(m_params); symbol pri = optp.priority(); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 8c4a79b76..19482c286 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -78,6 +78,7 @@ class inc_sat_solver : public solver { // this allows to access the internal state of the SAT solver and carry on partial results. bool m_internalized_converted; // have internalized formulas been converted back expr_ref_vector m_internalized_fmls; // formulas in internalized format + vector> m_var2value; typedef obj_map dep2asm_t; @@ -175,9 +176,27 @@ public: (m.is_not(e, e) && is_uninterp_const(e)); } + void initialize_values() { + if (m_mcs.back()) + m_mcs.back()->convert_initialize_value(m_var2value); + if (m_mcs.back()) + m_mcs.back()->display(verbose_stream()); + + for (auto & [var, value] : m_var2value) { + sat::bool_var b = m_map.to_bool_var(var); + if (b != sat::null_bool_var) + m_solver.set_phase(sat::literal(b, m.is_false(value))); + else if (get_euf()) + ensure_euf()->user_propagate_initialize_value(var, value); + } + } + lbool check_sat_core(unsigned sz, expr * const * assumptions) override { m_solver.pop_to_base_level(); m_core.reset(); + + + if (m_solver.inconsistent()) return l_false; expr_ref_vector _assumptions(m); obj_map asm2fml; @@ -202,6 +221,8 @@ public: r = internalize_assumptions(sz, _assumptions.data()); if (r != l_true) return r; + initialize_values(); + init_reason_unknown(); m_internalized_converted = false; bool reason_set = false; @@ -703,14 +724,7 @@ public: } void user_propagate_initialize_value(expr* var, expr* value) override { - expr_ref _var(var, m), _value(value, m); - if (m_mcs.back()) - m_mcs.back()->convert_initialize_value(_var, _value); - sat::bool_var b = m_map.to_bool_var(_var); - if (b != sat::null_bool_var) - m_solver.set_phase(sat::literal(b, m.is_false(_value))); - else if (get_euf()) - ensure_euf()->user_propagate_initialize_value(_var, _value); + m_var2value.push_back({expr_ref(var, m), expr_ref(value, m) }); } diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 223222f9a..e997cbc2c 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -32,13 +32,26 @@ class sat_tactic : public tactic { sat2goal m_sat2goal; scoped_ptr m_solver; params_ref m_params; + vector>& m_var2value; - imp(ast_manager & _m, params_ref const & p): + imp(ast_manager & _m, params_ref const & p, vector>& var2value): m(_m), m_solver(alloc(sat::solver, p, m.limit())), - m_params(p) { + m_params(p), + m_var2value(var2value) { updt_params(p); } + + void initialize_values(goal_ref const& g, atom2bool_var& map) { + g->mc()->convert_initialize_value(m_var2value); + for (auto & [var, value] : m_var2value) { + if (!m.is_bool(var)) + continue; + sat::bool_var b = map.to_bool_var(var); + if (b != sat::null_bool_var) + m_solver->set_phase(sat::literal(b, m.is_false(value))); + } + } void operator()(goal_ref const & g, goal_ref_buffer & result) { @@ -66,6 +79,8 @@ class sat_tactic : public tactic { g->reset(); g->m().compact_memory(); + initialize_values(g, map); + CASSERT("sat_solver", m_solver->check_invariant()); IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver->display_status(verbose_stream());); TRACE("sat_dimacs", m_solver->display_dimacs(tout);); @@ -184,11 +199,14 @@ class sat_tactic : public tactic { imp * m_imp; params_ref m_params; statistics m_stats; + ast_manager& m; + vector> m_var2value; public: sat_tactic(ast_manager & m, params_ref const & p): m_imp(nullptr), - m_params(p) { + m_params(p), + m(m) { sat_params p1(p); } @@ -215,7 +233,7 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override { - imp proc(g->m(), m_params); + imp proc(g->m(), m_params, m_var2value); scoped_set_imp set(this, &proc); try { proc(g, result); @@ -247,7 +265,8 @@ public: } void user_propagate_initialize_value(expr* var, expr* value) override { - + verbose_stream() << "initialize-value\n"; + m_var2value.push_back({ expr_ref(var, m), expr_ref(value, m) }); } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 163da9b16..deee05f6d 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2920,7 +2920,7 @@ namespace smt { } void context::initialize_value(expr* var, expr* value) { - IF_VERBOSE(10, verbose_stream() << "context initialize " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n"); + IF_VERBOSE(10, verbose_stream() << "initialize " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n"); sort* s = var->get_sort(); ensure_internalized(var); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index cf110298f..ca327891c 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1792,6 +1792,7 @@ namespace smt { void theory_bv::initialize_value(expr* var, expr* value) { rational val; unsigned sz; + TRACE("bv", tout << "initializing " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n"); if (!m_util.is_numeral(value, val, sz)) { IF_VERBOSE(5, verbose_stream() << "value should be a bit-vector " << mk_pp(value, m) << "\n"); return; diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp index 5958a9d38..5bc874abb 100644 --- a/src/tactic/bv/bit_blaster_model_converter.cpp +++ b/src/tactic/bv/bit_blaster_model_converter.cpp @@ -222,6 +222,34 @@ struct bit_blaster_model_converter : public model_converter { // no-op } + void convert_initialize_value(vector>& var2value) { + if (m_vars.empty() || var2value.empty()) + return; + rational r; + bv_util util(m()); + for (unsigned j = 0; j < var2value.size(); ++j) { + auto& [var, value] = var2value[j]; + if (!is_uninterp_const(var)) + continue; + if (!util.is_numeral(value, r)) + continue; + unsigned sz = m_vars.size(); + for (unsigned i = 0; i < sz; i++) { + if (m_vars.get(i) != to_app(var)->get_decl()) + continue; + unsigned k = 0; + expr_ref bit_k(m()); + for (auto arg : *to_app(m_bits.get(i))) { + bit_k = m().mk_bool_val(r.get_bit(k)); + var2value.push_back({ expr_ref(arg, m()), bit_k }); + ++k; + } + var2value[i] = var2value.back(); + var2value.pop_back(); + } + } + } + protected: bit_blaster_model_converter(ast_manager & m):m_vars(m), m_bits(m), m_newbits(m) { } public: