diff options
Diffstat (limited to 'src/prop/prop_engine.h')
| -rw-r--r-- | src/prop/prop_engine.h | 108 |
1 files changed, 8 insertions, 100 deletions
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 */ |