From db84323caa3009cf418f959313e49f5bea5d35a6 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 16 Nov 2020 11:15:19 +0100 Subject: Improve accuracy of resource limitation (#4763) The main goal of the resource limitation mechanism (via `--rlimit`) is to have a deterministic limitation on runtime. The ultimate goal would be that the actual runtime grows linearly with the spent resources. To achieve this, this PR does the following: - introduce new resources spent in places that are not yet covered - find resource weights that best approximate the runtime It provides a contrib script `learn_resource_weights.py` that uses statistics from a given benchmark run and uses linear regression to find good resource weights. The script also evaluates this estimate and identifies outliers, benchmarks for which this approximation is particularly bad. This probably indicates that on such a benchmark, some part of the code takes a significant amount of time but is not yet represented by a resource. Eventually, we should use the resulting resource weights as defaults for the options like `--rewrite-step`, `--theory-check-step`, etc. --- src/theory/arith/nl/nonlinear_extension.cpp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/theory/arith/nl') diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 5bd02cf19..22a69cadb 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -161,6 +161,8 @@ unsigned NonlinearExtension::filterLemmas(std::vector& lemmas, for (const NlLemma& lem : lemmas) { sum += filterLemma(lem, out); + d_containing.getOutputChannel().spendResource( + ResourceManager::Resource::ArithNlLemmaStep); } lemmas.clear(); return sum; -- cgit v1.2.3