cvc4-1.4
CVC4::expr Namespace Reference

Namespaces

 pickle
 

Data Structures

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

Functions

TypeNode exportTypeInternal (TypeNode n, NodeManager *from, NodeManager *nm, ExprManagerMapCollection &vmap)
 
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...
 

Function Documentation

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 1104 of file expr.h.

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

Referenced by CVC4::ExportUnsupportedException::ExportUnsupportedException().

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 1118 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 1132 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 1146 of file expr.h.

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