cvc4-1.3
CVC3::Expr Class Reference

Expr class for CVC3 compatibility layer. More...

#include <cvc3_compat.h>

Inheritance diagram for CVC3::Expr:
CVC4::Expr

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 ()
 
 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
 
const std::string & getName () const
 
const std::string & getUid () const
 
const std::string & getString () const
 
const std::vector< Expr > & getVars () const
 
const ExprgetExistential () const
 
int getBoundIndex () const
 
const ExprgetBody () const
 
const TheoremgetTheorem () 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 RationalgetRational () 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...
 
ExprManagergetEM () const
 
std::vector< ExprgetKids () 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< ExprgetChildren () 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_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...
 
template<>
bool const & getConst () const
 
ExprManagergetExprManager () 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)
 

Detailed Description

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.

Member Typedef Documentation

typedef expr::ExprDag CVC4::Expr::dag
inherited

IOStream manipulator to print expressions as a DAG (or not).

Definition at line 609 of file expr.h.

typedef expr::ExprPrintTypes CVC4::Expr::printtypes
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)))"

Definition at line 604 of file expr.h.

typedef expr::ExprSetDepth CVC4::Expr::setdepth
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 (...))"

Definition at line 589 of file expr.h.

typedef expr::ExprSetLanguage CVC4::Expr::setlanguage
inherited

IOStream manipulator to set the output language for Exprs.

Definition at line 614 of file expr.h.

Constructor & Destructor Documentation

CVC3::Expr::Expr ( )
CVC3::Expr::Expr ( const Expr e)
CVC3::Expr::Expr ( const CVC4::Expr e)
CVC3::Expr::Expr ( CVC4::Kind  k)

Member Function Documentation

Expr CVC3::Expr::andExpr ( const Expr right) const
Expr CVC4::Expr::andExpr ( const Expr e) const
inherited

Returns the conjunction of this expression and the given expression.

int CVC3::Expr::arity ( ) const
const_iterator CVC4::Expr::begin ( ) const
inherited

Returns an iterator to the first child of this Expr.

const_iterator CVC4::Expr::end ( ) const
inherited

Returns an iterator to one-off-the-last child of this Expr.

Expr CVC3::Expr::eqExpr ( const Expr right) const
Expr CVC4::Expr::exportTo ( ExprManager exprManager,
ExprManagerMapCollection variableMap,
uint32_t  flags = 0 
) const
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()().

const Expr& CVC3::Expr::getBody ( ) const
int CVC3::Expr::getBoundIndex ( ) const
std::vector<Expr> CVC4::Expr::getChildren ( ) const
inlineinherited

Returns the children of this Expr.

Definition at line 365 of file expr.h.

template<class T >
const T& CVC4::Expr::getConst ( ) const
inherited

Extract a constant of type T.

template<>
bool const& CVC4::Expr::getConst ( ) const
inherited
ExprManager* CVC3::Expr::getEM ( ) const
const Expr& CVC3::Expr::getExistential ( ) const
Expr CVC3::Expr::getExpr ( ) const
ExprManager* CVC4::Expr::getExprManager ( ) const
inherited

Returns the expression reponsible for this expression.

unsigned long CVC4::Expr::getId ( ) const
inherited

Get the ID of this expression (used for the comparison operators).

Returns
an identifier uniquely identifying the value this expression holds.

Referenced by CVC4::ExprHashFunction::operator()().

ExprIndex CVC3::Expr::getIndex ( ) const
std::vector<Expr> CVC3::Expr::getKids ( ) const
Kind CVC4::Expr::getKind ( ) const
inherited

Returns the kind of the expression (AND, PLUS ...).

Returns
the kind of the expression
const std::string& CVC3::Expr::getName ( ) const
size_t CVC4::Expr::getNumChildren ( ) const
inherited

Returns the number of children of this expression.

Returns
the number of children
Op CVC3::Expr::getOp ( ) const
Expr CVC4::Expr::getOperator ( ) const
inherited

Get the operator of this expression.

Exceptions
IllegalArgumentExceptionif it has no operator
Returns
the operator of this expression
Expr CVC3::Expr::getOpExpr ( ) const
int CVC3::Expr::getOpKind ( ) const
const Rational& CVC3::Expr::getRational ( ) const
const std::string& CVC3::Expr::getString ( ) const
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.

Type CVC4::Expr::getType ( bool  check = false) const
throw (TypeCheckingException
)
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.

Parameters
checkwhether we should check the type as we compute it (default: false)
const std::string& CVC3::Expr::getUid ( ) const
const std::vector<Expr>& CVC3::Expr::getVars ( ) const
static size_t CVC3::Expr::hash ( const Expr e)
static
size_t CVC3::Expr::hash ( ) const
bool CVC4::Expr::hasOperator ( ) const
inherited

Check if this is an expression that has an operator.

Returns
true if this expression has an operator
Expr CVC3::Expr::iffExpr ( const Expr right) const
Expr CVC4::Expr::iffExpr ( const Expr e) const
inherited

Returns the Boolean equivalence of this expression and the given expression.

Expr CVC3::Expr::impExpr ( const Expr right) const
Expr CVC4::Expr::impExpr ( const Expr e) const
inherited

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
bool CVC4::Expr::isConst ( ) const
inherited

Check if this is an expression representing a constant.

Returns
true if a constant expression
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
bool CVC4::Expr::isNull ( ) const
inherited

Check if this is a null expression.

Returns
true if 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
bool CVC4::Expr::isVariable ( ) const
inherited

Check if this is an expression representing a variable.

Returns
true if a variable expression
bool CVC3::Expr::isXor ( ) const
Expr CVC3::Expr::iteExpr ( const Expr thenpart,
const Expr elsepart 
) const
Expr CVC4::Expr::iteExpr ( const Expr then_e,
const Expr else_e 
) const
inherited

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
bool CVC4::Expr::operator!= ( const Expr e) const
inherited

Syntactic disequality operator.

Parameters
ethe expression to compare to
Returns
true if expressions differ syntactically, false otherwise
Expr CVC3::Expr::operator&& ( const Expr right) const
bool CVC4::Expr::operator< ( const Expr e) const
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.

Parameters
ethe expression to compare to
Returns
true if this expression is smaller than the given one
bool CVC4::Expr::operator<= ( const Expr e) const
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.

Parameters
ethe expression to compare to
Returns
true if this expression is smaller or equal to the given one

Definition at line 318 of file expr.h.

bool CVC4::Expr::operator== ( const Expr e) const
inherited

Syntactic comparison operator.

Returns true if expressions belong to the same expression manager and are syntactically identical.

Parameters
ethe expression to compare to
Returns
true if expressions are syntactically the same, false otherwise
bool CVC4::Expr::operator> ( const Expr e) const
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.

Parameters
ethe expression to compare to
Returns
true if this expression is greater than the given one
bool CVC4::Expr::operator>= ( const Expr e) const
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.

Parameters
ethe expression to compare to
Returns
true if this expression is greater or equal to the given one

Definition at line 330 of file expr.h.

Expr CVC4::Expr::operator[] ( unsigned  i) const
inherited

Returns the i'th child of this expression.

Parameters
ithe index of the child to retrieve
Returns
the child
Expr CVC3::Expr::operator[] ( int  i) const
Expr CVC3::Expr::operator|| ( const Expr right) const
Expr CVC3::Expr::orExpr ( const Expr right) const
Expr CVC4::Expr::orExpr ( const Expr e) const
inherited

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.

void CVC4::Expr::printAst ( std::ostream &  out,
int  indent = 0 
) const
inherited

Very basic pretty printer for Expr.

This is equivalent to calling e.getNode().printAst(...)

Parameters
outoutput stream to print to.
indentnumber 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
Expr CVC4::Expr::substitute ( Expr  e,
Expr  replacement 
) const
inherited

Substitute "replacement" in for "e".

Expr CVC4::Expr::substitute ( const std::vector< Expr exes,
const std::vector< Expr > &  replacements 
) const
inherited

Substitute "replacements" in for "exes".

Expr CVC4::Expr::substitute ( const std::hash_map< Expr, Expr, ExprHashFunction map) const
inherited

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
inherited

Outputs the string representation of the expression to the stream.

Parameters
outthe stream to serialize this expression to
toDepththe depth to which to print this expression, or -1 to print it fully
typesset to true to ascribe types to the output expressions (might break language compliance, but good for debugging expressions)
dagthe dagification threshold to use (0 == off)
languagethe language in which to output
std::string CVC4::Expr::toString ( ) const
inherited

Returns the string representation of the expression.

Returns
a string representation of the expression
Expr CVC3::Expr::unnegate ( ) const

Remove leading NOT if any.

Expr CVC3::Expr::xorExpr ( const Expr right) const
Expr CVC4::Expr::xorExpr ( const Expr e) const
inherited

Returns the exclusive disjunction of this expression and the given expression.


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