diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
commit | 3cbb76ef86a769cfe3dac5976a14e1bc43c42ca6 (patch) | |
tree | e08efdc63abd663de4f5750db9326b69c79829e5 /src/prop | |
parent | 3a7aafccadbfa1543c435b7dfe4f53116224a11f (diff) |
Interruption, time-out, and deterministic time-out ("resource-out") features.
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.
Also implemented TheoryEngine::properPropagation().
Other minor things.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/Makefile.am | 1 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 55 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 146 | ||||
-rw-r--r-- | src/prop/sat.cpp | 4 | ||||
-rw-r--r-- | src/prop/sat.h | 28 |
5 files changed, 214 insertions, 20 deletions
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 30be07d7c..c9442a401 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -12,6 +12,7 @@ libprop_la_SOURCES = \ prop_engine.h \ sat.h \ sat.cpp \ + sat_timer.h \ cnf_stream.h \ cnf_stream.cpp diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index e123db0ed..3d5a27d00 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -62,7 +62,12 @@ public: PropEngine::PropEngine(TheoryEngine* te, Context* context) : d_inCheckSat(false), d_theoryEngine(te), - d_context(context) { + d_context(context), + d_satSolver(NULL), + d_cnfStream(NULL), + d_satTimer(*this), + d_interrupted(false) { + Debug("prop") << "Constructing the PropEngine" << endl; d_satSolver = new SatSolver(this, d_theoryEngine, d_context); @@ -121,7 +126,7 @@ void PropEngine::printSatisfyingAssignment(){ } } -Result PropEngine::checkSat() { +Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "PropEngine::checkSat()" << endl; @@ -133,22 +138,37 @@ Result PropEngine::checkSat() { d_theoryEngine->presolve(); if(Options::current()->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 - bool result = d_satSolver->solve(); + SatLiteralValue result = d_satSolver->solve(resource); + + millis = d_satTimer.elapsed(); - if( result && Debug.isOn("prop") ) { + if( result == l_Undef ) { + Result::UnknownExplanation why = + d_satTimer.expired() ? Result::TIMEOUT : + (d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT); + return Result(Result::SAT_UNKNOWN, why); + } + + if( result == l_True && Debug.isOn("prop") ) { printSatisfyingAssignment(); } - Debug("prop") << "PropEngine::checkSat() => " - << (result ? "true" : "false") << endl; - if(result && d_theoryEngine->isIncomplete()) { + Debug("prop") << "PropEngine::checkSat() => " << result << endl; + if(result == l_True && d_theoryEngine->isIncomplete()) { return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE); } - return Result(result ? Result::SAT : Result::UNSAT); + return Result(result == l_True ? Result::SAT : Result::UNSAT); } Node PropEngine::getValue(TNode node) { @@ -170,6 +190,10 @@ bool PropEngine::isSatLiteral(TNode node) { return d_cnfStream->hasLiteral(node); } +bool PropEngine::isTranslatedSatLiteral(TNode node) { + return d_cnfStream->isTranslated(node); +} + bool PropEngine::hasValue(TNode node, bool& value) { Assert(node.getType().isBoolean()); SatLiteral lit = d_cnfStream->getLiteral(node); @@ -203,5 +227,20 @@ void PropEngine::pop() { Debug("prop") << "pop()" << endl; } +void PropEngine::interrupt() throw(ModalException) { + if(! d_inCheckSat) { + throw ModalException("SAT solver is not currently solving anything; " + "cannot interrupt it"); + } + + d_interrupted = true; + d_satSolver->interrupt(); + Debug("prop") << "interrupt()" << endl; +} + +void PropEngine::spendResource() throw() { + // TODO implement me +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 16cb34e04..25697b856 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -26,6 +26,9 @@ #include "expr/node.h" #include "util/options.h" #include "util/result.h" +#include "smt/modal_exception.h" + +#include <sys/time.h> namespace CVC4 { @@ -36,6 +39,80 @@ namespace prop { class CnfStream; class SatSolver; +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). @@ -43,7 +120,7 @@ class SatSolver; class PropEngine { /** - * Indicates that the sat solver is currently solving something and we should + * Indicates that the SAT solver is currently solving something and we should * not mess with it's internal state. */ bool d_inCheckSat; @@ -51,6 +128,7 @@ class PropEngine { /** The theory engine we will be using */ TheoryEngine *d_theoryEngine; + /** The context */ context::Context* d_context; /** The SAT solver proxy */ @@ -62,6 +140,13 @@ 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; + + /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); public: @@ -86,27 +171,34 @@ public: void shutdown() { } /** - * Converts the given formula to CNF and assert the CNF to the sat solver. + * Converts the given formula to CNF and assert the CNF to the SAT solver. * The formula is asserted permanently for the current context. * @param node the formula to assert */ void assertFormula(TNode node); /** - * Converts the given formula to CNF and assert the CNF to the sat solver. - * The formula can be removed by the sat solver after backtracking lower + * Converts the given formula to CNF and assert the CNF to the SAT solver. + * The formula can be removed by the SAT solver after backtracking lower * than the (SAT and SMT) level at which it was asserted. * * @param node the formula to assert - * @param negated whether the node should be considered to be negated at the top level (or not) - * @param removable whether this lemma can be quietly removed based on an activity heuristic (or not) + * @param negated whether the node should be considered to be negated + * at the top level (or not) + * @param removable whether this lemma can be quietly removed based + * on an activity heuristic (or not) */ void assertLemma(TNode node, bool negated, bool removable); /** * 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(); + Result checkSat(unsigned long& millis, unsigned long& resource); /** * Get the value of a boolean variable. @@ -116,12 +208,19 @@ public: */ Node getValue(TNode node); - /* - * Return true if node has an associated SAT literal + /** + * Return true if node has an associated SAT literal. */ bool isSatLiteral(TNode node); /** + * Return true if node has an associated SAT literal that is + * currently translated (i.e., it's relevant to the current + * user push/pop level). + */ + bool isTranslatedSatLiteral(TNode node); + + /** * Check if the node has a value and return it if yes. */ bool hasValue(TNode node, bool& value); @@ -143,8 +242,37 @@ public: */ void pop(); + /** + * 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. + */ + void spendResource() throw(); + };/* class PropEngine */ + +inline void SatTimer::check() { + if(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.cpp b/src/prop/sat.cpp index 386fb5aad..5d53bf100 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -83,6 +83,7 @@ TNode SatSolver::getNode(SatLiteral lit) { } void SatSolver::notifyRestart() { + d_propEngine->checkTime(); d_theoryEngine->notifyRestart(); } @@ -108,6 +109,9 @@ void SatSolver::logDecision(SatLiteral lit) { #endif /* CVC4_REPLAY */ } +void SatSolver::checkTime() { + d_propEngine->checkTime(); +} }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/sat.h b/src/prop/sat.h index ee3978555..026193eae 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -114,6 +114,8 @@ public: virtual void unregisterVar(SatLiteral lit) = 0; /** Register the variable (of the literal) for solving */ virtual void renewVar(SatLiteral lit, int level = -1) = 0; + /** Interrupt the solver */ + virtual void interrupt() = 0; }; /** @@ -214,7 +216,7 @@ public: virtual ~SatSolver(); - bool solve(); + SatLiteralValue solve(unsigned long& resource); void addClause(SatClause& clause, bool removable); @@ -253,6 +255,8 @@ public: void renewVar(SatLiteral lit, int level = -1); + void interrupt(); + TNode getNode(SatLiteral lit); void notifyRestart(); @@ -261,6 +265,8 @@ public: void logDecision(SatLiteral lit); + void checkTime(); + };/* class SatSolver */ /* Functions that delegate to the concrete SAT solver. */ @@ -293,8 +299,20 @@ inline SatSolver::~SatSolver() { delete d_minisat; } -inline bool SatSolver::solve() { - return d_minisat->solve(); +inline SatLiteralValue SatSolver::solve(unsigned long& resource) { + Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; + if(resource == 0) { + d_minisat->budgetOff(); + } else { + d_minisat->setConfBudget(resource); + } + Minisat::vec<SatLiteral> empty; + unsigned long conflictsBefore = d_minisat->conflicts; + SatLiteralValue result = d_minisat->solveLimited(empty); + d_minisat->clearInterrupt(); + resource = d_minisat->conflicts - conflictsBefore; + Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl; + return result; } inline void SatSolver::addClause(SatClause& clause, bool removable) { @@ -333,6 +351,10 @@ inline void SatSolver::renewVar(SatLiteral lit, int level) { d_minisat->renewVar(lit, level); } +inline void SatSolver::interrupt() { + d_minisat->interrupt(); +} + #endif /* __CVC4_USE_MINISAT */ inline size_t |