From: Morgan Deters Date: Thu, 13 Oct 2011 04:14:38 +0000 (+0000) Subject: Interruption, time-out, and deterministic time-out ("resource-out") features. X-Git-Tag: cvc5-1.0.0~8419 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3cbb76ef86a769cfe3dac5976a14e1bc43c42ca6;p=cvc5.git 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. --- diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 6adcb62a9..84ed78662 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1191,7 +1191,7 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, TypeNode child2, TypeNode child3) { - return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();; + return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode(); } // N-ary version for types 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 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,11 +208,18 @@ 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. */ @@ -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 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f80d9a135..ecd61c0b4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -180,9 +180,25 @@ using namespace CVC4::smt; SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_context(em->getContext()), + d_userLevels(), d_userContext(new UserContext()), d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), + d_theoryEngine(NULL), + d_propEngine(NULL), + d_definedFunctions(NULL), + d_assertionList(NULL), + d_assignments(NULL), + d_logic(""), + d_problemExtended(false), + d_queryMade(false), + d_timeBudgetCumulative(0), + d_timeBudgetPerCall(0), + d_resourceBudgetCumulative(0), + d_resourceBudgetPerCall(0), + d_cumulativeTimeUsed(0), + d_cumulativeResourceUsed(0), + d_status(), d_private(new smt::SmtEnginePrivate(*this)), d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), @@ -212,14 +228,22 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); - d_assertionList = NULL; if(Options::current()->interactive) { d_assertionList = new(true) AssertionList(d_userContext); } - d_assignments = NULL; - d_problemExtended = false; - d_queryMade = false; + if(Options::current()->perCallResourceLimit != 0) { + setResourceLimit(Options::current()->perCallResourceLimit, false); + } + if(Options::current()->cumulativeResourceLimit != 0) { + setResourceLimit(Options::current()->cumulativeResourceLimit, true); + } + if(Options::current()->perCallMillisecondLimit != 0) { + setTimeLimit(Options::current()->perCallMillisecondLimit, false); + } + if(Options::current()->cumulativeMillisecondLimit != 0) { + setTimeLimit(Options::current()->cumulativeMillisecondLimit, true); + } } void SmtEngine::shutdown() { @@ -719,12 +743,44 @@ void SmtEnginePrivate::simplifyAssertions() Result SmtEngine::check() { Trace("smt") << "SmtEngine::check()" << endl; - // make sure the prop layer has all assertions - Trace("smt") << "SmtEngine::check(): processing assertion" << endl; + // Make sure the prop layer has all of the assertions + Trace("smt") << "SmtEngine::check(): processing assertions" << endl; d_private->processAssertions(); + unsigned long millis = 0; + if(d_timeBudgetCumulative != 0) { + millis = getTimeRemaining(); + if(millis == 0) { + return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT); + } + } + if(d_timeBudgetPerCall != 0 && (millis == 0 || d_timeBudgetPerCall < millis)) { + millis = d_timeBudgetPerCall; + } + + unsigned long resource = 0; + if(d_resourceBudgetCumulative != 0) { + resource = getResourceRemaining(); + if(resource == 0) { + return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT); + } + } + if(d_resourceBudgetPerCall != 0 && (resource == 0 || d_resourceBudgetPerCall < resource)) { + resource = d_resourceBudgetPerCall; + } + Trace("smt") << "SmtEngine::check(): running check" << endl; - return d_propEngine->checkSat(); + Result result = d_propEngine->checkSat(millis, resource); + + // PropEngine::checkSat() returns the actual amount used in these + // variables. + d_cumulativeTimeUsed += millis; + d_cumulativeResourceUsed += resource; + + Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed + << ", conflicts " << d_cumulativeResourceUsed << std::endl; + + return result; } Result SmtEngine::quickCheck() { @@ -1082,6 +1138,9 @@ void SmtEngine::pop() { if(!Options::current()->incrementalSolving) { throw ModalException("Cannot pop when not solving incrementally (use --incremental)"); } + if(d_userContext->getLevel() == 0) { + throw ModalException("Cannot pop beyond the first user frame"); + } AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel()); while (d_userLevels.back() < d_userContext->getLevel()) { internalPop(); @@ -1113,6 +1172,56 @@ void SmtEngine::internalPop() { } } +void SmtEngine::interrupt() throw(ModalException) { + d_propEngine->interrupt(); +} + +void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) { + if(cumulative) { + Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << std::endl; + d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units); + } else { + Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << std::endl; + d_resourceBudgetPerCall = units; + } +} + +void SmtEngine::setTimeLimit(unsigned long millis, bool cumulative) { + if(cumulative) { + Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << std::endl; + d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis); + } else { + Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << std::endl; + d_timeBudgetPerCall = millis; + } +} + +unsigned long SmtEngine::getResourceUsage() const { + return d_cumulativeResourceUsed; +} + +unsigned long SmtEngine::getTimeUsage() const { + return d_cumulativeTimeUsed; +} + +unsigned long SmtEngine::getResourceRemaining() const throw(ModalException) { + if(d_resourceBudgetCumulative == 0) { + throw ModalException("No cumulative resource limit is currently set"); + } + + return d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 : + d_resourceBudgetCumulative - d_cumulativeResourceUsed; +} + +unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) { + if(d_timeBudgetCumulative == 0) { + throw ModalException("No cumulative time limit is currently set"); + } + + return d_timeBudgetCumulative <= d_cumulativeTimeUsed ? 0 : + d_timeBudgetCumulative - d_cumulativeTimeUsed; +} + StatisticsRegistry* SmtEngine::getStatisticsRegistry() const { return d_exprManager->d_nodeManager->getStatisticsRegistry(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f5036bed7..f898ee76a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -104,7 +104,7 @@ class CVC4_PUBLIC SmtEngine { /** Our expression manager */ ExprManager* d_exprManager; - /** Out internal expression/node manager */ + /** Our internal expression/node manager */ NodeManager* d_nodeManager; /** The decision engine */ TheoryEngine* d_theoryEngine; @@ -143,6 +143,20 @@ class CVC4_PUBLIC SmtEngine { */ bool d_queryMade; + /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */ + unsigned long d_timeBudgetCumulative; + /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */ + unsigned long d_timeBudgetPerCall; + /** A user-imposed cumulative resource budget. 0 = no limit. */ + unsigned long d_resourceBudgetCumulative; + /** A user-imposed per-call resource budget. 0 = no limit. */ + unsigned long d_resourceBudgetPerCall; + + /** The number of milliseconds used by this SmtEngine since its inception. */ + unsigned long d_cumulativeTimeUsed; + /** The amount of resource used by this SmtEngine since its inception. */ + unsigned long d_cumulativeResourceUsed; + /** * Most recent result of last checkSat/query or (set-info :status). */ @@ -323,6 +337,104 @@ public: */ void pop(); + /** + * Interrupt a running query. This can be called from another thread + * or from a signal handler. Throws a ModalException if the SmtEngine + * isn't currently in a query. + */ + void interrupt() throw(ModalException); + + /** + * Set a resource limit for SmtEngine operations. This is like a time + * limit, but it's deterministic so that reproducible results can be + * obtained. However, please note that it may not be deterministic + * between different versions of CVC4, or even the same version on + * different platforms. + * + * A cumulative and non-cumulative (per-call) resource limit can be + * set at the same time. A call to setResourceLimit() with + * cumulative==true replaces any cumulative resource limit currently + * in effect; a call with cumulative==false replaces any per-call + * resource limit currently in effect. Time limits can be set in + * addition to resource limits; the SmtEngine obeys both. That means + * that up to four independent limits can control the SmtEngine + * at the same time. + * + * When an SmtEngine is first created, it has no time or resource + * limits. + * + * Currently, these limits only cause the SmtEngine to stop what its + * doing when the limit expires (or very shortly thereafter); no + * heuristics are altered by the limits or the threat of them expiring. + * We reserve the right to change this in the future. + * + * @param units the resource limit, or 0 for no limit + * @param cumulative whether this resource limit is to be a cumulative + * resource limit for all remaining calls into the SmtEngine (true), or + * whether it's a per-call resource limit (false); the default is false + */ + void setResourceLimit(unsigned long units, bool cumulative = false); + + /** + * Set a time limit for SmtEngine operations. + * + * A cumulative and non-cumulative (per-call) time limit can be + * set at the same time. A call to setTimeLimit() with + * cumulative==true replaces any cumulative time limit currently + * in effect; a call with cumulative==false replaces any per-call + * time limit currently in effect. Resource limits can be set in + * addition to time limits; the SmtEngine obeys both. That means + * that up to four independent limits can control the SmtEngine + * at the same time. + * + * Note that the cumulative timer only ticks away when one of the + * SmtEngine's workhorse functions (things like assertFormula(), + * query(), checkSat(), and simplify()) are running. Between calls, + * the timer is still. + * + * When an SmtEngine is first created, it has no time or resource + * limits. + * + * Currently, these limits only cause the SmtEngine to stop what its + * doing when the limit expires (or very shortly thereafter); no + * heuristics are altered by the limits or the threat of them expiring. + * We reserve the right to change this in the future. + * + * @param millis the time limit in milliseconds, or 0 for no limit + * @param cumulative whether this time limit is to be a cumulative + * time limit for all remaining calls into the SmtEngine (true), or + * whether it's a per-call time limit (false); the default is false + */ + void setTimeLimit(unsigned long millis, bool cumulative = false); + + /** + * Get the current resource usage count for this SmtEngine. This + * function can be used to ascertain reasonable values to pass as + * resource limits to setResourceLimit(). + */ + unsigned long getResourceUsage() const; + + /** + * Get the current millisecond count for this SmtEngine. + */ + unsigned long getTimeUsage() const; + + /** + * Get the remaining resources that can be consumed by this SmtEngine + * according to the currently-set cumulative resource limit. If there + * is not a cumulative resource limit set, this function throws a + * ModalException. + */ + unsigned long getResourceRemaining() const throw(ModalException); + + /** + * Get the remaining number of milliseconds that can be consumed by + * this SmtEngine according to the currently-set cumulative time limit. + * If there is not a cumulative resource limit set, this function + * throws a ModalException. + */ + unsigned long getTimeRemaining() const throw(ModalException); + /** * Permit access to the underlying StatisticsRegistry. */ diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index 941b9d0b4..851a6893c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -277,7 +277,7 @@ bool RewriteRule::applies(Node node) { template<> Node RewriteRule::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - return node[1].eqNode(node[0]);; + return node[1].eqNode(node[0]); } } diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index f5bf620bf..625abc580 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -105,6 +105,20 @@ public: */ virtual void setIncomplete() throw(AssertionException) = 0; + /** + * "Spend" a "resource." The meaning is specific to the context in + * which the theory is operating, and may even be ignored. The + * intended meaning is that if the user has set a limit on the "units + * of resource" that can be expended in a search, and that limit is + * exceeded, then the search is terminated. Note that the check for + * termination occurs in the main search loop, so while theories + * should call OutputChannel::spendResource() during particularly + * long-running operations, they cannot rely on resource() to break + * out of infinite or intractable computations. + */ + virtual void spendResource() throw() { + } + };/* class OutputChannel */ }/* CVC4::theory namespace */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2d4672776..2cd3f4d72 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -100,6 +100,8 @@ void TheoryEngine::preRegister(TNode preprocessed) { */ void TheoryEngine::check(Theory::Effort effort) { + d_propEngine->checkTime(); + #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif @@ -263,20 +265,38 @@ bool TheoryEngine::properConflict(TNode conflict) const { bool value; if (conflict.getKind() == kind::AND) { for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) { - if (!getPropEngine()->hasValue(conflict[i], value)) return false; - if (!value) return false; + if (! getPropEngine()->hasValue(conflict[i], value)) { + Debug("properConflict") << "Bad conflict is due to unassigned atom: " + << conflict[i] << endl; + return false; + } + if (! value) { + Debug("properConflict") << "Bad conflict is due to false atom: " + << conflict[i] << endl; + return false; + } } } else { - if (!getPropEngine()->hasValue(conflict, value)) return false; - return value; + if (! getPropEngine()->hasValue(conflict, value)) { + Debug("properConflict") << "Bad conflict is due to unassigned atom: " + << conflict << endl; + return false; + } + if(! value) { + Debug("properConflict") << "Bad conflict is due to false atom: " + << conflict << endl; + return false; + } } return true; } bool TheoryEngine::properPropagation(TNode lit) const { - Assert(!lit.isNull()); -#warning implement TheoryEngine::properPropagation() - return true; + if(!getPropEngine()->isTranslatedSatLiteral(lit)) { + return false; + } + bool b; + return !getPropEngine()->hasValue(lit, b); } bool TheoryEngine::properExplanation(TNode node, TNode expl) const { @@ -471,6 +491,8 @@ void TheoryEngine::assertFact(TNode node) { Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + d_propEngine->checkTime(); + // Get the atom TNode atom = node.getKind() == kind::NOT ? node[0] : node; @@ -497,6 +519,8 @@ void TheoryEngine::assertFact(TNode node) void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Debug("theory") << "EngineOutputChannel::propagate(" << literal << ")" << std::endl; + + d_propEngine->checkTime(); if(Dump.isOn("t-propagations")) { Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") << std::endl diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 915373074..be3068a45 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -209,6 +209,11 @@ class TheoryEngine { void setIncomplete() throw(AssertionException) { d_engine->setIncomplete(d_theory); } + + void spendResource() throw() { + d_engine->spendResource(); + } + };/* class EngineOutputChannel */ /** @@ -223,7 +228,7 @@ class TheoryEngine { void conflict(TNode conflict) { - Assert(properConflict(conflict)); + Assert(properConflict(conflict), "not a proper conflict: %s", conflict.toString().c_str()); // Mark that we are in conflict d_inConflict = true; @@ -256,6 +261,13 @@ class TheoryEngine { d_incomplete = true; } + /** + * "Spend" a resource during a search or preprocessing. + */ + void spendResource() throw() { + d_propEngine->spendResource(); + } + /** * Is the theory active. */ diff --git a/src/util/options.cpp b/src/util/options.cpp index 9c438a5cd..a01237fd0 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -138,7 +138,11 @@ static const string optionsDescription = "\ --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ --disable-arithmetic-propagation turns on arithmetic propagation\n\ --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\ - --incremental | -i enable incremental solving\n"; + --incremental | -i enable incremental solving\n\ + --time-limit=MS enable time limiting (give milliseconds)\n\ + --time-limit-per=MS enable time limiting per query (give milliseconds)\n\ + --limit=N enable resource limiting\n\ + --limit-per=N enable resource limiting per query\n"; #warning "Change CL options as --disable-variable-removal cannot do anything currently." @@ -296,7 +300,11 @@ enum OptionValue { ARITHMETIC_PROPAGATION, ARITHMETIC_PIVOT_THRESHOLD, ARITHMETIC_PROP_MAX_LENGTH, - DISABLE_SYMMETRY_BREAKER + DISABLE_SYMMETRY_BREAKER, + TIME_LIMIT, + TIME_LIMIT_PER, + LIMIT, + LIMIT_PER };/* enum OptionValue */ /** @@ -371,6 +379,10 @@ static struct option cmdlineOptions[] = { { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL }, { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, + { "time-limit" , required_argument, NULL, TIME_LIMIT }, + { "time-limit-per", required_argument, NULL, TIME_LIMIT_PER }, + { "limit" , required_argument, NULL, LIMIT }, + { "limit-per" , required_argument, NULL, LIMIT_PER }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -677,6 +689,43 @@ throw(OptionException) { ufSymmetryBreaker = false; break; + case TIME_LIMIT: + { + int i = atoi(optarg); + if(i < 0) { + throw OptionException("--time-limit requires a nonnegative argument."); + } + cumulativeMillisecondLimit = (unsigned long) i; + } + break; + case TIME_LIMIT_PER: + { + int i = atoi(optarg); + if(i < 0) { + throw OptionException("--time-limit-per requires a nonnegative argument."); + } + perCallMillisecondLimit = (unsigned long) i; + } + break; + case LIMIT: + { + int i = atoi(optarg); + if(i < 0) { + throw OptionException("--limit requires a nonnegative argument."); + } + cumulativeResourceLimit = (unsigned long) i; + } + break; + case LIMIT_PER: + { + int i = atoi(optarg); + if(i < 0) { + throw OptionException("--limit-per requires a nonnegative argument."); + } + perCallResourceLimit = (unsigned long) i; + break; + } + case RANDOM_SEED: satRandomSeed = atof(optarg); break; diff --git a/src/util/options.h b/src/util/options.h index 7fc894d93..f9dc042d1 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -129,6 +129,16 @@ struct CVC4_PUBLIC Options { */ bool interactiveSetByUser; + /** Per-query resource limit. */ + unsigned long perCallResourceLimit; + /** Cumulative resource limit. */ + unsigned long cumulativeResourceLimit; + + /** Per-query time limit in milliseconds. */ + unsigned long perCallMillisecondLimit; + /** Cumulative time limit in milliseconds. */ + unsigned long cumulativeMillisecondLimit; + /** Whether we should "spin" on a SIG_SEGV. */ bool segvNoSpin; diff --git a/src/util/result.cpp b/src/util/result.cpp index 8a2bcf3b2..bdb17f54c 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -55,10 +55,18 @@ Result::Result(const std::string& instr) : d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = TIMEOUT; + } else if(s == "resourceout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = RESOURCEOUT; } else if(s == "memout") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = MEMOUT; + } else if(s == "interrupted") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = INTERRUPTED; } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; @@ -169,8 +177,11 @@ ostream& operator<<(ostream& out, case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break; case Result::INCOMPLETE: out << "INCOMPLETE"; break; case Result::TIMEOUT: out << "TIMEOUT"; break; + case Result::RESOURCEOUT: out << "RESOURCEOUT"; break; case Result::MEMOUT: out << "MEMOUT"; break; + case Result::INTERRUPTED: out << "INTERRUPTED"; break; case Result::NO_STATUS: out << "NO_STATUS"; break; + case Result::UNSUPPORTED: out << "UNSUPPORTED"; break; case Result::OTHER: out << "OTHER"; break; case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break; default: Unhandled(e); diff --git a/src/util/result.h b/src/util/result.h index c4733eab9..ac52ee382 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -59,7 +59,9 @@ public: REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT, + RESOURCEOUT, MEMOUT, + INTERRUPTED, NO_STATUS, UNSUPPORTED, OTHER, diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index 26b490d2d..2fe6c0210 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -81,6 +81,8 @@ public: void renewVar(SatLiteral lit, int level = -1) { } + void interrupt() { + } }; class CnfStreamBlack : public CxxTest::TestSuite {