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

improve output

Browse source
This commit is contained in:
Jakob Rath 2022-07-14 10:47:35 +02:00
parent 003896991d
commit c31503f67d
4 changed files with 29 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/conflict.cpp
View file

@ -80,11 +80,11 @@ namespace polysat {
m_used_vars.insert(v);
}
for (auto v : core.vars()) {
out_indent() << "v" << v << " := " << core.s.get_value(v) << "\n";
out_indent() << assignment_pp(core.s, v, core.s.get_value(v)) << "\n";
m_used_vars.insert(v);
}
for (auto v : core.bail_vars()) {
out_indent() << "v" << v << " := " << core.s.get_value(v) << " (bail)\n";
out_indent() << assignment_pp(core.s, v, core.s.get_value(v)) << " (bail)\n";
m_used_vars.insert(v);
}
if (core.is_bailout())

17
src/math/polysat/search_state.cpp
View file

@ -21,22 +21,17 @@ namespace polysat {
std::ostream& search_state::display_verbose(search_item const& item, std::ostream& out) const {
switch (item.kind()) {
case search_item_k::assignment: {
rational r;
pvar const v = item.var();
auto const& j = s.m_justification[v];
out << "v" << std::setw(3) << std::left << v << " := ";
out << std::setw(30) << std::left << s.m_value[v];
// if (value(item.var(), r)) {
// SASSERT_EQ(r, s.m_value[v]);
// out << r;
// } else
// out << "*";
pvar const var = item.var();
rational const& val = s.m_value[var];
auto const& j = s.m_justification[var];
out << "v" << std::setw(3) << std::left << var << " := ";
out << std::setw(30) << std::left << num_pp(s, var, val);
out << " @" << j.level();
switch (j.kind()) {
case justification_k::decision:
return out << " by decision";
case justification_k::propagation:
return out << " by " << viable::var_pp(s.m_viable, v);
return out << " by " << viable::var_pp(s.m_viable, var);
case justification_k::unassigned:
return out << " unassigned";
}

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

@ -1185,17 +1185,20 @@ namespace polysat {
}
std::ostream& assignment_pp::display(std::ostream& out) const {
out << "v" << var << " := ";
out << "v" << var << " := " << num_pp(s, var, val);
if (with_justification)
out << " (" << s.m_justification[var] << ")";
return out;
}
std::ostream& num_pp::display(std::ostream& out) const {
rational const& p = rational::power_of_two(s.size(var));
if (val > mod(-val, p))
out << -mod(-val, p);
else
out << val;
if (with_justification)
out << " (" << s.m_justification[var] << ")";
return out;
}
void solver::collect_statistics(statistics& st) const {
st.update("polysat iterations", m_stats.m_num_iterations);

14
src/math/polysat/solver.h
View file

@ -78,6 +78,7 @@ namespace polysat {
friend class viable;
friend class viable_fallback;
friend class search_state;
friend class num_pp;
friend class assignment_pp;
friend class assignments_pp;
friend class ex_polynomial_superposition;
@ -429,12 +430,25 @@ namespace polysat {
std::ostream& display(std::ostream& out) const;
};
/** Format value 'val' as member of the domain of 'var' */
class num_pp {
solver const& s;
pvar var;
rational const& val;
public:
num_pp(solver const& s, pvar var, rational const& val): s(s), var(var), val(val) {}
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, solver const& s) { return s.display(out); }
inline std::ostream& operator<<(std::ostream& out, num_pp const& v) { return v.display(out); }
inline std::ostream& operator<<(std::ostream& out, assignment_pp const& p) { return p.display(out); }
inline std::ostream& operator<<(std::ostream& out, assignments_pp const& a) { return a.display(out); }
}