Polysat updates (#5444)

* Simplify adding lemmas

* Remove misleading constructor from tmp_assign.

The idea is that tmp_assign is only created on the stack and
short-lived.  Instead of having a convenience constructor that takes a
constraint_ref, it's clearer to have an explicit .get() at the call
site.

* Remove some log messages

* bugfix

* fix

* Add stub for conflict_core

* wip

* Add example by Clemens

src/math/polysat/CMakeLists.txt

@@ -2,6 +2,7 @@ z3_add_component(polysat
   SOURCES
     boolean.cpp
     clause_builder.cpp
+    conflict_core.cpp
     constraint.cpp
     eq_constraint.cpp
     explain.cpp

src/math/polysat/conflict_core.cpp

@@ -0,0 +1,28 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat conflict
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+
+#include "math/polysat/conflict_core.h"
+#include "math/polysat/solver.h"
+#include "math/polysat/log.h"
+#include "math/polysat/log_helper.h"
+
+namespace polysat {
+
+    std::ostream& conflict_core::display(std::ostream& out) const {
+        out << "TODO: display conflict_core";
+        // depending on sign:   A /\ B /\ C     or     ¬A \/ ¬B \/ ¬C
+        return out;
+    }
+
+}

src/math/polysat/conflict_core.h

@@ -0,0 +1,66 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat conflict
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+#pragma once
+#include "math/polysat/constraint.h"
+
+namespace polysat {
+
+    /// Represents a conflict as core (~negation of clause).
+    ///
+    /// TODO: can probably move some clause_builder functionality into this class.
+    class conflict_core {
+        // constraint_ref_vector m_constraints;
+        vector<constraint_literal> m_constraints;
+        bool m_needs_model = true;  ///< True iff the conflict depends on the current variable assignment. (If so, additional constraints must be added to the final learned clause.)
+
+    public:
+        vector<constraint_literal> const& constraints() const {
+            return m_constraints;
+        }
+
+        bool empty() const {
+            return m_constraints.empty();
+        }
+
+        void reset() {
+            m_constraints.reset();
+            m_needs_model = true;
+        }
+
+        // for bailing out with a conflict at the base level
+        void set(std::nullptr_t) {
+            SASSERT(empty());
+            m_constraints.push_back({});
+            m_needs_model = false;
+        }
+
+        // void set(
+        
+        // TODO: set core from conflicting units
+        // TODO: set clause
+
+        // TODO: use iterator instead (this method is needed for marking so duplicates don't necessarily have to be skipped)
+        unsigned_vector vars(constraint_manager const& cm) const {
+            unsigned_vector vars;
+            for (auto const& c : m_constraints)
+                vars.append(c->vars());
+            return vars;
+        }
+
+        std::ostream& display(std::ostream& out) const;
+    };
+
+    inline std::ostream& operator<<(std::ostream& out, conflict_core const& c) { return c.display(out); }
+
+}

src/math/polysat/constraint.cpp

@@ -151,8 +151,9 @@ namespace polysat {
 
     std::ostream& constraint::display_extra(std::ostream& out) const {
         out << " @" << level() << " (b" << bvar() << ")";
-        if (is_undef())
-            out << " [inactive]";
+        if (is_positive()) out << " [pos]";
+        if (is_negative()) out << " [neg]";
+        if (is_undef()) out << " [inactive]";
         return out;
     }
 

src/math/polysat/constraint.h

@@ -166,7 +166,8 @@ namespace polysat {
 
         sat::literal blit() const { SASSERT(!is_undef()); return m_status == l_true ? sat::literal(m_bvar) : ~sat::literal(m_bvar); }
         void assign(bool is_true) {
-            SASSERT(m_status == l_undef /* || m_status == to_lbool(is_true) */);
+            SASSERT(m_status == l_undef || m_status == to_lbool(is_true));
+            // SASSERT(m_status == l_undef /* || m_status == to_lbool(is_true) */);
             m_status = to_lbool(is_true);
             // SASSERT(m_manager->m_bvars.value(bvar()) == l_undef || m_manager->m_bvars.value(bvar()) == m_status);  // TODO: is this always true? maybe we sometimes want to check the opposite phase temporarily.
         }
@@ -176,7 +177,7 @@ namespace polysat {
         bool is_negative() const { return m_status == l_false; }
 
         clause* unit_clause() const { return m_unit_clause; }
-        void set_unit_clause(clause* cl) { SASSERT(cl); SASSERT(!m_unit_clause); m_unit_clause = cl; }
+        void set_unit_clause(clause* cl) { SASSERT(cl); SASSERT(!m_unit_clause || m_unit_clause == cl); m_unit_clause = cl; }
         p_dependency* unit_dep() const;
 
         /** Precondition: all variables other than v are assigned.
@@ -351,6 +352,7 @@ namespace polysat {
         constraint* m_constraint;
         bool m_should_unassign = false;
     public:
+        /// c must live longer than tmp_assign.
         tmp_assign(constraint* c, sat::literal lit):
             m_constraint(c) {
             SASSERT(c);
@@ -362,8 +364,6 @@ namespace polysat {
             else
                 SASSERT_EQ(c->blit(), lit);
         }
-      // NSB review: assumes life-time of c extends use in tmp_assign.
-        tmp_assign(constraint_ref const& c, sat::literal lit): tmp_assign(c.get(), lit) {}
         void revert() {
             if (m_should_unassign) {
                 m_constraint->unassign();

src/math/polysat/explain.cpp

@@ -41,6 +41,30 @@ namespace polysat {
         for (auto* c : confl.clauses())
             m_conflict.push_back(c);
 
+        // Collect unit constraints
+        //
+        // TODO: the distinction between units and unit clauses is a bit awkward; maybe it should be removed.
+        //       We could then also remove the hybrid container 'constraints_and_clauses' by a clause_ref_vector
+        SASSERT(m_conflict_units.empty());
+        for (constraint* c : m_conflict.units())
+            // if (c->is_eq())
+                m_conflict_units.push_back(c);
+        for (auto clause : m_conflict.clauses()) {
+            if (clause->size() == 1) {                    
+                sat::literal lit = (*clause)[0];
+                constraint* c = m_solver.m_constraints.lookup(lit.var());                    
+                LOG("unit clause: " << show_deref(c));
+                // Morally, a derived unit clause is always asserted at the base level.
+                // (Even if we don't want to keep this one around. But maybe we should? Do we want to reconstruct proofs?)
+                c->set_unit_clause(clause);
+                c->assign(!lit.sign());
+                // this clause is really a unit.
+                // if (c->is_eq()) {
+                    m_conflict_units.push_back(c);
+                // }
+            }
+        }
+
         // TODO: we should share work done for examining constraints between different resolution methods
         clause_ref lemma;
         if (!lemma) lemma = by_polynomial_superposition();
@@ -57,9 +81,9 @@ namespace polysat {
                 }
                 // All constraints in the lemma must be false in the conflict state
                 for (auto lit : lemma->literals()) {
-                    if (m_solver.m_bvars.value(lit.var()) == l_false)
+                    if (m_solver.m_bvars.value(lit) == l_false)
                         continue;
-                    SASSERT(m_solver.m_bvars.value(lit.var()) != l_true);
+                    SASSERT(m_solver.m_bvars.value(lit) != l_true);
                     constraint* c = m_solver.m_constraints.lookup(lit.var());
                     SASSERT(c);
                     tmp_assign _t(c, lit);
@@ -90,6 +114,8 @@ namespace polysat {
      */
     clause_ref conflict_explainer::by_polynomial_superposition() {
         LOG_H3("units-size: " << m_conflict.units().size() << " conflict-clauses " << m_conflict.clauses().size());
+
+#if 0
         constraint* c1 = nullptr, *c2 = nullptr;
 
         if (m_conflict.units().size() == 2 && m_conflict.clauses().size() == 0) {
@@ -99,23 +125,26 @@ namespace polysat {
         else {
             // other combinations?
 
-#if 0
+#if 1
             // A clause can also be a unit.
             // Even if a clause is not a unit, we could still resolve a propagation 
             // into some literal in the current conflict clause.
             // Selecting resolvents should not be specific to superposition.
-            // 
 
             for (auto clause : m_conflict.clauses()) {
+                LOG("clause " << *clause << "  size " << clause->size());
                 if (clause->size() == 1) {                    
                     sat::literal lit = (*clause)[0];
-                    if (lit.sign())
-                        continue;
+                    // if (lit.sign())
+                    //     continue;
                     constraint* c = m_solver.m_constraints.lookup(lit.var());                    
-                    c->assign(true);
+                    // Morally, a derived unit clause is always asserted at the base level.
+                    // (Even if we don't want to keep this one around. But maybe we should? Do we want to reconstruct proofs?)
+                    c->set_unit_clause(clause);
+                    c->assign(!lit.sign());
                     // this clause is really a unit.
                     LOG("unit clause: " << *c);
-                    if (c->is_eq() && c->is_positive()) {
+                    if (c->is_eq()) { //  && c->is_positive()) {
                         c1 = c;
                         break;
                     }
@@ -134,6 +163,8 @@ namespace polysat {
         }
         if (!c1 || !c2 || c1 == c2)
             return nullptr;
+        LOG("c1: " << show_deref(c1));
+        LOG("c2: " << show_deref(c2));
         if (c1->is_eq() && c2->is_eq() && c1->is_positive() && c2->is_positive()) {
             pdd a = c1->to_eq().p();
             pdd b = c2->to_eq().p();
@@ -147,6 +178,72 @@ namespace polysat {
             clause.push_new_constraint(m_solver.m_constraints.eq(lvl, r));
             return clause.build();
         }
+        if (c1->is_eq() && c2->is_eq() && c1->is_negative() && c2->is_positive()) {
+            pdd a = c1->to_eq().p();
+            pdd b = c2->to_eq().p();
+            pdd r = a;
+            // TODO: only holds if the factor for 'a' is non-zero
+            if (!a.resolve(m_var, b, r))
+                return nullptr;
+            unsigned const lvl = std::max(c1->level(), c2->level());
+            clause_builder clause(m_solver);
+            clause.push_literal(~c1->blit());
+            clause.push_literal(~c2->blit());
+            clause.push_new_constraint(~m_solver.m_constraints.eq(lvl, r));
+            SASSERT(false);  // TODO "breakpoint" for debugging
+            return clause.build();
+        }
+
+#else
+        for (constraint* c1 : m_conflict_units) {
+            if (!c1->is_eq())
+                continue;
+            for (constraint* c2 : m_conflict_units) {  // TODO: can start iteration at index(c1)+1
+                if (c1 == c2)
+                    continue;
+                if (!c2->is_eq())
+                    continue;
+                if (c1->is_negative() && c2->is_negative())
+                    continue;
+                LOG("c1: " << show_deref(c1));
+                LOG("c2: " << show_deref(c2));
+                if (c1->is_positive() && c2->is_negative()) {
+                    std::swap(c1, c2);
+                }
+                pdd a = c1->to_eq().p();
+                pdd b = c2->to_eq().p();
+                pdd r = a;
+                unsigned const lvl = std::max(c1->level(), c2->level());
+                if (c1->is_positive() && c2->is_positive()) {
+                    if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r))
+                        continue;
+                    clause_builder clause(m_solver);
+                    clause.push_literal(~c1->blit());
+                    clause.push_literal(~c2->blit());
+                    clause.push_new_constraint(m_solver.m_constraints.eq(lvl, r));
+                    auto cl = clause.build();
+                    LOG("r: " << show_deref(cl->new_constraints()[0]));
+                    LOG("result: " << show_deref(cl));
+                    // SASSERT(false);  // NOTE: this is a simple "breakpoint" for debugging
+                    return cl;
+                }
+                if (c1->is_negative() && c2->is_positive()) {
+                    // TODO: only holds if the factor for 'a' is non-zero
+                    if (!a.resolve(m_var, b, r))
+                        continue;
+                    clause_builder clause(m_solver);
+                    clause.push_literal(~c1->blit());
+                    clause.push_literal(~c2->blit());
+                    clause.push_new_constraint(~m_solver.m_constraints.eq(lvl, r));
+                    auto cl = clause.build();
+                    LOG("r: " << show_deref(cl->new_constraints()[0]));
+                    LOG("result: " << show_deref(cl));
+                    // SASSERT(false);  // NOTE: this is a simple "breakpoint" for debugging
+                    return cl;
+                }
+            }
+        }
+#endif
         return nullptr;
     }
 

src/math/polysat/explain.h

@@ -24,6 +24,7 @@ namespace polysat {
     class conflict_explainer {
         solver& m_solver;
         constraints_and_clauses m_conflict;
+        ptr_vector<constraint> m_conflict_units;
         pvar m_var = null_var;
         ptr_vector<constraint> m_cjust_v;
 

src/math/polysat/log.cpp

@@ -25,9 +25,7 @@ Other:
 
 #if POLYSAT_LOGGING_ENABLED
 
-static LogLevel
-get_max_log_level(std::string const& fn, std::string const& pretty_fn)
-{
+static LogLevel get_max_log_level(std::string const& fn, std::string const& pretty_fn) {
   (void)fn;
   (void)pretty_fn;
 
@@ -46,16 +44,12 @@ get_max_log_level(std::string const& fn, std::string const& pretty_fn)
 }
 
 /// Filter log messages
-bool
-polysat_should_log(LogLevel msg_level, std::string fn, std::string pretty_fn)
-{
+bool polysat_should_log(LogLevel msg_level, std::string fn, std::string pretty_fn) {
   LogLevel max_log_level = get_max_log_level(fn, pretty_fn);
   return msg_level <= max_log_level;
 }
 
-static char const*
-level_color(LogLevel msg_level)
-{
+static char const* level_color(LogLevel msg_level) {
   switch (msg_level) {
     case LogLevel::Heading1:
       return ""; // red
@@ -70,9 +64,7 @@ level_color(LogLevel msg_level)
 
 int polysat_log_indent_level = 0;
 
-std::pair<std::ostream&, bool>
-polysat_log(LogLevel msg_level, std::string fn, std::string /* pretty_fn */)
-{
+std::pair<std::ostream&, bool> polysat_log(LogLevel msg_level, std::string fn, std::string /* pretty_fn */) {
   std::ostream& os = std::cerr;
 
   size_t width = 20;
@@ -87,25 +79,23 @@ polysat_log(LogLevel msg_level, std::string fn, std::string /* pretty_fn */)
   dwMode |= ENABLE_VIRTUAL_TERMINAL_PROCESSING;
   ok = ok && SetConsoleMode(hOut, dwMode);
 #else
-  int const fd = _fileno(stderr);
+  int const fd = fileno(stderr);
   if (color && !isatty(fd)) { color = nullptr; }
 #endif
 
-  if (color) { os << color; }
+  if (color)
+    os << color;
   os << "[" << fn << "] " << std::string(padding, ' ');
   os << std::string(polysat_log_indent_level, ' ');
   return {os, (bool)color};
 
 }
 
-polysat_log_indent::polysat_log_indent(int amount)
-  : m_amount{amount}
-{
+polysat_log_indent::polysat_log_indent(int amount): m_amount{amount} {
   polysat_log_indent_level += m_amount;
 }
 
-polysat_log_indent::~polysat_log_indent()
-{
+polysat_log_indent::~polysat_log_indent() {
   polysat_log_indent_level -= m_amount;
 }
 

src/math/polysat/solver.cpp

@@ -522,6 +522,7 @@ namespace polysat {
                 LOG("Lemma: " << show_deref(lemma));
                 clause_ref new_lemma = resolve(v);
                 LOG("New Lemma: " << show_deref(new_lemma));
+                // SASSERT(new_lemma); // TODO: only for debugging, to have a breakpoint on resolution failure
                 if (!new_lemma) {
                     backtrack(i, lemma);
                     return;
@@ -672,7 +673,7 @@ namespace polysat {
             }
         }
         while (i-- > 0);
-        add_lemma_clause(lemma);  // TODO: handle units correctly
+        add_lemma(lemma);  // TODO: this lemma is stored but otherwise "lost" because it will not be activated / not added to any watch data structures
         report_unsat();
     }
 
@@ -692,44 +693,27 @@ namespace polysat {
         m_dm.linearize(conflict_dep, deps);
     }
 
-    /**
-     * The polynomial p encodes an equality that the decision was infeasible.
-     * The effect of this function is that the assignment to v is undone and replaced 
-     * by a new decision or unit propagation or conflict.
-     * We add 'p == 0' as a lemma. The lemma depends on the dependencies used
-     * to derive p, and the level of the lemma is the maximal level of the dependencies.
-     */
     void solver::learn_lemma(pvar v, clause_ref lemma) {
         if (!lemma)
             return;
         LOG("Learning: " << show_deref(lemma));
+        SASSERT(lemma->size() > 0);
         SASSERT(m_conflict_level <= m_justification[v].level());
-        if (lemma->size() == 1) {
-            constraint_ref c;
-            if (lemma->new_constraints().size() > 0) {
-                SASSERT_EQ(lemma->new_constraints().size(), 1);
-                c = lemma->new_constraints()[0];
-            }
-            else {
-                c = m_constraints.lookup(lemma->literals()[0].var());
-            }
-            SASSERT_EQ(lemma->literals()[0].var(), c->bvar());
-            SASSERT(c);
-            add_lemma_unit(c);
-            push_cjust(v, c.get());
-            activate_constraint_base(c.get(), !lemma->literals()[0].sign());
+        clause* cl = lemma.get();
+        add_lemma(std::move(lemma));
+        if (cl->size() == 1) {
+            sat::literal lit = cl->literals()[0];
+            constraint* c = m_constraints.lookup(lit.var());
+            c->set_unit_clause(cl);
+            push_cjust(v, c);
+            activate_constraint_base(c, !lit.sign());
+        }
+        else {
+            sat::literal lit = decide_bool(*cl);
+            SASSERT(lit != sat::null_literal);
+            constraint* c = m_constraints.lookup(lit.var());
+            push_cjust(v, c);
         }
-        else
-            learn_lemma_clause(v, std::move(lemma));
-    }
-
-    void solver::learn_lemma_clause(pvar v, clause_ref lemma) {
-        SASSERT(lemma);
-        sat::literal lit = decide_bool(*lemma);
-        SASSERT(lit != sat::null_literal);
-        constraint* c = m_constraints.lookup(lit.var());
-        push_cjust(v, c);
-        add_lemma_clause(std::move(lemma));
     }
 
     // Guess a literal from the given clause; returns the guessed constraint
@@ -750,7 +734,6 @@ namespace polysat {
             return !c->is_currently_false(*this);
         };
 
-        // constraint *choice = nullptr;
         sat::literal choice = sat::null_literal;
         unsigned num_choices = 0;  // TODO: should probably cache this?
 
@@ -789,12 +772,7 @@ namespace polysat {
         rational val = m_value[v];
         LOG_H3("Reverting decision: pvar " << v << " := " << val);
         SASSERT(m_justification[v].is_decision());
-        constraints just(m_cjust[v]);
         backjump(m_justification[v].level()-1);
-        // Since decision "v -> val" caused a conflict, we may keep all
-        // viability restrictions on v and additionally exclude val.
-        // TODO: viability restrictions on 'v' must have happened before decision on 'v'. Do we really need to save/restore m_viable here?
-        SASSERT(m_cjust[v] == just);  // check this with assertion
 
         m_viable.add_non_viable(v, val);
 
@@ -815,7 +793,8 @@ namespace polysat {
             //         and then may lead to an assertion failure through this call to narrow.
             // TODO: what to do with "unassigned" constraints at this point? (we probably should have resolved those away, even in the 'backtrack' case.)
             //       NOTE: they are constraints from clauses that were added to cjust… how to deal with that? should we add the whole clause to cjust?
-            if (!c->is_undef())  // TODO: this check to be removed once this is fixed properly.
+            SASSERT(!c->is_undef());
+            // if (!c->is_undef())  // TODO: this check to be removed once this is fixed properly.
                 c->narrow(*this);
             if (is_conflict()) {
                 LOG_H1("Conflict during revert_decision/narrow!");
@@ -902,7 +881,7 @@ namespace polysat {
         m_conflict.reset();
 
         clause* reason_cl = reason.get();
-        add_lemma_clause(std::move(reason));
+        add_lemma(std::move(reason));
         propagate_bool(~lit, reason_cl);
         if (is_conflict()) {
             LOG_H1("Conflict during revert_bool_decision/propagate_bool!");
@@ -924,7 +903,7 @@ namespace polysat {
         if (reason->literals().size() == 1) {
             SASSERT(reason->literals()[0] == lit);
             constraint* c = m_constraints.lookup(lit.var());
-            m_redundant.push_back(c);
+            // m_redundant.push_back(c);
             activate_constraint_base(c, !lit.sign());
         }
         else
@@ -949,6 +928,7 @@ namespace polysat {
     /// Used for external unit constraints and unit consequences.
     void solver::activate_constraint_base(constraint* c, bool is_true) {
         SASSERT(c);
+        LOG("\n" << *this);
         // c must be in m_original or m_redundant so it can be deactivated properly when popping the base level
         SASSERT_EQ(std::count(m_original.begin(), m_original.end(), c) + std::count(m_redundant.begin(), m_redundant.end(), c), 1);
         sat::literal lit(c->bvar(), !is_true);
@@ -1016,30 +996,22 @@ namespace polysat {
     }
 
     // Add lemma to storage but do not activate it
-    void solver::add_lemma_unit(constraint_ref lemma) {
+    void solver::add_lemma(clause_ref lemma) {
         if (!lemma)
             return;
         LOG("Lemma: " << show_deref(lemma));
-        constraint* c = m_constraints.store(std::move(lemma));
-        insert_constraint(m_redundant, c);
-        // TODO: create unit clause
-    }
-
-    // Add lemma to storage but do not activate it
-    void solver::add_lemma_clause(clause_ref lemma) {
-        if (!lemma)
-            return;
-        // TODO: check for unit clauses!
-        LOG("Lemma: " << show_deref(lemma));
-        if (lemma->size() < 2) {
-            LOG_H1("TODO: this should be treated as unit constraint and asserted at the base level!");
-        }
-        // SASSERT(lemma->size() > 1);
+        SASSERT(lemma->size() > 0);
         clause* cl = m_constraints.store(std::move(lemma));
         m_redundant_clauses.push_back(cl);
+        if (cl->size() == 1) {
+            constraint* c = m_constraints.lookup(cl->literals()[0].var());
+            insert_constraint(m_redundant, c);
+        }
     }
 
     void solver::insert_constraint(ptr_vector<constraint>& cs, constraint* c) {
+        SASSERT(c);
+        LOG_V("INSERTING: " << *c);
         cs.push_back(c);
         for (unsigned i = cs.size() - 1; i-- > 0; ) {
             auto* c1 = cs[i + 1];
@@ -1082,17 +1054,17 @@ namespace polysat {
         return m_base_levels.empty() ? 0 : m_base_levels.back();
     }
 
-    bool solver::active_at_base_level(sat::bool_var bvar) const {
-        // NOTE: this active_at_base_level is actually not what we want!!!
-        //          first of all, it might not really be a base level: could be a non-base level between previous base levels.
-        //          in that case, how do we determine the right dependencies???
-        //          secondly, we are interested in "unit clauses", not as much whether we assigned something on the base level...
-        //          TODO: however, propagating stuff at the base level... need to be careful with dependencies there... might need to turn all base-level propagations into unit clauses...
-        VERIFY(false);
-        // bool res = m_bvars.is_assigned(bvar) && m_bvars.level(bvar) <= base_level();
-        // SASSERT_EQ(res, !!m_constraints.lookup(bvar)->unit_clause());
-        // return res;
-    }
+    // bool solver::active_at_base_level(sat::bool_var bvar) const {
+    //     // NOTE: this active_at_base_level is actually not what we want!!!
+    //     //          first of all, it might not really be a base level: could be a non-base level between previous base levels.
+    //     //          in that case, how do we determine the right dependencies???
+    //     //          secondly, we are interested in "unit clauses", not as much whether we assigned something on the base level...
+    //     //          TODO: however, propagating stuff at the base level... need to be careful with dependencies there... might need to turn all base-level propagations into unit clauses...
+    //     VERIFY(false);
+    //     // bool res = m_bvars.is_assigned(bvar) && m_bvars.level(bvar) <= base_level();
+    //     // SASSERT_EQ(res, !!m_constraints.lookup(bvar)->unit_clause());
+    //     // return res;
+    // }
 
     bool solver::try_eval(pdd const& p, rational& out_value) const {
         pdd r = p.subst_val(assignment());

src/math/polysat/solver.h

@@ -126,7 +126,8 @@ namespace polysat {
         void push_cjust(pvar v, constraint* c) {
             if (m_cjust[v].contains(c))  // TODO: better check (flag on constraint?)
                 return;
-            LOG_V("cjust[v" << v << "] += " << *c);
+            LOG_V("cjust[v" << v << "] += " << show_deref(c));
+            SASSERT(c);
             m_cjust[v].push_back(c);        
             m_trail.push_back(trail_instr_t::just_i);
             m_cjust_trail.push_back(v);
@@ -206,9 +207,6 @@ namespace polysat {
         bool is_conflict() const { return !m_conflict.empty(); }
         bool at_base_level() const;
         unsigned base_level() const;
-        bool active_at_base_level(sat::bool_var bvar) const;
-        bool active_at_base_level(sat::literal lit) const { return active_at_base_level(lit.var()); }
-        bool active_at_base_level(constraint& c) const { return active_at_base_level(c.bvar()); }
 
         void resolve_conflict();
         void backtrack(unsigned i, clause_ref lemma);
@@ -216,10 +214,8 @@ namespace polysat {
         void revert_decision(pvar v, clause_ref reason);
         void revert_bool_decision(sat::literal lit, clause_ref reason);
         void learn_lemma(pvar v, clause_ref lemma);
-        void learn_lemma_clause(pvar v, clause_ref lemma);
         void backjump(unsigned new_level);
-        void add_lemma_unit(constraint_ref lemma);
-        void add_lemma_clause(clause_ref lemma);
+        void add_lemma(clause_ref lemma);
 
         constraint_literal mk_eq(pdd const& p);
         constraint_literal mk_diseq(pdd const& p);

src/math/polysat/viable.cpp

@@ -265,11 +265,8 @@ namespace polysat {
                 if (is_viable(v, x)) 
                     xs.push_back(x);
                             
-            LOG("Viable for pvar " << v << ": " << xs);
+            LOG("Viable for v" << v << ": " << xs);
         } 
-        else {
-            LOG("Viable for pvar " << v << ": <range too big>");
-        }
     }
 #endif
 

src/test/polysat.cpp

@@ -43,6 +43,7 @@ namespace polysat {
 
     public:
         scoped_solver(std::string name): solver(lim), m_name(name) {
+            std::cout << "\n\n\n" << std::string(78, '#') << "\n";
             std::cout << "\nSTART: " << m_name << "\n";
         }
 
@@ -355,7 +356,7 @@ namespace polysat {
      * We do overflow checks by doubling the base bitwidth here.
      */
     static void test_monot(unsigned base_bw = 5) {
-        scoped_solver s(__func__);
+        scoped_solver s(std::string{__func__} + "(" + std::to_string(base_bw) + ")");
 
         auto max_int_const = rational::power_of_two(base_bw) - 1;
 
@@ -589,7 +590,7 @@ namespace polysat {
      * y*z >= 2^32
      */
     static void test_monot_bounds(unsigned base_bw = 32) {
-        scoped_solver s(__func__);
+        scoped_solver s(std::string{__func__} + "(" + std::to_string(base_bw) + ")");
         unsigned bw = 2 * base_bw;
         auto y = s.var(s.add_var(bw));
         auto z = s.var(s.add_var(bw));
@@ -709,6 +710,41 @@ namespace polysat {
     }
 
 
+    /**
+     * x*x <= z
+     * (x+1)*(x+1) <= z
+     * y == x+1
+     * ¬(y*y <= z)
+     *
+     * The original version had signed comparisons but that doesn't matter for the UNSAT result.
+     * UNSAT can be seen easily by substituting the equality.
+     */
+    static void test_subst(unsigned bw = 32) {
+        scoped_solver s(__func__);
+        auto x = s.var(s.add_var(bw));
+        auto y = s.var(s.add_var(bw));
+        auto z = s.var(s.add_var(bw));
+        s.add_ule(x * x, z);  // optional
+        s.add_ule((x + 1) * (x + 1), z);
+        s.add_eq(x + 1 - y);
+        s.add_ult(z, y*y);
+        s.check();
+        s.expect_unsat();
+    }
+
+    static void test_subst_signed(unsigned bw = 32) {
+        scoped_solver s(__func__);
+        auto x = s.var(s.add_var(bw));
+        auto y = s.var(s.add_var(bw));
+        auto z = s.var(s.add_var(bw));
+        s.add_sle(x * x, z);  // optional
+        s.add_sle((x + 1) * (x + 1), z);
+        s.add_eq(x + 1 - y);
+        s.add_slt(z, y*y);
+        s.check();
+        s.expect_unsat();
+    }
+
 
     // Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
     // NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
@@ -833,8 +869,9 @@ namespace polysat {
 
 
 void tst_polysat() {
+    polysat::test_subst();
     // polysat::test_monot_bounds(8);
-    polysat::test_monot_bounds_simple(8);
+    // polysat::test_monot_bounds_simple(8);
     return;
 
     polysat::test_add_conflicts();