cvc4-1.3
CVC4::expr Namespace Reference

Namespaces

 pickle
 

Data Structures

class  ExprSetDepth
 IOStream manipulator to set the maximum depth of Exprs when pretty-printing. More...
 
class  ExprPrintTypes
 IOStream manipulator to print type ascriptions or not. More...
 
class  ExprDag
 IOStream manipulator to print expressions as a dag (or not). More...
 
class  ExprSetLanguage
 IOStream manipulator to set the output language for Exprs. More...
 

Functions

NodeTemplate< true > exportInternal (NodeTemplate< false > n, ExprManager *from, ExprManager *to, ExprManagerMapCollection &vmap, uint32_t flags)
 
std::ostream & operator<< (std::ostream &out, ExprSetDepth sd)
 Sets the default depth when pretty-printing a Expr to an ostream. More...
 
std::ostream & operator<< (std::ostream &out, ExprPrintTypes pt)
 Sets the default print-types setting when pretty-printing an Expr to an ostream. More...
 
std::ostream & operator<< (std::ostream &out, ExprDag d)
 Sets the default dag setting when pretty-printing a Expr to an ostream. More...
 
std::ostream & operator<< (std::ostream &out, ExprSetLanguage l)
 Sets the output language when pretty-printing a Expr to an ostream. More...
 
TypeNode exportTypeInternal (TypeNode n, NodeManager *from, NodeManager *nm, ExprManagerMapCollection &vmap)
 

Function Documentation

NodeTemplate<true> CVC4::expr::exportInternal ( NodeTemplate< false >  n,
ExprManager from,
ExprManager to,
ExprManagerMapCollection &  vmap,
uint32_t  flags 
)
TypeNode CVC4::expr::exportTypeInternal ( TypeNode  n,
NodeManager *  from,
NodeManager *  nm,
ExprManagerMapCollection &  vmap 
)
std::ostream& CVC4::expr::operator<< ( std::ostream &  out,
ExprSetDepth  sd 
)
inline

Sets the default depth when pretty-printing a Expr to an ostream.

Use like this:

// let out be an ostream, e an Expr out << Expr::setdepth(n) << e << endl;

The depth stays permanently (until set again) with the stream.

Definition at line 1101 of file expr.h.

References CVC4::expr::ExprSetDepth::applyDepth(), and CVC4::options::out.

std::ostream& CVC4::expr::operator<< ( std::ostream &  out,
ExprPrintTypes  pt 
)
inline

Sets the default print-types setting when pretty-printing an Expr to an ostream.

Use like this:

// let out be an ostream, e an Expr out << Expr::printtypes(true) << e << endl;

The setting stays permanently (until set again) with the stream.

Definition at line 1115 of file expr.h.

References CVC4::expr::ExprPrintTypes::applyPrintTypes(), and CVC4::options::out.

std::ostream& CVC4::expr::operator<< ( std::ostream &  out,
ExprDag  d 
)
inline

Sets the default dag setting when pretty-printing a Expr to an ostream.

Use like this:

// let out be an ostream, e an Expr out << Expr::dag(true) << e << endl;

The setting stays permanently (until set again) with the stream.

Definition at line 1129 of file expr.h.

References CVC4::expr::ExprDag::applyDag(), and CVC4::options::out.

std::ostream& CVC4::expr::operator<< ( std::ostream &  out,
ExprSetLanguage  l 
)
inline

Sets the output language when pretty-printing a Expr to an ostream.

Use like this:

// let out be an ostream, e an Expr out << Expr::setlanguage(LANG_SMTLIB_V2) << e << endl;

The setting stays permanently (until set again) with the stream.

Definition at line 1143 of file expr.h.

References CVC4::expr::ExprSetLanguage::applyLanguage(), and CVC4::options::out.