add parity constraint for disequality

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

src/math/polysat/conflict.cpp

@@ -298,7 +298,7 @@ namespace polysat {
 
     void conflict::insert_vars(signed_constraint c) {
         for (pvar v : c->vars())
-            if (s.is_assigned(v))
+            if (s.is_assigned(v)) 
                 m_vars.insert(v);
     }
 

src/math/polysat/saturation.cpp

@@ -35,7 +35,10 @@ namespace polysat {
     void saturation::perform(pvar v, conflict& core) {
         for (auto c : core) 
             if (perform(v, c, core)) {
-                IF_VERBOSE(0, verbose_stream() << m_rule << " v" << v << " " << c << "\n");
+                IF_VERBOSE(0, auto const& cl = core.lemmas().back(); 
+                           verbose_stream() << m_rule << " v" << v << " "; 
+                           for (auto lit : *cl) verbose_stream() << s.lit2cnstr(lit) << " "; 
+                           verbose_stream() << "\n");
                 return;
             }
     }
@@ -50,6 +53,8 @@ namespace polysat {
             return true;
         if (try_parity(v, core, i))
             return true;
+        if (try_parity_diseq(v, core, i))
+            return true;
         if (try_factor_equality(v, core, i))
             return true;
         if (try_ugt_x(v, core, i))
@@ -251,6 +256,16 @@ namespace polysat {
         return y.is_val() && y.val() == 0 && i.rhs() == y && i.lhs() == a * s.var(x) + b;
     }
 
+    bool saturation::is_AxB_diseq_0(pvar x, inequality const& i, pdd& a, pdd& b, pdd& y) {
+        if (!i.is_strict())
+            return false;
+        y = i.lhs();
+        rational y_val;
+        if (!s.try_eval(y, y_val) || y_val != 0)
+            return false;
+        return i.rhs().degree(x) == 1 && (i.rhs().factor(x, 1, a, b), true);
+    }
+
     /**
      * Match [coeff*x] coeff*x*Y where x is a variable
      */
@@ -755,6 +770,32 @@ namespace polysat {
         return false;        
     }
 
+    /**
+     *  2^{K-1}*x*y != 0 => odd(x) & odd(y)
+     *  2^k*x != 0 => parity(x) < K - k
+     *  2^k*x*y != 0 => parity(x) + parity(y) < K - k
+     */
+    bool saturation::try_parity_diseq(pvar x, conflict& core, inequality const& axb_l_y) {
+        set_rule("[x] 2^k*x*y != 0 => parity(x) + parity(y) < K - k");
+        auto& m = s.var2pdd(x);
+        unsigned N = m.power_of_2();
+        pdd y = m.zero();
+        pdd a = y, b = y, X = y;
+        if (!is_AxB_diseq_0(x, axb_l_y, a, b, y))
+            return false;
+        if (!is_forced_eq(b, 0))
+            return false;
+        auto coeff = a.leading_coefficient();
+        if (coeff.is_odd())
+            return false;
+        SASSERT(coeff != 0);
+        unsigned k = coeff.trailing_zeros();
+        m_lemma.reset();
+        m_lemma.insert_eval(~s.eq(y));
+        m_lemma.insert_eval(~s.eq(b));        
+        return propagate(core, axb_l_y, ~s.parity(X, N - k));        
+    }
+
     /**
      * a*x = 0 => a = 0 or even(x)
      * a*x = 0 => a = 0 or x = 0 or even(a)

src/math/polysat/saturation.h

@@ -47,6 +47,7 @@ namespace polysat {
         bool try_ugt_z(pvar z, conflict& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x);
 
         bool try_parity(pvar x, conflict& core, inequality const& axb_l_y);
+        bool try_parity_diseq(pvar x, conflict& core, inequality const& axb_l_y);
         bool try_mul_bounds(pvar x, conflict& core, inequality const& axb_l_y);
         bool try_factor_equality(pvar x, conflict& core, inequality const& a_l_b);
         bool try_mul_eq_1(pvar x, conflict& core, inequality const& axb_l_y);
@@ -87,6 +88,8 @@ namespace polysat {
         bool is_AxB_eq_0(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y);
         bool verify_AxB_eq_0(pvar x, inequality const& c, pdd const& a, pdd const& b, pdd const& y);
 
+        // c := Ax + B != Y, val(Y) = 0
+        bool is_AxB_diseq_0(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y);
 
         // c := Y*X ~ z*X
         bool is_YX_l_zX(pvar z, inequality const& c, pdd& x, pdd& y);