summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/bvminisat/bvminisat.cpp4
-rw-r--r--src/prop/bvminisat/bvminisat.h7
-rw-r--r--src/prop/bvminisat/core/Solver.h7
-rw-r--r--src/prop/cnf_stream.cpp7
-rw-r--r--src/prop/cnf_stream.h6
-rw-r--r--src/prop/minisat/core/Solver.cc14
-rw-r--r--src/prop/minisat/core/Solver.h6
-rw-r--r--src/prop/minisat/minisat.cpp4
-rw-r--r--src/prop/minisat/minisat.h1
-rw-r--r--src/prop/prop_engine.cpp34
-rw-r--r--src/prop/prop_engine.h108
-rw-r--r--src/prop/sat_solver.h7
-rw-r--r--src/prop/theory_proxy.cpp6
-rw-r--r--src/prop/theory_proxy.h2
14 files changed, 62 insertions, 151 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 71b8eb69d..aceb0f2e9 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -97,10 +97,6 @@ void BVMinisatSatSolver::markUnremovable(SatLiteral lit){
d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
}
-bool BVMinisatSatSolver::spendResource(){
- // Do nothing for the BV solver.
- return false;
-}
void BVMinisatSatSolver::interrupt(){
d_minisat->interrupt();
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index fea437565..e163ddcfd 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -46,8 +46,11 @@ private:
d_notify->notify(satClause);
}
+ void spendResource() {
+ d_notify->spendResource();
+ }
void safePoint() {
- d_notify->safePoint();
+ d_notify->safePoint();
}
};
@@ -86,8 +89,6 @@ public:
void markUnremovable(SatLiteral lit);
- bool spendResource();
-
void interrupt();
SatValue solve();
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 882f23ef7..a7a55208d 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -52,6 +52,7 @@ public:
*/
virtual void notify(vec<Lit>& learnt) = 0;
+ virtual void spendResource() = 0;
virtual void safePoint() = 0;
};
@@ -412,8 +413,10 @@ inline void Solver::interrupt(){ asynch_interrupt = true; }
inline void Solver::clearInterrupt(){ asynch_interrupt = false; }
inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
inline bool Solver::withinBudget() const {
- Assert (notify);
- notify->safePoint();
+ Assert (notify);
+ notify->spendResource();
+ notify->safePoint();
+
return !asynch_interrupt &&
(conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
(propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index ad187aa46..8d7b014cc 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -30,6 +30,7 @@
#include "proof/proof_manager.h"
#include "proof/sat_proof.h"
#include "prop/minisat/minisat.h"
+#include "smt/smt_engine_scope.h"
#include <queue>
using namespace std;
@@ -665,6 +666,12 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated
void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+ if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
+ NodeManager::currentResourceManager()->spendResource();
+ d_convertAndAssertCounter = 0;
+ }
+ ++d_convertAndAssertCounter;
+
switch(node.getKind()) {
case AND:
convertAndAssertAnd(node, negated);
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index b76051279..b22290ae4 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -74,6 +74,12 @@ protected:
*/
const bool d_fullLitToNodeMap;
+ /**
+ * Counter for resource limiting that is used to spend a resource
+ * every ResourceManager::resourceCounter calls to convertAndAssert.
+ */
+ unsigned long d_convertAndAssertCounter;
+
/** The "registrar" for pre-registration of terms */
Registrar* d_registrar;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index e5e28bb0b..ea370ac08 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1593,7 +1593,7 @@ CRef Solver::updateLemmas() {
Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
// Avoid adding lemmas indefinitely without resource-out
- spendResource();
+ proxy->spendResource();
CRef conflict = CRef_Undef;
@@ -1710,3 +1710,15 @@ CRef Solver::updateLemmas() {
return conflict;
}
+
+inline bool Solver::withinBudget() const {
+ Assert (proxy);
+ // spendResource sets async_interrupt or throws UnsafeInterruptException
+ // depending on whether hard-limit is enabled
+ proxy->spendResource();
+
+ bool within_budget = !asynch_interrupt &&
+ (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
+ (propagation_budget < 0 || propagations < (uint64_t)propagation_budget);
+ return within_budget;
+}
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 6d9fd538f..3ec19b026 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -219,7 +219,6 @@ public:
void budgetOff();
void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver.
void clearInterrupt(); // Clear interrupt indicator flag.
- void spendResource();
// Memory managment:
//
@@ -535,11 +534,6 @@ inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagati
inline void Solver::interrupt(){ asynch_interrupt = true; }
inline void Solver::clearInterrupt(){ asynch_interrupt = false; }
inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
-inline bool Solver::withinBudget() const {
- return !asynch_interrupt &&
- (conflict_budget < 0 || conflicts + resources_consumed < (uint64_t)conflict_budget) &&
- (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
-inline void Solver::spendResource() { ++resources_consumed; }
// FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
// pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 99341455c..b9fa37230 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -182,10 +182,6 @@ SatValue MinisatSatSolver::solve() {
return toSatLiteralValue(d_minisat->solve());
}
-bool MinisatSatSolver::spendResource() {
- d_minisat->spendResource();
- return !d_minisat->withinBudget();
-}
void MinisatSatSolver::interrupt() {
d_minisat->interrupt();
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 96893fe41..7c6e10170 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -61,7 +61,6 @@ public:
SatValue solve();
SatValue solve(long unsigned int&);
- bool spendResource();
void interrupt();
SatValue value(SatLiteral l);
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index a998d4240..c7dae533e 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -32,6 +32,7 @@
#include "main/options.h"
#include "util/output.h"
#include "util/result.h"
+#include "util/resource_manager.h"
#include "expr/expr.h"
#include "expr/command.h"
@@ -74,8 +75,8 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
d_satSolver(NULL),
d_registrar(NULL),
d_cnfStream(NULL),
- d_satTimer(*this),
- d_interrupted(false) {
+ d_interrupted(false),
+ d_resourceManager(NodeManager::currentResourceManager()) {
Debug("prop") << "Constructing the PropEngine" << endl;
@@ -159,7 +160,7 @@ void PropEngine::printSatisfyingAssignment(){
}
}
-Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
+Result PropEngine::checkSat() {
Assert(!d_inCheckSat, "Sat solver in solve()!");
Debug("prop") << "PropEngine::checkSat()" << endl;
@@ -171,25 +172,23 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
d_theoryEngine->presolve();
if(options::preprocessOnly()) {
- millis = resource = 0;
return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
}
- // Set the timer
- d_satTimer.set(millis);
-
// Reset the interrupted flag
d_interrupted = false;
// Check the problem
- SatValue result = d_satSolver->solve(resource);
-
- millis = d_satTimer.elapsed();
+ SatValue result = d_satSolver->solve();
if( result == SAT_VALUE_UNKNOWN ) {
- Result::UnknownExplanation why =
- d_satTimer.expired() ? Result::TIMEOUT :
- (d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT);
+
+ Result::UnknownExplanation why = Result::INTERRUPTED;
+ if (d_resourceManager->outOfTime())
+ why = Result::TIMEOUT;
+ if (d_resourceManager->outOfResources())
+ why = Result::RESOURCEOUT;
+
return Result(Result::SAT_UNKNOWN, why);
}
@@ -279,16 +278,11 @@ void PropEngine::interrupt() throw(ModalException) {
d_interrupted = true;
d_satSolver->interrupt();
- d_theoryEngine->interrupt();
Debug("prop") << "interrupt()" << endl;
}
-void PropEngine::spendResource() throw() {
- if(d_satSolver->spendResource()) {
- d_satSolver->interrupt();
- d_theoryEngine->interrupt();
- }
- checkTime();
+void PropEngine::spendResource() throw (UnsafeInterruptException) {
+ d_resourceManager->spendResource();
}
bool PropEngine::properExplanation(TNode node, TNode expl) const {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index ed022a64f..2750319e6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -24,12 +24,14 @@
#include "expr/node.h"
#include "options/options.h"
#include "util/result.h"
+#include "util/unsafe_interrupt_exception.h"
#include "smt/modal_exception.h"
#include "proof/proof_manager.h"
#include <sys/time.h>
namespace CVC4 {
+class ResourceManager;
class DecisionEngine;
class TheoryEngine;
@@ -45,78 +47,6 @@ class DPLLSatSolverInterface;
class PropEngine;
/**
- * A helper class to keep track of a time budget and signal
- * the PropEngine when the budget expires.
- */
-class SatTimer {
-
- PropEngine& d_propEngine;
- unsigned long d_ms;
- timeval d_limit;
-
-public:
-
- /** Construct a SatTimer attached to the given PropEngine. */
- SatTimer(PropEngine& propEngine) :
- d_propEngine(propEngine),
- d_ms(0) {
- }
-
- /** Is the timer currently active? */
- bool on() const {
- return d_ms != 0;
- }
-
- /** Set a millisecond timer (0==off). */
- void set(unsigned long millis) {
- d_ms = millis;
- // keep track of when it was set, even if it's disabled (i.e. == 0)
- Trace("limit") << "SatTimer::set(" << d_ms << ")" << std::endl;
- gettimeofday(&d_limit, NULL);
- Trace("limit") << "SatTimer::set(): it's " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
- d_limit.tv_sec += millis / 1000;
- d_limit.tv_usec += (millis % 1000) * 1000;
- if(d_limit.tv_usec > 1000000) {
- ++d_limit.tv_sec;
- d_limit.tv_usec -= 1000000;
- }
- Trace("limit") << "SatTimer::set(): limit is at " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
- }
-
- /** Return the milliseconds elapsed since last set(). */
- unsigned long elapsed() {
- timeval tv;
- gettimeofday(&tv, NULL);
- Trace("limit") << "SatTimer::elapsed(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl;
- tv.tv_sec -= d_limit.tv_sec - d_ms / 1000;
- tv.tv_usec -= d_limit.tv_usec - (d_ms % 1000) * 1000;
- Trace("limit") << "SatTimer::elapsed(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
- return tv.tv_sec * 1000 + tv.tv_usec / 1000;
- }
-
- bool expired() {
- if(on()) {
- timeval tv;
- gettimeofday(&tv, NULL);
- Trace("limit") << "SatTimer::expired(): current time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
- Trace("limit") << "SatTimer::expired(): limit time is " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
- if(d_limit.tv_sec < tv.tv_sec ||
- (d_limit.tv_sec == tv.tv_sec && d_limit.tv_usec <= tv.tv_usec)) {
- Trace("limit") << "SatTimer::expired(): OVER LIMIT!" << std::endl;
- return true;
- } else {
- Trace("limit") << "SatTimer::expired(): within limit" << std::endl;
- }
- }
- return false;
- }
-
- /** Check the current time and signal the PropEngine if over-time. */
- void check();
-
-};/* class SatTimer */
-
-/**
* PropEngine is the abstraction of a Sat Solver, providing methods for
* solving the SAT problem and conversion to CNF (via the CnfStream).
*/
@@ -152,11 +82,10 @@ class PropEngine {
/** The CNF converter in use */
CnfStream* d_cnfStream;
- /** A timer for SAT calls */
- SatTimer d_satTimer;
-
/** Whether we were just interrupted (or not) */
bool d_interrupted;
+ /** Pointer to resource manager for associated SmtEngine */
+ ResourceManager* d_resourceManager;
/** Dump out the satisfying assignment (after SAT result) */
void printSatisfyingAssignment();
@@ -236,12 +165,8 @@ public:
/**
* Checks the current context for satisfiability.
*
- * @param millis the time limit for this call in milliseconds
- * (0==off); on output, it is set to the milliseconds used
- * @param on input, resource the number of resource units permitted
- * for this call (0==off); on output, it is set to the resource used
*/
- Result checkSat(unsigned long& millis, unsigned long& resource);
+ Result checkSat();
/**
* Get the value of a boolean variable.
@@ -295,21 +220,15 @@ public:
bool isRunning() const;
/**
- * Check the current time budget.
- */
- void checkTime();
-
- /**
* Interrupt a running solver (cause a timeout).
*/
void interrupt() throw(ModalException);
/**
- * "Spend" a "resource." If the sum of these externally-counted
- * resources and SAT-internal resources exceed the current limit,
- * SAT should terminate.
+ * Informs the ResourceManager that a resource has been spent. If out of
+ * resources, can throw an UnsafeInterruptException exception.
*/
- void spendResource() throw();
+ void spendResource() throw (UnsafeInterruptException);
/**
* For debugging. Return true if "expl" is a well-formed
@@ -326,17 +245,6 @@ public:
};/* class PropEngine */
-inline void SatTimer::check() {
- if(d_propEngine.isRunning() && expired()) {
- Trace("limit") << "SatTimer::check(): interrupt!" << std::endl;
- d_propEngine.interrupt();
- }
-}
-
-inline void PropEngine::checkTime() {
- d_satTimer.check();
-}
-
}/* CVC4::prop namespace */
}/* CVC4 namespace */
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index adf6dfd07..b71844590 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -62,12 +62,6 @@ public:
/** Check the satisfiability of the added clauses */
virtual SatValue solve(long unsigned int&) = 0;
- /**
- * Instruct the solver that it should bump its consumed resource count.
- * Returns true if resources are exhausted.
- */
- virtual bool spendResource() = 0;
-
/** Interrupt the solver */
virtual void interrupt() = 0;
@@ -102,6 +96,7 @@ public:
* Notify about a learnt clause.
*/
virtual void notify(SatClause& clause) = 0;
+ virtual void spendResource() = 0;
virtual void safePoint() = 0;
};/* class BVSatSolverInterface::Notify */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 2bcd48099..59e87dd33 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -103,7 +103,7 @@ TNode TheoryProxy::getNode(SatLiteral lit) {
}
void TheoryProxy::notifyRestart() {
- d_propEngine->checkTime();
+ d_propEngine->spendResource();
d_theoryEngine->notifyRestart();
static uint32_t lemmaCount = 0;
@@ -179,8 +179,8 @@ void TheoryProxy::logDecision(SatLiteral lit) {
#endif /* CVC4_REPLAY */
}
-void TheoryProxy::checkTime() {
- d_propEngine->checkTime();
+void TheoryProxy::spendResource() {
+ d_theoryEngine->spendResource();
}
bool TheoryProxy::isDecisionRelevant(SatVariable var) {
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index a962f653a..3565aa501 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -111,7 +111,7 @@ public:
void logDecision(SatLiteral lit);
- void checkTime();
+ void spendResource();
bool isDecisionEngineDone();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback