klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::ExprSMTLIBLetPrinter Class Reference

#include <ExprSMTLIBLetPrinter.h>

Inheritance diagram for klee::ExprSMTLIBLetPrinter:
Collaboration diagram for klee::ExprSMTLIBLetPrinter:

Public Member Functions

 ExprSMTLIBLetPrinter ()
 
virtual ~ExprSMTLIBLetPrinter ()
 
virtual void generateOutput ()
 
- Public Member Functions inherited from klee::ExprSMTLIBPrinter
bool setConstantDisplayMode (ConstantDisplayMode cdm)
 
ConstantDisplayMode getConstantDisplayMode ()
 
 ExprSMTLIBPrinter ()
 Create a new printer that will print a query in the SMTLIBv2 language. More...
 
void setOutput (llvm::raw_ostream &output)
 
void setQuery (const Query &q)
 
virtual ~ExprSMTLIBPrinter ()
 
bool setLogic (SMTLIBv2Logic l)
 
void setHumanReadable (bool hr)
 
bool setSMTLIBboolOption (SMTLIBboolOptions option, SMTLIBboolValues value)
 
void setArrayValuesToGet (const std::vector< const Array * > &a)
 
bool isHumanReadable ()
 

Protected Member Functions

virtual void scan (const ref< Expr > &e)
 
virtual void reset ()
 
virtual void generateBindings ()
 
void printExpression (const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
 
void printLetExpression ()
 
- Protected Member Functions inherited from klee::ExprSMTLIBPrinter
SMTLIB_SORT getSort (const ref< Expr > &e)
 Determine the SMTLIBv2 sort of the expression. More...
 
void printCastToSort (const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT sort)
 Print an expression but cast it to a particular SMTLIBv2 sort first. More...
 
virtual void scanAll ()
 
virtual void printNotice ()
 
virtual void printOptions ()
 
virtual void printSetLogic ()
 
virtual void printArrayDeclarations ()
 
virtual void printConstraints ()
 
virtual void printQuery ()
 
virtual void printAction ()
 
virtual void printExit ()
 Print the SMTLIBv2 command to exit. More...
 
void printConstant (const ref< ConstantExpr > &e)
 
virtual void printReadExpr (const ref< ReadExpr > &e)
 
virtual void printExtractExpr (const ref< ExtractExpr > &e)
 
virtual void printCastExpr (const ref< CastExpr > &e)
 
virtual void printNotEqualExpr (const ref< NeExpr > &e)
 
virtual void printSelectExpr (const ref< SelectExpr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s)
 
virtual void printSortArgsExpr (const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s)
 
virtual void printLogicalOrBitVectorExpr (const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s)
 
virtual void printUpdatesAndArray (const UpdateNode *un, const Array *root)
 Recursively prints updatesNodes. More...
 
virtual const char * getSMTLIBKeyword (const ref< Expr > &e)
 
virtual void printSeperator ()
 
virtual void scanUpdates (const UpdateNode *un)
 Helper function for scan() that scans the expressions of an update node. More...
 

Private Attributes

std::map< const ref< Expr >
, unsigned int > 
bindings
 Let expression binding number map. More...
 
std::set< ref< Expr > > firstEO
 
std::set< ref< Expr > > twoOrMoreEO
 
bool disablePrintedAbbreviations
 

Static Private Attributes

static const char BINDING_PREFIX [] = "?B"
 This is the prefix string used for all abbreviations in (let) expressions. More...
 

Additional Inherited Members

- Public Types inherited from klee::ExprSMTLIBPrinter
enum  SMTLIBv2Logic { QF_ABV, QF_AUFBV }
 
enum  SMTLIBboolOptions { PRINT_SUCCESS, PRODUCE_MODELS, INTERACTIVE_MODE }
 
enum  SMTLIBboolValues { OPTION_TRUE, OPTION_FALSE, OPTION_DEFAULT }
 
enum  ConstantDisplayMode { BINARY, HEX, DECIMAL }
 
enum  SMTLIB_SORT { SORT_BITVECTOR, SORT_BOOL }
 Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV. More...
 
- Protected Attributes inherited from klee::ExprSMTLIBPrinter
std::set< const Array * > usedArrays
 Contains the arrays found during scans. More...
 
llvm::raw_ostream * o
 Output stream to write to. More...
 
const Queryquery
 The query to print. More...
 
PrintContextp
 Helper printer class. More...
 
ref< ExprqueryAssert
 
bool haveConstantArray
 Indicates if there were any constant arrays founds during a scan() More...
 

Detailed Description

This printer behaves like ExprSMTLIBPrinter except that it will abbreviate expressions using the (let) SMT-LIBv2 command. Expression trees that appear two or more times in the Query passed to setQuery() will be abbreviated.

This class should be used just like ExprSMTLIBPrinter.

Definition at line 23 of file ExprSMTLIBLetPrinter.h.

Constructor & Destructor Documentation

klee::ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter ( )

Definition at line 26 of file ExprSMTLIBLetPrinter.cpp.

virtual klee::ExprSMTLIBLetPrinter::~ExprSMTLIBLetPrinter ( )
inlinevirtual

Definition at line 26 of file ExprSMTLIBLetPrinter.h.

Member Function Documentation

void klee::ExprSMTLIBLetPrinter::generateBindings ( )
protectedvirtual

Definition at line 83 of file ExprSMTLIBLetPrinter.cpp.

References bindings, and twoOrMoreEO.

Referenced by generateOutput().

Here is the caller graph for this function:

void klee::ExprSMTLIBLetPrinter::generateOutput ( )
virtual

Print the query to the llvm::raw_ostream setOutput() and setQuery() must be called before calling this.

All options should be set before calling this.

See also
setConstantDisplayMode
setLogic()
setHumanReadable
setSMTLIBboolOption
setArrayValuesToGet

Mostly it does not matter what order the options are set in. However calling setArrayValuesToGet() implies PRODUCE_MODELS is set so, if a call to setSMTLIBboolOption() is made that uses the PRODUCE_MODELS before calling setArrayValuesToGet() then the setSMTLIBboolOption() call will be ineffective.

Reimplemented from klee::ExprSMTLIBPrinter.

Definition at line 30 of file ExprSMTLIBLetPrinter.cpp.

References generateBindings(), klee::ExprSMTLIBPrinter::isHumanReadable(), klee::ExprSMTLIBPrinter::o, klee::ExprSMTLIBPrinter::p, klee::ExprSMTLIBPrinter::printAction(), klee::ExprSMTLIBPrinter::printArrayDeclarations(), klee::ExprSMTLIBPrinter::printExit(), printLetExpression(), klee::ExprSMTLIBPrinter::printNotice(), klee::ExprSMTLIBPrinter::printOptions(), klee::ExprSMTLIBPrinter::printSetLogic(), and klee::ExprSMTLIBPrinter::query.

Here is the call graph for this function:

void klee::ExprSMTLIBLetPrinter::printExpression ( const ref< Expr > &  e,
ExprSMTLIBPrinter::SMTLIB_SORT  expectedSort 
)
protectedvirtual

Recursively print expression

Parameters
eis the expression to print
expectedSortis the sort we want. If "e" is not of the right type a cast will be performed.

Reimplemented from klee::ExprSMTLIBPrinter.

Definition at line 93 of file ExprSMTLIBLetPrinter.cpp.

References BINDING_PREFIX, bindings, disablePrintedAbbreviations, klee::ExprSMTLIBPrinter::getSort(), klee::ExprSMTLIBPrinter::p, klee::ExprSMTLIBPrinter::printCastToSort(), and klee::ExprSMTLIBPrinter::printExpression().

Referenced by printLetExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBLetPrinter::reset ( )
protectedvirtual

Reimplemented from klee::ExprSMTLIBPrinter.

Definition at line 121 of file ExprSMTLIBLetPrinter.cpp.

References bindings, firstEO, klee::ExprSMTLIBPrinter::reset(), and twoOrMoreEO.

Here is the call graph for this function:

void klee::ExprSMTLIBLetPrinter::scan ( const ref< Expr > &  e)
protectedvirtual

Scan Expression recursively for Arrays in expressions. Found arrays are added to the usedArrays vector.

Reimplemented from klee::ExprSMTLIBPrinter.

Definition at line 48 of file ExprSMTLIBLetPrinter.cpp.

References firstEO, klee::ref< T >::get(), klee::Expr::getKid(), klee::Expr::getNumKids(), klee::ExprSMTLIBPrinter::haveConstantArray, klee::ExprSMTLIBPrinter::scanUpdates(), twoOrMoreEO, and klee::ExprSMTLIBPrinter::usedArrays.

Here is the call graph for this function:

Member Data Documentation

const char klee::ExprSMTLIBLetPrinter::BINDING_PREFIX = "?B"
staticprivate

This is the prefix string used for all abbreviations in (let) expressions.

Definition at line 57 of file ExprSMTLIBLetPrinter.h.

Referenced by printExpression(), and printLetExpression().

std::map<const ref<Expr>, unsigned int> klee::ExprSMTLIBLetPrinter::bindings
private

Let expression binding number map.

Definition at line 39 of file ExprSMTLIBLetPrinter.h.

Referenced by generateBindings(), printExpression(), printLetExpression(), and reset().

bool klee::ExprSMTLIBLetPrinter::disablePrintedAbbreviations
private

Definition at line 65 of file ExprSMTLIBLetPrinter.h.

Referenced by printExpression(), and printLetExpression().

std::set<ref<Expr> > klee::ExprSMTLIBLetPrinter::firstEO
private

Definition at line 54 of file ExprSMTLIBLetPrinter.h.

Referenced by reset(), and scan().

std::set<ref<Expr> > klee::ExprSMTLIBLetPrinter::twoOrMoreEO
private

Definition at line 54 of file ExprSMTLIBLetPrinter.h.

Referenced by generateBindings(), reset(), and scan().


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