klee
|
#include <ExprSMTLIBPrinter.h>
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 | AbbreviationMode { ABBR_NONE , ABBR_LET , ABBR_NAMED } |
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 () |
void | setAbbreviationMode (AbbreviationMode am) |
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) |
~ExprSMTLIBPrinter () | |
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 Types | |
typedef std::map< const ref< Expr >, int > | BindingMap |
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... | |
void | reset () |
void | scanAll () |
void | printNotice () |
void | printOptions () |
void | printSetLogic () |
void | printArrayDeclarations () |
void | printHumanReadableQuery () |
void | printMachineReadableQuery () |
void | printQueryInSingleAssert () |
void | printAction () |
void | printExit () |
Print the SMTLIBv2 command to exit. More... | |
void | printConstant (const ref< ConstantExpr > &e) |
void | printExpression (const ref< Expr > &e, SMTLIB_SORT expectedSort) |
void | scan (const ref< Expr > &e) |
void | scanBindingExprDeps () |
void | printReadExpr (const ref< ReadExpr > &e) |
void | printExtractExpr (const ref< ExtractExpr > &e) |
void | printCastExpr (const ref< CastExpr > &e) |
void | printNotEqualExpr (const ref< NeExpr > &e) |
void | printSelectExpr (const ref< SelectExpr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s) |
void | printAShrExpr (const ref< AShrExpr > &e) |
void | printSortArgsExpr (const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s) |
void | printLogicalOrBitVectorExpr (const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s) |
void | printUpdatesAndArray (const UpdateNode *un, const Array *root) |
Recursively prints updatesNodes. More... | |
const char * | getSMTLIBKeyword (const ref< Expr > &e) |
void | printSeperator () |
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... | |
std::set< ref< Expr > > | seenExprs |
Set of expressions seen during scan. More... | |
BindingMap | bindings |
std::vector< BindingMap > | orderedBindings |
llvm::raw_ostream * | o |
Output stream to write to. More... | |
const Query * | query |
The query to print. More... | |
PrintContext * | p |
Helper printer class. More... | |
ref< Expr > | queryAssert |
bool | haveConstantArray |
Indicates if there were any constant arrays founds during a scan() More... | |
Private Member Functions | |
const char * | getSMTLIBOptionString (ExprSMTLIBPrinter::SMTLIBboolOptions option) |
void | printFullExpression (const ref< Expr > &e, SMTLIB_SORT expectedSort) |
Print expression without top-level abbreviations. More... | |
void | printAssert (const ref< Expr > &e) |
Print an assert statement for the given expr. More... | |
Private Attributes | |
SMTLIBv2Logic | logicToUse |
volatile bool | humanReadable |
std::map< SMTLIBboolOptions, bool > | smtlibBoolOptions |
const std::vector< const Array * > * | arraysToCallGetValueOn |
ConstantDisplayMode | cdm |
AbbreviationMode | abbrMode |
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 abbreviates expressions according to its abbreviation mode.
It is intended to be used as follows
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.
Where is some assignment,
are the constraints in the query and
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:
The printed SMTLIBv2 query actually asks the following:
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.
|
protected |
Definition at line 220 of file ExprSMTLIBPrinter.h.
How to abbreviate repeatedly mentioned expressions. Some solvers do not understand all of them, hence the flexibility.
Enumerator | |
---|---|
ABBR_NONE | Do not abbreviate. |
ABBR_LET | Abbreviate with let. |
ABBR_NAMED | Abbreviate with :named annotations. |
Definition at line 114 of file ExprSMTLIBPrinter.h.
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 121 of file ExprSMTLIBPrinter.h.
Different SMTLIBv2 options that have a boolean value that can be set
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
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
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.
klee::ExprSMTLIBPrinter::ExprSMTLIBPrinter | ( | ) |
Create a new printer that will print a query in the SMTLIBv2 language.
Definition at line 56 of file ExprSMTLIBPrinter.cpp.
References ExprSMTLIBOptions::abbreviationMode(), ExprSMTLIBOptions::argConstantDisplayMode(), setAbbreviationMode(), and setConstantDisplayMode().
klee::ExprSMTLIBPrinter::~ExprSMTLIBPrinter | ( | ) |
Definition at line 65 of file ExprSMTLIBPrinter.cpp.
References p.
void klee::ExprSMTLIBPrinter::generateOutput | ( | ) |
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.
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.
Definition at line 517 of file ExprSMTLIBPrinter.cpp.
References humanReadable, o, p, printAction(), printArrayDeclarations(), printExit(), printHumanReadableQuery(), printMachineReadableQuery(), printNotice(), printOptions(), printSetLogic(), and query.
Referenced by klee::Executor::getConstraintLog(), printInputAsSMTLIBv2(), and SMTLIBLoggingSolver::printQuery().
|
inline |
Definition at line 128 of file ExprSMTLIBPrinter.h.
References cdm.
This method does the translation between Expr classes and SMTLIBv2 keywords
Definition at line 407 of file ExprSMTLIBPrinter.cpp.
References klee::Expr::Add, klee::Expr::Concat, klee::Expr::Eq, klee::Expr::Extract, klee::Expr::getKind(), klee::Expr::LShr, klee::Expr::Mul, klee::Expr::Ne, klee::Expr::Read, klee::Expr::SDiv, klee::Expr::Select, klee::Expr::SExt, klee::Expr::Sge, klee::Expr::Sgt, klee::Expr::Shl, klee::Expr::Sle, klee::Expr::Slt, klee::Expr::SRem, klee::Expr::Sub, klee::Expr::UDiv, klee::Expr::Uge, klee::Expr::Ugt, klee::Expr::Ule, klee::Expr::Ult, klee::Expr::URem, and klee::Expr::ZExt.
Referenced by printCastExpr(), printExtractExpr(), printReadExpr(), printSelectExpr(), and printSortArgsExpr().
|
private |
Definition at line 1153 of file ExprSMTLIBPrinter.cpp.
References INTERACTIVE_MODE, PRINT_SUCCESS, and PRODUCE_MODELS.
Referenced by printOptions().
|
protected |
Determine the SMTLIBv2 sort of the expression.
Definition at line 930 of file ExprSMTLIBPrinter.cpp.
References klee::Expr::And, klee::Expr::Bool, klee::Expr::Constant, klee::Expr::Eq, klee::Expr::getKid(), klee::Expr::getKind(), getSort(), klee::Expr::getWidth(), klee::Expr::Ne, klee::Expr::Not, klee::Expr::NotOptimized, klee::Expr::Or, klee::Expr::Sge, klee::Expr::Sgt, klee::Expr::Sle, klee::Expr::Slt, SORT_BITVECTOR, SORT_BOOL, klee::Expr::Uge, klee::Expr::Ugt, klee::Expr::Ule, klee::Expr::Ult, and klee::Expr::Xor.
Referenced by getSort(), printAssert(), printExpression(), and printFullExpression().
bool klee::ExprSMTLIBPrinter::isHumanReadable | ( | ) |
Definition at line 99 of file ExprSMTLIBPrinter.cpp.
References humanReadable.
|
protected |
Print the SMTLIBv2 command to check satisfiability and also optionally request for values
Definition at line 667 of file ExprSMTLIBPrinter.cpp.
References arraysToCallGetValueOn, klee::Array::getDomain(), o, and klee::Array::size.
Referenced by generateOutput().
|
protected |
Definition at line 562 of file ExprSMTLIBPrinter.cpp.
References PrintContext::breakLineI(), klee::Array::constantValues, klee::Array::getDomain(), haveConstantArray, humanReadable, klee::Array::isConstantArray(), klee::Array::name, o, p, PrintContext::popIndent(), printConstant(), printSeperator(), PrintContext::pushIndent(), and usedArrays.
Referenced by generateOutput().
|
protected |
Definition at line 340 of file ExprSMTLIBPrinter.cpp.
References klee::ConstantExpr::create(), p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BITVECTOR.
Referenced by printFullExpression().
Print an assert statement for the given expr.
Definition at line 859 of file ExprSMTLIBPrinter.cpp.
References ABBR_LET, abbrMode, bindings, PrintContext::breakLineI(), getSort(), orderedBindings, p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BOOL.
Referenced by printHumanReadableQuery(), and printQueryInSingleAssert().
Definition at line 309 of file ExprSMTLIBPrinter.cpp.
References getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BITVECTOR.
Referenced by printFullExpression().
|
protected |
Print an expression but cast it to a particular SMTLIBv2 sort first.
Definition at line 963 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 printExpression().
|
protected |
Print a Constant in the format specified by the current "Constant Display Mode"
Definition at line 109 of file ExprSMTLIBPrinter.cpp.
References BINARY, cdm, DECIMAL, HEX, and p.
Referenced by printArrayDeclarations(), and printFullExpression().
|
protected |
Print the SMTLIBv2 command to exit.
Definition at line 826 of file ExprSMTLIBPrinter.cpp.
References o.
Referenced by generateOutput().
|
protected |
Recursively print expression
e | is the expression to print |
expectedSort | is the sort we want. If "e" is not of the right type a cast will be performed. |
abbrMode | the abbreviation mode to use for this expression |
Definition at line 167 of file ExprSMTLIBPrinter.cpp.
References ABBR_LET, ABBR_NAMED, ABBR_NONE, abbrMode, bindings, getSort(), p, printCastToSort(), and printFullExpression().
Referenced by printAShrExpr(), printAssert(), printCastExpr(), printCastToSort(), printExtractExpr(), printFullExpression(), printLogicalOrBitVectorExpr(), printReadExpr(), printSelectExpr(), printSortArgsExpr(), and printUpdatesAndArray().
|
protected |
Definition at line 291 of file ExprSMTLIBPrinter.cpp.
References getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BITVECTOR.
Referenced by printFullExpression().
|
private |
Print expression without top-level abbreviations.
Definition at line 208 of file ExprSMTLIBPrinter.cpp.
References klee::Expr::And, klee::Expr::AShr, klee::Expr::Constant, klee::Expr::Eq, klee::Expr::Extract, klee::Expr::getKid(), klee::Expr::getKind(), getSort(), klee::Expr::Ne, klee::Expr::Not, klee::Expr::NotOptimized, klee::Expr::Or, printAShrExpr(), printCastExpr(), printConstant(), printExpression(), printExtractExpr(), printLogicalOrBitVectorExpr(), printReadExpr(), printSelectExpr(), printSortArgsExpr(), klee::Expr::Read, klee::Expr::Select, klee::Expr::SExt, SORT_BITVECTOR, klee::Expr::Xor, and klee::Expr::ZExt.
Referenced by printExpression().
|
protected |
Definition at line 623 of file ExprSMTLIBPrinter.cpp.
References ABBR_LET, abbrMode, klee::Query::constraints, klee::Expr::createIsZero(), klee::Query::expr, humanReadable, o, printAssert(), printQueryInSingleAssert(), query, and queryAssert.
Referenced by generateOutput().
|
protected |
For the set of operators that come in two sorts (e.g. (and () ()) (bvand () ()) ) These are and,xor,or,not
e | the Expression to print |
s | the sort of the expression we want |
Definition at line 1064 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 printFullExpression().
|
protected |
Definition at line 645 of file ExprSMTLIBPrinter.cpp.
References humanReadable, and printQueryInSingleAssert().
Referenced by generateOutput().
|
protected |
|
protected |
Definition at line 843 of file ExprSMTLIBPrinter.cpp.
References o.
Referenced by generateOutput().
|
protected |
Definition at line 849 of file ExprSMTLIBPrinter.cpp.
References getSMTLIBOptionString(), o, and smtlibBoolOptions.
Referenced by generateOutput().
|
protected |
Definition at line 651 of file ExprSMTLIBPrinter.cpp.
References klee::ConstraintSet::begin(), klee::Query::constraints, klee::Expr::createIsZero(), klee::ConstraintSet::end(), klee::Query::expr, printAssert(), query, and queryAssert.
Referenced by printHumanReadableQuery(), and printMachineReadableQuery().
Definition at line 273 of file ExprSMTLIBPrinter.cpp.
References klee::ref< T >::get(), getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), printUpdatesAndArray(), PrintContext::pushIndent(), and SORT_BITVECTOR.
Referenced by printFullExpression().
|
protected |
Definition at line 1020 of file ExprSMTLIBPrinter.cpp.
References getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BOOL.
Referenced by printFullExpression().
|
protected |
Definition at line 836 of file ExprSMTLIBPrinter.cpp.
References PrintContext::breakLineI(), humanReadable, p, and PrintContext::write().
Referenced by printArrayDeclarations(), printAShrExpr(), printAssert(), printCastExpr(), printCastToSort(), printExtractExpr(), printLogicalOrBitVectorExpr(), printReadExpr(), printSelectExpr(), printSortArgsExpr(), and printUpdatesAndArray().
|
protected |
Definition at line 539 of file ExprSMTLIBPrinter.cpp.
References logicToUse, o, QF_ABV, and QF_AUFBV.
Referenced by generateOutput().
|
protected |
Definition at line 1048 of file ExprSMTLIBPrinter.cpp.
References klee::Expr::getKid(), klee::Expr::getNumKids(), getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), and PrintContext::pushIndent().
Referenced by printFullExpression().
|
protected |
Recursively prints updatesNodes.
Definition at line 476 of file ExprSMTLIBPrinter.cpp.
References klee::UpdateNode::index, klee::Array::name, klee::UpdateNode::next, p, PrintContext::popIndent(), printExpression(), printSeperator(), printUpdatesAndArray(), PrintContext::pushIndent(), SORT_BITVECTOR, and klee::UpdateNode::value.
Referenced by printReadExpr(), and printUpdatesAndArray().
|
protected |
Definition at line 82 of file ExprSMTLIBPrinter.cpp.
References arraysToCallGetValueOn, bindings, haveConstantArray, OPTION_DEFAULT, orderedBindings, PRODUCE_MODELS, seenExprs, setSMTLIBboolOption(), and usedArrays.
Referenced by setQuery().
Scan Expression recursively for Arrays in expressions. Found arrays are added to the usedArrays vector.
Definition at line 692 of file ExprSMTLIBPrinter.cpp.
References bindings, klee::ref< T >::get(), klee::Expr::getKid(), klee::Expr::getNumKids(), haveConstantArray, scan(), scanUpdates(), seenExprs, and usedArrays.
Referenced by scan(), scanAll(), and scanUpdates().
|
protected |
Definition at line 504 of file ExprSMTLIBPrinter.cpp.
References ABBR_LET, abbrMode, klee::Query::constraints, klee::Query::expr, query, scan(), and scanBindingExprDeps().
Referenced by setQuery().
|
protected |
Scan bindings for expression intra-dependencies. The result is written to the orderedBindings vector that is later used for nested expression printing in the let abbreviation mode.
Definition at line 726 of file ExprSMTLIBPrinter.cpp.
References bindings, klee::Expr::getKid(), klee::Expr::getNumKids(), and orderedBindings.
Referenced by scanAll().
|
protected |
Helper function for scan() that scans the expressions of an update node.
Definition at line 818 of file ExprSMTLIBPrinter.cpp.
References klee::UpdateNode::index, klee::UpdateNode::next, scan(), and klee::UpdateNode::value.
Referenced by scan().
|
inline |
Definition at line 130 of file ExprSMTLIBPrinter.h.
References abbrMode.
Referenced by ExprSMTLIBPrinter().
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 1134 of file ExprSMTLIBPrinter.cpp.
References arraysToCallGetValueOn, OPTION_TRUE, PRODUCE_MODELS, setSMTLIBboolOption(), and usedArrays.
Referenced by printInputAsSMTLIBv2(), and SMTLIBLoggingSolver::printQuery().
bool klee::ExprSMTLIBPrinter::setConstantDisplayMode | ( | ConstantDisplayMode | cdm | ) |
Allows the way Constant bitvectors are printed to be changed. This setting is persistent across queries.
Definition at line 101 of file ExprSMTLIBPrinter.cpp.
Referenced by ExprSMTLIBPrinter().
void klee::ExprSMTLIBPrinter::setHumanReadable | ( | bool | hr | ) |
Sets how readable the printed SMTLIBv2 commands are.
hr | If set to true the printed commands are made more human readable. |
The printed commands are made human readable by...
Definition at line 847 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.
Definition at line 828 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 69 of file ExprSMTLIBPrinter.cpp.
Referenced by klee::Executor::getConstraintLog(), printInputAsSMTLIBv2(), and SMTLIBLoggingSolver::SMTLIBLoggingSolver().
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 76 of file ExprSMTLIBPrinter.cpp.
References query, reset(), and scanAll().
Referenced by klee::Executor::getConstraintLog(), printInputAsSMTLIBv2(), and SMTLIBLoggingSolver::printQuery().
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.
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 1104 of file ExprSMTLIBPrinter.cpp.
References INTERACTIVE_MODE, OPTION_DEFAULT, OPTION_TRUE, PRINT_SUCCESS, PRODUCE_MODELS, and smtlibBoolOptions.
Referenced by reset(), and setArrayValuesToGet().
|
private |
Definition at line 383 of file ExprSMTLIBPrinter.h.
Referenced by printAssert(), printExpression(), printHumanReadableQuery(), scanAll(), and setAbbreviationMode().
|
private |
Definition at line 380 of file ExprSMTLIBPrinter.h.
Referenced by printAction(), reset(), and setArrayValuesToGet().
|
protected |
Let expression binding number map. Under the :named abbreviation mode, negative binding numbers indicate that the abbreviation has already been emitted, so it may be used.
Definition at line 225 of file ExprSMTLIBPrinter.h.
Referenced by printAssert(), printExpression(), reset(), scan(), and scanBindingExprDeps().
|
private |
Definition at line 382 of file ExprSMTLIBPrinter.h.
Referenced by getConstantDisplayMode(), printConstant(), and setConstantDisplayMode().
|
protected |
Indicates if there were any constant arrays founds during a scan()
Definition at line 358 of file ExprSMTLIBPrinter.h.
Referenced by printArrayDeclarations(), reset(), and scan().
|
private |
Definition at line 363 of file ExprSMTLIBPrinter.h.
Referenced by generateOutput(), isHumanReadable(), printArrayDeclarations(), printCastToSort(), printHumanReadableQuery(), printMachineReadableQuery(), printSeperator(), and setHumanReadable().
|
private |
Definition at line 361 of file ExprSMTLIBPrinter.h.
Referenced by printSetLogic(), and setLogic().
|
protected |
Output stream to write to.
Definition at line 233 of file ExprSMTLIBPrinter.h.
Referenced by generateOutput(), printAction(), printArrayDeclarations(), printExit(), printHumanReadableQuery(), printNotice(), printOptions(), printSetLogic(), and setOutput().
|
protected |
An ordered list of expression bindings. Exprs in BindingMap at index i depend on Exprs in BindingMap at i-1. Exprs in orderedBindings[0] have no dependencies.
Definition at line 230 of file ExprSMTLIBPrinter.h.
Referenced by printAssert(), reset(), and scanBindingExprDeps().
|
protected |
Helper printer class.
Definition at line 351 of file ExprSMTLIBPrinter.h.
Referenced by generateOutput(), printArrayDeclarations(), printAShrExpr(), printAssert(), printCastExpr(), printCastToSort(), printConstant(), printExpression(), printExtractExpr(), printLogicalOrBitVectorExpr(), printReadExpr(), printSelectExpr(), printSeperator(), printSortArgsExpr(), printUpdatesAndArray(), setOutput(), and ~ExprSMTLIBPrinter().
|
protected |
The query to print.
Definition at line 236 of file ExprSMTLIBPrinter.h.
Referenced by generateOutput(), printHumanReadableQuery(), printQueryInSingleAssert(), scanAll(), and setQuery().
This contains the query from the solver but negated for our purposes.
Definition at line 355 of file ExprSMTLIBPrinter.h.
Referenced by printHumanReadableQuery(), and printQueryInSingleAssert().
Set of expressions seen during scan.
Definition at line 218 of file ExprSMTLIBPrinter.h.
|
private |
Definition at line 366 of file ExprSMTLIBPrinter.h.
Referenced by printOptions(), and setSMTLIBboolOption().
|
protected |
Contains the arrays found during scans.
Definition at line 215 of file ExprSMTLIBPrinter.h.
Referenced by printArrayDeclarations(), reset(), scan(), and setArrayValuesToGet().