ceta::axiom_set_t Class Reference

List of all members.

---

Detailed Description

Set of axioms for an operator in a theory.

This class is not constructable directly. Instead singleton sets can be constructed using none(), assoc(), comm(), left_id(), right_id(), id(), and then combined using operator|() and operator|=(). For example, the expression assoc() | comm() | id(c) constructs a set of axioms for an associative and commutative symbol with an identity c,

Definition at line 472 of file ta.hh.

Public Member Functions
axiom_set_t &	operator|= (const axiom_set_t &rhs)
	Adds attributes from rhs to these attributes.
Friends
bool	is_assoc (const axiom_set_t &axiom)
	Returns true if attributes contain associativity.
bool	is_comm (const axiom_set_t &axiom)
	Returns true if attributes contain commutativity.
id_type_t	id_type (const axiom_set_t &axiom)
	Returns type of identity for these attributes.
const boost::optional< op_t > &	id_symbol (const axiom_set_t &axiom)
	Returns identity for these attributes if there is one.
const axiom_set_t &	none ()
	Returns set containing no axioms.
const axiom_set_t &	assoc ()
	Returns set only containing associative axiom.
const axiom_set_t &	comm ()
	Returns set only containing commutativity axiom.
const axiom_set_t	left_id (const op_t &id)
	Returns set only containing left identity axiom.
const axiom_set_t	right_id (const op_t &id)
	Returns set only containing right identity axiom.
const axiom_set_t	id (const op_t &id)
	Returns set only containing left and right identity axioms.
Related Functions
(Note that these are not member functions.)
bool	operator== (const axiom_set_t &x, const axiom_set_t &y)
	Returns true if the two axiom sets are equal.
bool	operator!= (const axiom_set_t &x, const axiom_set_t &y)
	Returns true if the two axiom sets are not equal.
const axiom_set_t	operator| (const axiom_set_t &x, const axiom_set_t &y)
	Returns union of two axiom sets.
std::ostream &	operator<< (std::ostream &o, const axiom_set_t &axioms) CETA_DSO_EXPORT
	Writes axioms to stream for debugging purposes.

---

The documentation for this class was generated from the following file:

• ta.hh

---