cvc4-1.4
CVC4::Expr Class Reference

Class encapsulating CVC4 expressions and methods for constructing new expressions. More...

#include <expr.h>

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

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...
 
Exproperator= (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< ExprgetChildren () 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_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...
 
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...
 
template<>
bool const & getConst () const
 

Friends

class SmtEngine
 
class smt::SmtEnginePrivate
 
class ExprManager
 
class NodeManager
 
class TypeCheckingException
 
class expr::pickle::Pickler
 
class prop::TheoryProxy
 
class expr::ExportPrivate
 
template<bool ref_count>
class NodeTemplate
 
std::ostream & CVC4::operator<< (std::ostream &out, const Expr &e)
 

Detailed Description

Class encapsulating CVC4 expressions and methods for constructing new expressions.

Definition at line 227 of file expr.h.

Member Typedef Documentation

◆ dag

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

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

Definition at line 610 of file expr.h.

◆ printtypes

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)))"

Definition at line 605 of file expr.h.

◆ setdepth

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 (...))"

Definition at line 590 of file expr.h.

◆ setlanguage

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

IOStream manipulator to set the output language for Exprs.

Definition at line 615 of file expr.h.

Constructor & Destructor Documentation

◆ Expr() [1/2]

CVC4::Expr::Expr ( )

Default constructor, makes a null expression.

◆ Expr() [2/2]

CVC4::Expr::Expr ( const Expr e)

Copy constructor, makes a copy of a given expression.

Parameters
ethe expression to copy

◆ ~Expr()

CVC4::Expr::~Expr ( )

Destructor.

Member Function Documentation

◆ andExpr()

Expr CVC4::Expr::andExpr ( const Expr e) const

Returns the conjunction of this expression and the given expression.

◆ begin()

const_iterator CVC4::Expr::begin ( ) const

Returns an iterator to the first child of this Expr.

◆ end()

const_iterator CVC4::Expr::end ( ) const

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

◆ exportTo()

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()().

◆ getChildren()

std::vector<Expr> CVC4::Expr::getChildren ( ) const
inline

Returns the children of this Expr.

Definition at line 366 of file expr.h.

◆ getConst() [1/2]

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

Extract a constant of type T.

◆ getConst() [2/2]

template<>
bool const& CVC4::Expr::getConst ( ) const

◆ getExprManager()

ExprManager* CVC4::Expr::getExprManager ( ) const

Returns the expression reponsible for this expression.

◆ getId()

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

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()().

◆ getKind()

Kind CVC4::Expr::getKind ( ) const

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

Returns
the kind of the expression

◆ getNumChildren()

size_t CVC4::Expr::getNumChildren ( ) const

Returns the number of children of this expression.

Returns
the number of children

◆ getOperator()

Expr CVC4::Expr::getOperator ( ) const

Get the operator of this expression.

Exceptions
IllegalArgumentExceptionif it has no operator
Returns
the operator of this expression

◆ getType()

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.

Parameters
checkwhether we should check the type as we compute it (default: false)

◆ hasOperator()

bool CVC4::Expr::hasOperator ( ) const

Check if this is an expression that has an operator.

Returns
true if this expression has an operator

◆ iffExpr()

Expr CVC4::Expr::iffExpr ( const Expr e) const

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

◆ impExpr()

Expr CVC4::Expr::impExpr ( const Expr e) const

Returns the implication of this expression and the given expression.

◆ isConst()

bool CVC4::Expr::isConst ( ) const

Check if this is an expression representing a constant.

Returns
true if a constant expression

◆ isNull()

bool CVC4::Expr::isNull ( ) const

Check if this is a null expression.

Returns
true if a null expression

Referenced by CVC4::DatatypeConstructor::isResolved().

◆ isVariable()

bool CVC4::Expr::isVariable ( ) const

Check if this is an expression representing a variable.

Returns
true if a variable expression

◆ iteExpr()

Expr CVC4::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.

◆ notExpr()

Expr CVC4::Expr::notExpr ( ) const

Returns the Boolean negation of this Expr.

◆ operator!=()

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

Syntactic disequality operator.

Parameters
ethe expression to compare to
Returns
true if expressions differ syntactically, false otherwise

◆ operator<()

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.

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

◆ operator<=()

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

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

Definition at line 319 of file expr.h.

◆ operator=()

Expr& CVC4::Expr::operator= ( const Expr e)

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.

Parameters
ethe expression to assign
Returns
the reference to this expression after assignment

◆ operator==()

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.

Parameters
ethe expression to compare to
Returns
true if expressions are syntactically the same, false otherwise

◆ operator>()

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.

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

◆ operator>=()

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

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

Definition at line 331 of file expr.h.

◆ operator[]()

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

Returns the i'th child of this expression.

Parameters
ithe index of the child to retrieve
Returns
the child

◆ orExpr()

Expr CVC4::Expr::orExpr ( const Expr e) const

Returns the disjunction of this expression and the given expression.

◆ printAst()

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(...)

Parameters
outoutput stream to print to.
indentnumber of spaces to indent the formula by.

◆ substitute() [1/3]

Expr CVC4::Expr::substitute ( Expr  e,
Expr  replacement 
) const

Substitute "replacement" in for "e".

◆ substitute() [2/3]

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

Substitute "replacements" in for "exes".

◆ substitute() [3/3]

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

Substitute pairs of (ex,replacement) from the given map.

◆ toStream()

void CVC4::Expr::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.

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

◆ toString()

std::string CVC4::Expr::toString ( ) const

Returns the string representation of the expression.

Returns
a string representation of the expression

◆ xorExpr()

Expr CVC4::Expr::xorExpr ( const Expr e) const

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

Friends And Related Function Documentation

◆ CVC4::operator<<

std::ostream& CVC4::operator<< ( std::ostream &  out,
const Expr e 
)
friend

◆ expr::ExportPrivate

friend class expr::ExportPrivate
friend

Definition at line 655 of file expr.h.

◆ expr::pickle::Pickler

friend class expr::pickle::Pickler
friend

Definition at line 653 of file expr.h.

◆ ExprManager

friend class ExprManager
friend

Definition at line 650 of file expr.h.

◆ NodeManager

friend class NodeManager
friend

Definition at line 651 of file expr.h.

◆ NodeTemplate

template<bool ref_count>
friend class NodeTemplate
friend

Definition at line 657 of file expr.h.

◆ prop::TheoryProxy

friend class prop::TheoryProxy
friend

Definition at line 654 of file expr.h.

◆ smt::SmtEnginePrivate

friend class smt::SmtEnginePrivate
friend

Definition at line 649 of file expr.h.

◆ SmtEngine

friend class SmtEngine
friend

Definition at line 648 of file expr.h.

◆ TypeCheckingException

friend class TypeCheckingException
friend

Definition at line 652 of file expr.h.


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