Patch by Dan Liew: "Improve the doxygen comments for ExprSMTLIBPrinter"

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@181444 91177308-0d34-0410-b5e6-96231b3b80d8

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: