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:
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;
public:
/**
- * Constructor.
+ * Constructor for a null term.
*/
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
*/
*/
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
* (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,
/**
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 +
const_iterator begin() except +
const_iterator end() except +
bint isIntegerValue() except +
+ vector[Term] getSequenceValue() except +
cdef cppclass TermHashFunction:
TermHashFunction() except +
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)
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";
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):
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);
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)
projects / cvc5.git / commitdiff