cvc4-1.3
|
Class encapsulating CVC4 expressions and methods for constructing new expressions. More...
#include <expr.h>
Data Structures | |
class | const_iterator |
Iterator type for the children of an Expr. More... | |
Public Types | |
typedef expr::ExprSetDepth | setdepth |
IOStream manipulator to set the maximum depth of Exprs when pretty-printing. More... | |
typedef expr::ExprPrintTypes | printtypes |
IOStream manipulator to print type ascriptions or not. More... | |
typedef expr::ExprDag | dag |
IOStream manipulator to print expressions as a DAG (or not). More... | |
typedef expr::ExprSetLanguage | setlanguage |
IOStream manipulator to set the output language for Exprs. More... | |
Public Member Functions | |
Expr () | |
Default constructor, makes a null expression. More... | |
Expr (const Expr &e) | |
Copy constructor, makes a copy of a given expression. More... | |
~Expr () | |
Destructor. More... | |
Expr & | operator= (const Expr &e) |
Assignment operator, makes a copy of the given expression. More... | |
bool | operator== (const Expr &e) const |
Syntactic comparison operator. More... | |
bool | operator!= (const Expr &e) const |
Syntactic disequality operator. More... | |
bool | operator< (const Expr &e) const |
Order comparison operator. More... | |
bool | operator> (const Expr &e) const |
Order comparison operator. More... | |
bool | operator<= (const Expr &e) const |
Order comparison operator. More... | |
bool | operator>= (const Expr &e) const |
Order comparison operator. More... | |
unsigned long | getId () const |
Get the ID of this expression (used for the comparison operators). More... | |
Kind | getKind () const |
Returns the kind of the expression (AND, PLUS ...). More... | |
size_t | getNumChildren () const |
Returns the number of children of this expression. More... | |
Expr | operator[] (unsigned i) const |
Returns the i'th child of this expression. More... | |
std::vector< Expr > | getChildren () const |
Returns the children of this Expr. More... | |
Expr | notExpr () const |
Returns the Boolean negation of this Expr. More... | |
Expr | andExpr (const Expr &e) const |
Returns the conjunction of this expression and the given expression. More... | |
Expr | orExpr (const Expr &e) const |
Returns the disjunction of this expression and the given expression. More... | |
Expr | xorExpr (const Expr &e) const |
Returns the exclusive disjunction of this expression and the given expression. More... | |
Expr | iffExpr (const Expr &e) const |
Returns the Boolean equivalence of this expression and the given expression. More... | |
Expr | impExpr (const Expr &e) const |
Returns the implication of this expression and the given expression. More... | |
Expr | iteExpr (const Expr &then_e, const Expr &else_e) const |
Returns the if-then-else expression with this expression as the Boolean condition and the given expressions as the "then" and "else" expressions. More... | |
const_iterator | begin () const |
Returns an iterator to the first child of this Expr. More... | |
const_iterator | end () const |
Returns an iterator to one-off-the-last child of this Expr. More... | |
bool | hasOperator () const |
Check if this is an expression that has an operator. More... | |
Expr | getOperator () const |
Get the operator of this expression. More... | |
Type | getType (bool check=false) const throw (TypeCheckingException) |
Get the type for this Expr and optionally do type checking. More... | |
Expr | substitute (Expr e, Expr replacement) const |
Substitute "replacement" in for "e". More... | |
Expr | substitute (const std::vector< Expr > exes, const std::vector< Expr > &replacements) const |
Substitute "replacements" in for "exes". More... | |
Expr | substitute (const std::hash_map< Expr, Expr, ExprHashFunction > map) const |
Substitute pairs of (ex,replacement) from the given map. More... | |
std::string | toString () const |
Returns the string representation of the expression. More... | |
void | toStream (std::ostream &out, int toDepth=-1, bool types=false, size_t dag=1, OutputLanguage language=language::output::LANG_AST) const |
Outputs the string representation of the expression to the stream. More... | |
bool | isNull () const |
Check if this is a null expression. More... | |
bool | isVariable () const |
Check if this is an expression representing a variable. More... | |
bool | isConst () const |
Check if this is an expression representing a constant. More... | |
template<class T > | |
const T & | getConst () const |
Extract a constant of type T. More... | |
ExprManager * | getExprManager () const |
Returns the expression reponsible for this expression. More... | |
Expr | exportTo (ExprManager *exprManager, ExprManagerMapCollection &variableMap, uint32_t flags=0) const |
Maps this Expr into one for a different ExprManager, using variableMap for the translation and extending it with any new mappings. More... | |
void | printAst (std::ostream &out, int indent=0) const |
Very basic pretty printer for Expr. More... | |
template<> | |
bool const & | getConst () const |
Friends | |
class | SmtEngine |
class | smt::SmtEnginePrivate |
class | ExprManager |
class | NodeManager |
class | TypeCheckingException |
class | expr::pickle::Pickler |
class | prop::TheoryProxy |
template<bool ref_count> | |
class | NodeTemplate |
NodeTemplate< true > | expr::exportInternal (NodeTemplate< false > n, ExprManager *from, ExprManager *to, ExprManagerMapCollection &vmap, uint32_t flags) |
std::ostream & | CVC4::operator<< (std::ostream &out, const Expr &e) |
Class encapsulating CVC4 expressions and methods for constructing new expressions.
typedef expr::ExprDag CVC4::Expr::dag |
typedef expr::ExprPrintTypes CVC4::Expr::printtypes |
IOStream manipulator to print type ascriptions or not.
// let a, b, c, and d be variables of sort U Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) out << printtypes(true) << e;
gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
out << printtypes(false) << [same expr as above]
gives "(OR a b (AND c (NOT d)))"
typedef expr::ExprSetDepth CVC4::Expr::setdepth |
IOStream manipulator to set the maximum depth of Exprs when pretty-printing.
-1 means print to any depth. E.g.:
// let a, b, c, and d be VARIABLEs Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) out << setdepth(3) << e;
gives "(OR a b (AND c (NOT d)))", but
out << setdepth(1) << [same expr as above]
gives "(OR a b (...))"
typedef expr::ExprSetLanguage CVC4::Expr::setlanguage |
CVC4::Expr::Expr | ( | ) |
Default constructor, makes a null expression.
CVC4::Expr::Expr | ( | const Expr & | e | ) |
Copy constructor, makes a copy of a given expression.
e | the expression to copy |
CVC4::Expr::~Expr | ( | ) |
Destructor.
Returns the conjunction of this expression and the given expression.
const_iterator CVC4::Expr::begin | ( | ) | const |
Returns an iterator to the first child of this Expr.
const_iterator CVC4::Expr::end | ( | ) | const |
Returns an iterator to one-off-the-last child of this Expr.
Expr CVC4::Expr::exportTo | ( | ExprManager * | exprManager, |
ExprManagerMapCollection & | variableMap, | ||
uint32_t | flags = 0 |
||
) | const |
Maps this Expr into one for a different ExprManager, using variableMap for the translation and extending it with any new mappings.
Referenced by CVC4::Command::ExportTransformer::operator()().
|
inline |
const T& CVC4::Expr::getConst | ( | ) | const |
Extract a constant of type T.
bool const& CVC4::Expr::getConst | ( | ) | const |
ExprManager* CVC4::Expr::getExprManager | ( | ) | const |
Returns the expression reponsible for this expression.
unsigned long CVC4::Expr::getId | ( | ) | const |
Get the ID of this expression (used for the comparison operators).
Referenced by CVC4::ExprHashFunction::operator()().
Kind CVC4::Expr::getKind | ( | ) | const |
Returns the kind of the expression (AND, PLUS ...).
size_t CVC4::Expr::getNumChildren | ( | ) | const |
Returns the number of children of this expression.
Expr CVC4::Expr::getOperator | ( | ) | const |
Get the operator of this expression.
IllegalArgumentException | if it has no operator |
Type CVC4::Expr::getType | ( | bool | check = false | ) | const |
throw | ( | TypeCheckingException | |||
) |
Get the type for this Expr and optionally do type checking.
Initial type computation will be near-constant time if type checking is not requested. Results are memoized, so that subsequent calls to getType() without type checking will be constant time.
Initial type checking is linear in the size of the expression. Again, the results are memoized, so that subsequent calls to getType(), with or without type checking, will be constant time.
NOTE: A TypeCheckingException can be thrown even when type checking is not requested. getType() will always return a valid and correct type and, thus, an exception will be thrown when no valid or correct type can be computed (e.g., if the arguments to a bit-vector operation aren't bit-vectors). When type checking is not requested, getType() will do the minimum amount of checking required to return a valid result.
check | whether we should check the type as we compute it (default: false) |
bool CVC4::Expr::hasOperator | ( | ) | const |
Check if this is an expression that has an operator.
Returns the Boolean equivalence of this expression and the given expression.
Returns the implication of this expression and the given expression.
bool CVC4::Expr::isConst | ( | ) | const |
Check if this is an expression representing a constant.
bool CVC4::Expr::isNull | ( | ) | const |
Check if this is a null expression.
Referenced by CVC4::DatatypeConstructor::isResolved().
bool CVC4::Expr::isVariable | ( | ) | const |
Check if this is an expression representing a variable.
Returns the if-then-else expression with this expression as the Boolean condition and the given expressions as the "then" and "else" expressions.
bool CVC4::Expr::operator!= | ( | const Expr & | e | ) | const |
Syntactic disequality operator.
e | the expression to compare to |
bool CVC4::Expr::operator< | ( | const Expr & | e | ) | const |
Order comparison operator.
The only invariant on the order of expressions is that the expressions that were created sooner will be smaller in the ordering than all the expressions created later. Null expression is the smallest element of the ordering. The behavior of the operator is undefined if the expressions come from two different expression managers.
e | the expression to compare to |
|
inline |
Order comparison operator.
The only invariant on the order of expressions is that the expressions that were created sooner will be smaller in the ordering than all the expressions created later. Null expression is the smallest element of the ordering. The behavior of the operator is undefined if the expressions come from two different expression managers.
e | the expression to compare to |
Assignment operator, makes a copy of the given expression.
If the expression managers of the two expressions differ, the expression of the given expression will be used.
e | the expression to assign |
bool CVC4::Expr::operator== | ( | const Expr & | e | ) | const |
Syntactic comparison operator.
Returns true if expressions belong to the same expression manager and are syntactically identical.
e | the expression to compare to |
bool CVC4::Expr::operator> | ( | const Expr & | e | ) | const |
Order comparison operator.
The only invariant on the order of expressions is that the expressions that were created sooner will be smaller in the ordering than all the expressions created later. Null expression is the smallest element of the ordering. The behavior of the operator is undefined if the expressions come from two different expression managers.
e | the expression to compare to |
|
inline |
Order comparison operator.
The only invariant on the order of expressions is that the expressions that were created sooner will be smaller in the ordering than all the expressions created later. Null expression is the smallest element of the ordering. The behavior of the operator is undefined if the expressions come from two different expression managers.
e | the expression to compare to |
Expr CVC4::Expr::operator[] | ( | unsigned | i | ) | const |
Returns the i'th child of this expression.
i | the index of the child to retrieve |
Returns the disjunction of this expression and the given expression.
void CVC4::Expr::printAst | ( | std::ostream & | out, |
int | indent = 0 |
||
) | const |
Very basic pretty printer for Expr.
This is equivalent to calling e.getNode().printAst(...)
out | output stream to print to. |
indent | number of spaces to indent the formula by. |
Expr CVC4::Expr::substitute | ( | const std::vector< Expr > | exes, |
const std::vector< Expr > & | replacements | ||
) | const |
Substitute "replacements" in for "exes".
Expr CVC4::Expr::substitute | ( | const std::hash_map< Expr, Expr, ExprHashFunction > | map | ) | const |
Substitute pairs of (ex,replacement) from the given map.
void CVC4::Expr::toStream | ( | std::ostream & | out, |
int | toDepth = -1 , |
||
bool | types = false , |
||
size_t | dag = 1 , |
||
OutputLanguage | language = language::output::LANG_AST |
||
) | const |
Outputs the string representation of the expression to the stream.
out | the stream to serialize this expression to |
toDepth | the depth to which to print this expression, or -1 to print it fully |
types | set to true to ascribe types to the output expressions (might break language compliance, but good for debugging expressions) |
dag | the dagification threshold to use (0 == off) |
language | the language in which to output |
std::string CVC4::Expr::toString | ( | ) | const |
Returns the string representation of the expression.
Returns the exclusive disjunction of this expression and the given expression.
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |
|
friend |