Remove partial UDIV/UREM operators. (#6069)

This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 521ab98ea9b66fab379257c307dc67d5cf709420..9745673805aa3ad6241c7b563c6ca0a515390e05 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -433,8 +433,6 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {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 d8b309609f16b8753dd28bf04830c16da9267291..b743f580d3c32f24d59ecc035eba1c853eb222cd 100644 (file)
--- 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 5043718ca8b1055fc662e0e5fcb4e1cec9d3692f..6ca4a23ec8f42e8f2525f0f2c69a63b95c5df476 100644 (file)
--- 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<SgtEliminate>,
                                   RewriteRule<SgeEliminate>>::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 e50548ff8a8ab9ad2b85d7710ee9d1ddf89b2984..a7cc3663050158f8acc42c863db3a4224e29aa28 100644 (file)
--- 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 7ac2da40bce187f06df421ac7f91f7a6abc4b7ab..2733e9eefdd22ed4e1c61ca34156183f0d041e01 100644 (file)
--- 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 4f43431282612c4bef3efc947449c5837a40432b..a344964013423cdd3d204fb6eb38c19302efda08 100644 (file)
--- 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 8bab969c50d342cb9a85817f2062932f43f7a81b..2cc1b7e681d4dd4dda5eeba7fdc11c4d51df0e58 100644 (file)
--- 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<T>& q, TBitblaster<T>* 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<T> a, b;
   bb->bbTerm(node[0], a);
@@ -540,8 +540,8 @@ void DefaultUdivBB(TNode node, std::vector<T>& q, TBitblaster<T>* 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<T>& rem, TBitblaster<T>* 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<T> a, b;
   bb->bbTerm(node[0], a);
@@ -573,8 +573,8 @@ void DefaultUremBB(TNode node, std::vector<T>& rem, TBitblaster<T>* 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 a1763d081c383431dcf434c4c3738acc25445c67..1e9db15975db8508fcc8eb2bb1286626ca08bd39 100644 (file)
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -160,10 +160,8 @@ void TBitblaster<T>::initTermBBStrategies()
   d_termBBStrategies[kind::BITVECTOR_PLUS] = DefaultPlusBB<T>;
   d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB<T>;
   d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB<T>;
-  d_termBBStrategies[kind::BITVECTOR_UDIV] = UndefinedTermBBStrategy<T>;
-  d_termBBStrategies[kind::BITVECTOR_UREM] = UndefinedTermBBStrategy<T>;
-  d_termBBStrategies[kind::BITVECTOR_UDIV_TOTAL] = DefaultUdivBB<T>;
-  d_termBBStrategies[kind::BITVECTOR_UREM_TOTAL] = DefaultUremBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_UDIV] = DefaultUdivBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_UREM] = DefaultUremBB<T>;
   d_termBBStrategies[kind::BITVECTOR_SDIV] = UndefinedTermBBStrategy<T>;
   d_termBBStrategies[kind::BITVECTOR_SREM] = UndefinedTermBBStrategy<T>;
   d_termBBStrategies[kind::BITVECTOR_SMOD] = UndefinedTermBBStrategy<T>;

diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index 3cadac62155d0e6f9b84a2d384c86617aaf84604..fbf295a85621c2119817b8eb6fff69e4beb07b1c 100644 (file)
--- 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 e1230a56cbb99cd20548d3aa82087ca88eec9615..003e9dd1aff49b2a16f95c2ceb228d4af34daaa2 100644 (file)
--- 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 f9caf119af9eff9a11a485eaace2cf32da6f6194..32e0e9e85a1390008074a1ce4f0fb9cdf15f76ec 100644 (file)
--- 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 47974fc038839352eb07eb79c4a487210f7c9868..52bb55757e05abfdb95928828789a8c46f12e355 100644 (file)
--- 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 fafde0601d91cd8145a1c52430d052679101e905..685f25a92b61d08f230e45f9f156390e1a9f15a9 100644 (file)
--- 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<BVSolver> d_internal;
 
-  /**
-   * Maps from bit-vector width to division-by-zero uninterpreted
-   * function symbols.
-   */
-  std::unordered_map<unsigned, Node> d_ufDivByZero;
-  std::unordered_map<unsigned, Node> 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 dfcc4f052a7ddf904d5283180287252e8911a6f3..2334d96f202690ad0b5577b6d3cb732aa0cd0198 100644 (file)
--- 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<EvalNeg>::apply(TNode node) {
 }
 template<> inline
 bool RewriteRule<EvalUdiv>::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<EvalUdiv>::apply(TNode node) {
 }
 template<> inline
 bool RewriteRule<EvalUrem>::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 2fff03c104fead323a44e48be977bdb7a4c90894..dda5c042093a45b2e20862f949ef26172212cbb6 100644 (file)
--- 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<SdivEliminate>::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<SdivEliminateFewerBitwiseOps>::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<SremEliminate>::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<SremEliminateFewerBitwiseOps>::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 ca26577bf1d8618b2aeb101c3ea4f25c00bea661..d5a2300987a45a2433db7ad9c1080b24773af357 100644 (file)
--- 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<UdivPow2>::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<UdivPow2>::apply(TNode node)
 
 template <>
 inline bool RewriteRule<UdivZero>::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<UdivZero>::apply(TNode node) {
 
 template <>
 inline bool RewriteRule<UdivOne>::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<UremPow2>::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<UremPow2>::apply(TNode node)
 
 template<> inline
 bool RewriteRule<UremOne>::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<UremOne>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<UremSelf>::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<UgtUrem>::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 b883ab537438565aeb3408892cade426ca286ad8..4651b925690697fe0b85f7d83e1045e920975c7a 100644 (file)
--- 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<UdivPow2>::applies(node)) {
     resultNode = RewriteRule<UdivPow2>::run <false> (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<UremPow2>::applies(node)) {
@@ -477,7 +466,7 @@ RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite)
       RewriteRule<UremOne>,
       RewriteRule<UremSelf>
       >::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 e11f773a3c70ce1142e19fa8ae35bb7ae6c53d91..640d3309a4e2dda17d26a9e33fcbbcf679216899 100644 (file)
--- 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 8622ec483c387ccb070a42d7fb9d8d0866673003..8de1e5d3e2af5f55b6617bd5856d97ccce63665d 100644 (file)
--- 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 516fb1d05a36872280425309d093ce69f922806c..14ccbe9b72aa9dc607e74ee6dd8758699e16aa67 100644 (file)
--- 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 85871074652921730ca18de730b98a84b1afaf14..036e1c79801b02eb91be802a09776e33f58e15b3 100644 (file)
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -498,9 +498,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator/(
     const symbolicBitVector<isSigned> &op) const
 {
   return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
-      (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV_TOTAL,
-      *this,
-      op));
+      (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV, *this, op));
 }
 
 template <bool isSigned>
@@ -508,9 +506,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator%(
     const symbolicBitVector<isSigned> &op) const
 {
   return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
-      (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM_TOTAL,
-      *this,
-      op));
+      (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM, *this, op));
 }
 
 template <bool isSigned>

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 8d5e987800ed4fe962c84be8bc2ee7cd3eb95999..bf0765180b59a186be5abf91576ad9a2867589c1 100644 (file)
--- 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 0f1cdfadb2c275b17f2a936b980abadc8f68b56c..d7e035d83297f79574e8660994764e8ff165ed46 100644 (file)
--- 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 98a177f8695256053b3b7455afacd8b0eed18e14..3276b9ddec71a2dc8087598473e9d28af8e9bec3 100644 (file)
--- 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 33f74c7c4f1af4dc02646655c51799b6cedea954..63e54ff14a5daaa22f7ae7df11ac879eb542f514 100644 (file)
--- 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 c230c578cd23f45b7939327f2a78fd9bf1a2d64d..f6ebb628ac88c3fabf0985ce91bc76cb5f532e15 100644 (file)
--- 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 5e2e80e4aa59214dd54be3694ecfa96143e162e3..9ae4a7eac6f0e5fbb28e48e3fcd1875e09a0b741 100644 (file)
--- 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>(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>(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>(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>(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 b5996a68410d4f5fc8d144d3b508d834898b728c..fd740167f4d035404f96a8e73af68d08225a68d0 100644 (file)
--- 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 */