mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

Several changes:

Browse source 
- Extend fixed-bit FI to both directions
- really randomized restart
- MSB for fixed-bits
- Forward propagation (band, lshift, rshift) with good justifications (strengthen during saturation)
This commit is contained in:
Clemens Eisenhofer 2023-03-07 15:21:14 +01:00
parent 5a8c0ce9c0
commit 5b35450891
18 changed files with 539 additions and 1588 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/CMakeLists.txt
View file

@ -8,7 +8,6 @@ z3_add_component(polysat
constraint.cpp
constraint_manager.cpp
eq_explain.cpp
fixed_bits.cpp
forbidden_intervals.cpp
inference_logger.cpp
justification.cpp

1
src/math/polysat/constraint.h
View file

@ -83,7 +83,6 @@ namespace polysat {
bool is_currently_false(solver const& s, bool is_positive) const { return is_currently_true(s, !is_positive); }
virtual void narrow(solver& s, bool is_positive, bool first) = 0;
virtual bool propagate_bits(solver& s, bool is_positive) { return true; }
/**
* If possible, produce a lemma that contradicts the given assignment.
* This method should not modify the solver's search state.

837
src/math/polysat/fixed_bits.cpp
View file

@ -1,837 +0,0 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
fixed_bits
Abstract:
Associates every pdd with the set of already fixed bits and justifications for this
--*/
#include "math/polysat/fixed_bits.h"
#include "math/polysat/solver.h"
namespace polysat {
bit_justification* bit_justification::get_justification(fixed_bits& fixed, const pdd& p, unsigned idx) {
return fixed.get_bit_info(p).justification(idx).m_justification;
}
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);
}
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;
}
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;
}
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_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_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_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());
most = power(rational(2), tbv.num_tbits()) - most;
bit_dependencies dep;
for (unsigned i = tbv.num_tbits(); i > 0; i--) {
tbit b = tbv[i];
if (b == BIT_0 || b == BIT_1) {
(b == BIT_0 ? most : least) -= power(rational(2), i - 1);
dep.push_back({ v, i });
}
if (most.is_nonpos() && least.is_nonpos())
return alloc(bit_justification_constraint, s, c, std::move(dep));
}
SASSERT(most.is_pos() || least.is_pos());
VERIFY(false); // we assume that the possible values are indeed in [least; most]
return nullptr;
}
// multiplication: (1*p0 + 2*p1 + 4*p2 + 8*p3 + ...) * (1*q0 + 2*q1 + 4*q2 + 8*q3 + ...) =
// = 1 * (p0 q0) + 2 * (p0 q1 + p1 q0) + 4 * (p0 q2 + p1 q1 + p2 q0) + 8 * (p0 q3 + p1 q2 + p2 q1 + p3 q0) + ...
// that means
// r0 = (p0 q0)
// 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_justification_mul::propagate(solver& s, fixed_bits& fixed, const pdd& r, const pdd &p, const pdd &q) {
LOG_H2("Bit-Propagating: " << r << " = (" << p << ") * (" << q << ")");
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);
auto& m = r_tbv.manager();
// TODO: maybe propagate the bits only until the first "don't know" and as well for the leading "0"s [The bits in-between are rare and hard to compute]
unsigned min_val = 0; // The value of the current bit assuming all unknown bits are 0
unsigned max_val = 0; // The value of the current bit assuming all unknown bits are 1
unsigned highest_overflow_idx = -1; // The index which could result in the highest overflow (Used for backward propagation. Which previous bit-index could have the highest overflow to the current bit?)
unsigned highest_overflow_val = 0; // The respective value
bool highest_overflow_precise = false; // True if the highest overflow is still precise after all divisions by 2 (We can only use those for backward propagation. If it is not a power of 2 we don't know which values to set.)
// Forward propagation
// Example 1:
// r4 = (0 q3 + 1 1 + 0 q1 + 0 q0) + (1 1 + 0 q1 + 1 1) / 2
// min_val = 2 = 2 / 2 + 1; max_val = 2 = 2 / 2 + 1 and (0 q3 + 1 1 + 0 q1 + 0 q0) + (1 1 + 0 q1 + 1 1) / 2 = 2 we conclude r3 = 0 (and min_val = max_val := min_val / 2 + 2 / 2)
//
// Example 2:
// r4 = (0 q3 + 1 1 + 0 q1 + 0 q0) + (1 1 + 0 q1 + 1 q0) / 2
// min_val = 1 = 1 + 1 / 2; max_val = 2 = 1 + 2 / 2. We cannot propagate to r4 as we don't know the value of the overflow
//
// Example 3:
// r4 = (0 q3 + p1 1 + 0 q1 + 0 q0) + (1 1 + 0 q1 + 1 1) / 2
// min_val = 1 = 0 + 2 / 2; v = 2 = 1 + 2 / 2. We cannot propagate to r4 as we don't know the precise value
// Backward propagation
// Example 1:
// 0 = r3 = (1 1 + 0 q2 + 1 q1 + p3 0) + (0 q2 + 1 1 + 1 1) / 2
// highest_overflow_idx = 3 [meaning r3]; min_val = 2 = 1 + 2 / 2; max_val = 3 = 2 + 2 / 2. We can propagate q1 = 0 as min_val == max_val - 1
//
// Example 2:
// 0 = r3 = (1 1 + 0 q2 + 0 q1 + p3 0) + (0 q2 + p1 1 + p2 1) / 2
// highest_overflow_idx = 2; highest_overflow_precise = true; min_val = 1; max_val = 2. We can propagate p2 = p1 = 1 in r2 as min_val == max_val - 1 and we know that we can make all [highest_overflow_precise == true] undetermined products in r2 true
//
// Example 3:
// 0 = r3 = (1 1 + 0 q2 + 0 q1 + p3 0) + (1 q2 + 1 1 + p2 1) / 2
// highest_overflow_idx = 2; highest_overflow_precise = false; min_val = 1; max_val = 2. We can not propagate p2 = 1 or q2 = 1 in r2 as we don't know which [highest_overflow_precise == false i.e., 3 is not divisible by 2]
//
// Example 4:
// 0 = r3 = (1 1 + 0 q2 + 0 q1 + p3 0) + (p0 q2 + p1 1 + 0 1) / 2
// highest_overflow_idx = 2; highest_overflow_precise = true; min_val = 1; max_val = 2. We can propagate p1 = 1 but not p0 = 1 or q2 = 1 as we don't know which
//
// In all cases cases min_val == max_val after backward propagation [max_val = min_val if assigned to 0; min_val = max_val if assigned to 1]
// TODO: Check: Is the performance too worse? It is O(k^3) in the worst case...
for (unsigned i = 0; i < m.num_tbits(); i++) {
unsigned current_min_val = 0, current_max_val = 0;
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) {
current_min_val++; // we get two 1
current_max_val++;
}
else if (bit1 != BIT_0 && bit2 != BIT_0)
current_max_val++; // we could get two 1
}
if (max_val >= highest_overflow_val) {
highest_overflow_val = max_val;
highest_overflow_idx = i;
highest_overflow_precise = true;
}
min_val += current_min_val;
max_val += current_max_val;
if (min_val == max_val) {
// We know the value of this bit
// forward propagation
// this might add a conflict if the value is already set to another value
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) {
// backward propagation
// this cannot add a conflict. However, conflicts are already captured in the forward propagation case
tbit set;
if ((min_val & 1) == (r_tbv[i] == BIT_0 ? 0 : 1)) {
set = BIT_0;
max_val = min_val;
}
else {
set = BIT_1;
min_val = max_val;
}
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_justification_shared* j = nullptr;
unsigned_vector set_bits;
#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];
tbit bit2 = q_tbv[y];
if (set == BIT_0 && bit1 != bit2) {
// Sets: (1, z), (z, 1), (0, 1), (1, 0) [the cases with two constants are used for minimizing decision levels]
// 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 (!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 (!fixed.fix_bit(s, p, x, BIT_0, SHARED_JUSTIFICATION, false)) {
VERIFY(false);
}
set_bits.push_back(x << 1 | 0);
}
}
else if (set == BIT_1 && bit1 != BIT_0 && bit2 != BIT_0) {
// 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 (!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 (!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 (!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);
set_bits.push_back(x << 1 | 0);
}
}
}
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_justification_mul*)j->get_justification())->m_bit_indexes = set_bits;
}
}
}
// Subtract one; shift this to the next higher bit as "carry values"
min_val >>= 1;
max_val >>= 1;
highest_overflow_precise &= (highest_overflow_val & 1) == 0;
highest_overflow_val >>= 1;
}
}
// collect all bits that effect the given bit. These might be quite a lot
// We need to know how many previous bits are relevant
// r0 = (p0 q0) ... 0 overflow candidates
// r1 = (p0 q1 + p1 q0) + (p0 q0) / 2 = (p0 q1 + p1 q0) ... 0 overflow candidates
// 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 ... 1 overflow candidates
// ...
// r5 = ([6]) + ([5]) / 2 + ([4]) / 4 + ([3]) / 8 + ([2]) / 16 + ([1]) / 32 = ([6]) + ([5]) / 2 + ([4]) / 4 ... 2 overflow candidates
// ...
// r12 = ([11]) + ([10]) / 2 + ([9]) / 4 + ([8]) / 8 ... 3 overflow candidates
// ...
// r21 = ([20]) + ([19]) / 2 + ([18]) / 4 + ([17]) / 8 + ([16]) / 16 ... 4 overflow candidates
// ...
// r38 = ([37]) + ([36]) / 2 + ([35]) / 4 + ([34]) / 8 + ([33]) / 16 + ([32]) / 32 ... 5 overflow candidates
// ...
// r71 = ... 6 overflow candidates
// ...
// 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_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;
else
relevant_range = log2(m_idx - (log2(m_idx) + 1));
const tbv_ref& p_tbv = *get_tbv(fixed, *m_p);
const tbv_ref& q_tbv = *get_tbv(fixed, *m_q);
if (m_r)
get_dependencies_forward(fixed, to_process, p_tbv, q_tbv, relevant_range);
else
get_dependencies_backward(fixed, to_process, p_tbv, q_tbv, 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_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_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process);
else if (bit2 == BIT_0)
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?
VERIFY(false);
}
}
}
}
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++) {
for (unsigned x = 0, y = i; x <= i; x++, y--) {
unsigned i_p = x << 1 | 0;
unsigned i_q = y << 1 | 1;
// the list is ordered in the same way we iterate now through it so we just look at the first elements
unsigned next1 = set_idx >= m_bit_indexes.size() ? -1 : m_bit_indexes[set_idx];
unsigned next2 = set_idx + 1 >= m_bit_indexes.size() ? -1 : m_bit_indexes[set_idx + 1];
bool p_in_set = false, q_in_set =false;
if (i_p == next1 || i_p == next2) {
set_idx++;
p_in_set = true;
}
else if (i_q == next1 || i_q == next2) {
set_idx++;
q_in_set = true;
}
tbit bit1 = p_tbv[x];
tbit bit2 = q_tbv[y];
// TODO: Check once more
if (bit1 == BIT_1 && bit2 == BIT_1) {
if (!p_in_set)
get_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process);
if (!q_in_set)
get_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process);
}
else if (bit1 == BIT_0) {
if (!p_in_set)
get_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process);
else if (!q_in_set)
get_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process);
}
else if (bit2 == BIT_0 && !q_in_set) {
if (!q_in_set)
get_justification(fixed, *m_q, y)->get_dependencies(fixed, to_process);
else if (!p_in_set)
get_justification(fixed, *m_p, x)->get_dependencies(fixed, to_process);
}
else {
// unlike in the forward case this can happen
}
}
}
}
// similar to multiplying but far simpler/faster (only the direct predecessor might overflow)
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
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);
auto& m = r_tbv.manager();
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_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;
}
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_justification_add::get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) {
if (m_c1->power_of_2() > 1 && m_idx > 0) {
//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_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);
SASSERT(tbv1[m_idx] != BIT_z && tbv2[m_idx] != BIT_z);
);
}
tbv_manager& fixed_bits::get_manager(unsigned sz){
m_tbv_managers.reserve(sz + 1);
if (!m_tbv_managers[sz])
m_tbv_managers.set(sz, alloc(tbv_manager, sz));
return *m_tbv_managers[sz];
}
tbv_manager& fixed_bits::get_manager(const pdd& p) {
return get_manager(p.power_of_2());
}
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() <= p) {
m_var_to_tbv.reserve(v + 1);
auto& manager = get_manager(sz);
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(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(p)];*/
}
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 (free && (X)->can_dealloc()) { dealloc(X); } } while (false)
clause_builder conflict(s);
conflict.set_redundant(true);
auto insert_constraint = [&conflict, &s](bit_justification* j) {
constraint* constr;
if (!j->has_constraint(constr))
return;
SASSERT(constr);
if (constr->has_bvar()) {
SASSERT(s.m_bvars.is_assigned(constr->bvar()));
// add negated
conflict.insert(signed_constraint(constr, s.m_bvars.value(constr->bvar()) != l_true));
}
};
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();
if (curr.m_pdd->is_val()) {
to_process.pop_back();
continue; // We don't need an explanation for bits of constants
}
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<bit_justification*> 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, 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);
}
if (val == BIT_z) // just ignore this case
return false;
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
// 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(justfc, j); // the new justification is better. Let's take it
return true;
}
if (curr_val == BIT_z) {
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));
m_consistent = false;
return false;
}
// return: consistent?
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
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;
}
if (!m_consistent) {
LOG("Adding conflict on bit " << idx << " on pdd " << p);
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);
*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) {
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(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 (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() {
#if 0
m_trail_size.push_back(m_trail.size());
#endif
}
void fixed_bits::pop(unsigned pop_cnt) {
#if 0
SASSERT(pop_cnt > 0);
unsigned old_lvl = m_trail_size.size();
unsigned new_lvl = old_lvl - pop_cnt;
SASSERT(pop_cnt <= old_lvl);
unsigned prev_cnt = m_trail_size[new_lvl];
m_trail_size.resize(new_lvl);
unsigned last_to_keep = -1;
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);
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]);
}
else {
if (last_to_keep == -1)
last_to_keep = i;
}
}
if (last_to_keep == -1)
m_trail.resize(prev_cnt);
else
m_trail.resize(last_to_keep);
#endif
}
#define COUNT(DOWN, TO_COUNT) \
do { \
unsigned sz = ref.num_tbits(); \
unsigned least = 0; \
for (; least < sz; least++) { \
if (ref[((DOWN) ? sz - least - 1 : least)] != (TO_COUNT)) \
break; \
} \
if (least == sz) \
return { sz, sz }; /* For sure TO_COUNT */ \
unsigned most = least; \
for (; most < sz; most++) { \
if (ref[((DOWN) ? sz - most - 1 : most)] == ((TO_COUNT) == BIT_0 ? BIT_1 : BIT_0)) \
break; \
} \
return { least, most }; /* There are between "least" and "most" leading/trailing TO_COUNT */ \
} while(false)
std::pair<unsigned, unsigned> fixed_bits::leading_zeros(const tbv_ref& ref) { COUNT(false, BIT_0); }
std::pair<unsigned, unsigned> fixed_bits::trailing_zeros(const tbv_ref& ref) { COUNT(true, BIT_0); }
std::pair<unsigned, unsigned> fixed_bits::leading_ones(const tbv_ref& ref) { COUNT(false, BIT_1); }
std::pair<unsigned, unsigned> fixed_bits::trailing_ones(const tbv_ref& ref) { COUNT(true, BIT_1); }
std::pair<rational, rational> fixed_bits::min_max(const tbv_ref& ref) {
unsigned sz = ref.num_tbits();
rational least(0);
rational most(0);
for (unsigned i = 0; i < sz; i++) {
tbit v = ref[i];
least *= 2;
most *= 2;
if (v == BIT_1) {
least++;
most++;
}
else if (v == BIT_z)
most++;
}
return { least, most };
}
const tbv_ref* fixed_bits::eval(solver& s, const pdd& p) {
if (p.is_val() || p.is_var())
return get_tbv(p);
pdd zero = p.manager().zero();
pdd one = p.manager().one();
pdd sum = zero;
for (const dd::pdd_monomial& n : p) {
SASSERT(!n.coeff.is_zero());
pdd prod = p.manager().mk_val(n.coeff);
for (pvar fac : n.vars) {
pdd fac_pdd = s.var(fac);
pdd pre_prod = prod;
prod *= fac_pdd;
if (!pre_prod.is_val() || !pre_prod.val().is_one()) {
bit_justification_mul::propagate(s, *this, prod, pre_prod, fac_pdd);
if (!m_consistent)
return nullptr;
}
}
pdd pre_sum = sum;
sum += prod;
if (!pre_sum.is_val() || !pre_sum.val().is_zero()) {
bit_justification_add::propagate(s, *this, sum, pre_sum, prod);
if (!m_consistent)
return nullptr;
}
}
return get_tbv(sum);
}
//propagate to subterms of the polynomial/pdd
void fixed_bits::propagate_to_subterm(solver& s, const pdd& p) {
// we assume the tbv of p was already assigned and there was no conflict
if (p.is_var() || p.is_val())
return;
vector<pdd> sum_subterms; // TODO: optional?
vector<vector<pdd>> prod_subterms;
pdd zero = p.manager().zero();
pdd one = p.manager().one();
pdd sum = zero;
for (const dd::pdd_monomial& n : p) {
SASSERT(!n.coeff.is_zero());
pdd prod = p.manager().mk_val(n.coeff);
prod_subterms.push_back(vector<pdd>());
// TODO: Maybe process the coefficient first as we have the most information there
// (however, we cannot really revert the order as we used the coefficient first for forward propagation)
if (n.coeff != 1)
prod_subterms.back().push_back(prod);
for (pvar fac : n.vars) {
pdd fac_pdd = s.var(fac);
prod *= fac_pdd;
prod_subterms.back().push_back(prod);
prod_subterms.back().push_back(fac_pdd);
}
sum += prod;
sum_subterms.push_back(sum);
sum_subterms.push_back(prod);
}
SASSERT(sum_subterms[0] == sum_subterms[1] && sum_subterms.size() % 2 == 1);
SASSERT(2 * prod_subterms.size() == sum_subterms.size());
pdd current = p;
for (unsigned i = sum_subterms.size() - 1; i > 1; i -= 2) {
pdd rhs = sum_subterms[i]; // a monomial for sure
pdd lhs = sum_subterms[i - 1];
SASSERT(rhs.is_monomial());
bit_justification_add::propagate(s, *this, current, lhs, rhs);
current = rhs;
vector<pdd>& prod = prod_subterms[i / 2];
for (unsigned j = prod.size() - 1; j > 1; j -= 2) {
bit_justification_mul::propagate(s, *this, current, prod[j], prod[j - 1]);
current = prod[j - 1];
}
current = lhs;
}
}
}

366
src/math/polysat/fixed_bits.h
View file

@ -1,366 +0,0 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
fixed_bits
Abstract:
Associates every pdd with the set of already fixed bits and justifications for this
--*/
#pragma once
#include "math/polysat/constraint.h"
#include "math/polysat/types.h"
#include "util/hash.h"
#include "util/optional.h"
#include "util/tbv.h"
namespace polysat {
class solver;
class constraint;
class fixed_bits;
class bitvec_info;
struct bvpos {
optional<pdd> m_pdd;
unsigned m_bit_idx;
public:
bvpos() : m_pdd(optional<dd::pdd>::undef()), m_bit_idx(0) {}
bvpos(const bvpos& v) = default;
bvpos(bvpos&& v) = default;
bvpos(const pdd& pdd, unsigned bit_idx) : m_pdd(pdd), m_bit_idx(bit_idx) {}
bool operator==(const bvpos& other) const {
return m_pdd == other.m_pdd && m_bit_idx == other.m_bit_idx;
}
bvpos& operator=(bvpos&& other) {
m_pdd = other.m_pdd;
m_bit_idx = other.m_bit_idx;
return *this;
}
bvpos& operator=(bvpos& other) {
m_pdd = other.m_pdd;
m_bit_idx = other.m_bit_idx;
return *this;
}
unsigned get_idx() const { return m_bit_idx; }
const pdd& get_pdd() const { return *m_pdd; }
};
using bit_dependencies = vector<bvpos>;
class bit_justification {
protected:
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);
bit_justification() = default;
public:
virtual ~bit_justification() = default;
// 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; }
virtual void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) = 0; // returns if element may be deallocated after call (usually true)
};
// if multiple bits are justified by the same justification
// All elements have to be in the same decision-level
class bit_justification_shared : public bit_justification {
bit_justification* m_justification;
unsigned m_references = 0;
public:
bit_justification_shared(bit_justification* j) : m_justification(j), m_references(1) {
SASSERT(j);
m_decision_level = j->m_decision_level;
}
bit_justification* get_justification() { return m_justification; }
bool can_dealloc() override {
m_references = m_references == 0 ? 0 : m_references - 1;
if (m_references != 0)
return false;
if (m_justification->can_dealloc()) {
dealloc(m_justification);
m_justification = nullptr;
}
return true;
}
void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override {
SASSERT(m_justification);
m_justification->get_dependencies(fixed, to_process);
}
void inc_ref() { m_references++; }
};
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_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:
bool has_constraint(constraint*& constr) override {
constr = m_constraint;
return true;
}
void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override;
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_justification_constraint, s, c, std::move(dep));
}
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_justification_constraint, s, c, std::move(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_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_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_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_justification_mul : public bit_justification {
unsigned m_idx;
optional<pdd> m_p, m_q, m_r;
unsigned_vector m_bit_indexes;
public:
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;
void get_dependencies_forward(fixed_bits &fixed, bit_dependencies &to_process, const tbv_ref& p_tbv, const tbv_ref& q_tbv, unsigned relevant_range);
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_justification_add : public bit_justification {
unsigned m_idx;
optional<pdd> m_c1, m_c2;
public:
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_justification* m_justification;
justified_bvpos() = default;
justified_bvpos(const pdd & pdd, unsigned idx, bit_justification* jstfc) :
bvpos(pdd, idx), m_justification(jstfc) {}
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<justified_bvpos>(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_justification;
solver& m_solver;
scoped_ptr_vector<tbv_manager> m_tbv_managers;
using pdd_to_info_eq = default_eq<optional<pdd>>;
struct pdd_to_info_hash {
unsigned operator()(optional<pdd> const& args) const {
return args->hash();
}
};
using pdd_to_info_map = map<optional<pdd>, bitvec_info, pdd_to_info_hash, pdd_to_info_eq>;
//vector<optional<tbv_ref>> m_var_to_tbv;
pdd_to_info_map m_pdd_to_info;
svector<justified_bvpos*> 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& p);
tbv_manager& get_manager(unsigned sz);
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(justified_bvpos& jstfc, bit_justification* new_j);
void propagate_to_subterm(solver& s, const pdd& p);
public:
fixed_bits(solver& s) : m_solver(s) {}
const tbv_ref* get_tbv(const pdd& p);
// #count [min; max]
static std::pair<unsigned, unsigned> leading_zeros(const tbv_ref& ref);
static std::pair<unsigned, unsigned> trailing_zeros(const tbv_ref& ref);
static std::pair<unsigned, unsigned> leading_ones(const tbv_ref& ref);
static std::pair<unsigned, unsigned> trailing_ones(const tbv_ref& ref);
static std::pair<rational, rational> min_max(const tbv_ref& ref);
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_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);
const tbv_ref* eval(solver& s, const pdd& p);
};
}

154
src/math/polysat/op_constraint.cpp
View file

@ -130,11 +130,6 @@ namespace polysat {
if (first)
activate(s);
#if 0
if (!propagate_bits(s, is_positive))
return; // conflict
#endif
if (clause_ref lemma = produce_lemma(s, s.get_assignment()))
s.add_clause(*lemma);
@ -142,24 +137,6 @@ namespace polysat {
s.set_conflict(signed_constraint(this, is_positive));
}
bool op_constraint::propagate_bits(solver& s, bool is_positive) {
switch (m_op) {
case code::lshr_op:
return propagate_bits_lshr(s, is_positive);
case code::shl_op:
return propagate_bits_shl(s, is_positive);
case code::and_op:
return propagate_bits_and(s, is_positive);
case code::inv_op:
case code::udiv_op:
case code::urem_op:
return false;
default:
NOT_IMPLEMENTED_YET();
return false;
}
}
/**
* Produce lemmas that contradict the given assignment.
*
@ -278,17 +255,21 @@ namespace polysat {
}
else {
// forward propagation
/*SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
LOG(p() << " = " << pv << " and " << q() << " = " << qv << " yields [>>] " << r() << " = " << (qv.val().is_unsigned() ? machine_div(pv.val(), rational::power_of_two(qv.val().get_unsigned())) : rational::zero()));
if (qv.is_val() && !rv.is_val()) {
const rational& qr = qv.val();
if (qr >= m.power_of_2())
if (qr >= N)
return s.mk_clause(~lshr, ~s.ule(m.mk_val(m.power_of_2()), q()), s.eq(r()), true);
if (rv.is_val()) {
const rational& pr = pv.val();
return s.mk_clause(~lshr, ~s.eq(p(), m.mk_val(pr)), ~s.eq(q(), m.mk_val(qr)), s.eq(r(), m.mk_val(machine_div(pr, rational::power_of_two(qr.get_unsigned())))), true);
return s.mk_clause(~lshr, ~s.eq(p(), m.mk_val(pr)), ~s.eq(q(), m.mk_val(qr)), s.eq(r(), m.mk_val(
qr.is_unsigned()
? machine_div(pr, rational::power_of_two(qr.get_unsigned()))
: rational::zero())), true);
}
}*/
}
}
return {};
}
@ -313,12 +294,6 @@ namespace polysat {
return l_undef;
}
bool op_constraint::propagate_bits_lshr(solver& s, bool is_positive) {
// TODO: Implement: copy from the left shift
// TODO: Implement: negative case
return true;
}
/**
* Enforce axioms for constraint: r == p << q
*
@ -362,17 +337,18 @@ namespace polysat {
}
else {
// forward propagation
/*SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
LOG(p() << " = " << pv << " and " << q() << " = " << qv << " yields [<<] " << r() << " = " << (qv.val().is_unsigned() ? rational::power_of_two(qv.val().get_unsigned()) * pv.val() : rational::zero()));
if (qv.is_val() && !rv.is_val()) {
const rational& qr = qv.val();
if (qr >= m.power_of_2())
if (qr >= N)
return s.mk_clause(~shl, ~s.ule(m.mk_val(m.power_of_2()), q()), s.eq(r()), true);
if (rv.is_val()) {
const rational& pr = pv.val();
return s.mk_clause(~shl, ~s.eq(p(), m.mk_val(pr)), ~s.eq(q(), m.mk_val(qr)), s.eq(r(), m.mk_val(rational::power_of_two(qr.get_unsigned()) * pr)), true);
}
}*/
}
}
return {};
}
@ -400,59 +376,6 @@ namespace polysat {
return l_undef;
}
bool op_constraint::propagate_bits_shl(solver& s, bool is_positive) {
// TODO: Implement: negative case
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);
unsigned shift_min_u, shift_max_u;
if (!shift_min.is_unsigned() || shift_min.get_unsigned() > sz)
shift_min_u = sz;
else
shift_min_u = shift_min.get_unsigned();
if (!shift_max.is_unsigned() || shift_max.get_unsigned() > sz)
shift_max_u = sz;
else
shift_max_u = shift_max.get_unsigned();
SASSERT(shift_max_u <= sz);
SASSERT(shift_min_u <= shift_max_u);
unsigned span = shift_max_u - shift_min_u;
// Shift by at the value we know q to be at least
// 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_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];
if (val == BIT_z)
continue;
for (; j < span; j++) {
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_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;
}
}
return true;
}
void op_constraint::activate_and(solver& s) {
auto x = p(), y = q();
if (x.is_val())
@ -497,7 +420,7 @@ namespace polysat {
auto qv = a.apply_to(q());
auto rv = a.apply_to(r());
signed_constraint const andc(this, true);
signed_constraint const andc(this, true); // op_constraints are always true
// r <= p
if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
@ -559,9 +482,11 @@ namespace polysat {
if (qv.is_zero() && !rv.is_zero()) // rv not necessarily fully evaluated
return s.mk_clause(~andc, s.ule(r(), q()), true);
// p = a && q = b ==> r = a & b
/*if (pv.is_val() && qv.is_val() && !rv.is_val()) {
if (pv.is_val() && qv.is_val() && !rv.is_val()) {
// Just assign by this very weak justification. It will be strengthened in saturation in case of a conflict
LOG(p() << " = " << pv << " and " << q() << " = " << qv << " yields [band] " << r() << " = " << bitwise_and(pv.val(), qv.val()));
return s.mk_clause(~andc, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), bitwise_and(pv.val(), qv.val())), true);
}*/
}
return {};
}
@ -577,51 +502,6 @@ namespace polysat {
return l_undef;
}
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 << ")");
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];
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_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_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_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_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_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_bit(s, m_p, i, BIT_1, bit_justification_constraint::mk_binary(s, this, { m_q, i }, { m_r, i }), true))
return false;
}
}
}
return true;
}
/**
* Produce lemmas for constraint: r == inv p
* p = 0 ==> r = 0

5
src/math/polysat/op_constraint.h
View file

@ -60,15 +60,12 @@ namespace polysat {
clause_ref lemma_lshr(solver& s, assignment const& a);
static lbool eval_lshr(pdd const& p, pdd const& q, pdd const& r);
bool propagate_bits_lshr(solver& s, bool is_positive);
clause_ref lemma_shl(solver& s, assignment const& a);
static lbool eval_shl(pdd const& p, pdd const& q, pdd const& r);
bool propagate_bits_shl(solver& s, bool is_positive);
clause_ref lemma_and(solver& s, assignment const& a);
static lbool eval_and(pdd const& p, pdd const& q, pdd const& r);
bool propagate_bits_and(solver& s, bool is_positive);
clause_ref lemma_inv(solver& s, assignment const& a);
static lbool eval_inv(pdd const& p, pdd const& r);
@ -91,12 +88,12 @@ namespace polysat {
pdd const& p() const { return m_p; }
pdd const& q() const { return m_q; }
pdd const& r() const { return m_r; }
code get_op() const { return m_op; }
std::ostream& display(std::ostream& out, lbool status) const override;
std::ostream& display(std::ostream& out) const override;
lbool eval() const override;
lbool eval(assignment const& a) const override;
void narrow(solver& s, bool is_positive, bool first) override;
bool propagate_bits(solver& s, bool is_positive) override;
virtual clause_ref produce_lemma(solver& s, assignment const& a, bool is_positive) override;
unsigned hash() const override;
bool operator==(constraint const& other) const override;

2
src/math/polysat/restart.cpp
View file

@ -40,6 +40,8 @@ namespace polysat {
s.pop_levels(s.m_level - s.base_level());
m_conflicts_at_restart = s.m_stats.m_num_conflicts;
m_restart_threshold = m_restart_init * get_luby(++m_luby_idx);
verbose_stream() << "Restart with Conflict #" << s.m_stats.m_num_conflicts << "\n";
s.randomize_activity();
}
}

29
src/math/polysat/saturation.cpp
View file

@ -63,6 +63,9 @@ namespace polysat {
if (c->is_umul_ovfl())
return try_umul_ovfl(v, c, core);
if (c->is_op())
return try_op(v, c, core);
return false;
}
@ -222,6 +225,30 @@ namespace polysat {
return false;
}
bool saturation::try_op(pvar v, signed_constraint c, conflict& core) {
SASSERT(c->is_op());
SASSERT(c.is_positive());
return false;
op_constraint* op = ((op_constraint*)c.get());
clause_ref correction = op->produce_lemma(s, s.get_assignment(), c.is_positive());
if (correction) {
IF_LOGGING(
LOG("correcting op_constraint: " << *correction);
for (sat::literal lit : *correction) {
LOG("\t" << lit_pp(s, lit));
}
);
for (const sat::literal& l : *correction)
if (!s.m_bvars.is_assigned(l))
s.assign_eval(~l);
core.add_lemma(correction);
log_lemma(v, core);
return true;
}
return false;
}
signed_constraint saturation::ineq(bool is_strict, pdd const& lhs, pdd const& rhs) {
if (is_strict)
return s.ult(lhs, rhs);
@ -1028,7 +1055,7 @@ namespace polysat {
return false;
m_lemma.insert_eval(~c);
}
return propagate(x, core, axb_l_y, s.f());
return propagate(x, core, axb_l_y, s.f()); // TODO: Conflict overload
};
vector<signed_constraint> at_least_x, at_most_x, at_least_b, at_most_b, at_least_a, at_most_a;

2
src/math/polysat/saturation.h
View file

@ -173,6 +173,8 @@ namespace polysat {
bool try_umul_noovfl_bounds(pvar v, signed_constraint c, conflict& core);
bool try_umul_ovfl_bounds(pvar v, signed_constraint c, conflict& core);
bool try_op(pvar v, signed_constraint c, conflict& core);
public:
saturation(solver& s);
void perform(pvar v, conflict& core);

105
src/math/polysat/simplify_clause.cpp
View file

@ -358,7 +358,7 @@ namespace polysat {
}
// 2^(k - d) * x = m * 2^(k - d)
bool simplify_clause::get_trailing_mask(pdd lhs, pdd rhs, pdd& p, trailing_bits& mask, bool pos) {
bool simplify_clause::get_lsb(pdd lhs, pdd rhs, pdd& p, trailing_bits& info, bool pos) {
auto lhs_decomp = decouple_constant(lhs);
auto rhs_decomp = decouple_constant(rhs);
@ -375,10 +375,12 @@ namespace polysat {
p = lhs.div(rational::power_of_two(d));
rational rhs_val = rhs.val();
mask.bits = rhs_val / rational::power_of_two(d);
if (!mask.bits.is_int())
info.bits = rhs_val / rational::power_of_two(d);
if (!info.bits.is_int())
return false;
SASSERT(lhs.is_univariate() && lhs.degree() <= 1);
auto it = p.begin();
auto first = *it;
it++;
@ -388,32 +390,85 @@ namespace polysat {
rational inv;
VERIFY(first.coeff.mult_inverse(lhs.power_of_2(), inv));
p *= inv;
mask.bits = mod2k(mask.bits * inv, span);
info.bits = mod2k(info.bits * inv, span);
}
mask.length = span;
mask.positive = pos;
info.length = span;
info.positive = pos;
return true;
}
// 2^k - 2^(k - i) <= x -> first i bits 1
// 2^(k - i) > x -> first i bits 0
bool simplify_clause::get_msb(pdd lhs, pdd rhs, pdd& p, leading_bits& info, bool pos) {
if (lhs.is_var() && rhs.is_val()) {
if (rhs.is_zero())
return false;
// rewrite into expected form
pdd t = lhs;
lhs = rhs;
rhs = t - 1;
pos = !pos;
}
if (!rhs.is_var() || !lhs.is_val())
return false;
p = rhs;
rational v = lhs.val();
if (pos)
v = rational::power_of_two(lhs.power_of_2()) - v;
SASSERT(!v.is_neg());
info.positive = pos;
if (v.is_zero())
return false;
if (v.is_one()) {
if (pos)
return false;
info.length = lhs.power_of_2();
return true; // p = 0
}
unsigned d = (v - 1).get_num_bits(); // ceil(log2(lhs))
info.length = lhs.power_of_2() - d;
if (info.length == 0)
return false;
return true;
}
// 2^(k - 1) <= 2^(k - i - 1) * x (original definition) // TODO: Have this as well
// 2^(k - i - 1) * x + 2^(k - 1) <= 2^(k - 1) - 1 (currently we test only for this form)
// 2^(k - 1) <= 2^(k - i - 1) * x (original definition)
// 2^(k - i - 1) * x + 2^(k - 1) <= 2^(k - 1) - 1 (rewritten)
bool simplify_clause::get_bit(const pdd& lhs, const pdd& rhs, pdd& p, single_bit& bit, bool pos) {
if (!rhs.is_val())
return false;
rational rhs_val = rhs.val() + 1;
unsigned k = rhs.power_of_2();
if (rhs_val != rational::power_of_two(k - 1))
return false;
pdd rest = lhs - rhs_val;
unsigned d = rest.max_pow2_divisor();
bit.position = k - d - 1;
bit.positive = pos;
p = rest.div(rational::power_of_two(d));
return true;
if (rhs.is_val()) {
// 2^(k - i - 1) * x + 2^(k - 1) <= 2^(k - 1) - 1
rational rhs_val = rhs.val() + 1;
if (rhs_val != rational::power_of_two(k - 1))
return false;
pdd rest = lhs - rhs_val;
if (rest.is_val()) // e.g., lhs=2^255; rhs=2^255-1
return false;
SASSERT(lhs.is_univariate() && lhs.degree() <= 1);
unsigned d = rest.max_pow2_divisor();
bit.position = k - d - 1;
bit.positive = pos;
p = rest.div(rational::power_of_two(d));
return p.is_var();
}
else {
// 2^(k - 1) <= 2^(k - i - 1) * x
unsigned pow;
if (!lhs.is_val() || !lhs.val().is_power_of_two(pow) || pow != k - 1)
return false;
unsigned d = rhs.max_pow2_divisor();
bit.position = k - d - 1;
bit.positive = pos;
p = rhs.div(rational::power_of_two(d));
return p.is_var();
}
}
// Compares with respect to "subsumption"
@ -444,7 +499,7 @@ namespace polysat {
*
* let lsb(t, d) = m := 2^(k - d)*t = m * 2^(k - d) denotes that the last (least significant) d bits of t are the binary representation of m
* let bit(t, i) := 2^(k - 1) <= 2^(k - i - 1)*t
* TODO: 2^(k - 1 - d) <= 2^(k - i - 1)*t denotes that bits i-d...i are set to 0
* TODO: t == val || bit(t, i) resp. !bit(t, i) resp. lsb(t, d) = m with matching values removes the equality
*
* lsb(t, d) = m with log2(m) >= d => false
*
@ -500,7 +555,7 @@ namespace polysat {
trailing_bits mask;
single_bit bit;
pdd p = c->to_ule().lhs();
if ((c.is_eq() || c.is_diseq()) && get_trailing_mask(c->to_ule().lhs(), c->to_ule().rhs(), p, mask, c.is_positive())) {
if ((c.is_eq() || c.is_diseq()) && get_lsb(c->to_ule().lhs(), c->to_ule().rhs(), p, mask, c.is_positive())) {
if (mask.bits.bitsize() > mask.length) {
removed[i] = true; // skip this constraint. e.g., 2^(k-3)*x = 9*2^(k-3) is false as 9 >= 2^3
continue;

8
src/math/polysat/simplify_clause.h
View file

@ -24,6 +24,11 @@ namespace polysat {
bool positive;
unsigned src_idx;
};
struct leading_bits {
unsigned length;
bool positive; // either all 0 or all 1
unsigned src_idx;
};
struct single_bit {
bool positive;
unsigned position;
@ -60,7 +65,8 @@ namespace polysat {
bool apply(clause& cl);
static bool get_trailing_mask(pdd lhs, pdd rhs, pdd& p, trailing_bits& mask, bool pos);
static bool get_lsb(pdd lhs, pdd rhs, pdd& p, trailing_bits& info, bool pos);
static bool get_msb(pdd lhs, pdd rhs, pdd& p, leading_bits& info, bool pos);
static bool get_bit(const pdd& lhs, const pdd& rhs, pdd& p, single_bit& bit, bool pos);
};

18
src/math/polysat/solver.cpp
View file

@ -32,7 +32,6 @@ namespace polysat {
m_viable(*this),
m_viable_fallback(*this),
m_linear_solver(*this),
m_fixed_bits(*this),
m_conflict(*this),
m_simplify_clause(*this),
m_simplify(*this),
@ -595,9 +594,6 @@ namespace polysat {
m_trail.push_back(trail_instr_t::inc_level_i);
#if ENABLE_LINEAR_SOLVER
m_linear_solver.push();
#endif
#if 0
m_fixed_bits.push();
#endif
}
@ -610,9 +606,6 @@ namespace polysat {
LOG("Pop " << num_levels << " levels (lvl " << m_level << " -> " << target_level << ")");
#if ENABLE_LINEAR_SOLVER
m_linear_solver.pop(num_levels);
#endif
#if 0
m_fixed_bits.pop();
#endif
while (num_levels > 0) {
switch (m_trail.back()) {
@ -1403,6 +1396,17 @@ namespace polysat {
m_activity_inc >>= 14;
}
void solver::randomize_activity() {
m_activity_inc = activity_inc_default;
m_free_pvars.reset();
for (unsigned v = num_vars(); v > 0; v--) {
if (is_assigned(v - 1))
continue;
m_activity[v - 1] = m_rand() % activity_inc_default;
m_free_pvars.mk_var_eh(v - 1);
}
}
void solver::report_unsat() {
backjump(base_level());
VERIFY(!m_conflict.empty());

12
src/math/polysat/solver.h
View file

@ -24,7 +24,6 @@ Author:
#include "math/polysat/constraint.h"
#include "math/polysat/constraint_manager.h"
#include "math/polysat/clause_builder.h"
#include "math/polysat/fixed_bits.h"
#include "math/polysat/simplify_clause.h"
#include "math/polysat/simplify.h"
#include "math/polysat/restart.h"
@ -119,8 +118,6 @@ namespace polysat {
friend class conflict_explainer;
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;
@ -151,7 +148,6 @@ namespace polysat {
viable m_viable; // viable sets per variable
viable_fallback m_viable_fallback; // fallback for viable, using bitblasting over univariate constraints
linear_solver m_linear_solver;
fixed_bits m_fixed_bits;
conflict m_conflict;
simplify_clause m_simplify_clause;
simplify m_simplify;
@ -288,11 +284,13 @@ namespace polysat {
std::optional<lemma_score> compute_lemma_score(clause const& lemma);
// activity of variables based on standard VSIDS
unsigned m_activity_inc = 128;
unsigned m_variable_decay = 110;
const unsigned activity_inc_default = 128;
unsigned m_activity_inc = activity_inc_default;
const unsigned m_variable_decay = 110;
void inc_activity(pvar v);
void decay_activity();
void rescale_activity();
void randomize_activity();
void report_unsat();
void backjump(unsigned new_level);
@ -505,7 +503,7 @@ namespace polysat {
signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
signed_constraint t() { return eq(sz2pdd(1).mk_val(0)); }
signed_constraint f() { return eq(sz2pdd(1).mk_val(1)); }
signed_constraint f() { return ~t(); }
/** Create and activate constraints */
void add_eq(pdd const& p, dependency dep = null_dependency) { assign_eh(eq(p), dep); }

109
src/math/polysat/ule_constraint.cpp
View file

@ -295,10 +295,6 @@ namespace polysat {
// lhs > rhs ==> lhs > 0
s.add_clause(~sc, s.ult(0, lhs()), false);
}
#if 0
propagate_bits(s, is_positive);
#endif
}
// Evaluate lhs <= rhs
@ -326,111 +322,6 @@ namespace polysat {
lbool ule_constraint::eval(assignment const& a) const {
return eval(a.apply_to(lhs()), a.apply_to(rhs()));
}
bool ule_constraint::propagate_bits(solver& s, bool is_positive) {
if (is_eq() && is_positive) {
vector<optional<pdd>> e;
bool failed = false;
for (const auto& m : lhs()) {
if (e.size() > 1) {
failed = true;
break;
}
pdd p = lhs().manager().mk_val(m.coeff);
for (pvar v : m.vars)
p *= s.var(v);
e.push_back(optional(p));
if (e.size() == 2 && (m.coeff < 0 || m.coeff >= rational::power_of_two(p.power_of_2() - 1)))
std::swap(e[0], e[1]); // try to keep it positive
}
if (!failed && !e.empty()) {
if (e.size() == 1)
e.push_back(optional(lhs().manager().mk_val(0)));
else
e[0] = optional(-*(e[0]));
SASSERT(e.size() == 2);
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_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_bit(s, *(e[0]), i, rhs_val[i], bit_justification_constraint::mk_unary(s, this, { *(e[1]), i }), true))
return false;
}
}
return true;
}
}
pdd lhs = is_positive ? m_lhs : m_rhs;
pdd rhs = is_positive ? m_rhs : m_lhs;
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 << ")");
// TODO: Propagate powers of 2 (lower bound)
bool conflict = false;
bit_dependencies dep;
static unsigned char action_lookup[] = {
// lhs <= rhs
// 0 .. break; could be still satisfied;
// 1 ... continue; there might still be a conflict [lhs is the justification; rhs is propagated 1];
// 2 ... continue; --||-- [rhs is the justification; lhs is propagated 0];
// 3 ... conflict; lhs is for sure greater than rhs;
// 4 ... invalid (should not happen)
0, /*(z, z)*/ 0, /*(0, z)*/ 1, /*(1, z)*/ 4, /*(x, z)*/
2, /*(z, 0)*/ 2, /*(0, 0)*/ 3, /*(1, 0)*/ 4, /*(x, 0)*/
0, /*(z, 1)*/ 0, /*(0, 1)*/ 1, /*(1, 1)*/ 4, /*(x, 1)*/
// for the positive case (vice-versa for negative case -> we swap lhs/rhs + special treatment for index 0)
};
unsigned i = sz;
for (; i > (unsigned)!is_positive && !conflict; i--) {
tbit l = lhs_val[i - 1];
tbit r = rhs_val[i - 1];
unsigned char action = action_lookup[l | (r << 2)];
switch (action) {
case 0:
i = 0;
break;
case 1:
case 3:
dep.push_back({ lhs, i - 1 });
LOG("Added dependency: pdd: " << lhs << " idx: " << i - 1);
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_bit(s, lhs, i - 1, BIT_0, bit_justification_constraint::mk(s, this, dep), true);
SASSERT(!conflict);
break;
default:
VERIFY(false);
}
}
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_bit(s, lhs, 0, BIT_0, bit_justification_constraint::mk(s, this, dep), true);
if (!conflict)
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)
);
return !conflict;
}
unsigned ule_constraint::hash() const {
return mk_mix(lhs().hash(), rhs().hash(), kind());

1
src/math/polysat/ule_constraint.h
View file

@ -41,7 +41,6 @@ namespace polysat {
lbool eval() const override;
lbool eval(assignment const& a) const override;
void narrow(solver& s, bool is_positive, bool first) override;
bool propagate_bits(solver& s, bool is_positive) override;
unsigned hash() const override;
bool operator==(constraint const& other) const override;
bool is_eq() const override { return m_rhs.is_zero(); }

467
src/math/polysat/viable.cpp
View file

@ -563,15 +563,17 @@ namespace {
return true;
}
// TODO: Extend in both directions? (Less justifications vs. bigger intervals)
rational new_val2 = extend_by_bits<!FORWARD>(v_pdd, val, fixed, justifications, ne->src, ne->side_cond, ne->refined);
ne->coeff = 1;
if (FORWARD) {
LOG("refine-bits for v" << v << " [" << val << ", " << new_val << "[");
ne->interval = eval_interval::proper(v_pdd.manager().mk_val(val), val, v_pdd.manager().mk_val(new_val), new_val);
LOG("refine-bits FORWARD for v" << v << " = " << val << " to [" << new_val2 << ", " << new_val << "[");
ne->interval = eval_interval::proper(v_pdd.manager().mk_val(new_val2), new_val2, v_pdd.manager().mk_val(new_val), new_val);
}
else {
rational upper_bound = val == v_pdd.manager().max_value() ? rational::zero() : val + 1;;
LOG("refine-bits for v" << v << " [" << new_val << ", " << upper_bound << "[");
ne->interval = eval_interval::proper(v_pdd.manager().mk_val(new_val), new_val, v_pdd.manager().mk_val(upper_bound), upper_bound);
LOG("refine-bits BACKWARD for v" << v << " = " << val << " to [" << new_val << ", " << new_val2 << "[");
ne->interval = eval_interval::proper(v_pdd.manager().mk_val(new_val), new_val, v_pdd.manager().mk_val(new_val2), new_val2);
}
SASSERT(ne->interval.currently_contains(val));
intersect(v, ne);
@ -921,98 +923,150 @@ namespace {
fixed.resize(p.power_of_2(), l_undef);
justifications.resize(p.power_of_2(), ptr_vector<entry>());
auto* e = m_equal_lin[v];
auto* first = e;
if (!e)
auto* e1 = m_equal_lin[v];
auto* e2 = m_units[v];
auto* first = e1;
if (!e1 && !e2)
return true;
clause_builder builder(s, "bit check");
uint_set already_added;
vector<std::pair<entry*, trailing_bits>> postponed;
auto add_entry = [&builder](entry* e) {
for (const auto& sc : e->side_cond)
auto add_entry = [&builder, &already_added](entry* e) {
for (const auto& sc : e->side_cond) {
if (already_added.contains(sc.bvar()))
continue;
already_added.insert(sc.bvar());
builder.insert_eval(~sc);
for (const auto& src : e->src)
}
for (const auto& src : e->src) {
if (already_added.contains(src.bvar()))
continue;
already_added.insert(src.bvar());
builder.insert_eval(~src);
}
};
auto add_entry_list = [add_entry](const ptr_vector<entry>& list) {
for (const auto& e : list)
add_entry(e);
};
unsigned largest_mask = 0;
do {
if (e->src.size() != 1) {
// We just consider the ordinary constraints and not already contracted ones
e = e->next();
continue;
}
signed_constraint& src = e->src[0];
single_bit bit;
trailing_bits mask;
if (src->is_ule() &&
simplify_clause::get_bit(s.subst(src->to_ule().lhs()), s.subst(src->to_ule().rhs()), p, bit, src.is_positive()) && p.is_var()) {
lbool prev = fixed[bit.position];
fixed[bit.position] = bit.positive ? l_true : l_false;
//verbose_stream() << "Setting bit " << bit.position << " to " << bit.positive << " because of " << e->src << "\n";
if (prev != l_undef && fixed[bit.position] != prev) {
LOG("Bit conflicting " << e->src << " with " << justifications[bit.position][0]->src);
if (add_conflict) {
add_entry_list(justifications[bit.position]);
add_entry(e);
s.set_conflict(*builder.build());
}
return false;
}
// just override; we prefer bit constraints over parity as those are easier for subsumption to remove
// verbose_stream() << "Adding bit constraint: " << e->src[0] << " (" << bit.position << ")\n";
justifications[bit.position].clear();
justifications[bit.position].push_back(e);
}
else if ((src->is_eq() || src.is_diseq()) &&
simplify_clause::get_trailing_mask(s.subst(src->to_ule().lhs()), s.subst(src->to_ule().rhs()), p, mask, src.is_positive()) && p.is_var()) {
if (src.is_positive()) {
for (unsigned i = 0; i < mask.length; i++) {
lbool prev = fixed[i];
fixed[i] = mask.bits.get_bit(i) ? l_true : l_false;
//verbose_stream() << "Setting bit " << i << " to " << mask.bits.get_bit(i) << " because of parity " << e->src << "\n";
if (prev != l_undef) {
if (fixed[i] != prev) {
LOG("Positive parity conflicting " << e->src << " with " << justifications[i][0]->src);
if (add_conflict) {
add_entry_list(justifications[i]);
add_entry(e);
s.set_conflict(*builder.build());
}
return false;
}
else {
// Prefer justifications from larger masks (less premisses)
if (largest_mask < mask.length) {
largest_mask = mask.length;
justifications[i].clear();
justifications[i].push_back(e);
// verbose_stream() << "Adding parity constraint: " << e->src[0] << " (" << i << ")\n";
}
}
}
else {
SASSERT(justifications[i].empty());
justifications[i].push_back(e);
// verbose_stream() << "Adding parity constraint: " << e->src[0] << " (" << i << ")\n";
}
}
}
else
postponed.push_back({ e, mask });
}
e = e->next();
} while(e != first);
if (e1) {
unsigned largest_lsb = 0;
do {
if (e1->src.size() != 1) {
// We just consider the ordinary constraints and not already contracted ones
e1 = e1->next();
continue;
}
signed_constraint& src = e1->src[0];
single_bit bit;
trailing_bits lsb;
if (src->is_ule() &&
simplify_clause::get_bit(s.subst(src->to_ule().lhs()), s.subst(src->to_ule().rhs()), p, bit, src.is_positive()) && p.is_var()) {
lbool prev = fixed[bit.position];
fixed[bit.position] = bit.positive ? l_true : l_false;
//verbose_stream() << "Setting bit " << bit.position << " to " << bit.positive << " because of " << e->src << "\n";
if (prev != l_undef && fixed[bit.position] != prev) {
LOG("Bit conflicting " << e1->src << " with " << justifications[bit.position][0]->src);
if (add_conflict) {
add_entry_list(justifications[bit.position]);
add_entry(e1);
s.set_conflict(*builder.build());
}
return false;
}
// just override; we prefer bit constraints over parity as those are easier for subsumption to remove
// verbose_stream() << "Adding bit constraint: " << e->src[0] << " (" << bit.position << ")\n";
justifications[bit.position].clear();
justifications[bit.position].push_back(e1);
}
else if ((src->is_eq() || src.is_diseq()) &&
simplify_clause::get_lsb(s.subst(src->to_ule().lhs()), s.subst(src->to_ule().rhs()), p, lsb, src.is_positive()) && p.is_var()) {
if (src.is_positive()) {
for (unsigned i = 0; i < lsb.length; i++) {
lbool prev = fixed[i];
fixed[i] = lsb.bits.get_bit(i) ? l_true : l_false;
if (prev != l_undef) {
if (fixed[i] != prev) {
LOG("Positive parity conflicting " << e1->src << " with " << justifications[i][0]->src);
if (add_conflict) {
add_entry_list(justifications[i]);
add_entry(e1);
s.set_conflict(*builder.build());
}
return false;
}
else {
// Prefer justifications from larger masks (less premisses)
// TODO: Check that we don't override justifications comming from bit constraints
if (largest_lsb < lsb.length) {
justifications[i].clear();
justifications[i].push_back(e1);
}
}
}
else {
SASSERT(justifications[i].empty());
justifications[i].push_back(e1);
}
}
largest_lsb = std::max(largest_lsb, lsb.length);
}
else
postponed.push_back({ e1, lsb });
}
e1 = e1->next();
} while(e1 != first);
}
#if 0 // is the benefit enough?
if (e2) {
unsigned largest_msb = 0;
first = e2;
do {
if (e2->src.size() != 1) {
e2 = e2->next();
continue;
}
signed_constraint& src = e2->src[0];
leading_bits msb;
if (src->is_ule() &&
simplify_clause::get_msb(s.subst(src->to_ule().lhs()), s.subst(src->to_ule().rhs()), p, msb, src.is_positive()) && p.is_var()) {
for (unsigned i = fixed.size() - msb.length; i < fixed.size(); i++) {
lbool prev = fixed[i];
fixed[i] = msb.positive ? l_true : l_false;
if (prev != l_undef) {
if (fixed[i] != prev) {
LOG("msb conflicting " << e2->src << " with " << justifications[i][0]->src);
if (add_conflict) {
add_entry_list(justifications[i]);
add_entry(e2);
s.set_conflict(*builder.build());
}
return false;
}
else {
if (largest_msb < msb.length) {
justifications[i].clear();
justifications[i].push_back(e2);
}
}
}
else {
SASSERT(justifications[i].empty());
justifications[i].push_back(e2);
}
}
largest_msb = std::max(largest_msb, msb.length);
}
e2 = e2->next();
} while(e2 != first);
}
#endif
// TODO: Incomplete - e.g., if we know the trailing bits are not 00 not 10 not 01 and not 11 we could also detect a conflict
// This would require partially clause solving (worth the effort?)
bool_vector removed(postponed.size(), false);
@ -1074,6 +1128,151 @@ namespace {
return true;
}
#if 0
bool viable::collect_bit_information(pvar v, bool add_conflict, const vector<signed_constraint>& cnstr, svector<lbool>& fixed, vector<vector<signed_constraint>>& justifications) {
pdd p = s.var(v);
fixed.clear();
justifications.clear();
fixed.resize(p.power_of_2(), l_undef);
justifications.resize(p.power_of_2(), vector<signed_constraint>());
if (cnstr.empty())
return true;
clause_builder builder(s, "bit check");
uint_set already_added;
vector<std::pair<signed_constraint, trailing_bits>> postponed;
auto add_entry = [&builder, &already_added](const signed_constraint& src) {
if (already_added.contains(src.bvar()))
return;
already_added.insert(src.bvar());
builder.insert_eval(~src);
};
auto add_entry_list = [add_entry](const vector<signed_constraint>& list) {
for (const auto& e : list)
add_entry(e);
};
unsigned largest_mask = 0;
for (unsigned i = 0; i < cnstr.size(); i++) {
const signed_constraint& src = cnstr[i];
single_bit bit;
trailing_bits mask;
if (src->is_ule() &&
simplify_clause::get_bit(src->to_ule().lhs(), src->to_ule().rhs(), p, bit, src.is_positive()) && p.is_var()) {
lbool prev = fixed[bit.position];
fixed[bit.position] = bit.positive ? l_true : l_false;
if (prev != l_undef && fixed[bit.position] != prev) {
LOG("Bit conflicting " << src << " with " << justifications[bit.position][0]);
if (add_conflict) {
add_entry_list(justifications[bit.position]);
add_entry(src);
s.set_conflict(*builder.build());
}
return false;
}
justifications[bit.position].clear();
justifications[bit.position].push_back(src);
}
else if ((src->is_eq() || src.is_diseq()) &&
simplify_clause::get_lsb(src->to_ule().lhs(), src->to_ule().rhs(), p, mask, src.is_positive()) && p.is_var()) {
if (src.is_positive()) {
for (unsigned i = 0; i < mask.length; i++) {
lbool prev = fixed[i];
fixed[i] = mask.bits.get_bit(i) ? l_true : l_false;
//verbose_stream() << "Setting bit " << i << " to " << mask.bits.get_bit(i) << " because of parity " << e->src << "\n";
if (prev != l_undef) {
if (fixed[i] != prev) {
LOG("Positive parity conflicting " << src << " with " << justifications[i][0]);
if (add_conflict) {
add_entry_list(justifications[i]);
add_entry(src);
s.set_conflict(*builder.build());
}
return false;
}
else {
if (largest_mask < mask.length) {
largest_mask = mask.length;
justifications[i].clear();
justifications[i].push_back(src);
}
}
}
else {
SASSERT(justifications[i].empty());
justifications[i].push_back(src);
}
}
}
else
postponed.push_back({ src, mask });
}
}
bool_vector removed(postponed.size(), false);
bool changed;
do {
changed = false;
for (unsigned j = 0; j < postponed.size(); j++) {
if (removed[j])
continue;
const auto& neg = postponed[j];
unsigned indet = 0;
unsigned last_indet = 0;
unsigned i = 0;
for (; i < neg.second.length; i++) {
if (fixed[i] != l_undef) {
if (fixed[i] != (neg.second.bits.get_bit(i) ? l_true : l_false)) {
removed[j] = true;
break; // this is already satisfied
}
}
else {
indet++;
last_indet = i;
}
}
if (i == neg.second.length) {
if (indet == 0) {
// Already false
LOG("Found conflict with constraint " << neg.first);
if (add_conflict) {
for (unsigned k = 0; k < neg.second.length; k++)
add_entry_list(justifications[k]);
add_entry(neg.first);
s.set_conflict(*builder.build());
}
return false;
}
else if (indet == 1) {
// Simple BCP
auto& justification = justifications[last_indet];
SASSERT(justification.empty());
for (unsigned k = 0; k < neg.second.length; k++) {
if (k != last_indet) {
SASSERT(fixed[k] != l_undef);
for (const auto& just : justifications[k])
justification.push_back(just);
}
}
justification.push_back(neg.first);
fixed[last_indet] = neg.second.bits.get_bit(last_indet) ? l_false : l_true;
removed[j] = true;
LOG("Applying fast BCP on bit " << last_indet << " from constraint " << neg.first);
changed = true;
}
}
}
} while(changed);
return true;
}
#endif
bool viable::has_viable(pvar v) {
svector<lbool> fixed;
@ -1367,11 +1566,12 @@ namespace {
else {
UNREACHABLE();
}
if (refinements % 100 == 0)
verbose_stream() << "Refinements " << refinements << "\n";
if (res != l_undef)
return res;
}
verbose_stream() << "Fallback\n";
LOG("Refinement budget exhausted! Fall back to univariate solver.");
return query_fallback<mode>(v, result);
}
@ -1621,10 +1821,91 @@ namespace {
return true;
}
#if 0
void viable::make_bit_justification(pvar v) {
if (!m_units[v] || m_units[v]->interval.is_full())
return;
// TODO: Maybe this helps? This prefers justifications from bits
svector<lbool> fixed;
vector<ptr_vector<entry>> justifications;
if (!collect_bit_information(v, false, fixed, justifications))
return;
entry* first = m_units[v];
entry* e = first;
vector<eval_interval> intervals;
do {
intervals.push_back(e->interval);
e = e->next();
}
while (e != first);
int additional = 0;
for (unsigned i = 0; i < intervals.size(); i++) { // Try to justify by bits as good as possible
if (intervals[i].hi_val().is_zero())
additional += refine_bits<true>(v, s.var(v).manager().max_value(), fixed, justifications);
else
additional += refine_bits<true>(v, intervals[i].hi_val() - 1, fixed, justifications);
}
verbose_stream() << "Found " << additional << " intervals\n";
}
void viable::get_bit_min_max(pvar v, conflict& core, rational& min, rational& max, vector<signed_constraint>& justifications_min, vector<signed_constraint>& justifications_max) {
pdd v_pdd = s.var(v);
min = 0;
max = v_pdd.manager().max_value();
svector<lbool> fixed;
vector<vector<signed_constraint>> justifications;
vector<signed_constraint> candidates;
for (const auto& c : core) {
if (!c->is_ule())
continue;
ule_constraint ule = c->to_ule();
pdd sum = ule.lhs() + ule.rhs();
if (sum.is_univariate_in(v) && sum.degree(v) == 1)
candidates.push_back(c);
}
if (candidates.empty() || !collect_bit_information(v, false, candidates, fixed, justifications))
return;
for (unsigned i = 0; i < fixed.size(); i++) {
verbose_stream() << (fixed[fixed.size() - 1] == l_true ? '1' : fixed[fixed.size() - 1] == l_false ? '0' : '?');
}
verbose_stream() << "\n";
max = 0;
for (unsigned i = fixed.size(); i > 0; i--) {
min *= 2;
max *= 2;
lbool val = fixed[i - 1];
if (val == l_true) {
min++;
max++;
for (auto& add : justifications[i - 1])
justifications_min.push_back(add);
}
else if (val == l_undef)
max++;
else {
SASSERT(val == l_false);
for (auto& add : justifications[i - 1])
justifications_max.push_back(add);
}
}
}
#endif
bool viable::resolve_interval(pvar v, conflict& core) {
DEBUG_CODE( log(v); );
if (has_viable(v))
return false;
#if 0
// Prefer bit information as justifications
make_bit_justification(v);
#endif
entry const* e = m_units[v];
// TODO: in the forbidden interval paper, they start with the longest interval. We should also try that at some point.
entry const* first = e;
@ -1759,9 +2040,15 @@ namespace {
out << e->coeff << " * v" << v << " " << e->interval << " ";
else
out << e->interval << " ";
out << e->side_cond << " ";
for (const auto& src : e->src)
out << src << "; ";
if (e->side_cond.size() <= 5)
out << e->side_cond << " ";
else
out << e->side_cond.size() << " side-conditions ";
if (e->src.size() <= 5)
for (const auto& src : e->src)
out << src << "; ";
else
out << e->src.size() << " sources";
return out;
}

9
src/math/polysat/viable.h
View file

@ -73,6 +73,7 @@ namespace polysat {
class viable {
friend class test_fi;
friend class test_polysat;
friend class conflict;
solver& s;
forbidden_intervals m_forbidden_intervals;
@ -108,6 +109,9 @@ namespace polysat {
rational extend_by_bits(const pdd& var, const rational& bounds, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications, vector<signed_constraint>& src, vector<signed_constraint>& side_cond, ptr_vector<entry const>& refined) const;
bool collect_bit_information(pvar v, bool add_conflict, svector<lbool>& fixed, vector<ptr_vector<entry>>& justifications);
#if 0
bool collect_bit_information(pvar v, bool add_conflict, const vector<signed_constraint>& cnstr, svector<lbool>& fixed, vector<vector<signed_constraint>>& justifications);
#endif
std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const;
std::ostream& display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter = "") const;
@ -227,6 +231,11 @@ namespace polysat {
*/
lbool find_viable(pvar v, rational& out_lo, rational& out_hi);
#if 0
void make_bit_justification(pvar v);
void get_bit_min_max(pvar v, conflict& core, rational& min, rational& max, vector<signed_constraint>& justifications_min, vector<signed_constraint>& justifications_max);
#endif
/**
* Retrieve the unsat core for v,
* and add the forbidden interval lemma for v (which eliminates v from the unsat core).

1
src/test/polysat.cpp
View file

@ -1952,7 +1952,6 @@ static void STD_CALL polysat_on_ctrl_c(int) {
void tst_polysat() {
using namespace polysat;
test_polysat::test_ineq_axiom4(32, 7);
#if 0 // Enable this block to run a single unit test with detailed output.
collect_test_records = false;
test_max_conflicts = 50;