From f8f8103229a9b84e944148985ebb05abed814619 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 2 Jan 2018 16:54:32 -0800 Subject: 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. --- src/theory/quantifiers/bv_inverter.cpp | 101 +++--- .../theory/theory_quantifiers_bv_inverter_white.h | 395 +++++++++++++++++++-- 2 files changed, 425 insertions(+), 71 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 s 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); + } }; -- cgit v1.2.3