clause_builder::set_redundant

src/math/polysat/clause.h

@@ -20,10 +20,6 @@ namespace polysat {
     class signed_constraint;
     class simplify_clause;
 
-    class clause;
-    using clause_ref = ref<clause>;
-    using clause_ref_vector = sref_vector<clause>;
-
     /// Disjunction of constraints represented by boolean literals
     // NB code review:
     // right, ref-count is unlikely the right mechanism.
@@ -31,11 +27,14 @@ namespace polysat {
     // and deleted when they exist the arena.
     //
     class clause {
+    public:
+        static inline const bool redundant_default = true;
+    private:
         friend class constraint_manager;
         friend class simplify_clause;
 
         unsigned m_ref_count = 0;  // TODO: remove refcount once we confirm it's not needed anymore
-        bool m_redundant = true;
+        bool m_redundant = redundant_default;
         sat::literal_vector m_literals;
 
 

src/math/polysat/clause_builder.cpp

@@ -29,6 +29,7 @@ namespace polysat {
     void clause_builder::reset() {
         m_literals.reset();
         m_is_tautology = false;
+        m_redundant = clause::redundant_default;
         SASSERT(empty());
     }
 
@@ -49,6 +50,9 @@ namespace polysat {
         }
         m_literals.shrink(j);
         clause_ref cl = clause::from_literals(std::move(m_literals));
+        SASSERT(cl);
+        cl->set_redundant(m_redundant);
+        m_redundant = clause::redundant_default;
         SASSERT(empty());
         return cl;
     }

src/math/polysat/clause_builder.h

@@ -28,6 +28,7 @@ namespace polysat {
         /// 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;
 
     public:
         clause_builder(solver& s);
@@ -36,9 +37,11 @@ namespace polysat {
         clause_builder& operator=(clause_builder const& s) = delete;
         clause_builder& operator=(clause_builder&& s) = default;
 
-        bool empty() const { return m_literals.empty() && !m_is_tautology; }
+        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; }
+
         /// 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/types.h

@@ -28,6 +28,9 @@ namespace polysat {
     class solver;
     class clause;
 
+    using clause_ref = ref<clause>;
+    using clause_ref_vector = sref_vector<clause>;
+
     typedef dd::pdd pdd;
     typedef dd::bdd bdd;
     typedef dd::bddv bddv;