mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-30 18:08:46 +00:00
Code Activity

display

Browse source
This commit is contained in:
Jakob Rath 2024-03-12 16:24:28 +01:00
parent 450ed26440
commit 35e3211ca8
1 changed files with 11 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -922,8 +922,8 @@ namespace polysat {
} }
/// Let x = concat(y, z) and x not in [lo;hi[. /// Let x = concat(y, z) and x not in [lo;hi[.
/// Returns an interval I such that z not in I. /// Returns an interval I such that z not in I.
r_interval viable::chop_off_upper(r_interval const& i, unsigned const Ny, unsigned const Nz, rational const* y_fixed_value) { r_interval viable::chop_off_upper(r_interval const& i, unsigned const Ny, unsigned const Nz, rational const* y_fixed_value) {
if (i.is_full()) if (i.is_full())
return r_interval::full(); return r_interval::full();
@ -1097,8 +1097,9 @@ namespace polysat {
} }
/* /*
* Register constraint at index 'idx' as unitary in v. * Register constraint at index 'idx' as unitary in v.
*/ * Returns 'multiple' when either intervals are unchanged or there really are multiple values left.
*/
find_t viable::add_unitary(pvar v, constraint_id idx, rational& var_value) { find_t viable::add_unitary(pvar v, constraint_id idx, rational& var_value) {
if (c.is_assigned(v)) if (c.is_assigned(v))
@ -1471,7 +1472,7 @@ namespace polysat {
e = e->next(); e = e->next();
++count; ++count;
if (count > 10) { if (count > 10) {
out << " ..."; out << " ... (total: " << count << " entries)";
break; break;
} }
} }
@ -1484,9 +1485,7 @@ namespace polysat {
for (auto const& layer : m_units[v].get_layers()) { for (auto const& layer : m_units[v].get_layers()) {
if (!layer.entries) if (!layer.entries)
continue; continue;
out << "v" << v << ": "; out << "v" << v << "[" << layer.bit_width << "]: ";
if (layer.bit_width != c.size(v))
out << "width[" << layer.bit_width << "] ";
display_all(out, layer.entries, " "); display_all(out, layer.entries, " ");
out << "\n"; out << "\n";
} }
@ -1495,11 +1494,11 @@ namespace polysat {
} }
std::ostream& viable::display_state(std::ostream& out) const { std::ostream& viable::display_state(std::ostream& out) const {
out << "v" << m_var << ": "; out << "v" << m_var << ":";
for (auto const& slice : m_overlaps) { for (auto const& slice : m_overlaps) {
out << "v" << slice.v << ":" << c.size(slice.v) << "@" << slice.offset << " "; out << " v" << slice.v << ":" << c.size(slice.v) << "@" << slice.offset;
if (c.is_assigned(slice.v)) if (c.is_assigned(slice.v))
out << "value(" << c.get_assignment().value(slice.v) << ") "; out << " value=" << c.get_assignment().value(slice.v);
} }
out << "\n"; out << "\n";
return out; return out;
@ -1508,7 +1507,7 @@ namespace polysat {
std::ostream& viable::display_explain(std::ostream& out) const { std::ostream& viable::display_explain(std::ostream& out) const {
display_state(out); display_state(out);
for (auto const& e : m_explain) for (auto const& e : m_explain)
display_one(out << "v" << m_var << "[" << e.e->bit_width << "] : = " << e.value << " ", e.e) << "\n"; display_one(out << "v" << m_var << "[" << e.e->bit_width << "] := " << e.value << " ", e.e) << "\n";
return out; return out;
} }