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 6c3f97c6c93b38b4fdbccfa00ff459c4a352140e..d358a34ef759f305013463114dad76a03aa60911 100644 (file)
--- 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 9f8130b6e58af22a286fff6782f6dc3203b3c3d9..1abab37345f0c2f2c83c815e322c899dd39c0959 100644 (file)
--- 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 753ae164741c703c1a07a459fce141347e8d6653..9d1cab34004300cf0ddb87c8b02197bd25eb845a 100644 (file)
--- 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,