summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--docs/cpp/term.rst7
-rw-r--r--src/api/cpp/cvc5.cpp19
-rw-r--r--src/api/cpp/cvc5.h17
-rw-r--r--src/api/cpp/cvc5_kind.h2
-rw-r--r--src/api/python/cvc5.pxd2
-rw-r--r--src/api/python/cvc5.pxi4
-rw-r--r--src/parser/parser.cpp2
-rw-r--r--test/python/unit/api/test_term.py4
-rw-r--r--test/unit/api/term_black.cpp6
9 files changed, 22 insertions, 41 deletions
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 <cvc5::api::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 <cvc5::api::Kind>` enum.
+The :cpp:class:`Term <cvc5::api::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:`is<Type>Value()` and :code:`get<Type>Value()`, which returns the constant values in the best type standard C++ offers).
+
+Additionally, a :cpp:class:`Term <cvc5::api::Term>` can be hashed (using :cpp:class:`std::hash\<cvc5::api::Term>`) 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 <cvc5::api::Term>` only offers the default constructor to create a null term. Instead, the :cpp:class:`Solver <cvc5::api::Solver>` class provides factory functions for all other terms, e.g., :code:`Solver::mkTerm()` for generic terms and :code:`Solver::mk<Type>()` 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> 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<Node>& elems = d_node->getConst<Sequence>().getVec();
- std::vector<Term> 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
*/
@@ -1054,13 +1054,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<Term> 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<Term> cs = s.getConstSequenceElements();
+ std::vector<Term> 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback