Simplify some code, and add more comments.

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

1 files changed, 46 insertions, 43 deletions

diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 3f94f974..19f16821 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -62,7 +62,12 @@ class CexCachingSolver : public SolverImpl {
   bool searchForAssignment(KeyType &key, 
                            Assignment *&result);
   
-  bool lookupAssignment(const Query& query, Assignment *&result);
+  bool lookupAssignment(const Query& query, KeyType &key, Assignment *&result);
+
+  bool lookupAssignment(const Query& query, Assignment *&result) {
+    KeyType key;
+    return lookupAssignment(query, key, result);
+  }
 
   bool getAssignment(const Query& query, Assignment *&result);
   
@@ -101,8 +106,8 @@ struct NullOrSatisfyingAssignment {
 
 /// searchForAssignment - Look for a cached solution for a query.
 ///
-/// \param Key - The query to look up.
-/// \param Result - The cached result, if the lookup is succesful. This is
+/// \param key - The query to look up.
+/// \param result [out] - The cached result, if the lookup is succesful. This is
 /// either a satisfying assignment (for a satisfiable query), or 0 (for an
 /// unsatisfiable query).
 /// \return - True if a cached result was found.
@@ -163,9 +168,18 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) {
   return false;
 }
 
+/// lookupAssignment - Lookup a cached result for the given \arg query.
+///
+/// \param query - The query to lookup.
+/// \param key [out] - On return, the key constructed for the query.
+/// \param result [out] - The cached result, if the lookup is succesful. This is
+/// either a satisfying assignment (for a satisfiable query), or 0 (for an
+/// unsatisfiable query).
+/// \return True if a cached result was found.
 bool CexCachingSolver::lookupAssignment(const Query &query, 
+                                        KeyType &key,
                                         Assignment *&result) {
-  KeyType key(query.constraints.begin(), query.constraints.end());
+  key = KeyType(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createIsZero(query.expr);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
     if (CE->isFalse()) {
@@ -180,50 +194,39 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
 }
 
 bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
-  KeyType key(query.constraints.begin(), query.constraints.end());
-  ref<Expr> neg = Expr::createIsZero(query.expr);
-  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
-    if (CE->isFalse()) {
-      result = (Assignment*) 0;
-      return true;
-    }
-  } else {
-    key.insert(neg);
-  }
+  KeyType key;
+  if (lookupAssignment(query, key, result))
+    return true;
 
-  if (!searchForAssignment(key, result)) {
-    // Need to solve.
-    
-    std::vector<const Array*> objects;
-    findSymbolicObjects(key.begin(), key.end(), objects);
+  std::vector<const Array*> objects;
+  findSymbolicObjects(key.begin(), key.end(), objects);
 
-    std::vector< std::vector<unsigned char> > values;
-    bool hasSolution;
-    if (!solver->impl->computeInitialValues(query, objects, values, 
-                                            hasSolution))
-      return false;
+  std::vector< std::vector<unsigned char> > values;
+  bool hasSolution;
+  if (!solver->impl->computeInitialValues(query, objects, values, 
+                                          hasSolution))
+    return false;
     
-    Assignment *binding;
-    if (hasSolution) {
-      binding = new Assignment(objects, values);
-
-      // memoization
-      std::pair<assignmentsTable_ty::iterator, bool>
-        res = assignmentsTable.insert(binding);
-      if (!res.second) {
-        delete binding;
-        binding = *res.first;
-      }
-
-      if (DebugCexCacheCheckBinding)
-        assert(binding->satisfies(key.begin(), key.end()));
-    } else {
-      binding = (Assignment*) 0;
+  Assignment *binding;
+  if (hasSolution) {
+    binding = new Assignment(objects, values);
+
+    // Memoize the result.
+    std::pair<assignmentsTable_ty::iterator, bool>
+      res = assignmentsTable.insert(binding);
+    if (!res.second) {
+      delete binding;
+      binding = *res.first;
     }
-
-    result = binding;
-    cache.insert(key, binding);
+    
+    if (DebugCexCacheCheckBinding)
+      assert(binding->satisfies(key.begin(), key.end()));
+  } else {
+    binding = (Assignment*) 0;
   }
+  
+  result = binding;
+  cache.insert(key, binding);
 
   return true;
 }