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

#include <ExprSMTLIBPrinter.h>

Inheritance diagram for klee::ExprSMTLIBPrinter:
Collaboration diagram for klee::ExprSMTLIBPrinter:

Public Types

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

Public Member Functions

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 ()
 
virtual void generateOutput ()
 
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

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 reset ()
 
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 printExpression (const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
 
virtual void scan (const ref< Expr > &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...
 

Protected Attributes

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

Private Member Functions

void negateQueryExpression ()
 This sets queryAssert to be the boolean negation of the original Query. More...
 
const char * getSMTLIBOptionString (ExprSMTLIBPrinter::SMTLIBboolOptions option)
 

Private Attributes

SMTLIBv2Logic logicToUse
 
volatile bool humanReadable
 
std::map< SMTLIBboolOptions, bool > smtlibBoolOptions
 
const std::vector< const Array * > * arraysToCallGetValueOn
 
ConstantDisplayMode cdm
 

Detailed Description

Base Class for SMTLIBv2 printer for KLEE Queries. It uses the QF_ABV logic. Note however the logic can be set to QF_AUFBV because some solvers (e.g. STP) complain if this logic is set to QF_ABV.

This printer does not abbreviate expressions. The printer ExprSMTLIBLetPrinter does though.

It is intended to be used as follows

  1. Create instance of this class
  2. Set output ( setOutput() )
  3. Set query to print ( setQuery() )
  4. Set options using the methods prefixed with the word "set".
  5. Call generateOutput()

The class can then be used again on another query ( setQuery() ). The options set are persistent across queries (apart from setArrayValuesToGet() and PRODUCE_MODELS).

Note that in KLEE at the lowest level the solver checks for validity of the query, i.e.

\[ \forall X constraints(X) \to query(X) \]

Where $X$ is some assignment, $constraints(X)$ are the constraints in the query and $query(X)$ is the query expression. If the above formula is true the query is said to be valid, otherwise it is invalid.

The SMTLIBv2 language works in terms of satisfiability rather than validity so instead this class must ask the equivalent query but in terms of satisfiability which is:

\[ \lnot \exists X constraints(X) \land \lnot query(X) \]

The printed SMTLIBv2 query actually asks the following:

\[ \exists X constraints(X) \land \lnot query(X) \]

Hence the printed SMTLIBv2 query will just assert the constraints and the negation of the query expression.

If a SMTLIBv2 solver says the printed query is satisfiable the then original query passed to this class was invalid and if a SMTLIBv2 solver says the printed query is unsatisfiable then the original query passed to this class was valid.

Definition at line 79 of file ExprSMTLIBPrinter.h.

Member Enumeration Documentation

Enumerator
BINARY 

Display bit vector constants in binary e.g. #b00101101.

HEX 

Display bit vector constants in Hexidecimal e.g.#x2D.

DECIMAL 

Display bit vector constants in Decimal e.g. (_ bv45 8)

Definition at line 106 of file ExprSMTLIBPrinter.h.

Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV.

Enumerator
SORT_BITVECTOR 
SORT_BOOL 

Definition at line 113 of file ExprSMTLIBPrinter.h.

Different SMTLIBv2 options that have a boolean value that can be set

See also
setSMTLIBboolOption
Enumerator
PRINT_SUCCESS 

print-success SMTLIBv2 option

PRODUCE_MODELS 

produce-models SMTLIBv2 option

INTERACTIVE_MODE 

interactive-mode SMTLIBv2 option

Definition at line 91 of file ExprSMTLIBPrinter.h.

Different SMTLIBv2 bool option values

See also
setSMTLIBboolOption
Enumerator
OPTION_TRUE 

Set option to true.

OPTION_FALSE 

Set option to false.

OPTION_DEFAULT 

Use solver's defaults (the option will not be set in output)

Definition at line 99 of file ExprSMTLIBPrinter.h.

Different SMTLIBv2 logics supported by this class

See also
setLogic()
Enumerator
QF_ABV 

Logic using Theory of Arrays and Theory of Bitvectors.

QF_AUFBV 

Logic using Theory of Arrays and Theory of Bitvectors and has uninterpreted functions

Definition at line 83 of file ExprSMTLIBPrinter.h.

Constructor & Destructor Documentation

klee::ExprSMTLIBPrinter::ExprSMTLIBPrinter ( )

Create a new printer that will print a query in the SMTLIBv2 language.

Definition at line 38 of file ExprSMTLIBPrinter.cpp.

References ExprSMTLIBOptions::argConstantDisplayMode(), and setConstantDisplayMode().

Here is the call graph for this function:

klee::ExprSMTLIBPrinter::~ExprSMTLIBPrinter ( )
virtual

Definition at line 46 of file ExprSMTLIBPrinter.cpp.

References p.

Member Function Documentation

void klee::ExprSMTLIBPrinter::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 in klee::ExprSMTLIBLetPrinter.

Definition at line 421 of file ExprSMTLIBPrinter.cpp.

References humanReadable, o, p, printAction(), printArrayDeclarations(), printConstraints(), printExit(), printNotice(), printOptions(), printQuery(), printSetLogic(), and query.

Referenced by klee::Executor::getConstraintLog(), and printInputAsSMTLIBv2().

Here is the call graph for this function:

Here is the caller graph for this function:

ConstantDisplayMode klee::ExprSMTLIBPrinter::getConstantDisplayMode ( )
inline

Definition at line 120 of file ExprSMTLIBPrinter.h.

References cdm.

const char * klee::ExprSMTLIBPrinter::getSMTLIBKeyword ( const ref< Expr > &  e)
protectedvirtual
const char * klee::ExprSMTLIBPrinter::getSMTLIBOptionString ( ExprSMTLIBPrinter::SMTLIBboolOptions  option)
private

Definition at line 888 of file ExprSMTLIBPrinter.cpp.

References INTERACTIVE_MODE, PRINT_SUCCESS, and PRODUCE_MODELS.

Referenced by printOptions().

Here is the caller graph for this function:

bool klee::ExprSMTLIBPrinter::isHumanReadable ( )
Returns
True if human readable mode is switched on

Definition at line 80 of file ExprSMTLIBPrinter.cpp.

References humanReadable.

Referenced by klee::ExprSMTLIBLetPrinter::generateOutput(), and klee::ExprSMTLIBLetPrinter::printLetExpression().

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::negateQueryExpression ( )
private

This sets queryAssert to be the boolean negation of the original Query.

Definition at line 834 of file ExprSMTLIBPrinter.cpp.

References klee::Expr::createIsZero(), klee::Query::expr, query, and queryAssert.

Referenced by setQuery().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printAction ( )
protectedvirtual

Print the SMTLIBv2 command to check satisfiability and also optionally request for values

See also
setArrayValuesToGet()

Definition at line 544 of file ExprSMTLIBPrinter.cpp.

References arraysToCallGetValueOn, klee::Array::getDomain(), o, and klee::Array::size.

Referenced by klee::ExprSMTLIBLetPrinter::generateOutput(), and generateOutput().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printArrayDeclarations ( )
protectedvirtual
void klee::ExprSMTLIBPrinter::printCastExpr ( const ref< CastExpr > &  e)
protectedvirtual

Definition at line 256 of file ExprSMTLIBPrinter.cpp.

References getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BITVECTOR.

Referenced by printExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printCastToSort ( const ref< Expr > &  e,
ExprSMTLIBPrinter::SMTLIB_SORT  sort 
)
protected

Print an expression but cast it to a particular SMTLIBv2 sort first.

Definition at line 693 of file ExprSMTLIBPrinter.cpp.

References klee::Expr::Bool, PrintContext::breakLine(), PrintContext::breakLineI(), klee::Expr::getWidth(), humanReadable, p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), SORT_BITVECTOR, and SORT_BOOL.

Referenced by klee::ExprSMTLIBLetPrinter::printExpression(), and printExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printConstant ( const ref< ConstantExpr > &  e)
protected

Print a Constant in the format specified by the current "Constant Display Mode"

Definition at line 90 of file ExprSMTLIBPrinter.cpp.

References BINARY, cdm, DECIMAL, HEX, and p.

Referenced by printArrayDeclarations(), and printExpression().

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printConstraints ( )
protectedvirtual
void klee::ExprSMTLIBPrinter::printExit ( )
protectedvirtual

Print the SMTLIBv2 command to exit.

Definition at line 607 of file ExprSMTLIBPrinter.cpp.

References o.

Referenced by klee::ExprSMTLIBLetPrinter::generateOutput(), and generateOutput().

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printExtractExpr ( const ref< ExtractExpr > &  e)
protectedvirtual

Definition at line 238 of file ExprSMTLIBPrinter.cpp.

References getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BITVECTOR.

Referenced by printExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printLogicalOrBitVectorExpr ( const ref< Expr > &  e,
ExprSMTLIBPrinter::SMTLIB_SORT  s 
)
protectedvirtual

For the set of operators that come in two sorts (e.g. (and () ()) (bvand () ()) ) These are and,xor,or,not

Parameters
ethe Expression to print
sthe sort of the expression we want

Definition at line 794 of file ExprSMTLIBPrinter.cpp.

References klee::Expr::And, klee::Expr::getKid(), klee::Expr::getKind(), klee::Expr::getNumKids(), klee::Expr::Not, klee::Expr::Or, p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), SORT_BITVECTOR, and klee::Expr::Xor.

Referenced by printExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printNotEqualExpr ( const ref< NeExpr > &  e)
protectedvirtual

Definition at line 287 of file ExprSMTLIBPrinter.cpp.

References getSort(), p, PrintContext::popIndent(), printExpression(), printSeperator(), and PrintContext::pushIndent().

Referenced by printExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printNotice ( )
protectedvirtual

Definition at line 624 of file ExprSMTLIBPrinter.cpp.

References o.

Referenced by klee::ExprSMTLIBLetPrinter::generateOutput(), and generateOutput().

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printOptions ( )
protectedvirtual

Definition at line 630 of file ExprSMTLIBPrinter.cpp.

References getSMTLIBOptionString(), o, and smtlibBoolOptions.

Referenced by klee::ExprSMTLIBLetPrinter::generateOutput(), and generateOutput().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printQuery ( )
protectedvirtual

Definition at line 640 of file ExprSMTLIBPrinter.cpp.

References PrintContext::breakLineI(), humanReadable, p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), queryAssert, and SORT_BOOL.

Referenced by generateOutput().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printReadExpr ( const ref< ReadExpr > &  e)
protectedvirtual

Definition at line 220 of file ExprSMTLIBPrinter.cpp.

References getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), printUpdatesAndArray(), PrintContext::pushIndent(), and SORT_BITVECTOR.

Referenced by printExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printSelectExpr ( const ref< SelectExpr > &  e,
ExprSMTLIBPrinter::SMTLIB_SORT  s 
)
protectedvirtual

Definition at line 750 of file ExprSMTLIBPrinter.cpp.

References getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BOOL.

Referenced by printExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printSeperator ( )
protectedvirtual
void klee::ExprSMTLIBPrinter::printSetLogic ( )
protectedvirtual

Definition at line 439 of file ExprSMTLIBPrinter.cpp.

References logicToUse, o, QF_ABV, and QF_AUFBV.

Referenced by klee::ExprSMTLIBLetPrinter::generateOutput(), and generateOutput().

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printSortArgsExpr ( const ref< Expr > &  e,
ExprSMTLIBPrinter::SMTLIB_SORT  s 
)
protectedvirtual

Definition at line 778 of file ExprSMTLIBPrinter.cpp.

References klee::Expr::getKid(), klee::Expr::getNumKids(), getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), and PrintContext::pushIndent().

Referenced by printExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::printUpdatesAndArray ( const UpdateNode un,
const Array root 
)
protectedvirtual

Recursively prints updatesNodes.

Definition at line 383 of file ExprSMTLIBPrinter.cpp.

References klee::UpdateNode::index, klee::Array::name, klee::UpdateNode::next, p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), SORT_BITVECTOR, and klee::UpdateNode::value.

Referenced by printReadExpr().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::reset ( )
protectedvirtual

Reimplemented in klee::ExprSMTLIBLetPrinter.

Definition at line 66 of file ExprSMTLIBPrinter.cpp.

References arraysToCallGetValueOn, haveConstantArray, OPTION_DEFAULT, PRODUCE_MODELS, setSMTLIBboolOption(), and usedArrays.

Referenced by klee::ExprSMTLIBLetPrinter::reset(), and setQuery().

Here is the call graph for this function:

Here is the caller graph for this function:

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

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

Reimplemented in klee::ExprSMTLIBLetPrinter.

Definition at line 569 of file ExprSMTLIBPrinter.cpp.

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

Referenced by scanAll(), and scanUpdates().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::scanAll ( )
protectedvirtual

Definition at line 411 of file ExprSMTLIBPrinter.cpp.

References klee::ConstraintManager::begin(), klee::Query::constraints, klee::ConstraintManager::end(), klee::Query::expr, query, and scan().

Referenced by setQuery().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::scanUpdates ( const UpdateNode un)
protectedvirtual

Helper function for scan() that scans the expressions of an update node.

Definition at line 599 of file ExprSMTLIBPrinter.cpp.

References klee::UpdateNode::index, klee::UpdateNode::next, scan(), and klee::UpdateNode::value.

Referenced by klee::ExprSMTLIBLetPrinter::scan(), and scan().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::setArrayValuesToGet ( const std::vector< const Array * > &  a)

Set the array names that the SMTLIBv2 solver will be asked to determine. Calling this method implies the PRODUCE_MODELS option is true and will change any previously set value.

If no call is made to this function before ExprSMTLIBPrinter::generateOutput() then the solver will only be asked to check satisfiability.

If the passed vector is not empty then the values of those arrays will be requested via (get-value ()) SMTLIBv2 command in the output stream in the same order as vector.

Definition at line 869 of file ExprSMTLIBPrinter.cpp.

References arraysToCallGetValueOn, OPTION_TRUE, PRODUCE_MODELS, setSMTLIBboolOption(), and usedArrays.

Referenced by printInputAsSMTLIBv2().

Here is the call graph for this function:

Here is the caller graph for this function:

bool klee::ExprSMTLIBPrinter::setConstantDisplayMode ( ConstantDisplayMode  cdm)

Allows the way Constant bitvectors are printed to be changed. This setting is persistent across queries.

Returns
true if setting the mode was successful

Definition at line 82 of file ExprSMTLIBPrinter.cpp.

References cdm, and DECIMAL.

Referenced by ExprSMTLIBPrinter().

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::setHumanReadable ( bool  hr)

Sets how readable the printed SMTLIBv2 commands are.

Parameters
hrIf set to true the printed commands are made more human readable.

The printed commands are made human readable by...

  • Indenting and line breaking.
  • Adding comments

Definition at line 628 of file ExprSMTLIBPrinter.cpp.

References humanReadable.

bool klee::ExprSMTLIBPrinter::setLogic ( SMTLIBv2Logic  l)

Set which SMTLIBv2 logic to use. This only affects what logic is used in the (set-logic <logic>) command. The rest of the printed SMTLIBv2 commands are the same regardless of the logic used.

Returns
true if setting logic was successful.

Definition at line 609 of file ExprSMTLIBPrinter.cpp.

References logicToUse, and QF_AUFBV.

void klee::ExprSMTLIBPrinter::setOutput ( llvm::raw_ostream &  output)

Set the output stream that will be printed to. This call is persistent across queries.

Definition at line 51 of file ExprSMTLIBPrinter.cpp.

References o, and p.

Referenced by klee::Executor::getConstraintLog(), and printInputAsSMTLIBv2().

Here is the caller graph for this function:

void klee::ExprSMTLIBPrinter::setQuery ( const Query q)

Set the query to print. This will setArrayValuesToGet() to none (i.e. no array values will be requested using the SMTLIBv2 (get-value ()) command).

Definition at line 59 of file ExprSMTLIBPrinter.cpp.

References negateQueryExpression(), query, reset(), and scanAll().

Referenced by klee::Executor::getConstraintLog(), and printInputAsSMTLIBv2().

Here is the call graph for this function:

Here is the caller graph for this function:

bool klee::ExprSMTLIBPrinter::setSMTLIBboolOption ( SMTLIBboolOptions  option,
SMTLIBboolValues  value 
)

Set SMTLIB options. These options will be printed when generateOutput() is called via the SMTLIBv2 command (set-option :option-name

)

By default no options will be printed so the SMTLIBv2 solver will use its default values for all options.

Returns
true if option was successfully set.

The options set are persistent across calls to setQuery() apart from the PRODUCE_MODELS option which this printer may automatically set/unset.

Definition at line 839 of file ExprSMTLIBPrinter.cpp.

References INTERACTIVE_MODE, OPTION_DEFAULT, OPTION_TRUE, PRINT_SUCCESS, PRODUCE_MODELS, and smtlibBoolOptions.

Referenced by reset(), and setArrayValuesToGet().

Here is the caller graph for this function:

Member Data Documentation

const std::vector<const Array *>* klee::ExprSMTLIBPrinter::arraysToCallGetValueOn
private

Definition at line 342 of file ExprSMTLIBPrinter.h.

Referenced by printAction(), reset(), and setArrayValuesToGet().

ConstantDisplayMode klee::ExprSMTLIBPrinter::cdm
private
bool klee::ExprSMTLIBPrinter::haveConstantArray
protected

Indicates if there were any constant arrays founds during a scan()

Definition at line 323 of file ExprSMTLIBPrinter.h.

Referenced by printArrayDeclarations(), reset(), klee::ExprSMTLIBLetPrinter::scan(), and scan().

volatile bool klee::ExprSMTLIBPrinter::humanReadable
private
SMTLIBv2Logic klee::ExprSMTLIBPrinter::logicToUse
private

Definition at line 326 of file ExprSMTLIBPrinter.h.

Referenced by printSetLogic(), and setLogic().

llvm::raw_ostream* klee::ExprSMTLIBPrinter::o
protected
const Query* klee::ExprSMTLIBPrinter::query
protected
ref<Expr> klee::ExprSMTLIBPrinter::queryAssert
protected

This contains the query from the solver but negated for our purposes.

See also
negateQueryExpression()

Definition at line 320 of file ExprSMTLIBPrinter.h.

Referenced by negateQueryExpression(), klee::ExprSMTLIBLetPrinter::printLetExpression(), and printQuery().

std::map<SMTLIBboolOptions, bool> klee::ExprSMTLIBPrinter::smtlibBoolOptions
private

Definition at line 331 of file ExprSMTLIBPrinter.h.

Referenced by printOptions(), and setSMTLIBboolOption().

std::set<const Array *> klee::ExprSMTLIBPrinter::usedArrays
protected

Contains the arrays found during scans.

Definition at line 205 of file ExprSMTLIBPrinter.h.

Referenced by printArrayDeclarations(), reset(), klee::ExprSMTLIBLetPrinter::scan(), scan(), and setArrayValuesToGet().


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