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

slicing::collect_fixed should start at low-order base slice

Browse source
This commit is contained in:
Jakob Rath 2023-08-11 14:49:17 +02:00
parent 89f0fb05a5
commit 586dcba661
2 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1371,14 +1371,16 @@ namespace polysat {
get_base(var2slice(v), base);
rational a;
unsigned lo = 0;
for (enode* n : base) {
enode* r = n->get_root();
for (auto it = base.rbegin(); it != base.rend(); ++it) {
enode* const n = *it;
enode* const 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, n});
lo += w;
}
base.reset();
}
void slicing::explain_fixed(euf::enode* const n, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) {

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

@ -39,9 +39,11 @@ namespace polysat {
friend class test_slicing;
public:
using enode = euf::enode;
using enode_vector = euf::enode_vector;
private:
class dep_t {
std::variant<std::monostate, sat::literal, unsigned> m_data;
public:
@ -351,7 +353,7 @@ namespace polysat {
/** Collect fixed portions of the variable v */
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);
void explain_fixed(enode* just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
std::ostream& display(std::ostream& out) const;
std::ostream& display_tree(std::ostream& out) const;