From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Thu, 28 Apr 2022 00:51:20 +0000 (-0700)
Subject: Add resource limiting to coverings solver (#8672)
X-Git-Tag: cvc5-1.0.1~213
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25e24c210bdf0157e0f95c257ec3516bc57d7a1b;p=cvc5.git

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.
---

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<CACInterval> 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<CACInterval> 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,