Simplify clause_builder

src/math/polysat/clause_builder.cpp

@@ -61,7 +61,8 @@ namespace polysat {
     void clause_builder::push(signed_constraint c) {
         SASSERT(c);
         SASSERT(c->has_bvar());
-        SASSERT(!c.is_always_false());   // if this case occurs legitimately, we should skip the constraint.
+        if (c.is_always_false())  // filter out trivial constraints such as "4 < 2"
+            return;
         if (c.is_always_true()) {
             m_is_tautology = true;
             return;
@@ -73,10 +74,4 @@ namespace polysat {
 #endif
         m_literals.push_back(c.blit());
     }
-
-    void clause_builder::push_new(signed_constraint c) {
-        if (c.is_always_false())  // filter out trivial constraints such as "4 < 2" (may come in from forbidden intervals)
-            return;
-        push(c);
-    }
 }

src/math/polysat/clause_builder.h

@@ -12,9 +12,7 @@ Author:
 Notes:
 
  Builds a clause from literals and constraints.
- Takes care to
+ Skips trivial new constraints such as "4 <= 1".
- - resolve with unit clauses and accumulate their dependencies,
- - skip trivial new constraints such as "4 <= 1".
 
 --*/
 #pragma once
@@ -26,7 +24,7 @@ namespace polysat {
     class clause_builder {
         solver*               m_solver;
         sat::literal_vector   m_literals;
-        /// true iff clause contains a literal that is always true
+        /// 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;
 
@@ -40,19 +38,14 @@ namespace polysat {
         bool empty() const { return m_literals.empty() && !m_is_tautology; }
         void reset();
 
-
         /// 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();
 
-
         void push(sat::literal lit);
         void push(signed_constraint c);
         void push(inequality const& i) { push(i.as_signed_constraint()); }
 
-        /// Push a new constraint. Allocates a boolean variable for the constraint, if necessary.
-        void push_new(signed_constraint c);
-      
         using const_iterator = decltype(m_literals)::const_iterator;
         const_iterator begin() const { return m_literals.begin(); }
         const_iterator end() const { return m_literals.end(); }

src/math/polysat/conflict.cpp

@@ -332,7 +332,7 @@ namespace polysat {
             cb.push(~premises[i]);
         }
         SASSERT_EQ(c.bvalue(s), l_undef);
-        cb.push_new(c);
+        cb.push(c);
         clause_ref lemma = cb.build();
         SASSERT(lemma);
         lemma->set_redundant(true);

src/math/polysat/umul_ovfl_constraint.cpp

@@ -132,9 +132,9 @@ namespace polysat {
         SASSERT(bound * p.val() > max);
         SASSERT((bound - 1) * p.val() <= max);
         clause_builder cb(s);
-        cb.push_new(~sc);
+        cb.push(~sc);
-        cb.push_new(~premise);
+        cb.push(~premise);
-        cb.push_new(conseq);
+        cb.push(conseq);
         clause_ref just = cb.build();
         SASSERT(just);
         s.add_clause(*just);