mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

output

Browse source
This commit is contained in:
Jakob Rath 2022-10-04 14:09:57 +02:00
parent 9cc9d1fac4
commit 46c69766d1
2 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1113,8 +1113,10 @@ namespace polysat {
std::ostream& lit_pp::display(std::ostream& out) const { std::ostream& lit_pp::display(std::ostream& out) const {
auto c = s.lit2cnstr(lit); auto c = s.lit2cnstr(lit);
out << lpad(4, lit) << ": " << rpad(30, c) << " ["; out << lpad(4, lit) << ": " << rpad(30, c);
out << " " << s.m_bvars.value(lit); if (!c)
return out;
out << " [ " << s.m_bvars.value(lit);
if (s.m_bvars.is_assigned(lit)) { if (s.m_bvars.is_assigned(lit)) {
out << ' '; out << ' ';
if (s.m_bvars.is_assumption(lit)) if (s.m_bvars.is_assumption(lit))
@ -1123,6 +1125,8 @@ namespace polysat {
out << "bprop"; out << "bprop";
else if (s.m_bvars.is_value_propagation(lit)) else if (s.m_bvars.is_value_propagation(lit))
out << "eval"; out << "eval";
else if (s.m_bvars.is_decision(lit))
out << "decide";
out << '@' << s.m_bvars.level(lit); out << '@' << s.m_bvars.level(lit);
} }
if (c->is_pwatched()) if (c->is_pwatched())

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

@ -457,7 +457,7 @@ namespace polysat {
solver const& s; solver const& s;
sat::literal lit; sat::literal lit;
public: public:
lit_pp(solver const& s, signed_constraint c): s(s), lit(c.blit()) {} lit_pp(solver const& s, signed_constraint c): s(s), lit(c ? c.blit() : sat::null_literal) {}
lit_pp(solver const& s, sat::literal lit): s(s), lit(lit) {} lit_pp(solver const& s, sat::literal lit): s(s), lit(lit) {}
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
}; };