update to saturation

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

src/sat/smt/polysat/core.h

@@ -155,7 +155,7 @@ namespace polysat {
         dependency get_dependency(constraint_id idx) const;
         dependency_vector get_dependencies(constraint_id_vector const& ids) const;
         lbool eval(constraint_id id);
-        bool propagate(signed_constraint const& sc, constraint_id_vector const& ids) { return s.propagate(sc, ids); }
+        dependency propagate(signed_constraint const& sc, constraint_id_vector const& ids) { return s.propagate(sc, ids); }
         lbool eval(signed_constraint const& sc);
         constraint_id_vector explain_eval(signed_constraint const& sc);
 

src/sat/smt/polysat/saturation.cpp

@@ -38,11 +38,13 @@ namespace polysat {
         if (c.eval(id) == l_true)
             return false;
         auto sc = c.get_constraint(id);
+        if (!sc.vars().contains(v))
+            return false;
         m_propagated = false;
         if (sc.is_ule())
             propagate(v, inequality::from_ule(c, id));
-        else
+        else if (sc.is_umul_ovfl())
-            ;
+            try_umul_ovfl(v, umul_ovfl(id, sc));
 
         return m_propagated;
     }
@@ -51,33 +53,35 @@ namespace polysat {
         if (c.size(v) != i.lhs().power_of_2())
             return;
         propagate_infer_equality(v, i);
-        try_ugt_x(v, i);
+        try_ugt_x(v, i);       
-        return;
+        try_ugt_y(v, i);
-
+        try_ugt_z(v, i);    
     }
 
     void saturation::propagate(signed_constraint const& sc, std::initializer_list<constraint_id> const& premises) {
-        if (c.propagate(sc, constraint_id_vector(premises)))
+        c.propagate(sc, constraint_id_vector(premises));        
-            m_propagated = true;
     }
 
     void saturation::add_clause(char const* name, clause const& cs, bool is_redundant) { 
-        vector<std::variant<constraint_id, dependency>> core;
+        vector<constraint_or_dependency> lemma;
         for (auto const& e : cs) {
             if (std::holds_alternative<constraint_id>(e)) {
-                core.push_back(*std::get_if<constraint_id>(&e));
+                auto id = *std::get_if<constraint_id>(&e);
-                continue;
+                auto d = c.get_dependency(id);
+                lemma.push_back(~d);
             }
-            auto sc = *std::get_if<signed_constraint>(&e);
+            else if (std::holds_alternative<signed_constraint>(e)) {
-            if (c.eval(sc) != l_false)
+                auto sc = *std::get_if<signed_constraint>(&e);
-                return;            
+                if (c.eval(sc) != l_false)
-            c.propagate(~sc, c.explain_eval(sc));
+                    return;
-            // retrieve dep/id from propagated ~sc
+                auto d = c.propagate(~sc, c.explain_eval(sc));
-            // add to id to ids or ~dep to deps
+                lemma.push_back(~d);
-        }
+            }
-        // TODO
+            else
-        //
+                UNREACHABLE();
-        // c.add_axiom(name, core_vector(core.begin(), core.end()), is_redundant);
+        }        
+        c.add_axiom(name, core_vector(lemma.begin(), lemma.end()), is_redundant);
+        m_propagated = true;
     }
 
     bool saturation::match_core(std::function<bool(signed_constraint const& sc)> const& p, constraint_id& id_out) {
@@ -164,7 +168,7 @@ namespace polysat {
         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, j, C.umul_ovfl(x, y), ineq(is_strict, z_prime * x, z * x) }, false);
+        add_clause("[y] z' <= y & yx <= zx", { i.id(), j.id(), C.umul_ovfl(x, y), ineq(is_strict, z_prime * x, z * x)}, false);
     }
 
     /**
@@ -187,7 +191,7 @@ 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, j, c.umul_ovfl(x, y_prime), ineq(is_strict, y * x, y_prime * x) }, false);
+        add_clause("[z] z <= y' && yx <= zx", { i.id(), j.id(), c.umul_ovfl(x, y_prime), ineq(is_strict, y * x, y_prime * x)}, false);
     }
 
 
@@ -204,6 +208,37 @@ namespace polysat {
         return is_non_overflow(x, y) && (sc = c.umul_ovfl(x, y), 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();
+        constraint_id id;
+        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;
+        };
+        auto extract_mul_args = [&](auto const& sc2) -> std::pair<pdd, pdd> {
+            auto p2 = sc2.to_umul_ovfl().p(), q2 = sc2.to_umul_ovfl().q();
+            if (p == p2)
+                return { q, q2 };
+            else if (p == q2)
+                return { q, p2 };
+            else if (q == p2)
+                return { p, q2 };
+            else
+                return { p, p2 };
+        };
+        if (match_constraints([&](auto const& sc2) { return sc2.is_umul_ovfl() && sc.sign() != sc2.sign() && match_mul_arg(sc2); }, id)) {
+            auto sc2 = c.get_constraint(id);
+            auto [q1, q2] = extract_mul_args(sc2);
+            if (sc.sign())
+                add_clause("[y] ~ovfl(p, q1) & ovfl(p, q2) ==> q1 < q2", { sc.id(), id, C.ult(q1, q2) }, false);
+            else 
+                add_clause("[y] ovfl(p, q1) & ~ovfl(p, q2) ==> q1 > q2", { sc.id(), id, C.ult(q2, q1)}, false);
+        }         
+    }
+
 #if 0
 
 
@@ -281,55 +316,6 @@ namespace polysat {
         return false;
     }
 
-    bool saturation::try_umul_ovfl(pvar v, signed_constraint c, conflict& core) {
-        SASSERT(c->is_umul_ovfl());
-        bool prop = false;
-        if (try_umul_ovfl_noovfl(v, c, core))
-            prop = true;
-#if 0
-        if (c.is_positive()) {
-            prop = try_umul_ovfl_bounds(v, c, core);
-        }
-        else {
-            prop = try_umul_noovfl_bounds(v, c, core);
-            if (false && try_umul_noovfl_lo(v, c, core))
-                prop = true;
-        }
-#endif
-        return prop;
-    }
-
-    // Ovfl(x, y) & ~Ovfl(y, z) ==> x > z
-    // TODO: Ovfl(x, y1) & ~Ovfl(y2, z) & y1 <= y2 ==> x > z
-    bool saturation::try_umul_ovfl_noovfl(pvar v, signed_constraint c1, conflict& core) {
-        set_rule("[y] ovfl(x, y) & ~ovfl(y, z) ==> x > z");
-        SASSERT(c1->is_umul_ovfl());
-        if (!c1.is_positive())  // since we search for both premises in the core, break symmetry by requiring c1 to be positive
-            return false;
-        pdd p = c1->to_umul_ovfl().p();
-        pdd q = c1->to_umul_ovfl().q();
-        for (auto c2 : core) {
-            if (!c2.is_negative())
-                continue;
-            if (!c2->is_umul_ovfl())
-                continue;
-            pdd r = c2->to_umul_ovfl().p();
-            pdd u = c2->to_umul_ovfl().q();
-            if (p == u || q == u)
-                swap(r, u);
-            if (q == r || q == u)
-                swap(p, q);
-            if (p != r)
-                continue;
-            m_lemma.reset();
-            m_lemma.insert(~c1);
-            m_lemma.insert(~c2);
-            if (propagate(v, core, s.ult(u, q)))
-                return true;
-        }
-        return false;
-    }
-
     bool saturation::try_umul_noovfl_lo(pvar v, signed_constraint c, conflict& core) {
         set_rule("[x] ~ovfl(x, y) => y = 0 or x <= x * y");
         SASSERT(c->is_umul_ovfl());

src/sat/smt/polysat/saturation.h

@@ -18,12 +18,14 @@ Author:
 
 namespace polysat {
 
+    class umul_ovfl;
+
     /**
      * Introduce lemmas that derive new (simpler) constraints from the current conflict and partial model.
      */
     class saturation {
 
-        using clause = std::initializer_list<std::variant<constraint_id, signed_constraint>>;
+        using clause = std::initializer_list<constraint_id_or_constraint>;
         core& c;
         constraints& C;
         char const* m_rule = nullptr;
@@ -43,9 +45,11 @@ namespace polysat {
 
 
         void propagate_infer_equality(pvar x, inequality const& a_l_b);
+        void propagate_umul_ovfl(pvar v, umul_ovfl const& sc);
         void try_ugt_x(pvar v, inequality const& i);
         void try_ugt_y(pvar v, inequality const& i);
         void try_ugt_z(pvar z, inequality const& i);
+        void try_umul_ovfl(pvar v, umul_ovfl const& sc);
 
         signed_constraint ineq(bool is_strict, pdd const& x, pdd const& y);
         

src/sat/smt/polysat/types.h

@@ -81,10 +81,13 @@ namespace polysat {
     struct justified_fixed_bits : public fixed_bits, public dependency {};
 
     using dependency_vector = vector<dependency>;
+    using constraint_or_dependency = std::variant<signed_constraint, dependency>;
+    using constraint_id_or_constraint = std::variant<constraint_id, signed_constraint>;
+    using constraint_id_or_dependency = std::variant<constraint_id, dependency>;
 
-    using core_vector = std::initializer_list<std::variant<signed_constraint, dependency>>;
+    using core_vector = std::initializer_list<constraint_or_dependency>;
     using constraint_id_vector = svector<constraint_id>;
-    using constraint_ids = std::initializer_list<constraint_id>;
+    using constraint_id_list = std::initializer_list<constraint_id>;
 
 
     //
@@ -97,7 +100,7 @@ namespace polysat {
         virtual void add_eq_literal(pvar v, rational const& val) = 0;
         virtual bool add_axiom(char const* name, core_vector const& core, bool redundant) = 0;
         virtual void set_conflict(constraint_id_vector const& core) = 0;
-        virtual bool propagate(signed_constraint sc, constraint_id_vector const& deps) = 0;
+        virtual dependency propagate(signed_constraint sc, constraint_id_vector const& deps) = 0;
         virtual void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) = 0;
         virtual trail_stack& trail() = 0;
         virtual bool inconsistent() const = 0;

src/sat/smt/polysat/umul_ovfl_constraint.h

@@ -40,4 +40,16 @@ namespace polysat {
         void propagate(core& c, lbool value, dependency const& dep) override;
     };
 
+
+    class umul_ovfl {
+        constraint_id m_id;
+        signed_constraint sc;
+    public:
+        umul_ovfl(constraint_id id, signed_constraint sc) : m_id(id), sc(sc) {}
+        pdd p() const { return sc.to_umul_ovfl().p(); }
+        pdd q() const { return sc.to_umul_ovfl().q(); }
+        bool sign() const { return sc.sign(); }
+        constraint_id id() const { return m_id; }
+    };
+
 }

src/sat/smt/polysat_solver.cpp

@@ -208,15 +208,21 @@ namespace polysat {
     // Core uses the propagate callback to add unit propagations to the trail.
     // The polysat::solver takes care of translating signed constraints into expressions, which translate into literals.
     // Everything goes over expressions/literals. polysat::core is not responsible for replaying expressions. 
-    bool solver::propagate(signed_constraint sc, constraint_id_vector const& cs) {
+    
-        sat::literal lit = ctx.mk_literal(constraint2expr(sc));
+    dependency solver::propagate(signed_constraint sc, constraint_id_vector const& cs) {
+        sat::literal lit = ctx.mk_literal(constraint2expr(sc));        
         if (s().value(lit) == l_true)
-            return false;
+            return dependency(lit, s().lvl(lit));
         auto deps = m_core.get_dependencies(cs);
         auto [core, eqs] = explain_deps(deps);
         auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr);
+        unsigned level = 0;
+        for (auto c : core)
+            level = std::max(level, s().lvl(c));
+        if (!eqs.empty()) // over-approximate propagation level if it uses equalities.
+            level = level = s().scope_lvl();
         ctx.propagate(lit, ex);
-        return true;
+        return dependency(lit, level); 
     }
 
     void solver::propagate(dependency const& d, bool sign, constraint_id_vector const& cs) {

src/sat/smt/polysat_solver.h

@@ -162,7 +162,7 @@ namespace polysat {
         void add_eq_literal(pvar v, rational const& val) override;
         void set_conflict(constraint_id_vector const& core) override;
         bool add_axiom(char const* name, core_vector const& core, bool redundant) override;
-        bool propagate(signed_constraint sc, constraint_id_vector const& deps) override;
+        dependency propagate(signed_constraint sc, constraint_id_vector const& deps) override;
         void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) override;
         trail_stack& trail() override;
         bool inconsistent() const override;