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/node_manager.cpp | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 22 |
1 files changed, 22 insertions, 0 deletions
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; |