add stubs for shr

src/math/polysat/CMakeLists.txt

@@ -15,6 +15,7 @@ z3_add_component(polysat
     saturation.cpp
     search_state.cpp
     simplify.cpp
+    shr_constraint.cpp
     solver.cpp
     ule_constraint.cpp
     viable.cpp

src/math/polysat/constraint.h

@@ -20,11 +20,12 @@ Author:
 
 namespace polysat {
 
-    enum ckind_t { ule_t, mul_ovfl_t };
+    enum ckind_t { ule_t, mul_ovfl_t, shr_t };
 
     class constraint;
     class ule_constraint;
     class mul_ovfl_constraint;
+    class shr_constraint;
     class signed_constraint;
 
     using constraint_hash = obj_ptr_hash<constraint>;
@@ -134,6 +135,7 @@ namespace polysat {
         friend class clause;
         friend class ule_constraint;
         friend class mul_ovfl_constraint;
+        friend class shr_constraint;
 
         // constraint_manager* m_manager;
         ckind_t             m_kind;

src/math/polysat/mul_ovfl_constraint.cpp

@@ -139,7 +139,7 @@ namespace polysat {
         cb.push_new(~premise);
         cb.push_new(conseq);
         clause_ref just = cb.build();
-        s.add_lemma(*just);
+        s.add_clause(*just);
         s.propagate();
         SASSERT(s.m_bvars.is_true(conseq.blit()));
         return true;

src/math/polysat/shr_constraint.cpp

@@ -0,0 +1,101 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat shift right constraint.
+
+Author:
+
+    Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
+
+--*/
+#pragma once
+#include "math/polysat/shr_constraint.h"
+#include "math/polysat/solver.h"
+
+namespace polysat {
+
+
+    shr_constraint::shr_constraint(constraint_manager& m, pdd const& p, pdd const& q, pdd const& r):
+        constraint(m, ckind_t::shr_t), m_p(p), m_q(q), m_r(r) {
+    }    
+
+    lbool shr_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const {
+        if (p.is_val() && r.is_val()) {
+            if (p.val() >= p.manager().power_of_2())
+                return r.is_zero() ? l_true : l_false;            
+            if (r.is_val()) {
+                // todo
+            }
+            // other cases when we know lower 
+            // bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant.
+        }
+        return l_undef;
+    }
+    
+    bool shr_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
+        switch (eval(p, q, r)) {
+        case l_true: return !is_positive;
+        case l_false: return is_positive;
+        default: return false;
+        }
+    }
+
+    bool shr_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
+        switch (eval(p, q, r)) {
+        case l_true: return is_positive;
+        case l_false: return !is_positive;
+        default: return false;
+        }
+    }
+    
+    std::ostream& shr_constraint::display(std::ostream& out, lbool status) const {
+        switch (status) {
+        case l_true: return display(out);
+        case l_false: return display(out << "~");
+        default: return display(out << "?");
+        }
+    }
+    std::ostream& shr_constraint::display(std::ostream& out) const {
+        return out << r() << " == " << p() << " << " << q();
+    }
+    bool shr_constraint::is_always_false(bool is_positive) const {
+        return is_always_false(is_positive, p(), q(), r());
+    }
+    bool shr_constraint::is_currently_false(assignment_t const& a, bool is_positive) const {
+        return is_always_false(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a));
+    }
+    bool shr_constraint::is_currently_true(assignment_t const& a, bool is_positive) const {
+        return is_always_true(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a));
+    }
+
+    /**
+    * Enforce basic axioms, such as:
+    * 
+    * r = p >> q & q >= k -> r[i] = 0 for i > K - k
+    * r = p >> q & q >= K -> r = 0
+    * r = p >> q & q = k -> r[i] = p[i+k] for k + i < K
+    * r = p >> q & q >= k -> r <= 2^K-k-1
+    * 
+    * Enforce also inferences and bounds
+    * 
+    * We can assume that shr_constraint is only asserted positive.
+    */
+    void shr_constraint::narrow(solver& s, bool is_positive) {
+        SASSERT(is_positive);
+        NOT_IMPLEMENTED_YET();
+    }
+
+    unsigned shr_constraint::hash() const {
+        return mk_mix(p().hash(), q().hash(), r().hash());
+    }
+
+    bool shr_constraint::operator==(constraint const& other) const {
+        if (other.kind() != ckind_t::shr_t)
+            return false;
+        auto const& o = dynamic_cast<shr_constraint const&>(other);
+        return p() == o.p() && q() == o.q() && r() == o.r();
+    }
+
+}

src/math/polysat/shr_constraint.h

@@ -0,0 +1,48 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat shift right constraint.
+
+Author:
+
+    Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
+
+--*/
+#pragma once
+#include "math/polysat/constraint.h"
+
+namespace polysat {
+
+    class shr_constraint final : public constraint {
+        friend class constraint_manager;
+
+        pdd m_p;
+        pdd m_q;
+        pdd m_r;
+
+        shr_constraint(constraint_manager& m, pdd const& p, pdd const& q, pdd const& r);
+        void simplify();
+        bool is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const;
+        bool is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const;
+        lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
+
+    public:
+        ~shr_constraint() override {}
+        pdd const& p() const { return m_p; }
+        pdd const& q() const { return m_q; }
+        pdd const& r() const { return m_r; }
+        std::ostream& display(std::ostream& out, lbool status) const override;
+        std::ostream& display(std::ostream& out) const override;
+        bool is_always_false(bool is_positive) const override;
+        bool is_currently_false(assignment_t const& a, bool is_positive) const override;
+        bool is_currently_true(assignment_t const& a, bool is_positive) const override;
+        void narrow(solver& s, bool is_positive) override;
+        inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
+        unsigned hash() const override;
+        bool operator==(constraint const& other) const override;
+        bool is_eq() const override { return false; }
+    };
+
+}

src/test/polysat.cpp

@@ -961,6 +961,24 @@ namespace polysat {
         s.expect_sat();
     }
 
+    static void test_quot_rem2(unsigned bw = 32) {
+        scoped_solver s(__func__);
+        s.set_max_conflicts(5);
+        auto q = s.var(s.add_var(bw));
+        auto r = s.var(s.add_var(bw));
+        auto idx = s.var(s.add_var(bw));
+        auto second = s.var(s.add_var(bw));
+        auto first = s.var(s.add_var(bw));
+        s.add_eq(q*idx + r, UINT_MAX);
+        s.add_ult(r, idx);
+        s.add_noovfl(q, idx);
+        s.add_ult(first, second);
+        s.add_diseq(idx, 0);
+        s.add_ule(second - first, q);
+        s.add_noovfl(second  - first, idx);
+        s.check();       
+    }
+
 
     // Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
     // NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
@@ -1011,9 +1029,10 @@ namespace polysat {
             auto pa = to_pdd(m, s, expr2pdd, a);
             auto pb = to_pdd(m, s, expr2pdd, b);            
             s.add_eq(quot*pb + rem - pa);
-            s.add_ult(rem, pb);
-            // TODO:
-            // s.add_mul_noovfl(quot, pb);
+            s.add_ult(rem, pb);            
+            s.add_noovfl(quot, pb);
+            // todo: add clause or use external iteration?
+            // s.add_clause(s.ult(rem, pb), s.eq(b));
             r = alloc(pdd, quot);
         }
         else if (bv.is_numeral(e, n, sz))