BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)

8 files changed, 22 insertions, 24 deletions

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 86444b8cf..fd204fffd 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -108,7 +108,7 @@ 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
+         || k == BITVECTOR_ADD || 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;
@@ -284,7 +284,7 @@ Node BvInverter::solveBvLit(Node sv,
     {
       t = nm->mkNode(k, t);
     }
-    else if (litk == EQUAL && k == BITVECTOR_PLUS)
+    else if (litk == EQUAL && k == BITVECTOR_ADD)
     {
       t = nm->mkNode(BITVECTOR_SUB, t, s);
     }
diff --git a/src/theory/quantifiers/bv_inverter_utils.cpp b/src/theory/quantifiers/bv_inverter_utils.cpp
index ff932cf15..e7427178a 100644
--- a/src/theory/quantifiers/bv_inverter_utils.cpp
+++ b/src/theory/quantifiers/bv_inverter_utils.cpp
@@ -327,7 +327,7 @@ Node getICBvUrem(
          *          (or (= t z) (distinct (bvsub s (_ bv1 w)) t))))
          * where
          * z = 0 with getSize(z) = w  */
-        Node add = nm->mkNode(BITVECTOR_PLUS, t, t);
+        Node add = nm->mkNode(BITVECTOR_ADD, t, t);
         Node sub = nm->mkNode(BITVECTOR_SUB, add, s);
         Node a = nm->mkNode(BITVECTOR_AND, sub, s);
         scl = nm->mkNode(BITVECTOR_UGE, a, t);
@@ -386,7 +386,7 @@ Node getICBvUrem(
          * (or
          *   (bvuge (bvand (bvsub (bvadd t t) s) s) t)  ; eq, synthesized
          *   (bvult t s))                               ; ugt, synthesized  */
-        Node add = nm->mkNode(BITVECTOR_PLUS, t, t);
+        Node add = nm->mkNode(BITVECTOR_ADD, t, t);
         Node sub = nm->mkNode(BITVECTOR_SUB, add, s);
         Node a = nm->mkNode(BITVECTOR_AND, sub, s);
         Node sceq = nm->mkNode(BITVECTOR_UGE, a, t);
@@ -1920,7 +1920,7 @@ Node getICBvShl(
          * min is the signed minimum value with getSize(min) = w  */
         Node min = bv::utils::mkMinSigned(w);
         Node shl = nm->mkNode(BITVECTOR_SHL, min, s);
-        Node add = nm->mkNode(BITVECTOR_PLUS, t, min);
+        Node add = nm->mkNode(BITVECTOR_ADD, t, min);
         scl = nm->mkNode(BITVECTOR_ULT, shl, add);
       }
       else
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index ec15b926f..9ffb31df3 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -184,7 +184,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
       Assert(slack.isConst());
       // remember the slack value for the asserted literal
       d_alit_to_model_slack[lit] = slack;
-      ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack));
+      ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_ADD, t, slack));
       Trace("cegqi-bv") << "Slack is " << slack << std::endl;
     }
     else
@@ -218,7 +218,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
     else
     {
       Node bv_one = bv::utils::mkOne(bv::utils::getSize(s));
-      ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t);
+      ret = nm->mkNode(BITVECTOR_ADD, s, bv_one).eqNode(t);
     }
   }
   Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl;
@@ -573,7 +573,7 @@ Node BvInstantiator::rewriteTermForSolvePv(
       return result;
     }
   }
-  else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS)
+  else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_ADD)
   {
     if (options::cegqiBvLinearize() && contains_pv[n])
     {
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
index 5040125ba..9825130e5 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
@@ -166,8 +166,8 @@ Node normalizePvPlus(Node pv,
                      std::unordered_map<Node, bool>& contains_pv)
 {
   NodeManager* nm;
-  NodeBuilder nb_c(BITVECTOR_PLUS);
-  NodeBuilder nb_l(BITVECTOR_PLUS);
+  NodeBuilder nb_c(BITVECTOR_ADD);
+  NodeBuilder nb_l(BITVECTOR_ADD);
   BvLinearAttribute is_linear;
   bool neg;
 
@@ -199,7 +199,7 @@ Node normalizePvPlus(Node pv,
       nb_c << coeff;
       continue;
     }
-    else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear))
+    else if (nc.getKind() == BITVECTOR_ADD && nc.getAttribute(is_linear))
     {
       Assert(isLinearPlus(nc, pv, contains_pv));
       Node coeff = utils::getPvCoeff(pv, nc[0]);
@@ -240,7 +240,7 @@ Node normalizePvPlus(Node pv,
     }
     else
     {
-      result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs);
+      result = nm->mkNode(BITVECTOR_ADD, pv_mult_coeffs, leafs);
       contains_pv[result] = true;
       result.setAttribute(is_linear, true);
     }
@@ -272,7 +272,7 @@ Node normalizePvEqual(Node pv,
     }
     if (child.getAttribute(is_linear) || child == pv)
     {
-      if (child.getKind() == BITVECTOR_PLUS)
+      if (child.getKind() == BITVECTOR_ADD)
       {
         Assert(isLinearPlus(child, pv, contains_pv));
         coeffs[i] = utils::getPvCoeff(pv, child[0]);
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
index 6be22805d..4c7c096b4 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
@@ -66,7 +66,7 @@ Node normalizePvMult(TNode pv,
                      std::unordered_map<Node, bool>& contains_pv);
 
 /**
- * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks
+ * Normalizes the children of a BITVECTOR_ADD w.r.t. pv. contains_pv marks
  * terms in which pv occurs.
  * For example,
  *
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 29194ff36..047318e86 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -131,9 +131,9 @@ class ExtendedRewriter
    * be treated as immutable. This is for instance to prevent propagation
    * beneath illegal terms. As an example:
    *   (bvand A (bvor A B)) is equivalent to (bvand A (bvor 1...1 B)), but
-   *   (bvand A (bvplus A B)) is not equivalent to (bvand A (bvplus 1..1 B)),
+   *   (bvand A (bvadd A B)) is not equivalent to (bvand A (bvadd 1..1 B)),
    * hence, when using this function to do BCP for bit-vectors, we have that
-   * BITVECTOR_AND is a bcp_kind, but BITVECTOR_PLUS is not.
+   * BITVECTOR_AND is a bcp_kind, but BITVECTOR_ADD is not.
    *
    * If this function returns a non-null node ret, then n ---> ret.
    */
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 263b36abf..7ee22dc5b 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -811,7 +811,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       std::vector<Kind> bin_kinds = {BITVECTOR_AND,
                                      BITVECTOR_OR,
                                      BITVECTOR_XOR,
-                                     BITVECTOR_PLUS,
+                                     BITVECTOR_ADD,
                                      BITVECTOR_SUB,
                                      BITVECTOR_MULT,
                                      BITVECTOR_UDIV,
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index b771db986..0c9cb91d7 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -287,7 +287,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry)
     }
   }
   return k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR
-         || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT
+         || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT
          || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
          || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT
          || k == UNION || k == INTERSECTION || k == JOIN || k == PRODUCT
@@ -304,7 +304,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry)
     }
   }
   return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND
-         || k == OR || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT
+         || k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT
          || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
          || k == BITVECTOR_XNOR || k == UNION || k == INTERSECTION
          || k == SEP_STAR;
@@ -389,7 +389,7 @@ Node TermUtil::mkTypeValueOffset(TypeNode tn,
     else if (tn.isBitVector())
     {
       val_o = Rewriter::rewrite(
-          NodeManager::currentNM()->mkNode(BITVECTOR_PLUS, val, offset_val));
+          NodeManager::currentNM()->mkNode(BITVECTOR_ADD, val, offset_val));
     }
   }
   return val_o;
@@ -443,10 +443,8 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
   TypeNode tn = n.getType();
   if (n == mkTypeValue(tn, 0))
   {
-    if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_PLUS
-        || ik == BITVECTOR_OR
-        || ik == BITVECTOR_XOR
-        || ik == STRING_CONCAT)
+    if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_ADD
+        || ik == BITVECTOR_OR || ik == BITVECTOR_XOR || ik == STRING_CONCAT)
     {
       return true;
     }