add outline for ule constraints, change bit to var constraints

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

src/math/polysat/CMakeLists.txt

@@ -2,7 +2,8 @@ z3_add_component(polysat
   SOURCES
     constraint.cpp
     eq_constraint.cpp
-    bit_constraint.cpp
+    ule_constraint.cpp
+    var_constraint.cpp
     justification.cpp
     log.cpp
     solver.cpp

src/math/polysat/bit_constraint.cpp

@@ -1,49 +0,0 @@
-/*++
-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"
-#include "math/polysat/solver.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 s.m_viable[m_var].is_false();
-    }
-
-    void bit_constraint::narrow(solver& s) {
-        s.intersect_viable(m_var, m_value ? s.m_bdd.mk_var(m_index) : s.m_bdd.mk_nvar(m_index));
-    }
-
-}

src/math/polysat/bit_constraint.h

@@ -1,49 +0,0 @@
-/*++
-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,8 +15,9 @@ 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/var_constraint.h"
 #include "math/polysat/eq_constraint.h"
+#include "math/polysat/ule_constraint.h"
 
 namespace polysat {
 
@@ -32,4 +33,12 @@ namespace polysat {
         return alloc(eq_constraint, lvl, p, d);
     }
 
+    constraint* constraint::viable(unsigned lvl, pvar v, bdd const& b, p_dependency_ref& d) {
+        return alloc(var_constraint, lvl, v, b, d);
+    }
+
+    constraint* constraint::ule(unsigned lvl, pdd const& a, pdd const& b, p_dependency_ref& d) {
+        return alloc(ule_constraint, lvl, a, b, d);
+    }
+
 }

src/math/polysat/constraint.h

@@ -23,11 +23,11 @@ namespace polysat {
     enum ckind_t { eq_t, ule_t, sle_t, bit_t };
 
     class eq_constraint;
-    class bit_constraint;
+    class var_constraint;
     class ule_constraint;
 
     class constraint {
-        friend class bit_constraint;
+        friend class var_constraint;
         friend class eq_constraint;
         friend class ule_constraint;
         unsigned         m_level;
@@ -38,6 +38,8 @@ namespace polysat {
             m_level(lvl), m_kind(k), m_dep(dep) {}
     public:
         static constraint* eq(unsigned lvl, pdd const& p, p_dependency_ref& d);
+        static constraint* viable(unsigned lvl, pvar v, bdd const& b, p_dependency_ref& d);
+        static constraint* ule(unsigned lvl, pdd const& a, pdd const& b, p_dependency_ref& d);
         virtual ~constraint() {}
         bool is_eq() const { return m_kind == ckind_t::eq_t; }
         bool is_ule() const { return m_kind == ckind_t::ule_t; }

src/math/polysat/log.cpp

@@ -6,6 +6,19 @@
 #include "util/util.h"
 #include "math/polysat/log.h"
 
+/**
+For windows:
+https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/isatty?view=msvc-160
+
+So include <io.h> and create platform wrapper for _isatty / isatty.
+
+Other:
+- add option to configure z3 trace feature to point to std::err
+- roll this functionality into trace.cpp/trace.h in util
+- Generally, generic functionality should not reside in specific directories.
+- code diverges on coding conventions.
+*/
+
 #if POLYSAT_LOGGING_ENABLED
 
 static LogLevel

src/math/polysat/solver.cpp

@@ -138,13 +138,24 @@ namespace polysat {
     }
 
     void solver::add_diseq(pdd const& p, unsigned dep) {
-#if 0
-        // Basically: 
-        auto slack = add_var(p.size());
-        p = p + var(slack);
-        add_eq(p, dep);
-        m_viable[slack] &= slack != 0;
-#endif
+        if (p.is_val()) {
+            if (!p.is_zero()) 
+                return;
+            // set conflict.
+            NOT_IMPLEMENTED_YET();
+            return;
+        }
+        unsigned sz = size(p.var());
+        auto slack = add_var(size(p.var()));
+        auto q = p + var(slack);
+        add_eq(q, dep);
+        bdd non_zero = m_bdd.mk_false();
+        for (unsigned i = 0; i < sz; ++i) 
+            non_zero |= m_bdd.mk_var(i);
+        p_dependency_ref d(mk_dep(dep), m_dm);        
+        constraint* c = constraint::viable(m_level, slack, non_zero, d);
+        m_constraints.push_back(c);
+        c->narrow(*this);
     }
 
     void solver::add_ule(pdd const& p, pdd const& q, unsigned dep) {
@@ -352,8 +363,6 @@ namespace polysat {
      * 6. Otherwise, add accumulated constraints to explanation for the next viable solution, prune
      *    viable solutions by excluding the previous guess.
      *
-     * todos: replace accumulation of sub by something more incremental.
-     * 
      */
     void solver::resolve_conflict() {
         LOG_H2("Resolve conflict");

src/math/polysat/solver.h

@@ -20,7 +20,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/var_constraint.h"
+#include "math/polysat/ule_constraint.h"
 #include "math/polysat/justification.h"
 #include "math/polysat/trail.h"
 
@@ -37,7 +38,7 @@ namespace polysat {
         };
 
         friend class eq_constraint;
-        friend class bit_constraint;
+        friend class var_constraint;
 
         typedef ptr_vector<constraint> constraints;
 

src/math/polysat/ule_constraint.cpp

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat ule_constraints
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+
+#include "math/polysat/constraint.h"
+#include "math/polysat/solver.h"
+
+namespace polysat {
+
+    std::ostream& ule_constraint::display(std::ostream& out) const {
+        return out << m_lhs << " <=u " << m_rhs;
+    }
+
+    bool ule_constraint::propagate(solver& s, pvar v) {
+        return false;
+    }
+
+    constraint* ule_constraint::resolve(solver& s, pvar v) {
+        return nullptr;
+    }
+
+    void ule_constraint::narrow(solver& s) {
+    }
+
+    bool ule_constraint::is_always_false() {
+        return false;
+    }
+
+    bool ule_constraint::is_currently_false(solver& s) {
+        return false;
+    }
+
+}

src/math/polysat/ule_constraint.h

@@ -0,0 +1,43 @@
+/*++
+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 ule_constraint : public constraint {
+        pdd m_lhs;
+        pdd m_rhs;
+    public:
+        ule_constraint(unsigned lvl, pdd const& l, pdd const& r, p_dependency_ref& dep):
+            constraint(lvl, dep, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
+            m_vars.append(l.free_vars());
+            for (auto v : r.free_vars())
+                if (!m_vars.contains(v))
+                    m_vars.push_back(v);
+        }
+        ~ule_constraint() override {}
+        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/var_constraint.cpp

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat var_constraint
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+
+#include "math/polysat/var_constraint.h"
+#include "math/polysat/solver.h"
+
+namespace polysat {
+
+    std::ostream& var_constraint::display(std::ostream& out) const {
+        return out << "v" << m_var << ": " << m_viable << "\n";
+    }
+
+    bool var_constraint::propagate(solver& s, pvar v) {       
+        UNREACHABLE();
+        return false;
+    }
+
+    constraint* var_constraint::resolve(solver& s, pvar v) {
+        UNREACHABLE();
+        return nullptr;
+    }
+
+    bool var_constraint::is_always_false() {
+        return false;
+    }
+
+    bool var_constraint::is_currently_false(solver& s) {
+        return s.m_viable[m_var].is_false();
+    }
+
+    void var_constraint::narrow(solver& s) {
+        s.intersect_viable(m_var, m_viable);
+    }
+
+}

src/math/polysat/var_constraint.h

@@ -0,0 +1,42 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat var_constraint
+
+Abstract:
+
+    Var constraints restrict viable values.
+
+    The main way var-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/dd/dd_bdd.h"
+#include "math/polysat/constraint.h"
+
+
+namespace polysat {
+
+    class var_constraint : public constraint {
+        pvar        m_var;
+        bdd         m_viable;
+    public:
+        var_constraint(unsigned lvl, pvar v, bdd const & b, p_dependency_ref& dep):
+            constraint(lvl, dep, ckind_t::bit_t), m_var(v), m_viable(b) {}
+        ~var_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;
+    };
+}