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

src/math/polysat/conflict.cpp

@@ -158,6 +158,7 @@ namespace polysat {
             SASSERT(m_vars_occurring.empty());
             SASSERT(m_lemmas.empty());
             SASSERT(m_narrow_queue.empty());
+            SASSERT(m_dep.is_null());
         }
         return is_empty;
     }
@@ -170,6 +171,7 @@ namespace polysat {
         m_lemmas.reset();
         m_narrow_queue.reset();
         m_level = UINT_MAX;
+        m_dep = null_dependency;
         SASSERT(empty());
     }
 
@@ -181,10 +183,11 @@ namespace polysat {
         return contains(lit) || contains(~lit);
     }
 
-    void conflict::init_at_base_level() {
+    void conflict::init_at_base_level(dependency dep) {
         SASSERT(empty());
         SASSERT(s.at_base_level());
         m_level = s.m_level;
+        m_dep = dep;
         SASSERT(!empty());
         // TODO: logger().begin_conflict???
         // TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after...
@@ -303,15 +306,15 @@ namespace polysat {
     }
 
     void conflict::add_lemma(char const* name, clause_ref lemma) {
+        if (!name)
+            name = "<unknown>";
+        LOG_H3("Lemma " << name << ": " << show_deref(lemma));
+        VERIFY(lemma);
 
         for (auto lit : *lemma)
             if (s.m_bvars.is_true(lit))
                 verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n";
 
-        if (!name)
-            name = "<unknown>";
-        LOG_H3("Lemma " << name << ": " << show_deref(lemma));
-        SASSERT(lemma);
         s.m_simplify_clause.apply(*lemma);
         lemma->set_redundant(true);
         lemma->set_name(name);
@@ -434,7 +437,7 @@ namespace polysat {
 
         clause_builder lemma(s);
 
-        for (auto c : *this)
+        for (signed_constraint c : *this)
             lemma.insert(~c);
 
         for (unsigned v : m_vars) {
@@ -501,6 +504,27 @@ namespace polysat {
     }
 #endif
 
+    void conflict::find_deps(dependency_vector& out_deps) const {
+        sat::literal_vector todo;
+        sat::literal_set done;
+        indexed_uint_set deps;
+
+        LOG("conflict: " << *this);
+
+        // TODO: starting at literals/variables in the conflict, chase propagations backwards and accumulate dependencies.
+        verbose_stream() << "WARNING: unsat_core requested but dependency tracking in polysat is TODO\n";
+        for (signed_constraint c : *this) {
+            dependency d = s.m_bvars.dep(c.blit());
+            if (!d.is_null())
+                deps.insert(d.val());
+        }
+
+        for (unsigned d : deps)
+            out_deps.push_back(dependency(d));
+        if (!m_dep.is_null())
+            out_deps.push_back(m_dep);
+    }
+
     std::ostream& conflict::display(std::ostream& out) const {
         char const* sep = "";
         for (auto c : *this)

src/math/polysat/conflict.h

@@ -101,6 +101,7 @@ namespace polysat {
 
         // Level at which the conflict was discovered
         unsigned m_level = UINT_MAX;
+        dependency m_dep = null_dependency;
 
     public:
         conflict(solver& s);
@@ -126,7 +127,7 @@ namespace polysat {
         bool is_relevant(sat::literal lit) const;
 
         /** conflict due to obvious input inconsistency */
-        void init_at_base_level();
+        void init_at_base_level(dependency dep);
         /** conflict because the constraint c is false under current variable assignment */
         void init(signed_constraint c);
         /** boolean conflict with the given clause */
@@ -194,6 +195,8 @@ namespace polysat {
         /** Move the literals to be narrowed out of the conflict */
         sat::literal_vector take_narrow_queue();
 
+        void find_deps(dependency_vector& out_deps) const;
+
         std::ostream& display(std::ostream& out) const;
     };
 

src/math/polysat/saturation.cpp

@@ -1600,8 +1600,7 @@ namespace polysat {
     }
 
     /**
-     * if !x_split: update d such that 0 <= a*x*y0 + b*x + c*y0 + d < M for every value x_min <= x <= x_max
+     * Update d such that -M < a*x*y0 + b*x + c*y0 + d < M for every value x_min <= x <= x_max, return x_split such that [x_min,x_split[ and [x_split,x_max] can fit into [0,M[
-     * if x_split: update d such that -M < a*x*y0 + b*x + c*y0 + d < M for every value x_min <= x <= x_max, return x_split such that [x_min,x_split[ and [x_split,x_max] can fit into [0,M[
      * return false if there is no such d.
      */
     bool saturation::adjust_bound(rational const& x_min, rational const& x_max, rational const& y0, rational const& M, rational const& a, rational const& b, rational const& c, rational& d, rational* x_split) {
@@ -1614,14 +1613,22 @@ namespace polysat {
         if (max - min >= M)
             return false;
 
+        // k0 = min k. val + kM >= 0
+        //    = min k. k >= -val/M
+        //    = ceil(-val/M) = -floor(val/M)
         rational offset = rational::zero();
+#if 0
         if (max >= M)
             offset = -M * floor(max / M);
         else if (max < 0)
             offset = M * floor((-max + M - 1) / M);
+#else
+        if (max < 0 || max >= M)
+            offset = -M * floor(max / M);
+#endif
         d += offset;
 
-        // If min + offset < 0, then [min,max] contained a multiple of M.
+        // If min + offset < 0, then [min,max] contains a multiple of M.
         if (min + offset < 0) {
             if (!x_split)
                 return false;
@@ -1735,11 +1742,12 @@ namespace polysat {
 
         VERIFY(x_min <= x_max);
 
-        // TODO: d +/- M would suffice here
         rational d1 = dd1;
+        if (a1*x_min*y0 + b1*x_min + c1*y0 + d1 < 0)
+            d1 += M;
         rational d2 = dd2;
-        VERIFY(adjust_bound(x_min, x_max, y0, M, a1, b1, c1, d1, nullptr));
+        if (a2*x_min*y0 + b2*x_min + c2*y0 + d2 < 0)
-        VERIFY(adjust_bound(x_min, x_max, y0, M, a2, b2, c2, d2, nullptr));
+            d2 += M;
 
         IF_VERBOSE(2,
                    verbose_stream() << "Adjusted for x in [" << x_min << "; " << x_max << "]\n";
@@ -1837,8 +1845,8 @@ namespace polysat {
                    verbose_stream() << "\n---\n\n";
                    verbose_stream() << "constraint " << lit_pp(s, a_l_b) << "\n";
                    verbose_stream() << "x = v" << x << "\n";
-                   s.m_viable.display(verbose_stream(), x) << "\n";
                    verbose_stream() << "y = v" << y << "\n";
+                   s.m_viable.display(verbose_stream() << "\nx-intervals:\n", x, "\n") << "\n";
                    verbose_stream() << "\n";
                    verbose_stream() << "x_min " << x_min << " x_max " << x_max << "\n";
                    verbose_stream() << "v" << y << " " << y0 << "\n";
@@ -1855,6 +1863,7 @@ namespace polysat {
 
         if (x_sp1 > x_sp2)
             std::swap(x_sp1, x_sp2);
+        SASSERT(x_min <= x_sp1 && x_sp1 <= x_sp2 && x_sp2 <= x_max);
 
         IF_VERBOSE(2,
                    verbose_stream() << "Adjusted\n";

src/math/polysat/solver.cpp

@@ -158,8 +158,7 @@ namespace polysat {
         case l_false:
             // Input literal contradicts current boolean state (e.g., opposite literals in the input)
             // => conflict only flags the inconsistency
-            set_conflict_at_base_level();
+            set_conflict_at_base_level(dep);
-            SASSERT(dep == null_dependency && "track dependencies is TODO");
             return;
         case l_true:
             // constraint c is already asserted => ignore
@@ -174,8 +173,7 @@ namespace polysat {
         case l_false:
             // asserted an always-false constraint => conflict at base level
             LOG("Always false: " << c);
-            set_conflict_at_base_level();
+            set_conflict_at_base_level(dep);
-            SASSERT(dep == null_dependency && "track dependencies is TODO");
             return;
         case l_true:
             // asserted an always-true constraint => ignore
@@ -725,9 +723,7 @@ namespace polysat {
     /// Verify the value we're trying to assign against the univariate solver
     void solver::assign_verify(pvar v, rational val, justification j) {
         SASSERT(j.is_decision() || j.is_propagation());
-#ifndef NDEBUG
         unsigned const old_size = m_search.size();
-#endif
         signed_constraint c;
         clause_ref lemma;
         {
@@ -748,8 +744,8 @@ namespace polysat {
                 LOG("Produced lemma: " << show_deref(lemma));
             }
         }
-        SASSERT(m_search.size() == old_size);
+        VERIFY_EQ(m_search.size(), old_size);
-        SASSERT(!m_search.get_assignment().contains(v));
+        VERIFY(!m_search.get_assignment().contains(v));
         if (lemma) {
             add_clause(*lemma);
             if (is_conflict()) {
@@ -1178,7 +1174,18 @@ namespace polysat {
         LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
         for (sat::literal lit : clause) {
             LOG("   " << lit_pp(*this, lit));
-            // SASSERT(m_bvars.value(lit) != l_true);
+            if (!m_bvars.is_assigned(lit)) {
+                switch (lit2cnstr(lit).eval(*this)) {
+                case l_true:
+                    assign_eval(lit);
+                    break;
+                case l_false:
+                    assign_eval(~lit);
+                    break;
+                default:
+                    break;
+                }
+            }
             // it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint
             if (m_bvars.value(lit) == l_true) {
                 // in this case the clause is useless
@@ -1229,7 +1236,7 @@ namespace polysat {
     clause_ref solver::mk_clause(unsigned n, signed_constraint const* cs, bool is_redundant) {
         clause_builder cb(*this);
         for (unsigned i = 0; i < n; ++i)
-            cb.insert_try_eval(cs[i]);
+            cb.insert(cs[i]);
         cb.set_redundant(is_redundant);
         return cb.build();
     }
@@ -1320,14 +1327,9 @@ namespace polysat {
     }
 
     void solver::unsat_core(dependency_vector& deps) {
-        verbose_stream() << "WARNING: unsat_core requested but dependency tracking in polysat is TODO\n";
+        VERIFY(is_conflict());
         deps.reset();
-        LOG("conflict" << m_conflict);
+        m_conflict.find_deps(deps);
-        for (auto c : m_conflict) {
-            auto d = m_bvars.dep(c.blit());
-            if (d != null_dependency)
-                deps.push_back(d);
-        }
     }
 
     std::ostream& solver::display(std::ostream& out) const {

src/math/polysat/solver.h

@@ -253,7 +253,7 @@ namespace polysat {
         void erase_pwatch(pvar v, constraint* c);
         void erase_pwatch(constraint* c);
 
-        void set_conflict_at_base_level() { m_conflict.init_at_base_level(); }
+        void set_conflict_at_base_level(dependency dep) { m_conflict.init_at_base_level(dep); }
         void set_conflict(signed_constraint c) { m_conflict.init(c); }
         void set_conflict(clause& cl) { m_conflict.init(cl); }
         void set_conflict_by_viable_interval(pvar v) { m_conflict.init_by_viable_interval(v); }