From fbc91551abcc3806a08bb30462bb621ad6ea2863 Mon Sep 17 00:00:00 2001 From: Eric Rizzi Date: Mon, 6 Jul 2015 12:10:17 -0400 Subject: 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. --- lib/Solver/CexCachingSolver.cpp | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'lib') 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 @@ -34,6 +34,11 @@ namespace { cl::desc("try substituting all counterexamples before asking the SMT solver"), cl::init(false)); + cl::opt + CexCacheSuperSet("cex-cache-superset", + cl::desc("try substituting SAT super-set counterexample before asking the SMT solver (default=false)"), + cl::init(false)); + cl::opt 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 -- cgit 1.4.1