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

lit_pp with extra information

Browse source
This commit is contained in:
Jakob Rath 2022-08-17 09:29:00 +02:00
parent 618b3945c1
commit 201d841a90
2 changed files with 23 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -920,7 +920,7 @@ namespace polysat {
void solver::add_clause(clause& clause) {
LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
for (sat::literal lit : clause) {
LOG(" Literal " << lit << " is: " << lit2cnstr(lit));
LOG(" Literal " << lit << " is: " << lit_pp(*this, lit));
// SASSERT(m_bvars.value(lit) != l_true);
// it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint
if (m_bvars.value(lit) == l_true) {
@ -1046,6 +1046,17 @@ namespace polysat {
return out;
}
std::ostream& lit_pp::display(std::ostream& out) const {
auto c = s.lit2cnstr(lit);
out << lit << ": " << c << " [";
out << " bvalue=" << s.m_bvars.value(lit);
if (s.m_bvars.is_assigned(lit))
out << " @" << s.m_bvars.level(lit);
out << " pwatched=" << c->is_pwatched();
out << " ]";
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))

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

@ -80,6 +80,7 @@ namespace polysat {
friend class viable_fallback;
friend class search_state;
friend class num_pp;
friend class lit_pp;
friend class assignment_pp;
friend class assignments_pp;
friend class ex_polynomial_superposition;
@ -420,6 +421,14 @@ namespace polysat {
std::ostream& display(std::ostream& out) const;
};
class lit_pp {
solver const& s;
sat::literal lit;
public:
lit_pp(solver const& s, sat::literal lit): s(s), lit(lit) {}
std::ostream& display(std::ostream& out) const;
};
/** Format value 'val' as member of the domain of 'var' */
class num_pp {
solver const& s;
@ -434,6 +443,8 @@ namespace polysat {
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, assignment_pp const& p) { return p.display(out); }
inline std::ostream& operator<<(std::ostream& out, assignments_pp const& a) { return a.display(out); }