add review comments based on debugging

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

src/math/polysat/conflict.cpp

@@ -68,8 +68,14 @@ namespace polysat {
             , m_free_variable_elimination(s)
         {}
 
+        // 
+        // NSB review: the plugins need not be mutually exclusive
+        // Shouldn't saturation and superposition be allowed independently?
+        // If they create propagations or conflict lemmas we select the 
+        // tightest propagation as part of backjumping.
+        // 
         bool try_resolve_value(pvar v, conflict& core) {
-            if (m_poly_sup.perform(v, core))
+            if (m_poly_sup.perform(v, core)) 
                 return true;
             if (m_saturation.perform(v, core))
                 return true;
@@ -252,6 +258,10 @@ namespace polysat {
             logger().begin_conflict(header_with_var("forbidden interval lemma for v", v));
             VERIFY(s.m_viable.resolve(v, *this));
         }
+        // NSB review:
+        // Saturation is not invoked on forbidden interval conflicts.
+        // We miss propagations.
+        // m_resolver->try_resolve_value(v, *this);
         SASSERT(!empty());
     }
 
@@ -407,6 +417,11 @@ namespace polysat {
         }
         logger().log(inf_resolve_value(s, v));
 
+        //
+        // NSB review: if try_resolve_value returns true, it adds propagations or conflict lemmas.
+        // the return value should not influence resolution. Indeed the code in solver.cpp
+        // just ignores the return value. It seems this function should not have a return value.
+        // 
         if (m_resolver->try_resolve_value(v, *this))
             return true;
 

src/math/polysat/saturation.cpp

@@ -81,8 +81,17 @@ namespace polysat {
         // NSB - review is it enough to propagate a new literal even if it is not false?
         // unit propagation does not require conflicts.
         // it should just avoid redundant propagation on literals that are true
+        //
+        // Furthermore propagation cannot be used when the resolved variable comes from 
+        // forbidden interval conflicts. The propagated literal effectively adds a new and simpler bound
+        // on the non-viable variable. This bound then enables tighter non-viability conflicts.
+        // Effectively c is forced false, but it is forced false within the context of constraints used for viability.
+        //
+        // The effective level of the propagation is the level of all the other literals. If their level is below the
+        // last decision level (conflict level) we expect the propagation to be useful.
+        // The current assumptions on how conflict lemmas are used do not accomodate propagation it seems.
         // 
-        if (!is_forced_false(c))
+        if (!is_forced_false(c)) 
             return false;
 
         // TODO: ??? this means that c is already on the search stack, so presumably the lemma won't help. Should check whether this case occurs.
@@ -443,7 +452,7 @@ namespace polysat {
     }
 
     /**
-     * p <= k & p*x + q = 0 & q = 0 => p = 0 or x = 0 or x >= 2^K/k
+     * a <= k & a*x + b = 0 & b = 0 => a = 0 or x = 0 or x >= 2^K/k
      */
     bool saturation::try_mul_bounds(pvar x, conflict& core, inequality const& axb_l_y) {
         set_rule("[x] ax + b <= y & y = 0 & b = 0 & a <= k => x = 0 or a = 0 or x >= 2^K/k");
@@ -456,14 +465,13 @@ namespace polysat {
         rational b_val, y_val;
         if (!is_AxB_eq_0(x, axb_l_y, a, b, y))
             return false;
-
-        IF_VERBOSE(0, verbose_stream() << " mul bounds " << x << " " << axb_l_y.as_signed_constraint() << "\n");
-
+        if (a.is_val())
+            return false;        
         if (!is_forced_eq(b, 0))
             return false;
 
 
-#if 1
+#if 0
         // we could also use x.val(), a.val() if they exist and enforce bounds
         rational a_val, x_val;
         if (s.try_eval(a, a_val) && s.try_eval(X, x_val) && a_val*x_val != 0) {
@@ -471,6 +479,8 @@ namespace polysat {
         }
 #endif        
 
+        pdd minus_a = -a;
+
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;
@@ -480,8 +490,9 @@ namespace polysat {
             if (!d->is_ule())
                 continue;
             auto a_l_k = inequality::from_ule(d);
-            if (a_l_k.lhs() != a)
+            if (a_l_k.lhs() != a && a_l_k.lhs() != minus_a)
                 continue;
+            k = a_l_k.rhs();
             if (!k.is_val())
                 continue;
             if (k.val() <= 1)
@@ -498,9 +509,6 @@ namespace polysat {
             if (!is_forced_diseq(a, 0, a_eq_0))
                 return false;
 
-            IF_VERBOSE(0, verbose_stream() << " mul bounds " << axb_l_y.as_signed_constraint() << "\n");
-            return false;
-
             m_lemma.reset();
             m_lemma.insert(~s.eq(b));
             m_lemma.insert(~s.eq(y));

src/math/polysat/solver.cpp

@@ -823,6 +823,10 @@ namespace polysat {
         backjump_and_learn(max_jump_level);
     }
 
+    //
+    // NSB review: this code assumes that these lemmas are false.
+    // It does not allow saturation to add unit propagation into freshly created literals.
+    // 
     std::optional<lemma_score> solver::compute_lemma_score(clause const& lemma) {
         unsigned max_level = 0;     // highest level in lemma
         unsigned lits_at_max_level = 0;  // how many literals at the highest level in lemma