From 59d9aad4839e64e0f6d6b57ff112c418ffbbe9fb Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 5 Mar 2021 19:28:19 -0800 Subject: Remove partial UDIV/UREM operators. (#6069) This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total. --- test/unit/preprocessing/pass_bv_gauss_white.cpp | 62 ++++++---------- .../theory_quantifiers_bv_inverter_white.cpp | 86 +++++++++++----------- 2 files changed, 67 insertions(+), 81 deletions(-) (limited to 'test/unit') diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index 5e2e80e4a..9ae4a7eac 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -960,7 +960,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2) d_x); Node y_mul_one = d_nodeManager->mkNode( kind::BITVECTOR_MULT, - d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, d_one, d_five), + d_nodeManager->mkNode(kind::BITVECTOR_UREM, d_one, d_five), d_y); Node z_mul_one = d_nodeManager->mkNode(kind::BITVECTOR_MULT, bv::utils::mkOne(32), d_z); @@ -989,7 +989,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2) Node x_mul_four = d_nodeManager->mkNode( kind::BITVECTOR_MULT, d_nodeManager->mkNode( - kind::BITVECTOR_UDIV_TOTAL, + kind::BITVECTOR_UDIV, d_nodeManager->mkNode( kind::BITVECTOR_PLUS, d_nodeManager->mkNode(kind::BITVECTOR_MULT, @@ -2193,11 +2193,11 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid1) * ------------------------------------------------------------------- */ Node n1 = d_nodeManager->mkNode( - kind::BITVECTOR_UDIV_TOTAL, + kind::BITVECTOR_UDIV, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_three, d_x), d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_two, d_y)); Node n2 = d_nodeManager->mkNode( - kind::BITVECTOR_UREM_TOTAL, + kind::BITVECTOR_UREM, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_two, d_x), d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_five, d_y)); @@ -2699,39 +2699,29 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw1) Node concat2x = bv::utils::mkConcat(bv::utils::mkZero(16), zext48x); ASSERT_EQ(BVGauss::getMinBwExpr(concat2x), 16); - Node udiv1p = - d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p); + Node udiv1p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p); ASSERT_EQ(BVGauss::getMinBwExpr(udiv1p), 1); - Node udiv1x = - d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x); + Node udiv1x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x); ASSERT_EQ(BVGauss::getMinBwExpr(udiv1x), 48); - Node udiv2p = - d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p8); + Node udiv2p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p8); ASSERT_EQ(BVGauss::getMinBwExpr(udiv2p), 1); - Node udiv2x = - d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x8); + Node udiv2x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x8); ASSERT_EQ(BVGauss::getMinBwExpr(udiv2x), 48); - Node urem1p = - d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p); + Node urem1p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p); ASSERT_EQ(BVGauss::getMinBwExpr(urem1p), 1); - Node urem1x = - d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x); + Node urem1x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x); ASSERT_EQ(BVGauss::getMinBwExpr(urem1x), 1); - Node urem2p = - d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p8); + Node urem2p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p8); ASSERT_EQ(BVGauss::getMinBwExpr(urem2p), 1); - Node urem2x = - d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x8); + Node urem2x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x8); ASSERT_EQ(BVGauss::getMinBwExpr(urem2x), 16); - Node urem3p = - d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p8, zext48p); + Node urem3p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p8, zext48p); ASSERT_EQ(BVGauss::getMinBwExpr(urem3p), 1); - Node urem3x = - d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x8, zext48x); + Node urem3x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x8, zext48x); ASSERT_EQ(BVGauss::getMinBwExpr(urem3x), 8); Node add1p = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, extp, extp); @@ -2806,11 +2796,11 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw3a) Node z = d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16)); Node zextop5 = d_nodeManager->mkConst(BitVectorZeroExtend(5)); - Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, x, y); + Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, x, y); Node zext1 = d_nodeManager->mkNode(zextop5, udiv1); Node ext1 = bv::utils::mkExtract(zext1, 4, 0); Node ext2 = bv::utils::mkExtract(z, 4, 0); - Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2); + Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2); Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2); ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5); } @@ -2822,11 +2812,11 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw3b) * ((_ extract 4 0) z))) */ Node zextop5 = d_nodeManager->mkConst(BitVectorZeroExtend(5)); - Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, d_x, d_y); + Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, d_x, d_y); Node zext1 = d_nodeManager->mkNode(zextop5, udiv1); Node ext1 = bv::utils::mkExtract(zext1, 4, 0); Node ext2 = bv::utils::mkExtract(d_z, 4, 0); - Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2); + Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2); Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2); ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5); } @@ -2848,19 +2838,17 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4a) Node zextop7 = d_nodeManager->mkConst(BitVectorZeroExtend(7)); - Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, x, y); + Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, x, y); Node zext1 = d_nodeManager->mkNode(zextop5, udiv1); Node ext1_1 = bv::utils::mkExtract(zext1, 4, 0); Node ext2_1 = bv::utils::mkExtract(z, 4, 0); - Node udiv2_1 = - d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_1, ext2_1); + Node udiv2_1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_1, ext2_1); Node zext2_1 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2_1); Node ext1_2 = bv::utils::mkExtract(zext1, 2, 0); Node ext2_2 = bv::utils::mkExtract(z, 2, 0); - Node udiv2_2 = - d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_2, ext2_2); + Node udiv2_2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_2, ext2_2); Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2); Node plus = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2); @@ -2882,19 +2870,17 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4b) Node zextop7 = d_nodeManager->mkConst(BitVectorZeroExtend(7)); - Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, d_x, d_y); + Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, d_x, d_y); Node zext1 = d_nodeManager->mkNode(zextop5, udiv1); Node ext1_1 = bv::utils::mkExtract(zext1, 4, 0); Node ext2_1 = bv::utils::mkExtract(d_z, 4, 0); - Node udiv2_1 = - d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_1, ext2_1); + Node udiv2_1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_1, ext2_1); Node zext2_1 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2_1); Node ext1_2 = bv::utils::mkExtract(zext1, 2, 0); Node ext2_2 = bv::utils::mkExtract(d_z, 2, 0); - Node udiv2_2 = - d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_2, ext2_2); + Node udiv2_2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_2, ext2_2); Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2); Node plus = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2); diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index b5996a684..fd740167f 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -99,15 +99,15 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit unsigned idx, Node (*getsc)(bool, Kind, Kind, unsigned, Node, Node, Node)) { - ASSERT_TRUE(k == BITVECTOR_MULT || k == BITVECTOR_UREM_TOTAL - || k == BITVECTOR_UDIV_TOTAL || k == BITVECTOR_AND + ASSERT_TRUE(k == BITVECTOR_MULT || k == BITVECTOR_UREM + || k == BITVECTOR_UDIV || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR || k == BITVECTOR_SHL); Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t); ASSERT_FALSE(sc.isNull()); Kind ksc = sc.getKind(); - ASSERT_TRUE((k == BITVECTOR_UDIV_TOTAL && idx == 1 && pol == false) + ASSERT_TRUE((k == BITVECTOR_UDIV && idx == 1 && pol == false) || (k == BITVECTOR_ASHR && idx == 0 && pol == false) || ksc == IMPLIES); Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue(); @@ -301,44 +301,44 @@ TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_eq_false1) TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_true0) { - runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getICBvUrem); + runTest(true, EQUAL, BITVECTOR_UREM, 0, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_true1) { - runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 1, getICBvUrem); + runTest(true, EQUAL, BITVECTOR_UREM, 1, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_false0) { - runTest(false, EQUAL, BITVECTOR_UREM_TOTAL, 0, getICBvUrem); + runTest(false, EQUAL, BITVECTOR_UREM, 0, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_false1) { - runTest(false, EQUAL, BITVECTOR_UREM_TOTAL, 1, getICBvUrem); + runTest(false, EQUAL, BITVECTOR_UREM, 1, getICBvUrem); } /* Udiv */ TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_true0) { - runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv); + runTest(true, EQUAL, BITVECTOR_UDIV, 0, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_true1) { - runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv); + runTest(true, EQUAL, BITVECTOR_UDIV, 1, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_false0) { - runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv); + runTest(false, EQUAL, BITVECTOR_UDIV, 0, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_false1) { - runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv); + runTest(false, EQUAL, BITVECTOR_UDIV, 1, getICBvUdiv); } /* And */ @@ -877,164 +877,164 @@ TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_sgt_false1) TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_true0) { - runTest(true, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem); + runTest(true, BITVECTOR_ULT, BITVECTOR_UREM, 0, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_true1) { - runTest(true, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem); + runTest(true, BITVECTOR_ULT, BITVECTOR_UREM, 1, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_false0) { - runTest(false, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem); + runTest(false, BITVECTOR_ULT, BITVECTOR_UREM, 0, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_false1) { - runTest(false, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem); + runTest(false, BITVECTOR_ULT, BITVECTOR_UREM, 1, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_true0) { - runTest(true, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem); + runTest(true, BITVECTOR_UGT, BITVECTOR_UREM, 0, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_true1) { - runTest(true, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem); + runTest(true, BITVECTOR_UGT, BITVECTOR_UREM, 1, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_false0) { - runTest(false, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem); + runTest(false, BITVECTOR_UGT, BITVECTOR_UREM, 0, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_false1) { - runTest(false, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem); + runTest(false, BITVECTOR_UGT, BITVECTOR_UREM, 1, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_true0) { - runTest(true, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem); + runTest(true, BITVECTOR_SLT, BITVECTOR_UREM, 0, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_true1) { - runTest(true, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem); + runTest(true, BITVECTOR_SLT, BITVECTOR_UREM, 1, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_false0) { - runTest(false, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem); + runTest(false, BITVECTOR_SLT, BITVECTOR_UREM, 0, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_false1) { - runTest(false, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem); + runTest(false, BITVECTOR_SLT, BITVECTOR_UREM, 1, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_true0) { - runTest(true, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem); + runTest(true, BITVECTOR_SGT, BITVECTOR_UREM, 0, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_true1) { - runTest(true, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem); + runTest(true, BITVECTOR_SGT, BITVECTOR_UREM, 1, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_false0) { - runTest(false, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem); + runTest(false, BITVECTOR_SGT, BITVECTOR_UREM, 0, getICBvUrem); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_false1) { - runTest(false, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem); + runTest(false, BITVECTOR_SGT, BITVECTOR_UREM, 1, getICBvUrem); } /* Udiv */ TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_true0) { - runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv); + runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV, 0, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_true1) { - runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv); + runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV, 1, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_false0) { - runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv); + runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV, 0, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_false1) { - runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv); + runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV, 1, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_true0) { - runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv); + runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV, 0, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_true1) { - runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv); + runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV, 1, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_false0) { - runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv); + runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV, 0, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_false1) { - runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv); + runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV, 1, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_true0) { - runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv); + runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV, 0, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_true1) { - runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv); + runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV, 1, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_false0) { - runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv); + runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV, 0, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_false1) { - runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv); + runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV, 1, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_true0) { - runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv); + runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV, 0, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_true1) { - runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv); + runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV, 1, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_false0) { - runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv); + runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV, 0, getICBvUdiv); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_false1) { - runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv); + runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV, 1, getICBvUdiv); } /* And */ -- cgit v1.2.3