From 25e24c210bdf0157e0f95c257ec3516bc57d7a1b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 27 Apr 2022 17:51:20 -0700 Subject: [PATCH] Add resource limiting to coverings solver (#8672) Right now, resource limits are not checked while the coverings solver is computing. This PR adds a new resource and spends it within every recursive call of the coverings solver. This fixes cases where cvc5 does not honor the per-call time limit on QF_NRA. --- src/theory/arith/nl/coverings/cdcac.cpp | 2 ++ src/util/resource_manager.cpp | 1 + src/util/resource_manager.h | 1 + 3 files changed, 4 insertions(+) diff --git a/src/theory/arith/nl/coverings/cdcac.cpp b/src/theory/arith/nl/coverings/cdcac.cpp index 6c3f97c6c..d358a34ef 100644 --- a/src/theory/arith/nl/coverings/cdcac.cpp +++ b/src/theory/arith/nl/coverings/cdcac.cpp @@ -24,6 +24,7 @@ #include "theory/arith/nl/coverings/variable_ordering.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/resource_manager.h" using namespace cvc5::internal::kind; @@ -523,6 +524,7 @@ CACInterval CDCAC::intervalFromCharacterization( std::vector CDCAC::getUnsatCoverImpl(std::size_t curVariable, bool returnFirstInterval) { + d_env.getResourceManager()->spendResource(Resource::ArithNlCoveringStep); Trace("cdcac") << "Looking for unsat cover for " << d_variableOrdering[curVariable] << std::endl; std::vector intervals = getUnsatIntervals(curVariable); diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 9f8130b6e..1abab3734 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -73,6 +73,7 @@ const char* toString(Resource r) switch (r) { case Resource::ArithPivotStep: return "ArithPivotStep"; + case Resource::ArithNlCoveringStep: return "ArithNlCoveringStep"; case Resource::ArithNlLemmaStep: return "ArithNlLemmaStep"; case Resource::BitblastStep: return "BitblastStep"; case Resource::BvEagerAssertStep: return "BvEagerAssertStep"; diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 753ae1647..9d1cab340 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -73,6 +73,7 @@ class WallClockTimer enum class Resource { ArithPivotStep, + ArithNlCoveringStep, ArithNlLemmaStep, BitblastStep, BvEagerAssertStep, -- 2.30.2