diff options
-rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 37 |
1 files changed, 33 insertions, 4 deletions
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 2bdc7418..3f94f974 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -99,6 +99,13 @@ 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 +/// either a satisfying assignment (for a satisfiable query), or 0 (for an +/// unsatisfiable query). +/// \return - True if a cached result was found. bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { Assignment * const *lookup = cache.lookup(key); if (lookup) { @@ -107,12 +114,22 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { } if (CexCacheTryAll) { + // Look for a satisfying assignment for a superset, which is trivially an + // assignment for any subset. Assignment **lookup = cache.findSuperset(key, NonNullAssignment()); - if (!lookup) lookup = cache.findSubset(key, NullAssignment()); + + // Otherwise, look for a subset which is unsatisfiable, see below. + if (!lookup) + lookup = cache.findSubset(key, NullAssignment()); + + // If either lookup succeeded, then we have a cached solution. if (lookup) { result = *lookup; return true; } + + // Otherwise, iterate through the set of current assignments to see if one + // of them satisfies the query. for (assignmentsTable_ty::iterator it = assignmentsTable.begin(), ie = assignmentsTable.end(); it != ie; ++it) { Assignment *a = *it; @@ -122,9 +139,21 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { } } } else { - // XXX which order? one is sure to be better + // FIXME: Which order? one is sure to be better. + + // Look for a satisfying assignment for a superset, which is trivially an + // assignment for any subset. Assignment **lookup = cache.findSuperset(key, NonNullAssignment()); - if (!lookup) lookup = cache.findSubset(key, NullOrSatisfyingAssignment(key)); + + // Otherwise, look for a subset which is unsatisfiable -- if the subset is + // unsatisfiable then no additional constraints can produce a valid + // assignment. While searching subsets, we also explicitly the solutions for + // satisfiable subsets to see if they solve the current query and return + // them if so. This is cheap and frequently succeeds. + if (!lookup) + lookup = cache.findSubset(key, NullOrSatisfyingAssignment(key)); + + // If either lookup succeeded, then we have a cached solution. if (lookup) { result = *lookup; return true; @@ -163,7 +192,7 @@ bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) { } if (!searchForAssignment(key, result)) { - // need to solve + // Need to solve. std::vector<const Array*> objects; findSymbolicObjects(key.begin(), key.end(), objects); |