|
static term_type | not_ (const term_type &x) |
|
static void | make_not_ (term_type &result, const term_type &x) |
|
static term_type | and_ (const term_type &x, const term_type &y) |
|
static void | make_and_ (term_type &result, const term_type &x, const term_type &y) |
|
static term_type | or_ (const term_type &x, const term_type &y) |
|
static void | make_or_ (term_type &result, const term_type &x, const term_type &y) |
|
static term_type | imp (const term_type &x, const term_type &y) |
|
static void | make_imp (term_type &result, const term_type &x, const term_type &y) |
|
static void | make_forall (term_type &result, const variable_sequence_type &d, const term_type &x) |
|
static void | make_exists (term_type &result, const variable_sequence_type &d, const term_type &x) |
|
template<typename FwdIt > |
static term_type | join_or (FwdIt first, FwdIt last) |
|
template<typename FwdIt > |
static term_type | join_and (FwdIt first, FwdIt last) |
|
static term_type | true_ () |
| Make the value true.
|
|
static term_type | false_ () |
| Make the value false.
|
|
static term_type | not_ (const term_type &p) |
| Make a negation.
|
|
static void | make_not_ (term_type &result, const term_type &p) |
| Make a negation.
|
|
static term_type | and_ (const term_type &p, const term_type &q) |
| Make a conjunction.
|
|
static void | make_and_ (term_type &result, const term_type &p, const term_type &q) |
| Make a conjunction.
|
|
static term_type | or_ (const term_type &p, const term_type &q) |
| Make a disjunction.
|
|
static void | make_or_ (term_type &result, const term_type &p, const term_type &q) |
| Make a disjunction.
|
|
template<typename FwdIt > |
static term_type | join_or (FwdIt first, FwdIt last) |
|
template<typename FwdIt > |
static term_type | join_and (FwdIt first, FwdIt last) |
|
static term_type | imp (const term_type &p, const term_type &q) |
| Make an implication.
|
|
static void | make_imp (term_type &result, const term_type &p, const term_type &q) |
| Make an implication.
|
|
static term_type | forall (const variable_sequence_type &l, const term_type &p) |
| Make a universal quantification.
|
|
static void | make_forall (term_type &result, const variable_sequence_type &l, const term_type &p) |
| Make a universal quantification.
|
|
static term_type | exists (const variable_sequence_type &l, const term_type &p) |
| Make an existential quantification.
|
|
static void | make_exists (term_type &result, const variable_sequence_type &l, const term_type &p) |
| Make an existential quantification.
|
|
static bool | is_true (const term_type &t) |
| Test for the value true.
|
|
static bool | is_false (const term_type &t) |
| Test for the value false.
|
|
static bool | is_not (const term_type &t) |
| Test for a negation.
|
|
static bool | is_and (const term_type &t) |
| Test for a conjunction.
|
|
static bool | is_or (const term_type &t) |
| Test for a disjunction.
|
|
static bool | is_imp (const term_type &t) |
| Test for an implication.
|
|
static bool | is_forall (const term_type &t) |
| Test for an universal quantification.
|
|
static bool | is_exists (const term_type &t) |
| Test for an existential quantification.
|
|
static bool | is_data (const term_type &t) |
| Test for data term.
|
|
static bool | is_prop_var (const term_type &t) |
| Test for propositional variable instantiation.
|
|
static term_type | left (const term_type &t) |
| Returns the left argument of a term of type and, or or imp.
|
|
static term_type | right (const term_type &t) |
| Returns the right argument of a term of type and, or or imp.
|
|
static const term_type & | not_arg (const term_type &t) |
| Returns the argument of a term of type not.
|
|
static const variable_sequence_type & | var (const term_type &t) |
| Returns the quantifier variables of a quantifier expression.
|
|
static const string_type & | name (const term_type &t) |
| Returns the name of a propositional variable instantiation.
|
|
static const data_term_sequence_type & | param (const term_type &t) |
| Returns the parameter list of a propositional variable instantiation.
|
|
static const term_type & | variable2term (const variable_type &v) |
| Conversion from variable to term.
|
|
static bool | is_variable (const term_type &t) |
| Test if a term is a variable.
|
|
static std::string | pp (const term_type &t) |
| Pretty print function.
|
|
Contains type information for pbes expressions.
Definition at line 29 of file term_traits_optimized.h.