diff options
| -rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 54 |
1 files changed, 40 insertions, 14 deletions
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h index 588d9d19..2dc65438 100644 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -21,20 +21,46 @@ namespace klee { - ///Base Class for SMTLIBv2 printer for Expr trees. 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 - /// -# Create instance of this class - /// -# Set output ( setOutput() ) - /// -# Set query to print ( setQuery() ) - /// -# Set options using the methods prefixed with the word "set". - /// -# 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) + ///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 + /// -# Create instance of this class + /// -# Set output ( setOutput() ) + /// -# Set query to print ( setQuery() ) + /// -# Set options using the methods prefixed with the word "set". + /// -# 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. + /// + /// \f[ \forall X constraints(X) \to query(X) \f] + /// + /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints + /// in the query and \f$query(X)\f$ 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: + /// + /// \f[ \lnot \exists X constraints(X) \land \lnot query(X) \f] + /// + /// The printed SMTLIBv2 query actually asks the following: + /// + /// \f[ \exists X constraints(X) \land \lnot query(X) \f] + /// 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**. + /// class ExprSMTLIBPrinter { public: |