From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 3 Jan 2018 00:54:32 +0000 (-0800)
Subject: Fix handling for UGT/SGT. (#1467)
X-Git-Tag: cvc5-1.0.0~5394
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f8f8103229a9b84e944148985ebb05abed814619;p=cvc5.git

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.
---

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)
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
index 6f078d2e3..dc7164e54 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
@@ -43,27 +43,45 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
 
   void runTestPred(bool pol,
                    Kind k,
-                   unsigned idx,
-                   Node (*getsc)(bool, Kind, unsigned, Node, Node))
+                   Node (*getsc)(bool, Kind, Node, Node))
   {
-    Assert(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL);
+    Assert(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL
+           || k == BITVECTOR_UGT || k == BITVECTOR_SGT);
     Assert(k != EQUAL || pol == false);
 
-    Node sc = getsc(pol, k, idx, d_sk, d_t);
+    Node sc = getsc(pol, k, d_sk, d_t);
     Kind ksc = sc.getKind();
     TS_ASSERT((k == BITVECTOR_ULT && pol == false)
            || (k == BITVECTOR_SLT && pol == false)
+           || (k == BITVECTOR_UGT && pol == false)
+           || (k == BITVECTOR_SGT && pol == false)
            || ksc == IMPLIES);
     Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue();
     if (!pol)
     {
-      k = k == BITVECTOR_ULT
-        ? BITVECTOR_UGE
-        : (k == BITVECTOR_SLT ? BITVECTOR_SGE : DISTINCT);
+      if (k == BITVECTOR_ULT)
+      {
+        k = BITVECTOR_UGE;
+      }
+      else if (k == BITVECTOR_UGT)
+      {
+        k = BITVECTOR_ULE;
+      }
+      else if (k == BITVECTOR_SLT)
+      {
+        k = BITVECTOR_SGE;
+      }
+      else if (k == BITVECTOR_SGT)
+      {
+        k = BITVECTOR_ULE;
+      }
+      else
+      {
+        Assert(k == EQUAL);
+        k = DISTINCT;
+      }
     }
-    Node body = idx == 0
-      ? d_nm->mkNode(k, d_x, d_t)
-      : d_nm->mkNode(k, d_t, d_x);
+    Node body = d_nm->mkNode(k, d_x, d_t);
     Node scr = d_nm->mkNode(EXISTS, d_bvarlist, body);
     Expr a = d_nm->mkNode(DISTINCT, scl, scr).toExpr();
     Result res = d_smt->checkSat(a);
@@ -92,7 +110,8 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     TS_ASSERT (litk != EQUAL || sc != Node::null());
     if (sc.isNull())
     {
-      TS_ASSERT (litk == BITVECTOR_ULT || litk  == BITVECTOR_SLT);
+      TS_ASSERT (litk == BITVECTOR_ULT || litk  == BITVECTOR_SLT
+                 || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT);
       return;
     }
     Kind ksc = sc.getKind();
@@ -147,46 +166,46 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     delete d_em;
   }
 
-  /* Generic sidec conditions for LT ---------------------------------------  */
+  /* Generic side conditions for LT ---------------------------------------  */
 
-  void testGetScBvUltTrue0()
+  void testGetScBvUltTrue()
   {
-    runTestPred(true, BITVECTOR_ULT, 0, getScBvUlt);
+    runTestPred(true, BITVECTOR_ULT, getScBvUltUgt);
   }
 
-  void testGetScBvUltTrue1()
+  void testGetScBvUltFalse()
   {
-    runTestPred(true, BITVECTOR_ULT, 1, getScBvUlt);
+    runTestPred(false, BITVECTOR_ULT, getScBvUltUgt);
   }
 
-  void testGetScBvUltFalse0()
+  void testGetScBvUgtTrue()
   {
-    runTestPred(false, BITVECTOR_ULT, 0, getScBvUlt);
+    runTestPred(true, BITVECTOR_UGT, getScBvUltUgt);
   }
 
-  void testGetScBvUltFalse1()
+  void testGetScBvUgtFalse()
   {
-    runTestPred(false, BITVECTOR_ULT, 1, getScBvUlt);
+    runTestPred(false, BITVECTOR_UGT, getScBvUltUgt);
   }
 
-  void testGetScBvSltTrue0()
+  void testGetScBvSltTrue()
   {
-    runTestPred(true, BITVECTOR_SLT, 0, getScBvSlt);
+    runTestPred(true, BITVECTOR_SLT, getScBvSltSgt);
   }
 
-  void testGetScBvSltTrue1()
+  void testGetScBvSltFalse()
   {
-    runTestPred(true, BITVECTOR_SLT, 1, getScBvSlt);
+    runTestPred(false, BITVECTOR_SLT, getScBvSltSgt);
   }
 
-  void testGetScBvSltFalse0()
+  void testGetScBvSgtTrue()
   {
-    runTestPred(false, BITVECTOR_SLT, 0, getScBvSlt);
+    runTestPred(true, BITVECTOR_SGT, getScBvSltSgt);
   }
 
-  void testGetScBvSltFalse1()
+  void testGetScBvSgtFalse()
   {
-    runTestPred(false, BITVECTOR_SLT, 1, getScBvSlt);
+    runTestPred(false, BITVECTOR_SGT, getScBvSltSgt);
   }
 
   /* Equality and Disequality ----------------------------------------------  */
@@ -390,6 +409,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_ULT, BITVECTOR_MULT, 1, getScBvMult);
   }
 
+  void testGetScBvMultUgtTrue0()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_MULT, 0, getScBvMult);
+  }
+
+  void testGetScBvMultUgtTrue1()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_MULT, 1, getScBvMult);
+  }
+
+  void testGetScBvMultUgtFalse0()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_MULT, 0, getScBvMult);
+  }
+
+  void testGetScBvMultUgtFalse1()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_MULT, 1, getScBvMult);
+  }
+
   void testGetScBvMultSltTrue0()
   {
     runTest(true, BITVECTOR_SLT, BITVECTOR_MULT, 0, getScBvMult);
@@ -410,6 +449,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_SLT, BITVECTOR_MULT, 1, getScBvMult);
   }
 
+  void testGetScBvMultSgtTrue0()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_MULT, 0, getScBvMult);
+  }
+
+  void testGetScBvMultSgtTrue1()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_MULT, 1, getScBvMult);
+  }
+
+  void testGetScBvMultSgtFalse0()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_MULT, 0, getScBvMult);
+  }
+
+  void testGetScBvMultSgtFalse1()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_MULT, 1, getScBvMult);
+  }
+
   /* Urem */
 
   void testGetScBvUremUltTrue0()
@@ -432,6 +491,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 1, getScBvUrem);
   }
 
+  void testGetScBvUremUgtTrue0()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 0, getScBvUrem);
+  }
+
+  void testGetScBvUremUgtTrue1()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 1, getScBvUrem);
+  }
+
+  void testGetScBvUremUgtFalse0()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 0, getScBvUrem);
+  }
+
+  void testGetScBvUremUgtFalse1()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 1, getScBvUrem);
+  }
+
   void testGetScBvUremSltTrue0()
   {
     runTest(true, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 0, getScBvUrem);
@@ -452,6 +531,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 1, getScBvUrem);
   }
 
+  void testGetScBvUremSgtTrue0()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 0, getScBvUrem);
+  }
+
+  void testGetScBvUremSgtTrue1()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 1, getScBvUrem);
+  }
+
+  void testGetScBvUremSgtFalse0()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 0, getScBvUrem);
+  }
+
+  void testGetScBvUremSgtFalse1()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 1, getScBvUrem);
+  }
+
   /* Udiv */
 
   void testGetScBvUdivUltTrue0()
@@ -474,6 +573,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv);
   }
 
+  void testGetScBvUdivUgtTrue0()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv);
+  }
+
+  void testGetScBvUdivUgtTrue1()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv);
+  }
+
+  void testGetScBvUdivUgtFalse0()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv);
+  }
+
+  void testGetScBvUdivUgtFalse1()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv);
+  }
+
   void testGetScBvUdivSltTrue0()
   {
     runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv);
@@ -494,6 +613,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv);
   }
 
+  void testGetScBvUdivSgtTrue0()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv);
+  }
+
+  void testGetScBvUdivSgtTrue1()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv);
+  }
+
+  void testGetScBvUdivSgtFalse0()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv);
+  }
+
+  void testGetScBvUdivSgtFalse1()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv);
+  }
+
   /* And */
 
   void testGetScBvAndUltTrue0()
@@ -516,6 +655,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_ULT, BITVECTOR_AND, 1, getScBvAndOr);
   }
 
+  void testGetScBvAndUgtTrue0()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_AND, 0, getScBvAndOr);
+  }
+
+  void testGetScBvAndUgtTrue1()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_AND, 1, getScBvAndOr);
+  }
+
+  void testGetScBvAndUgtFalse0()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_AND, 0, getScBvAndOr);
+  }
+
+  void testGetScBvAndUgtFalse1()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_AND, 1, getScBvAndOr);
+  }
+
   void testGetScBvAndSltTrue0()
   {
     runTest(true, BITVECTOR_SLT, BITVECTOR_AND, 0, getScBvAndOr);
@@ -536,6 +695,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_SLT, BITVECTOR_AND, 1, getScBvAndOr);
   }
 
+  void testGetScBvAndSgtTrue0()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_AND, 0, getScBvAndOr);
+  }
+
+  void testGetScBvAndSgtTrue1()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_AND, 1, getScBvAndOr);
+  }
+
+  void testGetScBvAndSgtFalse0()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_AND, 0, getScBvAndOr);
+  }
+
+  void testGetScBvAndSgtFalse1()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_AND, 1, getScBvAndOr);
+  }
+
   /* Or */
 
   void testGetScBvOrUltTrue0()
@@ -558,6 +737,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_ULT, BITVECTOR_OR, 1, getScBvAndOr);
   }
 
+  void testGetScBvOrUgtTrue0()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_OR, 0, getScBvAndOr);
+  }
+
+  void testGetScBvOrUgtTrue1()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_OR, 1, getScBvAndOr);
+  }
+
+  void testGetScBvOrUgtFalse0()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_OR, 0, getScBvAndOr);
+  }
+
+  void testGetScBvOrUgtFalse1()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_OR, 1, getScBvAndOr);
+  }
+
   void testGetScBvOrSltTrue0()
   {
     runTest(true, BITVECTOR_SLT, BITVECTOR_OR, 0, getScBvAndOr);
@@ -578,6 +777,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_SLT, BITVECTOR_OR, 1, getScBvAndOr);
   }
 
+  void testGetScBvOrSgtTrue0()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_OR, 0, getScBvAndOr);
+  }
+
+  void testGetScBvOrSgtTrue1()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_OR, 1, getScBvAndOr);
+  }
+
+  void testGetScBvOrSgtFalse0()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_OR, 0, getScBvAndOr);
+  }
+
+  void testGetScBvOrSgtFalse1()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_OR, 1, getScBvAndOr);
+  }
+
   /* Lshr */
 
   void testGetScBvLshrUltTrue0()
@@ -600,6 +819,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_ULT, BITVECTOR_LSHR, 1, getScBvLshr);
   }
 
+  void testGetScBvLshrUgtTrue0()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_LSHR, 0, getScBvLshr);
+  }
+
+  void testGetScBvLshrUgtTrue1()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_LSHR, 1, getScBvLshr);
+  }
+
+  void testGetScBvLshrUgtFalse0()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_LSHR, 0, getScBvLshr);
+  }
+
+  void testGetScBvLshrUgtFalse1()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_LSHR, 1, getScBvLshr);
+  }
+
   void testGetScBvLshrSltTrue0()
   {
     runTest(true, BITVECTOR_SLT, BITVECTOR_LSHR, 0, getScBvLshr);
@@ -620,6 +859,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_SLT, BITVECTOR_LSHR, 1, getScBvLshr);
   }
 
+  void testGetScBvLshrSgtTrue0()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_LSHR, 0, getScBvLshr);
+  }
+
+  void testGetScBvLshrSgtTrue1()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_LSHR, 1, getScBvLshr);
+  }
+
+  void testGetScBvLshrSgtFalse0()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_LSHR, 0, getScBvLshr);
+  }
+
+  void testGetScBvLshrSgtFalse1()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_LSHR, 1, getScBvLshr);
+  }
+
   /* Ashr */
 
   void testGetScBvAshrUltTrue0()
@@ -642,6 +901,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_ULT, BITVECTOR_ASHR, 1, getScBvAshr);
   }
 
+  void testGetScBvAshrUgtTrue0()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_ASHR, 0, getScBvAshr);
+  }
+
+  void testGetScBvAshrUgtTrue1()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_ASHR, 1, getScBvAshr);
+  }
+
+  void testGetScBvAshrUgtFalse0()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_ASHR, 0, getScBvAshr);
+  }
+
+  void testGetScBvAshrUgtFalse1()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_ASHR, 1, getScBvAshr);
+  }
+
   void testGetScBvAshrSltTrue0()
   {
     runTest(true, BITVECTOR_SLT, BITVECTOR_ASHR, 0, getScBvAshr);
@@ -662,6 +941,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_SLT, BITVECTOR_ASHR, 1, getScBvAshr);
   }
 
+  void testGetScBvAshrSgtTrue0()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_ASHR, 0, getScBvAshr);
+  }
+
+  void testGetScBvAshrSgtTrue1()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_ASHR, 1, getScBvAshr);
+  }
+
+  void testGetScBvAshrSgtFalse0()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_ASHR, 0, getScBvAshr);
+  }
+
+  void testGetScBvAshrSgtFalse1()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_ASHR, 1, getScBvAshr);
+  }
+
   /* Shl */
 
   void testGetScBvShlUltTrue0()
@@ -684,6 +983,26 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, BITVECTOR_ULT, BITVECTOR_SHL, 1, getScBvShl);
   }
 
+  void testGetScBvShlUgtTrue0()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_SHL, 0, getScBvShl);
+  }
+
+  void testGetScBvShlUgtTrue1()
+  {
+    runTest(true, BITVECTOR_UGT, BITVECTOR_SHL, 1, getScBvShl);
+  }
+
+  void testGetScBvShlUgtFalse0()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_SHL, 0, getScBvShl);
+  }
+
+  void testGetScBvShlUgtFalse1()
+  {
+    runTest(false, BITVECTOR_UGT, BITVECTOR_SHL, 1, getScBvShl);
+  }
+
   void testGetScBvShlSltTrue0()
   {
     runTest(true, BITVECTOR_SLT, BITVECTOR_SHL, 0, getScBvShl);
@@ -703,4 +1022,24 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
   {
     runTest(false, BITVECTOR_SLT, BITVECTOR_SHL, 1, getScBvShl);
   }
+
+  void testGetScBvShlSgtTrue0()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_SHL, 0, getScBvShl);
+  }
+
+  void testGetScBvShlSgtTrue1()
+  {
+    runTest(true, BITVECTOR_SGT, BITVECTOR_SHL, 1, getScBvShl);
+  }
+
+  void testGetScBvShlSgtFalse0()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_SHL, 0, getScBvShl);
+  }
+
+  void testGetScBvShlSgtFalse1()
+  {
+    runTest(false, BITVECTOR_SGT, BITVECTOR_SHL, 1, getScBvShl);
+  }
 };