diff options
author | Liana Hadarean <lianah@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
commit | 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 (patch) | |
tree | 845ae47600ffff9c68fa654c0f78d3474e406beb /src/smt | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/options | 12 | ||||
-rw-r--r-- | src/smt/options_handlers.h | 58 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 309 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 34 | ||||
-rw-r--r-- | src/smt/smt_engine_scope.h | 3 |
5 files changed, 228 insertions, 188 deletions
diff --git a/src/smt/options b/src/smt/options index 0dc416474..20dd5b7d5 100644 --- a/src/smt/options +++ b/src/smt/options @@ -87,14 +87,18 @@ option - regular-output-channel argument :handler CVC4::smt::setRegularOutputCha option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h" set the diagnostic output channel of the solver -common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" +common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler CVC4::smt::tlimitHandler :handler-include "smt/options_handlers.h" enable time limiting (give milliseconds) -common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" +common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" :handler CVC4::smt::tlimitPerHandler :handler-include "smt/options_handlers.h" enable time limiting per query (give milliseconds) -common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" +common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler CVC4::smt::rlimitHandler :handler-include "smt/options_handlers.h" enable resource limiting (currently, roughly the number of SAT conflicts) -common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" +common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler CVC4::smt::rlimitPerHandler :handler-include "smt/options_handlers.h" enable resource limiting per query +common-option hardLimit hard-limit --hard-limit bool :default false + the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out) +common-option cpuTime cpu-time --cpu-time bool :default false + measures CPU time if set to true and wall time if false (default false) expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index d02b88fd2..fc2b796d3 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -21,6 +21,7 @@ #include "cvc4autoconfig.h" #include "util/dump.h" +#include "util/resource_manager.h" #include "smt/modal_exception.h" #include "smt/smt_engine.h" #include "lib/strtok_r.h" @@ -452,6 +453,63 @@ inline void statsEnabledBuild(std::string option, bool value, SmtEngine* smt) th #endif /* CVC4_STATISTICS_ON */ } +inline unsigned long tlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + unsigned long ms; + std::istringstream convert(optarg); + if (!(convert >> ms)) + throw OptionException("option `"+option+"` requires a number as an argument"); + + // make sure the resource is set if the option is updated + // if the smt engine is null the resource will be set in the + if (smt != NULL) { + ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager(); + rm->setTimeLimit(ms, true); + } + return ms; +} + +inline unsigned long tlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + unsigned long ms; + + std::istringstream convert(optarg); + if (!(convert >> ms)) + throw OptionException("option `"+option+"` requires a number as an argument"); + + if (smt != NULL) { + ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager(); + rm->setTimeLimit(ms, false); + } + return ms; +} + +inline unsigned long rlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + unsigned long ms; + + std::istringstream convert(optarg); + if (!(convert >> ms)) + throw OptionException("option `"+option+"` requires a number as an argument"); + + if (smt != NULL) { + ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager(); + rm->setResourceLimit(ms, true); + } + return ms; +} + +inline unsigned long rlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + unsigned long ms; + + std::istringstream convert(optarg); + if (!(convert >> ms)) + throw OptionException("option `"+option+"` requires a number as an argument"); + + if (smt != NULL) { + ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager(); + rm->setResourceLimit(ms, false); + } + return ms; +} + }/* CVC4::smt namespace */ }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8bf093370..c87753d8d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -51,6 +51,7 @@ #include "main/options.h" #include "util/unsat_core.h" #include "util/proof.h" +#include "util/resource_manager.h" #include "proof/proof.h" #include "proof/proof_manager.h" #include "util/boolean_simplification.h" @@ -297,6 +298,10 @@ struct SmtEngineStatistics { */ class SmtEnginePrivate : public NodeManagerListener { SmtEngine& d_smt; + /** + * Manager for limiting time and abstract resource usage. + */ + ResourceManager* d_resourceManager; /** Learned literals */ vector<Node> d_nonClausalLearnedLiterals; @@ -435,12 +440,13 @@ private: * * Returns false if the formula simplifies to "false" */ - bool simplifyAssertions() throw(TypeCheckingException, LogicException); + bool simplifyAssertions() throw(TypeCheckingException, LogicException, UnsafeInterruptException); public: SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), + d_resourceManager(NULL), d_nonClausalLearnedLiterals(), d_realAssertionsEnd(0), d_booleanTermConverter(NULL), @@ -460,6 +466,7 @@ public: { d_smt.d_nodeManager->subscribeEvents(this); d_true = NodeManager::currentNM()->mkConst(true); + d_resourceManager = NodeManager::currentResourceManager(); } ~SmtEnginePrivate() { @@ -474,6 +481,11 @@ public: d_smt.d_nodeManager->unsubscribeEvents(this); } + ResourceManager* getResourceManager() { return d_resourceManager; } + void spendResource() throw(UnsafeInterruptException) { + d_resourceManager->spendResource(); + } + void nmNotifyNewSort(TypeNode tn, uint32_t flags) { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, @@ -562,7 +574,7 @@ public: * Expand definitions in n. */ Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly = false) - throw(TypeCheckingException, LogicException); + throw(TypeCheckingException, LogicException, UnsafeInterruptException); /** * Rewrite Boolean terms in a Node. @@ -685,12 +697,6 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_queryMade(false), d_needPostsolve(false), d_earlyTheoryPP(true), - d_timeBudgetCumulative(0), - d_timeBudgetPerCall(0), - d_resourceBudgetCumulative(0), - d_resourceBudgetPerCall(0), - d_cumulativeTimeUsed(0), - d_cumulativeResourceUsed(0), d_status(), d_private(NULL), d_smtAttributes(NULL), @@ -764,19 +770,6 @@ void SmtEngine::finishInit() { } d_dumpCommands.clear(); - if(options::perCallResourceLimit() != 0) { - setResourceLimit(options::perCallResourceLimit(), false); - } - if(options::cumulativeResourceLimit() != 0) { - setResourceLimit(options::cumulativeResourceLimit(), true); - } - if(options::perCallMillisecondLimit() != 0) { - setTimeLimit(options::perCallMillisecondLimit(), false); - } - if(options::cumulativeMillisecondLimit() != 0) { - setTimeLimit(options::cumulativeMillisecondLimit(), true); - } - PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); } @@ -1058,7 +1051,7 @@ void SmtEngine::setDefaults() { } // If in arrays, set the UF handler to arrays - if(d_logic.isTheoryEnabled(THEORY_ARRAY) && ( !d_logic.isQuantified() || + if(d_logic.isTheoryEnabled(THEORY_ARRAY) && ( !d_logic.isQuantified() || (d_logic.isQuantified() && !d_logic.isTheoryEnabled(THEORY_UF)))) { Theory::setUninterpretedSortOwner(THEORY_ARRAY); } else { @@ -1639,7 +1632,7 @@ void SmtEngine::defineFunction(Expr func, } Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) - throw(TypeCheckingException, LogicException) { + throw(TypeCheckingException, LogicException, UnsafeInterruptException) { stack< triple<Node, Node, bool> > worklist; stack<Node> result; @@ -1649,6 +1642,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF // or upward pass). do { + spendResource(); n = worklist.top().first; // n is the input / original Node node = worklist.top().second; // node is the output / result bool childrenPushed = worklist.top().third; @@ -1785,7 +1779,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF void SmtEnginePrivate::removeITEs() { d_smt.finalOptionsAreSet(); - + spendResource(); Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl; // Remove all of the ITE occurrences and normalize @@ -1797,6 +1791,7 @@ void SmtEnginePrivate::removeITEs() { void SmtEnginePrivate::staticLearning() { d_smt.finalOptionsAreSet(); + spendResource(); TimerStat::CodeTimer staticLearningTimer(d_smt.d_stats->d_staticLearningTime); @@ -1829,6 +1824,7 @@ static void dumpAssertions(const char* key, const AssertionPipeline& assertionLi // returns false if it learns a conflict bool SmtEnginePrivate::nonClausalSimplify() { + spendResource(); d_smt.finalOptionsAreSet(); if(options::unsatCores()) { @@ -2157,6 +2153,7 @@ void SmtEnginePrivate::bvAbstraction() { void SmtEnginePrivate::bvToBool() { Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl; + spendResource(); std::vector<Node> new_assertions; d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions); for (unsigned i = 0; i < d_assertions.size(); ++ i) { @@ -2167,10 +2164,13 @@ void SmtEnginePrivate::bvToBool() { bool SmtEnginePrivate::simpITE() { TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); + spendResource(); + Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl; unsigned numAssertionOnEntry = d_assertions.size(); for (unsigned i = 0; i < d_assertions.size(); ++i) { + spendResource(); Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]); d_assertions.replace(i, result); if(result.isConst() && !result.getConst<bool>()){ @@ -2217,6 +2217,7 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ void SmtEnginePrivate::unconstrainedSimp() { TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime); + spendResource(); Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl; d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref()); } @@ -2664,7 +2665,8 @@ void SmtEnginePrivate::doMiplibTrick() { // returns false if simplification led to "false" bool SmtEnginePrivate::simplifyAssertions() - throw(TypeCheckingException, LogicException) { + throw(TypeCheckingException, LogicException, UnsafeInterruptException) { + spendResource(); Assert(d_smt.d_pendingPops == 0); try { ScopeCounter depth(d_simplifyAssertionsDepth); @@ -2791,6 +2793,18 @@ Result SmtEngine::check() { Trace("smt") << "SmtEngine::check()" << endl; + ResourceManager* resourceManager = d_private->getResourceManager(); + + resourceManager->beginCall(); + + // Only way we can be out of resource is if cumulative budget is on + if (resourceManager->cumulativeLimitOn() && + resourceManager->out()) { + Result::UnknownExplanation why = resourceManager->outOfResources() ? + Result::RESOURCEOUT : Result::TIMEOUT; + return Result(Result::VALIDITY_UNKNOWN, why, d_filename); + } + // Make sure the prop layer has all of the assertions Trace("smt") << "SmtEngine::check(): processing assertions" << endl; d_private->processAssertions(); @@ -2810,41 +2824,16 @@ Result SmtEngine::check() { } } - unsigned long millis = 0; - if(d_timeBudgetCumulative != 0) { - millis = getTimeRemaining(); - if(millis == 0) { - return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT, d_filename); - } - } - 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, d_filename); - } - } - if(d_resourceBudgetPerCall != 0 && (resource == 0 || d_resourceBudgetPerCall < resource)) { - resource = d_resourceBudgetPerCall; - } - TimerStat::CodeTimer solveTimer(d_stats->d_solveTime); Chat() << "solving..." << endl; Trace("smt") << "SmtEngine::check(): running check" << endl; - Result result = d_propEngine->checkSat(millis, resource); + Result result = d_propEngine->checkSat(); - // PropEngine::checkSat() returns the actual amount used in these - // variables. - d_cumulativeTimeUsed += millis; - d_cumulativeResourceUsed += resource; + resourceManager->endCall(); + Trace("limit") << "SmtEngine::check(): cumulative millis " << resourceManager->getTimeUsage() + << ", resources " << resourceManager->getResourceUsage() << endl; - Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed - << ", conflicts " << d_cumulativeResourceUsed << endl; return Result(result, d_filename); } @@ -2917,6 +2906,9 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) { TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime); + + spendResource(); + if(d_booleanTermConverter == NULL) { // This needs to be initialized _after_ the whole SMT framework is in place, subscribed // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype @@ -2950,7 +2942,7 @@ Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) { void SmtEnginePrivate::processAssertions() { TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime); - + spendResource(); Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); @@ -3069,6 +3061,7 @@ void SmtEnginePrivate::processAssertions() { << "applying substitutions" << endl; for (unsigned i = 0; i < d_assertions.size(); ++ i) { Trace("simplify") << "applying to " << d_assertions[i] << endl; + spendResource(); d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i]))); Trace("simplify") << " got " << d_assertions[i] << endl; } @@ -3085,6 +3078,7 @@ void SmtEnginePrivate::processAssertions() { Chat() << "...doing bvToBool..." << endl; bvToBool(); dumpAssertions("post-bv-to-bool", d_assertions); + Trace("smt") << "POST bvToBool" << endl; } if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { @@ -3189,7 +3183,6 @@ void SmtEnginePrivate::processAssertions() { } dumpAssertions("post-static-learning", d_assertions); - Trace("smt") << "POST bvToBool" << endl; Debug("smt") << " d_assertions : " << d_assertions.size() << endl; @@ -3332,14 +3325,14 @@ void SmtEnginePrivate::processAssertions() { // introducing new ones dumpAssertions("post-everything", d_assertions); - + //set instantiation level of everything to zero if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){ for( unsigned i=0; i < d_assertions.size(); i++ ) { theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertions[i], 0 ); } } - + // Push the formula to SAT { Chat() << "converting to CNF..." << endl; @@ -3384,86 +3377,93 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { } Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) { - Assert(ex.isNull() || ex.getExprManager() == d_exprManager); - SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + try { + Assert(ex.isNull() || ex.getExprManager() == d_exprManager); + SmtScope smts(this); + finalOptionsAreSet(); + doPendingPops(); - Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl; + Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl; - if(d_queryMade && !options::incrementalSolving()) { - throw ModalException("Cannot make multiple queries unless " - "incremental solving is enabled " - "(try --incremental)"); - } + if(d_queryMade && !options::incrementalSolving()) { + throw ModalException("Cannot make multiple queries unless " + "incremental solving is enabled " + "(try --incremental)"); + } - Expr e; - if(!ex.isNull()) { - // Substitute out any abstract values in ex. - e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); - // Ensure expr is type-checked at this point. - ensureBoolean(e); - // Give it to proof manager - PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); ); - } + Expr e; + if(!ex.isNull()) { + // Substitute out any abstract values in ex. + e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); + // Ensure expr is type-checked at this point. + ensureBoolean(e); + // Give it to proof manager + PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); ); + } - // check to see if a postsolve() is pending - if(d_needPostsolve) { - d_theoryEngine->postsolve(); - d_needPostsolve = false; - } + // check to see if a postsolve() is pending + if(d_needPostsolve) { + d_theoryEngine->postsolve(); + d_needPostsolve = false; + } - // Push the context - internalPush(); + // Push the context + internalPush(); - // Note that a query has been made - d_queryMade = true; + // Note that a query has been made + d_queryMade = true; - // Add the formula - if(!e.isNull()) { - d_problemExtended = true; - if(d_assertionList != NULL) { - d_assertionList->push_back(e); + // Add the formula + if(!e.isNull()) { + d_problemExtended = true; + if(d_assertionList != NULL) { + d_assertionList->push_back(e); + } + d_private->addFormula(e.getNode()); } - d_private->addFormula(e.getNode()); - } - // Run the check - Result r = check().asSatisfiabilityResult(); - d_needPostsolve = true; + Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + r = check().asSatisfiabilityResult(); + d_needPostsolve = true; - // Dump the query if requested - if(Dump.isOn("benchmark")) { - // the expr already got dumped out if assertion-dumping is on - Dump("benchmark") << CheckSatCommand(); - } + // Dump the query if requested + if(Dump.isOn("benchmark")) { + // the expr already got dumped out if assertion-dumping is on + Dump("benchmark") << CheckSatCommand(); + } - // Pop the context - internalPop(); + // Pop the context + internalPop(); - // Remember the status - d_status = r; + // Remember the status + d_status = r; - d_problemExtended = false; + d_problemExtended = false; - Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl; + Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl; - // Check that SAT results generate a model correctly. - if(options::checkModels()) { - if(r.asSatisfiabilityResult().isSat() == Result::SAT || - (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){ - checkModel(/* hard failure iff */ ! r.isUnknown()); + // Check that SAT results generate a model correctly. + if(options::checkModels()) { + if(r.asSatisfiabilityResult().isSat() == Result::SAT || + (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){ + checkModel(/* hard failure iff */ ! r.isUnknown()); + } } - } - // Check that UNSAT results generate a proof correctly. - if(options::checkProofs()) { - if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { - TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); - checkProof(); + // Check that UNSAT results generate a proof correctly. + if(options::checkProofs()) { + if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); + checkProof(); + } } - } - return r; + return r; + } catch (UnsafeInterruptException& e) { + AlwaysAssert(d_private->getResourceManager()->out()); + Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ? + Result::RESOURCEOUT : Result::TIMEOUT; + return Result(Result::SAT_UNKNOWN, why, d_filename); + } }/* SmtEngine::checkSat() */ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) { @@ -3474,6 +3474,7 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce doPendingPops(); Trace("smt") << "SMT query(" << ex << ")" << endl; + try { if(d_queryMade && !options::incrementalSolving()) { throw ModalException("Cannot make multiple queries unless " "incremental solving is enabled " @@ -3507,7 +3508,8 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce d_private->addFormula(e.getNode().notNode()); // Run the check - Result r = check().asValidityResult(); + Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + r = check().asValidityResult(); d_needPostsolve = true; // Dump the query if requested @@ -3542,9 +3544,15 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce } return r; + } catch (UnsafeInterruptException& e) { + AlwaysAssert(d_private->getResourceManager()->out()); + Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ? + Result::RESOURCEOUT : Result::TIMEOUT; + return Result(Result::VALIDITY_UNKNOWN, why, d_filename); + } }/* SmtEngine::query() */ -Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException) { +Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); @@ -3575,7 +3583,7 @@ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { return realValue; } -Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) { +Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); @@ -3598,7 +3606,9 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep return n.toExpr(); } -Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException) { +Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { + d_private->spendResource(); + Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); @@ -3621,7 +3631,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L return n.toExpr(); } -Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException) { +Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) { Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); @@ -3727,7 +3737,7 @@ bool SmtEngine::addToAssignment(const Expr& ex) throw() { return true; } -CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { +CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, UnsafeInterruptException) { Trace("smt") << "SMT getAssignment()" << endl; SmtScope smts(this); finalOptionsAreSet(); @@ -3826,7 +3836,7 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool } } -Model* SmtEngine::getModel() throw(ModalException) { +Model* SmtEngine::getModel() throw(ModalException, UnsafeInterruptException) { Trace("smt") << "SMT getModel()" << endl; SmtScope smts(this); @@ -4034,7 +4044,7 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; } -UnsatCore SmtEngine::getUnsatCore() throw(ModalException) { +UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptException) { Trace("smt") << "SMT getUnsatCore()" << endl; SmtScope smts(this); finalOptionsAreSet(); @@ -4058,7 +4068,7 @@ UnsatCore SmtEngine::getUnsatCore() throw(ModalException) { #endif /* CVC4_PROOF */ } -Proof* SmtEngine::getProof() throw(ModalException) { +Proof* SmtEngine::getProof() throw(ModalException, UnsafeInterruptException) { Trace("smt") << "SMT getProof()" << endl; SmtScope smts(this); finalOptionsAreSet(); @@ -4111,7 +4121,7 @@ vector<Expr> SmtEngine::getAssertions() throw(ModalException) { return vector<Expr>(d_assertionList->begin(), d_assertionList->end()); } -void SmtEngine::push() throw(ModalException, LogicException) { +void SmtEngine::push() throw(ModalException, LogicException, UnsafeInterruptException) { SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); @@ -4141,7 +4151,7 @@ void SmtEngine::push() throw(ModalException, LogicException) { << d_userContext->getLevel() << endl; } -void SmtEngine::pop() throw(ModalException) { +void SmtEngine::pop() throw(ModalException, UnsafeInterruptException) { SmtScope smts(this); finalOptionsAreSet(); Trace("smt") << "SMT pop()" << endl; @@ -4263,49 +4273,26 @@ void SmtEngine::interrupt() throw(ModalException) { } void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) { - if(cumulative) { - Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << endl; - d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units); - } else { - Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << endl; - d_resourceBudgetPerCall = units; - } + d_private->getResourceManager()->setResourceLimit(units, cumulative); } - -void SmtEngine::setTimeLimit(unsigned long millis, bool cumulative) { - if(cumulative) { - Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << endl; - d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis); - } else { - Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << endl; - d_timeBudgetPerCall = millis; - } +void SmtEngine::setTimeLimit(unsigned long milis, bool cumulative) { + d_private->getResourceManager()->setTimeLimit(milis, cumulative); } unsigned long SmtEngine::getResourceUsage() const { - return d_cumulativeResourceUsed; + return d_private->getResourceManager()->getResourceUsage(); } unsigned long SmtEngine::getTimeUsage() const { - return d_cumulativeTimeUsed; + return d_private->getResourceManager()->getTimeUsage(); } 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; + return d_private->getResourceManager()->getResourceRemaining(); } 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; + return d_private->getResourceManager()->getTimeRemaining(); } Statistics SmtEngine::getStatistics() const throw() { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 489d34d79..a39d2a7b5 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -35,6 +35,7 @@ #include "util/result.h" #include "util/sexpr.h" #include "util/hash.h" +#include "util/unsafe_interrupt_exception.h" #include "util/statistics.h" #include "theory/logic_info.h" @@ -233,19 +234,6 @@ class CVC4_PUBLIC SmtEngine { */ bool d_earlyTheoryPP; - /** 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). @@ -383,7 +371,7 @@ class CVC4_PUBLIC SmtEngine { * or INVALID query). Only permitted if CVC4 was built with model * support and produce-models is on. */ - Model* getModel() throw(ModalException); + Model* getModel() throw(ModalException, UnsafeInterruptException); // disallow copy/assignment SmtEngine(const SmtEngine&) CVC4_UNDEFINED; @@ -463,7 +451,7 @@ public: * takes a Boolean flag to determine whether to include this asserted * formula in an unsat core (if one is later requested). */ - Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException); + Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException, UnsafeInterruptException); /** * Check validity of an expression with respect to the current set @@ -487,20 +475,20 @@ public: * @todo (design) is this meant to give an equivalent or an * equisatisfiable formula? */ - Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException); + Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException); /** * Expand the definitions in a term or formula. No other * simplification or normalization is done. */ - Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException); + Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException); /** * Get the assigned value of an expr (only if immediately preceded * by a SAT or INVALID query). Only permitted if the SmtEngine is * set to operate interactively and produce-models is on. */ - Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException); + Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException); /** * Add a function to the set of expressions whose value is to be @@ -518,14 +506,14 @@ public: * INVALID query). Only permitted if the SmtEngine is set to * operate interactively and produce-assignments is on. */ - CVC4::SExpr getAssignment() throw(ModalException); + CVC4::SExpr getAssignment() throw(ModalException, UnsafeInterruptException); /** * Get the last proof (only if immediately preceded by an UNSAT * or VALID query). Only permitted if CVC4 was built with proof * support and produce-proofs is on. */ - Proof* getProof() throw(ModalException); + Proof* getProof() throw(ModalException, UnsafeInterruptException); /** * Print all instantiations made by the quantifiers module. @@ -537,7 +525,7 @@ public: * UNSAT or VALID query). Only permitted if CVC4 was built with * unsat-core support and produce-unsat-cores is on. */ - UnsatCore getUnsatCore() throw(ModalException); + UnsatCore getUnsatCore() throw(ModalException, UnsafeInterruptException); /** * Get the current set of assertions. Only permitted if the @@ -548,12 +536,12 @@ public: /** * Push a user-level context. */ - void push() throw(ModalException, LogicException); + void push() throw(ModalException, LogicException, UnsafeInterruptException); /** * Pop a user-level context. Throws an exception if nothing to pop. */ - void pop() throw(ModalException); + void pop() throw(ModalException, UnsafeInterruptException); /** * Completely reset the state of the solver, as though destroyed and diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index fb5810fd5..701775c9c 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -38,6 +38,9 @@ inline SmtEngine* currentSmtEngine() { Assert(s_smtEngine_current != NULL); return s_smtEngine_current; } +inline bool smtEngineInScope() { + return s_smtEngine_current != NULL; +} inline ProofManager* currentProofManager() { #ifdef CVC4_PROOF |