mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

display_explain

Browse source
This commit is contained in:
Jakob Rath 2024-03-28 16:38:41 +01:00
parent a7c84da44d
commit 0d3e88fd31
2 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1208,11 +1208,15 @@ namespace polysat {
out << "explain_kind " << m_explain_kind << "\n";
display_state(out);
for (auto const& e : m_explain)
display_one(out << "v" << m_var << "[" << e.e->bit_width << "] := " << e.value << " ", e.e) << "\n";
display_explain(out, e) << "\n";
return out;
}
/*
std::ostream& viable::display_explain(std::ostream& out, explanation const& e) const {
return display_one(out << "v" << e.e->var << "[" << e.e->bit_width << "] := " << e.value << " ", e.e);
}
/*
* Lower bounds are strictly ascending.
* Intervals don't contain each-other (since lower bounds are ascending, it suffices to check containment in one direction).
*/

1
src/sat/smt/polysat/viable.h
View file

@ -153,6 +153,7 @@ namespace polysat {
void init_overlaps(pvar v);
std::ostream& display_state(std::ostream& out) const;
std::ostream& display_explain(std::ostream& out) const;
std::ostream& display_explain(std::ostream& out, explanation const& e) const;
public:
viable(core& c);