Fix handling for UGT/SGT. (#1467)

Previously, we only handled the case x s < t. With this fix, we now get BITVECTOR_[SU]GT for litk
if we encounter a literal t < x s.

1 files changed, 58 insertions, 43 deletions

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index c1e59e3c0..8068b563e 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -205,15 +205,15 @@ static Node dropChild(Node n, unsigned index)
   return nb.constructNode();
 }
 
-static Node getScBvUlt(bool pol, Kind k, unsigned idx, Node x, Node t)
+static Node getScBvUltUgt(bool pol, Kind k, Node x, Node t)
 {
-  Assert(k == BITVECTOR_ULT);
+  Assert(k == BITVECTOR_ULT || k == BITVECTOR_UGT);
 
   NodeManager* nm = NodeManager::currentNM();
   unsigned w = bv::utils::getSize(t);
   Node sc;
 
-  if (idx == 0)
+  if (k == BITVECTOR_ULT)
   {
     if (pol == true)
     {
@@ -227,41 +227,42 @@ static Node getScBvUlt(bool pol, Kind k, unsigned idx, Node x, Node t)
     else
     {
       /* x >= t
-       * no side condition  */
+       * true (no side condition)  */
       sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
     }
   }
-  else if (idx == 1)
+  else
   {
+    Assert(k == BITVECTOR_UGT);
     if (pol == true)
     {
-      /* t < x
+      /* x > t
        * with side condition:
        * t != ~0  */
       Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w));
-      Node scr = nm->mkNode(k, t, x);
+      Node scr = nm->mkNode(k, x, t);
       sc = nm->mkNode(IMPLIES, scl, scr);
     }
     else
     {
-      /* t >= x
-       * no side condition */
-      sc = nm->mkNode(NOT, nm->mkNode(k, t, x));
+      /* x <= t
+       * true (no side condition) */
+      sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
     }
   }
   Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
   return sc;
 }
 
-static Node getScBvSlt(bool pol, Kind k, unsigned idx, Node x, Node t)
+static Node getScBvSltSgt(bool pol, Kind k, Node x, Node t)
 {
-  Assert(k == BITVECTOR_SLT);
+  Assert(k == BITVECTOR_SLT || k == BITVECTOR_SGT);
 
   NodeManager* nm = NodeManager::currentNM();
   unsigned w = bv::utils::getSize(t);
   Node sc;
 
-  if (idx == 0)
+  if (k == BITVECTOR_SLT)
   {
     if (pol == true)
     {
@@ -276,28 +277,29 @@ static Node getScBvSlt(bool pol, Kind k, unsigned idx, Node x, Node t)
     else
     {
       /* x >= t
-       * no side condition */
+       * true (no side condition) */
       sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
     }
   }
-  else if (idx == 1)
+  else
   {
+    Assert(k == BITVECTOR_SGT);
     if (pol == true)
     {
-      /* t < x
+      /* x > t
        * with side condition:
        * t != 01...1  */
       BitVector bv = BitVector(w).setBit(w - 1);
       Node max = bv::utils::mkConst(~bv);
       Node scl = nm->mkNode(DISTINCT, t, max);
-      Node scr = nm->mkNode(k, t, x);
+      Node scr = nm->mkNode(k, x, t);
       sc = nm->mkNode(IMPLIES, scl, scr);
     }
     else
     {
-      /* t >= x
-       * no side condition */
-      sc = nm->mkNode(NOT, nm->mkNode(k, t, x));
+      /* x <= t
+       * true (no side condition) */
+      sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
     }
   }
   Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
@@ -363,7 +365,8 @@ static Node getScBvUrem(bool pol,
                         Node t)
 {
   Assert(k == BITVECTOR_UREM_TOTAL);
-  Assert (litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT);
+  Assert (litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT
+          || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT);
 
   NodeManager* nm = NodeManager::currentNM();
   Node scl;
@@ -472,7 +475,7 @@ static Node getScBvUrem(bool pol,
       }
     }
   }
-  else  /* litk == BITVECTOR_SLT  */
+  else if (litk == BITVECTOR_SLT)
   {
     if (idx == 0)
     {
@@ -531,6 +534,10 @@ static Node getScBvUrem(bool pol,
       }
     }
   }
+  else
+  {
+    return Node::null();
+  }
 
   Node scr =
     nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t);
@@ -644,7 +651,8 @@ static Node getScBvAndOr(bool pol,
                          Node t)
 {
   Assert (k == BITVECTOR_AND || k == BITVECTOR_OR);
-  Assert (litk == EQUAL || litk == BITVECTOR_SLT || litk == BITVECTOR_ULT);
+  Assert (litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT
+          || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT);
 
   NodeManager* nm = NodeManager::currentNM();
   Node scl, scr;
@@ -788,7 +796,8 @@ static Node getScBvLshr(bool pol,
                         Node t)
 {
   Assert(k == BITVECTOR_LSHR);
-  Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT);
+  Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT
+         || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT);
 
   NodeManager* nm = NodeManager::currentNM();
   Node scl;
@@ -915,7 +924,7 @@ static Node getScBvLshr(bool pol,
       }
     }
   }
-  else /* litk == BITVECTOR_SLT */
+  else if (litk == BITVECTOR_SLT)
   {
     if (idx == 0)
     {
@@ -967,6 +976,10 @@ static Node getScBvLshr(bool pol,
       }
     }
   }
+  else
+  {
+    return Node::null();
+  }
   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());
@@ -1258,6 +1271,14 @@ Node BvInverter::solveBvLit(Node sv,
 
   Node sv_t = lit[index];
   Node t = lit[1-index];
+  if (litk == BITVECTOR_ULT && index == 1)
+  {
+    litk = BITVECTOR_UGT;
+  }
+  else if (litk == BITVECTOR_SLT && index == 1)
+  {
+    litk = BITVECTOR_SGT;
+  }
 
   /* Bit-vector layer -------------------------------------------- */
 
@@ -1273,7 +1294,7 @@ Node BvInverter::solveBvLit(Node sv,
     {
       t = nm->mkNode(k, t);
     }
-    else if (k == BITVECTOR_CONCAT)
+    else if (k == BITVECTOR_CONCAT && litk == EQUAL)
     {
       /* x = t[upper:lower]
        * where
@@ -1291,7 +1312,7 @@ Node BvInverter::solveBvLit(Node sv,
       }
       t = bv::utils::mkExtract(t, upper, lower);
     }
-    else if (k == BITVECTOR_SIGN_EXTEND)
+    else if (k == BITVECTOR_SIGN_EXTEND && litk == EQUAL)
     {
       t = bv::utils::mkExtract(t, bv::utils::getSize(sv_t[index]) - 1, 0);
     }
@@ -1307,15 +1328,11 @@ Node BvInverter::solveBvLit(Node sv,
       Node s = nchildren == 2 ? sv_t[1 - index] : dropChild(sv_t, index);
       /* Note: All n-ary kinds except for CONCAT (i.e., AND, OR, MULT, PLUS)
        *       are commutative (no case split based on index). */
-      if (k == BITVECTOR_PLUS)
+      if (k == BITVECTOR_PLUS && litk == EQUAL)
       {
         t = nm->mkNode(BITVECTOR_SUB, t, s);
       }
-      else if (k == BITVECTOR_SUB)
-      {
-        t = nm->mkNode(BITVECTOR_PLUS, t, s);
-      }
-      else if (k == BITVECTOR_XOR)
+      else if (k == BITVECTOR_XOR && litk == EQUAL)
       {
         t = nm->mkNode(BITVECTOR_XOR, t, s);
       }
@@ -1373,16 +1390,14 @@ Node BvInverter::solveBvLit(Node sv,
         if (sc.isNull())
         {
           solve_tn = sv_t.getType();
-          if (litk == BITVECTOR_ULT)
+          if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT)
           {
-            sc = getScBvUlt(
-                pol, litk, index, getSolveVariable(solve_tn), t);
+            sc = getScBvUltUgt(pol, litk, getSolveVariable(solve_tn), t);
           }
           else
           {
-            Assert (litk == BITVECTOR_SLT);
-            sc = getScBvSlt(
-                pol, litk, index, getSolveVariable(solve_tn), t);
+            Assert (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT);
+            sc = getScBvSltSgt(pol, litk, getSolveVariable(solve_tn), t);
           }
         }
         /* We generate a choice term (choice x0. SC => x0 <k> s <litk> t) for
@@ -1398,16 +1413,16 @@ Node BvInverter::solveBvLit(Node sv,
     sv_t = sv_t[index];
   }
   Assert(sv_t == sv);
-  if (litk == BITVECTOR_ULT)
+  if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT)
   {
     TypeNode solve_tn = sv_t.getType();
-    Node sc = getScBvUlt(pol, litk, index, getSolveVariable(solve_tn), t);
+    Node sc = getScBvUltUgt(pol, litk, getSolveVariable(solve_tn), t);
     t = getInversionNode(sc, solve_tn, m);
   }
-  else if (litk == BITVECTOR_SLT)
+  else if (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT)
   {
     TypeNode solve_tn = sv_t.getType();
-    Node sc = getScBvSlt(pol, litk, index, getSolveVariable(solve_tn), t);
+    Node sc = getScBvSltSgt(pol, litk, getSolveVariable(solve_tn), t);
     t = getInversionNode(sc, solve_tn, m);
   }
   else if (pol == false)