From b1072d0a1c1a9aeb2851f530372fd090b6713f3b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Dec 2023 10:59:27 -0800 Subject: [PATCH] hoist out fixed-bits reasoning into self-contained module without dependencies on viable entries --- src/sat/smt/polysat/core.h | 2 +- src/sat/smt/polysat/fixed_bits.cpp | 101 ++++++++++++++++++++++++++--- src/sat/smt/polysat/fixed_bits.h | 34 ++++++++-- src/sat/smt/polysat/types.h | 42 +++++++----- src/sat/smt/polysat/viable.cpp | 56 ++++------------ src/sat/smt/polysat/viable.h | 85 ++---------------------- src/sat/smt/polysat_egraph.cpp | 2 +- src/sat/smt/polysat_solver.cpp | 19 ++++++ 8 files changed, 183 insertions(+), 158 deletions(-) diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index 4ee1628f3..dc67b0ddc 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -145,7 +145,7 @@ namespace polysat { * Viable */ void get_bitvector_suffixes(pvar v, offset_slices& out); - void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits); + void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slice); void get_subslices(pvar v, offset_slices& out); /* diff --git a/src/sat/smt/polysat/fixed_bits.cpp b/src/sat/smt/polysat/fixed_bits.cpp index 85b35de66..515f0d019 100644 --- a/src/sat/smt/polysat/fixed_bits.cpp +++ b/src/sat/smt/polysat/fixed_bits.cpp @@ -13,14 +13,95 @@ Author: #include "sat/smt/polysat/fixed_bits.h" #include "sat/smt/polysat/ule_constraint.h" +#include "sat/smt/polysat/core.h" namespace polysat { + // reset with fixed bits information for variable v + void fixed_bits::reset(pvar v) { + m_fixed_slices.reset(); + m_var = v; + m_fixed.reset(); + m_fixed.resize(c.size(v), l_undef); + m_bits.reserve(c.size(v)); + fixed_bits_vector fbs; + c.get_fixed_bits(v, fbs); + for (auto const& fb : fbs) + for (unsigned i = fb.lo; i <= fb.hi; ++i) + m_fixed[i] = to_lbool(fb.value.get_bit(i - fb.lo)); + } + + // find then next value >= val that agrees with fixed bits, or false if none exists within the maximal value for val. + // examples + // fixed bits: 1?0 (least significant bit is last) + // val: 101 + // next: 110 + + // fixed bits ?1?0 + // val 1011 + // next 1100 + + // algorith: Let i be the most significant index where fixed bits disagree with val. + // If m_fixed[i] == l_true; then updating val to mask by fixed bits sufficies. + // Otherwise, the range above the disagreement has to be incremented. + // Increment the non-fixed bits by 1 + // The first non-fixed 0 position is set to 1, non-fixed positions below are set to 0.s + // If there are none, then the value is maximal and we return false. + + bool fixed_bits::next(rational& val) { + if (m_fixed_slices.empty()) + return true; + unsigned sz = c.size(m_var); + for (unsigned i = 0; i < sz; ++i) + m_bits[i] = val.get_bit(i); + unsigned i = sz; + for (; i-- > 0; ) + if (m_fixed[i] != l_undef && m_fixed[i] != to_lbool(m_bits[i])) + break; + if (i == 0) + return true; + + for (unsigned j = 0; j < sz; ++j) { + if (m_fixed[j] != l_undef) + m_bits[j] = m_fixed[j] == l_true; + else if (j < i) + m_bits[j] = false; + } + + if (m_fixed[i] == l_false) { + for (; i < sz; ++i) { + if (m_fixed[i] != l_undef) + continue; + if (m_bits[i]) + m_bits[i] = false; + else { + m_bits[i] = true; + break; + } + } + // overflow + if (i == sz) + return false; + } + val = 0; + for (unsigned i = sz; i-- > 0;) + val = val * 2 + rational(m_bits[i]); + return true; + } + + // explain the fixed bits ranges. + dependency_vector fixed_bits::explain() { + dependency_vector result; + for (auto const& slice : m_fixed_slices) + result.push_back(dependency({ m_var, slice })); + return result; + } + /** * 2^k * x = 2^k * b * ==> x[N-k-1:0] = b[N-k-1:0] */ - bool get_eq_fixed_lsb(pdd const& p, fixed_bits& out) { + bool get_eq_fixed_lsb(pdd const& p, fixed_slice& out) { SASSERT(!p.is_val()); unsigned const N = p.power_of_2(); // Recognize p = 2^k * a * x - 2^k * b @@ -39,7 +120,7 @@ namespace polysat { if (d.parity(N) < k) return false; rational const b = machine_div2k(d, k); - out = fixed_bits(N - k - 1, 0, b); + out = fixed_slice(N - k - 1, 0, b); SASSERT_EQ(d, b * rational::power_of_two(k)); SASSERT_EQ(p, (p.manager().mk_var(p.var()) - out.value) * rational::power_of_two(k)); return true; @@ -66,7 +147,7 @@ namespace polysat { #endif } - bool get_eq_fixed_bits(pdd const& p, fixed_bits& out) { + bool get_eq_fixed_slice(pdd const& p, fixed_slice& out) { if (get_eq_fixed_lsb(p, out)) return true; return false; @@ -80,7 +161,7 @@ namespace polysat { * ==> x[1:0] = 1 * -- TODO: Generalize [the obvious solution does not work] */ - bool get_ule_fixed_lsb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out) { + bool get_ule_fixed_lsb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out) { return false; } @@ -90,7 +171,7 @@ namespace polysat { * x <= 2^k - 1 ==> x[N-1:k] = 0 * x < 2^k ==> x[N-1:k] = 0 */ - bool get_ule_fixed_msb(pdd const& p, pdd const& q, bool is_positive, fixed_bits& out) { + bool get_ule_fixed_msb(pdd const& p, pdd const& q, bool is_positive, fixed_slice& out) { SASSERT(!q.is_zero()); // equalities are handled elsewhere unsigned const N = p.power_of_2(); pdd const& lhs = is_positive ? p : q; @@ -117,14 +198,14 @@ namespace polysat { } // 2^(N-1) <= 2^(N-1-i) * x - bool get_ule_fixed_bit(pdd const& p, pdd const& q, bool is_positive, fixed_bits& out) { + bool get_ule_fixed_bit(pdd const& p, pdd const& q, bool is_positive, fixed_slice& out) { return false; } - bool get_ule_fixed_bits(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out) { + bool get_ule_fixed_slice(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out) { SASSERT(ule_constraint::is_simplified(lhs, rhs)); if (rhs.is_zero()) - return is_positive ? get_eq_fixed_bits(lhs, out) : false; + return is_positive ? get_eq_fixed_slice(lhs, out) : false; if (get_ule_fixed_msb(lhs, rhs, is_positive, out)) return true; if (get_ule_fixed_lsb(lhs, rhs, is_positive, out)) @@ -134,10 +215,10 @@ namespace polysat { return false; } - bool get_fixed_bits(signed_constraint c, fixed_bits& out) { + bool get_fixed_slice(signed_constraint c, fixed_slice& out) { SASSERT_EQ(c.vars().size(), 1); // this only makes sense for univariate constraints if (c.is_ule()) - return get_ule_fixed_bits(c.to_ule().lhs(), c.to_ule().rhs(), c.is_positive(), out); + return get_ule_fixed_slice(c.to_ule().lhs(), c.to_ule().rhs(), c.is_positive(), out); // if (c->is_op()) // ; // TODO: x & constant = constant ==> bitmask ... but we have trouble recognizing that because we introduce a new variable for '&' before we see the equality. return false; diff --git a/src/sat/smt/polysat/fixed_bits.h b/src/sat/smt/polysat/fixed_bits.h index 2de5f2692..5a30ac039 100644 --- a/src/sat/smt/polysat/fixed_bits.h +++ b/src/sat/smt/polysat/fixed_bits.h @@ -17,13 +17,33 @@ Author: namespace polysat { - bool get_eq_fixed_lsb(pdd const& p, fixed_bits& out); - bool get_eq_fixed_bits(pdd const& p, fixed_bits& out); + class core; - bool get_ule_fixed_lsb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out); - bool get_ule_fixed_msb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out); - bool get_ule_fixed_bit(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out); - bool get_ule_fixed_bits(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out); - bool get_fixed_bits(signed_constraint c, fixed_bits& out); + bool get_eq_fixed_lsb(pdd const& p, fixed_slice& out); + bool get_eq_fixed_slice(pdd const& p, fixed_slice& out); + bool get_ule_fixed_lsb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out); + bool get_ule_fixed_msb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out); + bool get_ule_fixed_bit(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out); + bool get_ule_fixed_slice(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out); + bool get_fixed_slice(signed_constraint c, fixed_slice& out); + + class fixed_bits { + core& c; + pvar m_var = null_var; + vector m_fixed_slices; + svector m_fixed; + bool_vector m_bits; + public: + fixed_bits(core& c) : c(c) {} + + // reset with fixed bits information for variable v + void reset(pvar v); + + // find then next value >= val that agrees with fixed bits, or false if none exists within the maximal value for val. + bool next(rational& val); + + // explain the fixed bits ranges. + dependency_vector explain(); + }; } diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index 603db7e8f..7e5bf5e38 100644 --- a/src/sat/smt/polysat/types.h +++ b/src/sat/smt/polysat/types.h @@ -34,24 +34,46 @@ namespace polysat { class signed_constraint; + struct fixed_slice { + unsigned hi = 0; + unsigned lo = 0; + rational value; + fixed_slice() = default; + fixed_slice(unsigned hi, unsigned lo, rational value) : hi(hi), lo(lo), value(value) {} + }; + + struct fixed_claim : public fixed_slice { + pvar v; + fixed_claim() = default; + fixed_claim(pvar v, unsigned hi, unsigned lo, rational value) : fixed_slice(hi, lo, value), v(v) {} + fixed_claim(pvar, fixed_slice const& s) : fixed_slice(s), v(v) {} + }; + + struct offset_slice { + pvar v; + unsigned offset; + }; class dependency { struct axiom_t {}; - std::variant m_data; + std::variant m_data; dependency(): m_data(axiom_t()) {} public: dependency(sat::bool_var v) : m_data(v){} - dependency(theory_var v1, theory_var v2) : m_data(std::make_pair(v1, v2)) {} + dependency(theory_var v1, theory_var v2) : m_data(std::make_pair(v1, v2)) {} dependency(offset_claim const& c) : m_data(c) {} + dependency(fixed_claim const& c): m_data(c) {} static dependency axiom() { return dependency(); } bool is_null() const { return is_bool_var() && *std::get_if(&m_data) == sat::null_bool_var; } bool is_axiom() const { return std::holds_alternative(m_data); } bool is_eq() const { return std::holds_alternative(m_data); } bool is_bool_var() const { return std::holds_alternative(m_data); } bool is_offset_claim() const { return std::holds_alternative(m_data); } + bool is_fixed_claim() const { return std::holds_alternative(m_data); } sat::bool_var bool_var() const { SASSERT(is_bool_var()); return *std::get_if(&m_data); } theory_var_pair eq() const { SASSERT(is_eq()); return *std::get_if(&m_data); } offset_claim offset() const { return *std::get_if(&m_data); } + fixed_claim fixed() const { return *std::get_if(&m_data); } }; inline const dependency null_dependency = dependency(sat::null_bool_var); @@ -72,24 +94,12 @@ namespace polysat { } - struct fixed_bits { - unsigned hi = 0; - unsigned lo = 0; - rational value; - fixed_bits() = default; - fixed_bits(unsigned hi, unsigned lo, rational value) : hi(hi), lo(lo), value(value) {} - }; - - struct offset_slice { - pvar v; - unsigned offset; - }; inline std::ostream& operator<<(std::ostream& out, offset_slice const& js) { return out << "v" << js.v << "[" << js.offset << "[ @"; } - using fixed_bits_vector = svector; + using fixed_bits_vector = svector; using dependency_vector = vector; using constraint_or_dependency = std::variant; @@ -118,7 +128,7 @@ namespace polysat { virtual void get_bitvector_suffixes(pvar v, offset_slices& out) = 0; virtual void get_bitvector_sub_slices(pvar v, offset_slices& out) = 0; virtual void get_bitvector_super_slices(pvar v, offset_slices& out) = 0; - virtual void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits) = 0; + virtual void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slice) = 0; virtual unsigned level(dependency const& d) = 0; }; diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 17a867b2e..e588da9fd 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -26,7 +26,7 @@ namespace polysat { using dd::val_pp; - viable::viable(core& c) : c(c), cs(c.cs()), m_forbidden_intervals(c) {} + viable::viable(core& c) : c(c), cs(c.cs()), m_forbidden_intervals(c), m_fixed_bits(c) {} viable::~viable() { for (auto* e : m_alloc) @@ -123,7 +123,7 @@ namespace polysat { lbool viable::find_viable(pvar v, rational& lo, rational& hi) { m_explain.reset(); - init_fixed_bits(v); + m_fixed_bits.reset(v); init_overlays(v); return l_undef; @@ -132,7 +132,7 @@ namespace polysat { rational const& max_value = c.var2pdd(v).max_value(); - lbool r = find_on_layers(v, m_widths, m_overlaps, m_fbi, rational::zero(), max_value, lo); + lbool r = find_on_layers(v, m_widths, m_overlaps, rational::zero(), max_value, lo); if (r != l_true) return r; @@ -141,7 +141,7 @@ namespace polysat { return l_true; } - r = find_on_layers(v, m_widths, m_overlaps, m_fbi, lo + 1, max_value, hi); + r = find_on_layers(v, m_widths, m_overlaps, lo + 1, max_value, hi); if (r != l_false) return r; @@ -156,7 +156,6 @@ namespace polysat { pvar const v, unsigned_vector const& widths, offset_slices const& overlaps, - fixed_bits_info const& fbi, rational const& to_cover_lo, rational const& to_cover_hi, rational& val) { @@ -169,7 +168,7 @@ namespace polysat { while (refinements--) { m_explain.shrink(explain_size); - lbool result = find_on_layer(v, widths.size() - 1, widths, overlaps, fbi, to_cover_lo, to_cover_hi, val, refine_todo); + lbool result = find_on_layer(v, widths.size() - 1, widths, overlaps, to_cover_lo, to_cover_hi, val, refine_todo); // store bit-intervals we have used for (entry* e : refine_todo) @@ -183,6 +182,7 @@ namespace polysat { // start refinement on smallest variable // however, we probably should rotate to avoid getting stuck in refinement loop on a 'bad' constraint bool refined = false; +#if 0 for (unsigned i = overlaps.size(); i-- > 0; ) { pvar x = overlaps[i].v; rational const& mod_value = c.var2pdd(x).two_to_N(); @@ -192,6 +192,7 @@ namespace polysat { break; } } +#endif if (!refined) return l_true; @@ -210,7 +211,6 @@ namespace polysat { unsigned const w_idx, unsigned_vector const& widths, offset_slices const& overlaps, - fixed_bits_info const& fbi, rational const& to_cover_lo, rational const& to_cover_hi, rational& val, @@ -283,6 +283,7 @@ namespace polysat { } } +#if 0 // when we cannot make progress by existing intervals any more, try interval from fixed bits if (!e) { e = refine_bits(v, val, w, fbi); @@ -291,6 +292,7 @@ namespace polysat { display_one(std::cerr << "found entry by bits: ", 0, e) << "\n"; } } +#endif // no more progress on current layer if (!e) @@ -346,6 +348,7 @@ namespace polysat { if (distance(val, n, mod_value) < distance(val, next_val, mod_value)) next_val = n; } +#if 0 if (entry* e = refine_bits(v, next_val, w, fbi)) { refine_todo.push_back(e); rational const& n = e->interval.lo_val(); @@ -353,6 +356,7 @@ namespace polysat { next_val = n; } SASSERT(!refine_bits(v, val, w, fbi)); +#endif SASSERT(val != next_val); unsigned const lower_w = widths[w_idx - 1]; @@ -366,7 +370,7 @@ namespace polysat { lower_cover_lo = 0; lower_cover_hi = lower_mod_value; rational a; - lbool result = find_on_layer(v, w_idx - 1, widths, overlaps, fbi, lower_cover_lo, lower_cover_hi, a, refine_todo); + lbool result = find_on_layer(v, w_idx - 1, widths, overlaps, lower_cover_lo, lower_cover_hi, a, refine_todo); VERIFY(result != l_undef); if (result == l_false) { SASSERT(c.inconsistent()); @@ -388,7 +392,7 @@ namespace polysat { lower_cover_hi = mod(next_val, lower_mod_value); rational a; - lbool result = find_on_layer(v, w_idx - 1, widths, overlaps, fbi, lower_cover_lo, lower_cover_hi, a, refine_todo); + lbool result = find_on_layer(v, w_idx - 1, widths, overlaps, lower_cover_lo, lower_cover_hi, a, refine_todo); if (result == l_false) { SASSERT(c.inconsistent()); return l_false; // conflict @@ -431,38 +435,6 @@ namespace polysat { return true; } - // returns true iff no conflict was encountered - bool viable::collect_bit_information(pvar v, bool add_conflict, fixed_bits_info& out_fbi) { - - pdd p = c.var(v); - unsigned const v_sz = c.size(v); - out_fbi.reset(v_sz); - auto& [fixed, just_src, just_side_cond, just_slice] = out_fbi; - - fixed_bits_vector fbs; - c.get_fixed_bits(v, fbs); - - for (auto const& fb : fbs) { - LOG("slicing fixed bits: v" << v << "[" << fb.hi << ":" << fb.lo << "] = " << fb.value); - for (unsigned i = fb.lo; i <= fb.hi; ++i) { - SASSERT(out_fbi.just_src[i].empty()); // since we don't get overlapping ranges from collect_fixed. - SASSERT(out_fbi.just_side_cond[i].empty()); - SASSERT(out_fbi.just_slicing[i].empty()); - out_fbi.fixed[i] = to_lbool(fb.value.get_bit(i - fb.lo)); - out_fbi.just_slicing[i].push_back(fb); - } - } - - entry* e1 = m_equal_lin[v]; - entry* e2 = m_units[v].get_entries(c.size(v)); // TODO: take other widths into account (will be done automatically by tracking fixed bits in the slicing egraph) - entry* first = e1; - if (!e1 && !e2) - return true; - - return true; - } - - /* * Explain why the current variable is not viable or signleton. */ @@ -474,7 +446,7 @@ namespace polysat { result.push_back(d); result.append(c.explain_eval(sc)); } - // TODO: explaination for fixed bits + result.append(m_fixed_bits.explain()); return result; } diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h index 2b552abfd..fc42cf931 100644 --- a/src/sat/smt/polysat/viable.h +++ b/src/sat/smt/polysat/viable.h @@ -23,6 +23,8 @@ Author: #include "sat/smt/polysat/types.h" #include "sat/smt/polysat/forbidden_intervals.h" +#include "sat/smt/polysat/fixed_bits.h" + namespace polysat { @@ -103,56 +105,6 @@ namespace polysat { entry* get_entries(unsigned bit_width) const { layer const* l = get_layer(bit_width); return l ? l->entries : nullptr; } }; - struct fixed_bits_info { - svector fixed; - vector> just_src; - vector> just_side_cond; - vector just_slicing; - - bool is_empty() const { - SASSERT_EQ(fixed.empty(), just_src.empty()); - SASSERT_EQ(fixed.empty(), just_side_cond.empty()); - return fixed.empty(); - } - - bool is_empty_at(unsigned i) const { - return fixed[i] == l_undef && just_src[i].empty() && just_side_cond[i].empty(); - } - - void reset(unsigned num_bits) { - fixed.reset(); - fixed.resize(num_bits, l_undef); - just_src.reset(); - just_src.resize(num_bits); - just_side_cond.reset(); - just_side_cond.resize(num_bits); - just_slicing.reset(); - just_slicing.resize(num_bits); - } - - void reset_just(unsigned i) { - just_src[i].reset(); - just_side_cond[i].reset(); - just_slicing[i].reset(); - } - - void set_just(unsigned i, entry* e) { - reset_just(i); - push_just(i, e); - } - - void push_just(unsigned i, entry* e) { - just_src[i].append(e->src); - just_side_cond[i].append(e->side_cond); - } - - void push_from_bit(unsigned i, unsigned src) { - just_src[i].append(just_src[src]); - just_side_cond[i].append(just_side_cond[src]); - just_slicing[i].append(just_slicing[src]); - } - }; - ptr_vector m_alloc; vector m_units; // set of viable values based on unit multipliers, layered by bit-width in descending order @@ -187,7 +139,6 @@ namespace polysat { pvar v, unsigned_vector const& widths, offset_slices const& overlaps, - fixed_bits_info const& fbi, rational const& to_cover_lo, rational const& to_cover_hi, rational& out_val); @@ -197,39 +148,14 @@ namespace polysat { unsigned w_idx, unsigned_vector const& widths, offset_slices const& overlaps, - fixed_bits_info const& fbi, rational const& to_cover_lo, rational const& to_cover_hi, rational& out_val, ptr_vector& refine_todo); - template - bool refine_viable(pvar v, rational const& val, fixed_bits_info const& fbi) { - throw default_exception("refine nyi"); - } - bool refine_viable(pvar v, rational const& val) { - throw default_exception("refine nyi"); - } - template - bool refine_bits(pvar v, rational const& val, fixed_bits_info const& fbi) { - throw default_exception("refine nyi"); - } - - template - entry* refine_bits(pvar v, rational const& val, unsigned num_bits, fixed_bits_info const& fbi) { - throw default_exception("refine nyi"); - } - - bool refine_equal_lin(pvar v, rational const& val) { - throw default_exception("refine nyi"); - } - - bool refine_disequal_lin(pvar v, rational const& val) { - throw default_exception("refine nyi"); - } void set_conflict_by_interval(pvar v, unsigned w, ptr_vector& intervals, unsigned first_interval); bool set_conflict_by_interval_rec(pvar v, unsigned w, entry** intervals, unsigned num_intervals, bool& create_lemma, uint_set& vars_to_explain); @@ -238,10 +164,7 @@ namespace polysat { throw default_exception("fine_value nyi"); } - bool collect_bit_information(pvar v, bool add_conflict, fixed_bits_info& out_fbi); - - - fixed_bits_info m_fbi; + fixed_bits m_fixed_bits; void init_fixed_bits(pvar v); unsigned_vector m_widths; @@ -259,7 +182,7 @@ namespace polysat { find_t find_viable(pvar v, rational& out_val); /* - * Explain why the current variable is not viable or signleton. + * Explain the current variable is not viable or signleton. */ dependency_vector explain(); diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp index ca56f0556..3981b05ad 100644 --- a/src/sat/smt/polysat_egraph.cpp +++ b/src/sat/smt/polysat_egraph.cpp @@ -107,7 +107,7 @@ namespace polysat { unsigned lo = offset, hi = bv.get_bv_size(n->get_expr()); rational value; VERIFY(bv.is_numeral(n->get_expr(), value)); - out.push_back({ fixed_bits(lo, hi, value) }); + out.push_back({ fixed_slice(lo, hi, value) }); return false; }; theory_var v = m_pddvar2var[pv]; diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 4aae1cd0e..956ecf535 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -223,6 +223,18 @@ namespace polysat { level = std::max(level, s().lvl(lit)); return level; } + else if (d.is_fixed_claim()) { + auto const& f = d.fixed(); + sat::literal_vector lits; + std::function consume = [&](auto* a, auto* b) { + ctx.get_eq_antecedents(a, b, lits); + }; + explain_fixed(f.v, f.lo, f.hi, f.value, consume); + unsigned level = 0; + for (auto lit : lits) + level = std::max(level, s().lvl(lit)); + return level; + } else { SASSERT(d.is_axiom()); return 0; @@ -281,6 +293,13 @@ namespace polysat { }; explain_slice(v, w, offset, consume); } + else if (d.is_fixed_claim()) { + auto const& f = d.fixed(); + std::function consume = [&](auto* a, auto* b) { + lits.push_back(~eq_internalize(a, b)); + }; + explain_fixed(f.v, f.lo, f.hi, f.value, consume); + } else { SASSERT(d.is_axiom()); }