From: Liana Hadarean Date: Mon, 17 Nov 2014 20:26:42 +0000 (-0500) Subject: Resource-limiting work. X-Git-Tag: cvc5-1.0.0~6492 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5;p=cvc5.git Resource-limiting work. Signed-off-by: Morgan Deters --- diff --git a/.mailmap b/.mailmap index 7cf2a12f0..eaae8872c 100644 --- a/.mailmap +++ b/.mailmap @@ -3,6 +3,7 @@ Morgan Deters Dejan Jovanovic Dejan Jovanovic Francois Bobot +Liana Hadarean Liana Hadarean Andrew Reynolds Andrew Reynolds diff --git a/src/cvc4.i b/src/cvc4.i index 62cd68cab..3ad08660c 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -153,6 +153,7 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %typemap(throws) CVC4::ScopeException = CVC4::Exception; %typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception; %typemap(throws) CVC4::AssertionException = CVC4::Exception; +%typemap(throws) CVC4::UnsafeInterruptException = CVC4::Exception; %typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception; %typemap(throws) CVC4::parser::ParserException = CVC4::Exception; @@ -293,6 +294,7 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; #endif /* SWIGJAVA */ %include "util/exception.i" +%include "util/unsafe_interrupt_exception.i" %include "util/integer.i" %include "util/rational.i" %include "util/language.i" @@ -319,6 +321,7 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %include "util/regexp.i" %include "util/uninterpreted_constant.i" %include "util/proof.i" +%include "util/resource_manager.i" %include "expr/kind.i" %include "expr/expr.i" diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 39ed89a68..61900e59d 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -30,6 +30,7 @@ #include "theory/decision_attributes.h" #include "util/ite_removal.h" #include "util/output.h" +#include "smt/smt_engine_scope.h" using namespace std; using namespace CVC4::prop; @@ -117,6 +118,7 @@ public: /** Gets the next decision based on strategies that are enabled */ SatLiteral getNext(bool &stopSearch) { + NodeManager::currentResourceManager()->spendResource(); Assert(d_cnfStream != NULL, "Forgot to set cnfStream for decision engine?"); Assert(d_satSolver != NULL, diff --git a/src/expr/command.cpp b/src/expr/command.cpp index be1b06cb8..242e018f6 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -39,6 +39,7 @@ namespace CVC4 { const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); +const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted(); std::ostream& operator<<(std::ostream& out, const Command& c) throw() { c.toStream(out, @@ -97,6 +98,10 @@ bool Command::fail() const throw() { return d_commandStatus != NULL && dynamic_cast(d_commandStatus) != NULL; } +bool Command::interrupted() const throw() { + return d_commandStatus != NULL && dynamic_cast(d_commandStatus) != NULL; +} + void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { invoke(smtEngine); if(!(isMuted() && ok())) { @@ -201,6 +206,8 @@ void AssertCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->assertFormula(d_expr, d_inUnsatCore); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -224,6 +231,8 @@ void PushCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->push(); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -247,6 +256,8 @@ void PopCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->pop(); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -840,6 +851,8 @@ void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() { try { d_result = smtEngine->simplify(d_term); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -953,6 +966,8 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { } d_result = em->mkExpr(kind::SEXPR, result); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -1000,6 +1015,8 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() { try { d_result = smtEngine->getAssignment(); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -1043,6 +1060,8 @@ void GetModelCommand::invoke(SmtEngine* smtEngine) throw() { d_result = smtEngine->getModel(); d_smtEngine = smtEngine; d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -1089,6 +1108,8 @@ void GetProofCommand::invoke(SmtEngine* smtEngine) throw() { try { d_result = smtEngine->getProof(); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } diff --git a/src/expr/command.h b/src/expr/command.h index c4f2fc1bc..cfa00bff4 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -168,6 +168,13 @@ public: CommandStatus& clone() const { return const_cast(*this); } };/* class CommandSuccess */ +class CVC4_PUBLIC CommandInterrupted : public CommandStatus { + static const CommandInterrupted* s_instance; +public: + static const CommandInterrupted* instance() throw() { return s_instance; } + CommandStatus& clone() const { return const_cast(*this); } +};/* class CommandInterrupted */ + class CVC4_PUBLIC CommandUnsupported : public CommandStatus { public: CommandStatus& clone() const { return *new CommandUnsupported(*this); } @@ -240,6 +247,11 @@ public: */ bool fail() const throw(); + /** + * The command was ran but was interrupted due to resource limiting. + */ + bool interrupted() const throw(); + /** Get the command status (it's NULL if we haven't run yet). */ const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index fb9da3e37..c5249075b 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -130,6 +130,10 @@ const Options& ExprManager::getOptions() const { return d_nodeManager->getOptions(); } +ResourceManager* ExprManager::getResourceManager() throw() { + return d_nodeManager->getResourceManager(); +} + BooleanType ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()))); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index deb2f6918..2fabea0ff 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -45,6 +45,7 @@ class Options; class IntStat; struct ExprManagerMapCollection; class StatisticsRegistry; +class ResourceManager; namespace expr { namespace pickle { @@ -120,9 +121,12 @@ public: */ ~ExprManager() throw(); - /** Get this node manager's options */ + /** Get this expr manager's options */ const Options& getOptions() const; + /** Get this expr manager's resource manager */ + ResourceManager* getResourceManager() throw(); + /** Get the type for booleans */ BooleanType booleanType() const; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 5c2b81645..48aacddf2 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -22,7 +22,9 @@ #include "expr/attribute.h" #include "util/cvc4_assert.h" #include "options/options.h" +#include "smt/options.h" #include "util/statistics_registry.h" +#include "util/resource_manager.h" #include "util/tls.h" #include "expr/type_checker.h" @@ -83,6 +85,7 @@ struct NVReclaim { NodeManager::NodeManager(ExprManager* exprManager) : d_options(new Options()), d_statisticsRegistry(new StatisticsRegistry()), + d_resourceManager(new ResourceManager()), next_id(0), d_attrManager(new expr::attr::AttributeManager()), d_exprManager(exprManager), @@ -97,6 +100,7 @@ NodeManager::NodeManager(ExprManager* exprManager, const Options& options) : d_options(new Options(options)), d_statisticsRegistry(new StatisticsRegistry()), + d_resourceManager(new ResourceManager()), next_id(0), d_attrManager(new expr::attr::AttributeManager()), d_exprManager(exprManager), @@ -117,6 +121,22 @@ void NodeManager::init() { d_operators[i] = mkConst(Kind(k)); } } + d_resourceManager->setHardLimit((*d_options)[options::hardLimit]); + if((*d_options)[options::perCallResourceLimit] != 0) { + d_resourceManager->setResourceLimit((*d_options)[options::perCallResourceLimit], false); + } + if((*d_options)[options::cumulativeResourceLimit] != 0) { + d_resourceManager->setResourceLimit((*d_options)[options::cumulativeResourceLimit], true); + } + if((*d_options)[options::perCallMillisecondLimit] != 0) { + d_resourceManager->setTimeLimit((*d_options)[options::perCallMillisecondLimit], false); + } + if((*d_options)[options::cumulativeMillisecondLimit] != 0) { + d_resourceManager->setTimeLimit((*d_options)[options::cumulativeMillisecondLimit], true); + } + if((*d_options)[options::cpuTime]) { + d_resourceManager->useCPUTime(true); + } } NodeManager::~NodeManager() { @@ -162,6 +182,8 @@ NodeManager::~NodeManager() { // defensive coding, in case destruction-order issues pop up (they often do) delete d_statisticsRegistry; d_statisticsRegistry = NULL; + delete d_resourceManager; + d_resourceManager = NULL; delete d_attrManager; d_attrManager = NULL; delete d_options; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index d4d89109c..f4c3a1999 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -42,6 +42,7 @@ namespace CVC4 { class StatisticsRegistry; +class ResourceManager; namespace expr { namespace attr { @@ -101,6 +102,7 @@ class NodeManager { Options* d_options; StatisticsRegistry* d_statisticsRegistry; + ResourceManager* d_resourceManager; NodeValuePool d_nodeValuePool; @@ -317,6 +319,8 @@ public: /** The node manager in the current public-facing CVC4 library context */ static NodeManager* currentNM() { return s_current; } + /** The resource manager associated with the current node manager */ + static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; } /** Get this node manager's options (const version) */ const Options& getOptions() const { @@ -328,6 +332,9 @@ public: return *d_options; } + /** Get this node manager's resource manager */ + ResourceManager* getResourceManager() throw() { return d_resourceManager; } + /** Get this node manager's statistics registry */ StatisticsRegistry* getStatisticsRegistry() const throw() { return d_statisticsRegistry; diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index df71f13c9..9035ed8b8 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -298,8 +298,21 @@ int runCvc4(int argc, char* argv[], Options& opts) { // have the replay parser use the declarations input interactively replayParser->useDeclarationsFrom(shell.getParser()); } - while((cmd = shell.readCommand())) { + + while(true) { + try { + cmd = shell.readCommand(); + } catch(UnsafeInterruptException& e) { + *opts[options::out] << CommandInterrupted(); + break; + } + if (cmd == NULL) + break; status = pExecutor->doCommand(cmd) && status; + if (cmd->interrupted()) { + delete cmd; + break; + } delete cmd; } } else if(opts[options::tearDownIncremental]) { @@ -332,15 +345,34 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(parser); } bool needReset = false; - while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { + // true if one of the commands was interrupted + bool interrupted = false; + while (status || opts[options::continuedExecution]) { + if (interrupted) { + *opts[options::out] << CommandInterrupted(); + break; + } + + try { + cmd = parser->nextCommand(); + if (cmd == NULL) break; + } catch (UnsafeInterruptException& e) { + interrupted = true; + continue; + } + if(dynamic_cast(cmd) != NULL) { if(needReset) { pExecutor->reset(); - for(size_t i = 0; i < allCommands.size(); ++i) { - for(size_t j = 0; j < allCommands[i].size(); ++j) { + for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { + if (interrupted) break; + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + } delete cmd; } } @@ -351,29 +383,44 @@ int runCvc4(int argc, char* argv[], Options& opts) { } else if(dynamic_cast(cmd) != NULL) { allCommands.pop_back(); // fixme leaks cmds here pExecutor->reset(); - for(size_t i = 0; i < allCommands.size(); ++i) { - for(size_t j = 0; j < allCommands[i].size(); ++j) { + for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + } delete cmd; } } + if (interrupted) continue; *opts[options::out] << CommandSuccess(); } else if(dynamic_cast(cmd) != NULL || dynamic_cast(cmd) != NULL) { if(needReset) { pExecutor->reset(); - for(size_t i = 0; i < allCommands.size(); ++i) { - for(size_t j = 0; j < allCommands[i].size(); ++j) { + for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + } delete cmd; } } } + if (interrupted) { + continue; + } + status = pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + continue; + } needReset = true; } else if(dynamic_cast(cmd) != NULL) { pExecutor->doCommand(cmd); @@ -396,6 +443,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { allCommands.back().push_back(copy); } status = pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + continue; + } + if(dynamic_cast(cmd) != NULL) { delete cmd; break; @@ -428,8 +480,27 @@ int runCvc4(int argc, char* argv[], Options& opts) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser); } - while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { + bool interrupted = false; + while(status || opts[options::continuedExecution]) { + if (interrupted) { + *opts[options::out] << CommandInterrupted(); + pExecutor->reset(); + break; + } + try { + cmd = parser->nextCommand(); + if (cmd == NULL) break; + } catch (UnsafeInterruptException& e) { + interrupted = true; + continue; + } + status = pExecutor->doCommand(cmd); + if (cmd->interrupted() && status == 0) { + interrupted = true; + break; + } + if(dynamic_cast(cmd) != NULL) { delete cmd; break; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 0aee195e4..3b237f6a4 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -172,7 +172,7 @@ InteractiveShell::~InteractiveShell() { #endif /* HAVE_LIBREADLINE */ } -Command* InteractiveShell::readCommand() { +Command* InteractiveShell::readCommand() throw (UnsafeInterruptException) { char* lineBuf = NULL; string line = ""; diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 43054f980..ef55919a1 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -19,6 +19,7 @@ #include #include "util/language.h" +#include "util/unsafe_interrupt_exception.h" #include "options/options.h" namespace CVC4 { @@ -56,7 +57,7 @@ public: * Read a command from the interactive shell. This will read as * many lines as necessary to parse a well-formed command. */ - Command* readCommand(); + Command* readCommand() throw (UnsafeInterruptException); /** * Return the internal parser being used. diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 045cd4ae1..dc44ed5ba 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -26,9 +26,12 @@ #include "parser/parser_exception.h" #include "expr/command.h" #include "expr/expr.h" +#include "expr/node.h" #include "expr/kind.h" #include "expr/type.h" #include "util/output.h" +#include "util/resource_manager.h" +#include "options/options.h" using namespace std; using namespace CVC4::kind; @@ -38,6 +41,7 @@ namespace parser { Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : d_exprManager(exprManager), + d_resourceManager(d_exprManager->getResourceManager()), d_input(input), d_symtabAllocated(), d_symtab(&d_symtabAllocated), @@ -460,7 +464,7 @@ void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); } -Command* Parser::nextCommand() throw(ParserException) { +Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException) { Debug("parser") << "nextCommand()" << std::endl; Command* cmd = NULL; if(!d_commandQueue.empty()) { @@ -483,11 +487,19 @@ Command* Parser::nextCommand() throw(ParserException) { } } Debug("parser") << "nextCommand() => " << cmd << std::endl; + if (cmd != NULL && + dynamic_cast(cmd) == NULL && + dynamic_cast(cmd) == NULL) { + // don't count set-option commands as to not get stuck in an infinite + // loop of resourcing out + d_resourceManager->spendResource(); + } return cmd; } -Expr Parser::nextExpression() throw(ParserException) { +Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) { Debug("parser") << "nextExpression()" << std::endl; + d_resourceManager->spendResource(); Expr result; if(!done()) { try { diff --git a/src/parser/parser.h b/src/parser/parser.h index ffe33a980..53241709d 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -30,6 +30,7 @@ #include "expr/symbol_table.h" #include "expr/kind.h" #include "expr/expr_stream.h" +#include "util/unsafe_interrupt_exception.h" namespace CVC4 { @@ -39,6 +40,7 @@ class ExprManager; class Command; class FunctionType; class Type; +class ResourceManager; namespace parser { @@ -108,6 +110,8 @@ class CVC4_PUBLIC Parser { /** The expression manager */ ExprManager *d_exprManager; + /** The resource manager associated with this expr manager */ + ResourceManager *d_resourceManager; /** The input that we're parsing. */ Input *d_input; @@ -504,10 +508,10 @@ public: bool isPredicate(const std::string& name); /** Parse and return the next command. */ - Command* nextCommand() throw(ParserException); + Command* nextCommand() throw(ParserException, UnsafeInterruptException); /** Parse and return the next expression. */ - Expr nextExpression() throw(ParserException); + Expr nextExpression() throw(ParserException, UnsafeInterruptException); /** Issue a warning to the user. */ inline void warning(const std::string& msg) { diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 94ca46257..c24ed8372 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -179,7 +179,8 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw if(tryToStream(out, s) || tryToStream(out, s) || - tryToStream(out, s)) { + tryToStream(out, s) || + tryToStream(out, s)) { return; } @@ -373,6 +374,10 @@ static void toStream(std::ostream& out, const CommandSuccess* s) throw() { } } +static void toStream(std::ostream& out, const CommandInterrupted* s) throw() { + out << "INTERRUPTED" << endl; +} + static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { out << "UNSUPPORTED" << endl; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index f8df9d906..2e1170666 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -905,7 +905,8 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw if(tryToStream(out, s, d_cvc3Mode) || tryToStream(out, s, d_cvc3Mode) || - tryToStream(out, s, d_cvc3Mode)) { + tryToStream(out, s, d_cvc3Mode) || + tryToStream(out, s, d_cvc3Mode)) { return; } @@ -1267,6 +1268,10 @@ static void toStream(std::ostream& out, const CommandUnsupported* s, bool cvc3Mo out << "UNSUPPORTED" << endl; } +static void toStream(std::ostream& out, const CommandInterrupted* s, bool cvc3Mode) throw() { + out << "INTERRUPTED" << endl; +} + static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode) throw() { out << s->getMessage() << endl; } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 88bcce5ae..4f12ed012 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -794,7 +794,8 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro if(tryToStream(out, s, d_variant) || tryToStream(out, s, d_variant) || - tryToStream(out, s, d_variant)) { + tryToStream(out, s, d_variant) || + tryToStream(out, s, d_variant)) { return; } @@ -1208,6 +1209,10 @@ static void toStream(std::ostream& out, const CommandSuccess* s, Variant v) thro } } +static void toStream(std::ostream& out, const CommandInterrupted* s, Variant v) throw() { + out << "interrupted" << endl; +} + static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) throw() { #ifdef CVC4_COMPETITION_MODE // if in competition mode, lie and say we're ok 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& 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 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 namespace CVC4 { +class ResourceManager; class DecisionEngine; class TheoryEngine; @@ -44,78 +46,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. @@ -294,22 +219,16 @@ 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(); 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 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& 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& cache, bool expandOnly) - throw(TypeCheckingException, LogicException) { + throw(TypeCheckingException, LogicException, UnsafeInterruptException) { stack< triple > worklist; stack result; @@ -1649,6 +1642,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mapd_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 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()){ @@ -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_mapd_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 SmtEngine::getAssertions() throw(ModalException) { return vector(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 diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 0ff12da95..e13587323 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -28,6 +28,7 @@ #include "prop/sat_solver.h" #include "theory/valuation.h" #include "theory/theory_registrar.h" +#include "util/resource_manager.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; @@ -134,6 +135,7 @@ class TLazyBitblaster : public TBitblaster { {} bool notify(prop::SatLiteral lit); void notify(prop::SatClause& clause); + void spendResource(); void safePoint(); }; @@ -228,7 +230,8 @@ private: Statistics(const std::string& name); ~Statistics(); }; - std::string d_name; + std::string d_name; +public: Statistics d_statistics; }; @@ -237,6 +240,9 @@ public: MinisatEmptyNotify() {} bool notify(prop::SatLiteral lit) { return true; } void notify(prop::SatClause& clause) { } + void spendResource() { + NodeManager::currentResourceManager()->spendResource(); + } void safePoint() {} }; diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index f9f8ff581..57a635c20 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -67,6 +67,7 @@ bool EagerBitblastSolver::isInitialized() { } void EagerBitblastSolver::assertFormula(TNode formula) { + d_bv->spendResource(); Assert (isInitialized()); Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula "<< formula <<"\n"; d_assertionSet.insert(formula); diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index e8acf268f..5b139e327 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -557,6 +557,7 @@ bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in) { void AlgebraicSolver::processAssertions(std::vector& worklist, SubstitutionEx& subst) { bool changed = true; while(changed) { + // d_bv->spendResource(); changed = false; for (unsigned i = 0; i < worklist.size(); ++i) { // apply current substitutions diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index d0b99f869..c86572ead 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -103,8 +103,11 @@ void BitblastSolver::bitblastQueue() { // don't bit-blast lemma atoms continue; } - Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n"; - d_bitblaster->bbAtom(atom); + Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n"; + { + TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer); + d_bitblaster->bbAtom(atom); + } } } @@ -149,6 +152,7 @@ bool BitblastSolver::check(Theory::Effort e) { // We need to ensure we are fully propagated, so propagate now if (d_useSatPropagation) { + d_bv->spendResource(); bool ok = d_bitblaster->propagate(); if (!ok) { std::vector conflictAtoms; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index d2c79fec2..938a93b85 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -166,6 +166,9 @@ bool CoreSolver::decomposeFact(TNode fact) { bool CoreSolver::check(Theory::Effort e) { Trace("bitvector::core") << "CoreSolver::check \n"; + + d_bv->spendResource(); + d_checkCalled = true; Assert (!d_bv->inConflict()); ++(d_statistics.d_numCallstoCheck); diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 917b10c33..660551fe2 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -29,6 +29,7 @@ using namespace CVC4::theory::bv::utils; bool InequalitySolver::check(Theory::Effort e) { Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n"; ++(d_statistics.d_numCallstoCheck); + d_bv->spendResource(); bool ok = true; while (!done() && ok) { diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 877baec4e..065d5d5ef 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -103,6 +103,7 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) { return; } + d_bv->spendResource(); Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; d_termBBStrategies[node.getKind()] (node, bits, this); diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index b74506e4d..e5b5ed664 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -170,6 +170,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) { return; } + d_bv->spendResource(); Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numTerms; @@ -355,6 +356,10 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { } } +void TLazyBitblaster::MinisatNotify::spendResource() { + d_bv->spendResource(); +} + void TLazyBitblaster::MinisatNotify::safePoint() { d_bv->d_out->safePoint(); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 99bc764dd..eddd5017c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -107,6 +107,10 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { } } +void TheoryBV::spendResource() throw(UnsafeInterruptException) { + getOutputChannel().spendResource(); +} + TheoryBV::Statistics::Statistics(): d_avgConflictSize("theory::bv::AvgBVConflictSize"), d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0), @@ -362,6 +366,7 @@ void TheoryBV::check(Effort e) return; } Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); // we may be getting new assertions so the model cache may not be sound d_invalidateModelCache.set(true); // if we are using the eager solver diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index a37a4019e..11d8cb895 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -103,6 +103,7 @@ private: Statistics d_statistics; + void spendResource() throw(UnsafeInterruptException); /** * Return the uninterpreted function symbol corresponding to division-by-zero @@ -218,6 +219,7 @@ private: friend class CoreSolver; friend class InequalitySolver; friend class AlgebraicSolver; + friend class EagerBitblastSolver; };/* class TheoryBV */ }/* CVC4::theory::bv namespace */ diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 40eba6ff5..fdf253d3f 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -21,6 +21,7 @@ #include "util/cvc4_assert.h" #include "theory/interrupted.h" +#include "util/resource_manager.h" namespace CVC4 { namespace theory { @@ -84,7 +85,7 @@ public: * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ - virtual void safePoint() throw(Interrupted, AssertionException) { + virtual void safePoint() throw(Interrupted, UnsafeInterruptException, AssertionException) { } /** @@ -97,7 +98,7 @@ public: * unit conflict) which is assigned TRUE (and T-conflicting) in the * current assignment. */ - virtual void conflict(TNode n) throw(AssertionException) = 0; + virtual void conflict(TNode n) throw(AssertionException, UnsafeInterruptException) = 0; /** * Propagate a theory literal. @@ -105,7 +106,7 @@ public: * @param n - a theory consequence at the current decision level * @return false if an immediate conflict was encountered */ - virtual bool propagate(TNode n) throw(AssertionException) = 0; + virtual bool propagate(TNode n) throw(AssertionException, UnsafeInterruptException) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has @@ -119,7 +120,7 @@ public: */ virtual LemmaStatus lemma(TNode n, bool removable = false, bool preprocess = false) - throw(TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * Request a split on a new theory atom. This is equivalent to @@ -128,12 +129,12 @@ public: * @param n - a theory atom; must be of Boolean type */ LemmaStatus split(TNode n) - throw(TypeCheckingExceptionPrivate, AssertionException) { + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { return splitLemma(n.orNode(n.notNode())); } virtual LemmaStatus splitLemma(TNode n, bool removable = false) - throw(TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * If a decision is made on n, it must be in the phase specified. @@ -148,7 +149,7 @@ public: * @param phase - the phase to decide on n */ virtual void requirePhase(TNode n, bool phase) - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * Flips the most recent unflipped decision to the other phase and @@ -191,14 +192,14 @@ public: * could be flipped, or if the root decision was re-flipped */ virtual bool flipDecision() - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * Notification from a theory that it realizes it is incomplete at * this context level. If SAT is later determined by the * TheoryEngine, it should actually return an UNKNOWN result. */ - virtual void setIncomplete() throw(AssertionException) = 0; + virtual void setIncomplete() throw(AssertionException, UnsafeInterruptException) = 0; /** * "Spend" a "resource." The meaning is specific to the context in @@ -211,7 +212,7 @@ public: * long-running operations, they cannot rely on resource() to break * out of infinite or intractable computations. */ - virtual void spendResource() throw() {} + virtual void spendResource() throw(UnsafeInterruptException) {} /** * Handle user attribute. @@ -226,7 +227,7 @@ public: * Using this leads to non-termination issues. * It is appropriate for prototyping for theories. */ - virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {} + virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {} };/* class OutputChannel */ diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 960602846..a940bcc3d 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -18,12 +18,16 @@ #include "theory/theory.h" #include "theory/rewriter.h" #include "theory/rewriter_tables.h" +#include "smt/smt_engine_scope.h" +#include "util/resource_manager.h" using namespace std; namespace CVC4 { namespace theory { +unsigned long Rewriter::d_iterationCount = 0; + static TheoryId theoryOf(TNode node) { return Theory::theoryOf(THEORY_OF_TYPE_BASED, node); } @@ -76,7 +80,7 @@ struct RewriteStackElement { } }; -Node Rewriter::rewrite(TNode node) { +Node Rewriter::rewrite(TNode node) throw (UnsafeInterruptException){ return rewriteTo(theoryOf(node), node); } @@ -102,9 +106,20 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { vector rewriteStack; rewriteStack.push_back(RewriteStackElement(node, theoryId)); + ResourceManager* rm = NULL; + bool hasSmtEngine = smt::smtEngineInScope(); + if (hasSmtEngine) { + rm = NodeManager::currentResourceManager(); + } // Rewrite until the stack is empty for (;;){ + if (hasSmtEngine && + d_iterationCount % ResourceManager::getFrequencyCount() == 0) { + rm->spendResource(); + d_iterationCount = 0; + } + // Get the top of the recursion stack RewriteStackElement& rewriteStackTop = rewriteStack.back(); @@ -139,7 +154,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { rewriteStackTop.theoryId = theoryOf(cached); } } - + rewriteStackTop.original =rewriteStackTop.node; // Now it's time to rewrite the children, check if this has already been done Node cached = Rewriter::getPostRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); @@ -233,5 +248,15 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { return Node::null(); }/* Rewriter::rewriteTo() */ +void Rewriter::clearCaches() { +#ifdef CVC4_ASSERTIONS + if(s_rewriteStack != NULL) { + delete s_rewriteStack; + s_rewriteStack = NULL; + } +#endif + Rewriter::clearCachesInternal(); +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index b150b186a..44035e7d9 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -19,6 +19,8 @@ #pragma once #include "expr/node.h" +#include "util/unsafe_interrupt_exception.h" + //#include "expr/attribute.h" namespace CVC4 { @@ -56,7 +58,7 @@ class RewriterInitializer; class Rewriter { friend class RewriterInitializer; - + static unsigned long d_iterationCount; /** Returns the appropriate cache for a node */ static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node); @@ -100,20 +102,19 @@ class Rewriter { * Should be called to clean up any state. */ static void shutdown(); - + static void clearCachesInternal(); public: /** * Rewrites the node using theoryOf() to determine which rewriter to * use on the node. */ - static Node rewrite(TNode node); + static Node rewrite(TNode node) throw (UnsafeInterruptException); /** * Garbage collects the rewrite caches. */ - static void garbageCollect(); - + static void clearCaches(); };/* class Rewriter */ }/* CVC4::theory namespace */ diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index 9b51d2b32..d79f464b5 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -85,7 +85,7 @@ void Rewriter::shutdown() { ${rewrite_shutdown} } -void Rewriter::garbageCollect() { +void Rewriter::clearCachesInternal() { typedef CVC4::expr::attr::AttributeUniqueId AttributeUniqueId; std::vector preids; ${pre_rewrite_attribute_ids} diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 12a169e09..d83626a6b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -26,6 +26,7 @@ #include "expr/node_builder.h" #include "options/options.h" #include "util/lemma_output_channel.h" +#include "util/resource_manager.h" #include "theory/theory.h" #include "theory/theory_engine.h" @@ -142,6 +143,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_true(), d_false(), d_interrupted(false), + d_resourceManager(NodeManager::currentResourceManager()), d_inPreregister(false), d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), @@ -334,8 +336,7 @@ void TheoryEngine::dumpAssertions(const char* tag) { * @param effort the effort level to use */ void TheoryEngine::check(Theory::Effort effort) { - - d_propEngine->checkTime(); + // spendResource(); // Reset the interrupt flag d_interrupted = false; @@ -846,6 +847,7 @@ struct preprocess_stack_element { Node TheoryEngine::preprocess(TNode assertion) { Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion << ")" << endl; + // spendResource(); // Do a topological sort of the subexpressions and substitute them vector toVisit; @@ -1082,7 +1084,7 @@ void TheoryEngine::assertFact(TNode literal) { Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl; - d_propEngine->checkTime(); + // spendResource(); // If we're in conflict, nothing to do if (d_inConflict) { @@ -1145,7 +1147,7 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl; - d_propEngine->checkTime(); + // spendResource(); if(Dump.isOn("t-propagations")) { Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") @@ -1368,7 +1370,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector& atoms, theory::The theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) { // For resource-limiting (also does a time check). - spendResource(); + // spendResource(); // Do we need to check atoms if (atomsTo != theory::THEORY_LAST) { @@ -1553,7 +1555,7 @@ bool TheoryEngine::donePPSimpITE(std::vector& assertions){ Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl; Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl; d_iteUtilities->clear(); - Rewriter::garbageCollect(); + Rewriter::clearCaches(); d_iteRemover.garbageCollect(); nm->reclaimZombiesUntil(options::zombieHuntThreshold()); Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl; @@ -1742,3 +1744,7 @@ std::pair TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T return th->entailmentCheck(lit, params, seffects); } + +void TheoryEngine::spendResource() { + d_resourceManager->spendResource(); +} diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 136c0409f..6360ea5fb 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -39,6 +39,7 @@ #include "util/statistics_registry.h" #include "util/cvc4_assert.h" #include "util/sort_inference.h" +#include "util/unsafe_interrupt_exception.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/uf/equality_engine.h" #include "theory/bv/bv_to_bool.h" @@ -46,6 +47,8 @@ namespace CVC4 { +class ResourceManager; + /** * A pair of a theory and a node. This is used to mark the flow of * propagations between theories. @@ -279,42 +282,42 @@ class TheoryEngine { { } - void safePoint() throw(theory::Interrupted, AssertionException) { + void safePoint() throw(theory::Interrupted, UnsafeInterruptException, AssertionException) { spendResource(); if (d_engine->d_interrupted) { throw theory::Interrupted(); } } - void conflict(TNode conflictNode) throw(AssertionException) { + void conflict(TNode conflictNode) throw(AssertionException, UnsafeInterruptException) { Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; ++ d_statistics.conflicts; d_engine->d_outputChannelUsed = true; d_engine->conflict(conflictNode, d_theory); } - bool propagate(TNode literal) throw(AssertionException) { + bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException) { Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; ++ d_statistics.propagations; d_engine->d_outputChannelUsed = true; return d_engine->propagate(literal, d_theory); } - theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException) { + theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; return d_engine->lemma(lemma, false, removable, preprocess, theory::THEORY_LAST); } - theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { + theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; return d_engine->lemma(lemma, false, removable, false, d_theory); } - void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) { + void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { NodeManager* curr = NodeManager::currentNM(); Node restartVar = curr->mkSkolem("restartVar", curr->booleanType(), @@ -325,7 +328,7 @@ class TheoryEngine { } void requirePhase(TNode n, bool phase) - throw(theory::Interrupted, AssertionException) { + throw(theory::Interrupted, AssertionException, UnsafeInterruptException) { Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase << ")" << std::endl; ++ d_statistics.requirePhase; @@ -333,18 +336,18 @@ class TheoryEngine { } bool flipDecision() - throw(theory::Interrupted, AssertionException) { + throw(theory::Interrupted, AssertionException, UnsafeInterruptException) { Debug("theory") << "EngineOutputChannel::flipDecision()" << std::endl; ++ d_statistics.flipDecision; return d_engine->d_propEngine->flipDecision(); } - void setIncomplete() throw(AssertionException) { + void setIncomplete() throw(AssertionException, UnsafeInterruptException) { Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl; d_engine->setIncomplete(d_theory); } - void spendResource() throw() { + void spendResource() throw(UnsafeInterruptException) { d_engine->spendResource(); } @@ -387,12 +390,6 @@ class TheoryEngine { d_incomplete = true; } - /** - * "Spend" a resource during a search or preprocessing. - */ - void spendResource() throw() { - d_propEngine->spendResource(); - } /** * Mapping of propagations from recievers to senders. @@ -477,6 +474,7 @@ class TheoryEngine { /** Whether we were just interrupted (or not) */ bool d_interrupted; + ResourceManager* d_resourceManager; public: @@ -487,6 +485,10 @@ public: ~TheoryEngine(); void interrupt() throw(ModalException); + /** + * "Spend" a resource during a search or preprocessing. + */ + void spendResource(); /** * Adds a theory. Only one theory per TheoryId can be present, so if diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 6d1275c20..46a717cc5 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -23,13 +23,13 @@ #include "expr/node.h" #include "theory/output_channel.h" #include "theory/interrupted.h" +#include "util/unsafe_interrupt_exception.h" #include #include #include namespace CVC4 { - namespace theory { /** @@ -72,42 +72,44 @@ public: void safePoint() throw(Interrupted, AssertionException) {} void conflict(TNode n) - throw(AssertionException) { + throw(AssertionException, UnsafeInterruptException) { push(CONFLICT, n); } bool propagate(TNode n) - throw(AssertionException) { + throw(AssertionException, UnsafeInterruptException) { push(PROPAGATE, n); return true; } void propagateAsDecision(TNode n) - throw(AssertionException) { + throw(AssertionException, UnsafeInterruptException) { push(PROPAGATE_AS_DECISION, n); } - LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException) { + LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException, UnsafeInterruptException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } - void requirePhase(TNode, bool) throw(Interrupted, AssertionException) { + void requirePhase(TNode, bool) throw(Interrupted, AssertionException, UnsafeInterruptException) { } - bool flipDecision() throw(Interrupted, AssertionException) { + bool flipDecision() throw(Interrupted, AssertionException, UnsafeInterruptException) { return true; } - void setIncomplete() throw(AssertionException) {} + void setIncomplete() throw(AssertionException, UnsafeInterruptException) { + } - void handleUserAttribute( const char* attr, theory::Theory* t ){} + void handleUserAttribute( const char* attr, theory::Theory* t ) { + } void clear() { d_callHistory.clear(); } - LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException){ + LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } @@ -125,7 +127,7 @@ public: return d_callHistory.size(); } - void printIth(std::ostream& os, int i){ + void printIth(std::ostream& os, int i) { os << "[TestOutputChannel " << i; os << " " << getIthCallType(i); os << " " << getIthNode(i) << "]"; diff --git a/src/util/Makefile.am b/src/util/Makefile.am index fc9192dd9..a6543391d 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -99,7 +99,10 @@ libutil_la_SOURCES = \ didyoumean.h \ didyoumean.cpp \ unsat_core.h \ - unsat_core.cpp + unsat_core.cpp \ + resource_manager.h \ + resource_manager.cpp \ + unsafe_interrupt_exception.h libstatistics_la_SOURCES = \ statistics_registry.h \ @@ -158,6 +161,7 @@ EXTRA_DIST = \ uninterpreted_constant.i \ chain.i \ regexp.i \ + resource_manager.i \ proof.i \ unsat_core.i diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp new file mode 100644 index 000000000..2aca55616 --- /dev/null +++ b/src/util/resource_manager.cpp @@ -0,0 +1,285 @@ +/********************* */ +/*! \file resource_manager.h +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** Minor contributors (to current version): none +** This file is part of the CVC4 project. +** Copyright (c) 2009-2014 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief Manages and updates various resource and time limits. +** +** Manages and updates various resource and time limits. +**/ + +#include "util/resource_manager.h" +#include "util/output.h" +#include "smt/smt_engine_scope.h" +#include "smt/options.h" +#include "theory/rewriter.h" + +using namespace CVC4; +using namespace std; + +void Timer::set(unsigned long millis, bool wallTime) { + d_ms = millis; + Trace("limit") << "Timer::set(" << d_ms << ")" << std::endl; + // keep track of when it was set, even if it's disabled (i.e. == 0) + d_wall_time = wallTime; + if (d_wall_time) { + // Wall time + gettimeofday(&d_wall_limit, NULL); + Trace("limit") << "Timer::set(): it's " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; + d_wall_limit.tv_sec += millis / 1000; + d_wall_limit.tv_usec += (millis % 1000) * 1000; + if(d_wall_limit.tv_usec > 1000000) { + ++d_wall_limit.tv_sec; + d_wall_limit.tv_usec -= 1000000; + } + Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; + } else { + // CPU time + d_cpu_start_time = ((double)clock())/(CLOCKS_PER_SEC *0.001); + d_cpu_limit = d_cpu_start_time + d_ms; + } +} + +/** Return the milliseconds elapsed since last set(). */ +unsigned long Timer::elapsedWall() const { + Assert (d_wall_time); + timeval tv; + gettimeofday(&tv, NULL); + Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl; + tv.tv_sec -= d_wall_limit.tv_sec - d_ms / 1000; + tv.tv_usec -= d_wall_limit.tv_usec - (d_ms % 1000) * 1000; + Trace("limit") << "Timer::elapsedWallTime(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl; + return tv.tv_sec * 1000 + tv.tv_usec / 1000; +} + +unsigned long Timer::elapsedCPU() const { + Assert (!d_wall_time); + clock_t elapsed = ((double)clock())/(CLOCKS_PER_SEC *0.001)- d_cpu_start_time; + Trace("limit") << "Timer::elapsedCPUTime(): elapsed time is " << elapsed << " ms" <= d_cpu_limit) { + Debug("limit") << "Timer::expired(): OVER LIMIT!" << current << std::endl; + return true; + } + return false; +} + +const unsigned long ResourceManager::s_resourceCount = 1000; + +ResourceManager::ResourceManager() + : d_cumulativeTimer() + , d_perCallTimer() + , d_timeBudgetCumulative(0) + , d_timeBudgetPerCall(0) + , d_resourceBudgetCumulative(0) + , d_resourceBudgetPerCall(0) + , d_cumulativeTimeUsed(0) + , d_cumulativeResourceUsed(0) + , d_thisCallResourceUsed(0) + , d_thisCallTimeBudget(0) + , d_thisCallResourceBudget(0) + , d_isHardLimit() + , d_on(false) + , d_cpuTime(false) + , d_spendResourceCalls(0) +{} + + +void ResourceManager::setResourceLimit(unsigned long units, bool cumulative) { + d_on = true; + if(cumulative) { + Trace("limit") << "ResourceManager: setting cumulative resource limit to " << units << endl; + d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units); + d_thisCallResourceBudget = d_resourceBudgetCumulative; + } else { + Trace("limit") << "ResourceManager: setting per-call resource limit to " << units << endl; + d_resourceBudgetPerCall = units; + } +} + +void ResourceManager::setTimeLimit(unsigned long millis, bool cumulative) { + d_on = true; + if(cumulative) { + Trace("limit") << "ResourceManager: setting cumulative time limit to " << millis << " ms" << endl; + d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis); + d_cumulativeTimer.set(millis, !d_cpuTime); + } else { + Trace("limit") << "ResourceManager: setting per-call time limit to " << millis << " ms" << endl; + d_timeBudgetPerCall = millis; + // perCall timer will be set in beginCall + } + +} + +unsigned long ResourceManager::getResourceUsage() const { + return d_cumulativeResourceUsed; +} + +unsigned long ResourceManager::getTimeUsage() const { + if (d_timeBudgetCumulative) { + return d_cumulativeTimer.elapsed(); + } + return d_cumulativeTimeUsed; +} + +unsigned long ResourceManager::getResourceRemaining() const { + if (d_thisCallResourceBudget <= d_thisCallResourceUsed) + return 0; + return d_thisCallResourceBudget - d_thisCallResourceUsed; +} + +unsigned long ResourceManager::getTimeRemaining() const { + unsigned long time_passed = d_cumulativeTimer.elapsed(); + if (time_passed >= d_thisCallTimeBudget) + return 0; + return d_thisCallTimeBudget - time_passed; +} + +void ResourceManager::spendResource() throw (UnsafeInterruptException) { + ++d_spendResourceCalls; + if (!d_on) return; + + Debug("limit") << "ResourceManager::spendResource()" << std::endl; + ++d_cumulativeResourceUsed; + ++d_thisCallResourceUsed; + if(out()) { + Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl; + Trace("limit") << " on call " << d_spendResourceCalls << std::endl; + if (outOfTime()) { + Trace("limit") << "ResourceManager::spendResource: elapsed time" << d_cumulativeTimer.elapsed() << std::endl; + } + + if (smt::smtEngineInScope()) { + theory::Rewriter::clearCaches(); + } + if (d_isHardLimit) { + throw UnsafeInterruptException(); + } + + // interrupt it next time resources are checked + if (smt::smtEngineInScope()) { + smt::currentSmtEngine()->interrupt(); + } + } +} + +void ResourceManager::beginCall() { + + d_perCallTimer.set(d_timeBudgetPerCall, !d_cpuTime); + d_thisCallResourceUsed = 0; + if (!d_on) return; + + if (cumulativeLimitOn()) { + if (d_resourceBudgetCumulative) { + d_thisCallResourceBudget = d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 : + d_resourceBudgetCumulative - d_cumulativeResourceUsed; + } + + if (d_timeBudgetCumulative) { + + AlwaysAssert(d_cumulativeTimer.on()); + // timer was on since the option was set + d_cumulativeTimeUsed = d_cumulativeTimer.elapsed(); + d_thisCallTimeBudget = d_timeBudgetCumulative <= d_cumulativeTimeUsed? 0 : + d_timeBudgetCumulative - d_cumulativeTimeUsed; + d_cumulativeTimer.set(d_thisCallTimeBudget, d_cpuTime); + } + // we are out of resources so we shouldn't update the + // budget for this call to the per call budget + if (d_thisCallTimeBudget == 0 || + d_thisCallResourceUsed == 0) + return; + } + + if (perCallLimitOn()) { + // take min of what's left and per-call budget + if (d_resourceBudgetPerCall) { + d_thisCallResourceBudget = d_thisCallResourceBudget < d_resourceBudgetPerCall && d_thisCallResourceBudget != 0 ? d_thisCallResourceBudget : d_resourceBudgetPerCall; + } + + if (d_timeBudgetPerCall) { + d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall && d_thisCallTimeBudget != 0 ? d_thisCallTimeBudget : d_timeBudgetPerCall; + } + } +} + +void ResourceManager::endCall() { + unsigned long usedInCall = d_perCallTimer.elapsed(); + d_perCallTimer.set(0); + d_cumulativeTimeUsed += usedInCall; +} + +bool ResourceManager::cumulativeLimitOn() const { + return d_timeBudgetCumulative || d_resourceBudgetCumulative; +} + +bool ResourceManager::perCallLimitOn() const { + return d_timeBudgetPerCall || d_resourceBudgetPerCall; +} + +bool ResourceManager::outOfResources() const { + // resource limiting not enabled + if (d_resourceBudgetPerCall == 0 && + d_resourceBudgetCumulative == 0) + return false; + + return getResourceRemaining() == 0; +} + +bool ResourceManager::outOfTime() const { + if (d_timeBudgetPerCall == 0 && + d_timeBudgetCumulative == 0) + return false; + + return d_cumulativeTimer.expired() || d_perCallTimer.expired(); +} + +void ResourceManager::useCPUTime(bool cpu) { + Trace("limit") << "ResourceManager::useCPUTime("<< cpu <<")\n"; + d_cpuTime = cpu; +} + +void ResourceManager::setHardLimit(bool value) { + Trace("limit") << "ResourceManager::setHardLimit("<< value <<")\n"; + d_isHardLimit = value; +} + +void ResourceManager::enable(bool on) { + Trace("limit") << "ResourceManager::enable("<< on <<")\n"; + d_on = on; +} diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h new file mode 100644 index 000000000..a16f60910 --- /dev/null +++ b/src/util/resource_manager.h @@ -0,0 +1,158 @@ +/********************* */ +/*! \file resource_manager.h +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** Minor contributors (to current version): none +** This file is part of the CVC4 project. +** Copyright (c) 2009-2014 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief Manages and updates various resource and time limits +** +** Manages and updates various resource and time limits. +**/ + +#include "cvc4_public.h" + +#ifndef __CVC4__RESOURCE_MANAGER_H +#define __CVC4__RESOURCE_MANAGER_H + +#include +#include + +#include "util/exception.h" +#include "util/unsafe_interrupt_exception.h" + +namespace CVC4 { + +/** + * A helper class to keep track of a time budget and signal + * the PropEngine when the budget expires. + */ +class CVC4_PUBLIC Timer { + + unsigned long d_ms; + timeval d_wall_limit; + clock_t d_cpu_start_time; + clock_t d_cpu_limit; + + bool d_wall_time; + + /** Return the milliseconds elapsed since last set() cpu time. */ + unsigned long elapsedCPU() const; + /** Return the milliseconds elapsed since last set() wall time. */ + unsigned long elapsedWall() const; + +public: + + /** Construct a Timer. */ + Timer() + : d_ms(0) + , d_cpu_start_time(0) + , d_cpu_limit(0) + , d_wall_time(true) + {} + + /** Is the timer currently active? */ + bool on() const { + return d_ms != 0; + } + + /** Set a millisecond timer (0==off). */ + void set(unsigned long millis, bool wall_time = true); + /** Return the milliseconds elapsed since last set() wall/cpu time + depending on d_wall_time*/ + unsigned long elapsed() const; + bool expired() const; + +};/* class Timer */ + + +class CVC4_PUBLIC ResourceManager { + + Timer d_cumulativeTimer; + Timer d_perCallTimer; + + /** 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. */ + unsigned long d_cumulativeTimeUsed; + /** The amount of resource used. */ + unsigned long d_cumulativeResourceUsed; + + /** The ammount of resource used during this call. */ + unsigned long d_thisCallResourceUsed; + + /** + * The ammount of resource budget for this call (min between per call + * budget and left-over cumulative budget. + */ + unsigned long d_thisCallTimeBudget; + unsigned long d_thisCallResourceBudget; + + bool d_isHardLimit; + bool d_on; + bool d_cpuTime; + unsigned long d_spendResourceCalls; + + /** Counter indicating how often to check resource manager in loops */ + static const unsigned long s_resourceCount; + +public: + + ResourceManager(); + + bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); } + bool cumulativeLimitOn() const; + bool perCallLimitOn() const; + + bool outOfResources() const; + bool outOfTime() const; + bool out() const { return d_on && (outOfResources() || outOfTime()); } + + unsigned long getResourceUsage() const; + unsigned long getTimeUsage() const; + unsigned long getResourceRemaining() const; + unsigned long getTimeRemaining() const; + + unsigned long getResourceBudgetForThisCall() { + return d_thisCallResourceBudget; + } + + void spendResource() throw(UnsafeInterruptException); + + void setHardLimit(bool value); + void setResourceLimit(unsigned long units, bool cumulative = false); + void setTimeLimit(unsigned long millis, bool cumulative = false); + void useCPUTime(bool cpu); + + void enable(bool on); + + /** + * Resets perCall limits to mark the start of a new call, + * updates budget for current call and starts the timer + */ + void beginCall(); + + /** + * Marks the end of a SmtEngine check call, stops the per + * call timer, updates cumulative time used. + */ + void endCall(); + + static unsigned long getFrequencyCount() { return s_resourceCount; } + +};/* class ResourceManager */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__RESOURCE_MANAGER_H */ diff --git a/src/util/resource_manager.i b/src/util/resource_manager.i new file mode 100644 index 000000000..0f55c2bce --- /dev/null +++ b/src/util/resource_manager.i @@ -0,0 +1,5 @@ +%{ +#include "util/resource_manager.h" +%} + +%include "util/resource_manager.h" diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h new file mode 100644 index 000000000..e19fc37ce --- /dev/null +++ b/src/util/unsafe_interrupt_exception.h @@ -0,0 +1,43 @@ +/********************* */ +/*! \file modal_exception.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An exception that is thrown when the solver is out of time/resources + ** and is interrupted in an unsafe state + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H +#define __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H + +#include "util/exception.h" + +namespace CVC4 { + +class CVC4_PUBLIC UnsafeInterruptException : public CVC4::Exception { +public: + UnsafeInterruptException() : + Exception("Interrupted in unsafe state due to " + "time/resource limit.") { + } + + UnsafeInterruptException(const std::string& msg) : + Exception(msg) { + } + + UnsafeInterruptException(const char* msg) : + Exception(msg) { + } +};/* class UnsafeInterruptException */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */ diff --git a/src/util/unsafe_interrupt_exception.i b/src/util/unsafe_interrupt_exception.i new file mode 100644 index 000000000..94a552877 --- /dev/null +++ b/src/util/unsafe_interrupt_exception.i @@ -0,0 +1,7 @@ +%{ +#include "util/unsafe_interrupt_exception.h" +%} + +%ignore CVC4::UnsafeInterruptException::UnsafeInterruptException(const char*); + +%include "util/unsafe_interrupt_exception.h" diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index eed173366..8fddf7394 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -53,21 +53,21 @@ public: TheoryBVWhite() {} - void setUp() { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); d_smt->setOption("bitblast", SExpr("eager")); - d_bb = new EagerBitblaster(NULL); - + d_bb = new EagerBitblaster(dynamic_cast(d_smt->d_theoryEngine->d_theoryTable[THEORY_BV])); } + void tearDown() { - // delete d_bb; + delete d_bb; + delete d_scope; + delete d_smt; delete d_em; } - void testBitblasterCore() { Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16)); @@ -84,5 +84,4 @@ public: bool res = d_bb->solve(); TS_ASSERT (res == false); } - -}; +};/* class TheoryBVWhite */