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

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f19ee2bf7feabec7160500da63b89f7e7ded1865..ecec6f8c37af84a6f5274d5192140e2fbf3ae539 100644 (file)
--- 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 c53d6f828966bce13b87d7fc141c2b3aa77b7605..679f397507b2f25b9ef531dbb10882d9034031a8 100644 (file)
--- 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 987db93636aaa8aa05263d25964ac9542b6dde75..a9f2e3abc37edc730457415eacad768afcb2a357 100644 (file)
--- 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 bf135dca2093811f90b9606108a7aea5d7410ed6..deadc68493ea963262cab39eb2d5c89178014fc9 100644 (file)
--- 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 6eb0924acc6fe47b7c73101fae44b510af9a2e41..292871d2a92ce23af880a8ccf010fbd018fc3c46 100644 (file)
--- 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 84e25c36ba0514f11fbdcd22fd14951e44cb3d93..b9b7de1495675e8ee37c845fc49ee1d292841094 100644 (file)
--- 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 "

diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index 7430104cc1618c8997237361ce8f8db2570a90ee..9c25b584fbc6c86c9067f86bac7edede6343a921 100644 (file)
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -110,10 +110,10 @@ def test_is_const():
     x = solver.mkConst(intsort, 'x')
     xpone = solver.mkTerm(kinds.Plus, x, one)
     onepone = solver.mkTerm(kinds.Plus, one, one)
-    assert not x.isConst()
-    assert one.isConst()
-    assert not xpone.isConst()
-    assert not onepone.isConst()
+    assert not x.isValue()
+    assert one.isValue()
+    assert not xpone.isValue()
+    assert not onepone.isValue()
 
 def test_const_sequence_elements():
     solver = pycvc4.Solver()
@@ -121,7 +121,7 @@ def test_const_sequence_elements():
     seqsort = solver.mkSequenceSort(realsort)
     s = solver.mkEmptySequence(seqsort)
 
-    assert s.isConst()
+    assert s.isValue()
 
     assert s.getKind() == kinds.ConstSequence
     # empty sequence has zero elements

diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py
index f8cd234ee52b48084d5f18f9d1bcd6359a526aa4..3ce08f6b8d1c116b07ba2c18c4d5f167cd748b40 100644 (file)
--- a/test/unit/api/python/test_to_python_obj.py
+++ b/test/unit/api/python/test_to_python_obj.py
@@ -45,7 +45,7 @@ def testGetArray():
     stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(2), solver.mkReal(3))
     stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(4), solver.mkReal(5))
 
-    assert stores.isConst()
+    assert stores.isValue()
 
     array_dict = stores.toPythonObj()
 

diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index 59b122710ec7f36ca5f7c7aa7ad6eded46609334..cb8ad944a94dc84c88db73449fe4a08dc9acafad 100644 (file)
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -42,7 +42,7 @@ class TermBlack : public CxxTest::TestSuite
   void testTermCompare();
   void testTermChildren();
   void testSubstitute();
-  void testIsConst();
+  void testIsValue();
   void testConstArray();
   void testConstSequenceElements();
 
@@ -748,18 +748,18 @@ void TermBlack::testSubstitute()
   TS_ASSERT_THROWS(xpx.substitute(es, rs), CVC4ApiException&);
 }
 
-void TermBlack::testIsConst()
+void TermBlack::testIsValue()
 {
   Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
   Term one = d_solver.mkReal(1);
   Term xpone = d_solver.mkTerm(PLUS, x, one);
   Term onepone = d_solver.mkTerm(PLUS, one, one);
-  TS_ASSERT(!x.isConst());
-  TS_ASSERT(one.isConst());
-  TS_ASSERT(!xpone.isConst());
-  TS_ASSERT(!onepone.isConst());
+  TS_ASSERT(!x.isValue());
+  TS_ASSERT(one.isValue());
+  TS_ASSERT(!xpone.isValue());
+  TS_ASSERT(!onepone.isValue());
   Term tnull;
-  TS_ASSERT_THROWS(tnull.isConst(), CVC4ApiException&);
+  TS_ASSERT_THROWS(tnull.isValue(), CVC4ApiException&);
 }
 
 void TermBlack::testConstArray()
@@ -770,8 +770,8 @@ void TermBlack::testConstArray()
   Term one = d_solver.mkReal(1);
   Term constarr = d_solver.mkConstArray(arrsort, one);
 
-  TS_ASSERT(!a.isConst());
-  TS_ASSERT(constarr.isConst());
+  TS_ASSERT(!a.isValue());
+  TS_ASSERT(constarr.isValue());
 
   TS_ASSERT_EQUALS(constarr.getKind(), CONST_ARRAY);
   TS_ASSERT_EQUALS(constarr.getConstArrayBase(), one);
@@ -784,7 +784,7 @@ void TermBlack::testConstSequenceElements()
   Sort seqsort = d_solver.mkSequenceSort(realsort);
   Term s = d_solver.mkEmptySequence(seqsort);
 
-  TS_ASSERT(s.isConst());
+  TS_ASSERT(s.isValue());
 
   TS_ASSERT_EQUALS(s.getKind(), CONST_SEQUENCE);
   // empty sequence has zero elements