mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

display

Browse source
This commit is contained in:
Jakob Rath 2023-07-12 15:46:40 +02:00
parent f12a7d62ab
commit f61bf0843b
3 changed files with 38 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -703,35 +703,46 @@ namespace polysat {
base.reset(); base.reset();
slice const vs = var2slice(v); slice const vs = var2slice(v);
find_base(vs, base); find_base(vs, base);
// unsigned hi = width(var2slice(v)) - 1; for (slice s : base)
for (slice s : base) {
// unsigned w = width(s);
// unsigned lo = hi - w + 1;
// out << " s" << s << "_[" << hi << ":" << lo << "]";
// hi -= w;
display(out << " ", s); display(out << " ", s);
} // if (has_value(vs)) {
if (has_value(vs)) { // out << " -- (val:" << get_value(vs) << ")";
out << " -- (val:" << get_value(vs) << ")"; // }
}
out << "\n"; out << "\n";
} }
for (pvar v = 0; v < m_var2slice.size(); ++v) {
out << "v" << v << ":";
slice const s = m_var2slice[v];
}
return out; return out;
} }
std::ostream& slicing::display_tree(std::ostream& out, char const* name, slice s) const { std::ostream& slicing::display_tree(std::ostream& out) const {
// TODO for (pvar v = 0; v < m_var2slice.size(); ++v) {
out << "v" << v << ":\n";
slice const s = var2slice(v);
display_tree(out, s, 4, width(s) - 1, 0);
}
return out;
}
std::ostream& slicing::display_tree(std::ostream& out, slice s, unsigned indent, unsigned hi, unsigned lo) const {
out << std::string(indent, ' ') << "[" << hi << ":" << lo << "]";
out << " id=" << s;
out << " w=" << width(s);
if (find(s) != s)
out << " root=" << find(s);
// if (has_value(s))
// out << " value=" << get_value(s);
out << "\n";
if (has_sub(s)) {
unsigned cut = m_slice_cut[s];
display_tree(out, sub_hi(s), indent + 4, hi, cut + 1 + lo);
display_tree(out, sub_lo(s), indent + 4, cut + lo, lo);
}
return out;
} }
std::ostream& slicing::display(std::ostream& out, slice s) const { std::ostream& slicing::display(std::ostream& out, slice s) const {
out << "{id:" << s << ",w:" << width(s); out << "{id:" << s << ",w:" << width(s);
if (has_value(s)) { // if (has_value(s))
out << ",val:" << get_value(s); // out << ",val:" << get_value(s);
}
out << "}"; out << "}";
return out; return out;
} }

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

@ -250,8 +250,10 @@ namespace polysat {
void propagate(signed_constraint c); void propagate(signed_constraint c);
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
std::ostream& display_tree(std::ostream& out, char const* name, slice s) const;
std::ostream& display(std::ostream& out, slice s) const; std::ostream& display(std::ostream& out, slice s) const;
std::ostream& display_tree(std::ostream& out) const;
std::ostream& display_tree(std::ostream& out, slice s, unsigned indent, unsigned hi, unsigned lo) const;
}; };
inline std::ostream& operator<<(std::ostream& out, slicing const& s) { return s.display(out); } inline std::ostream& operator<<(std::ostream& out, slicing const& s) { return s.display(out); }

8
src/test/slicing.cpp
View file

@ -49,6 +49,8 @@ namespace polysat {
sl.find_base(sl.var2slice(y), y_base); sl.find_base(sl.var2slice(y), y_base);
VERIFY(sl.merge(x_base, y_base, sat::literal(3))); VERIFY(sl.merge(x_base, y_base, sat::literal(3)));
std::cout << sl << "\n"; std::cout << sl << "\n";
sl.display_tree(std::cout);
} }
// x[7:3] = a // x[7:3] = a
@ -185,9 +187,9 @@ namespace polysat {
void tst_slicing() { void tst_slicing() {
using namespace polysat; using namespace polysat;
test_slicing::test1(); test_slicing::test1();
test_slicing::test2(); // test_slicing::test2();
test_slicing::test3(); // test_slicing::test3();
test_slicing::test4(); // test_slicing::test4();
// test_slicing::test5(); // test_slicing::test5();
std::cout << "ok\n"; std::cout << "ok\n";
} }