diff options
Diffstat (limited to 'include/klee/util/ExprSMTLIBPrinter.h')
-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 |