bv: Add resource limits support for CaDiCaL. (#8788)

Fixes #8776.

diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index 8763389f245f2d9b5b650061f291ec52dd8ff600..684c81b2d6a0b7a8f4071317d4ab476cff40a20c 100644 (file)
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -82,23 +82,27 @@ void CadicalSolver::init()
 CadicalSolver::~CadicalSolver() {}
 
 /**
- * Terminator class that notifies CaDiCaL to terminate when time limit is
- * reached (used for time limits specified via --tlimit-per).
+ * Terminator class that notifies CaDiCaL to terminate when the resource limit
+ * is reached (used for resource limits specified via --rlimit or --tlimit).
  */
-class TimeLimitTerminator : public CaDiCaL::Terminator
+class ResourceLimitTerminator : public CaDiCaL::Terminator
 {
  public:
-  TimeLimitTerminator(ResourceManager& resmgr) : d_resmgr(resmgr){};
+  ResourceLimitTerminator(ResourceManager& resmgr) : d_resmgr(resmgr){};
 
-  bool terminate() override { return d_resmgr.outOfTime(); }
+  bool terminate() override
+  {
+    d_resmgr.spendResource(Resource::BvSatStep);
+    return d_resmgr.outOfResources() || d_resmgr.outOfTime();
+  }
 
  private:
   ResourceManager& d_resmgr;
 };
 
-void CadicalSolver::setTimeLimit(ResourceManager* resmgr)
+void CadicalSolver::setResourceLimit(ResourceManager* resmgr)
 {
-  d_terminator.reset(new TimeLimitTerminator(*resmgr));
+  d_terminator.reset(new ResourceLimitTerminator(*resmgr));
   d_solver->connect_terminator(d_terminator.get());
 }
 

diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index 0baf52212865c3926edd737bc691d96040fecfe9..0e15f68a4a09d2b0208d696f392e8d4d92fbfe19 100644 (file)
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -75,9 +75,9 @@ class CadicalSolver : public SatSolver
   void init();
 
   /**
-   * Set time limit per solve() call.
+   * Set resource limit.
    */
-  void setTimeLimit(ResourceManager* resmgr);
+  void setResourceLimit(ResourceManager* resmgr);
 
   std::unique_ptr<CaDiCaL::Solver> d_solver;
   std::unique_ptr<CaDiCaL::Terminator> d_terminator;

diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index db2f83ff52b71d6ea2815e180199e00165fbe44b..9e6a7601bf68cb04257e428b948ff43e4a497d65 100644 (file)
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -52,10 +52,7 @@ SatSolver* SatSolverFactory::createCadical(StatisticsRegistry& registry,
 {
   CadicalSolver* res = new CadicalSolver(registry, name);
   res->init();
-  if (resmgr->limitOn())
-  {
-    res->setTimeLimit(resmgr);
-  }
+  res->setResourceLimit(resmgr);
   return res;
 }
 

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 1abab37345f0c2f2c83c815e322c899dd39c0959..7817e36565f17d9225066ecdd43a9f2c37c89c17 100644 (file)
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -76,11 +76,7 @@ const char* toString(Resource r)
     case Resource::ArithNlCoveringStep: return "ArithNlCoveringStep";
     case Resource::ArithNlLemmaStep: return "ArithNlLemmaStep";
     case Resource::BitblastStep: return "BitblastStep";
-    case Resource::BvEagerAssertStep: return "BvEagerAssertStep";
-    case Resource::BvPropagationStep: return "BvPropagationStep";
-    case Resource::BvSatConflictsStep: return "BvSatConflictsStep";
-    case Resource::BvSatPropagateStep: return "BvSatPropagateStep";
-    case Resource::BvSatSimplifyStep: return "BvSatSimplifyStep";
+    case Resource::BvSatStep: return "BvSatStep";
     case Resource::CnfStep: return "CnfStep";
     case Resource::DecisionStep: return "DecisionStep";
     case Resource::LemmaStep: return "LemmaStep";

diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 9d1cab34004300cf0ddb87c8b02197bd25eb845a..032f99b0469db91870d6ba02f6cfc91429697714 100644 (file)
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -76,11 +76,7 @@ enum class Resource
   ArithNlCoveringStep,
   ArithNlLemmaStep,
   BitblastStep,
-  BvEagerAssertStep,
-  BvPropagationStep,
-  BvSatConflictsStep,
-  BvSatPropagateStep,
-  BvSatSimplifyStep,
+  BvSatStep,
   CnfStep,
   DecisionStep,
   LemmaStep,