add ovfl constraint

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

src/math/polysat/CMakeLists.txt

@@ -10,6 +10,7 @@ z3_add_component(polysat
     justification.cpp
     linear_solver.cpp
     log.cpp
+    mul_ovfl_constraint.cpp
     saturation.cpp
     search_state.cpp
     solver.cpp

src/math/polysat/constraint.cpp

@@ -18,6 +18,7 @@ Author:
 #include "math/polysat/log.h"
 #include "math/polysat/log_helper.h"
 #include "math/polysat/ule_constraint.h"
+#include "math/polysat/mul_ovfl_constraint.h"
 
 namespace polysat {
 
@@ -241,6 +242,14 @@ namespace polysat {
         return *dynamic_cast<ule_constraint const*>(this);
     }
 
+    mul_ovfl_constraint& constraint::to_mul_ovfl() {
+        return *dynamic_cast<mul_ovfl_constraint*>(this);
+    }
+
+    mul_ovfl_constraint const& constraint::to_mul_ovfl() const {
+        return *dynamic_cast<mul_ovfl_constraint const*>(this);
+    }
+
     std::string constraint::bvar2string() const {
         std::stringstream out;
         out << " (b";

src/math/polysat/constraint.h

@@ -20,10 +20,11 @@ Author:
 
 namespace polysat {
 
-    enum ckind_t { ule_t };
+    enum ckind_t { ule_t, mul_ovfl_t };
 
     class constraint;
     class ule_constraint;
+    class mul_ovfl_constraint;
     class signed_constraint;
 
     using constraint_hash = obj_ptr_hash<constraint>;
@@ -130,6 +131,7 @@ namespace polysat {
         friend class constraint_manager;
         friend class clause;
         friend class ule_constraint;
+        friend class mul_ovfl_constraint;
 
         // constraint_manager* m_manager;
         ckind_t             m_kind;
@@ -156,6 +158,7 @@ namespace polysat {
 
         virtual bool is_eq() const { return false; }
         bool is_ule() const { return m_kind == ckind_t::ule_t; }
+        bool is_mul_ovfl() const { return m_kind == ckind_t::mul_ovfl_t; }
         ckind_t kind() const { return m_kind; }
         virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
         virtual std::ostream& display(std::ostream& out) const = 0;
@@ -170,6 +173,8 @@ namespace polysat {
 
         ule_constraint& to_ule();
         ule_constraint const& to_ule() const;
+        mul_ovfl_constraint& to_mul_ovfl();
+        mul_ovfl_constraint const& to_mul_ovfl() const;
         unsigned_vector& vars() { return m_vars; }
         unsigned_vector const& vars() const { return m_vars; }
         unsigned var(unsigned idx) const { return m_vars[idx]; }

src/math/polysat/mul_ovfl_constraint.cpp

@@ -0,0 +1,95 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat multiplication overflow constraint
+
+Author:
+
+    Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
+
+--*/
+#pragma once
+#include "math/polysat/mul_ovfl_constraint.h"
+
+namespace polysat {
+
+
+    mul_ovfl_constraint::mul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q):
+        constraint(m, ckind_t::mul_ovfl_t), m_p(p), m_q(q) {
+
+        simplify();
+        m_vars.append(m_p.free_vars());
+        for (auto v : m_q.free_vars())
+            if (!m_vars.contains(v))
+                m_vars.push_back(v);
+
+    }
+    void mul_ovfl_constraint::simplify() {
+        if (m_p.is_zero() || m_q.is_zero() ||
+            m_p.is_one() || m_q.is_one()) {
+            m_q = 0;
+            m_p = 0;
+            return;
+        }
+    }
+
+    std::ostream& mul_ovfl_constraint::display(std::ostream& out, lbool status) const {
+        switch (status) {
+        case l_true: return display(out);
+        case l_false: return display(out << "~");
+        case l_undef: return display(out << "?");
+        }       
+    }
+
+    std::ostream& mul_ovfl_constraint::display(std::ostream& out) const {
+        return "ovfl*(" << m_p << ", " << m_q << ")";       
+    }
+
+
+    bool mul_ovfl_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q) const {
+        if (!is_positive && (p.is_zero() || q.is_zero() ||
+            p.is_one() || q.is_one()))
+            return true;
+        if (p.is_val() && q.is_val()) {
+            bool ovfl = p.val() * q.val() > p().manager().max_value();
+            return is_positive == ovfl;
+        }
+        return false;
+    }
+
+    bool mul_ovfl_constraint::is_always_false(bool is_positive) const {
+        return is_always_false(is_positive, m_p, m_q);
+    }
+
+    bool mul_ovfl_constraint::is_currently_false(assignment_t const& a, bool is_positive) const {
+        auto p = p().subst_val(s.assignment());
+        auto q = q().subst_val(s.assignment());
+        return is_always_false(is_positive, p, q);
+    }
+
+    bool mul_ovfl_constraint::is_currently_true(assignment_t const& a, bool is_positive) const {
+        return !is_currently_false(a, !is_positive);
+    }
+
+    void mul_ovfl_constraint::narrow(solver& s, bool is_positive) {    
+        auto p = p().subst_val(s.assignment());
+        auto q = q().subst_val(s.assignment());
+
+        if (is_always_false(is_positive, p, q)) {
+            s.set_conflict({ this, is_positive });
+            return;
+        }
+
+        NOT_IMPLEMENTED_YET();
+    }
+
+    unsigned mul_ovfl_constraint::hash() const {
+    	return mk_mix(p().hash(), q().hash(), 25);
+    }
+
+    bool mul_ovfl_constraint::operator==(constraint const& other) const {
+        return other.is_mul_ovfl() && p() == other.to_mul_ovfl().p() && q() == other.to_mul_ovfl().q();
+    }
+}

src/math/polysat/mul_ovfl_constraint.h

@@ -0,0 +1,44 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat multiplication overflow constraint
+
+Author:
+
+    Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
+
+--*/
+#pragma once
+#include "math/polysat/constraint.h"
+
+namespace polysat {
+
+    class mul_ovfl_constraint final : public constraint {
+        friend class constraint_manager;
+
+        pdd m_p;
+        pdd m_q;
+
+        mul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q);
+        void simplify();
+        bool is_always_false(bool is_positive, pdd const& p, pdd const& q) const;
+
+    public:
+        ~mul_ovfl_constraint() override {}
+        pdd const& p() const { return m_p; }
+        pdd const& q() const { return m_q; }
+        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; }
+    };
+
+}