Clean-up and add documentation

3 files changed, 40 insertions, 32 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;
   };
 
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 6b576435..2a4c2adb 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -9,10 +9,9 @@
 
 #include "klee/Expr/Constraints.h"
 
-#include "klee/Expr/ExprPPrinter.h"
 #include "klee/Expr/ExprVisitor.h"
-#include "klee/Support/OptionCategories.h"
 #include "klee/Module/KModule.h"
+#include "klee/Support/OptionCategories.h"
 
 #include "llvm/IR/Function.h"
 #include "llvm/Support/CommandLine.h"
@@ -28,29 +27,28 @@ llvm::cl::opt<bool> RewriteEqualities(
                    "constant is added (default=true)"),
     llvm::cl::init(true),
     llvm::cl::cat(SolvingCat));
-}
+} // namespace
 
 class ExprReplaceVisitor : public ExprVisitor {
 private:
   ref<Expr> src, dst;
 
 public:
-  ExprReplaceVisitor(ref<Expr> _src, ref<Expr> _dst) : src(_src), dst(_dst) {}
+  ExprReplaceVisitor(const ref<Expr> &_src, const ref<Expr> &_dst)
+      : src(_src), dst(_dst) {}
 
-  Action visitExpr(const Expr &e) {
-    if (e == *src.get()) {
+  Action visitExpr(const Expr &e) override {
+    if (e == *src) {
       return Action::changeTo(dst);
-    } else {
-      return Action::doChildren();
     }
+    return Action::doChildren();
   }
 
-  Action visitExprPost(const Expr &e) {
-    if (e == *src.get()) {
+  Action visitExprPost(const Expr &e) override {
+    if (e == *src) {
       return Action::changeTo(dst);
-    } else {
-      return Action::doChildren();
     }
+    return Action::doChildren();
   }
 };
 
@@ -59,17 +57,16 @@ private:
   const std::map< ref<Expr>, ref<Expr> > &replacements;
 
 public:
-  ExprReplaceVisitor2(const std::map<ref<Expr>, ref<Expr>> &_replacements)
+  explicit ExprReplaceVisitor2(
+      const std::map<ref<Expr>, ref<Expr>> &_replacements)
       : ExprVisitor(true), replacements(_replacements) {}
 
-  Action visitExprPost(const Expr &e) {
-    std::map< ref<Expr>, ref<Expr> >::const_iterator it =
-      replacements.find(ref<Expr>(const_cast<Expr*>(&e)));
+  Action visitExprPost(const Expr &e) override {
+    auto it = replacements.find(ref<Expr>(const_cast<Expr *>(&e)));
     if (it!=replacements.end()) {
       return Action::changeTo(it->second);
-    } else {
-      return Action::doChildren();
     }
+    return Action::doChildren();
   }
 };
 
@@ -118,7 +115,7 @@ ref<Expr> ConstraintManager::simplifyExpr(const ConstraintSet &constraints,
   return ExprReplaceVisitor2(equalities).visit(e);
 }
 
-void ConstraintManager::addConstraintInternal(ref<Expr> e) {
+void ConstraintManager::addConstraintInternal(const ref<Expr> &e) {
   // rewrite any known equalities and split Ands into different conjuncts
 
   switch (e->getKind()) {
@@ -158,9 +155,9 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
   }
 }
 
-void ConstraintManager::addConstraint(ref<Expr> e) {
-  e = simplifyExpr(constraints, e);
-  addConstraintInternal(e);
+void ConstraintManager::addConstraint(const ref<Expr> &e) {
+  ref<Expr> simplified = simplifyExpr(constraints, e);
+  addConstraintInternal(simplified);
 }
 
 ConstraintManager::ConstraintManager(ConstraintSet &_constraints)