remove var_constraint to get rid of bdd dependencies

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

src/math/polysat/constraint.cpp

@@ -103,6 +103,7 @@ namespace polysat {
         return *dynamic_cast<ule_constraint const*>(this);
     }
 
+#if 0
     var_constraint& constraint::to_bit() {
         return *dynamic_cast<var_constraint*>(this);
     }
@@ -111,13 +112,16 @@ namespace polysat {
         return *dynamic_cast<var_constraint const*>(this);
     }
 
+    constraint_ref constraint_manager::viable(unsigned lvl, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d) {
+        return alloc(var_constraint, *this, lvl, sign, v, b, d);
+    }
+
+#endif
+
     constraint_ref constraint_manager::eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d) {
         return alloc(eq_constraint, *this, lvl, sign, p, d);
     }
 
-    constraint_ref constraint_manager::viable(unsigned lvl, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d) {
-        return alloc(var_constraint, *this, lvl, sign, v, b, d);
-    }
 
     constraint_ref constraint_manager::ule(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
         return alloc(ule_constraint, *this, lvl, sign, a, b, d);

src/math/polysat/constraint.h

@@ -22,7 +22,7 @@ Author:
 
 namespace polysat {
 
-    enum ckind_t { eq_t, ule_t, bit_t };
+    enum ckind_t { eq_t, ule_t };
     enum csign_t : bool { neg_t = false, pos_t = true };
 
     class constraint;
@@ -30,7 +30,7 @@ namespace polysat {
     class clause;
     class scoped_clause;
     class eq_constraint;
-    class var_constraint;
+    // class var_constraint;
     class ule_constraint;
     using constraint_ref = ref<constraint>;
     using constraint_ref_vector = sref_vector<constraint>;
@@ -85,7 +85,7 @@ namespace polysat {
         friend class constraint_manager;
         friend class clause;
         friend class scoped_clause;
-        friend class var_constraint;
+        // friend class var_constraint;
         friend class eq_constraint;
         friend class ule_constraint;
 
@@ -122,7 +122,6 @@ namespace polysat {
 
         bool is_eq() const { return m_kind == ckind_t::eq_t; }
         bool is_ule() const { return m_kind == ckind_t::ule_t; }
-        bool is_bit() const { return m_kind == ckind_t::bit_t; }
         ckind_t kind() const { return m_kind; }
         virtual std::ostream& display(std::ostream& out) const = 0;
         bool propagate(solver& s, pvar v);
@@ -135,8 +134,6 @@ namespace polysat {
         eq_constraint const& to_eq() const;
         ule_constraint& to_ule();
         ule_constraint const& to_ule() const;
-        var_constraint& to_bit();
-        var_constraint const& to_bit() const;
         p_dependency* dep() const { return m_dep; }
         unsigned_vector& vars() { return m_vars; }
         unsigned_vector const& vars() const { return m_vars; }

src/math/polysat/eq_constraint.cpp

@@ -72,6 +72,7 @@ namespace polysat {
             return;
         }
 
+
         // TODO: what other constraints can be extracted cheaply?
     }
 

src/math/polysat/linear_solver.cpp

@@ -189,13 +189,6 @@ namespace polysat {
         m_rows.push_back(std::make_pair(v, sz));
     }
 
-    void linear_solver::new_bit(var_constraint& c) {
-    }
-
-    void linear_solver::assert_bit(var_constraint& c) {
-
-    }
-
 
     void linear_solver::new_constraint(constraint& c) {
         switch (c.kind()) {
@@ -205,9 +198,6 @@ namespace polysat {
         case ckind_t::ule_t:
             new_le(c.to_ule());
             break;
-        case ckind_t::bit_t:
-            new_bit(c.to_bit());
-            break;
         default:
             UNREACHABLE();
             break;
@@ -223,9 +213,6 @@ namespace polysat {
         case ckind_t::ule_t:
             assert_le(c.to_ule());
             break;
-        case ckind_t::bit_t:
-            assert_bit(c.to_bit());            
-            break;
         default:
             UNREACHABLE();
             break;

src/math/polysat/linear_solver.h

@@ -100,10 +100,8 @@ namespace polysat {
         var_t internalize_pdd(pdd const& p);
         void new_eq(eq_constraint& eq);
         void new_le(ule_constraint& le);
-        void new_bit(var_constraint& vc);
         void assert_eq(eq_constraint& eq);
         void assert_le(ule_constraint& le);
-        void assert_bit(var_constraint& vc);
 
         // bind monomial to variable.
         var_t mono2var(unsigned sz, unsigned_vector const& m);

src/math/polysat/solver.cpp

@@ -117,12 +117,13 @@ namespace polysat {
     }
 
     constraint_ref solver::mk_diseq(pdd const& p, unsigned dep) {
+        return m_constraints.eq(m_level, neg_t, p, mk_dep_ref(dep));
+#if 0
         if (p.is_val()) {
             // if (!p.is_zero())
             //     return nullptr;  // TODO: probably better to create a dummy always-true constraint?
             // // Use 0 != 0 for a constraint that is always false
             // Use p != 0 as evaluable dummy constraint
-            return m_constraints.eq(m_level, neg_t, p, mk_dep_ref(dep));
         }
         unsigned sz = size(p.var());
         auto slack = add_var(sz);
@@ -130,6 +131,7 @@ namespace polysat {
         add_eq(q, dep);  // TODO: 'dep' now refers to two constraints; this is not yet supported
         auto non_zero = m_vble.sz2bits(sz).non_zero();
         return m_constraints.viable(m_level, pos_t, slack, non_zero, mk_dep_ref(dep));
+#endif
     }
 
     constraint_ref solver::mk_ule(pdd const& p, pdd const& q, unsigned dep) {

src/math/polysat/var_constraint.cpp

@@ -12,6 +12,7 @@ Author:
 
 --*/
 
+#if 0
 #include "math/polysat/var_constraint.h"
 #include "math/polysat/solver.h"
 
@@ -44,3 +45,4 @@ namespace polysat {
     }
 
 }
+#endif

src/math/polysat/var_constraint.h

@@ -18,6 +18,10 @@ Author:
     Jakob Rath 2021-04-6
 
 --*/
+
+
+#if 0
+// to remove
 #pragma once
 #include "math/dd/dd_bdd.h"
 #include "math/polysat/constraint.h"
@@ -40,3 +44,5 @@ namespace polysat {
         bool is_currently_true(solver& s) override;
     };
 }
+
+#endif