bv: Add --tlimit-per support for CaDiCaL. (#8085)

This commit adds --tlimit-per support for CaDiCaL via CaDiCaL's Terminator class.

Fixes #8049

diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index ddf20f5a1e00a5e33a39388bc49d5097ca52ea1c..570db18086dc3738f5c7747a2e46cd33042aeb1e 100644 (file)
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -18,6 +18,7 @@
 #include "prop/cadical.h"
 
 #include "base/check.h"
+#include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 
 namespace cvc5 {
@@ -80,6 +81,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).
+ */
+class TimeLimitTerminator : public CaDiCaL::Terminator
+{
+ public:
+  TimeLimitTerminator(ResourceManager& resmgr) : d_resmgr(resmgr){};
+
+  bool terminate() override { return d_resmgr.outOfTime(); }
+
+ private:
+  ResourceManager& d_resmgr;
+};
+
+void CadicalSolver::setTimeLimit(ResourceManager* resmgr)
+{
+  d_terminator.reset(new TimeLimitTerminator(*resmgr));
+  d_solver->connect_terminator(d_terminator.get());
+}
+
 ClauseId CadicalSolver::addClause(SatClause& clause, bool removable)
 {
   for (const SatLiteral& lit : clause)

diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index 46c7c7e42cd2b94d5ce5eeb561a588210d0ecb19..b2181623a362b9e184bb35c7f587bb68198a26b8 100644 (file)
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -74,7 +74,14 @@ class CadicalSolver : public SatSolver
    */
   void init();
 
+  /**
+   * Set time limit per solve() call.
+   */
+  void setTimeLimit(ResourceManager* resmgr);
+
   std::unique_ptr<CaDiCaL::Solver> d_solver;
+  std::unique_ptr<CaDiCaL::Terminator> d_terminator;
+
   /**
    * Stores the current set of assumptions provided via solve() and is used to
    * query the solver if a given assumption is false.

diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index dfd660ace616a11bf3d8f78ded522e9c0ed2edcf..ab72f74bcaa076ccd61d710ea3c927f8536e89d9 100644 (file)
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -42,10 +42,15 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry& registry,
 }
 
 SatSolver* SatSolverFactory::createCadical(StatisticsRegistry& registry,
+                                           ResourceManager* resmgr,
                                            const std::string& name)
 {
   CadicalSolver* res = new CadicalSolver(registry, name);
   res->init();
+  if (resmgr->limitOn())
+  {
+    res->setTimeLimit(resmgr);
+  }
   return res;
 }
 

diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index fce8e31e280a8fbc676ff16f73e5970deb3e69c0..f7751ebbf8c3ed7225f65bd964a71a4c6e89da73 100644 (file)
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -39,6 +39,7 @@ class SatSolverFactory
                                         const std::string& name = "");
 
   static SatSolver* createCadical(StatisticsRegistry& registry,
+                                  ResourceManager* resmgr,
                                   const std::string& name = "");
 
   static SatSolver* createKissat(StatisticsRegistry& registry,

diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 0a9fc78873fc40a04dd4f378cb0852eaa7eab62e..be7e658cbd923841f1cb492b7347c59b3989ceda 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -336,7 +336,9 @@ void BVSolverBitblast::initSatSolver()
       break;
     default:
       d_satSolver.reset(prop::SatSolverFactory::createCadical(
-          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
+          smtStatisticsRegistry(),
+          d_env.getResourceManager(),
+          "theory::bv::BVSolverBitblast::"));
   }
   d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
                                         d_bbRegistrar.get(),