summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/command.cpp21
-rw-r--r--src/expr/command.h12
-rw-r--r--src/expr/expr_manager_template.cpp4
-rw-r--r--src/expr/expr_manager_template.h6
-rw-r--r--src/expr/node_manager.cpp22
-rw-r--r--src/expr/node_manager.h7
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback