Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat

src/math/polysat/conflict.cpp

@@ -191,7 +191,7 @@ namespace polysat {
 
         SASSERT(lit != sat::null_literal);
         SASSERT(~lit != sat::null_literal);
-        SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c){ return !c->has_bvar(); }));
+        SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c){ return !c->has_bvar(); }));
         SASSERT(contains_literal(lit));
         SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
         SASSERT(!contains_literal(~lit));
@@ -219,7 +219,7 @@ namespace polysat {
 
     clause_builder conflict::build_lemma() {
         SASSERT(std::all_of(m_vars.begin(), m_vars.end(), [&](pvar v) { return s.is_assigned(v); }));
-        SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c) { return !c->has_bvar(); }));
+        SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c) { return !c->has_bvar(); }));
 
         LOG_H3("Build lemma from core");
         LOG("core: " << *this);

src/math/polysat/explain.cpp

@@ -146,7 +146,7 @@ namespace polysat {
                 if (!c2->has_bvar() || l_undef == c2.bvalue(s))
                     core.keep(c2);  // adds propagation of c to the search stack
                 core.reset();
-                LOG("reduced to " << c2);
+                LOG_H3("Polynomial superposition " << eq << " " << c << " reduced to " << c2);
                 if (c2.bvalue(s) == l_false) {
                     core.insert(eq);
                     core.insert(c);
@@ -161,12 +161,10 @@ namespace polysat {
     }
 
     bool ex_polynomial_superposition::try_explain(pvar v, conflict& core) {
-        LOG_H3("Trying polynomial superposition...");
         reduce_by(v, core);
         lbool result = l_undef;
         while (result == l_undef)
             result = try_explain1(v, core);
-        LOG("success? " << result);
         return result == l_true;
     }
 

src/math/polysat/fixplex_def.h

@@ -1335,7 +1335,7 @@ namespace polysat {
     template<typename Ext>
     bool fixplex<Ext>::propagate_strict_bounds(ineq const& i) {
         var_t v = i.v, w = i.w;
-        bool s = i.strict;
+        //bool s = i.strict;
         auto* vlo = m_vars[v].m_lo_dep, *vhi = m_vars[v].m_hi_dep;
         auto* wlo = m_vars[w].m_lo_dep, *whi = m_vars[w].m_hi_dep;
 
@@ -1363,7 +1363,7 @@ namespace polysat {
     template<typename Ext>
     bool fixplex<Ext>::propagate_non_strict_bounds(ineq const& i) {
         var_t v = i.v, w = i.w;
-        bool s = i.strict;
+        // bool s = i.strict;
         auto* vlo = m_vars[v].m_lo_dep, *vhi = m_vars[v].m_hi_dep;
         auto* wlo = m_vars[w].m_lo_dep, *whi = m_vars[w].m_hi_dep;
 

src/math/polysat/forbidden_intervals.cpp

@@ -13,11 +13,6 @@ Author:
     Jakob Rath 2021-04-6
 
 
-TODO:
-compute forbidden interval coefficients a1, a2 modulo current assignment to handle pseudo-linear cases.
-test_mont_bounds(8) produces constraint 13 <= v1*v2, where v2 = 1, then v1 is linear and is constrained above 13.
-
-
 
 --*/
 #include "math/polysat/forbidden_intervals.h"
@@ -175,6 +170,7 @@ namespace polysat {
     }
 
 
+
     /** Precondition: all variables other than v are assigned.
      *
      * \param[out] out_interval     The forbidden interval for this constraint
@@ -186,6 +182,20 @@ namespace polysat {
     {
         if (!c->is_ule())
             return false;
+        
+        struct backtrack {
+            bool released = false;
+            vector<signed_constraint>& side_cond;
+            unsigned sz;
+            backtrack(vector<signed_constraint>& s):side_cond(s), sz(s.size()) {}
+            ~backtrack() {
+                if (!released)
+                    side_cond.shrink(sz);
+            }
+        };
+
+        backtrack _backtrack(out_side_cond);
+        
         // Current only works when degree(v) is at most one on both sides
         pdd lhs = c->to_ule().lhs();
         pdd rhs = c->to_ule().rhs();
@@ -206,6 +216,16 @@ namespace polysat {
         rational const pow2 = rational::power_of_two(sz);
         rational const minus_one = pow2 - 1;
 
+        /**
+        * TODO: to express the interval for coefficient 2^i symbolically,
+        * we need right-shift/upper-bits-extract in the language.
+        * So currently we can only do it if the coefficient is 1 or -1.
+        */
+
+        auto coefficient_is_handled = [&](rational const& r) {
+            return r.is_zero() || r.is_one() || r == minus_one;
+        };
+
         pdd p1 = m.zero();
         pdd e1 = m.zero();
         if (deg1 == 0)
@@ -247,13 +267,13 @@ namespace polysat {
         }
         rational a1 = p1.val();
         rational a2 = p2.val();
-        // TODO: to express the interval for coefficient 2^i symbolically, we need right-shift/upper-bits-extract in the language.
+
-        // So currently we can only do it if the coefficient is 1 or -1.
         LOG("values " << a1 << " " << a2);
-        if (!a1.is_zero() && !a1.is_one() && a1 != minus_one)
+        if (!coefficient_is_handled(a1)) 
             return false;
-        if (!a2.is_zero() && !a2.is_one() && a2 != minus_one)
+        if (!coefficient_is_handled(a2))
             return false;
+        
         /*
         unsigned j1 = 0;
         unsigned j2 = 0;
@@ -269,7 +289,9 @@ namespace polysat {
         // Concrete values of evaluable terms
         auto e1s = e1.subst_val(s.assignment());
         auto e2s = e2.subst_val(s.assignment());
-        // TODO: this is not always true! cjust[v]/conflict may contain unassigned variables (they're coming from a previous conflict, but together they lead to a conflict. need something else to handle that.)
+        // TODO: this is not always true! cjust[v]/conflict may contain unassigned variables
+        // (they're coming from a previous conflict, but together they lead to a conflict.
+        // need something else to handle that.)
         if (!e1s.is_val())
             return false;
         if (!e2s.is_val())
@@ -280,9 +302,9 @@ namespace polysat {
         bool is_trivial;
         pdd condition_body = m.zero();
         pdd lo = m.zero();
-        rational lo_val = rational::zero();
+        rational lo_val(0);
         pdd hi = m.zero();
-        rational hi_val = rational::zero();
+        rational hi_val(0);
 
         if (a2.is_zero()) {
             SASSERT(!a1.is_zero());
@@ -326,6 +348,8 @@ namespace polysat {
             }
         }
 
+        _backtrack.released = true;
+
         if (condition_body.is_val()) {
             // Condition is trivial; no need to create a constraint for that.
             SASSERT(is_trivial == condition_body.is_zero());

src/math/polysat/saturation.cpp

@@ -147,20 +147,26 @@ namespace polysat {
         auto c2 = s.ule(y, pddm.mk_val(y_lo));
         new_constraints.insert(c1);
         new_constraints.insert(c2);
-        LOG("bounded " << bound << " : " << c1 << " " << c2);
+        LOG("bounded " << bound << " : " << x << " " << x_max << " " << y << " " << y_max << " " << c1 << " " << c2);
+    }
+
+    rational inf_saturate::max_value(pdd const& x) {
+        if (x.is_var())
+            return s.m_viable.max_viable(x.var());
+        else if (x.is_val())
+            return x.val();
+        else
+            return x.manager().max_value();
     }
 
     // determine worst case upper bounds for x, y
     // then extract premises for a non-worst-case bound.
     void inf_saturate::push_omega(vector<signed_constraint>& new_constraints, pdd const& x, pdd const& y) {     
         auto& pddm = x.manager();
-        rational x_max = pddm.max_value();
+        rational x_max = max_value(x);
-        rational y_max = pddm.max_value();
+        rational y_max = max_value(y);
         
-        if (x.is_var()) 
+        LOG("pushing " << x << " " << y);
-            x_max = s.m_viable.max_viable(x.var());
-        if (y.is_var()) 
-            y_max = s.m_viable.max_viable(y.var());        
 
         if (x_max * y_max  > pddm.max_value())            
             push_omega_bisect(new_constraints, x, x_max, y, y_max);
@@ -419,11 +425,13 @@ namespace polysat {
         new_constraints.push_back(c.as_signed_constraint());
         if (c.is_strict) {
             new_constraints.push_back(s.ule(l_val, c.lhs));
-            return propagate(core, c, c, s.ult(r_val, c.rhs), new_constraints);
+            auto conseq = s.ult(r_val, c.rhs);
+            return propagate(core, c, c, conseq, new_constraints);
         }
         else {
             new_constraints.push_back(s.ule(c.rhs, r_val));
-            return propagate(core, c, c, s.ule(c.lhs, r_val), new_constraints);
+            auto conseq = s.ule(c.lhs, r_val);
+            return propagate(core, c, c, conseq, new_constraints);
         }
     }
 

src/math/polysat/saturation.h

@@ -89,6 +89,8 @@ namespace polysat {
         // p := coeff*x*y where coeff_x = coeff*x, x a variable
         bool is_coeffxY(pdd const& coeff_x, pdd const& p, pdd& y);
 
+        rational max_value(pdd const& x);
+
     public:
         inf_saturate(solver& s) : inference_engine(s) {}
         bool perform(pvar v, conflict& core) override;

src/math/polysat/solver.cpp

@@ -450,9 +450,7 @@ namespace polysat {
                     continue;
                 justification& j = m_justification[v];
                 LOG("Justification: " << j);
-                if (j.level() <= base_level())
+                if (j.level() > base_level() && !resolve_value(v) && j.is_decision()) {
-                    break;
-                if (!resolve_value(v) && j.is_decision()) {               
                     revert_decision(v);
                     return;
                 }
@@ -464,8 +462,8 @@ namespace polysat {
                 sat::bool_var const var = lit.var();
                 if (!m_conflict.is_bmarked(var))
                     continue;
-                if (m_bvars.level(var) <= base_level())  // TODO: this doesn't work with out-of-level-order iteration.
+                if (m_bvars.level(var) <= base_level())  
-                    break;
+                    continue;
                 if (m_bvars.is_decision(var)) {
                     revert_bool_decision(lit);
                     return;
@@ -489,7 +487,7 @@ namespace polysat {
     */
     void solver::resolve_bool(sat::literal lit) {       
         SASSERT(m_bvars.is_propagation(lit.var()));
-        clause other = *m_bvars.reason(lit.var());
+        clause const& other = *m_bvars.reason(lit.var());
         LOG_H3("resolve_bool: " << lit << " " << other);
         m_conflict.resolve(m_constraints, lit, other);
     }
@@ -518,6 +516,7 @@ namespace polysat {
         SASSERT(!lemma.empty());
         lemma.set_justified_var(v);
         add_lemma(lemma);
+        if (!is_conflict())
             decide_bool(lemma);
     }
 
@@ -623,7 +622,8 @@ namespace polysat {
         clause_builder reason_builder = m_conflict.build_lemma();
         
 
-        bool contains_lit = std::find(reason_builder.begin(), reason_builder.end(), ~lit);
+        SASSERT(std::find(reason_builder.begin(), reason_builder.end(), ~lit));
+#if 0
         if (!contains_lit) {
             // At this point, we do not have ~lit in the reason.
             // For now, we simply add it (thus weakening the reason)
@@ -638,6 +638,7 @@ namespace polysat {
             std::cout << "ADD extra " << ~lit << "\n";
             reason_builder.push(~lit);
         }
+#endif
         clause_ref reason = reason_builder.build();
 
         if (reason->empty()) {

src/test/fixplex.cpp

@@ -389,7 +389,7 @@ namespace polysat {
         std::cout << "    test_lp(rows, ineqs, bounds); \n }\n";
     }
 
-    static unsigned num_test = 0;
+    //    static unsigned num_test = 0;
 
     static void test_lp(
         vector<svector<std::pair<unsigned, uint64_t>>> const& rows,

src/test/polysat.cpp

@@ -876,10 +876,10 @@ namespace polysat {
     }
 
     // x*y <= b & a <= x & !Omega(x*y) => a*y <= b
-    static void test_ineq_non_axiom4(unsigned bw = 32) {
+    static void test_ineq_non_axiom4(unsigned bw, unsigned i) {
         auto const bound = rational::power_of_two(bw - 1);
-        for (unsigned i = 0; i < 24; ++i) {
         scoped_solver s(__func__);
+        LOG("permutation: " << i);
         auto x = s.var(s.add_var(bw));
         auto y = s.var(s.add_var(bw));
         auto a = s.var(s.add_var(bw));
@@ -893,6 +893,10 @@ namespace polysat {
         s.check();
         s.expect_sat();
     }
+    
+    static void test_ineq_non_axiom4(unsigned bw = 32) {
+        for (unsigned i = 0; i < 24; ++i)
+            test_ineq_non_axiom4(bw, i);
     }
 
     // a < xy & x <= b  & !Omega(x*y) => a < b*y
@@ -1063,8 +1067,8 @@ void tst_polysat() {
 //    polysat::test_ineq_axiom1();
 //    polysat::test_ineq_axiom2();
 //    polysat::test_ineq_axiom3();
-    polysat::test_ineq_non_axiom1();
+ //   polysat::test_ineq_non_axiom1();
-    polysat::test_ineq_non_axiom4();
+    polysat::test_ineq_non_axiom4(32, 5);
     polysat::test_ineq_axiom4();
     polysat::test_ineq_axiom5();
     polysat::test_ineq_axiom6();