Clean-up and add documentation

2 files changed, 21 insertions, 10 deletions

diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h
index ae0f86f2..a9a1ce70 100644
--- a/include/klee/Expr/Constraints.h
+++ b/include/klee/Expr/Constraints.h
@@ -24,7 +24,7 @@ public:
   using iterator = constraints_ty::iterator;
   using const_iterator = constraints_ty::const_iterator;
 
-  typedef const_iterator constraint_iterator;
+  using constraint_iterator = const_iterator;
 
   bool empty() const;
   constraint_iterator begin() const;
@@ -49,20 +49,30 @@ class ExprVisitor;
 /// Manages constraints, e.g. optimisation
 class ConstraintManager {
 public:
-  // create from constraints with no optimization
+  /// Create constraint manager that modifies constraints
+  /// \param constraints
   explicit ConstraintManager(ConstraintSet &constraints);
 
+  /// Simplify expression expr based on constraints
+  /// \param constraints set of constraints used for simplification
+  /// \param expr to simplify
+  /// \return simplified expression
   static ref<Expr> simplifyExpr(const ConstraintSet &constraints,
-                                const ref<Expr> &e);
+                                const ref<Expr> &expr);
 
-  void addConstraint(ref<Expr> e);
+  /// Add constraint to the referenced constraint set
+  /// \param constraint
+  void addConstraint(const ref<Expr> &constraint);
 
-  // returns true iff the constraints were modified
+private:
+  /// Rewrite set of constraints using the visitor
+  /// \param visitor constraint rewriter
+  /// \return true iff any constraint has been changed
   bool rewriteConstraints(ExprVisitor &visitor);
 
-  void addConstraintInternal(ref<Expr> e);
+  /// Add constraint to the set of constraints
+  void addConstraintInternal(const ref<Expr> &constraint);
 
-private:
   ConstraintSet &constraints;
 };
 
diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h
index 8d5f87d5..263f1626 100644
--- a/include/klee/Solver/Solver.h
+++ b/include/klee/Solver/Solver.h
@@ -21,10 +21,11 @@ namespace klee {
   class Expr;
   class SolverImpl;
 
-  /// Collection of meta data used by a solver
-  ///
+  /// Collection of meta data that a solver can have access to. This is
+  /// independent of the actual constraints but can be used as a two-way
+  /// communication between solver and context of query.
   struct SolverQueryMetaData {
-    /// @brief Costs for all queries issued for this state, in seconds
+    /// @brief Costs for all queries issued for this state
     time::Span queryCost;
   };