cleanup

src/sat/smt/polysat/core.cpp

@@ -151,25 +151,25 @@ namespace polysat {
     // create equality literal for unassigned variable.
     // return new_eq if there is a new literal.
 
-    sat::check_result core::check() {
+    lbool core::assign_variable() {
         if (m_var_queue.empty())
-            return final_check();
+            return l_true;
         m_var = m_var_queue.min_var();
         CTRACE("bv", is_assigned(m_var), display(tout << "v" << m_var << " is assigned\n"););
         SASSERT(!is_assigned(m_var));
-        
+
         auto& var_value = m_values[m_var];
         switch (m_viable.find_viable(m_var, var_value)) {
         case find_t::empty:
             viable_conflict(m_var);
-            return sat::check_result::CR_CONTINUE;
+            return l_false;
         case find_t::singleton: {
             auto p = var2pdd(m_var).mk_var(m_var);
             auto sc = m_constraints.eq(p, var_value);
             TRACE("bv", tout << "check-propagate v" << m_var << " := " << var_value << " " << sc << "\n");
             auto d = s.propagate(sc, m_viable.explain(), "viable-propagate");
             propagate_assignment(m_var, var_value, d);
-            return sat::check_result::CR_CONTINUE;
+            return l_false;
         }
         case find_t::multiple: {
             dependency d = null_dependency;
@@ -188,19 +188,31 @@ namespace polysat {
                 // let core assign equality.                    
                 break;
             }
-            return sat::check_result::CR_CONTINUE;
+            return l_false;
         }
         case find_t::resource_out:
             TRACE("bv", tout << "check-resource out v" << m_var << "\n");
-            return sat::check_result::CR_GIVEUP;
+            return l_undef;
         }
         UNREACHABLE();
-        return sat::check_result::CR_GIVEUP;
+        return l_undef;
     }
 
-    sat::check_result core::final_check() {
+    sat::check_result core::check() {
-
         lbool r = l_true;
+
+        switch (assign_variable()) {
+        case l_true:
+            break;
+        case l_false:
+            return sat::check_result::CR_CONTINUE;
+        case l_undef:
+            return sat::check_result::CR_GIVEUP;
+            // or:
+            // r = l_undef;
+            // break;
+        }
+
         switch (m_monomials.refine()) {
         case l_true:
             break;
@@ -268,7 +280,6 @@ namespace polysat {
         return result;
     }
 
-    // First propagate Boolean assignment, then propagate value assignment
     bool core::propagate() { 
         if (m_qhead == m_prop_queue.size())
             return false;
@@ -293,7 +304,6 @@ namespace polysat {
         TRACE("bv", tout << "propagate " << sc << " using " << dep << " := " << value << "\n");
         if (sc.is_always_false()) {
             s.set_conflict({dep}, "infeasible assignment");
-            decay_activity();
             return;
         }
         rational var_value;

src/sat/smt/polysat/core.h

@@ -90,9 +90,8 @@ namespace polysat {
 
         void add_watch(unsigned idx, unsigned var);
 
-        sat::check_result final_check();
+        lbool assign_variable();
         
-
         void add_axiom(signed_constraint sc);
 
         unsigned m_activity_inc = 128;

src/sat/smt/polysat/saturation.cpp

@@ -10,18 +10,6 @@ Author:
     Nikolaj Bjorner (nbjorner) 2021-03-19
     Jakob Rath 2021-04-6
 
-
-TODO: preserve falsification
-- each rule selects a certain premises that are problematic.
-  If the problematic premise is false under the current assignment, the newly inferred
-  literal should also be false in the assignment in order to preserve conflicts.
-
-
-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)
-
 --*/
 #include "sat/smt/polysat/core.h"
 #include "sat/smt/polysat/saturation.h"
@@ -125,16 +113,15 @@ namespace polysat {
         pdd x = c.var(v);
         pdd y = x;
         pdd z = x;       
-        auto& C = c.cs();
 
         if (!i.is_xY_l_xZ(v, y, z))
             return;
 
         auto ovfl = C.umul_ovfl(x, y);
         if (i.is_strict()) 
-            add_clause("[x] yx < zx ==>  Ω*(x,y) \\/ y < z", { i.dep(), ovfl, C.ult(y, z)}, false);
+            add_clause("[x] yx < zx ==> Ω*(x,y) \\/ y < z", { i.dep(), ovfl, C.ult(y, z)}, true);
         else 
-            add_clause("[x] yx <= zx  ==>  Ω*(x,y) \\/ y <= z \\/ x = 0", { i.dep(), ovfl, C.eq(x), C.ule(y, z) }, false);
+            add_clause("[x] yx <= zx ==> Ω*(x,y) \\/ y <= z \\/ x = 0", { i.dep(), ovfl, C.eq(x), C.ule(y, z) }, true);
     }
 
     /**
@@ -149,14 +136,14 @@ namespace polysat {
         auto y = c.var(v);
         pdd x = y;
         pdd z = y;
-        auto& C = c.cs();
         if (!i.is_Xy_l_XZ(v, x, z))
             return;
         for (constraint_id id : constraint_iterator(c, [&](auto const& sc) { return inequality::is_l_v(y, sc); })) {
             auto j = inequality::from_ule(c, id);
             pdd const& z_prime = i.lhs();
             bool is_strict = i.is_strict() || j.is_strict();
-            add_clause("[y] z' <= y & yx <= zx", { i.dep(), j.dep(), C.umul_ovfl(x, y), ineq(is_strict, z_prime * x, z * x) }, true);
+            add_clause("[y] z' <= y & yx <= zx ==> Ω*(x,y) \/ z'x <= zx", 
+                { i.dep(), j.dep(), C.umul_ovfl(x, y), ineq(is_strict, z_prime * x, z * x) }, true);
         }
     }
 
@@ -178,14 +165,14 @@ namespace polysat {
             auto j = inequality::from_ule(c, id);
             auto y_prime = j.rhs();
             bool is_strict = i.is_strict() || j.is_strict();
-            add_clause("[z] z <= y' && yx <= zx", { i.dep(), j.dep(), c.umul_ovfl(x, y_prime), ineq(is_strict, y * x, y_prime * x) }, true);
+            add_clause("[z] z <= y' && yx <= zx ==> Ω*(x,y') \/ yx <= y'x", 
+                { i.dep(), j.dep(), c.umul_ovfl(x, y_prime), ineq(is_strict, y * x, y_prime * x) }, true);
         }
     }
 
     // Ovfl(x, y) & ~Ovfl(y, z) ==> x > z
     void saturation::try_umul_ovfl(pvar v, umul_ovfl const& sc) {
         auto p = sc.p(), q = sc.q();
-        auto& C = c.cs();
         auto match_mul_arg = [&](auto const& sc2) { 
             auto p2 = sc2.to_umul_ovfl().p(), q2 = sc2.to_umul_ovfl().q(); 
             return p == p2 || p == q2 || q == p2 || q == q2;
@@ -209,9 +196,9 @@ namespace polysat {
             auto d2 = c.get_dependency(id);
             auto [q1, q2] = extract_mul_args(sc2);
             if (sc.sign())
-                add_clause("[y] ~ovfl(p, q1) & ovfl(p, q2) ==> q1 < q2", { d1, d2, C.ult(q1, q2) }, false);
+                add_clause("[y] ~ovfl(p, q1) & ovfl(p, q2) ==> q1 < q2", { d1, d2, C.ult(q1, q2) }, true);
             else 
-                add_clause("[y] ovfl(p, q1) & ~ovfl(p, q2) ==> q1 > q2", { d1, d2, C.ult(q2, q1)}, false);
+                add_clause("[y] ovfl(p, q1) & ~ovfl(p, q2) ==> q1 > q2", { d1, d2, C.ult(q2, q1)}, true);
         }         
     }