cvc4-1.4
|
Expr class for CVC3 compatibility layer. More...
#include <cvc3_compat.h>
Public Types | |
typedef CVC4::Expr::const_iterator | iterator |
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 () | |
Expr (const Expr &e) | |
Expr (const CVC4::Expr &e) | |
Expr (CVC4::Kind k) | |
Expr | eqExpr (const Expr &right) const |
Expr | notExpr () const |
Expr | negate () const |
Expr | andExpr (const Expr &right) const |
Expr | orExpr (const Expr &right) const |
Expr | iteExpr (const Expr &thenpart, const Expr &elsepart) const |
Expr | iffExpr (const Expr &right) const |
Expr | impExpr (const Expr &right) const |
Expr | xorExpr (const Expr &right) const |
Expr | substExpr (const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const |
Expr | substExpr (const ExprHashMap< Expr > &oldToNew) const |
Expr | operator! () const |
Expr | operator && (const Expr &right) const |
Expr | operator|| (const Expr &right) const |
size_t | hash () const |
bool | isFalse () const |
bool | isTrue () const |
bool | isBoolConst () const |
bool | isVar () const |
bool | isBoundVar () const |
bool | isString () const |
bool | isSymbol () const |
bool | isTerm () const |
bool | isType () const |
bool | isClosure () const |
bool | isQuantifier () const |
bool | isForall () const |
bool | isExists () const |
bool | isLambda () const |
bool | isApply () const |
bool | isTheorem () const |
bool | isConstant () const |
bool | isRawList () const |
bool | isAtomic () const |
bool | isAtomicFormula () const |
bool | isAbsAtomicFormula () const |
bool | isLiteral () const |
bool | isAbsLiteral () const |
bool | isBoolConnective () const |
bool | isPropLiteral () const |
bool | isPropAtom () const |
std::string | getName () const |
std::string | getUid () const |
std::string | getString () const |
std::vector< Expr > | getVars () const |
Expr | getExistential () const |
int | getBoundIndex () const |
Expr | getBody () const |
Theorem | getTheorem () const |
bool | isEq () const |
bool | isNot () const |
bool | isAnd () const |
bool | isOr () const |
bool | isITE () const |
bool | isIff () const |
bool | isImpl () const |
bool | isXor () const |
bool | isRational () const |
bool | isSkolem () const |
const Rational & | getRational () const |
Op | mkOp () const |
Op | getOp () const |
Expr | getOpExpr () const |
int | getOpKind () const |
Expr | getExpr () const |
std::vector< std::vector< Expr > > | getTriggers () const |
Get the manual triggers of the closure Expr. More... | |
ExprManager * | getEM () const |
std::vector< Expr > | getKids () const |
ExprIndex | getIndex () const |
int | arity () const |
Expr | operator[] (int i) const |
Expr | unnegate () const |
Remove leading NOT if any. More... | |
bool | isInitialized () const |
Type | getType () const |
Get the type. Recursively compute if necessary. More... | |
Type | lookupType () const |
Look up the current type. Do not recursively compute (i.e. may be NULL) More... | |
void | pprint () const |
Pretty-print the expression. More... | |
void | pprintnodag () const |
Pretty-print without dagifying. 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 | 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_AUTO) 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... | |
template<> | |
bool const & | getConst () const |
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... | |
Static Public Member Functions | |
static size_t | hash (const Expr &e) |
Expr class for CVC3 compatibility layer.
This class is identical to (and convertible to/from) a CVC4 Expr, except that a few additional functions are supported to provide naming compatibility with CVC3.
Definition at line 319 of file cvc3_compat.h.
|
inherited |
typedef CVC4::Expr::const_iterator CVC3::Expr::iterator |
Definition at line 321 of file cvc3_compat.h.
|
inherited |
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)))"
|
inherited |
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 (...))"
|
inherited |
CVC3::Expr::Expr | ( | ) |
CVC3::Expr::Expr | ( | const Expr & | e | ) |
CVC3::Expr::Expr | ( | const CVC4::Expr & | e | ) |
CVC3::Expr::Expr | ( | CVC4::Kind | k | ) |
Returns the conjunction of this expression and the given expression.
int CVC3::Expr::arity | ( | ) | const |
|
inherited |
Returns an iterator to the first child of this Expr.
|
inherited |
Returns an iterator to one-off-the-last child of this Expr.
|
inherited |
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()().
Expr CVC3::Expr::getBody | ( | ) | const |
int CVC3::Expr::getBoundIndex | ( | ) | const |
|
inlineinherited |
|
inherited |
Extract a constant of type T.
|
inherited |
ExprManager* CVC3::Expr::getEM | ( | ) | const |
Expr CVC3::Expr::getExistential | ( | ) | const |
Expr CVC3::Expr::getExpr | ( | ) | const |
|
inherited |
Returns the expression reponsible for this expression.
|
inherited |
Get the ID of this expression (used for the comparison operators).
Referenced by CVC4::ExprHashFunction::operator()().
ExprIndex CVC3::Expr::getIndex | ( | ) | const |
std::vector<Expr> CVC3::Expr::getKids | ( | ) | const |
|
inherited |
Returns the kind of the expression (AND, PLUS ...).
std::string CVC3::Expr::getName | ( | ) | const |
|
inherited |
Returns the number of children of this expression.
Op CVC3::Expr::getOp | ( | ) | const |
|
inherited |
Get the operator of this expression.
IllegalArgumentException | if it has no operator |
Expr CVC3::Expr::getOpExpr | ( | ) | const |
int CVC3::Expr::getOpKind | ( | ) | const |
const Rational& CVC3::Expr::getRational | ( | ) | const |
std::string CVC3::Expr::getString | ( | ) | const |
Theorem CVC3::Expr::getTheorem | ( | ) | const |
std::vector< std::vector<Expr> > CVC3::Expr::getTriggers | ( | ) | const |
Get the manual triggers of the closure Expr.
Type CVC3::Expr::getType | ( | ) | const |
Get the type. Recursively compute if necessary.
|
inherited |
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) |
std::string CVC3::Expr::getUid | ( | ) | const |
std::vector<Expr> CVC3::Expr::getVars | ( | ) | const |
|
static |
size_t CVC3::Expr::hash | ( | ) | const |
|
inherited |
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 CVC3::Expr::isAbsAtomicFormula | ( | ) | const |
bool CVC3::Expr::isAbsLiteral | ( | ) | const |
bool CVC3::Expr::isAnd | ( | ) | const |
bool CVC3::Expr::isApply | ( | ) | const |
bool CVC3::Expr::isAtomic | ( | ) | const |
bool CVC3::Expr::isAtomicFormula | ( | ) | const |
bool CVC3::Expr::isBoolConnective | ( | ) | const |
bool CVC3::Expr::isBoolConst | ( | ) | const |
bool CVC3::Expr::isBoundVar | ( | ) | const |
bool CVC3::Expr::isClosure | ( | ) | const |
|
inherited |
Check if this is an expression representing a constant.
bool CVC3::Expr::isConstant | ( | ) | const |
bool CVC3::Expr::isEq | ( | ) | const |
bool CVC3::Expr::isExists | ( | ) | const |
bool CVC3::Expr::isFalse | ( | ) | const |
bool CVC3::Expr::isForall | ( | ) | const |
bool CVC3::Expr::isIff | ( | ) | const |
bool CVC3::Expr::isImpl | ( | ) | const |
bool CVC3::Expr::isInitialized | ( | ) | const |
bool CVC3::Expr::isITE | ( | ) | const |
bool CVC3::Expr::isLambda | ( | ) | const |
bool CVC3::Expr::isLiteral | ( | ) | const |
bool CVC3::Expr::isNot | ( | ) | const |
|
inherited |
Check if this is a null expression.
Referenced by CVC4::DatatypeConstructor::isResolved().
bool CVC3::Expr::isOr | ( | ) | const |
bool CVC3::Expr::isPropAtom | ( | ) | const |
bool CVC3::Expr::isPropLiteral | ( | ) | const |
bool CVC3::Expr::isQuantifier | ( | ) | const |
bool CVC3::Expr::isRational | ( | ) | const |
bool CVC3::Expr::isRawList | ( | ) | const |
bool CVC3::Expr::isSkolem | ( | ) | const |
bool CVC3::Expr::isString | ( | ) | const |
bool CVC3::Expr::isSymbol | ( | ) | const |
bool CVC3::Expr::isTerm | ( | ) | const |
bool CVC3::Expr::isTheorem | ( | ) | const |
bool CVC3::Expr::isTrue | ( | ) | const |
bool CVC3::Expr::isType | ( | ) | const |
bool CVC3::Expr::isVar | ( | ) | const |
|
inherited |
Check if this is an expression representing a variable.
bool CVC3::Expr::isXor | ( | ) | const |
Returns the if-then-else expression with this expression as the Boolean condition and the given expressions as the "then" and "else" expressions.
Type CVC3::Expr::lookupType | ( | ) | const |
Look up the current type. Do not recursively compute (i.e. may be NULL)
Op CVC3::Expr::mkOp | ( | ) | const |
Expr CVC3::Expr::negate | ( | ) | const |
Expr CVC3::Expr::notExpr | ( | ) | const |
Expr CVC3::Expr::operator! | ( | ) | const |
|
inherited |
Syntactic disequality operator.
e | the expression to compare to |
|
inherited |
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 |
|
inlineinherited |
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 |
|
inherited |
Syntactic comparison operator.
Returns true if expressions belong to the same expression manager and are syntactically identical.
e | the expression to compare to |
|
inherited |
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 |
|
inlineinherited |
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 |
|
inherited |
Returns the i'th child of this expression.
i | the index of the child to retrieve |
Expr CVC3::Expr::operator[] | ( | int | i | ) | const |
Returns the disjunction of this expression and the given expression.
void CVC3::Expr::pprint | ( | ) | const |
Pretty-print the expression.
void CVC3::Expr::pprintnodag | ( | ) | const |
Pretty-print without dagifying.
|
inherited |
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 CVC3::Expr::substExpr | ( | const std::vector< Expr > & | oldTerms, |
const std::vector< Expr > & | newTerms | ||
) | const |
Expr CVC3::Expr::substExpr | ( | const ExprHashMap< Expr > & | oldToNew | ) | const |
Substitute "replacement" in for "e".
|
inherited |
Substitute "replacements" in for "exes".
|
inherited |
Substitute pairs of (ex,replacement) from the given map.
|
inherited |
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 |
|
inherited |
Returns the string representation of the expression.
Expr CVC3::Expr::unnegate | ( | ) | const |
Remove leading NOT if any.
Returns the exclusive disjunction of this expression and the given expression.