Remove partial UDIV/UREM operators. (#6069)

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

20 files changed, 74 insertions, 208 deletions

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<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 a1763d081..1e9db1597 100644
--- 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 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<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 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<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 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<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 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<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 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<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 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<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 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)))