From 9784b39d8815cdc1c884d6b365cd16d70f2657bf Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 9 Feb 2022 15:56:59 -0800 Subject: [PATCH] bv: Add --tlimit-per support for CryptoMiniSat. (#8086) --- src/prop/cryptominisat.cpp | 24 +++++++++++++++++++++--- src/prop/cryptominisat.h | 12 ++++++++++++ src/prop/sat_solver_factory.cpp | 5 +++++ src/prop/sat_solver_factory.h | 1 + src/theory/bv/bv_solver_bitblast.cpp | 4 +++- src/util/resource_manager.cpp | 5 +++++ src/util/resource_manager.h | 2 ++ 7 files changed, 49 insertions(+), 4 deletions(-) diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index ef13a0b46..446ddd2d4 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -19,11 +19,12 @@ #ifdef CVC5_USE_CRYPTOMINISAT +#include + #include "base/check.h" +#include "util/resource_manager.h" #include "util/statistics_registry.h" -#include - 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& 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 58ce33bcf..8eaa30e03 100644 --- 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 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 ab72f74bc..1b0b27b49 100644 --- 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 f7751ebbf..419877767 100644 --- 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 be7e658cb..d0c5125f7 100644 --- 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 4a5be537c..797d5515e 100644 --- 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 cb5d70a7b..27771c22c 100644 --- 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; -- 2.30.2