Patch by Dan Liew (with a few changes by me) that improves the Doxygen documentation for Solver/SolverImpl.

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

2 files changed, 87 insertions, 16 deletions

diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 46925164..1af30870 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -67,27 +67,53 @@ namespace klee {
     Solver(SolverImpl *_impl) : impl(_impl) {}
     virtual ~Solver();
 
-    /// evaluate - Determine the full validity of an expression in particular
-    /// state.
-    ////
-    /// \param [out] result - The validity of the given expression (provably
-    /// true, provably false, or neither).
+    /// evaluate - Determine for a particular state if the query
+    /// expression is provably true, provably false or neither.
+    ///
+    /// \param [out] result - if
+    /// \f[ \forall X constraints(X) \to query(X) \f]
+    /// then Solver::True,
+    /// else if
+    /// \f[ \forall X constraints(X) \to \lnot query(X) \f]
+    /// then Solver::False,
+    /// else
+    /// Solver::Unknown
     ///
     /// \return True on success.
     bool evaluate(const Query&, Validity &result);
   
     /// mustBeTrue - Determine if the expression is provably true.
+    /// 
+    /// This evaluates the following logical formula:
+    ///
+    /// \f[ \forall X constraints(X) \to query(X) \f]
+    ///
+    /// which is equivalent to
     ///
-    /// \param [out] result - On success, true iff the expresssion is provably
-    /// false.
+    /// \f[ \lnot \exists X constraints(X) \land \lnot 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.
+    ///
+    /// \param [out] result - On success, true iff the logical formula is true
     ///
     /// \return True on success.
     bool mustBeTrue(const Query&, bool &result);
 
     /// mustBeFalse - Determine if the expression is provably false.
     ///
-    /// \param [out] result - On success, true iff the expresssion is provably
-    /// false.
+    /// This evaluates the following logical formula:
+    ///
+    /// \f[ \lnot \exists X constraints(X) \land query(X) \f]
+    ///
+    /// which is equivalent to
+    ///
+    ///  \f[ \forall X constraints(X) \to \lnot 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.
+    ///
+    /// \param [out] result - On success, true iff the logical formula is false
     ///
     /// \return True on success.
     bool mustBeFalse(const Query&, bool &result);
@@ -95,8 +121,18 @@ namespace klee {
     /// mayBeTrue - Determine if there is a valid assignment for the given state
     /// in which the expression evaluates to true.
     ///
-    /// \param [out] result - On success, true iff the expresssion is true for
-    /// some satisfying assignment.
+    /// This evaluates the following logical formula:
+    ///
+    /// \f[ \exists X constraints(X) \land query(X) \f]
+    ///
+    /// which is equivalent to
+    ///
+    /// \f[ \lnot \forall X constraints(X) \to \lnot 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.
+    ///
+    /// \param [out] result - On success, true iff the logical formula may be true
     ///
     /// \return True on success.
     bool mayBeTrue(const Query&, bool &result);
@@ -104,8 +140,18 @@ namespace klee {
     /// mayBeFalse - Determine if there is a valid assignment for the given
     /// state in which the expression evaluates to false.
     ///
-    /// \param [out] result - On success, true iff the expresssion is false for
-    /// some satisfying assignment.
+    /// This evaluates the following logical formula:
+    ///
+    /// \f[ \exists X constraints(X) \land \lnot query(X) \f]
+    ///
+    /// which is equivalent to
+    ///
+    /// \f[ \lnot \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.
+    ///
+    /// \param [out] result - On success, true iff the logical formula may be false
     ///
     /// \return True on success.
     bool mayBeFalse(const Query&, bool &result);
@@ -113,7 +159,7 @@ namespace klee {
     /// getValue - Compute one possible value for the given expression.
     ///
     /// \param [out] result - On success, a value for the expression in some
-    /// satisying assignment.
+    /// satisfying assignment.
     ///
     /// \return True on success.
     bool getValue(const Query&, ref<ConstantExpr> &result);
@@ -123,7 +169,7 @@ namespace klee {
     /// \param [out] result - On success, this vector will be filled in with an
     /// array of bytes for each given object (with length matching the object
     /// size). The bytes correspond to the initial values for the objects for
-    /// some satisying assignment.
+    /// some satisfying assignment.
     ///
     /// \return True on success.
     ///
diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h
index 09be849b..e200205b 100644
--- a/include/klee/SolverImpl.h
+++ b/include/klee/SolverImpl.h
@@ -46,19 +46,44 @@ namespace klee {
     /// SolverImpl provides a default implementation which uses
     /// computeTruth. Clients should override this if a more efficient
     /// implementation is available.
+    ///
+    /// \param [out] result - if
+    /// \f[ \forall X constraints(X) \to query(X) \f]
+    /// then Solver::True,
+    /// else if
+    /// \f[ \forall X constraints(X) \to \lnot query(X) \f]
+    /// then Solver::False,
+    /// else
+    /// Solver::Unknown
+    ///
+    /// \return True on success
     virtual bool computeValidity(const Query& query, Solver::Validity &result);
     
-    /// computeTruth - Determine whether the given query is provable.
+    /// computeTruth - Determine whether the given query expression is provably true
+    /// given the constraints.
     ///
     /// The query expression is guaranteed to be non-constant and have
     /// bool type.
+    ///
+    /// This method should evaluate the logical formula:
+    ///
+    /// \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.
+    ///
+    /// \param [out] isValid - On success, true iff the logical formula is true.
+    /// \return True on success
     virtual bool computeTruth(const Query& query, bool &isValid) = 0;
 
     /// computeValue - Compute a feasible value for the expression.
     ///
     /// The query expression is guaranteed to be non-constant.
+    ///
+    /// \return True on success
     virtual bool computeValue(const Query& query, ref<Expr> &result) = 0;
     
+    /// \sa Solver::getInitialValues()
     virtual bool computeInitialValues(const Query& query,
                                       const std::vector<const Array*> 
                                         &objects,