Renamed bv::utils::isBVGroundTerm to isBvConstTerm. (#1568)

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 b53f7bb082fd5d6922c0669044c848796ee74b36..503fe5157c5182215b0b2b84a37b3c1f67313444 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -31,7 +31,7 @@ bool RewriteRule<EvalAnd>::applies(TNode node) {
   Unreachable();
   return (node.getKind() == kind::BITVECTOR_AND &&
           node.getNumChildren() == 2 &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -50,7 +50,7 @@ bool RewriteRule<EvalOr>::applies(TNode node) {
   Unreachable();
   return (node.getKind() == kind::BITVECTOR_OR &&
           node.getNumChildren() == 2 &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -69,7 +69,7 @@ bool RewriteRule<EvalXor>::applies(TNode node) {
   Unreachable();
   return (node.getKind() == kind::BITVECTOR_XOR &&
           node.getNumChildren() == 2 &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -86,7 +86,7 @@ Node RewriteRule<EvalXor>::apply(TNode node) {
 // template<> inline
 // bool RewriteRule<EvalXnor>::applies(TNode node) {
 //   return (node.getKind() == kind::BITVECTOR_XNOR &&
-//           utils::isBVGroundTerm(node));
+//           utils::isBvConstTerm(node));
 // }
 
 // template<> inline
@@ -101,7 +101,7 @@ Node RewriteRule<EvalXor>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalNot>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NOT &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -115,7 +115,7 @@ Node RewriteRule<EvalNot>::apply(TNode node) {
 // template<> inline
 // bool RewriteRule<EvalComp>::applies(TNode node) {
 //   return (node.getKind() == kind::BITVECTOR_COMP &&
-//           utils::isBVGroundTerm(node));
+//           utils::isBvConstTerm(node));
 // }
 
 // template<> inline
@@ -136,7 +136,7 @@ Node RewriteRule<EvalNot>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalMult>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_MULT &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -153,7 +153,7 @@ Node RewriteRule<EvalMult>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalPlus>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_PLUS &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -170,7 +170,7 @@ Node RewriteRule<EvalPlus>::apply(TNode node) {
 // template<> inline
 // bool RewriteRule<EvalSub>::applies(TNode node) {
 //   return (node.getKind() == kind::BITVECTOR_SUB &&
-//           utils::isBVGroundTerm(node));
+//           utils::isBvConstTerm(node));
 // }
 
 // template<> inline
@@ -185,7 +185,7 @@ Node RewriteRule<EvalPlus>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalNeg>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NEG &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -198,7 +198,7 @@ Node RewriteRule<EvalNeg>::apply(TNode node) {
 }
 template<> inline
 bool RewriteRule<EvalUdiv>::applies(TNode node) {
-  return (utils::isBVGroundTerm(node) &&
+  return (utils::isBvConstTerm(node) &&
           (node.getKind() == kind::BITVECTOR_UDIV_TOTAL ||
            (node.getKind() == kind::BITVECTOR_UDIV && node[1].isConst())));
 }
@@ -214,7 +214,7 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) {
 }
 template<> inline
 bool RewriteRule<EvalUrem>::applies(TNode node) {
-  return (utils::isBVGroundTerm(node) &&
+  return (utils::isBvConstTerm(node) &&
           (node.getKind() == kind::BITVECTOR_UREM_TOTAL ||
            (node.getKind() == kind::BITVECTOR_UREM && node[1].isConst())));
 }
@@ -231,7 +231,7 @@ Node RewriteRule<EvalUrem>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalShl>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SHL &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -247,7 +247,7 @@ Node RewriteRule<EvalShl>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalLshr>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_LSHR &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -263,7 +263,7 @@ Node RewriteRule<EvalLshr>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalAshr>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ASHR &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -279,7 +279,7 @@ Node RewriteRule<EvalAshr>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalUlt>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULT &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -297,7 +297,7 @@ Node RewriteRule<EvalUlt>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalUltBv>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULTBV &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -315,7 +315,7 @@ Node RewriteRule<EvalUltBv>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalSlt>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SLT &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -334,7 +334,7 @@ Node RewriteRule<EvalSlt>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalSltBv>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SLTBV &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -354,7 +354,7 @@ template<> inline
 bool RewriteRule<EvalITEBv>::applies(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<EvalITEBv>::applies(" << node << ")" << std::endl;
   return (node.getKind() == kind::BITVECTOR_ITE &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -373,7 +373,7 @@ Node RewriteRule<EvalITEBv>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalUle>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULE &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -391,7 +391,7 @@ Node RewriteRule<EvalUle>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalSle>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SLE &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -409,7 +409,7 @@ Node RewriteRule<EvalSle>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalExtract>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -427,7 +427,7 @@ Node RewriteRule<EvalExtract>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalConcat>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_CONCAT &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -445,7 +445,7 @@ Node RewriteRule<EvalConcat>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalSignExtend>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -461,7 +461,7 @@ Node RewriteRule<EvalSignExtend>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalEquals>::applies(TNode node) {
   return (node.getKind() == kind::EQUAL &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline
@@ -479,7 +479,7 @@ Node RewriteRule<EvalEquals>::apply(TNode node) {
 template<> inline
 bool RewriteRule<EvalComp>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_COMP &&
-          utils::isBVGroundTerm(node));
+          utils::isBvConstTerm(node));
 }
 
 template<> inline

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index c514a25381ddba7501b5c0c8a5dd91715414a29b..da3822aa68d17b523d7b99b94b4d315e9dbc31b6 100644 (file)
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -117,7 +117,7 @@ unsigned isPow2Const(TNode node, bool& isNeg)
   return false;
 }
 
-bool isBVGroundTerm(TNode node)
+bool isBvConstTerm(TNode node)
 {
   if (node.getNumChildren() == 0)
   {

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 4554d371c602e719568d1ffe6014229abc71e1dd..6115a7e96a690103385c0fe8610f9d46b7be2769 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -81,9 +81,8 @@ bool isZero(TNode node);
  * c+1. Otherwise, this function returns 0. The flag isNeg is updated to
  * indicate whether node is negative.  */
 unsigned isPow2Const(TNode node, bool& isNeg);
-// TODO: need a better name, this is not technically a ground term
 /* Returns true if node or all of its children is const. */
-bool isBVGroundTerm(TNode node);
+bool isBvConstTerm(TNode node);
 /* Returns true if node is a predicate over bit-vector nodes. */
 bool isBVPredicate(TNode node);
 /* Returns true if given term is a THEORY_BV term.  */