From f5aec6ecdf41b8e800ba50e07ae15468275ccc89 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jan 2024 13:12:42 -0800 Subject: [PATCH] bugbash Signed-off-by: Nikolaj Bjorner --- src/math/polynomial/algebraic_numbers.cpp | 2 + src/sat/smt/intblast_solver.cpp | 54 ++++++++++++++++------- src/sat/smt/polysat/viable.cpp | 43 ++++++++++++++---- 3 files changed, 75 insertions(+), 24 deletions(-) diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 736d08708..d8e4c2852 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -652,6 +652,7 @@ namespace algebraic_numbers { // collect non-basic roots sz = m_isolate_lowers.size(); for (unsigned i = 0; i < sz; i++) { + m_limit.inc(); mpbq & lower = m_isolate_lowers[i]; mpbq & upper = m_isolate_uppers[i]; if (!upm().isolating2refinable(f.size(), f.data(), bqm(), lower, upper)) { @@ -664,6 +665,7 @@ namespace algebraic_numbers { roots.push_back(numeral(c)); } } + checkpoint(); m_isolate_roots.reset(); m_isolate_lowers.reset(); m_isolate_uppers.reset(); diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index f3fee6ce2..1c6a8ef3b 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -18,6 +18,7 @@ Author: #include "sat/smt/intblast_solver.h" #include "sat/smt/euf_solver.h" #include "sat/smt/arith_value.h" +#include "smt/smt_solver.h" namespace intblast { @@ -199,7 +200,10 @@ namespace intblast { m_core.reset(); m_vars.reset(); m_is_plugin = false; - m_solver = mk_smt2_solver(m, s.params(), symbol::null); + params_ref p(s.params()); + p.set_uint("smt.bv.solver", 0); + p.set_bool("sat.smt", false); + m_solver = mk_smt_solver(m, p, symbol::null); for (unsigned i = 0; i < m_translate.size(); ++i) m_translate[i] = nullptr; @@ -211,21 +215,36 @@ namespace intblast { es.push_back(m.mk_eq(a->get_expr(), b->get_expr())); original_es.append(es); - translate(es); - for (auto e : m_vars) { - auto v = translated(e); - auto b = rational::power_of_two(bv.get_bv_size(e)); - m_solver->assert_expr(a.mk_le(a.mk_int(0), v)); - m_solver->assert_expr(a.mk_lt(v, a.mk_int(b))); + + verbose_stream() << es << "\n"; + + lbool r; + if (true) { + params_ref p; + p.set_uint("smt.bv.solver",0); + m_solver->updt_params(p); + r = m_solver->check_sat(es); + + } + else { + + translate(es); + + for (auto e : m_vars) { + auto v = translated(e); + auto b = rational::power_of_two(bv.get_bv_size(e)); + m_solver->assert_expr(a.mk_le(a.mk_int(0), v)); + m_solver->assert_expr(a.mk_lt(v, a.mk_int(b))); + } + + IF_VERBOSE(2, verbose_stream() << "check\n" << original_es << "\n"); + IF_VERBOSE(3, verbose_stream() << "check\n"; + m_solver->display(verbose_stream()); + verbose_stream() << es << "\n"); + + r = m_solver->check_sat(es); } - - IF_VERBOSE(2, verbose_stream() << "check\n" << original_es << "\n"); - IF_VERBOSE(3, verbose_stream() << "check\n"; - m_solver->display(verbose_stream()); - verbose_stream() << es << "\n"); - - lbool r = m_solver->check_sat(es); m_solver->collect_statistics(m_stats); @@ -357,6 +376,8 @@ namespace intblast { for (expr* e : es) { if (is_translated(e)) continue; + if (visited.is_marked(e)) + continue; sorted.push_back(e); visited.mark(e); } @@ -936,8 +957,11 @@ namespace intblast { set_translated(e, m.mk_ite(arg(0), arg(1), arg(2))); else if (m_is_plugin) set_translated(e, e); - else + else { + verbose_stream() << mk_pp(e, m) << "\n"; + verbose_stream() << mk_pp(m.mk_app(e->get_decl(), m_args), m) << "\n"; set_translated(e, m.mk_app(e->get_decl(), m_args)); + } } rational solver::get_value(expr* e) const { diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 65d48a683..44f97f95c 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -160,7 +160,7 @@ namespace polysat { void viable::update_value_to_high(rational& val, entry* e) { unsigned v_width = m_num_bits; - unsigned b_width = c.size(e->var); + unsigned b_width = e->bit_width; SASSERT(b_width <= v_width); auto hi = e->interval.hi_val(); @@ -456,6 +456,11 @@ namespace polysat { bool viable::is_conflict() { auto last = m_explain.back(); unsigned bw = last.e->bit_width; + if (last.e->interval.is_full()) { + m_explain.reset(); + m_explain.push_back(last); + return true; + } for (unsigned i = m_explain.size() - 1; i-- > 0; ) { auto e = m_explain[i]; if (bw < e.e->bit_width) @@ -472,17 +477,27 @@ namespace polysat { */ dependency_vector viable::explain() { dependency_vector result; - SASSERT(is_conflict()); + SASSERT(is_conflict()); uint_set seen; auto last = m_explain.back(); auto after = last; unsigned bw = c.size(last.e->var); + + result.append(m_fixed_bits.explain()); + + if (last.e->interval.is_full()) { + if (m_var != last.e->var) + result.push_back(offset_claim(m_var, { last.e->var, 0 })); + for (auto const& sc : last.e->side_cond) + result.push_back(c.propagate(sc, c.explain_eval(sc))); + result.push_back(c.get_dependency(last.e->constraint_index)); + SASSERT(m_explain.size() == 1); + } + for (unsigned i = m_explain.size() - 1; i-- > 0; ) { auto e = m_explain[i]; auto index = e.e->constraint_index; explain_overlap(e, after, result); - if (e.e == last.e) - break; after = e; if (seen.contains(index.id)) continue; @@ -492,9 +507,11 @@ namespace polysat { for (auto const& sc : e.e->side_cond) result.push_back(c.propagate(sc, c.explain_eval(sc))); result.push_back(c.get_dependency(index)); + if (e.e == last.e) + break; } - result.append(m_fixed_bits.explain()); + TRACE("bv", tout << "viable-explain v" << m_var << " - " << result.size() << "\n"); return result; } @@ -524,18 +541,25 @@ namespace polysat { void viable::explain_overlap(explanation const& e, explanation const& after, dependency_vector& deps) { auto bw = c.size(e.e->var); + auto ebw = e.e->bit_width; auto bw_after = c.size(after.e->var); + auto abw = after.e->bit_width; auto t = e.e->interval.hi(); auto lo = after.e->interval.lo(); auto hi = after.e->interval.hi(); - verbose_stream() << e.e->interval << " then " << after.e->interval << "\n"; + verbose_stream() << e.e->interval << " " << e.value << " " << t << " then " << after.e->interval << "\n"; SASSERT(after.e->bit_width <= bw_after); - SASSERT(e.e->bit_width <= bw); + SASSERT(ebw <= bw); + + if (ebw < bw) { + NOT_IMPLEMENTED_YET(); + } if (bw_after > bw) { auto eq = cs.eq(t, c.value(mod(e.value, rational::power_of_two(bw)), bw)); + SASSERT(!eq.is_always_false()); if (!eq.is_always_true()) deps.push_back(c.propagate(eq, c.explain_eval(eq))); t.reset(lo.manager()); @@ -544,19 +568,20 @@ namespace polysat { if (bw_after < bw) { auto eq = cs.eq(t, c.value(e.value, bw)); + SASSERT(!eq.is_always_false()); if (!eq.is_always_true()) deps.push_back(c.propagate(eq, c.explain_eval(eq))); t.reset(lo.manager()); t = c.value(mod(e.value, rational::power_of_two(bw_after)), bw_after); } - if (after.e->bit_width < bw_after) + if (abw < bw_after) t *= rational::power_of_two(bw_after - after.e->bit_width); auto sc = cs.ult(t - lo, hi - lo); - verbose_stream() << "in interval: " << sc << "\n"; if (sc.is_always_true()) return; + verbose_stream() << "in interval: " << sc << "\n"; SASSERT(!sc.is_always_false()); deps.push_back(c.propagate(sc, c.explain_eval(sc))); }