From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Sat, 30 Dec 2017 04:02:38 +0000 (-0800)
Subject: Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)
X-Git-Tag: cvc5-1.0.0~5398
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dc2f9914f49076d56cdb18e14971df67fbe567bb;p=cvc5.git

Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)

We now can handle all cases of (in|dis)equality over UREM. Previously, we could not handle equality
for index=0 and had to rewrite x % s = t to x - x / s * s. Since we can now handle this case, we do not
apply this rewriting anymore.
---

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 9fe645a9a..cce56ab01 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -111,7 +111,7 @@ static bool isInvertible(Kind k, unsigned index)
       ||  k == BITVECTOR_PLUS
       ||  k == BITVECTOR_SUB
       ||  k == BITVECTOR_MULT
-      || (k == BITVECTOR_UREM_TOTAL && index == 1)
+      ||  k == BITVECTOR_UREM_TOTAL
       ||  k == BITVECTOR_UDIV_TOTAL
       ||  k == BITVECTOR_AND
       ||  k == BITVECTOR_OR
@@ -363,11 +363,10 @@ static Node getScBvUrem(bool pol,
                         Node t)
 {
   Assert(k == BITVECTOR_UREM_TOTAL);
-  Assert(litk != EQUAL || pol == false || idx == 1);
-
+  Assert (litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT);
 
   NodeManager* nm = NodeManager::currentNM();
-  Node scl, scr;
+  Node scl;
   unsigned w = bv::utils::getSize(s);
   Assert (w == bv::utils::getSize(t));
   Node z = bv::utils::mkZero(w);
@@ -376,37 +375,46 @@ static Node getScBvUrem(bool pol,
   {
     if (idx == 0)
     {
-      Assert (pol == false);
-      /* x % s != t
-       * with side condition:
-       * s != 1 || t != 0  */
-      scl = nm->mkNode(OR,
-          s.eqNode(bv::utils::mkOne(w)).notNode(),
-          t.eqNode(z).notNode());
-      scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t);
+      if (pol)
+      {
+        /* x % s = t
+         * with side condition (synthesized):
+         * (not (bvult (bvnot (bvneg s)) t)) 
+         * <->
+         * ~(-s) >= t*/
+        Node neg = nm->mkNode(BITVECTOR_NEG, s);
+        scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t);
+      }
+      else
+      {
+        /* x % s != t
+         * with side condition:
+         * s != 1 || t != 0  */
+        scl = nm->mkNode(OR,
+            s.eqNode(bv::utils::mkOne(w)).notNode(),
+            t.eqNode(z).notNode());
+      }
     }
     else
     {
       if (pol)
       {
         /* s % x = t
-         * with side condition:
+         * with side condition (synthesized):
+         * (bvuge (bvand (bvsub (bvadd t t) s) s) t)
+         * <->
+         * (t + t - s) & s >= t
+         *
+         * is equivalent to:
          * s = t
          * ||
          * ( s > t
          *   && s-t > t
          *   && (t = 0 || t != s-1) )  */
-
-        Node a1 = nm->mkNode(BITVECTOR_UGT, s, t);
-        Node a2 = nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t);
-        Node a3 = nm->mkNode(OR,
-            t.eqNode(z),
-            t.eqNode(bv::utils::mkDec(s)).notNode());
-
-        scl = nm->mkNode(OR,
-              t.eqNode(s),
-              nm->mkNode(AND, a1, nm->mkNode(AND, a2, a3)));
-        scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t);
+        Node add = nm->mkNode(BITVECTOR_PLUS, t, t);
+        Node sub = nm->mkNode(BITVECTOR_SUB, add, s);
+        Node a = nm->mkNode(BITVECTOR_AND, sub, s);
+        scl = nm->mkNode(BITVECTOR_UGE, a, t);
       }
       else
       {
@@ -414,16 +422,119 @@ static Node getScBvUrem(bool pol,
          * with side condition:
          * s != 0 || t != 0  */
         scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
-        scr = nm->mkNode(DISTINCT, nm->mkNode(k, s, x), t);
       }
     }
   }
-  else
+  else if (litk == BITVECTOR_ULT)
   {
-    return Node::null();
+    if (idx == 0)
+    {
+      if (pol)
+      {
+        /* x % s < t
+         * with side condition:
+         * (distinct t z)
+         * where z = 0 with getSize(z) = w  */
+        scl = t.eqNode(z).notNode();
+      }
+      else
+      {
+        /* x % s >= t
+         * with side condition (synthesized):
+         * (bvuge (bvnot (bvneg s)) t)  */
+        Node neg = nm->mkNode(BITVECTOR_NEG, s);
+        scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t);
+      }
+    }
+    else
+    {
+      if (pol)
+      {
+        /* s % x < t
+         * with side condition:
+         * (distinct t z)
+         * where z = 0 with getSize(z) = w  */
+        scl = t.eqNode(z).notNode();
+      }
+      else
+      {
+        /* s % x < t
+         * with side condition (combination of = and >):
+         * (or
+         *   (bvuge (bvand (bvsub (bvadd t t) s) s) t)  ; eq, synthesized
+         *   (bvult t s))                               ; ugt, synthesized  */
+        Node add = nm->mkNode(BITVECTOR_PLUS, t, t);
+        Node sub = nm->mkNode(BITVECTOR_SUB, add, s);
+        Node a = nm->mkNode(BITVECTOR_AND, sub, s);
+        Node sceq = nm->mkNode(BITVECTOR_UGE, a, t);
+        Node scugt = nm->mkNode(BITVECTOR_ULT, t, s);
+        scl = nm->mkNode(OR, sceq, scugt);
+      }
+    }
+  }
+  else  /* litk == BITVECTOR_SLT  */
+  {
+    if (idx == 0)
+    {
+      if (pol)
+      {
+        /* x % s < t
+         * with side condition (synthesized):
+         * (bvslt (bvnot t) (bvor (bvneg s) (bvneg t)))  */
+        Node o1 = nm->mkNode(BITVECTOR_NEG, s);
+        Node o2 = nm->mkNode(BITVECTOR_NEG, t);
+        Node o = nm->mkNode(BITVECTOR_OR, o1, o2);
+        scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_NOT, t), o);
+      }
+      else
+      {
+        /* x % s >= t
+         * with side condition (synthesized):
+         * (or (bvslt t s) (bvsge z s))
+         * where z = 0 with getSize(z) = w  */
+        Node s1 = nm->mkNode(BITVECTOR_SLT, t, s);
+        Node s2 = nm->mkNode(BITVECTOR_SGE, z, s);
+        scl = nm->mkNode(OR, s1, s2);
+      }
+    }
+    else
+    {
+      if (pol)
+      {
+        /* s % x < t
+         * with side condition (synthesized):
+         * (or (bvslt s t) (bvslt z t))
+         * where z = 0 with getSize(z) = w  */
+        Node slt1 = nm->mkNode(BITVECTOR_SLT, s, t);
+        Node slt2 = nm->mkNode(BITVECTOR_SLT, z, t);
+        scl = nm->mkNode(OR, slt1, slt2);
+      }
+      else
+      {
+        /* s % x < t
+         * with side condition:
+         * (and
+         *   (=> (= s z) (bvsle t z))
+         *   (=> (bvsgt s z) (bvsge s t))
+         *   (=> (and (bvslt s z) (bvsge t z)) (bvugt (bvsub s t) t)))
+         * where z = 0 with getSize(z) = w  */
+        Node i1 = nm->mkNode(IMPLIES,
+            s.eqNode(z), nm->mkNode(BITVECTOR_SLE, t, z));
+        Node i2 = nm->mkNode(IMPLIES,
+            nm->mkNode(BITVECTOR_SLT, s, z), nm->mkNode(BITVECTOR_SGE, s, t));
+        Node i3 = nm->mkNode(IMPLIES,
+            nm->mkNode(AND,
+              nm->mkNode(BITVECTOR_SLT, s, z), nm->mkNode(BITVECTOR_SGE, t, z)),
+            nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t));
+        scl = nm->mkNode(AND, i1, i2, i3);
+        return Node::null();
+      }
+    }
   }
 
-  Node sc = nm->mkNode(IMPLIES, scl, scr);
+  Node scr =
+    nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t);
+  Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode());
   Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
   return sc;
 }
@@ -1141,13 +1252,6 @@ Node BvInverter::solveBvLit(Node sv,
             break;
 
           case BITVECTOR_UREM_TOTAL:
-            if (index == 0)
-            {
-              /* x % s = t is rewritten to x - x / y * y */
-              Trace("bv-invert") << "bv-invert : Unsupported for index "
-                                 << index << ", from " << sv_t << std::endl;
-              return Node::null();
-            }
             sc = getScBvUrem(
                 pol, litk, k, index, getSolveVariable(solve_tn), s, t);
             break;
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index f0031cd54..4b326ede6 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -1761,21 +1761,7 @@ Node BvInstantiator::rewriteTermForSolvePv(
 
   // [1] rewrite cases of non-invertible operators
 
-  // if n is urem( x, y ) where x contains pv but y does not, then
-  // rewrite urem( x, y ) ---> x - udiv( x, y )*y
-  if (n.getKind() == BITVECTOR_UREM_TOTAL)
-  {
-    if (contains_pv[n[0]] && !contains_pv[n[1]])
-    {
-      return nm->mkNode(
-          BITVECTOR_SUB,
-          children[0],
-          nm->mkNode(BITVECTOR_MULT,
-                     nm->mkNode(BITVECTOR_UDIV_TOTAL, children[0], children[1]),
-                     children[1]));
-    }
-  }
-  else if (n.getKind() == EQUAL)
+  if (n.getKind() == EQUAL)
   {
     TNode lhs = children[0];
     TNode rhs = children[1];
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
index e1d950050..6f078d2e3 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
@@ -85,8 +85,6 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
            || k == BITVECTOR_ASHR
 
            || k == BITVECTOR_SHL);
-    Assert(litk != EQUAL 
-           || k != BITVECTOR_UREM_TOTAL || pol == false || idx == 1);
 
     Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t);
     // TODO amend / remove the following six lines as soon as inequality
@@ -219,8 +217,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
 
   void testGetScBvUremEqTrue0()
   {
-    TS_ASSERT_THROWS(runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem),
-                     AssertionException);
+    runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem);
   }
 
   void testGetScBvUremEqTrue1()