merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/polysat/conflict_core.cpp

@@ -138,14 +138,6 @@ namespace polysat {
         m_constraints.shrink(j);
     }
 
-    void conflict_core::keep(signed_constraint c) {
-        SASSERT(!c->has_bvar());
-        cm().ensure_bvar(c.get());
-        LOG("new constraint: " << c);
-        // Insert the temporary constraint from saturation into \Gamma.
-        handle_saturation_premises(c);
-    }
-
     void conflict_core::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) {
         // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
         //       clause: x \/ u \/ v
@@ -177,7 +169,9 @@ namespace polysat {
     }
 
     /** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */
-    void conflict_core::handle_saturation_premises(signed_constraint c) {
+    void conflict_core::keep(signed_constraint c) {
+        cm().ensure_bvar(c.get());
+        LOG_H3("keeping: " << c);
         // NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
         auto it = m_saturation_premises.find_iterator(c);
         if (it == m_saturation_premises.end())
@@ -186,9 +180,7 @@ namespace polysat {
         auto& premises = it->m_value;
         clause_builder c_lemma(s());
         for (auto premise : premises) {
-            cm().ensure_bvar(premise.get());
-            // keep(premise);
-            handle_saturation_premises(premise);
+            keep(premise);
             SASSERT(premise->has_bvar());
             c_lemma.push(~premise.blit());
             active_level = std::max(active_level, s().m_bvars.level(premise.blit()));
@@ -246,8 +238,8 @@ namespace polysat {
         for (unsigned v : m_vars) {
             if (!is_pmarked(v))
                 continue;
-            // SASSERT(!s().is_assigned());  // TODO: why does this trigger????
-            if (!s().is_assigned())
+            // SASSERT(!s().is_assigned(v));  // TODO: why does this trigger????
+            if (!s().is_assigned(v))
                 continue;
             if (s().m_justification[v].level() > model_level)
                 continue;

src/math/polysat/conflict_core.h

@@ -61,7 +61,6 @@ namespace polysat {
 
         // ptr_addr_map<constraint, vector<signed_constraint>> m_saturation_premises;
         map<signed_constraint, vector<signed_constraint>, obj_hash<signed_constraint>, default_eq<signed_constraint>> m_saturation_premises;
-        void handle_saturation_premises(signed_constraint c);
     public:
         conflict_core(solver& s);
         ~conflict_core();

src/math/polysat/explain.cpp

@@ -17,8 +17,6 @@ Author:
 
 namespace polysat {
 
-    constraint_manager& explainer::cm() { return s().m_constraints; }
-
     signed_constraint ex_polynomial_superposition::resolve1(pvar v, signed_constraint c1, signed_constraint c2) {
         // c1 is true, c2 is false
         SASSERT(c1.is_currently_true(s()));
@@ -35,7 +33,7 @@ namespace polysat {
         // (this condition might be too strict, but we use it for now to prevent looping)
         if (b.degree(v) <= r.degree(v))
             return {};
-        signed_constraint c = cm().eq(r);
+        signed_constraint c = s().eq(r);
         LOG("resolved: " << c << "        currently false? " << c.is_currently_false(s()));
         if (!c.is_currently_false(s()))
             return {};

src/math/polysat/explain.h

@@ -20,7 +20,6 @@ Author:
 namespace polysat {
 
     class solver;
-    class constraint_manager;
 
     class explainer {
         friend class conflict_core;
@@ -28,7 +27,6 @@ namespace polysat {
         void set_solver(solver& s) { m_solver = &s; }
     protected:
         solver& s() { return *m_solver; }
-        constraint_manager& cm();
     public:
         virtual ~explainer() {}
         virtual bool try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict_core& core) = 0;

src/math/polysat/search_state.h

@@ -75,13 +75,14 @@ namespace polysat {
     inline std::ostream& operator<<(std::ostream& out, search_state const& s) { return s.display(out); }
 
 
-    // Go backwards over the search_state
+    // Go backwards over the search_state.
+    // If new entries are added during processing an item, they will be queued for processing next after the current item.
     class search_iterator {
 
         search_state*   m_search;
 
         unsigned current;
-        unsigned first;
+        unsigned first;  // highest index + 1
 
         struct idx_range {
             unsigned current;
@@ -89,22 +90,41 @@ namespace polysat {
         };
         vector<idx_range>     m_index_stack;
 
-    public:
-        search_iterator(search_state& search):
-            m_search(&search) {
+        void init() {
             first = m_search->size();
-            current = first;  // we start one before the beginning, then it also works for empty m_search
+            current = first - 1;
         }
 
-        search_item const& operator*() const {
-            return (*m_search)[current];
+        void try_push_block() {
+            if (first != m_search->size()) {
+                m_index_stack.push_back({current, first});
+                init();
+            }
+        }
+
+        void pop_block() {
+            current = m_index_stack.back().current;
+            first = m_index_stack.back().first;
+            m_index_stack.pop_back();
         }
 
         unsigned last() {
             return m_index_stack.empty() ? 0 : m_index_stack.back().first;
         }
 
+    public:
+        search_iterator(search_state& search):
+            m_search(&search) {
+            init();
+            current++;  // we start one before the beginning, then it also works for empty m_search
+        }
+
+        search_item const& operator*() const {
+            return (*m_search)[current];
+        }
+
         bool next() {
+            try_push_block();
             if (current > last()) {
                 --current;
                 return true;
@@ -113,21 +133,10 @@ namespace polysat {
                 SASSERT(current == last());
                 if (m_index_stack.empty())
                     return false;
-                current = m_index_stack.back().current;
-                first = m_index_stack.back().first;
-                m_index_stack.pop_back();
+                pop_block();
                 return true;
             }
         }
-
-        // to be called after all saturations for a step are done
-        void push_block() {
-            if (first != m_search->size()) {
-                m_index_stack.push_back({current, first});
-                first = m_search->size();
-                current = first - 1;
-            }
-        }
     };
 
 }

src/math/polysat/solver.cpp

@@ -456,6 +456,7 @@ namespace polysat {
         while (search_it.next()) {
             LOG("Conflict: " << m_conflict);
             auto const& item = *search_it;
+            LOG_H2("Working on " << item);
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
@@ -477,7 +478,6 @@ namespace polysat {
                 // Resolve over boolean literal
                 SASSERT(item.is_boolean());
                 sat::literal const lit = item.lit();
-                LOG_H2("Working on blit " << lit);
                 sat::bool_var const var = lit.var();
                 if (!m_conflict.is_bmarked(var))
                     continue;

src/math/polysat/solver.h

@@ -62,6 +62,7 @@ namespace polysat {
         friend class viable;
         friend class assignment_pp;
         friend class assignments_pp;
+        friend class ex_polynomial_superposition;
         friend class inf_saturate;
         friend class constraint_manager;
 

src/math/polysat/ule_constraint.h

@@ -44,7 +44,7 @@ namespace polysat {
         inequality as_inequality(bool is_positive) const override;
         unsigned hash() const override;
         bool operator==(constraint const& other) const override;
-        bool is_eq() const { return m_rhs.is_zero(); }
+        bool is_eq() const override { return m_rhs.is_zero(); }
         pdd const& p() const { SASSERT(is_eq()); return m_lhs; }
     };