From: Gereon Kremer Date: Thu, 20 May 2021 14:29:17 +0000 (+0200) Subject: Minor improvements to the API (#6585) X-Git-Tag: cvc5-1.0.0~1725 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=777b1a5f2bbfec6040e292cc182f5ec5f48d03e5;p=cvc5.git Minor improvements to the API (#6585) This PR does some minor improvements to the API: - remove getConstSequenceElements(), use getSequenceValue() instead - improve documentation for Term --- diff --git a/docs/cpp/term.rst b/docs/cpp/term.rst index 022c570b5..1f112a58a 100644 --- a/docs/cpp/term.rst +++ b/docs/cpp/term.rst @@ -1,6 +1,13 @@ Term ==== +The :cpp:class:`Term ` class represents arbitrary expressions that are Boolean or from some of the supported theories. The list of all supported types (or kinds) is given by the :cpp:enum:`Kind ` enum. +The :cpp:class:`Term ` class provides methods for general inspection (e.g., comparison, retrieve the kind and sort, access sub-terms), but also methods to retrieving constant values for the supported theories (i.e., :code:`isValue()` and :code:`getValue()`, which returns the constant values in the best type standard C++ offers). + +Additionally, a :cpp:class:`Term ` can be hashed (using :cpp:class:`std::hash\`) and given to output streams, including terms within standard containers like :code:`std::map`, :code:`std::set`, or :code:`std::vector`. + +The :cpp:class:`Term ` only offers the default constructor to create a null term. Instead, the :cpp:class:`Solver ` class provides factory functions for all other terms, e.g., :code:`Solver::mkTerm()` for generic terms and :code:`Solver::mk()` for constant values of a given type. + .. doxygenclass:: cvc5::api::Term :project: cvc5 :members: diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index d7959c950..ed35659f0 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -2309,25 +2309,6 @@ bool Term::isNull() const CVC5_API_TRY_CATCH_END; } -std::vector Term::getConstSequenceElements() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(d_node->getKind() == cvc5::Kind::CONST_SEQUENCE) - << "Expecting a CONST_SEQUENCE Term when calling " - "getConstSequenceElements()"; - //////// all checks before this line - const std::vector& elems = d_node->getConst().getVec(); - std::vector terms; - for (const Node& t : elems) - { - terms.push_back(Term(d_solver, t)); - } - return terms; - //////// - CVC5_API_TRY_CATCH_END; -} - Term Term::notTerm() const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 42d162e18..f77869c2c 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -945,7 +945,7 @@ class CVC5_EXPORT Term public: /** - * Constructor. + * Constructor for a null term. */ Term(); @@ -973,28 +973,28 @@ class CVC5_EXPORT Term bool operator!=(const Term& t) const; /** - * Comparison for ordering on terms. + * Comparison for ordering on terms by their id. * @param t the term to compare to * @return true if this term is less than t */ bool operator<(const Term& t) const; /** - * Comparison for ordering on terms. + * Comparison for ordering on terms by their id. * @param t the term to compare to * @return true if this term is greater than t */ bool operator>(const Term& t) const; /** - * Comparison for ordering on terms. + * Comparison for ordering on terms by their id. * @param t the term to compare to * @return true if this term is less than or equal to t */ bool operator<=(const Term& t) const; /** - * Comparison for ordering on terms. + * Comparison for ordering on terms by their id. * @param t the term to compare to * @return true if this term is greater than or equal to t */ @@ -1053,13 +1053,6 @@ class CVC5_EXPORT Term */ bool isNull() const; - /** - * Return the elements of a constant sequence - * throws an exception if the kind is not CONST_SEQUENCE - * @return the elements of the constant sequence. - */ - std::vector getConstSequenceElements() const; - /** * Boolean negation. * @return the Boolean negation of this term diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 0375b5e60..cad029b72 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -3200,7 +3200,7 @@ enum CVC5_EXPORT Kind : int32_t * (seq.++ (seq.unit c1) ... (seq.unit cn)) * * where n>=0 and c1, ..., cn are constants of some sort. The elements - * can be extracted by `Term::getConstSequenceElements()`. + * can be extracted by `Term::getSequenceValue()`. */ CONST_SEQUENCE, /** diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 24f8ac0a0..6fbc5ab57 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -359,7 +359,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Op getOp() except + bint isNull() except + Term getConstArrayBase() except + - vector[Term] getConstSequenceElements() except + Term notTerm() except + Term andTerm(const Term& t) except + Term orTerm(const Term& t) except + @@ -377,6 +376,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": const_iterator begin() except + const_iterator end() except + bint isIntegerValue() except + + vector[Term] getSequenceValue() except + cdef cppclass TermHashFunction: TermHashFunction() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 6d197168d..cd643d3f3 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1550,9 +1550,9 @@ cdef class Term: term.cterm = self.cterm.getConstArrayBase() return term - def getConstSequenceElements(self): + def getSequenceValue(self): elems = [] - for e in self.cterm.getConstSequenceElements(): + for e in self.cterm.getSequenceValue(): term = Term(self.solver) term.cterm = e elems.append(term) diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index d57ec0c9a..eb952f8db 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -548,7 +548,7 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) ss << "Type ascription on empty sequence must be a sequence, got " << s; parseError(ss.str()); } - if (!t.getConstSequenceElements().empty()) + if (!t.getSequenceValue().empty()) { std::stringstream ss; ss << "Cannot apply a type ascription to a non-empty sequence"; diff --git a/test/python/unit/api/test_term.py b/test/python/unit/api/test_term.py index 702634807..936ff3e1c 100644 --- a/test/python/unit/api/test_term.py +++ b/test/python/unit/api/test_term.py @@ -1003,14 +1003,14 @@ def test_const_sequence_elements(solver): assert s.getKind() == kinds.ConstSequence # empty sequence has zero elements - cs = s.getConstSequenceElements() + cs = s.getSequenceValue() assert len(cs) == 0 # A seq.unit app is not a constant sequence (regardless of whether it is # applied to a constant). su = solver.mkTerm(kinds.SeqUnit, solver.mkReal(1)) with pytest.raises(RuntimeError): - su.getConstSequenceElements() + su.getSequenceValue() def test_term_scoped_to_string(solver): diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index 50ef8bf0f..d7f9a4dc3 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -1077,7 +1077,7 @@ TEST_F(TestApiBlackTerm, constArray) d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5)); } -TEST_F(TestApiBlackTerm, constSequenceElements) +TEST_F(TestApiBlackTerm, getSequenceValue) { Sort realsort = d_solver.getRealSort(); Sort seqsort = d_solver.mkSequenceSort(realsort); @@ -1085,13 +1085,13 @@ TEST_F(TestApiBlackTerm, constSequenceElements) ASSERT_EQ(s.getKind(), CONST_SEQUENCE); // empty sequence has zero elements - std::vector cs = s.getConstSequenceElements(); + std::vector cs = s.getSequenceValue(); ASSERT_TRUE(cs.empty()); // A seq.unit app is not a constant sequence (regardless of whether it is // applied to a constant). Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1)); - ASSERT_THROW(su.getConstSequenceElements(), CVC5ApiException); + ASSERT_THROW(su.getSequenceValue(), CVC5ApiException); } TEST_F(TestApiBlackTerm, termScopedToString)