clause_builder: rename push to insert

src/math/polysat/clause_builder.cpp

@@ -54,11 +54,11 @@ namespace polysat {
     }
 
 
-    void clause_builder::push(sat::literal lit) {
+    void clause_builder::insert(sat::literal lit) {
-        push(m_solver->lit2cnstr(lit));
+        insert(m_solver->lit2cnstr(lit));
     }
 
-    void clause_builder::push(signed_constraint c) {
+    void clause_builder::insert(signed_constraint c) {
         SASSERT(c);
         if (c.is_always_false())  // filter out trivial constraints such as "4 < 2"
             return;
@@ -66,11 +66,6 @@ namespace polysat {
             m_is_tautology = true;
             return;
         }
-#if 0
-        if (c->unit_clause()) {
-            return;
-        }       
-#endif
         m_literals.push_back(c.blit());
     }
 
@@ -82,6 +77,6 @@ namespace polysat {
         if (c.bvalue(*m_solver) == l_undef) {
             m_solver->assign_eval(~c.blit());
         }
-        push(c);
+        insert(c);
     }
 }

src/math/polysat/clause_builder.h

@@ -44,12 +44,8 @@ namespace polysat {
         clause_ref build();
 
         /// Insert constraints into the clause.
-        void push(sat::literal lit);
+        void insert(sat::literal lit);
-        void push(signed_constraint c);
+        void insert(signed_constraint c);
-        void push(inequality const& i) { push(i.as_signed_constraint()); }
-        // TODO: remove push
-        void insert(sat::literal lit) { push(lit); }
-        void insert(signed_constraint c) { push(c); }
         void insert(inequality const& i) { insert(i.as_signed_constraint()); }
 
         /// Inserting constraints into the clause.

src/math/polysat/conflict.cpp

@@ -308,7 +308,7 @@ namespace polysat {
     void conflict::add_lemma(signed_constraint const* cs, size_t cs_len) {
         clause_builder cb(s);
         for (size_t i = 0; i < cs_len; ++i)
-            cb.push(cs[i]);
+            cb.insert(cs[i]);
         add_lemma(cb.build());
     }
 
@@ -467,13 +467,11 @@ namespace polysat {
         clause_builder lemma(s);
 
         for (auto c : *this)
-            lemma.push(~c);
+            lemma.insert(~c);
 
         for (unsigned v : m_vars) {
             auto eq = s.eq(s.var(v), s.get_value(v));
-            if (eq.bvalue(s) == l_undef)
+            lemma.insert_eval(~eq);
-                s.assign_eval(eq.blit());
-            lemma.push(~eq);
         }
         s.decay_activity();
 

src/math/polysat/solver.cpp

@@ -1033,12 +1033,8 @@ namespace polysat {
 
     void solver::add_clause(unsigned n, signed_constraint* cs, bool is_redundant) {
         clause_builder cb(*this);
-        for (unsigned i = 0; i < n; ++i) {
+        for (unsigned i = 0; i < n; ++i)
-            signed_constraint c = cs[i];
+            cb.insert(cs[i]);
-            if (c.is_always_false())
-                continue;
-            cb.push(c);
-        }
         clause_ref clause = cb.build();
         if (clause) {
             clause->set_redundant(is_redundant);

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(~sc);
+        cb.insert(~sc);
-        cb.push(~premise);
+        cb.insert(~premise);
-        cb.push(conseq);
+        cb.insert(conseq);
         clause_ref just = cb.build();
         SASSERT(just);
         s.add_clause(*just);

src/math/polysat/variable_elimination.cpp

@@ -103,10 +103,10 @@ namespace polysat {
 
             clause_builder cb(s);
             for (auto [w, wv] : a)
-                cb.push(~s.eq(s.var(w), wv));
+                cb.insert(~s.eq(s.var(w), wv));
-            cb.push(~c);
+            cb.insert(~c);
-            cb.push(~c_target);
+            cb.insert(~c_target);
-            cb.push(c_new);
+            cb.insert(c_new);
             core.add_lemma(cb.build());
         }
     }

src/test/polysat.cpp

@@ -490,9 +490,9 @@ namespace polysat {
             clause_builder cb(s);
             auto u = s.var(s.add_var(4));
             auto v = s.var(s.add_var(4));
-            cb.push(s.eq(u));
+            cb.insert(s.eq(u));
-            cb.push(~s.eq(u - 1));
+            cb.insert(~s.eq(u - 1));
-            cb.push(s.ule(u, v));
+            cb.insert(s.ule(u, v));
             auto cl = cb.build();
             simp.apply(*cl);
             std::cout << *cl << "\n";