From 0fb8c72f50684db328babbb1f47d2e3c0e899a03 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 29 Jun 2022 14:26:25 +0200 Subject: [PATCH] print more information --- src/math/polysat/conflict.cpp | 10 +++--- src/math/polysat/conflict.h | 2 +- src/math/polysat/explain.cpp | 52 ++++++++++++++++++++---------- src/math/polysat/op_constraint.cpp | 4 +-- src/math/polysat/op_constraint.h | 4 +-- src/math/polysat/solver.cpp | 3 +- src/math/polysat/viable.cpp | 6 ++-- src/math/polysat/viable.h | 6 ++-- 8 files changed, 53 insertions(+), 34 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 4d7377c3b..db6a53271 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -53,16 +53,16 @@ namespace polysat { std::string hline() const { return std::string(70, '-'); } public: - void begin_conflict() { + void begin_conflict(char const* text) { ++m_conflicts; - LOG("Begin CONFLICT #" << m_conflicts); + LOG("Begin CONFLICT #" << m_conflicts << " (" << text << ")"); m_used_constraints.reset(); m_used_vars.reset(); if (!m_out) m_out = alloc(std::ofstream, "conflicts.txt"); else out() << "\n\n\n\n\n\n\n\n\n\n\n\n"; - out() << "CONFLICT #" << m_conflicts << "\n"; + out() << "CONFLICT #" << m_conflicts << " (" << text << ")" << "\n"; } void log_inference(conflict const& core, inference const* inf) { @@ -147,9 +147,9 @@ namespace polysat { conflict::~conflict() {} - void conflict::begin_conflict() { + void conflict::begin_conflict(char const* text) { if (m_logger) { - m_logger->begin_conflict(); + m_logger->begin_conflict(text); // log initial conflict state m_logger->log_inference(*this, nullptr); } diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index ef7f4e137..e11afb79f 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -133,7 +133,7 @@ namespace polysat { ~conflict(); /// Begin next conflict - void begin_conflict(); + void begin_conflict(char const* text); /// Log inference at the current state. void log_inference(inference const& inf); void log_inference(char const* name) { log_inference(inference_named(name)); } diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index eb3c9417c..b7e0ab118 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -17,6 +17,34 @@ Author: namespace polysat { + struct post_propagate2 : public inference { + const char* name; + signed_constraint conclusion; + signed_constraint premise1; + signed_constraint premise2; + post_propagate2(const char* name, signed_constraint conclusion, signed_constraint premise1, signed_constraint premise2) + : name(name), conclusion(conclusion), premise1(premise1), premise2(premise2) {} + std::ostream& display(std::ostream& out) const override { + return out << "Post-propagate (by " << name << "), " + << "conclusion " << conclusion.blit() << ": " << conclusion + << " from " << premise1.blit() << ": " << premise1 + << " and " << premise2.blit() << ": " << premise2; + } + }; + + struct inference_sup : public inference { + const char* name; + pvar var; + signed_constraint reduced; + signed_constraint reducer; + inference_sup(const char* name, pvar var, signed_constraint reduced, signed_constraint reducer) : name(name), var(var), reduced(reduced), reducer(reducer) {} + std::ostream& display(std::ostream& out) const override { + return out << "Superposition (" << name << "), reduced v" << var + << " in " << reduced.blit() << ": " << reduced + << " by " << reducer.blit() << ": " << reducer; + } + }; + signed_constraint ex_polynomial_superposition::resolve1(pvar v, signed_constraint c1, signed_constraint c2) { // c1 is true, c2 is false SASSERT(c1.is_currently_true(s)); @@ -62,6 +90,7 @@ namespace polysat { if (!c) continue; + char const* inf_name = "?"; switch (c.bvalue(s)) { case l_false: // new conflict state based on propagation and theory conflict @@ -69,9 +98,10 @@ namespace polysat { core.insert(c1); core.insert(c2); core.insert(~c); - core.log_inference("superposition 1"); + core.log_inference(inference_sup("1", v, c2, c1)); return l_true; case l_undef: + SASSERT(premises.empty()); // Ensure that c is assigned and justified premises.push_back(c1); premises.push_back(c2); @@ -80,8 +110,9 @@ namespace polysat { // gets created, c is assigned to false by evaluation propagation // It should have been assigned true by unit propagation. core.replace(c2, c, premises); - core.log_inference("superposition 2"); - SASSERT_EQ(l_true, c.bvalue(s)); // TODO: currently violated, check this! + core.log_inference(post_propagate2("superposition", c, c2, c1)); + inf_name = "2"; + SASSERT_EQ(l_true, c.bvalue(s)); SASSERT(c.is_currently_false(s)); break; default: @@ -92,7 +123,7 @@ namespace polysat { // c alone (+ variables) is now enough to represent the conflict. core.reset(); core.set(c); - core.log_inference("superposition 3"); + core.log_inference(inference_sup(inf_name, v, c2, c1)); return c->contains_var(v) ? l_undef : l_true; } return l_false; @@ -143,19 +174,6 @@ namespace polysat { } } - struct inference_sup : public inference { - const char* name; - pvar var; - signed_constraint reduced; - signed_constraint reducer; - inference_sup(const char* name, pvar var, signed_constraint reduced, signed_constraint reducer) : name(name), var(var), reduced(reduced), reducer(reducer) {} - std::ostream& display(std::ostream& out) const override { - return out << "Superposition " << name << ", reduced v" << var - << " in " << reduced.blit() << ": " << reduced - << " by " << reducer.blit() << ": " << reducer; - } - }; - bool ex_polynomial_superposition::reduce_by(pvar v, signed_constraint eq, conflict& core) { pdd p = eq.eq(); LOG("using v" << v << " " << eq); diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 6046dffbc..7f3340477 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -225,7 +225,7 @@ namespace polysat { } } - lbool op_constraint::eval_lshr(pdd const& p, pdd const& q, pdd const& r) const { + lbool op_constraint::eval_lshr(pdd const& p, pdd const& q, pdd const& r) { auto& m = p.manager(); if (p.is_val() && q.is_val() && r.is_val()) @@ -289,7 +289,7 @@ namespace polysat { } } - lbool op_constraint::eval_and(pdd const& p, pdd const& q, pdd const& r) const { + lbool op_constraint::eval_and(pdd const& p, pdd const& q, pdd const& r) { if ((p.is_zero() || q.is_zero()) && r.is_zero()) return l_true; diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h index 05b112aeb..de34be74a 100644 --- a/src/math/polysat/op_constraint.h +++ b/src/math/polysat/op_constraint.h @@ -43,10 +43,10 @@ namespace polysat { lbool eval(pdd const& p, pdd const& q, pdd const& r) const; void narrow_lshr(solver& s); - lbool eval_lshr(pdd const& p, pdd const& q, pdd const& r) const; + static lbool eval_lshr(pdd const& p, pdd const& q, pdd const& r); void narrow_and(solver& s); - lbool eval_and(pdd const& p, pdd const& q, pdd const& r) const; + static lbool eval_and(pdd const& p, pdd const& q, pdd const& r); public: ~op_constraint() override {} diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index d619dcd00..575a1dd98 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -610,9 +610,9 @@ namespace polysat { ++m_stats.m_num_conflicts; SASSERT(is_conflict()); - m_conflict.begin_conflict(); if (m_conflict.conflict_var() != null_var) { + m_conflict.begin_conflict("backtrack_fi"); pvar v = m_conflict.conflict_var(); // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack. // TODO: use unsat core from m_viable_fallback if the conflict is from there @@ -620,6 +620,7 @@ namespace polysat { backtrack_fi(); return; } + m_conflict.begin_conflict("resolve_conflict"); search_iterator search_it(m_search); while (search_it.next()) { diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 305a9c81f..75a32aa53 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -37,7 +37,7 @@ namespace polysat { dealloc(e); } - void viable::push_var(unsigned sz) { + void viable::push_var(unsigned bit_width) { m_units.push_back(nullptr); m_equal_lin.push_back(nullptr); m_diseq_lin.push_back(nullptr); @@ -745,9 +745,9 @@ namespace polysat { m_usolver_factory = mk_univariate_bitblast_factory(); } - void viable_fallback::push_var(unsigned sz) { + void viable_fallback::push_var(unsigned bit_width) { auto& mk_solver = *m_usolver_factory; - m_usolver.push_back(mk_solver(sz)); + m_usolver.push_back(mk_solver(bit_width)); m_constraints.push_back({}); } diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index e972e0e05..8afef8ccf 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -69,7 +69,7 @@ namespace polysat { ~viable(); // declare and remove var - void push_var(unsigned sz); + void push_var(unsigned bit_width); void pop_var(); // undo adding/removing of entries @@ -223,7 +223,7 @@ namespace polysat { return v.v.display(out, v.var); } - + // TODO: don't push on each constraint add/remove; but only when necessary class viable_fallback { solver& s; @@ -236,7 +236,7 @@ namespace polysat { viable_fallback(solver& s); // declare and remove var - void push_var(unsigned sz); + void push_var(unsigned bit_width); void pop_var(); // add/remove constraints stored in the fallback solver