New C++ API: Rename Term::isConst() to Term::isValue(). (#5211)

6 files changed, 14 insertions, 14 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f19ee2bf7..ecec6f8c3 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1715,7 +1715,7 @@ Op Term::getOp() const
 
 bool Term::isNull() const { return isNullHelper(); }
 
-bool Term::isConst() const
+bool Term::isValue() const
 {
   CVC4_API_CHECK_NOT_NULL;
   return d_node->isConst();
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index c53d6f828..679f39750 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -958,11 +958,11 @@ class CVC4_PUBLIC Term
   bool isNull() const;
 
   /**
-   * Check if this is a Term representing a constant.
+   * Check if this is a Term representing a value.
    *
-   * @return true if a constant Term
+   * @return true if this is a Term representing a value
    */
-  bool isConst() const;
+  bool isValue() const;
 
   /**
    *  Return the base (element stored at all indices) of a constant array
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 987db9363..a9f2e3abc 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -330,7 +330,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint hasOp() except +
         Op getOp() except +
         bint isNull() except +
-        bint isConst() except +
+        bint isValue() except +
         Term getConstArrayBase() except +
         vector[Term] getConstSequenceElements() except +
         Term notTerm() except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index bf135dca2..deadc6849 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -1461,8 +1461,8 @@ cdef class Term:
     def isNull(self):
         return self.cterm.isNull()
 
-    def isConst(self):
-        return self.cterm.isConst()
+    def isValue(self):
+        return self.cterm.isValue()
 
     def getConstArrayBase(self):
         cdef Term term = Term(self.solver)
@@ -1515,7 +1515,7 @@ cdef class Term:
     def toPythonObj(self):
         '''
         Converts a constant value Term to a Python object.
-        Requires isConst to hold.
+        Requires isValue to hold.
 
         Currently supports:
           Boolean -- returns a Python bool
@@ -1527,7 +1527,7 @@ cdef class Term:
           String  -- returns a Python Unicode string
         '''
 
-        if not self.isConst():
+        if not self.isValue():
             raise RuntimeError("Cannot call toPythonObj on a non-const Term")
 
         string_repr = self.cterm.toString().decode()
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 6eb0924ac..292871d2a 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2177,7 +2177,7 @@ simpleTerm[CVC4::api::Term& f]
        * literals, we can use the push/pop scope. */
       /* PARSER_STATE->popScope(); */
       t = SOLVER->mkArraySort(t, t2);
-      if(!f.isConst()) {
+      if(!f.isValue()) {
         std::stringstream ss;
         ss << "expected constant term inside array constant, but found "
            << "nonconstant term" << std::endl
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 84e25c36b..b9b7de149 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1101,7 +1101,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       parseError("Too many arguments to array constant.");
     }
     api::Term constVal = args[0];
-    if (!constVal.isConst())
+    if (!constVal.isValue())
     {
       // To parse array constants taking reals whose values are specified by
       // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
@@ -1111,15 +1111,15 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       // like 5.0 which are converted to (/ 5 1) to distinguish them from
       // integer constants. We must ensure numerator and denominator are
       // constant and the denominator is non-zero.
-      if (constVal.getKind() == api::DIVISION && constVal[0].isConst()
-          && constVal[1].isConst()
+      if (constVal.getKind() == api::DIVISION && constVal[0].isValue()
+          && constVal[1].isValue()
           && !constVal[1].getExpr().getConst<Rational>().isZero())
       {
         std::stringstream sdiv;
         sdiv << constVal[0] << "/" << constVal[1];
         constVal = d_solver->mkReal(sdiv.str());
       }
-      if (!constVal.isConst())
+      if (!constVal.isValue())
       {
         std::stringstream ss;
         ss << "expected constant term inside array constant, but found "