Dedup op constraints

src/math/polysat/constraint.h

@@ -31,6 +31,9 @@ namespace polysat {
     class op_constraint;
     class signed_constraint;
 
+    using constraints = ptr_vector<constraint>;
+    using signed_constraints = vector<signed_constraint>;
+
     /// Normalized inequality:
     ///     lhs <= rhs, if !is_strict
     ///     lhs < rhs, otherwise
@@ -44,7 +47,6 @@ namespace polysat {
         signed_constraint as_signed_constraint() const;
     };
 
-
     class constraint {
         friend class constraint_manager;
         friend class signed_constraint;
@@ -126,7 +128,6 @@ namespace polysat {
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
 
-
     class signed_constraint final {
     public:
         using ptr_t = constraint*;

src/math/polysat/constraint_manager.cpp

@@ -24,13 +24,6 @@ Author:
 
 namespace polysat {
 
-    // class constraint_dedup {
-    // public:
-    //     using op_constraint_args_eq = default_eq<op_constraint_args>;
-    //     using op_constraint_args_hash = obj_hash<op_constraint_args>;
-    //     map<op_constraint_args, pvar, op_constraint_args_hash, op_constraint_args_eq> op_constraint_vars;
-    // };
-
     constraint_manager::constraint_manager(solver& s): s(s) {}
 
     void constraint_manager::assign_bv2c(sat::bool_var bv, constraint* c) {
@@ -155,14 +148,14 @@ namespace polysat {
     /** Look up constraint among stored constraints. */
     constraint* constraint_manager::dedup(constraint* c1) {
         constraint* c2 = nullptr;
-        if (m_constraint_table.find(c1, c2)) {
+        if (m_dedup.constraints.find(c1, c2)) {
             dealloc(c1);
             return c2;
         }
         else {
             SASSERT(!c1->has_bvar());
             ensure_bvar(c1);
-            m_constraint_table.insert(c1);
+            m_dedup.constraints.insert(c1);
             store(c1);
             return c1;
         }
@@ -289,10 +282,14 @@ namespace polysat {
     }
 
     pdd constraint_manager::band(pdd const& p, pdd const& q) {
+        op_constraint_args const args(op_constraint::code::and_op, p, q);
         auto& m = p.manager();
+        auto it = m_dedup.op_constraint_expr.find_iterator(args);
+        if (it != m_dedup.op_constraint_expr.end())
+            return m.mk_var(it->m_value);
         unsigned sz = m.power_of_2();
-        // TODO: return existing r if we call again with the same arguments
         pdd r = m.mk_var(s.add_var(sz));
+        m_dedup.op_constraint_expr.insert(args, r.var());
         s.assign_eh(band(p, q, r), null_dependency);
         return r;
     }

src/math/polysat/constraint_manager.h

@@ -12,25 +12,24 @@ Author:
 
 --*/
 #pragma once
-#include "math/polysat/constraint.h"
 #include "math/polysat/clause.h"
-#include <iostream>
+#include "math/polysat/constraint.h"
+#include "math/polysat/op_constraint.h"
 
 namespace polysat {
 
-    class constraint;
-    class ule_constraint;
-    class umul_ovfl_constraint;
-    class smul_fl_constraint;
-    class op_constraint;
-    class signed_constraint;
+    class constraint_dedup {
+    public:
+        using constraint_hash = obj_ptr_hash<constraint>;
+        using constraint_eq = deref_eq<constraint>;
+        using constraint_table = ptr_hashtable<constraint, constraint_hash, constraint_eq>;
+        constraint_table constraints;
 
-    using constraint_hash = obj_ptr_hash<constraint>;
-    using constraint_eq = deref_eq<constraint>;
-    using constraint_table = ptr_hashtable<constraint, constraint_hash, constraint_eq>;
-
-    using constraints = ptr_vector<constraint>;
-    using signed_constraints = vector<signed_constraint>;
+        using op_constraint_args_eq = default_eq<op_constraint_args>;
+        using op_constraint_args_hash = obj_hash<op_constraint_args>;
+        using op_constraint_expr_map = map<op_constraint_args, pvar, op_constraint_args_hash, op_constraint_args_eq>;
+        op_constraint_expr_map op_constraint_expr;
+    };
 
     // Manage constraint lifetime, deduplication, and connection to boolean variables/literals.
     class constraint_manager {
@@ -40,11 +39,10 @@ namespace polysat {
 
         // Constraints indexed by their boolean variable
         ptr_vector<constraint> m_bv2constraint;
-        // Constraints that have a boolean variable, for deduplication
-        constraint_table m_constraint_table;
+
         scoped_ptr_vector<constraint> m_constraints;
 
-        // scoped_ptr<constraint_dedup> m_dedup;
+        constraint_dedup m_dedup;
 
         // Clause storage per level
         vector<vector<clause_ref>> m_clauses;

src/math/polysat/op_constraint.cpp

@@ -75,7 +75,11 @@ namespace polysat {
     }
 
     bool op_constraint::is_currently_false(solver& s, bool is_positive) const {
-        return is_always_false(is_positive, s.subst(p()), s.subst(q()), s.subst(r()));        
+        return is_always_false(is_positive, s.subst(p()), s.subst(q()), s.subst(r()));
+    }
+
+    bool op_constraint::is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const {
+        return is_always_false(is_positive, s.subst(sub, p()), s.subst(sub, q()), s.subst(sub, r()));
     }
 
     std::ostream& op_constraint::display(std::ostream& out, lbool status) const {
@@ -189,7 +193,7 @@ namespace polysat {
             // q = 0 -> p = r
             s.add_clause(~lshr, ~s.eq(q()), s.eq(p(), r()), true);
         else if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && !pv.is_zero() && pv.val() <= rv.val())
-            // q != 0 & p > 0 => r < p 
+            // q != 0 & p > 0 => r < p
             s.add_clause(~lshr, s.eq(q()), s.ule(p(), 0), s.ult(r(), p()), true);
         else if (qv.is_val() && !qv.is_zero() && qv.val() < K && rv.is_val() &&
             rv.val() > rational::power_of_two(K - qv.val().get_unsigned() - 1))
@@ -197,7 +201,7 @@ namespace polysat {
             s.add_clause(~lshr, ~s.ule(qv.val(), q()), s.ule(r(), rational::power_of_two(K - qv.val().get_unsigned() - 1)), true);
         else if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero())
             // q >= K -> r = 0
-            s.add_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true);            
+            s.add_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true);
         // q = k -> r[i - k] = p[i] for K - k <= i < K
         else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) {
             unsigned k = qv.val().get_unsigned();
@@ -222,11 +226,11 @@ namespace polysat {
 
         if (p.is_val() && q.is_val() && r.is_val())
             return r == p * m.mk_val(rational::power_of_two(q.val().get_unsigned())) ? l_true : l_false;
-            
+
         if (q.is_val() && q.val() >= m.power_of_2() && r.is_val())
             return r.is_zero() ? l_true : l_false;
-                
-        // other cases when we know lower 
+
+        // other cases when we know lower
         // bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant.
         return l_undef;
     }
@@ -239,7 +243,7 @@ namespace polysat {
     * p = 0 => r = 0
     * q = 0 => r = 0
     * p[i] && q[i] = r[i]
-    * 
+    *
     * Possible other:
     * p = max_value => q = r
     * q = max_value => p = r
@@ -248,7 +252,7 @@ namespace polysat {
         auto pv = s.subst(p());
         auto qv = s.subst(q());
         auto rv = s.subst(r());
-        
+
         signed_constraint andc(this, true);
         if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
             s.add_clause(~andc, s.ule(r(), p()), true);

src/math/polysat/op_constraint.h

@@ -12,7 +12,7 @@ Module Name:
     or:   r == p | q
     not:  r == ~p
     xor:  r == p ^ q
-    
+
 Author:
 
     Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
@@ -20,6 +20,7 @@ Author:
 --*/
 #pragma once
 #include "math/polysat/constraint.h"
+#include <optional>
 
 namespace polysat {
 
@@ -48,7 +49,7 @@ namespace polysat {
         void narrow_and(solver& s);
         static lbool eval_and(pdd const& p, pdd const& q, pdd const& r);
 
-    public:        
+    public:
         ~op_constraint() override {}
         pdd const& p() const { return m_p; }
         pdd const& q() const { return m_q; }
@@ -57,7 +58,7 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override;
         bool is_always_false(bool is_positive) const override;
         bool is_currently_false(solver& s, bool is_positive) const override;
-        bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
+        bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override;
         void narrow(solver& s, bool is_positive, bool first) override;
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;
@@ -67,4 +68,24 @@ namespace polysat {
         void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
     };
 
+    struct op_constraint_args {
+        op_constraint::code op;
+        // NOTE: this is only optional because table2map requires a default constructor
+        std::optional<std::pair<pdd, pdd>> args;
+
+        op_constraint_args() = default;
+        op_constraint_args(op_constraint::code op, pdd lhs, pdd rhs)
+            : op(op), args({std::move(lhs), std::move(rhs)}) {}
+
+        bool operator==(op_constraint_args const& other) const {
+            return op == other.op && args == other.args;
+        }
+
+        unsigned hash() const {
+            unsigned const lhs_hash = args ? args->first.hash() : 0;
+            unsigned const rhs_hash = args ? args->second.hash() : 0;
+            return mk_mix(static_cast<unsigned>(op), lhs_hash, rhs_hash);
+        }
+    };
+
 }