Each theory is a data structure containing an ordered collection of kinds, an ordered collection of operators whose domain and range is specified in terms of those kinds, and equations involving the operators. Currently, the equations can be associativity, commutativity, or identity axioms, and arbitrary equations are not allowed. We allow left-identity and right-identity axioms if a symbol is neither associative or commutative, however one-way identities are not allowed if the binary symbol is associative or commutative. Additionally, identity terms must be constants, and a binary operator may contain at most one identity.
If a programmer attempts to violate these constraints, an exception may be thrown, however this behavior should not be relied upon. The exception is only there to aid client debugging.
Iterators to kinds and operators returned by instances of this class are guaranteed to iterate over their elements in order. Due to the the implementation using reference counting and copy-on-write semantics, iterators are not guaranteed to remain valid after the theory is modified.
Definition at line 647 of file ta.hh.
Public Types | |
| typedef std::set< kind_t >::const_iterator | kind_iterator |
| Type of constant bidirectional iterator that is used to iterate through the kinds in a theory. | |
| typedef std::set< op_t >::const_iterator | op_iterator |
| Type of constant bidirectional iterator that is used to iterate through the operators in a theory. | |
Public Member Functions | |
| theory_t () | |
| Constructs an empty equational theory. | |
Friends | |
| class | axiom_set_proxy_t |
| const kind_iterator | add_kind (theory_t &theory, const kind_t &kind) |
| Adds kind to theory. | |
| const op_iterator | add_op (theory_t &theory, const op_t &op) |
| Adds operator to theory. | |
| void | set_axioms (theory_t &theory, const op_t &bin_op, const axiom_set_t &axioms) |
| Sets axioms for a binary operator. | |
| const axiom_set_t & | axioms (const theory_t &theory, const op_t &op) |
| Returns set of axioms for operator. | |
| theory_t::kind_iterator | kinds_begin (const theory_t &theory) |
| Returns iterator that points to first kind in the theory. | |
| theory_t::kind_iterator | kinds_end (const theory_t &theory) |
| Returns iterator that points one past the last kind in the theory. | |
| bool | member (const theory_t &theory, const kind_t &kind) |
| Returns true if kind is in the theory. | |
| bool | member (const theory_t &theory, const op_t &op) |
| Returns true if operator is in the theory. | |
| theory_t::op_iterator | ops_begin (const theory_t &theory) |
| Returns iterator that points to the first operator in the theory. | |
| theory_t::op_iterator | ops_end (const theory_t &theory) |
| Returns iterator that points one past the last operator in the theory. | |
| bool | operator== (const theory_t &x, const theory_t &y) |
| Returns true if two theories are equal. | |
| theory_t::op_iterator | id_contexts_begin (const theory_t &theory, const op_t &id_symbol) |
| Returns iterator that points to the first binary operator that has an identity id_symbol in the theory. | |
| theory_t::op_iterator | id_contexts_end (const theory_t &theory, const op_t &id_symbol) |
| Returns iterator that points one past the last binary operator that has an identity id_symbol in the theory. | |
Related Functions | |
| (Note that these are not member functions.) | |
| bool | operator!= (const theory_t &lhs, const theory_t &rhs) |
| Returns true if theories are not equal. | |
| std::ostream & | operator<< (std::ostream &o, const theory_t &theory) CETA_DSO_EXPORT |
| Writes theory representation to stream for debugging purposes. | |
|
|
Type of constant bidirectional iterator that is used to iterate through the kinds in a theory. Iterators may be invalidated if the automaton is modified. |
|
|
Type of constant bidirectional iterator that is used to iterate through the operators in a theory. Iterators may be invalidated if the automaton is modified. |
1.4.6