diff options
author | Eric Rizzi <eric.rizzi@gmail.com> | 2015-07-06 12:10:17 -0400 |
---|---|---|
committer | Eric Rizzi <eric.rizzi@gmail.com> | 2015-07-06 12:10:17 -0400 |
commit | fbc91551abcc3806a08bb30462bb621ad6ea2863 (patch) | |
tree | 9005402efcc165640cd68032c6826a10c73b6bee /lib/Solver/CexCachingSolver.cpp | |
parent | 637e884bb0ad4ead31d61583f47db475f5ec1ab7 (diff) | |
download | klee-fbc91551abcc3806a08bb30462bb621ad6ea2863.tar.gz |
Make the super-set check in CexCachingSolver default off
The super-set check in the CexCachingSolver takes MUCH longer than the sub-set check. Upon closer inspection, the super-set check gets slower and slower as more counterexamples fill the UBTree. Pretty quickly, the cost of the super-set check becomes larger than the time required to simply bypass it and go to the Solver.
Diffstat (limited to 'lib/Solver/CexCachingSolver.cpp')
-rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index df7fffc5..d51c1695 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -35,6 +35,11 @@ namespace { cl::init(false)); cl::opt<bool> + CexCacheSuperSet("cex-cache-superset", + cl::desc("try substituting SAT super-set counterexample before asking the SMT solver (default=false)"), + cl::init(false)); + + cl::opt<bool> CexCacheExperimental("cex-cache-exp", cl::init(false)); } @@ -124,8 +129,10 @@ 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()); - + Assignment **lookup = 0; + if (CexCacheSuperSet) + lookup = cache.findSuperset(key, NonNullAssignment()); + // Otherwise, look for a subset which is unsatisfiable, see below. if (!lookup) lookup = cache.findSubset(key, NullAssignment()); @@ -151,7 +158,9 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { // Look for a satisfying assignment for a superset, which is trivially an // assignment for any subset. - Assignment **lookup = cache.findSuperset(key, NonNullAssignment()); + Assignment **lookup = 0; + if (CexCacheSuperSet) + lookup = cache.findSuperset(key, NonNullAssignment()); // Otherwise, look for a subset which is unsatisfiable -- if the subset is // unsatisfiable then no additional constraints can produce a valid |