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

fixing fixed-bits viable

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-11 11:09:06 -08:00
parent 0d3a465e75
commit 9fb86a4d4f
6 changed files with 18 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -34,10 +34,12 @@ namespace polysat {
bool fixed_bits::check(rational const& val, fi_record& fi) {
unsigned sz = c.size(m_var);
rational bw = rational::power_of_two(sz);
// verbose_stream() << "check for fixed bits v" << m_var << "[" << sz << "] := " << val << "\n";
for (auto const& s : m_fixed_slices) {
rational sbw = rational::power_of_two(s.length);
// slice is properly contained in bit-vector variable
if (s.length <= sz && s.value != mod(machine_div2k(val, s.offset + 1), sbw)) {
// verbose_stream() << " slice " << s.value << "[" << s.length << "]@" << s.offset << "\n";
if (s.length <= sz && s.value != mod(machine_div2k(val, s.offset), sbw)) {
SASSERT(s.offset + s.length <= sz);
rational hi_val = s.value;
rational lo_val = mod(s.value + 1, sbw);
@ -46,6 +48,7 @@ namespace polysat {
fi.reset();
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
fi.deps.push_back(dependency({ m_var, s }));
fi.bit_width = s.length;
fi.coeff = 1;
return false;
@ -59,7 +62,7 @@ namespace polysat {
pdd hi = c.value(hi_val, sz);
fi.reset();
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
fi.deps.push_back(dependency({ m_var, s }));
fi.deps.push_back(dependency({ m_var, s }));
fi.bit_width = sz;
fi.coeff = 1;
return false;

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

@ -21,6 +21,11 @@ Author:
namespace polysat {
std::ostream& operator<<(std::ostream& out, fi_record const& fi) {
out << "fi_record(bw = " << fi.bit_width << ", coeff = " << fi.coeff << ", " << fi.interval << ", " << fi.src << fi.side_cond << fi.deps << ")";
return out;
}
/**
*
* \param[in] c Original constraint

2
src/sat/smt/polysat/forbidden_intervals.h
View file

@ -49,6 +49,8 @@ namespace polysat {
};
};
std::ostream& operator<<(std::ostream& out, fi_record const& fi);
class forbidden_intervals {
void push_eq(bool is_trivial, pdd const& p, vector<signed_constraint>& side_cond);

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

@ -47,7 +47,7 @@ namespace polysat {
pvar v;
fixed_claim() = default;
fixed_claim(pvar v, rational value, unsigned offset, unsigned length) : fixed_slice(value, offset, length), v(v) {}
fixed_claim(pvar, fixed_slice const& s) : fixed_slice(s), v(v) {}
fixed_claim(pvar v, fixed_slice const& s) : fixed_slice(s), v(v) {}
};
struct offset_slice {

11
src/sat/smt/polysat/viable.cpp
View file

@ -92,7 +92,6 @@ namespace polysat {
m_conflict = false;
m_propagation = false;
// verbose_stream() << "find viable v" << v << " starting with " << lo << "\n";
for (unsigned rounds = 0; rounds < 10; ) {
@ -361,9 +360,6 @@ namespace polysat {
}
bool viable::check_fixed_bits(pvar v, rational const& val) {
// disable fixed bits for now
return true;
auto e = alloc_entry(v, constraint_id::null());
if (m_fixed_bits.check(val, *e)) {
m_alloc.push_back(e);
@ -371,6 +367,7 @@ namespace polysat {
}
else {
intersect(v, e);
TRACE("bv", tout << "fixed " << *e << "\n");
return false;
}
}
@ -391,11 +388,6 @@ namespace polysat {
m_diseq_lin[v] = m_diseq_lin[v]->next();
do {
// IF_LOGGING(
// verbose_stream() << "refine-disequal-lin for v" << v << " in src: ";
// for (const auto& src : e->src)
// verbose_stream() << lit_pp(s, src) << "\n";
// );
// We compute an interval if the concrete value 'val' violates the constraint:
// p*val + q > r*val + s if e->src.is_positive()
@ -806,7 +798,6 @@ namespace polysat {
bool viable::intersect(pvar v, entry* ne) {
SASSERT(!c.is_assigned(v));
SASSERT(!ne->src.empty());
entry*& entries = m_units[v].ensure_layer(ne->bit_width).entries;
entry* e = entries;
if (e && e->interval.is_full()) {

12
src/sat/smt/polysat_egraph.cpp
View file

@ -94,26 +94,22 @@ namespace polysat {
// walk the e-graph to retrieve fixed overlaps
void solver::get_fixed_bits(pvar pv, fixed_bits_vector& out) {
std::function<bool(euf::enode*, unsigned)> consume_slice = [&](euf::enode* n, unsigned offset) {
// verbose_stream() << "sub-slice " << ctx.bpp(n) << " " << offset << "\n";
n = n->get_root();
if (!n->interpreted())
return true;
auto w = n->get_root()->get_th_var(get_id());
auto w = n->get_th_var(get_id());
if (w == euf::null_theory_var)
return true;
auto const& p = m_var2pdd[w];
if (!p.is_var())
return true;
unsigned length = bv.get_bv_size(n->get_expr());
rational value;
VERIFY(bv.is_numeral(n->get_expr(), value));
out.push_back({ fixed_slice(value, offset, length) });
return false;
};
theory_var v = m_pddvar2var[pv];
// verbose_stream() << "Get fixed_bits " << ctx.bpp(var2enode(v)) << "\n";
theory_var v = m_pddvar2var[pv];
m_bv_plugin->sub_slices(var2enode(v), consume_slice);
m_bv_plugin->super_slices(var2enode(v), consume_slice);
}
void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function<void(euf::enode*, euf::enode*)>& consume_eq) {