Add separate state for deciding on lemmas

src/math/polysat/solver.cpp

@@ -75,6 +75,7 @@ namespace polysat {
             else if (m_constraints.should_gc()) m_constraints.gc(*this);
             else if (m_simplify.should_apply()) m_simplify();
             else if (m_restart.should_apply()) m_restart();
+            else if (can_decide_on_lemma()) decide_on_lemma();
             else decide();
         }
         LOG_H2("UNDEF (resource limit)");
@@ -201,9 +202,10 @@ namespace polysat {
     void solver::propagate() {
         if (!can_propagate())
             return;
-        if (m_propagating)
+#ifndef NDEBUG
-            return;
+        SASSERT(!m_propagating);
-        m_propagating = true;
+        flet<bool> save_(m_propagating, true);
+#endif
         push_qhead();
         while (can_propagate()) {
             auto const& item = m_search[m_qhead++];
@@ -215,7 +217,6 @@ namespace polysat {
         linear_propagate();
         SASSERT(wlist_invariant());
         SASSERT(assignment_invariant());
-        m_propagating = false;
     }
 
     /**
@@ -320,6 +321,7 @@ namespace polysat {
 #if ENABLE_LINEAR_SOLVER
         m_linear_solver.pop(num_levels);
 #endif
+        drop_enqueued_lemma();
         while (num_levels > 0) {
             switch (m_trail.back()) {
             case trail_instr_t::qhead_i: {
@@ -598,12 +600,33 @@ namespace polysat {
         LOG("Learning: "<< lemma);
         SASSERT(!lemma.empty());
         add_clause(lemma);
-        if (!is_conflict())
+        enqueue_decision_on_lemma(lemma);
-            decide_bool(lemma);
     }
 
-    // Guess a literal from the given clause; returns the guessed constraint
+    void solver::enqueue_decision_on_lemma(clause& lemma) {
-    void solver::decide_bool(clause& lemma) {
+        m_lemmas.push_back(&lemma);
+    }
+
+    void solver::drop_enqueued_lemma() {
+        m_lemmas.reset();
+    }
+
+    bool solver::can_decide_on_lemma() {
+        return !m_lemmas.empty();
+    }
+
+    void solver::decide_on_lemma() {
+        SASSERT(!is_conflict());
+        SASSERT(m_lemmas.size() == 1);  // we expect to only have a single one
+        // TODO: maybe it would be nicer to have a queue of lemmas, instead of storing lemmas per-literal in m_bvars?
+        while (!m_lemmas.empty()) {
+            clause* lemma = m_lemmas.back();
+            m_lemmas.pop_back();
+            decide_on_lemma(*lemma);
+        }
+    }
+
+    void solver::decide_on_lemma(clause& lemma) {
         LOG_H3("Guessing literal in lemma: " << lemma);
         IF_LOGGING(m_viable.log());
         LOG("Boolean assignment: " << m_bvars);
@@ -718,10 +741,11 @@ namespace polysat {
 
         backjump(m_bvars.level(var) - 1);
 
+        // reason should force ~lit after propagation
         add_clause(*reason);
 
-        if (!is_conflict() && lemma)
+        if (lemma)  // TODO: can (should) this ever be NULL?
-            decide_bool(*lemma);
+            enqueue_decision_on_lemma(*lemma);
     }
 
     unsigned solver::level(sat::literal lit0, clause const& cl) {
@@ -808,7 +832,6 @@ namespace polysat {
         }
         SASSERT(!clause.empty());
         m_constraints.store(&clause, *this);
-        propagate();
     }
 
     void solver::add_clause(unsigned n, signed_constraint* cs, bool is_redundant) {

src/math/polysat/solver.h

@@ -105,8 +105,9 @@ namespace polysat {
         vector<signed_constraints> m_pwatch;      // watch list datastructure into constraints.
 #ifndef NDEBUG
         std::optional<pvar>      m_locked_wlist;  // restrict watch list modification while it is being propagated
-#endif
         bool                     m_propagating = false;  // set to true during propagation
+#endif
+        ptr_vector<clause>       m_lemmas;
 
         unsigned_vector          m_activity; 
         vector<pdd>              m_vars;
@@ -155,15 +156,18 @@ namespace polysat {
         void assign_eval(sat::literal lit);
         void activate_constraint(signed_constraint c);
         void deactivate_constraint(signed_constraint c);
-        void decide_bool(clause& lemma);
-        void decide_bool(sat::literal lit, clause* lemma);
         unsigned level(sat::literal lit, clause const& cl);
 
+        bool can_decide_on_lemma();
+        void decide_on_lemma();
+        void decide_on_lemma(clause& lemma);
+        void enqueue_decision_on_lemma(clause& lemma);
+        void drop_enqueued_lemma();
+
         void assign_core(pvar v, rational const& val, justification const& j);
         bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }
         bool is_decision(search_item const& item) const;
 
-
         bool should_search();
 
         void propagate(sat::literal lit);
@@ -369,7 +373,7 @@ namespace polysat {
 
         void updt_params(params_ref const& p);
 
-    };
+    };  // class solver
 
     class assignments_pp {
         solver const& s;