From 39a4bb025ba286e3563c4f28ffb9e117c7b477d7 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer Date: Tue, 27 Dec 2022 08:44:55 +0100 Subject: [PATCH 1/2] Propagate assignment if all bits are assigned and use better justification if any found --- src/math/polynomial/polynomial.cpp | 4 +- src/math/polysat/fixed_bits.cpp | 421 ++++++++++++++++------------ src/math/polysat/fixed_bits.h | 259 +++++++++++------ src/math/polysat/op_constraint.cpp | 46 +-- src/math/polysat/solver.h | 1 + src/math/polysat/ule_constraint.cpp | 40 +-- src/test/polysat.cpp | 2 +- 7 files changed, 460 insertions(+), 313 deletions(-) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index b85ac1cf5..5d7d00afe 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -4398,8 +4398,8 @@ namespace polynomial { TRACE("gcd_calls", tout << "gcd\nu: "; u->display(tout, m_manager); tout << "\nv: "; v->display(tout, m_manager); tout << "\n";); TRACE("polynomial_gcd", tout << "gcd\nu: "; u->display(tout, m_manager); tout << "\nv: "; v->display(tout, m_manager); - tout << "\nis_zero(u): " << is_zero(u) << ", is_const(u): " << is_const(u) << "\n"; - tout << "is_zero(v): " << is_zero(v) << ", is_const(v): " << is_const(v) << "\n"; + tout << "\nis_zero(u): " << is_zero(u) << ", is_determined(u): " << is_const(u) << "\n"; + tout << "is_zero(v): " << is_zero(v) << ", is_determined(v): " << is_const(v) << "\n"; tout << "modular: " << m().modular() << "\n";); if (is_zero(u)) { r = const_cast(v); diff --git a/src/math/polysat/fixed_bits.cpp b/src/math/polysat/fixed_bits.cpp index d697f3312..34d954e22 100644 --- a/src/math/polysat/fixed_bits.cpp +++ b/src/math/polysat/fixed_bits.cpp @@ -16,45 +16,56 @@ Abstract: namespace polysat { - bit_justication* bit_justication::get_other_justification(const fixed_bits& fixed, const pdd& p, unsigned idx) { - return fixed.m_bvpos_to_justification[{ p, idx }].m_justification; + bit_justification* bit_justification::get_justification(fixed_bits& fixed, const pdd& p, unsigned idx) { + return fixed.get_bit_info(p).justification(idx).m_justification; } - - const tbv_ref* bit_justication::get_tbv(fixed_bits& fixed, const pdd& p) { + + unsigned bit_justification::get_level(fixed_bits& fixed, const pdd& p, unsigned idx) { + if (p.is_val()) + return 0; + bit_justification* j = get_justification(fixed, p, idx); + SASSERT(j); + return j->m_decision_level; + } + + const tbv_ref* bit_justification::get_tbv(fixed_bits& fixed, const pdd& p) { return fixed.get_tbv(p); } - - // returns: Is it consistent - bool bit_justication::fix_bit(solver& s, fixed_bits& fixed, const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication** j) { - SASSERT(j && *j); - if (!fixed.fix_bit(s, p, tbv, idx, val, *j) && (*j)->can_dealloc()) { - // TODO: Potential double deallocation; Check! - dealloc(*j); - *j = nullptr; + + bit_justification_constraint::bit_justification_constraint(solver& s, constraint* c, bit_dependencies&& dep) : m_constraint(c), m_dependencies(dep) { + fixed_bits& fixed = s.m_fixed_bits; + unsigned max = 0; + for (const auto& d : dep) { + unsigned lvl = get_level(fixed, *d.m_pdd, d.m_bit_idx); + if (lvl > max) + max = lvl; } - return fixed.m_consistent; + if (c->has_bvar() && s.m_bvars.is_assigned(c->bvar())) { + unsigned lvl = s.m_bvars.level(c->bvar()); + if (lvl > max) + max = lvl; + } + m_decision_level = max; } - - bool bit_justication::fix_bit(solver& s, fixed_bits& fixed, const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j) { - return fix_bit(s, fixed, p, tbv, idx, val, &j); - } - - void bit_justication_constraint::get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) { + + void bit_justification_constraint::get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) { for (const auto& dep : this->m_dependencies) { LOG("Dependency: pdd: " << dep.m_pdd << " idx: " << dep.m_bit_idx); + if (dep.m_pdd->is_val()) // We don't need to justify them + continue; to_process.push_back(dep); } } - bit_justication_constraint* bit_justication_constraint::mk_justify_at_least(constraint *c, const pdd& v, const tbv_ref& tbv, const rational& least) { - return mk_justify_between(c, v, tbv, least, rational::power_of_two(tbv.num_tbits()) - 1); + bit_justification_constraint* bit_justification_constraint::mk_justify_at_least(solver& s, constraint *c, const pdd& v, const tbv_ref& tbv, const rational& least) { + return mk_justify_between(s, c, v, tbv, least, rational::power_of_two(tbv.num_tbits()) - 1); } - bit_justication_constraint* bit_justication_constraint::mk_justify_at_most(constraint *c, const pdd& v, const tbv_ref& tbv, const rational& most) { - return mk_justify_between(c, v, tbv, rational::zero(), most); + bit_justification_constraint* bit_justification_constraint::mk_justify_at_most(solver& s, constraint *c, const pdd& v, const tbv_ref& tbv, const rational& most) { + return mk_justify_between(s, c, v, tbv, rational::zero(), most); } - bit_justication_constraint* bit_justication_constraint::mk_justify_between(constraint *c, const pdd& v, const tbv_ref& tbv, rational least, rational most) { + bit_justification_constraint* bit_justification_constraint::mk_justify_between(solver& s, constraint *c, const pdd& v, const tbv_ref& tbv, rational least, rational most) { SASSERT(least.is_nonneg()); SASSERT(most.is_nonneg()); @@ -67,7 +78,7 @@ namespace polysat { dep.push_back({ v, i }); } if (most.is_nonpos() && least.is_nonpos()) - return alloc(bit_justication_constraint, c, std::move(dep)); + return alloc(bit_justification_constraint, s, c, std::move(dep)); } SASSERT(most.is_pos() || least.is_pos()); @@ -82,11 +93,11 @@ namespace polysat { // r1 = (p0 q1 + p1 q0) + (p0 q0) / 2 = (p0 q1 + p1 q0) // r2 = (p0 q2 + p1 q1 + p2 q0) + (p0 q1 + p1 q0) / 2 + (p0 q0) / 4 = (p0 q2 + p1 q1 + p2 q0) + (p0 q1 + p1 q0) / 2 // r3 = (p0 q3 + p1 q2 + p2 q1 + p3 q0) + (p0 q2 + p1 q1 + p2 q0) / 2 + (p0 q1 + p1 q0) / 4 + (p0 q0) / 8 = (p0 q3 + p1 q2 + p2 q1 + p3 q0) + (p0 q2 + p1 q1 + p2 q0) / 2 - void bit_justication_mul::propagate(solver& s, fixed_bits& fixed, const pdd& r, const pdd &p, const pdd &q) { + void bit_justification_mul::propagate(solver& s, fixed_bits& fixed, const pdd& r, const pdd &p, const pdd &q) { LOG_H2("Bit-Propagating: " << r << " = (" << p << ") * (" << q << ")"); - tbv_ref& p_tbv = *fixed.get_tbv(p); - tbv_ref& q_tbv = *fixed.get_tbv(q); - tbv_ref& r_tbv = *fixed.get_tbv(r); + const tbv_ref& p_tbv = *fixed.get_tbv(p); + const tbv_ref& q_tbv = *fixed.get_tbv(q); + const tbv_ref& r_tbv = *fixed.get_tbv(r); LOG("p: " << p << " = " << p_tbv); LOG("q: " << q << " = " << q_tbv); LOG("r: " << r << " = " << r_tbv); @@ -158,7 +169,7 @@ namespace polysat { // We know the value of this bit // forward propagation // this might add a conflict if the value is already set to another value - if (!fix_bit(s, fixed, r, r_tbv, i, min_val & 1 ? BIT_1 : BIT_0, alloc(bit_justication_mul, i, p, q))) + if (!fixed.fix_bit(s, r, i, min_val & 1 ? BIT_1 : BIT_0, alloc(bit_justification_mul, i, p, q), false)) return; } else if (r_tbv[i] != BIT_z && min_val == max_val - 1) { @@ -176,9 +187,9 @@ namespace polysat { SASSERT(set == BIT_0 || set == BIT_1); SASSERT(highest_overflow_idx <= i); if (highest_overflow_precise) { // Otherwise, we cannot set the elements in the previous ri but we at least know max_val == min_val (resp., vice-versa) - bit_justication_shared* j = nullptr; + bit_justification_shared* j = nullptr; unsigned_vector set_bits; -#define SHARED_JUSTIFICATION (j ? (j->inc_ref(), (bit_justication**)&j) : (j = alloc(bit_justication_shared, alloc(bit_justication_mul, i, p, q, r)), (bit_justication**)&j)) +#define SHARED_JUSTIFICATION (j ? (j->inc_ref(), (bit_justification**)&j) : (j = alloc(bit_justification_shared, alloc(bit_justification_mul, i, p, q, r)), (bit_justification**)&j)) for (unsigned x = 0, y = i; x <= highest_overflow_idx; x++, y--) { tbit bit1 = p_tbv[x]; @@ -188,13 +199,13 @@ namespace polysat { // Does not set: (1, 1), (0, 0), (0, z), (z, 0) // Also does not set: (z, z) [because we don't know which one. We only know that it has to be 0 => we can still set max_val = min_val] if (bit1 == BIT_1) { - if (!fix_bit(s, fixed, q, q_tbv, y, BIT_0, SHARED_JUSTIFICATION)) { + if (!fixed.fix_bit(s, q, y, BIT_0, SHARED_JUSTIFICATION, false)) { VERIFY(false); } set_bits.push_back(y << 1 | 1); } else if (bit2 == BIT_1) { - if (!fix_bit(s, fixed, p, p_tbv, x, BIT_0, SHARED_JUSTIFICATION)) { + if (!fixed.fix_bit(s, p, x, BIT_0, SHARED_JUSTIFICATION, false)) { VERIFY(false); } set_bits.push_back(x << 1 | 0); @@ -204,20 +215,20 @@ namespace polysat { // Sets: (1, z), (z, 1), (1, 1), (z, z) // Does not set: (0, 0), (0, z), (z, 0), (0, 1), (1, 0) if (bit1 == BIT_1) { - if (!fix_bit(s, fixed, q, q_tbv, y, BIT_1, SHARED_JUSTIFICATION)) { + if (!fixed.fix_bit(s, q, y, BIT_1, SHARED_JUSTIFICATION, false)) { VERIFY(false); } set_bits.push_back(y << 1 | 1); } if (bit2 == BIT_1) { - if (!fix_bit(s, fixed, p, p_tbv, x, BIT_1, SHARED_JUSTIFICATION)) { + if (!fixed.fix_bit(s, p, x, BIT_1, SHARED_JUSTIFICATION, false)) { VERIFY(false); } set_bits.push_back(x << 1 | 0); } if (bit1 == BIT_z && bit2 == BIT_z) { - if (!fix_bit(s, fixed, p, p_tbv, i, BIT_1, SHARED_JUSTIFICATION) || - !fix_bit(s, fixed, q, q_tbv, i, BIT_1, SHARED_JUSTIFICATION)) { + if (!fixed.fix_bit(s, p, i, BIT_1, SHARED_JUSTIFICATION, false) || + !fixed.fix_bit(s, q, i, BIT_1, SHARED_JUSTIFICATION, false)) { VERIFY(false); } set_bits.push_back(y << 1 | 1); @@ -229,7 +240,7 @@ namespace polysat { if (j) { // the reference count might be higher than the number of elements in the vector // some elements might not be relevant for the justification (e.g., because of decision-level) - ((bit_justication_mul*)j->get_justification())->m_bit_indexes = set_bits; + ((bit_justification_mul*)j->get_justification())->m_bit_indexes = set_bits; } } } @@ -260,7 +271,7 @@ namespace polysat { // ... // the overflow increases on { 2, 5, 12, 21, 21, 38, 71, ... } that is 2^k + idx + 1 = 2^idx // Hence we can calculate it by "ilog2(idx - ilog2(idx) - 1)" if idx >= 7 or otherwise use the lookup table [0, 0, 1, 1, 1, 1, 1] (as the intermediate result is negative) - void bit_justication_mul::get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) { + void bit_justification_mul::get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) { unsigned relevant_range; // the number of previous places that might overflow to this bit if (m_idx < 7) relevant_range = m_idx >= 2; @@ -276,20 +287,20 @@ namespace polysat { get_dependencies_backward(fixed, to_process, p_tbv, q_tbv, relevant_range); } - void bit_justication_mul::get_dependencies_forward(fixed_bits &fixed, bit_dependencies &to_process, const tbv_ref& p_tbv, const tbv_ref& q_tbv, unsigned relevant_range) { + void bit_justification_mul::get_dependencies_forward(fixed_bits &fixed, bit_dependencies &to_process, const tbv_ref& p_tbv, const tbv_ref& q_tbv, unsigned relevant_range) { for (unsigned i = m_idx - relevant_range; i <= m_idx; i++) { for (unsigned x = 0, y = i; x <= i; x++, y--) { tbit bit1 = p_tbv[x]; tbit bit2 = q_tbv[y]; if (bit1 == BIT_1 && bit2 == BIT_1) { - get_other_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process); - get_other_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process); } else if (bit1 == BIT_0) // TODO: Take the better one if both are zero - get_other_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process); else if (bit2 == BIT_0) - get_other_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process); else { // The bit is apparently not set because we cannot derive a truth-value. // Why do we ask for an explanation? @@ -299,7 +310,7 @@ namespace polysat { } } - void bit_justication_mul::get_dependencies_backward(fixed_bits& fixed, bit_dependencies& to_process, const tbv_ref& p_tbv, const tbv_ref& q_tbv, unsigned relevant_range) { + void bit_justification_mul::get_dependencies_backward(fixed_bits& fixed, bit_dependencies& to_process, const tbv_ref& p_tbv, const tbv_ref& q_tbv, unsigned relevant_range) { SASSERT(!m_bit_indexes.empty()); // Who asked us for an explanation if there is nothing in the set? unsigned set_idx = 0; for (unsigned i = m_idx - relevant_range; i <= m_idx; i++) { @@ -330,21 +341,21 @@ namespace polysat { if (bit1 == BIT_1 && bit2 == BIT_1) { if (!p_in_set) - get_other_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process); if (!q_in_set) - get_other_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process); } else if (bit1 == BIT_0) { if (!p_in_set) - get_other_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process); else if (!q_in_set) - get_other_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process); } else if (bit2 == BIT_0 && !q_in_set) { if (!q_in_set) - get_other_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process); else if (!p_in_set) - get_other_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process); } else { // unlike in the forward case this can happen @@ -354,12 +365,12 @@ namespace polysat { } // similar to multiplying but far simpler/faster (only the direct predecessor might overflow) - void bit_justication_add::propagate(solver& s, fixed_bits& fixed, const pdd& r, const pdd& p, const pdd& q) { + void bit_justification_add::propagate(solver& s, fixed_bits& fixed, const pdd& r, const pdd& p, const pdd& q) { LOG_H2("Bit-Propagating: " << r << " = (" << p << ") + (" << q << ")"); // TODO: Add backward propagation - tbv_ref& p_tbv = *fixed.get_tbv(p); - tbv_ref& q_tbv = *fixed.get_tbv(q); - tbv_ref& r_tbv = *fixed.get_tbv(r); + const tbv_ref& p_tbv = *fixed.get_tbv(p); + const tbv_ref& q_tbv = *fixed.get_tbv(q); + const tbv_ref& r_tbv = *fixed.get_tbv(r); LOG("p: " << p << " = " << p_tbv); LOG("q: " << q << " = " << q_tbv); LOG("r: " << r << " = " << r_tbv); @@ -369,44 +380,59 @@ namespace polysat { unsigned min_bit_value = 0; unsigned max_bit_value = 0; + unsigned prev_max = 0; + unsigned max = 0; + for (unsigned i = 0; i < m.num_tbits(); i++) { tbit bit1 = p_tbv[i]; tbit bit2 = q_tbv[i]; - if (bit1 == BIT_1) { - min_bit_value++; + if (bit1 == BIT_z) max_bit_value++; + else { + if (bit1 == BIT_1) { + min_bit_value++; + max_bit_value++; + } + unsigned lvl = get_level(fixed, p, i); + if (lvl > max) + max = lvl; } - else if (bit1 == BIT_z) - max_bit_value++; - - if (bit2 == BIT_1) { - min_bit_value++; - max_bit_value++; - } - else if (bit2 == BIT_z) - max_bit_value++; - if (min_bit_value == max_bit_value) - if (!fix_bit(s, fixed, r, r_tbv, i, min_bit_value & 1 ? BIT_1 : BIT_0, alloc(bit_justication_add))) + if (bit2 == BIT_z) + max_bit_value++; + else { + if (bit2 == BIT_1) { + min_bit_value++; + max_bit_value++; + } + unsigned lvl = get_level(fixed, q, i); + if (lvl > max) + max = lvl; + } + + if (min_bit_value == max_bit_value) // TODO: We might not need a dedicated justification subclass for this + if (!fixed.fix_bit(s, r, i, min_bit_value & 1 ? BIT_1 : BIT_0, alloc(bit_justification_add, max > prev_max ? max : prev_max, i, p, q), false)) return; min_bit_value >>= 1; max_bit_value >>= 1; + prev_max = max; } } - void bit_justication_add::get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) { + void bit_justification_add::get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) { if (m_c1->power_of_2() > 1 && m_idx > 0) { - get_other_justification(fixed, *m_c1, m_idx - 1)->get_dependencies(fixed, to_process); - get_other_justification(fixed, *m_c2, m_idx - 1)->get_dependencies(fixed, to_process); + //TODO: Sure? Some might be nullptr if not set... + get_justification(fixed, *m_c1, m_idx - 1)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_c2, m_idx - 1)->get_dependencies(fixed, to_process); DEBUG_CODE( const tbv_ref& tbv1 = *get_tbv(fixed, *m_c1); const tbv_ref& tbv2 = *get_tbv(fixed, *m_c2); SASSERT(tbv1[m_idx - 1] != BIT_z && tbv2[m_idx - 1] != BIT_z); ); } - get_other_justification(fixed, *m_c1, m_idx)->get_dependencies(fixed, to_process); - get_other_justification(fixed, *m_c2, m_idx)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_c1, m_idx)->get_dependencies(fixed, to_process); + get_justification(fixed, *m_c2, m_idx)->get_dependencies(fixed, to_process); DEBUG_CODE( const tbv_ref& tbv1 = *get_tbv(fixed, *m_c1); const tbv_ref& tbv2 = *get_tbv(fixed, *m_c2); @@ -421,50 +447,53 @@ namespace polysat { return *m_tbv_managers[sz]; } - tbv_manager& fixed_bits::get_manager(const pdd& v) { - return get_manager(v.power_of_2()); + tbv_manager& fixed_bits::get_manager(const pdd& p) { + return get_manager(p.power_of_2()); } - tbv_ref* fixed_bits::get_tbv(const pdd& v) { - LOG("Looking for tbv for " << v); - auto found = m_var_to_tbv.find_iterator(optional(v)); - if (found == m_var_to_tbv.end()) { - auto& manager = get_manager(v.power_of_2()); - if (v.is_val()) - m_var_to_tbv.insert(optional(v), alloc(tbv_ref, manager, manager.allocate(v.val()))); - else - m_var_to_tbv.insert(optional(v), alloc(tbv_ref, manager, manager.allocate())); - return m_var_to_tbv[optional(v)]; + bitvec_info& fixed_bits::get_bit_info(const pdd& p) { + auto found = m_pdd_to_info.find_iterator(optional(p)); + if (found == m_pdd_to_info.end()) { + auto& manager = get_manager(p.power_of_2()); + if (p.is_val()) + m_pdd_to_info.insert(optional(p), bitvec_info(alloc(tbv_ref, manager, manager.allocate(p.val())))); + else + m_pdd_to_info.insert(optional(p), bitvec_info(alloc(tbv_ref, manager, manager.allocate()))); + return m_pdd_to_info[optional(p)]; } - /*if (m_var_to_tbv.size() <= v) { + /*if (m_var_to_tbv.size() <= p) { m_var_to_tbv.reserve(v + 1); auto& manager = get_manager(sz); - m_var_to_tbv[v] = tbv_ref(manager, manager.allocate()); - return *m_var_to_tbv[v]; + m_var_to_tbv[p] = tbv_ref(manager, manager.allocate()); + return *m_var_to_tbv[p]; }*/ return found->m_value; - /*auto& old_manager = m_var_to_tbv[optional(v)]->manager(); - if (old_manager.num_tbits() >= v.power_of_2()) - return *(m_var_to_tbv[optional(v)]); - tbv* old_tbv = m_var_to_tbv[optional(v)]->detach(); - auto& new_manager = get_manager(v.power_of_2()); + /*auto& old_manager = m_var_to_tbv[optional(p)]->manager(); + if (old_manager.num_tbits() >= p.power_of_2()) + return *(m_var_to_tbv[optional(p)]); + tbv* old_tbv = m_var_to_tbv[optional(p)]->detach(); + auto& new_manager = get_manager(p.power_of_2()); tbv* new_tbv = new_manager.allocate(); old_manager.copy(*new_tbv, *old_tbv); // Copy the lower bits to the new (larger) tbv old_manager.deallocate(old_tbv); m_var_to_tbv[optional(v)] = optional(tbv_ref(new_manager, new_tbv)); - return *m_var_to_tbv[optional(v)];*/ + return *m_var_to_tbv[optional(p)];*/ } - - clause_ref fixed_bits::get_explanation(solver& s, bit_justication* j1, bit_justication* j2) { + + const tbv_ref* fixed_bits::get_tbv(const pdd& v) { + return get_bit_info(v).get_tbv(); + } + + clause_ref fixed_bits::get_explanation(solver& s, bit_justification** js, unsigned cnt, bool free, signed_constraint* consequence) { bit_dependencies to_process; // TODO: Check that we do not process the same tuple multiples times (efficiency) - -#define GET_DEPENDENCY(X) do { (X)->get_dependencies(*this, to_process); if ((X)->can_dealloc()) { dealloc(X); } } while (false) - + +#define GET_DEPENDENCY(X) do { (X)->get_dependencies(*this, to_process); if (free && (X)->can_dealloc()) { dealloc(X); } } while (false) + clause_builder conflict(s); conflict.set_redundant(true); - - auto insert_constraint = [&conflict, &s](bit_justication* j) { + + auto insert_constraint = [&conflict, &s](bit_justification* j) { constraint* constr; if (!j->has_constraint(constr)) return; @@ -475,13 +504,13 @@ namespace polysat { conflict.insert(signed_constraint(constr, s.m_bvars.value(constr->bvar()) != l_true)); } }; - - insert_constraint(j1); - insert_constraint(j2); - - GET_DEPENDENCY(j1); - GET_DEPENDENCY(j2); - + + for (unsigned i = 0; i < cnt; i++) { + bit_justification* j = js[i]; + GET_DEPENDENCY(j); + insert_constraint(j); + } + // In principle, the dependencies should be acyclic so this should terminate. If there are cycles it is for sure a bug while (!to_process.empty()) { bvpos& curr = to_process.back(); @@ -489,121 +518,145 @@ namespace polysat { to_process.pop_back(); continue; // We don't need an explanation for bits of constants } - SASSERT(m_bvpos_to_justification.contains(curr)); - - bit_justication* j = m_bvpos_to_justification[curr].m_justification; + + bitvec_info& info = get_bit_info(*curr.m_pdd); + SASSERT(info.justification(curr.m_bit_idx).m_justification); + + bit_justification* j = info.justification(curr.m_bit_idx).m_justification; to_process.pop_back(); insert_constraint(j); GET_DEPENDENCY(j); } - + + if (consequence) + conflict.insert(*consequence); + return conflict.build(); } + clause_ref fixed_bits::get_explanation_assignment(solver& s, const pdd& p) { + SASSERT(!p.is_val()); + bitvec_info& info = get_bit_info(p); + rational value = info.get_value(); + signed_constraint eq = s.eq(p, p.manager().mk_val(value)); + svector justifications; + unsigned cnt = info.num_tbits(); + for (unsigned i = 0; i < cnt; i++) { + SASSERT(info.justification(i).m_justification); + justifications.push_back(info.justification(i).m_justification); + } + + return get_explanation(s, justifications.data(), info.num_tbits(), false, &eq); + } + + clause_ref fixed_bits::get_explanation_conflict(solver& s, bit_justification* j1, bit_justification* j2) { + SASSERT(!j1 && !j2); + bit_justification* conflict[2] { j1, j2 }; + return get_explanation(s, conflict, 2, true, nullptr); + } + + clause_ref fixed_bits::get_explanation_conflict(solver& s, bit_justification* j) { + SASSERT(!j); + return get_explanation(s, &j, 1, true, nullptr); + } + tbit fixed_bits::get_value(const pdd& p, unsigned idx) { SASSERT(p.is_var()); return (*get_tbv(p))[idx]; } // True iff the justification was stored (must not be deallocated!) - bool fixed_bits::fix_value_core(const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j) { - LOG("Fixing bit " << idx << " in " << p << " (" << tbv << ")"); + bool fixed_bits::fix_value_core(const pdd& p, bitvec_info& info, unsigned idx, tbit val, bit_justification* j) { + LOG("Fixing bit " << idx << " in " << p << " (" << *info.get_tbv() << ")"); constraint* c; if (j->has_constraint(c)) { LOG("justification constraint: " << *c); } - SASSERT(val != BIT_x); // We don't use don't-cares if (val == BIT_z) // just ignore this case return false; - tbit curr_val = tbv[idx]; - bvpos pos(p, idx); + tbit curr_val = info.get_bit(idx); if (val == curr_val) { // we already have the "correct" value there if (p.is_val()) return false; // no justification because it is trivial - SASSERT(m_bvpos_to_justification.contains(pos)); - justified_bvpos& old_j = m_bvpos_to_justification[pos]; - if (old_j.m_justification->m_decision_level > j->m_decision_level) + // Maybe the new justification is better + justified_bvpos& justfc = info.justification(idx); + if (justfc.m_justification->m_decision_level <= j->m_decision_level) return false; - replace_justification(old_j, j); // the new justification is better. Let's take it + replace_justification(justfc, j); // the new justification is better. Let's take it return true; } - auto& m = tbv.manager(); - if (curr_val == BIT_z) { - m.set(*tbv, idx, val); - justified_bvpos jpos(pos, j, m_trail.size()); - - auto jstfc = m_bvpos_to_justification.get(pos, {}); - if (jstfc.m_justification && jstfc.m_justification->can_dealloc()) - dealloc(jstfc.m_justification); - - m_bvpos_to_justification.insert(pos, jpos); - m_trail.push_back(jpos); + info.set_bit(idx, val); + justified_bvpos& just = info.justification(idx); + just.set(j); + m_trail.push_back(&just); + SASSERT(!info.is_determined()); + info.dec_unset(); return true; } SASSERT((curr_val == BIT_1 && val == BIT_0) || (curr_val == BIT_0 && val == BIT_1)); - SASSERT(p.is_val() || m_bvpos_to_justification.contains(pos)); m_consistent = false; return false; } - bool fixed_bits::fix_bit(solver& s, const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j) { - SASSERT(m_trail.size() == s.m_level); - - bool changed = fix_value_core(p, tbv, idx, val, j); - if (changed) - return true; - - if (!m_consistent) { - bvpos pos(p, idx); - clause_ref explanation = get_explanation(s, j, m_bvpos_to_justification[pos].m_justification); - s.set_conflict(*explanation); - } - return false; - } - // return: consistent? - bool fixed_bits::fix_value(solver& s, const pdd& p, unsigned idx, tbit val, bit_justication* j) { - tbv_ref& tbv = *get_tbv(p); - bool changed = fix_value_core(p, tbv, idx, val, j); + bool fixed_bits::fix_bit(solver& s, const pdd& p, unsigned idx, tbit val, bit_justification** j, bool recursive) { + SASSERT(m_trail_size.size() == s.m_level); + SASSERT(j && *j); + + bitvec_info& info = get_bit_info(p); + bool changed = fix_value_core(p, info, idx, val, *j); if (changed) { // this implies consistency - propagate_to_subterm(s, p); + SASSERT(!p.is_val()); + if (info.is_determined()) + // We might propagate again if we find a better explanation + get_explanation_assignment(s, p); + if (recursive) + propagate_to_subterm(s, p); return true; } - // TODO: Propagate equality if everything is set if (!m_consistent) { LOG("Adding conflict on bit " << idx << " on pdd " << p); - clause_ref explanation = get_explanation(s, j, m_bvpos_to_justification[{ p, idx }].m_justification); + auto& other = info.justification(idx); + clause_ref explanation = + other.m_pdd->is_val() + ? get_explanation_conflict(s, *j) + : get_explanation_conflict(s, *j, info.justification(idx).m_justification); s.set_conflict(*explanation); return false; // get_explanation will dealloc the justification } - if (j->can_dealloc()) - dealloc(j); + if ((*j)->can_dealloc()) { + dealloc(*j); + *j = nullptr; + } return m_consistent; } + bool fixed_bits::fix_bit(solver& s, const pdd& p, unsigned idx, tbit val, bit_justification* j, bool recursive) { + return fix_bit(s, p, idx, val, &j, recursive); + } + void fixed_bits::clear_value(const pdd& p, unsigned idx) { - tbv_ref& tbv = *get_tbv(p); - auto& m = tbv.manager(); - m.set(*tbv, idx, BIT_z); - bvpos pos(p, idx); - SASSERT(m_bvpos_to_justification.contains(pos)); - const auto& jstfc = m_bvpos_to_justification[pos]; - if (jstfc.m_justification->can_dealloc()) - dealloc(jstfc.m_justification); - m_bvpos_to_justification.remove(pos); + bitvec_info& info = get_bit_info(p); + info.set_bit(idx, BIT_z); + justified_bvpos& j = info.justification(idx); + SASSERT(j.m_justification); + + if (j.m_justification->can_dealloc()) + dealloc(j.m_justification); + j.m_justification = nullptr; } - void fixed_bits::replace_justification(const justified_bvpos& old_j, bit_justication* new_j) { - SASSERT(old_j.m_justification->m_decision_level > new_j->m_decision_level); - SASSERT(m_trail[old_j.m_trail_pos] == old_j); + void fixed_bits::replace_justification(justified_bvpos& jstfc, bit_justification* new_j) { + SASSERT(jstfc.m_justification->m_decision_level > new_j->m_decision_level); + //SASSERT(m_trail[old_j.m_trail_pos] == &old_j); - if (old_j.m_justification->can_dealloc()) - dealloc(old_j.m_justification); - m_trail[old_j.m_trail_pos].m_justification = new_j; // We only overwrite with smaller decision-levels. This way we preserve some kind of "order" + if (jstfc.m_justification->can_dealloc()) + dealloc(jstfc.m_justification); + jstfc.m_justification = new_j; // We only overwrite with smaller decision-levels. This way we preserve some kind of "order" } void fixed_bits::push() { @@ -614,7 +667,6 @@ namespace polysat { void fixed_bits::pop(unsigned pop_cnt) { #if 0 - SASSERT(!m_consistent); // Why do we backtrack if this is true? We might remove this for (random) restarts SASSERT(pop_cnt > 0); unsigned old_lvl = m_trail_size.size(); @@ -628,11 +680,12 @@ namespace polysat { for (unsigned i = m_trail.size(); i > prev_cnt; i--) { // all elements m_trail[j] with (j > i) have higher decision levels than new_lvl - justified_bvpos& curr = m_trail[i - 1]; - SASSERT(curr.m_justification->m_decision_level <= old_lvl); + justified_bvpos*& curr = m_trail[i - 1]; + SASSERT(curr->m_justification->m_decision_level <= old_lvl); - if (curr.m_justification->m_decision_level > new_lvl) { - clear_value(curr.get_pdd(), curr.get_idx()); + if (curr->m_justification->m_decision_level > new_lvl) { + get_bit_info(curr->get_pdd()).inc_unset(); // TODO: Suboptimal to query this again; Optimize! + clear_value(curr->get_pdd(), curr->get_idx()); if (last_to_keep != -1) std::swap(curr, m_trail[--last_to_keep]); } @@ -691,7 +744,7 @@ namespace polysat { return { least, most }; } - tbv_ref* fixed_bits::eval(solver& s, const pdd& p) { + const tbv_ref* fixed_bits::eval(solver& s, const pdd& p) { if (p.is_val() || p.is_var()) return get_tbv(p); @@ -711,7 +764,7 @@ namespace polysat { prod *= fac_pdd; if (!pre_prod.is_val() || !pre_prod.val().is_one()) { - bit_justication_mul::propagate(s, *this, prod, pre_prod, fac_pdd); + bit_justification_mul::propagate(s, *this, prod, pre_prod, fac_pdd); if (!m_consistent) return nullptr; } @@ -720,7 +773,7 @@ namespace polysat { sum += prod; if (!pre_sum.is_val() || !pre_sum.val().is_zero()) { - bit_justication_add::propagate(s, *this, sum, pre_sum, prod); + bit_justification_add::propagate(s, *this, sum, pre_sum, prod); if (!m_consistent) return nullptr; } @@ -734,7 +787,7 @@ namespace polysat { if (p.is_var() || p.is_val()) return; - vector sum_subterms; + vector sum_subterms; // TODO: optional? vector> prod_subterms; pdd zero = p.manager().zero(); pdd one = p.manager().one(); @@ -771,11 +824,11 @@ namespace polysat { pdd rhs = sum_subterms[i]; // a monomial for sure pdd lhs = sum_subterms[i - 1]; SASSERT(rhs.is_monomial()); - bit_justication_add::propagate(s, *this, current, lhs, rhs); + bit_justification_add::propagate(s, *this, current, lhs, rhs); current = rhs; - auto& prod = prod_subterms[i / 2]; + vector& prod = prod_subterms[i / 2]; for (unsigned j = prod.size() - 1; j > 1; j -= 2) { - bit_justication_mul::propagate(s, *this, current, prod[j], prod[j - 1]); + bit_justification_mul::propagate(s, *this, current, prod[j], prod[j - 1]); current = prod[j - 1]; } current = lhs; diff --git a/src/math/polysat/fixed_bits.h b/src/math/polysat/fixed_bits.h index 940f2a961..2a1a8c6e3 100644 --- a/src/math/polysat/fixed_bits.h +++ b/src/math/polysat/fixed_bits.h @@ -12,7 +12,8 @@ Abstract: --*/ #pragma once -#include "types.h" +#include "math/polysat/constraint.h" +#include "math/polysat/types.h" #include "util/hash.h" #include "util/optional.h" #include "util/tbv.h" @@ -23,7 +24,8 @@ namespace polysat { class solver; class constraint; class fixed_bits; - + class bitvec_info; + struct bvpos { optional m_pdd; unsigned m_bit_idx; @@ -58,15 +60,19 @@ namespace polysat { using bit_dependencies = vector; - class bit_justication { + class bit_justification { protected: - static bit_justication* get_other_justification(const fixed_bits& fixed, const pdd& p, unsigned idx); + static bit_justification* get_justification(fixed_bits& fixed, const pdd& p, unsigned idx); + static unsigned get_level(fixed_bits& fixed, const pdd& p, unsigned idx); static const tbv_ref* get_tbv(fixed_bits& fixed, const pdd& p); - static bool fix_bit(solver& s, fixed_bits& fixed, const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication** j); - static bool fix_bit(solver& s, fixed_bits& fixed, const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j); + + bit_justification() = default; public: - - unsigned m_decision_level; + + // if we reduce this value we would have to reduce some decision levels of justifications depending on it. + // However, we don't do this for now. (Should be still correct but generate weaker justifications) + // This value is used for comparing which of two justifications is better. Does not have to be 100% correct + unsigned m_decision_level = UINT32_MAX; // maybe better "weight"? virtual bool can_dealloc() { return true; } // we may not dealloc if the justification is used for multiple bits virtual bool has_constraint(constraint*& constr) { return false; } @@ -75,14 +81,16 @@ namespace polysat { // if multiple bits are justified by the same justification // All elements have to be in the same decision-level - class bit_justication_shared : public bit_justication { - bit_justication* m_justification; + class bit_justification_shared : public bit_justification { + bit_justification* m_justification; unsigned m_references = 0; public: - bit_justication_shared() = default; - bit_justication_shared(bit_justication* j) : m_justification(j), m_references(1) {} + bit_justification_shared(bit_justification* j) : m_justification(j), m_references(1) { + SASSERT(j); + m_decision_level = j->m_decision_level; + } - bit_justication* get_justification() { return m_justification; } + bit_justification* get_justification() { return m_justification; } virtual bool can_dealloc() { m_references = m_references == 0 ? 0 : m_references - 1; @@ -103,52 +111,50 @@ namespace polysat { void inc_ref() { m_references++; } }; - class bit_justication_constraint : public bit_justication { + class bit_justification_constraint : public bit_justification { constraint* m_constraint = nullptr; // A pdd might occur multiple times if more bits of it are relevant bit_dependencies m_dependencies; - bit_justication_constraint(constraint* c) : m_constraint(c) {} - bit_justication_constraint(constraint* c, const bit_dependencies& dep) : m_constraint(c), m_dependencies(dep) {} - bit_justication_constraint(constraint* c, bit_dependencies&& dep) : m_constraint(c), m_dependencies(dep) {} - + bit_justification_constraint(solver& s, constraint* c, bit_dependencies&& dep); + bit_justification_constraint(solver& s, constraint* c, const bit_dependencies& dep) : bit_justification_constraint(s, c, bit_dependencies(dep)) {} + bit_justification_constraint(solver& s, constraint* c) : bit_justification_constraint(s, c, bit_dependencies()) {} + public: - - bit_justication_constraint() = default; - + bool has_constraint(constraint*& constr) { constr = m_constraint; return true; } void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override; - static bit_justication_constraint* mk_assignment(constraint* c) { return alloc(bit_justication_constraint, c ); } - static bit_justication_constraint* mk_unary(constraint* c, bvpos v) { + static bit_justification_constraint* mk_assignment(solver& s, constraint* c) { return alloc(bit_justification_constraint, s, c); } + static bit_justification_constraint* mk_unary(solver& s, constraint* c, bvpos v) { bit_dependencies dep; dep.push_back(std::move(v)); - return alloc(bit_justication_constraint, c, std::move(dep)); + return alloc(bit_justification_constraint, s, c, std::move(dep)); } - static bit_justication_constraint* mk_binary(constraint* c, bvpos v1, bvpos v2) { + static bit_justification_constraint* mk_binary(solver& s, constraint* c, bvpos v1, bvpos v2) { bit_dependencies dep; dep.push_back(std::move(v1)); dep.push_back(std::move(v2)); - return alloc(bit_justication_constraint, c, std::move(dep)); + return alloc(bit_justification_constraint, s, c, std::move(dep)); } - static bit_justication_constraint* mk(constraint* c, const bit_dependencies& dep) { return alloc(bit_justication_constraint, c, dep); } + static bit_justification_constraint* mk(solver& s, constraint* c, const bit_dependencies& dep) { return alloc(bit_justification_constraint, s, c, dep); } // gives the highest bits such that they already enforce a value of "tbv" that is at least "val" - static bit_justication_constraint* mk_justify_at_least(constraint *c, const pdd& v, const tbv_ref& tbv, const rational& least); + static bit_justification_constraint* mk_justify_at_least(solver& s, constraint *c, const pdd& v, const tbv_ref& tbv, const rational& least); // similar to mk_justify_at_least: gives the highest bits such that they already enforce a value of "tbv" that is at most "val" - static bit_justication_constraint* mk_justify_at_most(constraint *c, const pdd& v, const tbv_ref& tbv, const rational& most); + static bit_justification_constraint* mk_justify_at_most(solver& s, constraint *c, const pdd& v, const tbv_ref& tbv, const rational& most); // a combination of mk_justify_at_least and mk_justify_at_most - static bit_justication_constraint* mk_justify_between(constraint *c, const pdd& v, const tbv_ref& tbv, rational least, rational most); + static bit_justification_constraint* mk_justify_between(solver& s, constraint *c, const pdd& v, const tbv_ref& tbv, rational least, rational most); }; // lazy generation of the justifications. Generating them eagerly can generate a huge overhead - class bit_justication_mul : public bit_justication { + class bit_justification_mul : public bit_justification { unsigned m_idx; optional m_p, m_q, m_r; @@ -156,10 +162,15 @@ namespace polysat { public: - bit_justication_mul() = default; - bit_justication_mul(unsigned idx, const pdd& p, const pdd& q) : m_idx(idx), m_p(p), m_q(q) {} - bit_justication_mul(unsigned idx, const pdd& p, const pdd& q, const pdd& r) : m_idx(idx), m_p(p), m_q(q), m_r(r) {} - + bit_justification_mul(unsigned idx, const pdd& p, const pdd& q, const pdd& r) : m_idx(idx), m_p(p), m_q(q), m_r(r) { + // we can also track the decision level but multiplications are unpleasant anyway. + // We prefer any other justification (Othw. take the max of all coefficients that influence the result) + m_decision_level = UINT32_MAX; + } + bit_justification_mul(unsigned idx, const pdd& p, const pdd& q) : m_idx(idx), m_p(p), m_q(q) { + m_decision_level = UINT32_MAX; + } + // propagates from p, q => r (forward) and r, p/q => q/p (backward) static void propagate(solver& s, fixed_bits& fixed, const pdd& r, const pdd &p, const pdd &q); void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override; @@ -167,91 +178,172 @@ namespace polysat { void get_dependencies_backward(fixed_bits& fixed, bit_dependencies& to_process, const tbv_ref& p_tbv, const tbv_ref& q_tbv, unsigned relevant_range); }; - class bit_justication_add : public bit_justication { + class bit_justification_add : public bit_justification { unsigned m_idx; optional m_c1, m_c2; public: - bit_justication_add() = default; - bit_justication_add(unsigned idx, const pdd& c1, const pdd& c2) : m_idx(idx), m_c1(c1), m_c2(c2) {} + bit_justification_add(unsigned lvl, unsigned idx, const pdd& c1, const pdd& c2) : m_idx(idx), m_c1(c1), m_c2(c2) { + m_decision_level = lvl; + } static void propagate(solver& s, fixed_bits& fixed, const pdd& r, const pdd& p, const pdd& q); void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override; }; struct justified_bvpos : public bvpos { - bit_justication* m_justification; - unsigned m_trail_pos; + bit_justification* m_justification; justified_bvpos() = default; - justified_bvpos(const pdd & pdd, unsigned idx, bit_justication* jstfc, unsigned int trail_pos) : - bvpos(pdd, idx), m_justification(jstfc), m_trail_pos(trail_pos) {} + justified_bvpos(const pdd & pdd, unsigned idx, bit_justification* jstfc) : + bvpos(pdd, idx), m_justification(jstfc) {} - justified_bvpos(const bvpos& pos, bit_justication* jstfc, unsigned int trail_pos) : - bvpos(pos), m_justification(jstfc), m_trail_pos(trail_pos) {} + justified_bvpos(const bvpos& pos, bit_justification* jstfc) : + bvpos(pos), m_justification(jstfc) {} + + void set(bit_justification* new_justification){ + if (m_justification && m_justification->can_dealloc()) + dealloc(m_justification); + m_justification = new_justification; + } + }; + + class bitvec_info { + tbv_ref* m_bits = nullptr; + justified_bvpos* m_justifications = nullptr; // do not alter this pointer (except setting it 0 for moving - we refer to it in trail) + unsigned m_unset = 0; // For constant pdds this value is completely ignored/not maintained + + public: + + bitvec_info() = default; + bitvec_info(tbv_ref* bits) : m_bits(bits), m_justifications(alloc_vect(bits->num_tbits())), m_unset(bits->num_tbits()) {} + bitvec_info(bitvec_info&& other) : m_bits(other.m_bits), m_justifications(other.m_justifications), m_unset(other.m_unset) { + other.m_bits = nullptr; + other.m_justifications = nullptr; + } + + bitvec_info& operator=(bitvec_info&& other) { + m_bits = other.m_bits; + m_justifications = other.m_justifications; + m_unset = other.m_unset; + + other.m_bits = nullptr; + other.m_justifications = nullptr; + return *this; + } + + ~bitvec_info() { + SASSERT((bool)m_bits == (bool)m_justifications); + if (!m_bits) + return; + + unsigned cnt = num_tbits(); + for (unsigned i = 0; i < cnt; i++) { + if (m_justifications[i].m_justification->can_dealloc()) + dealloc(m_justifications[i].m_justification); + } + dealloc_svect(m_justifications); + dealloc(m_bits); + } + + bool is_determined() const { + return m_unset == 0; + }; + + unsigned num_tbits() const { + return m_bits->num_tbits(); + } + + void inc_unset() { + SASSERT(m_unset < num_tbits()); + m_unset++; + } + + void dec_unset() { + SASSERT(m_unset > 0); + m_unset--; + } + + rational get_value() const { + SASSERT(is_determined()); + rational value(0); + unsigned cnt = num_tbits(); + for (unsigned i = cnt; i > 0; i--) { + SASSERT((*m_bits)[i - 1] == BIT_0 || (*m_bits)[i - 1] == BIT_1); + value *= 2; + value += (*m_bits)[i - 1] == BIT_1; + } + return value; + } + + void set_bit(unsigned idx, tbit v) { + SASSERT(v != BIT_x); // We don't use don't-cares + m_bits->manager().set(**m_bits, idx, v); + } + + tbit get_bit(unsigned idx) const { + return (*m_bits)[idx]; + } + + const tbv_ref* get_tbv() const { + return m_bits; + } + + justified_bvpos& justification(unsigned idx) { + return m_justifications[idx]; + } + + const justified_bvpos& justification(unsigned idx) const { + return m_justifications[idx]; + } }; class fixed_bits final { - friend bit_justication; + friend bit_justification; solver& m_solver; scoped_ptr_vector m_tbv_managers; - - using pdd_to_tbv_key = optional; - using pdd_to_tbv_eq = default_eq; - struct pdd_to_tbv_hash { - unsigned operator()(pdd_to_tbv_key const& args) const { - return args ? args->hash() : 0; + + using pdd_to_info_eq = default_eq>; + struct pdd_to_info_hash { + unsigned operator()(optional const& args) const { + return args->hash(); } }; - using pdd_to_tbv_map = map; - - using bvpos_to_justification_eq = default_eq; - struct bvpos_to_justification_hash { - unsigned operator()(bvpos const& args) const { - return combine_hash(args.get_pdd().hash(), args.get_idx()); - } - }; - using bvpos_to_justification_map = map; + using pdd_to_info_map = map, bitvec_info, pdd_to_info_hash, pdd_to_info_eq>; //vector> m_var_to_tbv; - pdd_to_tbv_map m_var_to_tbv; - bvpos_to_justification_map m_bvpos_to_justification; + pdd_to_info_map m_pdd_to_info; - svector m_trail; + svector m_trail; unsigned_vector m_trail_size; bool m_consistent = true; // in case evaluating results in a bit-conflict - tbv_manager& get_manager(const pdd& v); + tbv_manager& get_manager(const pdd& p); tbv_manager& get_manager(unsigned sz); - - clause_ref get_explanation(solver& s, bit_justication* j1, bit_justication* j2); - bool fix_value_core(const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j); - bool fix_bit(solver& s, const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j); + + bitvec_info& get_bit_info(const pdd& p); + + clause_ref get_explanation(solver& s, bit_justification** js, unsigned cnt, bool free, signed_constraint* consequence); + clause_ref get_explanation_assignment(solver& s, const pdd& p); + clause_ref get_explanation_conflict(solver& s, bit_justification* j1, bit_justification* j2); + clause_ref get_explanation_conflict(solver& s, bit_justification* j); // Conflict with constant + bool fix_value_core(const pdd& p, bitvec_info& info, unsigned idx, tbit val, bit_justification* j); void clear_value(const pdd& p, unsigned idx); - void replace_justification(const justified_bvpos& old_j, bit_justication* new_j); + void replace_justification(justified_bvpos& jstfc, bit_justification* new_j); void propagate_to_subterm(solver& s, const pdd& p); public: - fixed_bits(solver& s) : m_solver(s) {} - - ~fixed_bits() { - for (auto& tbv : m_var_to_tbv) - dealloc(tbv.m_value); - for (justified_bvpos& just : m_trail) { - if (just.m_justification->can_dealloc()) - dealloc(just.m_justification); - } - } - - tbv_ref* get_tbv(const pdd& p); + fixed_bits(solver& s) : m_solver(s) {} + + const tbv_ref* get_tbv(const pdd& p); // #count [min; max] static std::pair leading_zeros(const tbv_ref& ref); @@ -262,11 +354,12 @@ namespace polysat { tbit get_value(const pdd& p, unsigned idx); // More efficient than calling "eval" and accessing the returned tbv elements // call this function also if we already know that the correct value is written there. We might decrease the decision level (for "replay") - bool fix_value(solver& s, const pdd& p, unsigned idx, tbit val, bit_justication* j); + bool fix_bit(solver& s, const pdd& p, unsigned idx, tbit val, bit_justification** j, bool recursive); + bool fix_bit(solver& s, const pdd& p, unsigned idx, tbit val, bit_justification* j, bool recursive); void push(); void pop(unsigned pop_cnt = 1); - tbv_ref* eval(solver& s, const pdd& p); + const tbv_ref* eval(solver& s, const pdd& p); }; } diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 0cf0c92ba..a54f37b5c 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -362,12 +362,12 @@ namespace polysat { bool op_constraint::propagate_bits_shl(solver& s, bool is_positive) { // TODO: Implement: negative case - tbv_ref* p_val = s.m_fixed_bits.eval(s, m_p); - tbv_ref* q_val = s.m_fixed_bits.eval(s, m_q); - tbv_ref* r_val = s.m_fixed_bits.eval(s, m_r); + const tbv_ref& p_val = *s.m_fixed_bits.eval(s, m_p); + const tbv_ref& q_val = *s.m_fixed_bits.eval(s, m_q); + const tbv_ref& r_val = *s.m_fixed_bits.eval(s, m_r); unsigned sz = m_p.power_of_2(); - auto [shift_min, shift_max] = fixed_bits::min_max(*q_val); + auto [shift_min, shift_max] = fixed_bits::min_max(q_val); unsigned shift_min_u, shift_max_u; @@ -390,23 +390,23 @@ namespace polysat { // TODO: Improve performance; we can reuse the justifications from the previous iteration if (shift_min_u > 0) { for (unsigned i = 0; i < shift_min_u; i++) { - if (!s.m_fixed_bits.fix_value(s, m_r, i, BIT_0, bit_justication_constraint::mk_justify_at_least(this, m_q, *q_val, rational(i + 1)))) + if (!s.m_fixed_bits.fix_bit(s, m_r, i, BIT_0, bit_justification_constraint::mk_justify_at_least(s, this, m_q, q_val, rational(i + 1)), true)) return false; } } for (unsigned i = shift_min_u; i < sz; i++) { unsigned j = 0; - tbit val = (*p_val)[i - shift_min_u]; + tbit val = p_val[i - shift_min_u]; if (val == BIT_z) continue; for (; j < span; j++) { - if ((*p_val)[i - shift_min_u + 1] != val) + if (p_val[i - shift_min_u + 1] != val) break; } if (j == span) { // all elements we could shift there are equal. We can safely set this value // TODO: Relax. Sometimes we can reduce the span if further elements in q are set to the respective value - if (!s.m_fixed_bits.fix_value(s, m_r, i, val, bit_justication_constraint::mk_justify_between(this, m_q, *q_val, shift_min, shift_max))) + if (!s.m_fixed_bits.fix_bit(s, m_r, i, val, bit_justification_constraint::mk_justify_between(s, this, m_q, q_val, shift_min, shift_max), true)) return false; } } @@ -529,41 +529,41 @@ namespace polysat { bool op_constraint::propagate_bits_and(solver& s, bool is_positive) { // TODO: Implement: negative case LOG_H2("Bit-Propagating: " << m_r << " = (" << m_p << ") & (" << m_q << ")"); - tbv_ref* p_val = s.m_fixed_bits.eval(s, m_p); - tbv_ref* q_val = s.m_fixed_bits.eval(s, m_q); - tbv_ref* r_val = s.m_fixed_bits.eval(s, m_r); - LOG("p: " << m_p << " = " << *p_val); - LOG("q: " << m_q << " = " << *q_val); - LOG("r: " << m_r << " = " << *r_val); + const tbv_ref& p_val = *s.m_fixed_bits.eval(s, m_p); + const tbv_ref& q_val = *s.m_fixed_bits.eval(s, m_q); + const tbv_ref& r_val = *s.m_fixed_bits.eval(s, m_r); + LOG("p: " << m_p << " = " << p_val); + LOG("q: " << m_q << " = " << q_val); + LOG("r: " << m_r << " = " << r_val); unsigned sz = m_p.power_of_2(); for (unsigned i = 0; i < sz; i++) { - tbit bp = (*p_val)[i]; - tbit bq = (*q_val)[i]; - tbit br = (*r_val)[i]; + tbit bp = p_val[i]; + tbit bq = q_val[i]; + tbit br = r_val[i]; if (bp == BIT_0 || bq == BIT_0) { // TODO: In case both are 0 use the one with the lower decision-level and not necessarily p - if (!s.m_fixed_bits.fix_value(s, m_r, i, BIT_0, bit_justication_constraint::mk_unary(this, { bp == BIT_0 ? m_p : m_q, i }))) + if (!s.m_fixed_bits.fix_bit(s, m_r, i, BIT_0, bit_justification_constraint::mk_unary(s, this, { bp == BIT_0 ? m_p : m_q, i }), true)) return false; } else if (bp == BIT_1 && bq == BIT_1) { - if (!s.m_fixed_bits.fix_value(s, m_r, i, BIT_1, bit_justication_constraint::mk_binary(this, { m_p, i }, { m_q, i }))) + if (!s.m_fixed_bits.fix_bit(s, m_r, i, BIT_1, bit_justification_constraint::mk_binary(s, this, { m_p, i }, { m_q, i }), true)) return false; } else if (br == BIT_1) { - if (!s.m_fixed_bits.fix_value(s, m_p, i, BIT_1, bit_justication_constraint::mk_unary(this, { m_r, i }))) + if (!s.m_fixed_bits.fix_bit(s, m_p, i, BIT_1, bit_justification_constraint::mk_unary(s, this, { m_r, i }), true)) return false; - if (!s.m_fixed_bits.fix_value(s, m_q, i, BIT_1, bit_justication_constraint::mk_unary(this, { m_r, i }))) + if (!s.m_fixed_bits.fix_bit(s, m_q, i, BIT_1, bit_justification_constraint::mk_unary(s, this, { m_r, i }), true)) return false; } else if (br == BIT_0) { if (bp == BIT_1) { - if (!s.m_fixed_bits.fix_value(s, m_q, i, BIT_1, bit_justication_constraint::mk_binary(this, { m_p, i }, { m_r, i }))) + if (!s.m_fixed_bits.fix_bit(s, m_q, i, BIT_1, bit_justification_constraint::mk_binary(s, this, { m_p, i }, { m_r, i }), true)) return false; } else if (bq == BIT_1) { - if (!s.m_fixed_bits.fix_value(s, m_p, i, BIT_1, bit_justication_constraint::mk_binary(this, { m_q, i }, { m_r, i }))) + if (!s.m_fixed_bits.fix_bit(s, m_p, i, BIT_1, bit_justification_constraint::mk_binary(s, this, { m_q, i }, { m_r, i }), true)) return false; } } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index ff964020e..a9e384634 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -120,6 +120,7 @@ namespace polysat { friend class simplify_clause; friend class simplify; friend class fixed_bits; + friend class bit_justification_constraint; friend class restart; friend class explainer; friend class inference_engine; diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index e3ba7854d..0f951f7b1 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -262,18 +262,18 @@ namespace polysat { else e[0] = optional(-*(e[0])); SASSERT(e.size() == 2); - tbv_ref* lhs_val = s.m_fixed_bits.eval(s, *(e[0])); - tbv_ref* rhs_val = s.m_fixed_bits.eval(s, *(e[1])); - LOG("Bit-Propagating: " << *lhs_val << " = " << *rhs_val); - unsigned sz = lhs_val->num_tbits(); + const tbv_ref& lhs_val = *s.m_fixed_bits.eval(s, *(e[0])); + const tbv_ref& rhs_val = *s.m_fixed_bits.eval(s, *(e[1])); + LOG("Bit-Propagating: " << lhs_val << " = " << rhs_val); + unsigned sz = lhs_val.num_tbits(); for (unsigned i = 0; i < sz; i++) { // we propagate in both directions to get the least decision level - if ((*lhs_val)[i] != BIT_z) { - if (!s.m_fixed_bits.fix_value(s, *(e[1]), i, (*lhs_val)[i], bit_justication_constraint::mk_unary(this, { *(e[0]), i }))) + if (lhs_val[i] != BIT_z) { + if (!s.m_fixed_bits.fix_bit(s, *(e[1]), i, lhs_val[i], bit_justification_constraint::mk_unary(s, this, { *(e[0]), i }), true)) return false; } - if ((*rhs_val)[i] != BIT_z) { - if (!s.m_fixed_bits.fix_value(s, *(e[0]), i, (*rhs_val)[i], bit_justication_constraint::mk_unary(this, { *(e[1]), i }))) + if (rhs_val[i] != BIT_z) { + if (!s.m_fixed_bits.fix_bit(s, *(e[0]), i, rhs_val[i], bit_justification_constraint::mk_unary(s, this, { *(e[1]), i }), true)) return false; } } @@ -284,11 +284,11 @@ namespace polysat { pdd lhs = is_positive ? m_lhs : m_rhs; pdd rhs = is_positive ? m_rhs : m_lhs; - tbv_ref* lhs_val = s.m_fixed_bits.eval(s, lhs); - tbv_ref* rhs_val = s.m_fixed_bits.eval(s, rhs); - unsigned sz = lhs_val->num_tbits(); + const tbv_ref& lhs_val = *s.m_fixed_bits.eval(s, lhs); + const tbv_ref& rhs_val = *s.m_fixed_bits.eval(s, rhs); + unsigned sz = lhs_val.num_tbits(); - LOG("Bit-Propagating: " << lhs << " (" << *lhs_val << ") " << (is_positive ? "<= " : "< ") << rhs << " (" << *rhs_val << ")"); + LOG("Bit-Propagating: " << lhs << " (" << lhs_val << ") " << (is_positive ? "<= " : "< ") << rhs << " (" << rhs_val << ")"); // TODO: Propagate powers of 2 (lower bound) bool conflict = false; @@ -307,8 +307,8 @@ namespace polysat { }; unsigned i = sz; for (; i > (unsigned)!is_positive && !conflict; i--) { - tbit l = (*lhs_val)[i - 1]; - tbit r = (*rhs_val)[i - 1]; + tbit l = lhs_val[i - 1]; + tbit r = rhs_val[i - 1]; unsigned char action = action_lookup[l | (r << 2)]; switch (action) { @@ -319,13 +319,13 @@ namespace polysat { case 3: dep.push_back({ lhs, i - 1 }); LOG("Added dependency: pdd: " << lhs << " idx: " << i - 1); - conflict = !s.m_fixed_bits.fix_value(s, rhs, i - 1, BIT_1, bit_justication_constraint::mk(this, dep)); + conflict = !s.m_fixed_bits.fix_bit(s, rhs, i - 1, BIT_1, bit_justification_constraint::mk(s, this, dep), true); SASSERT((action != 3) == conflict); break; case 2: dep.push_back({ rhs, i - 1 }); LOG("Added dependency: pdd: " << rhs << " idx: " << i - 1); - conflict = !s.m_fixed_bits.fix_value(s, lhs, i - 1, BIT_0, bit_justication_constraint::mk(this, dep)); + conflict = !s.m_fixed_bits.fix_bit(s, lhs, i - 1, BIT_0, bit_justification_constraint::mk(s, this, dep), true); SASSERT(!conflict); break; default: @@ -334,13 +334,13 @@ namespace polysat { } if (!conflict && !is_positive && i == 1) { // Special treatment for lhs < rhs (note: we swapped lhs <-> rhs so this is really a less and not a greater) - conflict = !s.m_fixed_bits.fix_value(s, lhs, 0, BIT_0, bit_justication_constraint::mk(this, dep)); + conflict = !s.m_fixed_bits.fix_bit(s, lhs, 0, BIT_0, bit_justification_constraint::mk(s, this, dep), true); if (!conflict) - conflict = !s.m_fixed_bits.fix_value(s, rhs, 0, BIT_1, bit_justication_constraint::mk(this, dep)); + conflict = !s.m_fixed_bits.fix_bit(s, rhs, 0, BIT_1, bit_justification_constraint::mk(s, this, dep), true); } SASSERT( - is_positive && conflict == (fixed_bits::min_max(*lhs_val).first > fixed_bits::min_max(*rhs_val).second) || - !is_positive && conflict == (fixed_bits::min_max(*lhs_val).second <= fixed_bits::min_max(*rhs_val).first) + is_positive && conflict == (fixed_bits::min_max(lhs_val).first > fixed_bits::min_max(rhs_val).second) || + !is_positive && conflict == (fixed_bits::min_max(lhs_val).second <= fixed_bits::min_max(rhs_val).first) ); return !conflict; } diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 366679895..efcc806f2 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -2036,7 +2036,7 @@ void tst_polysat() { return; #endif - // If non-empty, only run tests whose name c9ontains the run_filter + // If non-empty, only run tests whose name contains the run_filter run_filter = ""; test_max_conflicts = 20; From 4b8577eaa299979e4f5f0b4a5b6268a34c514ad2 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer Date: Tue, 27 Dec 2022 08:47:27 +0100 Subject: [PATCH 2/2] Reverted unintended changes --- src/math/polynomial/polynomial.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 5d7d00afe..b85ac1cf5 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -4398,8 +4398,8 @@ namespace polynomial { TRACE("gcd_calls", tout << "gcd\nu: "; u->display(tout, m_manager); tout << "\nv: "; v->display(tout, m_manager); tout << "\n";); TRACE("polynomial_gcd", tout << "gcd\nu: "; u->display(tout, m_manager); tout << "\nv: "; v->display(tout, m_manager); - tout << "\nis_zero(u): " << is_zero(u) << ", is_determined(u): " << is_const(u) << "\n"; - tout << "is_zero(v): " << is_zero(v) << ", is_determined(v): " << is_const(v) << "\n"; + tout << "\nis_zero(u): " << is_zero(u) << ", is_const(u): " << is_const(u) << "\n"; + tout << "is_zero(v): " << is_zero(v) << ", is_const(v): " << is_const(v) << "\n"; tout << "modular: " << m().modular() << "\n";); if (is_zero(u)) { r = const_cast(v);