From 9912da3912436a71949b1b97d96975bddcb169e3 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 18 Aug 2023 15:07:27 +0100 Subject: Remove broken experimental optimisation for validity (--cex-cache-exp) --- lib/Solver/CexCachingSolver.cpp | 19 ------------------- 1 file changed, 19 deletions(-) (limited to 'lib') diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index dbbd3516..87e6169c 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -48,11 +48,6 @@ cl::opt "before asking the SMT solver (default=false)"), cl::cat(SolvingCat)); -cl::opt CexCacheExperimental( - "cex-cache-exp", cl::init(false), - cl::desc("Optimization for validity queries (default=false)"), - cl::cat(SolvingCat)); - } // namespace /// @@ -302,20 +297,6 @@ bool CexCachingSolver::computeTruth(const Query& query, bool &isValid) { TimerStatIncrementer t(stats::cexCacheTime); - // There is a small amount of redundancy here. We only need to know - // truth and do not really need to compute an assignment. This means - // that we could check the cache to see if we already know that - // state ^ query has no assignment. In that case, by the validity of - // state, we know that state ^ !query must have an assignment, and - // so query cannot be true (valid). This does get hits, but doesn't - // really seem to be worth the overhead. - - if (CexCacheExperimental) { - Assignment *a; - if (lookupAssignment(query.negateExpr(), a) && !a) - return false; - } - Assignment *a; if (!getAssignment(query, a)) return false; -- cgit 1.4.1