From 59d9aad4839e64e0f6d6b57ff112c418ffbbe9fb Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 5 Mar 2021 19:28:19 -0800 Subject: [PATCH] Remove partial UDIV/UREM operators. (#6069) This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total. --- src/api/cvc4cpp.cpp | 2 - src/preprocessing/passes/bv_gauss.cpp | 4 +- src/preprocessing/passes/bv_to_int.cpp | 22 +---- .../passes/unconstrained_simplifier.cpp | 2 - src/printer/cvc/cvc_printer.cpp | 6 -- src/printer/smt2/smt2_printer.cpp | 8 +- .../bitblast/bitblast_strategies_template.h | 12 +-- src/theory/bv/bitblast/bitblaster.h | 6 +- src/theory/bv/bv_solver_lazy.cpp | 4 +- src/theory/bv/bv_subtheory_algebraic.cpp | 7 +- src/theory/bv/kinds | 9 +- src/theory/bv/theory_bv.cpp | 55 ------------ src/theory/bv/theory_bv.h | 15 ---- ...ory_bv_rewrite_rules_constant_evaluation.h | 8 +- ...ry_bv_rewrite_rules_operator_elimination.h | 8 +- .../theory_bv_rewrite_rules_simplification.h | 21 +++-- src/theory/bv/theory_bv_rewriter.cpp | 19 +--- src/theory/datatypes/sygus_datatype_utils.cpp | 10 +-- src/theory/datatypes/sygus_extension.cpp | 2 +- src/theory/evaluator.cpp | 36 ++------ src/theory/fp/fp_converter.cpp | 8 +- src/theory/quantifiers/bv_inverter.cpp | 12 +-- src/theory/quantifiers/bv_inverter_utils.cpp | 28 +++--- .../quantifiers/sygus/sygus_grammar_cons.cpp | 4 +- src/theory/quantifiers/term_util.cpp | 14 ++- src/theory/subs_minimize.cpp | 4 +- .../preprocessing/pass_bv_gauss_white.cpp | 62 ++++++------- .../theory_quantifiers_bv_inverter_white.cpp | 86 +++++++++---------- 28 files changed, 147 insertions(+), 327 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 521ab98ea..974567380 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -433,8 +433,6 @@ const static std::unordered_map {CVC4::Kind::BITVECTOR_SDIV, BITVECTOR_SDIV}, {CVC4::Kind::BITVECTOR_SREM, BITVECTOR_SREM}, {CVC4::Kind::BITVECTOR_SMOD, BITVECTOR_SMOD}, - {CVC4::Kind::BITVECTOR_UDIV_TOTAL, INTERNAL_KIND}, - {CVC4::Kind::BITVECTOR_UREM_TOTAL, INTERNAL_KIND}, {CVC4::Kind::BITVECTOR_SHL, BITVECTOR_SHL}, {CVC4::Kind::BITVECTOR_LSHR, BITVECTOR_LSHR}, {CVC4::Kind::BITVECTOR_ASHR, BITVECTOR_ASHR}, diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index d8b309609..b743f580d 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -164,7 +164,7 @@ unsigned BVGauss::getMinBwExpr(Node expr) break; } - case kind::BITVECTOR_UREM_TOTAL: + case kind::BITVECTOR_UREM: case kind::BITVECTOR_LSHR: case kind::BITVECTOR_ASHR: { @@ -213,7 +213,7 @@ unsigned BVGauss::getMinBwExpr(Node expr) default: { - /* BITVECTOR_UDIV_TOTAL (since x / 0 = -1) + /* BITVECTOR_UDIV (since x / 0 = -1) * BITVECTOR_NOT * BITVECTOR_NEG * BITVECTOR_SHL */ diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 5043718ca..6ca4a23ec 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -191,20 +191,6 @@ Node BVToInt::eliminationPass(Node n) RewriteRule, RewriteRule>::apply(current); - // expanding definitions of udiv and urem - if (k == kind::BITVECTOR_UDIV) - { - currentEliminated = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, - currentEliminated[0], - currentEliminated[1]); - } - else if (k == kind::BITVECTOR_UREM) - { - currentEliminated = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, - currentEliminated[0], - currentEliminated[1]); - } - // save in the cache d_eliminationCache[current] = currentEliminated; // also assign the eliminated now to itself to avoid revisiting. @@ -357,10 +343,6 @@ Node BVToInt::translateWithChildren(Node original, // The following variable will only be used in assertions. CVC4_UNUSED uint64_t originalNumChildren = original.getNumChildren(); Node returnNode; - // Assert that BITVECTOR_UDIV/UREM were replaced by their - // *_TOTAL versions - Assert(oldKind != kind::BITVECTOR_UDIV); - Assert(oldKind != kind::BITVECTOR_UREM); switch (oldKind) { case kind::BITVECTOR_PLUS: @@ -381,7 +363,7 @@ Node BVToInt::translateWithChildren(Node original, returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, mult, p2); break; } - case kind::BITVECTOR_UDIV_TOTAL: + case kind::BITVECTOR_UDIV: { uint64_t bvsize = original[0].getType().getBitVectorSize(); // we use an ITE for the case where the second operand is 0. @@ -395,7 +377,7 @@ Node BVToInt::translateWithChildren(Node original, divNode); break; } - case kind::BITVECTOR_UREM_TOTAL: + case kind::BITVECTOR_UREM: { // we use an ITE for the case where the second operand is 0. Node modNode = diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index e50548ff8..a7cc36630 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -364,8 +364,6 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::BITVECTOR_ASHR: case kind::BITVECTOR_UDIV: case kind::BITVECTOR_UREM: - case kind::BITVECTOR_UDIV_TOTAL: - case kind::BITVECTOR_UREM_TOTAL: case kind::BITVECTOR_SDIV: case kind::BITVECTOR_SREM: case kind::BITVECTOR_SMOD: diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 7ac2da40b..2733e9eef 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -663,15 +663,9 @@ void CvcPrinter::toStreamNode(std::ostream& out, case kind::BITVECTOR_UDIV: op << "BVUDIV"; break; - case kind::BITVECTOR_UDIV_TOTAL: - op << "BVUDIV_TOTAL"; - break; case kind::BITVECTOR_UREM: op << "BVUREM"; break; - case kind::BITVECTOR_UREM_TOTAL: - op << "BVUREM_TOTAL"; - break; case kind::BITVECTOR_SDIV: op << "BVSDIV"; break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 4f4343128..a34496401 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -741,10 +741,8 @@ void Smt2Printer::toStream(std::ostream& out, case kind::BITVECTOR_PLUS: out << "bvadd "; forceBinary = true; break; case kind::BITVECTOR_SUB: out << "bvsub "; break; case kind::BITVECTOR_NEG: out << "bvneg "; break; - case kind::BITVECTOR_UDIV: - case kind::BITVECTOR_UDIV_TOTAL: out << "bvudiv "; break; - case kind::BITVECTOR_UREM: - case kind::BITVECTOR_UREM_TOTAL: out << "bvurem "; break; + case kind::BITVECTOR_UDIV: out << "bvudiv "; break; + case kind::BITVECTOR_UREM: out << "bvurem "; break; case kind::BITVECTOR_SDIV: out << "bvsdiv "; break; case kind::BITVECTOR_SREM: out << "bvsrem "; break; case kind::BITVECTOR_SMOD: out << "bvsmod "; break; @@ -1144,9 +1142,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::BITVECTOR_PLUS: return "bvadd"; case kind::BITVECTOR_SUB: return "bvsub"; case kind::BITVECTOR_NEG: return "bvneg"; - case kind::BITVECTOR_UDIV_TOTAL: case kind::BITVECTOR_UDIV: return "bvudiv"; - case kind::BITVECTOR_UREM_TOTAL: case kind::BITVECTOR_UREM: return "bvurem"; case kind::BITVECTOR_SDIV: return "bvsdiv"; case kind::BITVECTOR_SREM: return "bvsrem"; diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h index 8bab969c5..2cc1b7e68 100644 --- a/src/theory/bv/bitblast/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -517,7 +517,7 @@ void DefaultUdivBB(TNode node, std::vector& q, TBitblaster* bb) { Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0); + Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0); std::vector a, b; bb->bbTerm(node[0], a); @@ -540,8 +540,8 @@ void DefaultUdivBB(TNode node, std::vector& q, TBitblaster* bb) } // cache the remainder in case we need it later - Node remainder = Rewriter::rewrite(NodeManager::currentNM()->mkNode( - kind::BITVECTOR_UREM_TOTAL, node[0], node[1])); + Node remainder = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_UREM, node[0], node[1])); bb->storeBBTerm(remainder, r); } @@ -550,7 +550,7 @@ void DefaultUremBB(TNode node, std::vector& rem, TBitblaster* bb) { Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0); + Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0); std::vector a, b; bb->bbTerm(node[0], a); @@ -573,8 +573,8 @@ void DefaultUremBB(TNode node, std::vector& rem, TBitblaster* bb) } // cache the quotient in case we need it later - Node quotient = Rewriter::rewrite(NodeManager::currentNM()->mkNode( - kind::BITVECTOR_UDIV_TOTAL, node[0], node[1])); + Node quotient = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_UDIV, node[0], node[1])); bb->storeBBTerm(quotient, q); } diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index a1763d081..1e9db1597 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -160,10 +160,8 @@ void TBitblaster::initTermBBStrategies() d_termBBStrategies[kind::BITVECTOR_PLUS] = DefaultPlusBB; d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB; d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB; - d_termBBStrategies[kind::BITVECTOR_UDIV] = UndefinedTermBBStrategy; - d_termBBStrategies[kind::BITVECTOR_UREM] = UndefinedTermBBStrategy; - d_termBBStrategies[kind::BITVECTOR_UDIV_TOTAL] = DefaultUdivBB; - d_termBBStrategies[kind::BITVECTOR_UREM_TOTAL] = DefaultUremBB; + d_termBBStrategies[kind::BITVECTOR_UDIV] = DefaultUdivBB; + d_termBBStrategies[kind::BITVECTOR_UREM] = DefaultUremBB; d_termBBStrategies[kind::BITVECTOR_SDIV] = UndefinedTermBBStrategy; d_termBBStrategies[kind::BITVECTOR_SREM] = UndefinedTermBBStrategy; d_termBBStrategies[kind::BITVECTOR_SMOD] = UndefinedTermBBStrategy; diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index 3cadac621..fbf295a85 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -208,7 +208,7 @@ void BVSolverLazy::checkForLemma(TNode fact) if (fact.getKind() == kind::EQUAL) { NodeManager* nm = NodeManager::currentNM(); - if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) + if (fact[0].getKind() == kind::BITVECTOR_UREM) { TNode urem = fact[0]; TNode result = fact[1]; @@ -220,7 +220,7 @@ void BVSolverLazy::checkForLemma(TNode fact) kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); lemma(split); } - if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) + if (fact[1].getKind() == kind::BITVECTOR_UREM) { TNode urem = fact[1]; TNode result = fact[0]; diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index e1230a56c..003e9dd1a 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -781,9 +781,10 @@ AlgebraicSolver::Statistics::~Statistics() { } bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) { - if (fact.getKind() == kind::BITVECTOR_MULT || - fact.getKind() == kind::BITVECTOR_UDIV_TOTAL || - fact.getKind() == kind::BITVECTOR_UREM_TOTAL) { + if (fact.getKind() == kind::BITVECTOR_MULT + || fact.getKind() == kind::BITVECTOR_UDIV + || fact.getKind() == kind::BITVECTOR_UREM) + { return true; } diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index f9caf119a..32e0e9e85 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -56,14 +56,12 @@ operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors" operator BITVECTOR_NEG 1 "unary negation of a bit-vector" operator BITVECTOR_PLUS 2: "addition of two or more bit-vectors" operator BITVECTOR_SUB 2 "subtraction of two bit-vectors" -operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0)" -operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0)" +operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)" +operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)" operator BITVECTOR_SDIV 2 "2's complement signed division" operator BITVECTOR_SMOD 2 "2's complement signed remainder (sign follows divisor)" operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)" # total division kinds -operator BITVECTOR_UDIV_TOTAL 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)" -operator BITVECTOR_UREM_TOTAL 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)" ## shift kinds operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)" @@ -183,9 +181,6 @@ typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -# total division kinds -typerule BITVECTOR_UDIV_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_UREM_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule ## shift kinds typerule BITVECTOR_ASHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 47974fc03..52bb55757 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -36,8 +36,6 @@ TheoryBV::TheoryBV(context::Context* c, std::string name) : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name), d_internal(nullptr), - d_ufDivByZero(), - d_ufRemByZero(), d_rewriter(), d_state(c, u, valuation), d_im(*this, d_state, nullptr, "theory::bv"), @@ -126,46 +124,6 @@ void TheoryBV::finishInit() } } -Node TheoryBV::getUFDivByZero(Kind k, unsigned width) -{ - NodeManager* nm = NodeManager::currentNM(); - if (k == kind::BITVECTOR_UDIV) - { - if (d_ufDivByZero.find(width) == d_ufDivByZero.end()) - { - // lazily create the function symbols - std::ostringstream os; - os << "BVUDivByZero_" << width; - Node divByZero = - nm->mkSkolem(os.str(), - nm->mkFunctionType(nm->mkBitVectorType(width), - nm->mkBitVectorType(width)), - "partial bvudiv", - NodeManager::SKOLEM_EXACT_NAME); - d_ufDivByZero[width] = divByZero; - } - return d_ufDivByZero[width]; - } - else if (k == kind::BITVECTOR_UREM) - { - if (d_ufRemByZero.find(width) == d_ufRemByZero.end()) - { - std::ostringstream os; - os << "BVURemByZero_" << width; - Node divByZero = - nm->mkSkolem(os.str(), - nm->mkFunctionType(nm->mkBitVectorType(width), - nm->mkBitVectorType(width)), - "partial bvurem", - NodeManager::SKOLEM_EXACT_NAME); - d_ufRemByZero[width] = divByZero; - } - return d_ufRemByZero[width]; - } - - Unreachable(); -} - TrustNode TheoryBV::expandDefinition(Node node) { Debug("bitvector-expandDefinition") @@ -180,19 +138,6 @@ TrustNode TheoryBV::expandDefinition(Node node) ret = TheoryBVRewriter::eliminateBVSDiv(node); break; - case kind::BITVECTOR_UDIV: - case kind::BITVECTOR_UREM: - { - NodeManager* nm = NodeManager::currentNM(); - - Kind kind = node.getKind() == kind::BITVECTOR_UDIV - ? kind::BITVECTOR_UDIV_TOTAL - : kind::BITVECTOR_UREM_TOTAL; - ret = nm->mkNode(kind, node[0], node[1]); - break; - } - break; - default: break; } if (!ret.isNull() && node != ret) diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index fafde0601..685f25a92 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -107,24 +107,9 @@ class TheoryBV : public Theory private: void notifySharedTerm(TNode t) override; - /** - * Return the UF symbol corresponding to division-by-zero for this particular - * bit-width. - * @param k should be UREM or UDIV - * @param width bit-width - */ - Node getUFDivByZero(Kind k, unsigned width); - /** Internal BV solver. */ std::unique_ptr d_internal; - /** - * Maps from bit-vector width to division-by-zero uninterpreted - * function symbols. - */ - std::unordered_map d_ufDivByZero; - std::unordered_map d_ufRemByZero; - /** The theory rewriter for this theory. */ TheoryBVRewriter d_rewriter; diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index dfcc4f052..2334d96f2 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -198,9 +198,7 @@ Node RewriteRule::apply(TNode node) { } template<> inline bool RewriteRule::applies(TNode node) { - return (utils::isBvConstTerm(node) && - (node.getKind() == kind::BITVECTOR_UDIV_TOTAL || - (node.getKind() == kind::BITVECTOR_UDIV && node[1].isConst()))); + return utils::isBvConstTerm(node) && node.getKind() == kind::BITVECTOR_UDIV; } template<> inline @@ -214,9 +212,7 @@ Node RewriteRule::apply(TNode node) { } template<> inline bool RewriteRule::applies(TNode node) { - return (utils::isBvConstTerm(node) && - (node.getKind() == kind::BITVECTOR_UREM_TOTAL || - (node.getKind() == kind::BITVECTOR_UREM && node[1].isConst()))); + return utils::isBvConstTerm(node) && node.getKind() == kind::BITVECTOR_UREM; } template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 2fff03c10..dda5c0420 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -464,7 +464,7 @@ inline Node RewriteRule::apply(TNode node) Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, abs_a, abs_b); + Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b); Node condition = nm->mkNode(kind::XOR, a_lt_0, b_lt_0); @@ -502,7 +502,7 @@ inline Node RewriteRule::apply(TNode node) Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, abs_a, abs_b); + Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b); Node result = nm->mkNode(kind::ITE, a_lt_0.xorNode(b_lt_0), neg_result, a_udiv_b); @@ -536,7 +536,7 @@ inline Node RewriteRule::apply(TNode node) Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM_TOTAL, abs_a, abs_b); + Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b); Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); @@ -571,7 +571,7 @@ inline Node RewriteRule::apply(TNode node) nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a); Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM_TOTAL, abs_a, abs_b); + Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b); Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index ca26577bf..d5a230098 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1393,7 +1393,7 @@ template <> inline bool RewriteRule::applies(TNode node) { bool isNeg = false; - if (node.getKind() == kind::BITVECTOR_UDIV_TOTAL + if (node.getKind() == kind::BITVECTOR_UDIV && utils::isPow2Const(node[1], isNeg)) { return !isNeg; @@ -1439,8 +1439,8 @@ inline Node RewriteRule::apply(TNode node) template <> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && - node[1] == utils::mkConst(utils::getSize(node), 0)); + return (node.getKind() == kind::BITVECTOR_UDIV + && node[1] == utils::mkConst(utils::getSize(node), 0)); } template <> @@ -1459,8 +1459,8 @@ inline Node RewriteRule::apply(TNode node) { template <> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && - node[1] == utils::mkConst(utils::getSize(node), 1)); + return (node.getKind() == kind::BITVECTOR_UDIV + && node[1] == utils::mkConst(utils::getSize(node), 1)); } template <> @@ -1481,7 +1481,7 @@ template <> inline bool RewriteRule::applies(TNode node) { bool isNeg; - if (node.getKind() == kind::BITVECTOR_UREM_TOTAL + if (node.getKind() == kind::BITVECTOR_UREM && utils::isPow2Const(node[1], isNeg)) { return !isNeg; @@ -1521,8 +1521,8 @@ inline Node RewriteRule::apply(TNode node) template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && - node[1] == utils::mkConst(utils::getSize(node), 1)); + return (node.getKind() == kind::BITVECTOR_UREM + && node[1] == utils::mkConst(utils::getSize(node), 1)); } template<> inline @@ -1541,8 +1541,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && - node[0] == node[1]); + return (node.getKind() == kind::BITVECTOR_UREM && node[0] == node[1]); } template<> inline @@ -1590,7 +1589,7 @@ template <> inline bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_UGT - && node[0].getKind() == kind::BITVECTOR_UREM_TOTAL + && node[0].getKind() == kind::BITVECTOR_UREM && node[0][1] == node[1]); } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index b883ab537..4651b9256 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -440,18 +440,6 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) { RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool prerewrite){ Node resultNode = node; - return RewriteUdivTotal(node, prerewrite); -} - -RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool prerewrite){ - Node resultNode = node; - - return RewriteUremTotal(node, prerewrite); -} - -RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){ - Node resultNode = node; - if(RewriteRule::applies(node)) { resultNode = RewriteRule::run (node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -464,7 +452,8 @@ RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){ return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite) { +RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool prerewrite) +{ Node resultNode = node; if(RewriteRule::applies(node)) { @@ -477,7 +466,7 @@ RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite) RewriteRule, RewriteRule >::apply(node); - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(REWRITE_DONE, resultNode); } RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool prerewrite) { @@ -705,8 +694,6 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_NEG ] = RewriteNeg; d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv; d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem; - d_rewriteTable [ kind::BITVECTOR_UDIV_TOTAL ] = RewriteUdivTotal; - d_rewriteTable [ kind::BITVECTOR_UREM_TOTAL ] = RewriteUremTotal; d_rewriteTable [ kind::BITVECTOR_SMOD ] = RewriteSmod; d_rewriteTable [ kind::BITVECTOR_SDIV ] = RewriteSdiv; d_rewriteTable [ kind::BITVECTOR_SREM ] = RewriteSrem; diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index e11f773a3..640d3309a 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -124,15 +124,7 @@ Kind getEliminateKind(Kind ok) Kind nk = ok; // We also must ensure that builtin operators which are eliminated // during expand definitions are replaced by the proper operator. - if (ok == BITVECTOR_UDIV) - { - nk = BITVECTOR_UDIV_TOTAL; - } - else if (ok == BITVECTOR_UREM) - { - nk = BITVECTOR_UREM_TOTAL; - } - else if (ok == DIVISION) + if (ok == DIVISION) { nk = DIVISION_TOTAL; } diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 8622ec483..8de1e5d3e 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -725,7 +725,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e, Node req_const; if (nk == GT || nk == LT || nk == XOR || nk == MINUS || nk == BITVECTOR_SUB || nk == BITVECTOR_XOR - || nk == BITVECTOR_UREM_TOTAL) + || nk == BITVECTOR_UREM) { // must have the zero element req_const = quantifiers::TermUtil::mkTypeValue(tnb, 0); diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 516fb1d05..14ccbe9b7 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -792,41 +792,17 @@ EvalResult Evaluator::evalInternal( break; } case kind::BITVECTOR_UDIV: - case kind::BITVECTOR_UDIV_TOTAL: { - if (currNodeVal.getKind() == kind::BITVECTOR_UDIV_TOTAL - || results[currNode[1]].d_bv.getValue() != 0) - { - BitVector res = results[currNode[0]].d_bv; - res = res.unsignedDivTotal(results[currNode[1]].d_bv); - results[currNode] = EvalResult(res); - } - else - { - results[currNode] = EvalResult(); - evalAsNode[currNode] = - needsReconstruct ? reconstruct(currNode, results, evalAsNode) - : currNodeVal; - } + BitVector res = results[currNode[0]].d_bv; + res = res.unsignedDivTotal(results[currNode[1]].d_bv); + results[currNode] = EvalResult(res); break; } case kind::BITVECTOR_UREM: - case kind::BITVECTOR_UREM_TOTAL: { - if (currNodeVal.getKind() == kind::BITVECTOR_UREM_TOTAL - || results[currNode[1]].d_bv.getValue() != 0) - { - BitVector res = results[currNode[0]].d_bv; - res = res.unsignedRemTotal(results[currNode[1]].d_bv); - results[currNode] = EvalResult(res); - } - else - { - results[currNode] = EvalResult(); - evalAsNode[currNode] = - needsReconstruct ? reconstruct(currNode, results, evalAsNode) - : currNodeVal; - } + BitVector res = results[currNode[0]].d_bv; + res = res.unsignedRemTotal(results[currNode[1]].d_bv); + results[currNode] = EvalResult(res); break; } diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 858710746..036e1c798 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -498,9 +498,7 @@ symbolicBitVector symbolicBitVector::operator/( const symbolicBitVector &op) const { return symbolicBitVector(NodeManager::currentNM()->mkNode( - (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV_TOTAL, - *this, - op)); + (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV, *this, op)); } template @@ -508,9 +506,7 @@ symbolicBitVector symbolicBitVector::operator%( const symbolicBitVector &op) const { return symbolicBitVector(NodeManager::currentNM()->mkNode( - (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM_TOTAL, - *this, - op)); + (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM, *this, op)); } template diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 8d5e98780..bf0765180 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -108,10 +108,10 @@ static bool isInvertible(Kind k, unsigned index) return k == NOT || k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == BITVECTOR_COMP || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == BITVECTOR_CONCAT || k == BITVECTOR_SIGN_EXTEND - || k == BITVECTOR_PLUS || k == BITVECTOR_MULT - || k == BITVECTOR_UREM_TOTAL || k == BITVECTOR_UDIV_TOTAL - || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR - || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR || k == BITVECTOR_SHL; + || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_UREM + || k == BITVECTOR_UDIV || k == BITVECTOR_AND || k == BITVECTOR_OR + || k == BITVECTOR_XOR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR + || k == BITVECTOR_SHL; } Node BvInverter::getPathToPv( @@ -314,11 +314,11 @@ Node BvInverter::solveBvLit(Node sv, { ic = utils::getICBvShl(pol, litk, k, index, x, s, t); } - else if (k == BITVECTOR_UREM_TOTAL) + else if (k == BITVECTOR_UREM) { ic = utils::getICBvUrem(pol, litk, k, index, x, s, t); } - else if (k == BITVECTOR_UDIV_TOTAL) + else if (k == BITVECTOR_UDIV) { ic = utils::getICBvUdiv(pol, litk, k, index, x, s, t); } diff --git a/src/theory/quantifiers/bv_inverter_utils.cpp b/src/theory/quantifiers/bv_inverter_utils.cpp index 0f1cdfadb..d7e035d83 100644 --- a/src/theory/quantifiers/bv_inverter_utils.cpp +++ b/src/theory/quantifiers/bv_inverter_utils.cpp @@ -278,7 +278,7 @@ Node getICBvMult( Node getICBvUrem( bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t) { - Assert(k == BITVECTOR_UREM_TOTAL); + Assert(k == BITVECTOR_UREM); Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); @@ -586,7 +586,7 @@ Node getICBvUrem( Node getICBvUdiv( bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t) { - Assert(k == BITVECTOR_UDIV_TOTAL); + Assert(k == BITVECTOR_UDIV); Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); @@ -618,7 +618,7 @@ Node getICBvUdiv( * umulo(s, t) is true if s * t produces and overflow * and z = 0 with getSize(z) = w */ Node mul = nm->mkNode(BITVECTOR_MULT, s, t); - Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, s); + Node div = nm->mkNode(BITVECTOR_UDIV, mul, s); scl = nm->mkNode(EQUAL, div, t); } else @@ -655,8 +655,8 @@ Node getICBvUdiv( * * where * z = 0 with getSize(z) = w */ - Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, s, t); - scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, s, div), t); + Node div = nm->mkNode(BITVECTOR_UDIV, s, t); + scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV, s, div), t); } else { @@ -701,7 +701,7 @@ Node getICBvUdiv( * with invertibility condition (synthesized): * (= (bvand (bvudiv (bvmul s t) t) s) s) */ Node mul = nm->mkNode(BITVECTOR_MULT, s, t); - Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, t); + Node div = nm->mkNode(BITVECTOR_UDIV, mul, t); scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_AND, div, s), s); } } @@ -739,7 +739,7 @@ Node getICBvUdiv( * where * ones = ~0 with getSize(ones) = w */ Node ones = bv::utils::mkOnes(w); - Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s); + Node div = nm->mkNode(BITVECTOR_UDIV, ones, s); scl = nm->mkNode(BITVECTOR_UGT, div, t); } else @@ -792,7 +792,7 @@ Node getICBvUdiv( * and min is the minimum signed value with getSize(min) = w */ Node min = bv::utils::mkMinSigned(w); Node sle = nm->mkNode(BITVECTOR_SLE, t, z); - Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, min, s); + Node div = nm->mkNode(BITVECTOR_UDIV, min, s); Node slt = nm->mkNode(BITVECTOR_SLT, div, t); scl = nm->mkNode(IMPLIES, sle, slt); } @@ -808,8 +808,8 @@ Node getICBvUdiv( * and max is the maximum signed value with getSize(max) = w */ Node max = bv::utils::mkMaxSigned(w); Node ones = bv::utils::mkOnes(w); - Node udiv1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s); - Node udiv2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, max, s); + Node udiv1 = nm->mkNode(BITVECTOR_UDIV, ones, s); + Node udiv2 = nm->mkNode(BITVECTOR_UDIV, max, s); Node sge1 = nm->mkNode(BITVECTOR_SGE, udiv1, t); Node sge2 = nm->mkNode(BITVECTOR_SGE, udiv2, t); scl = nm->mkNode(OR, sge1, sge2); @@ -877,9 +877,9 @@ Node getICBvUdiv( * and max is the maximum signed value with getSize(max) = w */ Node max = bv::utils::mkMaxSigned(w); Node ones = bv::utils::mkOnes(w); - Node div1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s); + Node div1 = nm->mkNode(BITVECTOR_UDIV, ones, s); Node sgt1 = nm->mkNode(BITVECTOR_SGT, div1, t); - Node div2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, max, s); + Node div2 = nm->mkNode(BITVECTOR_UDIV, max, s); Node sgt2 = nm->mkNode(BITVECTOR_SGT, div2, t); scl = nm->mkNode(OR, sgt1, sgt2); } @@ -894,11 +894,11 @@ Node getICBvUdiv( * z = 0 with getSize(z) = w * and min is the minimum signed value with getSize(min) = w */ Node mul = nm->mkNode(BITVECTOR_MULT, s, t); - Node div1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, s); + Node div1 = nm->mkNode(BITVECTOR_UDIV, mul, s); Node o1 = nm->mkNode(EQUAL, div1, t); Node min = bv::utils::mkMinSigned(w); Node sle = nm->mkNode(BITVECTOR_SLE, t, z); - Node div2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, min, s); + Node div2 = nm->mkNode(BITVECTOR_UDIV, min, s); Node slt = nm->mkNode(BITVECTOR_SLT, div2, t); Node o2 = nm->mkNode(IMPLIES, sle, slt); scl = nm->mkNode(OR, o1, o2); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 98a177f86..3276b9dde 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -817,8 +817,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( BITVECTOR_PLUS, BITVECTOR_SUB, BITVECTOR_MULT, - BITVECTOR_UDIV_TOTAL, - BITVECTOR_UREM_TOTAL, + BITVECTOR_UDIV, + BITVECTOR_UREM, BITVECTOR_SDIV, BITVECTOR_SREM, BITVECTOR_SHL, diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 33f74c7c4..63e54ff14 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -458,10 +458,8 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg) return true; } else if (ik == MINUS || ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR - || ik == BITVECTOR_ASHR - || ik == BITVECTOR_SUB - || ik == BITVECTOR_UREM - || ik == BITVECTOR_UREM_TOTAL) + || ik == BITVECTOR_ASHR || ik == BITVECTOR_SUB + || ik == BITVECTOR_UREM) { return arg == 1; } @@ -476,7 +474,6 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg) || ik == INTS_DIVISION_TOTAL || ik == INTS_MODULUS || ik == INTS_MODULUS_TOTAL - || ik == BITVECTOR_UDIV_TOTAL || ik == BITVECTOR_UDIV || ik == BITVECTOR_SDIV) { @@ -503,15 +500,14 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg) return n; } else if (ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR || ik == BITVECTOR_ASHR - || ik == BITVECTOR_UREM - || ik == BITVECTOR_UREM_TOTAL) + || ik == BITVECTOR_UREM) { if (arg == 0) { return n; } } - else if (ik == BITVECTOR_UDIV_TOTAL || ik == BITVECTOR_UDIV + else if (ik == BITVECTOR_UDIV || ik == BITVECTOR_UDIV || ik == BITVECTOR_SDIV) { if (arg == 0) @@ -554,7 +550,7 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg) } else if (n == mkTypeValue(tn, 1)) { - if (ik == BITVECTOR_UREM_TOTAL) + if (ik == BITVECTOR_UREM) { return mkTypeValue(tn, 0); } diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp index c230c578c..f6ebb628a 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -426,8 +426,8 @@ bool SubstitutionMinimize::isSingularArg(Node n, Kind k, unsigned arg) return true; } } - if (k == BITVECTOR_AND || k == BITVECTOR_MULT || k == BITVECTOR_UDIV_TOTAL - || k == BITVECTOR_UREM_TOTAL + if (k == BITVECTOR_AND || k == BITVECTOR_MULT || k == BITVECTOR_UDIV + || k == BITVECTOR_UREM || (arg == 0 && (k == BITVECTOR_SHL || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR))) 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 */ -- 2.30.2