mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

Added justifications for intermediate values [e.g., 2 * x in the pdd (2 * x) + y]

Browse source 
This might allow propagation in both directions
This commit is contained in:
Clemens Eisenhofer 2022-12-21 13:52:27 +01:00
parent ec06027515
commit c8b9127028
6 changed files with 475 additions and 172 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -53,8 +53,6 @@ namespace polysat {
constraint(constraint_manager& m, ckind_t k): m_kind(k) {}
bool has_bvar() const { return m_bvar != sat::null_bool_var; }
public:
virtual ~constraint() {}
@ -85,7 +83,7 @@ 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 void propagate_bits(solver& s, bool is_positive) {}
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.
@ -105,6 +103,7 @@ namespace polysat {
unsigned_vector const& vars() const { return m_vars; }
unsigned var(unsigned idx) const { return m_vars[idx]; }
bool contains_var(pvar v) const { return m_vars.contains(v); }
bool has_bvar() const { return m_bvar != sat::null_bool_var; }
sat::bool_var bvar() const { SASSERT(has_bvar()); return m_bvar; }
std::string bvar2string() const;

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

@ -15,6 +15,206 @@ Abstract:
#include "math/polysat/solver.h"
namespace polysat {
bit_justication* bit_justication::get_other_justification(const fixed_bits& fixed, const pdd& p, unsigned idx) {
return fixed.m_tbv_to_justification[{ p, idx }];
}
const tbv_ref& bit_justication::get_tbv(fixed_bits& fixed, const pdd& p) {
return fixed.get_tbv(p);
}
bool bit_justication::fix_value(fixed_bits& fixed, const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j) {
return fixed.fix_value(p, tbv, idx, val, j);
}
void bit_justication_constraint::get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) {
for (const auto& dep : this->m_dependencies)
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_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_justication_constraint* bit_justication_constraint::mk_justify_between(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_justication_constraint, 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
tbv_ref& bit_justication_mul::mul(fixed_bits& fixed, const pdd& p, const tbv_ref& in1, const tbv_ref& in2) {
auto m = in1.manager();
tbv_ref& out = fixed.get_tbv(p);
unsigned min_bit_value = 0; // The value of the current bit assuming all unknown bits are 0
unsigned max_bit_value = 0; // The value of the current bit assuming all unknown bits are 1
// TODO: Check: Is the performance too worse? It is O(k^2)
for (unsigned i = 0; i < m.num_tbits(); i++) {
for (unsigned x = 0, y = i; x <= i; x++, y--) {
tbit bit1 = in1[x];
tbit bit2 = in2[y];
if (bit1 == BIT_1 && bit2 == BIT_1) {
min_bit_value++; // we get two 1
max_bit_value++;
}
else if (bit1 != BIT_0 && bit2 != BIT_0) {
max_bit_value++; // we could get two 1
}
}
if (min_bit_value == max_bit_value) {
// We know the value of this bit
if (!fix_value(fixed, p, out, i, min_bit_value & 1 ? BIT_1 : BIT_0, alloc(bit_justication_mul)))
return out;
}
// Subtract one; shift this to the next higher bit as "carry value"
min_bit_value >>= 1;
max_bit_value >>= 1;
}
return out;
}
// 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_justication_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& tbv1 = get_tbv(fixed, *m_c1);
const tbv_ref& tbv2 = get_tbv(fixed, *m_c2);
for (unsigned i = m_idx - relevant_range; i <= m_idx; i++) {
for (unsigned x = 0, y = i; x <= i; x++, y--) {
tbit bit1 = tbv1[x];
tbit bit2 = tbv2[y];
if (bit1 == BIT_1 && bit2 == BIT_1) {
get_other_justification(fixed, *m_c1, x)->get_dependencies(fixed, to_process);
get_other_justification(fixed, *m_c2, x)->get_dependencies(fixed, to_process);
}
else if (bit1 == BIT_0) // TODO: Take the better one if both are zero
get_other_justification(fixed, *m_c1, x)->get_dependencies(fixed, to_process);
else if (bit2 == BIT_0)
get_other_justification(fixed, *m_c2, x)->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);
}
}
}
}
// similar to multiplying but far simpler/faster (only the direct predecessor might overflow)
tbv_ref& bit_justication_add::add(fixed_bits& fixed, const pdd& p, const tbv_ref& in1, const tbv_ref& in2) {
auto m = in1.manager();
tbv_ref& out = fixed.get_tbv(p);
unsigned min_bit_value = 0;
unsigned max_bit_value = 0;
for (unsigned i = 0; i < m.num_tbits(); i++) {
tbit bit1 = in1[i];
tbit bit2 = in2[i];
if (bit1 == BIT_1 && bit2 == BIT_1) {
min_bit_value++;
max_bit_value++;
}
else if (bit1 != BIT_0 && bit2 != BIT_0) {
max_bit_value++;
}
if (min_bit_value == max_bit_value)
if (!fix_value(fixed, p, out, i, min_bit_value & 1 ? BIT_1 : BIT_0, alloc(bit_justication_add)))
return out;
min_bit_value >>= 1;
max_bit_value >>= 1;
}
if (min_bit_value == max_bit_value) // Overflow to the first bit
fix_value(fixed, p, out, 0, min_bit_value & 1 ? BIT_1 : BIT_0, alloc(bit_justication_add));
return out;
}
void bit_justication_add::get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) {
if (m_c1->power_of_2() > 1) {
if (m_idx == 0) {
get_other_justification(fixed, *m_c1, m_c1->power_of_2() - 1)->get_dependencies(fixed, to_process);
get_other_justification(fixed, *m_c2, m_c1->power_of_2() - 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_c1->power_of_2() - 1] != BIT_z && tbv2[m_c1->power_of_2() - 1] != BIT_z);
);
}
else {
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);
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);
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);
@ -27,57 +227,107 @@ namespace polysat {
return get_manager(v.power_of_2());
}
tbv_ref& fixed_bits::get_tbv(pvar v, unsigned sz) {
if (m_var_to_tbv.size() <= v) {
tbv_ref& fixed_bits::get_tbv(const pdd& 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[optional(v)] = optional(tbv_ref(manager, manager.allocate(v.val())));
else
m_var_to_tbv[optional(v)] = optional(tbv_ref(manager, manager.allocate()));
return *m_var_to_tbv[optional(v)];
}
/*if (m_var_to_tbv.size() <= v) {
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];
}
auto& old_manager = m_var_to_tbv[v]->manager();
if (old_manager.num_tbits() >= sz)
return *(m_var_to_tbv[v]);
tbv* old_tbv = m_var_to_tbv[v]->detach();
auto& new_manager = get_manager(sz);
}*/
return *m_var_to_tbv[optional(v)];
/*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());
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[v] = tbv_ref(new_manager, new_tbv);
return *m_var_to_tbv[v];
m_var_to_tbv[optional(v)] = optional(tbv_ref(new_manager, new_tbv));
return *m_var_to_tbv[optional(v)];*/
}
tbv_ref& fixed_bits::get_tbv(const pdd& p) {
SASSERT(p.is_var());
return get_tbv(p.var(), p.power_of_2());
clause_ref fixed_bits::get_explanation(solver& s, bit_justication* j1, bit_justication* j2) {
bit_dependencies to_process;
// TODO: Check that we do not process the same tuple multiples times (efficiency)
j1->get_dependencies(*this, to_process);
j2->get_dependencies(*this, to_process);
clause_builder conflict(s);
conflict.set_redundant(true);
auto insert_constraint = [&conflict, &s](bit_justication* 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));
}
};
insert_constraint(j1);
insert_constraint(j2);
// 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()) {
bit_dependency& curr = to_process.back();
to_process.pop_back();
SASSERT(m_tbv_to_justification.contains(curr));
bit_justication* j = m_tbv_to_justification[curr];
insert_constraint(j);
j->get_dependencies(*this, to_process);
}
return conflict.build();
}
tbit fixed_bits::get_value(const pdd& p, unsigned idx) {
SASSERT(p.is_var());
return get_tbv(p)[idx];
}
bool fixed_bits::fix_value(solver& s, const pdd& p, unsigned idx, tbit val, constraint* c, bit_dependency& dep) {
bool fixed_bits::fix_value(const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j) {
SASSERT(val != BIT_x); // We don't use don't-cares
SASSERT(p.is_var());
if (val == BIT_z)
return true;
tbv_ref& tbv = get_tbv(p);
tbit curr_val = tbv[idx];
if (val == curr_val)
return true;
return true; // TODO: Take the new justification if it has a lower decision level
auto& m = tbv.manager();
if (curr_val == BIT_z) {
m.set(*tbv, idx, val);
m_tbv_to_justification[std::pair(tbv.get(), idx)] = bit_justication(c, (bit_dependency&&)std::move(dep));
delete m_tbv_to_justification[{ p, idx }];
m_tbv_to_justification[{ p, idx }] = j;
return true;
}
SASSERT((curr_val == BIT_1 && val == BIT_0) || (curr_val == BIT_0 && val == BIT_1));
SASSERT(m_tbv_to_justification.contains({ p, idx }));
return m_consistent = false;
}
bool fixed_bits::fix_value(solver& s, const pdd& p, unsigned idx, tbit val, bit_justication* j) {
tbv_ref& tbv = get_tbv(p);
if (fix_value(p, tbv, idx, val, j))
return true;
clause_ref explanation = get_explanation(s, j, m_tbv_to_justification[{ p, idx }]);
s.set_conflict(*explanation);
return false;
}
void fixed_bits::clear_value(const pdd& p, unsigned idx) {
@ -86,8 +336,9 @@ namespace polysat {
auto& m = tbv.manager();
m.set(*tbv, idx, BIT_z);
SASSERT(m_tbv_to_justification.contains(std::pair(tbv.get(), idx)));
m_tbv_to_justification[std::pair(tbv.get(), idx)] = bit_justication();
SASSERT(m_tbv_to_justification.contains({ p, idx }));
delete m_tbv_to_justification[{ p, idx }];
m_tbv_to_justification[{ p, idx }] = nullptr;
}
#define COUNT(DOWN, TO_COUNT) \
@ -133,90 +384,30 @@ namespace polysat {
return { least, most };
}
// 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) + ...
// maintains
void fixed_bits::multiply(tbv_ref& in_out, const tbv_ref& in2) {
auto m= in_out.manager();
m_aux_values.reserve(m.num_tbits());
unsigned min_bit_value = 0; // The value of the current bit assuming all unknown bits are 0
unsigned max_bit_value = 0; // The value of the current bit assuming all unknown bits are 1
// TODO: Check: Is the performance too worse? It is O(k^2)
for (unsigned i = 0; i < m.num_tbits(); i++) {
for (unsigned x = 0, y = i; x <= i; x++, y--) {
tbit bit1 = in_out[x];
tbit bit2 = in2[y];
if (bit1 == BIT_1 && bit2 == BIT_1) {
min_bit_value++; // we get two 1
max_bit_value++;
}
else if (bit1 != BIT_0 && bit2 != BIT_0) {
max_bit_value++; // we could get two 1
}
tbv_ref& fixed_bits::eval(solver& s, const pdd& p) {
pdd zero = p.manager().zero();
pdd one = p.manager().one();
pdd sum = zero;
tbv_ref* prev_sum_tbv = &get_tbv(sum);
for (const dd::pdd_monomial& n : p) {
SASSERT(!n.coeff.is_zero());
pdd prod = p.manager().mk_val(n.coeff);
tbv_ref* prev_mul_tbv = &get_tbv(prod);
for (pvar fac : n.vars) {
pdd fac_pdd = s.var(fac);
prod *= fac_pdd;
prev_mul_tbv = &bit_justication_mul::mul(*this, prod, *prev_mul_tbv, get_tbv(fac_pdd));
if (!m_consistent)
return *prev_sum_tbv;
}
if (min_bit_value == max_bit_value) {
// We know the value of this bit
// As we might access in_out in some later iteration again we first write to aux-list
m_aux_values[i] = min_bit_value & 1 ? BIT_1 : BIT_0;
}
else {
m_aux_values[i] = BIT_z;
}
// Subtract one; shift this to the next higher bit as "carry value"
min_bit_value >>= 1;
max_bit_value >>= 1;
sum += prod;
prev_sum_tbv = &bit_justication_add::add(*this, sum, *prev_sum_tbv, *prev_mul_tbv);
if (!m_consistent)
return *prev_sum_tbv;
}
// Copy aux to result tbv
for (unsigned i = 0; i < m.num_tbits(); i++) {
m.set(*in_out, i, (tbit)m_aux_values[i]);
}
}
// similar to multiplying
void fixed_bits::add(tbv_ref& in_out, const tbv_ref& in2) {
auto m= in_out.manager();
unsigned min_bit_value = 0;
unsigned max_bit_value = 0;
for (unsigned i = 0; i < m.num_tbits(); i++) {
tbit bit1 = in_out[i];
tbit bit2 = in2[i];
if (bit1 == BIT_1 && bit2 == BIT_1) {
min_bit_value++;
max_bit_value++;
}
else if (bit1 != BIT_0 && bit2 != BIT_0) {
max_bit_value++;
}
if (min_bit_value == max_bit_value)
// for addition we don't need previous values so we can directly write to the output variable
m.set(*in_out, i, min_bit_value & 1 ? BIT_1 : BIT_0);
else
m.set(*in_out, i, BIT_z);
min_bit_value >>= 1;
max_bit_value >>= 1;
}
}
tbv_ref fixed_bits::eval(const pdd& p) {
tbv_manager m = get_manager(p);
unsigned sz = m.num_tbits();
tbv_ref ret = tbv_ref(m, m.allocate(0ull));
for (const dd::pdd_monomial& s : p) {
SASSERT(!s.coeff.is_zero());
tbv_ref sum = tbv_ref(m, m.allocate(s.coeff));
for (pvar fac : s.vars) {
multiply(sum, get_tbv(fac, sz));
}
add(ret, sum);
}
return ret;
return *prev_sum_tbv;
}
}

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

@ -21,63 +21,150 @@ Abstract:
namespace polysat {
class solver;
using bit_dependency = vector<std::pair<pdd, unsigned>>;
struct bit_justication {
constraint* m_constraint = nullptr;
// variables + resp., bit-index
// (a variable might occur multiple times if more bits are relevant)
bit_dependency m_dependencies;
public:
bit_justication(constraint *pRaint, bit_dependency vector) = default;
bit_justication(constraint* c) : m_constraint(c) { }
bit_justication(constraint* c, bit_dependency&& dep) : m_constraint(c), m_dependencies(dep) { }
class constraint;
class fixed_bits;
struct bit_dependency {
optional<pdd> m_pdd;
unsigned m_bit_idx;
bit_dependency() : m_pdd(optional<pdd>::undef()), m_bit_idx(0) {}
bit_dependency(const bit_dependency& v) = default;
bit_dependency(bit_dependency&& v) = default;
bit_dependency(const pdd& pdd, unsigned bit_idx) : m_pdd(pdd), m_bit_idx(bit_idx) {}
bool operator==(const bit_dependency& other) const {
return m_pdd == other.m_pdd && m_bit_idx == other.m_bit_idx;
}
};
using bit_dependencies = vector<bit_dependency>;
class bit_justication {
protected:
static bit_justication* get_other_justification(const fixed_bits& fixed, const pdd& p, unsigned idx);
static const tbv_ref& get_tbv(fixed_bits& fixed, const pdd& p);
static bool fix_value(fixed_bits& fixed, const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j);
public:
virtual bool has_constraint(constraint*& constr) { return false; }
virtual void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) = 0;
};
class bit_justication_constraint : public bit_justication {
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, bit_dependencies&& dep) : m_constraint(c), m_dependencies(dep) { }
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, bit_dependency v) {
bit_dependencies dep(1);
dep.push_back(std::move(v));
return alloc(bit_justication_constraint, c, std::move(dep));
}
static bit_justication_constraint* mk_binary(constraint* c, bit_dependency v1, bit_dependency v2) {
bit_dependencies dep(2);
dep.push_back(std::move(v1));
dep.push_back(std::move(v2));
return alloc(bit_justication_constraint, c, std::move(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);
// 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);
// 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);
};
// lazy generation of the justifications. Generating them eagerly can generate a huge overhead
class bit_justication_mul : public bit_justication {
unsigned m_idx;
optional<pdd> m_c1, m_c2;
public:
bit_justication_mul() = default;
bit_justication_mul(unsigned idx, const pdd& c1, const pdd& c2) : m_idx(idx), m_c1(c1), m_c2(c2) {}
static tbv_ref& mul(fixed_bits& fixed, const pdd& p, const tbv_ref& in1, const tbv_ref& in2);
void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override;
};
class bit_justication_add : public bit_justication {
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) {}
static tbv_ref& add(fixed_bits& fixed, const pdd& p, const tbv_ref& in1, const tbv_ref& in2);
void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override;
};
class fixed_bits {
friend bit_justication;
solver& m_solver;
scoped_ptr_vector<tbv_manager> m_tbv_managers;
char_vector m_aux_values;
//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_tbv_map = map<pdd_to_tbv_key, tbv_ref, pdd_to_tbv_hash, pdd_to_tbv_eq>;
using tbv_to_justification_key = std::pair<tbv*, unsigned>;
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_tbv_map = map<pdd_to_tbv_key, optional<tbv_ref>, pdd_to_tbv_hash, pdd_to_tbv_eq>;
using tbv_to_justification_key = bit_dependency;
using tbv_to_justification_eq = default_eq<tbv_to_justification_key>;
struct tbv_to_justification_hash {
unsigned operator()(tbv_to_justification_key const& args) const {
return combine_hash((unsigned)args.first, args.second);
return combine_hash((*args.m_pdd).hash(), args.m_bit_idx);
}
};
using tbv_to_justification_map = map<tbv_to_justification_key, bit_justication, tbv_to_justification_hash, tbv_to_justification_eq>;
using tbv_to_justification_map = map<tbv_to_justification_key, bit_justication*, tbv_to_justification_hash, tbv_to_justification_eq>;
vector<optional<tbv_ref>> m_var_to_tbv;
tbv_to_justification_map m_tbv_to_justification;
//vector<optional<tbv_ref>> m_var_to_tbv;
pdd_to_tbv_map m_var_to_tbv;
tbv_to_justification_map m_tbv_to_justification; // the elements are pointers. Deallocate them before replacing them
bool m_consistent = true; // in case evaluating results in a bit-conflict
tbv_manager& get_manager(const pdd& v);
tbv_manager& get_manager(unsigned sz);
void add(tbv_ref& in_out, const tbv_ref& in2);
void multiply(tbv_ref& in_out, const tbv_ref& in2);
tbv_ref& get_tbv(pvar v, unsigned sz);
tbv_ref& get_tbv(const pdd& p);
clause_ref get_explanation(solver& s, bit_justication* j1, bit_justication* j2);
bool fix_value(const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j);
public:
fixed_bits(solver& s) : m_solver(s) {}
fixed_bits(solver& s) : m_solver(s) {}
tbv_ref& get_tbv(const pdd& p);
// #count [min; max]
static std::pair<unsigned, unsigned> leading_zeros(const tbv_ref& ref);
@ -87,16 +174,11 @@ namespace polysat {
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
bool fix_value(solver& s, const pdd& p, unsigned idx, tbit val, constraint* c, bit_dependency& dep);
bool fix_value(solver& s, const pdd& p, unsigned idx, tbit val, constraint* c, std::pair<pdd, unsigned> v1, std::pair<pdd, unsigned> v2) {
bit_dependency dep(2);
dep.push_back(v1);
dep.push_back(v2);
return fix_value(s, p, idx, val, c, dep);
}
// 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);
void clear_value(const pdd& p, unsigned idx);
tbv_ref eval(const pdd& p);
tbv_ref& eval(solver& s, const pdd& p);
};
};
}

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

@ -277,6 +277,12 @@ 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
*
@ -353,9 +359,10 @@ namespace polysat {
}
bool op_constraint::propagate_bits_shl(solver& s, bool is_positive) {
tbv_ref p_val = s.m_fixed_bits.eval(m_p);
tbv_ref q_val = s.m_fixed_bits.eval(m_q);
tbv_ref r_val = s.m_fixed_bits.eval(m_r);
// 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);
unsigned sz = m_p.power_of_2();
auto [shift_min, shift_max] = s.m_fixed_bits.min_max(q_val);
@ -374,15 +381,34 @@ namespace polysat {
SASSERT(shift_max_u <= sz);
SASSERT(shift_min_u <= shift_max_u);
unsigned span = shift_max_u - shift_min_u;
for (unsigned i = 0; i < shift_min_u; i++) {
if (!s.m_fixed_bits.fix_value(s, m_r, i, BIT_0, this, s.))
return false;
// 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_value(s, m_r, i, BIT_0, bit_justication_constraint::mk_justify_at_least(this, m_q, q_val, rational(i + 1))))
return false;
}
}
for (unsigned i = shift_min_u; i < sz; i++) {
propagate_bit(s, m_r.var(), i, p_val[i - shift_min_u]);
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_value(s, m_r, i, val, bit_justication_constraint::mk_justify_between(this, m_q, q_val, shift_min, shift_max)))
return false;
}
}
return true;
}
void op_constraint::activate_and(solver& s) {
@ -499,12 +525,13 @@ namespace polysat {
}
bool op_constraint::propagate_bits_and(solver& s, bool is_positive){
tbv_ref p_val = s.m_fixed_bits.eval(m_p);
tbv_ref q_val = s.m_fixed_bits.eval(m_q);
tbv_ref r_val = s.m_fixed_bits.eval(m_r);
// 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);
unsigned sz = m_p.power_of_2();
for (int i = 0; i < sz; i++) {
for (unsigned i = 0; i < sz; i++) {
tbit bp = p_val[i];
tbit bq = q_val[i];
tbit br = r_val[i];
@ -512,11 +539,12 @@ namespace polysat {
// TODO: Propagate from the result to the operands. e.g., 110... = xx1... & yyy...
// TODO: ==> x = 111..., y = 110...
if (bp == BIT_0 || bq == BIT_0) {
if (!s.m_fixed_bits.fix_value(s, m_r, i, BIT_0, this, std::pair(m_p, i), std::pair(m_q, i)))
// 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 })))
return false;
}
else if (bp == BIT_1 && bq == BIT_1) {
if (!s.m_fixed_bits.fix_value(s, m_r, i, BIT_1, this, std::pair(m_p, i), std::pair(m_q, i)))
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 })))
return false;
}
}

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

@ -31,6 +31,7 @@ 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),

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

@ -105,6 +105,7 @@ namespace polysat {
stats() { reset(); }
};
// TODO: Why so many friends? Can't we just make the relevant functions public?
friend class assignment;
friend class constraint;
friend class ule_constraint;
@ -118,6 +119,7 @@ namespace polysat {
friend class conflict_explainer;
friend class simplify_clause;
friend class simplify;
friend class fixed_bits;
friend class restart;
friend class explainer;
friend class inference_engine;