mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat
This commit is contained in:
Nikolaj Bjorner
commit
45e772b223
6 changed files with 458 additions and 311 deletions
|
|
@ -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<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, 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<pdd> sum_subterms;
|
||||
vector<pdd> sum_subterms; // TODO: optional?
|
||||
vector<vector<pdd>> 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<pdd>& 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;
|
||||
|
|
|
|||
|
|
@ -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<pdd> m_pdd;
|
||||
unsigned m_bit_idx;
|
||||
|
|
@ -58,15 +60,19 @@ namespace polysat {
|
|||
|
||||
using bit_dependencies = vector<bvpos>;
|
||||
|
||||
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<pdd> 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<pdd> 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<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_justication;
|
||||
friend bit_justification;
|
||||
|
||||
solver& m_solver;
|
||||
scoped_ptr_vector<tbv_manager> m_tbv_managers;
|
||||
|
||||
using pdd_to_tbv_key = optional<pdd>;
|
||||
using pdd_to_tbv_eq = default_eq<pdd_to_tbv_key>;
|
||||
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<optional<pdd>>;
|
||||
struct pdd_to_info_hash {
|
||||
unsigned operator()(optional<pdd> const& args) const {
|
||||
return args->hash();
|
||||
}
|
||||
};
|
||||
using pdd_to_tbv_map = map<pdd_to_tbv_key, tbv_ref*, pdd_to_tbv_hash, pdd_to_tbv_eq>;
|
||||
|
||||
using bvpos_to_justification_eq = default_eq<bvpos>;
|
||||
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<bvpos, justified_bvpos, bvpos_to_justification_hash, bvpos_to_justification_eq>;
|
||||
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_tbv_map m_var_to_tbv;
|
||||
bvpos_to_justification_map m_bvpos_to_justification;
|
||||
pdd_to_info_map m_pdd_to_info;
|
||||
|
||||
svector<justified_bvpos> m_trail;
|
||||
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& 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<unsigned, unsigned> 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);
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue