We need more clause names

src/math/polysat/clause_builder.cpp

@@ -22,19 +22,23 @@ namespace polysat {
     static_assert(std::is_move_assignable_v<clause_builder>);
     static_assert(std::is_move_constructible_v<clause_builder>);
 
-    clause_builder::clause_builder(solver& s):
-        m_solver(&s)
+    clause_builder::clause_builder(solver& s, char const* name):
+        m_solver(&s), m_name(name)
     {}
 
     void clause_builder::reset() {
         m_literals.reset();
         m_is_tautology = false;
         m_redundant = clause::redundant_default;
+        m_name = "";
         SASSERT(empty());
     }
 
     clause_ref clause_builder::build() {
         if (m_is_tautology) {
+            verbose_stream() << "Tautology: " << m_literals << " (" << (m_name ? m_name : "<null>") << ")\n";
+            for (sat::literal lit : m_literals)
+                verbose_stream() << "    " << lit_pp(*m_solver, lit) << "\n";
             reset();
             return nullptr;
         }
@@ -52,7 +56,9 @@ namespace polysat {
         clause_ref cl = clause::from_literals(std::move(m_literals));
         SASSERT(cl);
         cl->set_redundant(m_redundant);
+        cl->set_name(m_name);
         m_redundant = clause::redundant_default;
+        m_name = "";
         SASSERT(empty());
         return cl;
     }

src/math/polysat/clause_builder.h

@@ -23,30 +23,32 @@ Notes:
 namespace polysat {
   
     class clause_builder {
-        solver*               m_solver;
-        sat::literal_vector   m_literals;
+        solver*             m_solver;
+        sat::literal_vector m_literals;
         /// True iff clause contains a literal that is always true
         /// (only this specific case of tautology is covered by this flag)
-        bool                  m_is_tautology = false;
-        bool                  m_redundant = clause::redundant_default;
+        bool                m_is_tautology = false;
+        bool                m_redundant = clause::redundant_default;
+        char const*         m_name;
 
         solver& s() const { return *m_solver; }
 
     public:
-        clause_builder(solver& s);
-        clause_builder(clause_builder const& s) = delete;
-        clause_builder(clause_builder&& s) = default;
-        clause_builder& operator=(clause_builder const& s) = delete;
-        clause_builder& operator=(clause_builder&& s) = default;
+        clause_builder(solver& s, char const* name = "");
+        clause_builder(clause_builder const&) = delete;
+        clause_builder(clause_builder&&) = default;
+        clause_builder& operator=(clause_builder const&) = delete;
+        clause_builder& operator=(clause_builder&&) = default;
 
         bool empty() const { return m_literals.empty() && !m_is_tautology && m_redundant == clause::redundant_default; }
         void reset();
 
         void set_redundant(bool r) { m_redundant = r; }
+        void set_name(char const* name) { m_name = name; }
 
         /// Build the clause. This will reset the clause builder so it can be reused.
         /// Returns nullptr if the clause is a tautology and should not be added to the solver.
-        clause_ref build();
+        [[nodiscard]] clause_ref build();
 
         /// Insert constraints into the clause.
         void insert(sat::literal lit);

src/math/polysat/solver.cpp

@@ -1121,6 +1121,11 @@ namespace polysat {
         }
     }
 
+    void solver::add_clause(clause_ref clause) {
+        VERIFY(clause);
+        add_clause(*clause);
+    }
+
     // Add clause to solver
     void solver::add_clause(clause& clause) {
         LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);

src/math/polysat/solver.h

@@ -290,6 +290,7 @@ namespace polysat {
         void learn_lemma(clause& lemma);
         void backjump(unsigned new_level);
 
+        void add_clause(clause_ref clause);
         void add_clause(clause& clause);
         void add_clause(signed_constraint c1, bool is_redundant);
         void add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant);

src/math/polysat/umul_ovfl_constraint.cpp

@@ -117,6 +117,8 @@ namespace polysat {
         auto const& max = p.manager().max_value();
         // p * q >= max + 1 <=> q >= (max + 1)/p <=> q >= ceil((max+1)/p)
         auto bound = ceil((max + 1) / p.val());
+        SASSERT(bound * p.val() > max);
+        SASSERT((bound - 1) * p.val() <= max);
 
         //
         // the clause that explains bound <= q or bound > q
@@ -126,20 +128,20 @@ namespace polysat {
         //
 
         signed_constraint sc(this, is_positive);
-        signed_constraint premise = is_positive ? s.ule(p0, p.val()) : s.ule(p.val(), p0);
-        signed_constraint conseq = is_positive ? s.ule(bound, q0) : s.ult(q0, bound);
-
-        SASSERT(premise.is_currently_true(s));
-        SASSERT(bound * p.val() > max);
-        SASSERT((bound - 1) * p.val() <= max);
-        clause_builder cb(s);
-        cb.insert_eval(~sc);
-        cb.insert_eval(~premise);
-        cb.insert(conseq);
-        clause_ref just = cb.build();
-        SASSERT(just);
-        s.add_clause(*just);
-        SASSERT(s.m_bvars.is_true(conseq.blit()));
+        if (is_positive) {
+            clause_builder lemma(s, "Ovfl(p, q) & p <= p.val() ==> q >= bound");
+            lemma.insert_eval(~sc);
+            lemma.insert_eval(~s.ule(p0, p.val()));
+            lemma.insert(s.ule(bound, q0));
+            s.add_clause(lemma.build());
+        }
+        else {
+            clause_builder lemma(s, "~Ovfl(p, q) & p >= p.val() ==> q < bound");
+            lemma.insert_eval(~sc);
+            lemma.insert_eval(~s.ule(p.val(), p0));
+            lemma.insert(s.ult(q0, bound));
+            s.add_clause(lemma.build());
+        }
         return true;
     }