about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2014-12-02 13:33:01 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2014-12-02 18:39:04 +0000
commit03c58b5c78206e17164c4c9ef35ab133de63e705 (patch)
treef74daa6a7eb2009c62af7a74b14b7b1b2e61df35 /include
parent591b3d4715327b25d09f57a7198d48ed7174a017 (diff)
downloadklee-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.h12
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