na

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

src/math/dd/dd_bdd.cpp

@@ -927,7 +927,7 @@ namespace dd {
         SASSERT(a.size() == b.size());
         bdd lt = mk_false();
         bdd eq = mk_true();
-        for (unsigned i = a.size(); i-- > 0; ) {
+        for (unsigned i = a.size(); i-- > 0 && !eq.is_false(); ) {
             lt |= eq && (!a[i] && b[i]);
             eq &= !(a[i] ^ b[i]);
         }
@@ -1179,4 +1179,19 @@ namespace dd {
         m_bits[size() - 1] = m->mk_false();
     }
 
+    bdd bddv::all0() const {
+        bdd r = m->mk_true();
+        for (unsigned i = size(); i-- > 0; )
+            r &= !m_bits[i];
+        return r;
+    }
+
+    bdd bddv::all1() const {
+        bdd r = m->mk_true();
+        for (unsigned i = size(); i-- > 0; )
+            r &= m_bits[i];
+        return r;
+    }
+
+
 }

src/math/dd/dd_bdd.h

@@ -338,6 +338,9 @@ namespace dd {
         bdd slt(bddv const& other) const { return m->mk_slt(*this, other); }
         bdd sgt(bddv const& other) const { return m->mk_sgt(*this, other); }
 
+        bdd all0() const;        
+        bdd all1() const;
+
         bdd operator==(bddv const& other) const { return m->mk_eq(*this, other); }
         bdd operator==(rational const& other) const { return m->mk_eq(*this, other); }
         bdd operator!=(bddv const& other) const { return !m->mk_eq(*this, other); }

src/math/polysat/eq_constraint.cpp

@@ -59,20 +59,29 @@ namespace polysat {
         if (q.is_unilinear()) {
             // a*x + b == 0
             pvar v = q.var();
+            s.push_cjust(v, this);
+
             rational a = q.hi().val();
             rational b = q.lo().val();
             bddv const& x = s.var2bits(v).var();
-            bddv lhs = a * x + b;
-            rational zero = rational::zero();
-            bdd xs = is_positive() ? (lhs == zero) : (lhs != zero);
-            s.push_cjust(v, this);
-            s.intersect_viable(v, xs);
-
-            rational val;
-            if (s.find_viable(v, val) == dd::find_t::singleton) {
-                s.propagate(v, val, *this);
+            if (b == 0 && a.is_odd()) {
+                // hacky test optimizing special case.
+                // general case is compute inverse(a)*-b for equality 2^k*a*x + b == 0
+                // then constrain x.
+                // 
+                s.intersect_viable(v, is_positive() ? x.all0() : !x.all0());
+            }
+            else {
+                IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << "\n");
+                
+                bddv lhs = a * x + b;
+                bdd xs = is_positive() ? lhs.all0() : !lhs.all0();
+                s.intersect_viable(v, xs);
             }
 
+            rational val;
+            if (s.find_viable(v, val) == dd::find_t::singleton) 
+                s.propagate(v, val, *this);
             return;
         }
 

src/math/polysat/solver.h

@@ -188,6 +188,7 @@ namespace polysat {
 
         void del_var();
 
+        dd::bdd_manager& get_bdd() { return m_bdd; }
         dd::pdd_manager& sz2pdd(unsigned sz);
         dd::fdd const& sz2bits(unsigned sz);
         dd::fdd const& var2bits(pvar v) { return sz2bits(size(v)); }

src/math/polysat/ule_constraint.cpp

@@ -75,11 +75,18 @@ namespace polysat {
         }
         if (v != null_var) {
             bddv const& x = s.var2bits(v).var();
-            bddv l = a * x + b;
-            bddv r = c * x + d;
-            bdd xs = is_positive() ? (l <= r) : (l > r);
             s.push_cjust(v, this);
-            s.intersect_viable(v, xs);
+            // hacky special case
+            if (a == 1 && b == 0 && c == 0 && d == 0) 
+                // x <= 0
+                s.intersect_viable(v, is_positive() ? x.all0() : !x.all0());
+            else {
+                IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << (is_positive() ? " <= " : " > ") << c << "*x + " << d << "\n");
+                bddv l = a * x + b;
+                bddv r = c * x + d;
+                bdd xs = is_positive() ? (l <= r) : (l > r);
+                s.intersect_viable(v, xs);
+            }
 
             rational val;
             if (s.find_viable(v, val) == dd::find_t::singleton) {