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, 367 insertions, 28 deletions

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);
+  }
 };