mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 15:53:41 +00:00
Code Activity

more pp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-20 10:13:59 -07:00
parent 4066087138
commit d78313e001
2 changed files with 15 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -125,7 +125,7 @@ namespace polysat {
LOG_H1("Next solving loop iteration"); LOG_H1("Next solving loop iteration");
LOG("Free variables: " << m_free_vars); LOG("Free variables: " << m_free_vars);
LOG("Assignment: " << assignments_pp(*this)); LOG("Assignment: " << assignments_pp(*this));
LOG("Conflict: " << m_conflict); if (!m_conflict.empty()) LOG("Conflict: " << m_conflict);
IF_LOGGING(log_viable()); IF_LOGGING(log_viable());
if (pending_disjunctive_lemma()) { LOG_H2("UNDEF (handle lemma externally)"); return l_undef; } if (pending_disjunctive_lemma()) { LOG_H2("UNDEF (handle lemma externally)"); return l_undef; }
@ -444,7 +444,7 @@ namespace polysat {
++m_stats.m_num_decisions; ++m_stats.m_num_decisions;
else else
++m_stats.m_num_propagations; ++m_stats.m_num_propagations;
LOG("v" << v << " := " << val << " by " << j); LOG(assignment_pp(*this, v, val) << " by " << j);
SASSERT(is_viable(v, val)); SASSERT(is_viable(v, val));
SASSERT(std::all_of(assignment().begin(), assignment().end(), [v](auto p) { return p.first != v; })); SASSERT(std::all_of(assignment().begin(), assignment().end(), [v](auto p) { return p.first != v; }));
m_value[v] = val; m_value[v] = val;
@ -458,6 +458,7 @@ namespace polysat {
void solver::set_conflict(constraint& c) { void solver::set_conflict(constraint& c) {
LOG("Conflict: " << c); LOG("Conflict: " << c);
LOG(*this);
SASSERT(!is_conflict()); SASSERT(!is_conflict());
m_conflict.push_back(&c); m_conflict.push_back(&c);
} }
@ -516,6 +517,7 @@ namespace polysat {
*/ */
void solver::resolve_conflict() { void solver::resolve_conflict() {
LOG_H2("Resolve conflict"); LOG_H2("Resolve conflict");
LOG_H2(*this);
++m_stats.m_num_conflicts; ++m_stats.m_num_conflicts;
SASSERT(is_conflict()); SASSERT(is_conflict());
@ -1201,11 +1203,13 @@ namespace polysat {
} }
std::ostream& solver::display(std::ostream& out) const { std::ostream& solver::display(std::ostream& out) const {
for (auto p : assignment()) { for (auto [v, val] : assignment()) {
auto v = p.first; auto j = m_justification[v];
auto lvl = m_justification[v].level(); out << assignment_pp(*this, v, val) << " @" << j.level();
out << "v" << v << " := " << p.second << " @" << lvl << "\n"; if (j.is_propagation())
out << m_viable[v] << "\n"; out << " " << m_cjust[v];
out << "\n";
// out << m_viable[v] << "\n";
} }
out << "Original:\n"; out << "Original:\n";
for (auto* c : m_original) for (auto* c : m_original)

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

@ -383,18 +383,18 @@ namespace polysat {
}; };
class assignments_pp { class assignments_pp {
solver& s; solver const& s;
public: public:
assignments_pp(solver& s): s(s) {} assignments_pp(solver const& s): s(s) {}
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
}; };
class assignment_pp { class assignment_pp {
solver& s; solver const& s;
pvar var; pvar var;
rational const& val; rational const& val;
public: public:
assignment_pp(solver& s, pvar var, rational const& val): s(s), var(var), val(val) {} assignment_pp(solver const& s, pvar var, rational const& val): s(s), var(var), val(val) {}
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
}; };