From c8b95a25e4e458aad19ef3891e7a09d3032d2ac0 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 28 Dec 2017 19:24:35 -0800 Subject: [PATCH] Add unit tests for side conditions for inequality for CBQI BV. (#1455) --- src/theory/quantifiers/bv_inverter.cpp | 2 +- .../theory_quantifiers_bv_inverter_white.h | 373 +++++++++++++++++- 2 files changed, 371 insertions(+), 4 deletions(-) diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index a970e3395..cdabaabb8 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -363,7 +363,7 @@ static Node getScBvUrem(bool pol, Node t) { Assert(k == BITVECTOR_UREM_TOTAL); - Assert(pol == false || idx == 1); + Assert(litk != EQUAL || pol == false || idx == 1); NodeManager* nm = NodeManager::currentNM(); diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index 5e1d404dc..48df04845 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -83,11 +83,20 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite || k == BITVECTOR_OR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR + || k == BITVECTOR_SHL); - Assert(k != BITVECTOR_UREM_TOTAL || pol == false || idx == 1); + 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 + // handling is implemented in getScBv* TS_ASSERT (litk != EQUAL || sc != Node::null()); + if (sc.isNull()) + { + TS_ASSERT (litk == BITVECTOR_ULT || litk == BITVECTOR_SLT); + return; + } Kind ksc = sc.getKind(); TS_ASSERT((k == BITVECTOR_UDIV_TOTAL && idx == 1 && pol == false) || (k == BITVECTOR_ASHR && idx == 0 && pol == false) @@ -140,6 +149,8 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite delete d_em; } + /* Generic sidec conditions for LT --------------------------------------- */ + void testGetScBvUltTrue0() { runTestPred(true, BITVECTOR_ULT, 0, getScBvUlt); @@ -180,6 +191,10 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite runTestPred(false, BITVECTOR_SLT, 1, getScBvSlt); } + /* Equality and Disequality ---------------------------------------------- */ + + /* Mult */ + void testGetScBvMultEqTrue0() { runTest(true, EQUAL, BITVECTOR_MULT, 0, getScBvMult); @@ -200,6 +215,8 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite runTest(false, EQUAL, BITVECTOR_MULT, 1, getScBvMult); } + /* Urem */ + void testGetScBvUremEqTrue0() { TS_ASSERT_THROWS(runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem), @@ -220,6 +237,8 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite { runTest(false, EQUAL, BITVECTOR_UREM_TOTAL, 1, getScBvUrem); } + + /* Udiv */ void testGetScBvUdivEqTrue0() { runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); @@ -230,16 +249,18 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); } - void testGetScBvUdivFalse0() + void testGetScBvUdivEqFalse0() { runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); } - void testGetScBvUdivFalse1() + void testGetScBvUdivEqFalse1() { runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); } + /* And */ + void testGetScBvAndEqTrue0() { runTest(true, EQUAL, BITVECTOR_AND, 0, getScBvAndOr); @@ -260,6 +281,8 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite runTest(false, EQUAL, BITVECTOR_AND, 1, getScBvAndOr); } + /* Or */ + void testGetScBvOrEqTrue0() { runTest(true, EQUAL, BITVECTOR_OR, 0, getScBvAndOr); @@ -280,6 +303,8 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite runTest(false, EQUAL, BITVECTOR_OR, 1, getScBvAndOr); } + /* Lshr */ + void testGetScBvLshrEqTrue0() { runTest(true, EQUAL, BITVECTOR_LSHR, 0, getScBvLshr); @@ -300,6 +325,8 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite runTest(false, EQUAL, BITVECTOR_LSHR, 1, getScBvLshr); } + /* Ashr */ + void testGetScBvAshrEqTrue0() { runTest(true, EQUAL, BITVECTOR_ASHR, 0, getScBvAshr); @@ -320,6 +347,8 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite runTest(false, EQUAL, BITVECTOR_ASHR, 1, getScBvAshr); } + /* Shl */ + void testGetScBvShlEqTrue0() { runTest(true, EQUAL, BITVECTOR_SHL, 0, getScBvShl); @@ -339,4 +368,342 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite { runTest(false, EQUAL, BITVECTOR_SHL, 1, getScBvShl); } + + /* Inequality ------------------------------------------------------------ */ + + /* Mult */ + + void testGetScBvMultUltTrue0() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_MULT, 0, getScBvMult); + } + + void testGetScBvMultUltTrue1() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_MULT, 1, getScBvMult); + } + + void testGetScBvMultUltFalse0() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_MULT, 0, getScBvMult); + } + + void testGetScBvMultUltFalse1() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_MULT, 1, getScBvMult); + } + + void testGetScBvMultSltTrue0() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_MULT, 0, getScBvMult); + } + + void testGetScBvMultSltTrue1() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_MULT, 1, getScBvMult); + } + + void testGetScBvMultSltFalse0() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_MULT, 0, getScBvMult); + } + + void testGetScBvMultSltFalse1() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_MULT, 1, getScBvMult); + } + + /* Urem */ + + void testGetScBvUremUltTrue0() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 0, getScBvUrem); + } + + void testGetScBvUremUltTrue1() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 1, getScBvUrem); + } + + void testGetScBvUremUltFalse0() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 0, getScBvUrem); + } + + void testGetScBvUremUltFalse1() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 1, getScBvUrem); + } + + void testGetScBvUremSltTrue0() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 0, getScBvUrem); + } + + void testGetScBvUremSltTrue1() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 1, getScBvUrem); + } + + void testGetScBvUremSltFalse0() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 0, getScBvUrem); + } + + void testGetScBvUremSltFalse1() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 1, getScBvUrem); + } + + /* Udiv */ + + void testGetScBvUdivUltTrue0() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); + } + + void testGetScBvUdivUltTrue1() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); + } + + void testGetScBvUdivUltFalse0() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); + } + + void testGetScBvUdivUltFalse1() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); + } + + void testGetScBvUdivSltTrue0() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); + } + + void testGetScBvUdivSltTrue1() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); + } + + void testGetScBvUdivSltFalse0() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); + } + + void testGetScBvUdivSltFalse1() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); + } + + /* And */ + + void testGetScBvAndUltTrue0() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_AND, 0, getScBvAndOr); + } + + void testGetScBvAndUltTrue1() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_AND, 1, getScBvAndOr); + } + + void testGetScBvAndUltFalse0() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_AND, 0, getScBvAndOr); + } + + void testGetScBvAndUltFalse1() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_AND, 1, getScBvAndOr); + } + + void testGetScBvAndSltTrue0() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_AND, 0, getScBvAndOr); + } + + void testGetScBvAndSltTrue1() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_AND, 1, getScBvAndOr); + } + + void testGetScBvAndSltFalse0() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_AND, 0, getScBvAndOr); + } + + void testGetScBvAndSltFalse1() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_AND, 1, getScBvAndOr); + } + + /* Or */ + + void testGetScBvOrUltTrue0() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_OR, 0, getScBvAndOr); + } + + void testGetScBvOrUltTrue1() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_OR, 1, getScBvAndOr); + } + + void testGetScBvOrUltFalse0() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_OR, 0, getScBvAndOr); + } + + void testGetScBvOrUltFalse1() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_OR, 1, getScBvAndOr); + } + + void testGetScBvOrSltTrue0() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_OR, 0, getScBvAndOr); + } + + void testGetScBvOrSltTrue1() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_OR, 1, getScBvAndOr); + } + + void testGetScBvOrSltFalse0() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_OR, 0, getScBvAndOr); + } + + void testGetScBvOrSltFalse1() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_OR, 1, getScBvAndOr); + } + + /* Lshr */ + + void testGetScBvLshrUltTrue0() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_LSHR, 0, getScBvLshr); + } + + void testGetScBvLshrUltTrue1() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_LSHR, 1, getScBvLshr); + } + + void testGetScBvLshrUltFalse0() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_LSHR, 0, getScBvLshr); + } + + void testGetScBvLshrUltFalse1() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_LSHR, 1, getScBvLshr); + } + + void testGetScBvLshrSltTrue0() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_LSHR, 0, getScBvLshr); + } + + void testGetScBvLshrSltTrue1() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_LSHR, 1, getScBvLshr); + } + + void testGetScBvLshrSltFalse0() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_LSHR, 0, getScBvLshr); + } + + void testGetScBvLshrSltFalse1() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_LSHR, 1, getScBvLshr); + } + + /* Ashr */ + + void testGetScBvAshrUltTrue0() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_ASHR, 0, getScBvAshr); + } + + void testGetScBvAshrUltTrue1() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_ASHR, 1, getScBvAshr); + } + + void testGetScBvAshrUltFalse0() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_ASHR, 0, getScBvAshr); + } + + void testGetScBvAshrUltFalse1() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_ASHR, 1, getScBvAshr); + } + + void testGetScBvAshrSltTrue0() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_ASHR, 0, getScBvAshr); + } + + void testGetScBvAshrSltTrue1() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_ASHR, 1, getScBvAshr); + } + + void testGetScBvAshrSltFalse0() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_ASHR, 0, getScBvAshr); + } + + void testGetScBvAshrSltFalse1() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_ASHR, 1, getScBvAshr); + } + + /* Shl */ + + void testGetScBvShlUltTrue0() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_SHL, 0, getScBvShl); + } + + void testGetScBvShlUltTrue1() + { + runTest(true, BITVECTOR_ULT, BITVECTOR_SHL, 1, getScBvShl); + } + + void testGetScBvShlUltFalse0() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_SHL, 0, getScBvShl); + } + + void testGetScBvShlUltFalse1() + { + runTest(false, BITVECTOR_ULT, BITVECTOR_SHL, 1, getScBvShl); + } + + void testGetScBvShlSltTrue0() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_SHL, 0, getScBvShl); + } + + void testGetScBvShlSltTrue1() + { + runTest(true, BITVECTOR_SLT, BITVECTOR_SHL, 1, getScBvShl); + } + + void testGetScBvShlSltFalse0() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_SHL, 0, getScBvShl); + } + + void testGetScBvShlSltFalse1() + { + runTest(false, BITVECTOR_SLT, BITVECTOR_SHL, 1, getScBvShl); + } }; -- 2.30.2