about summary refs log tree commit diff homepage
path: root/lib/Solver/CexCachingSolver.cpp
diff options
context:
space:
mode:
authorEric Rizzi <eric.rizzi@gmail.com>2015-07-06 12:10:17 -0400
committerEric Rizzi <eric.rizzi@gmail.com>2015-07-06 12:10:17 -0400
commitfbc91551abcc3806a08bb30462bb621ad6ea2863 (patch)
tree9005402efcc165640cd68032c6826a10c73b6bee /lib/Solver/CexCachingSolver.cpp
parent637e884bb0ad4ead31d61583f47db475f5ec1ab7 (diff)
downloadklee-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.cpp15
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