na

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

src/math/polysat/conflict_core.cpp

@@ -10,6 +10,17 @@ Author:
     Nikolaj Bjorner (nbjorner) 2021-03-19
     Jakob Rath 2021-04-6
 
+Notes:
+
+ TODO: constraints containing v could be tracked incrementally when constraints are added/removed using an index.
+
+ TODO: try a final core reduction step or other core minimization
+
+
+ TODO: maybe implement by marking literals instead (like SAT solvers are doing); if we need to iterate, keep an indexed_uint_set (from util/uint_set.h)
+       (i.e., instead of keeping an explicit list of constraints as core, we just mark them.)
+       (we still need the list though, for new/temporary constraints.)
+
 --*/
 
 #include "math/polysat/conflict_core.h"
@@ -124,9 +135,6 @@ namespace polysat {
             SASSERT((core_has_pos && clause_has_pos) || (core_has_neg && clause_has_neg));
         });
 
-        // TODO: maybe implement by marking literals instead (like SAT solvers are doing); if we need to iterate, keep an indexed_uint_set (from util/uint_set.h)
-        //       (i.e., instead of keeping an explicit list of constraints as core, we just mark them.)
-        //       (we still need the list though, for new/temporary constraints.)
         int j = 0;
         for (auto c : m_constraints)
             if (c->bvar() != var)
@@ -196,14 +204,14 @@ namespace polysat {
         LOG("model_level: " << model_level);
         clause_builder lemma(*m_solver);
 
-        // TODO: try a final core reduction step?
-
         for (auto c : m_constraints) {
             if (!c->has_bvar())
                 keep(c);
             lemma.push(~c);
         }
 
+
+        // TODO: need to revisit this for when there are literals obtained by semantic propagation 
         if (m_needs_model) {
             // TODO: add equalities corresponding to current model.
             //       until we properly track variables (use marks from solver?), we just use all of them (reverted decision and the following ones should have been popped from the stack)
@@ -270,7 +278,7 @@ namespace polysat {
                 return true;
 
         // No value resolution method was successful => fall back to saturation and variable elimination
-        while (true) {  // TODO: limit?
+        while (s().inc()) { 
             // TODO: as a last resort, substitute v by m_value[v]?
             if (!try_saturate(v))
                 break;
@@ -281,18 +289,11 @@ namespace polysat {
     }
 
     bool conflict_core::try_eliminate(pvar v) {       
-        // TODO: could be tracked incrementally when constraints are added/removed
+        bool has_v = false;
-        vector<signed_constraint> v_constraints;
         for (auto c : *this)
-            if (c->contains_var(v)) {
+            has_v |= c->contains_var(v);
-                v_constraints.push_back(c);
+        if (!has_v)
-                break;
-            }
-
-        // Variable already eliminated trivially (does this ever happen?)
-        if (v_constraints.empty())
             return true;
-
         for (auto* engine : ve_engines)
             if (engine->perform(*m_solver, v, *this))
                 return true;

src/math/polysat/saturation.cpp

@@ -23,6 +23,11 @@ TODO: when we check that 'x' is "unary":
 - in principle, 'x' could be any polynomial. However, we need to divide the lhs by x, and we don't have general polynomial division yet.
   so for now we just allow the form 'value*variable'.
    (extension to arbitrary monomials for 'x' should be fairly easy too)
+
+TODO: 
+- resolve away the "problematic" premise (non-linear inequality etc) that is reduced by a saturation rule.
+  - it would work by adding the explanations for the resolved premises to the reason clause 
+  - and removing the literal from the core
 --*/
 #include "math/polysat/saturation.h"
 #include "math/polysat/solver.h"

src/math/polysat/solver.h

@@ -228,7 +228,7 @@ namespace polysat {
         void new_constraint(signed_constraint c, unsigned dep, bool activate);
         static void insert_constraint(signed_constraints& cs, signed_constraint c);
 
-        viable& get_viable() { return m_viable; }
+        bool inc() { return m_lim.inc(); }
 
         bool invariant();
         static bool invariant(signed_constraints const& cs);