Function term_is_sequence_value 

pub unsafe extern "C" fn term_is_sequence_value(term: Term) -> bool

Determine if a given term is a sequence value.

A term is a sequence value if it has kind #CVC5_KIND_CONST_SEQUENCE. In contrast to values for the set sort (as described in isSetValue()), a sequence value is represented as a Term with no children.

Semantically, a sequence value is a concatenation of unit sequences whose elements are themselves values. For example:

\verbatim embed:rst:leading-asterisk .. code:: smtlib

(seq.++ (seq.unit 0) (seq.unit 1))

\endverbatim

The above term has two representations in Term. One is as the sequence concatenation term:

\rst .. code:: lisp

(SEQ_CONCAT (SEQ_UNIT 0) (SEQ_UNIT 1))

\endrst

where 0 and 1 are the terms corresponding to the integer constants 0 and 1.

Alternatively, the above term is represented as the constant sequence value:

\rst .. code:: lisp

CONST_SEQUENCE_{0,1}

\endrst

where calling getSequenceValue() on the latter returns the vector {0, 1}.

The former term is not a sequence value, but the latter term is.

Constant sequences cannot be constructed directly via the API. They are returned in response to API calls such cvc5_get_value() and cvc5_simplify().

@param term The term. @return True if the term is a sequence value.