From: Aina Niemetz Date: Wed, 7 Oct 2020 17:55:29 +0000 (-0700) Subject: New C++ API: Rename Term::isConst() to Term::isValue(). (#5211) X-Git-Tag: cvc5-1.0.0~2740 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a6817647ee9bae0df0f1922c0d521d7f100d0245;p=cvc5.git New C++ API: Rename Term::isConst() to Term::isValue(). (#5211) --- 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& 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& 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().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 7430104cc..9c25b584f 100644 --- 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 f8cd234ee..3ce08f6b8 100644 --- 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 59b122710..cb8ad944a 100644 --- 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