Skip to main content

term_is_set_value

cvc5_sys

Function term_is_set_value 

Source 
pub unsafe extern "C" fn term_is_set_value(term: Term) -> bool
Expand description

Determine if a given term is a set value.

A term is a set value if it is considered to be a (canonical) constant set value. A canonical set value is one whose AST is:

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

(union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))

\endverbatim

where @f$c_1 … c_n@f$ are values ordered by id such that @f$c_1 > … > c_n@f$.

@note A universe set term (kind #CVC5_KIND_SET_UNIVERSE) is not considered to be a set value.

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