cleanup

src/math/polysat/conflict.cpp

@@ -70,7 +70,7 @@ namespace polysat {
 
         void infer_lemmas_for_value(pvar v, conflict& core) {
             (void)m_poly_sup.perform(v, core);
-            (void)m_saturation.perform(v, core);
+            m_saturation.perform(v, core);
         }
 
         void infer_lemmas_for_value(pvar v, signed_constraint const& c, conflict& core) {
@@ -267,10 +267,9 @@ namespace polysat {
     void conflict::insert(signed_constraint c) {
         if (contains(c))
             return;
-        if (c.is_always_true())
-            return;
         LOG("Inserting " << lit_pp(s, c));
         SASSERT_EQ(c.bvalue(s), l_true);
+        SASSERT(!c.is_always_true());   // such constraints would be removed earlier
         SASSERT(!c.is_always_false());  // if we added c, the core would be a tautology
         SASSERT(!c->vars().empty());
         m_literals.insert(c.blit().index());
@@ -283,19 +282,6 @@ namespace polysat {
         }
     }
 
-    void conflict::insert_eval(signed_constraint c) {
-        switch (c.bvalue(s)) {
-        case l_undef:
-            s.assign_eval(c.blit());
-            break;
-        case l_true:
-            break;
-        case l_false:
-            break;
-        }
-        insert(c);
-    }
-
     void conflict::insert_vars(signed_constraint c) {
         for (pvar v : c->vars())
             if (s.is_assigned(v))
@@ -307,16 +293,14 @@ namespace polysat {
     }
 
     void conflict::add_lemma(char const* name, signed_constraint const* cs, size_t cs_len) {
-        clause_builder cb(s);
+        clause_builder cb(s, name);
         for (size_t i = 0; i < cs_len; ++i)
             cb.insert_eval(cs[i]);
-        add_lemma(name, cb.build());
+        add_lemma(cb.build());
     }
 
-    void conflict::add_lemma(char const* name, clause_ref lemma) {
+    void conflict::add_lemma(clause_ref lemma) {
-        if (!name)
+        LOG_H3("Lemma: " << ": " << show_deref(lemma));
-            name = "<unknown>";
-        LOG_H3("Lemma " << name << ": " << show_deref(lemma));
         VERIFY(lemma);
 
         for (auto lit : *lemma)
@@ -325,7 +309,6 @@ namespace polysat {
 
         s.m_simplify_clause.apply(*lemma);
         lemma->set_redundant(true);
-        lemma->set_name(name);
         for (sat::literal lit : *lemma) {
             LOG(lit_pp(s, lit));
             // NOTE: it can happen that the literal's bvalue is l_true at this point.

src/math/polysat/conflict.h

@@ -145,29 +145,24 @@ namespace polysat {
 
         /**
          * Insert constraint c into conflict state.
-         *
-         * Skips trivial constraints:
-         *  - e.g., constant constraints such as "4 > 1"
          */
         void insert(signed_constraint c);
 
         /** Insert assigned variables of c */
         void insert_vars(signed_constraint c);
 
-        /** Evaluate constraint under assignment and insert it into conflict state. */
-        void insert_eval(signed_constraint c);
-
         /** Add a lemma to the conflict, to be added after conflict resolution */
         void add_lemma(char const* name, std::initializer_list<signed_constraint> cs);
         void add_lemma(char const* name, signed_constraint const* cs, size_t cs_len);
-        void add_lemma(char const* name, clause_ref lemma);
+        void add_lemma(clause_ref lemma);
+        void add_lemma(char const* name, clause_ref lemma) { lemma->set_name(name); add_lemma(lemma); }  // remove
 
         /** Re-add a lemma to the conflict that we were unable to add after the previous conflict. */
         void restore_lemma(clause_ref lemma);
 
         /** Remove c from core */
         void remove(signed_constraint c);
-        void remove_var(pvar v);
+
         /**
          * Remove all constraints and variables from the conflict state.
          * Use this during conflict resolution if the core needs to be replaced.

src/math/polysat/saturation.cpp

@@ -216,8 +216,8 @@ namespace polysat {
         SASSERT(all_of(m_lemma, [this](sat::literal lit) { return is_forced_false(s.lit2cnstr(lit)); }));
 
         m_lemma.insert(c);
-        core.add_lemma(m_rule, m_lemma.build());
+        m_lemma.set_name(m_rule);
-        verbose_stream() << "Lemma\n";
+        core.add_lemma(m_lemma.build());
         log_lemma(v, core);
         return true;
     }
@@ -247,7 +247,8 @@ namespace polysat {
             return false;
 
         m_lemma.insert_eval(c);
-        core.add_lemma(m_rule, m_lemma.build());
+        m_lemma.set_name(m_rule);
+        core.add_lemma(m_lemma.build());
         log_lemma(v, core);
         return true;
     }

src/math/polysat/solver.cpp

@@ -1056,10 +1056,9 @@ namespace polysat {
     void solver::assign_eval(sat::literal lit) {
         signed_constraint const c = lit2cnstr(lit);
         LOG_V(10, "Evaluate: " << lit_pp(*this, lit));
-        // assertion is false
         if (!c.is_currently_true(*this)) IF_VERBOSE(0, verbose_stream() << c << " is not currently true\n");
         SASSERT(c.is_currently_true(*this));
-        VERIFY(c.is_currently_true(*this));
+        VERIFY_EQ(c.eval(*this), l_true);
         unsigned level = 0;
         // NOTE: constraint may be evaluated even if some variables are still unassigned (e.g., 0*x doesn't depend on x).
         for (auto v : c->vars())

src/math/polysat/solver.h

@@ -287,7 +287,6 @@ namespace polysat {
         void rescale_activity();
 
         void report_unsat();
-        void learn_lemma(clause& lemma);
         void backjump(unsigned new_level);
 
         void add_clause(clause_ref clause);

src/math/polysat/variable_elimination.cpp

@@ -421,7 +421,7 @@ namespace polysat {
             LOG("p1:    " << p1);
             LOG("p2:    " << p2);
                         
-            clause_builder cb(s);
+            clause_builder cb(s, "variable elimination");
 
             if (evaluated) {
                 for (auto [w, wv] : sub)
@@ -434,7 +434,7 @@ namespace polysat {
             cb.insert(c_new);
             ref<clause> c = cb.build();
             if (c) // Can we get tautologies this way?
-                core.add_lemma("variable elimination", c);
+                core.add_lemma(c);
         }
     }