bv: Add --tlimit-per support for CryptoMiniSat. (#8086)

diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index ef13a0b4614639b0c53a1d0021708c683564d606..446ddd2d491f34e0538bf7588ce2e5777702b0c0 100644 (file)
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -19,11 +19,12 @@
 
 #ifdef CVC5_USE_CRYPTOMINISAT
 
+#include <cryptominisat5/cryptominisat.h>
+
 #include "base/check.h"
+#include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 
-#include <cryptominisat5/cryptominisat.h>
-
 namespace cvc5 {
 namespace prop {
 
@@ -75,7 +76,8 @@ CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry& registry,
     : d_solver(new CMSat::SATSolver()),
       d_numVariables(0),
       d_okay(true),
-      d_statistics(registry, name)
+      d_statistics(registry, name),
+      d_resmgr(nullptr)
 {
 }
 
@@ -94,6 +96,20 @@ void CryptoMinisatSolver::init()
 
 CryptoMinisatSolver::~CryptoMinisatSolver() {}
 
+void CryptoMinisatSolver::setTimeLimit(ResourceManager* resmgr)
+{
+  d_resmgr = resmgr;
+}
+
+void CryptoMinisatSolver::setMaxTime()
+{
+  if (d_resmgr)
+  {
+    // Set time limit to remaining number of seconds.
+    d_solver->set_max_time(d_resmgr->getRemainingTime() / 1000.0);
+  }
+}
+
 ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
                                            bool rhs,
                                            bool removable)
@@ -170,6 +186,7 @@ void CryptoMinisatSolver::interrupt(){
 SatValue CryptoMinisatSolver::solve(){
   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
   ++d_statistics.d_statCallsToSolve;
+  setMaxTime();
   return toSatLiteralValue(d_solver->solve());
 }
 
@@ -189,6 +206,7 @@ SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions)
     assumpts.push_back(toInternalLit(lit));
   }
   ++d_statistics.d_statCallsToSolve;
+  setMaxTime();
   return toSatLiteralValue(d_solver->solve(&assumpts));
 }
 

diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index 58ce33bcf8e8e3d71000eb3f86569b1ddfe9e986..8eaa30e03e23417a53e9ce251becf66545fb7747 100644 (file)
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -93,6 +93,17 @@ class CryptoMinisatSolver : public SatSolver
    */
   void init();
 
+  /**
+   * Set time limit per solve() call.
+   */
+  void setTimeLimit(ResourceManager* resmgr);
+
+  /**
+   * Set CryptoMiniSat's maximum time limit based on the already elapsed time
+   * of the --tlimit-per limit.
+   */
+  void setMaxTime();
+
   std::unique_ptr<CMSat::SATSolver> d_solver;
   unsigned d_numVariables;
   bool d_okay;
@@ -100,6 +111,7 @@ class CryptoMinisatSolver : public SatSolver
   SatVariable d_false;
 
   Statistics d_statistics;
+  ResourceManager* d_resmgr;
 };
 
 }  // namespace prop

diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index ab72f74bcaa076ccd61d710ea3c927f8536e89d9..1b0b27b490ba110221d18bf0bc0d88e0ec2fe891 100644 (file)
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -30,11 +30,16 @@ MinisatSatSolver* SatSolverFactory::createCDCLTMinisat(
 }
 
 SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry& registry,
+                                                 ResourceManager* resmgr,
                                                  const std::string& name)
 {
 #ifdef CVC5_USE_CRYPTOMINISAT
   CryptoMinisatSolver* res = new CryptoMinisatSolver(registry, name);
   res->init();
+  if (resmgr->limitOn())
+  {
+    res->setTimeLimit(resmgr);
+  }
   return res;
 #else
   Unreachable() << "cvc5 was not compiled with Cryptominisat support.";

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

diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index be7e658cbd923841f1cb492b7347c59b3989ceda..d0c5125f7c94119713bd23e722897a6accd7eb00 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -332,7 +332,9 @@ void BVSolverBitblast::initSatSolver()
   {
     case options::SatSolverMode::CRYPTOMINISAT:
       d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
-          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
+          smtStatisticsRegistry(),
+          d_env.getResourceManager(),
+          "theory::bv::BVSolverBitblast::"));
       break;
     default:
       d_satSolver.reset(prop::SatSolverFactory::createCadical(

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 4a5be537c161d6ed81e8451eb2361eba028bae8f..797d5515e4a4d7becdeb53fa35a2d59286f02835 100644 (file)
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -188,6 +188,11 @@ uint64_t ResourceManager::getResourceUsage() const
 
 uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; }
 
+uint64_t ResourceManager::getRemainingTime() const
+{
+  return d_options.base.perCallMillisecondLimit - d_perCallTimer.elapsed();
+}
+
 uint64_t ResourceManager::getResourceRemaining() const
 {
   if (d_options.base.cumulativeResourceLimit <= d_cumulativeResourceUsed)

diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index cb5d70a7bb03e6d58884c6dd687ef7224bf4b66d..27771c22c2238266665055a359b69256b43a2d76 100644 (file)
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -141,6 +141,8 @@ class ResourceManager
   uint64_t getResourceUsage() const;
   /** Retrieves time used over all calls. */
   uint64_t getTimeUsage() const;
+  /** Retrieves the remaining time until the time limit is reached. */
+  uint64_t getRemainingTime() const;
   /** Retrieves the remaining number of cumulative resources. */
   uint64_t getResourceRemaining() const;