sketch bit-constraints

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

src/math/polysat/bit_constraint.cpp

@@ -0,0 +1,57 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat bit_constraint
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+
+#include "math/polysat/bit_constraint.h"
+
+namespace polysat {
+
+    std::ostream& bit_constraint::display(std::ostream& out) const {
+            if (!m_value)
+                out << "~";
+            out << "v" << m_var << "[" << m_index << "] ";
+        }
+        return out;
+    }
+
+    bool bit_constraint::propagate(solver& s, pvar v) {       
+        UNREACHABLE();
+        return false;
+    }
+
+    constraint* bit_constraint::resolve(solver& s, pvar v) {
+        UNREACHABLE();
+        return nullptr;
+    }
+
+    bool bit_constraint::is_always_false() {
+        return false;
+    }
+
+    bool bit_constraint::is_currently_false(solver& s) {
+        return false;
+    }
+
+    void bit_constraint::narrow(solver& s) {
+        bdd viable = s.m_bdd.mk_true();
+        if (m_value)
+            viable &= s.m_bdd.mk_var(m_index);
+        else 
+            viable &= s.m_bdd.mk_nvar(m_index);
+        s.push_viable(v);
+        s.m_viable[v] &= viable;
+        if (s.m_viable[v].is_false()) 
+            s.set_conflict(v);
+    }
+
+}

src/math/polysat/bit_constraint.h

@@ -0,0 +1,49 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat bit_constraint
+
+Abstract:
+
+    Bit constraints fix a subrange of bits
+    
+    The first version assumes the requirement is to fix bit positions 
+    to specific values. This is insufficient to encode that x != 0.
+    A more general approach is required since bit constraints should
+    be able to also let us reduce inequality reasoning to having slack
+    variables.
+
+    The main way bit-constraints interact with the solver is to 
+    narrow m_viable during initialization. 
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+#pragma once
+#include "math/polysat/constraint.h"
+
+
+namespace polysat {
+
+    class bit_constraint : public constraint {
+        pvar        m_var;
+        unsigned    m_index;
+        bool        m_value;
+    public:
+        bit_constraint(unsigned lvl, pvar v, unsigned i, bool val, p_dependency_ref& dep):
+            constraint(lvl, dep, ckind_t::bit_t), m_var(v), m_index(i), m_value(val) {
+        }
+        ~bit_constraint() override {}
+        std::ostream& display(std::ostream& out) const override;
+        bool propagate(solver& s, pvar v) override;
+        constraint* resolve(solver& s, pvar v) override;
+        void narrow(solver& s) override;
+        bool is_always_false() override;
+        bool is_currently_false(solver& s) override;
+    };
+}

src/math/polysat/constraint.cpp

@@ -15,6 +15,8 @@ Author:
 #include "math/polysat/constraint.h"
 #include "math/polysat/solver.h"
 #include "math/polysat/log.h"
+#include "math/polysat/bit_constraint.h"
+#include "math/polysat/eq_constraint.h"
 
 namespace polysat {
 

src/math/polysat/constraint.h

@@ -12,20 +12,22 @@ Abstract:
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
 
 --*/
 #pragma once
 #include "math/polysat/types.h"
 
-
 namespace polysat {
 
-    enum ckind_t { eq_t, ule_t, sle_t };
+    enum ckind_t { eq_t, ule_t, sle_t, bit_t };
 
     class eq_constraint;
+    class bit_constraint;
     class ule_constraint;
 
     class constraint {
+        friend class bit_constraint;
         friend class eq_constraint;
         friend class ule_constraint;
         unsigned         m_level;
@@ -46,6 +48,7 @@ namespace polysat {
         virtual constraint* resolve(solver& s, pvar v) = 0;
         virtual bool is_always_false() = 0;
         virtual bool is_currently_false(solver& s) = 0;
+        virtual void narrow(solver& s) = 0;
         eq_constraint& to_eq();
         eq_constraint const& to_eq() const;
         p_dependency* dep() const { return m_dep; }
@@ -53,22 +56,6 @@ namespace polysat {
         unsigned level() const { return m_level; }
     };
 
-    class eq_constraint : public constraint {
-        pdd m_poly;
-    public:
-        eq_constraint(unsigned lvl, pdd const& p, p_dependency_ref& dep):
-            constraint(lvl, dep, ckind_t::eq_t), m_poly(p) {
-            m_vars.append(p.free_vars());
-        }
-        ~eq_constraint() override {}
-        pdd const & p() const { return m_poly; }
-        std::ostream& display(std::ostream& out) const override;
-        bool propagate(solver& s, pvar v) override;
-        constraint* resolve(solver& s, pvar v) override;
-        bool is_always_false() override;
-        bool is_currently_false(solver& s) override;
-    };
-
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
         
 

src/math/polysat/eq_constraint.cpp

@@ -25,7 +25,6 @@ namespace polysat {
     bool eq_constraint::propagate(solver& s, pvar v) {
         LOG_H3("Propagate " << s.m_vars[v] << " in " << *this);
         SASSERT(!vars().empty());
-        auto var = s.m_vars[v].var();
         unsigned idx = 0;
         if (vars()[idx] != v)
             idx = 1;
@@ -47,8 +46,6 @@ namespace polysat {
             return false;
         if (q.is_never_zero()) {
             LOG("Conflict (never zero under current assignment)");
-            // we could tag constraint to allow early substitution before 
-            // swapping watch variable in case we can detect conflict earlier.
             s.set_conflict(*this);
             return false;
         }
@@ -134,13 +131,18 @@ namespace polysat {
             if (!a.resolve(v, b, r)) 
                 return nullptr;
             p_dependency_ref d(s.m_dm.mk_join(c->dep(), dep()), s.m_dm);
-            // d = ;
             unsigned lvl = std::max(c->level(), level());
             return constraint::eq(lvl, r, d);             
         }
         return nullptr;
     }
 
+    void eq_constraint::narrow(solver& s) {
+        if (!p().is_linear())
+            return;
+        // TODO apply affine constraints and other that can be extracted cheaply
+    }
+
     bool eq_constraint::is_always_false() {
         return p().is_never_zero();
     }

src/math/polysat/eq_constraint.h

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat constraints
+
+Abstract:
+
+    Polynomial equality constriants
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+
+--*/
+#pragma once
+#include "math/polysat/constraint.h"
+
+
+namespace polysat {
+
+    class eq_constraint : public constraint {
+        pdd m_poly;
+    public:
+        eq_constraint(unsigned lvl, pdd const& p, p_dependency_ref& dep):
+            constraint(lvl, dep, ckind_t::eq_t), m_poly(p) {
+            m_vars.append(p.free_vars());
+        }
+        ~eq_constraint() override {}
+        pdd const & p() const { return m_poly; }
+        std::ostream& display(std::ostream& out) const override;
+        bool propagate(solver& s, pvar v) override;
+        constraint* resolve(solver& s, pvar v) override;
+        bool is_always_false() override;
+        bool is_currently_false(solver& s) override;
+        void narrow(solver& s) override;
+    };
+
+}

src/math/polysat/solver.cpp

@@ -154,6 +154,7 @@ namespace polysat {
         LOG("Adding constraint: " << *c);
         m_constraints.push_back(c);
         add_watch(*c);
+        c->narrow(*this);
     }
 
     void solver::add_diseq(pdd const& p, unsigned dep) {

src/math/polysat/solver.h

@@ -19,6 +19,8 @@ Author:
 
 #include "util/statistics.h"
 #include "math/polysat/constraint.h"
+#include "math/polysat/eq_constraint.h"
+#include "math/polysat/bit_constraint.h"
 #include "math/polysat/justification.h"
 #include "math/polysat/trail.h"