From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Sun, 22 May 2022 16:04:55 +0000 (-0700)
Subject: bv: Add resource limits support for CaDiCaL. (#8788)
X-Git-Tag: cvc5-1.0.1~106
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=01aa886ace1f040d16fa3aa8e6f2ea57fd9de0a2;p=cvc5.git

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

Fixes #8776.
---

diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index 8763389f2..684c81b2d 100644
--- 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 0baf52212..0e15f68a4 100644
--- 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 db2f83ff5..9e6a7601b 100644
--- 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 1abab3734..7817e3656 100644
--- 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 9d1cab340..032f99b04 100644
--- 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,