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

make offset_claim structured similar to fixed_claim

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-25 11:19:37 -08:00
parent b1072d0a1c
commit f0c23f9b7b
3 changed files with 24 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/polysat/fixed_bits.cpp
View file

@ -41,11 +41,12 @@ namespace polysat {
// val 1011
// next 1100
// algorith: Let i be the most significant index where fixed bits disagree with val.
// algorithm: Let i be the most significant index where fixed bits disagree with val.
// Set non-fixed values below i to 0.
// If m_fixed[i] == l_true; then updating val to mask by fixed bits sufficies.
// Otherwise, the range above the disagreement has to be incremented.
// Increment the non-fixed bits by 1
// The first non-fixed 0 position is set to 1, non-fixed positions below are set to 0.s
// The first non-fixed 0 position is set to 1, non-fixed positions below are set to 0.
// If there are none, then the value is maximal and we return false.
bool fixed_bits::next(rational& val) {

20
src/sat/smt/polysat/types.h
View file

@ -29,7 +29,7 @@ namespace polysat {
using pvar_vector = unsigned_vector;
using theory_var_pair = std::pair<theory_var, theory_var>;
using offset_claim = std::tuple<pvar, pvar, unsigned>;
inline const pvar null_var = UINT_MAX;
class signed_constraint;
@ -54,6 +54,12 @@ namespace polysat {
unsigned offset;
};
struct offset_claim : public offset_slice {
pvar w;
offset_claim() = default;
offset_claim(pvar w, offset_slice const& s) : offset_slice(s), w(w) {}
};
class dependency {
struct axiom_t {};
std::variant<axiom_t, sat::bool_var, theory_var_pair, offset_claim, fixed_claim> m_data;
@ -87,9 +93,17 @@ namespace polysat {
return out << d.bool_var();
else if (d.is_eq())
return out << "v" << d.eq().first << " == v" << d.eq().second;
else if (d.is_offset_claim()) {
auto offs = d.offset();
return out << "v" << offs.v << " == v" << offs.w << " offset " << offs.offset;
}
else if (d.is_fixed_claim()) {
auto fixed = d.fixed();
return out << fixed.value << " == v" << fixed.v << " [" << fixed.hi << ":" << fixed.lo << "]";
}
else {
auto [v1, v2, offset] = d.offset();
return out << "v" << v1 << " == v" << v2 << " offset " << offset;
UNREACHABLE();
return out;
}
}

8
src/sat/smt/polysat_solver.cpp
View file

@ -212,12 +212,12 @@ namespace polysat {
return level;
}
else if (d.is_offset_claim()) {
auto [v, w, offset] = d.offset();
auto const& offs = d.offset();
sat::literal_vector lits;
std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
ctx.get_eq_antecedents(a, b, lits);
};
explain_slice(v, w, offset, consume);
explain_slice(offs.v, offs.w, offs.offset, consume);
unsigned level = 0;
for (auto lit : lits)
level = std::max(level, s().lvl(lit));
@ -287,11 +287,11 @@ namespace polysat {
lits.push_back(~eq_internalize(var2enode(v1), var2enode(v2)));
}
else if (d.is_offset_claim()) {
auto [v, w, offset] = d.offset();
auto const& o = d.offset();
std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
lits.push_back(~eq_internalize(a, b));
};
explain_slice(v, w, offset, consume);
explain_slice(o.v, o.w, o.offset, consume);
}
else if (d.is_fixed_claim()) {
auto const& f = d.fixed();