diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-12-02 13:33:01 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-12-02 18:39:04 +0000 |
commit | 03c58b5c78206e17164c4c9ef35ab133de63e705 (patch) | |
tree | f74daa6a7eb2009c62af7a74b14b7b1b2e61df35 /include | |
parent | 591b3d4715327b25d09f57a7198d48ed7174a017 (diff) | |
download | klee-03c58b5c78206e17164c4c9ef35ab133de63e705.tar.gz |
The printing of constraints and the QueryExpr have been merged into a
single method with two different implementations. There is one version of this method for human readability (printHumanReadableQuery()) and a version for machine consumption (printMachineReadableQuery()). The reason for having two versions is because different behaviour is needed in different scenarios * In machine readable mode the entire query is printed inside a single ``(assert ...)``. This is done to allow ``(let ...)`` to abbreviate as much as possible. * In human readable mode each constraint and query expression is printed inside its own ``(assert ...)`` unless the abbreviation mode is ABBR_LET in which case all constraints and query expr are printed inside a single ``(assert ...)`` much like in the machine readable mode Whilst I was here I also fixed a bug handling identation when printing ``(let ...)`` expressions in printAssert()
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h index ff024e11..48d300eb 100644 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -253,11 +253,15 @@ protected: // Print SMTLIBv2 assertions for constant arrays void printArrayDeclarations(); - // Print SMTLIBv2 for all constraints in the query - void printConstraints(); + // Print SMTLIBv2 for the query optimised for human readability + void printHumanReadableQuery(); - // Print SMTLIBv2 assert statement for the negated query expression - void printQueryExpr(); + // Print SMTLIBv2 for the query optimised for minimal query size. + // This does not imply ABBR_LET or ABBR_NAMED (although it would be wise + // to use them to minimise the query size further) + void printMachineReadableQuery(); + + void printQueryInSingleAssert(); /// Print the SMTLIBv2 command to check satisfiability and also optionally /// request for values |