clause_builder should not fail on always-true literals

Otherwise, e.g. when adding axioms, the caller would have to check each literal before adding it.

src/math/polysat/clause_builder.cpp

@@ -28,10 +28,15 @@ namespace polysat {
 
     void clause_builder::reset() {
         m_literals.reset();
+        m_is_tautology = false;
         SASSERT(empty());
     }
 
     clause_ref clause_builder::build() {
+        if (m_is_tautology) {
+            reset();
+            return nullptr;
+        }
         std::sort(m_literals.data(), m_literals.data() + m_literals.size());
         sat::literal prev = sat::null_literal;
         unsigned j = 0;
@@ -56,7 +61,10 @@ namespace polysat {
     void clause_builder::push(signed_constraint c) {
         SASSERT(c);
         SASSERT(c->has_bvar());
-        SASSERT(!c.is_always_true());  // clause would be a tautology
+        if (c.is_always_true()) {
+            m_is_tautology = true;
+            return;
+        }
 #if 0
         if (c->unit_clause()) {
             return;

src/math/polysat/clause_builder.h

@@ -26,6 +26,9 @@ namespace polysat {
     class clause_builder {
         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;
 
     public:
         clause_builder(solver& s);
@@ -34,11 +37,12 @@ namespace polysat {
         clause_builder& operator=(clause_builder const& s) = delete;
         clause_builder& operator=(clause_builder&& s) = default;
 
-        bool empty() const { return m_literals.empty(); }
+        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();
 
 

src/math/polysat/conflict.cpp

@@ -160,6 +160,7 @@ namespace polysat {
         }
         c_lemma.push(c.blit());
         clause_ref lemma = c_lemma.build();
+        SASSERT(lemma);
         cm().store(lemma.get(), s);
         if (s.m_bvars.value(c.blit()) == l_undef)
             s.assign_propagate(c.blit(), *lemma);

src/math/polysat/mul_ovfl_constraint.cpp

@@ -138,6 +138,7 @@ namespace polysat {
         cb.push_new(~premise);
         cb.push_new(conseq);
         clause_ref just = cb.build();
+        SASSERT(just);
         s.add_clause(*just);
         s.propagate();
         SASSERT(s.m_bvars.is_true(conseq.blit()));

src/math/polysat/solver.cpp

@@ -674,6 +674,7 @@ namespace polysat {
 
         SASSERT(std::find(reason_builder.begin(), reason_builder.end(), ~lit));
         clause_ref reason = reason_builder.build();
+        SASSERT(reason);
 
         if (reason->empty()) {
             report_unsat();
@@ -788,9 +789,11 @@ namespace polysat {
             cb.push(c);
         }
         clause_ref clause = cb.build();
+        if (clause) {
             clause->set_redundant(is_redundant);
             add_clause(*clause);
         }
+    }
 
     void solver::add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant) {
         signed_constraint cs[2] = { c1, c2 };