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

clause_pp

Browse source
This commit is contained in:
Jakob Rath 2023-07-26 09:14:38 +02:00
parent 1e5255508c
commit e6e655f0eb
2 changed files with 17 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1626,6 +1626,13 @@ namespace polysat {
return out;
}
std::ostream& clause_pp::display(std::ostream& out) const {
out << cl << "\n";
for (sat::literal lit : cl)
out << " " << lit_pp(s, lit) << "\n";
return out;
}
std::ostream& num_pp::display(std::ostream& out) const {
return out << dd::val_pp(s.var2pdd(var), val, require_parens);
}

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

@ -677,6 +677,15 @@ namespace polysat {
std::ostream& display(std::ostream& out) const;
};
class clause_pp {
solver const& s;
clause const& cl;
public:
clause_pp(solver const& s, clause const& cl): s(s), cl(cl) {}
clause_pp(solver const& s, clause_ref const& cl): s(s), cl(*cl) {}
std::ostream& display(std::ostream& out) const;
};
/** Format value 'val' as member of the domain of 'var' */
class num_pp {
solver const& s;
@ -689,13 +698,10 @@ namespace polysat {
};
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, lit_pp const& l) { return l.display(out); }
inline std::ostream& operator<<(std::ostream& out, clause_pp const& c) { return c.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); }
}