diff options
author | Liana Hadarean <lianah@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
commit | 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 (patch) | |
tree | 845ae47600ffff9c68fa654c0f78d3474e406beb /src/expr | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 21 | ||||
-rw-r--r-- | src/expr/command.h | 12 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 6 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 22 | ||||
-rw-r--r-- | src/expr/node_manager.h | 7 |
6 files changed, 71 insertions, 1 deletions
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<const CommandFailure*>(d_commandStatus) != NULL; } +bool Command::interrupted() const throw() { + return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(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<CommandSuccess&>(*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<CommandInterrupted&>(*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; |