mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

use struct

Browse source
This commit is contained in:
Jakob Rath 2023-08-08 17:19:46 +02:00
parent 3573305917
commit 6eb81fbb9d
3 changed files with 16 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/polysat/slicing.cpp
View file

@ -1363,7 +1363,7 @@ namespace polysat {
SASSERT(all_of(m_egraph.nodes(), [](enode* n) { return !n->is_marked1(); }));
}
void slicing::collect_fixed(pvar v, fixed_bits_vector& out, euf::enode_vector& out_just) {
void slicing::collect_fixed(pvar v, justified_fixed_bits_vector& out) {
enode_vector& base = m_tmp2;
SASSERT(base.empty());
get_base(var2slice(v), base);
@ -1373,10 +1373,8 @@ namespace polysat {
enode* r = n->get_root();
unsigned const w = width(n);
unsigned const hi = lo + w - 1;
if (try_get_value(r, a)) {
out.push_back({hi, lo, a});
out_just.push_back(n);
}
if (try_get_value(r, a))
out.push_back({hi, lo, a, n});
lo += w;
}
}

10
src/math/polysat/slicing.h
View file

@ -338,8 +338,16 @@ namespace polysat {
/** For a given variable v, find the set of variables w such that w = v[|w|:0]. */
void collect_simple_overlaps(pvar v, pvar_vector& out);
struct justified_fixed_bits : public fixed_bits {
enode* just;
justified_fixed_bits(unsigned hi, unsigned lo, rational value, enode* just): fixed_bits(hi, lo, value), just(just) {}
};
using justified_fixed_bits_vector = vector<justified_fixed_bits>;
/** Collect fixed portions of the variable v */
void collect_fixed(pvar v, fixed_bits_vector& out, enode_vector& out_just);
void collect_fixed(pvar v, justified_fixed_bits_vector& out);
void explain_fixed(euf::enode* just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
std::ostream& display(std::ostream& out) const;

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

@ -975,18 +975,15 @@ namespace {
#if 0
// TODO: wip
fixed_bits_vector fbs;
euf::enode_vector fbs_just;
s.m_slicing.collect_fixed(v, fbs, fbs_just);
slicing::justified_fixed_bits_vector fbs;
s.m_slicing.collect_fixed(v, fbs);
for (unsigned idx = fbs.size(); idx-- > 0; ) {
fixed_bits const& fb = fbs[idx];
euf::enode_pair const& just = fbs_just[idx];
for (auto const& fb : fbs) {
for (unsigned i = fb.lo; i <= fb.hi; ++i) {
SASSERT(out_fbi.just_src[i].empty()); // since we don't get overlapping ranges from collect_fixed.
SASSERT(out_fbi.just_side_cond[i].empty());
out_fbi.fixed[i] = to_lbool(fb.value.get_bit(i - fb.lo));
// TODO: can add an euf::enode_pair to the fixed_bits_info. then we do not have to call explain_fixed() here already.
// TODO: can add an euf::enode* to the fixed_bits_info. then we do not have to call explain_fixed() here already.
// TODO: s.m_slicing.explain_fixed( ... ); with out_fbi.just_src[i].push_back(...)
}
}