diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 6f08fe6a1..078515184 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -628,9 +628,6 @@ namespace arith { } else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) { anum const& an = nl_value(v, m_nla->tmp1()); - - - if (a.is_int(o) && !m_nla->am().is_int(an)) value = a.mk_numeral(rational::zero(), a.is_int(o)); else diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 0607f530d..c9deb5726 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -177,10 +177,9 @@ namespace polysat { s.set_lemma(m_viable.get_core(), m_viable.explain()); // propagate_unsat_core(); return sat::check_result::CR_CONTINUE; - case find_t::singleton: { + case find_t::singleton: s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain()); - return sat::check_result::CR_CONTINUE; - } + return sat::check_result::CR_CONTINUE; case find_t::multiple: s.add_eq_literal(m_var, m_value); return sat::check_result::CR_CONTINUE; diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index fb0875ec8..46661dc84 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -60,10 +60,10 @@ namespace polysat { // attributes associated with variables vector m_vars; // for each variable a pdd vector m_values; // current value of assigned variable - svector m_justification; // justification for assignment - activity m_activity; // activity of variables - var_queue m_var_queue; // priority queue of variables to assign - vector m_watch; // watch lists for variables for constraints on m_prop_queue where they occur + svector m_justification; // justification for assignment + activity m_activity; // activity of variables + var_queue m_var_queue; // priority queue of variables to assign + vector m_watch; // watch lists for variables for constraints on m_prop_queue where they occur // values to split on rational m_value; @@ -101,6 +101,7 @@ namespace polysat { constraint_id register_constraint(signed_constraint& sc, dependency d); bool propagate(); void assign_eh(constraint_id idx, bool sign, unsigned level); + pvar next_var() { return m_var_queue.next_var(); } pdd value(rational const& v, unsigned sz); pdd subst(pdd const&); diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp index b7d312d55..175d3a145 100644 --- a/src/sat/smt/polysat/op_constraint.cpp +++ b/src/sat/smt/polysat/op_constraint.cpp @@ -96,7 +96,21 @@ namespace polysat { } lbool op_constraint::eval_ashr(pdd const& p, pdd const& q, pdd const& r) { - NOT_IMPLEMENTED_YET(); + auto& m = p.manager(); + if (r.is_val() && p.is_val() && q.is_val()) { + auto M = m.max_value(); + auto N = M + 1; + if (p.val() >= N/2) { + if (q.val() >= m.power_of_2()) + return to_lbool(r.val() == M); + unsigned k = q.val().get_unsigned(); + return to_lbool(r.val() == p.val() - rational::power_of_two(k)); + } + else + return eval_lshr(p, q, r); + } + if (q.is_val() && q.is_zero() && p == r) + return l_true; return l_undef; } diff --git a/src/sat/smt/polysat_model.cpp b/src/sat/smt/polysat_model.cpp index 5bd8d4dc9..028aeed6b 100644 --- a/src/sat/smt/polysat_model.cpp +++ b/src/sat/smt/polysat_model.cpp @@ -23,12 +23,7 @@ Author: namespace polysat { - void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { - - if (m_use_intblast_model) { - m_intblast.add_value(n, mdl, values); - return; - } + void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { auto p = expr2pdd(n->get_expr()); rational val; if (!m_core.try_eval(p, val)) { @@ -82,8 +77,7 @@ namespace polysat { for (unsigned v = 0; v < get_num_vars(); ++v) if (m_var2pdd_valid.get(v, false)) out << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n"; - if (m_use_intblast_model) - m_intblast.display(out); + m_intblast.display(out); return out; } } diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 75dd09075..219b9017a 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -61,25 +61,36 @@ namespace polysat { return sat::check_result::CR_DONE; case sat::check_result::CR_CONTINUE: return sat::check_result::CR_CONTINUE; - case sat::check_result::CR_GIVEUP: { - if (!m.inc()) - return sat::check_result::CR_GIVEUP; - switch (m_intblast.check_solver_state()) { - case l_true: - trail().push(value_trail(m_use_intblast_model)); - m_use_intblast_model = true; - return sat::check_result::CR_DONE; - case l_false: { - auto core = m_intblast.unsat_core(); - for (auto& lit : core) - lit.neg(); - s().add_clause(core.size(), core.data(), sat::status::th(true, get_id(), nullptr)); - return sat::check_result::CR_CONTINUE; - } - case l_undef: - return sat::check_result::CR_GIVEUP; - } + case sat::check_result::CR_GIVEUP: + return intblast(); } + UNREACHABLE(); + return sat::check_result::CR_GIVEUP; + } + + sat::check_result solver::intblast() { + if (!m.inc()) + return sat::check_result::CR_GIVEUP; + switch (m_intblast.check_solver_state()) { + case l_true: { + pvar pv = m_core.next_var(); + auto v = m_pddvar2var[pv]; + auto n = var2expr(v); + auto val = m_intblast.get_value(n); + sat::literal lit = eq_internalize(n, bv.mk_numeral(val, get_bv_size(v))); + s().set_phase(lit); + return sat::check_result::CR_CONTINUE; + } + case l_false: { + IF_VERBOSE(2, verbose_stream() << "unsat core: " << m_intblast.unsat_core() << "\n"); + auto core = m_intblast.unsat_core(); + for (auto& lit : core) + lit.neg(); + s().add_clause(core.size(), core.data(), sat::status::th(true, get_id(), nullptr)); + return sat::check_result::CR_CONTINUE; + } + case l_undef: + return sat::check_result::CR_GIVEUP; } UNREACHABLE(); return sat::check_result::CR_GIVEUP; diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index 0ecc8941b..60535207b 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -59,7 +59,6 @@ namespace polysat { stats m_stats; core m_core; intblast::solver m_intblast; - bool m_use_intblast_model = false; vector m_var2pdd; // theory_var 2 pdd bool_vector m_var2pdd_valid; // valid flag @@ -73,6 +72,8 @@ namespace polysat { unsigned m_lemma_level = 0; expr_ref_vector m_lemma; + sat::check_result intblast(); + // internalize bool visit(expr* e) override; bool visited(expr* e) override;