From e2cb581253b18b50d6526cc4a28ee7ff933a29bf Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 20 Mar 2021 22:10:03 +0000 Subject: Refactored maxStaticPctChecks into a sequence of conditions. --- lib/Core/Executor.cpp | 28 +++++++++++++++++++--------- 1 file changed, 19 insertions(+), 9 deletions(-) (limited to 'lib') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 7bfc0dac..6891dc93 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -986,18 +986,28 @@ ref Executor::maxStaticPctChecks(ExecutionState ¤t, StatisticManager &sm = *theStatisticManager; CallPathNode *cpn = current.stack.back().callPathNode; - if ((MaxStaticForkPct < 1. && - sm.getIndexedValue(stats::forks, sm.getIndex()) > - stats::forks * MaxStaticForkPct) || - (MaxStaticCPForkPct < 1. && cpn && - (cpn->statistics.getValue(stats::forks) > - stats::forks * MaxStaticCPForkPct)) || + + bool reached_max_fork_limit = + (MaxStaticForkPct < 1. && + (sm.getIndexedValue(stats::forks, sm.getIndex()) > + stats::forks * MaxStaticForkPct)); + + bool reached_max_cp_fork_limit = (MaxStaticCPForkPct < 1. && cpn && + (cpn->statistics.getValue(stats::forks) > + stats::forks * MaxStaticCPForkPct)); + + bool reached_max_solver_limit = (MaxStaticSolvePct < 1 && - sm.getIndexedValue(stats::solverTime, sm.getIndex()) > - stats::solverTime * MaxStaticSolvePct) || + (sm.getIndexedValue(stats::solverTime, sm.getIndex()) > + stats::solverTime * MaxStaticSolvePct)); + + bool reached_max_cp_solver_limit = (MaxStaticCPForkPct < 1. && cpn && (cpn->statistics.getValue(stats::solverTime) > - stats::solverTime * MaxStaticCPSolvePct))) { + stats::solverTime * MaxStaticCPSolvePct)); + + if (reached_max_fork_limit || reached_max_cp_fork_limit || + reached_max_solver_limit || reached_max_cp_solver_limit) { ref value; bool success = solver->getValue(current.constraints, condition, value, current.queryMetaData); -- cgit 1.4.1