From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 9 Feb 2022 21:50:18 +0000 (-0800)
Subject: bv: Add --tlimit-per support for CaDiCaL. (#8085)
X-Git-Tag: cvc5-1.0.0~431
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=803afe174e09eb6845ca1d206fceb219c798adcb;p=cvc5.git

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 ddf20f5a1..570db1808 100644
--- 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 46c7c7e42..b2181623a 100644
--- 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 dfd660ace..ab72f74bc 100644
--- 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 fce8e31e2..f7751ebbf 100644
--- 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 0a9fc7887..be7e658cb 100644
--- 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(),