summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/Makefile.am2
-rw-r--r--src/smt/smt_engine.cpp68
-rw-r--r--src/smt/smt_engine.h4
-rw-r--r--src/smt/smt_engine_scope.cpp10
-rw-r--r--src/smt/smt_engine_scope.h40
5 files changed, 89 insertions, 35 deletions
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 3e777ec89..5cc0cedd1 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -8,6 +8,8 @@ noinst_LTLIBRARIES = libsmt.la
libsmt_la_SOURCES = \
smt_engine.cpp \
smt_engine.h \
+ smt_engine_scope.cpp \
+ smt_engine_scope.h \
modal_exception.h \
bad_option_exception.h \
no_such_function_exception.h
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4cccb8d10..01ce73be1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -38,6 +38,7 @@
#include "smt/modal_exception.h"
#include "smt/no_such_function_exception.h"
#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/theory_engine.h"
#include "proof/proof_manager.h"
#include "util/proof.h"
@@ -48,16 +49,9 @@
#include "util/output.h"
#include "util/hash.h"
#include "theory/substitutions.h"
-#include "theory/builtin/theory_builtin.h"
-#include "theory/booleans/theory_bool.h"
-#include "theory/booleans/circuit_propagator.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/bv/theory_bv.h"
-#include "theory/datatypes/theory_datatypes.h"
#include "theory/theory_traits.h"
#include "theory/logic_info.h"
+#include "theory/booleans/circuit_propagator.h"
#include "util/ite_removal.h"
#include "theory/model.h"
@@ -265,6 +259,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
d_cumulativeResourceUsed(0),
d_status(),
d_private(new smt::SmtEnginePrivate(*this)),
+ d_statisticsRegistry(new StatisticsRegistry()),
d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
@@ -277,7 +272,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
StatisticsRegistry::registerStat(&d_definitionExpansionTime);
StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
@@ -382,7 +377,7 @@ void SmtEngine::shutdown() {
}
SmtEngine::~SmtEngine() throw() {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
try {
while(Options::current()->incrementalSolving && d_userContext->getLevel() > 1) {
@@ -424,6 +419,9 @@ SmtEngine::~SmtEngine() throw() {
delete d_theoryEngine;
delete d_propEngine;
//delete d_decisionEngine;
+
+ delete d_statisticsRegistry;
+
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << endl
<< e << endl;
@@ -431,7 +429,7 @@ SmtEngine::~SmtEngine() throw() {
}
void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
if(Dump.isOn("benchmark")) {
Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
@@ -442,7 +440,7 @@ void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
}
void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
setLogic(LogicInfo(s));
}
@@ -605,7 +603,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
void SmtEngine::setInfo(const std::string& key, const SExpr& value)
throw(BadOptionException, ModalException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
if(Dump.isOn("benchmark")) {
@@ -629,7 +627,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
if(! value.isAtom()) {
throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string");
}
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
d_logic = value.getValue();
setLogicInternal();
return;
@@ -664,7 +662,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
SExpr SmtEngine::getInfo(const std::string& key) const
throw(BadOptionException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT getInfo(" << key << ")" << endl;
if(key == ":all-statistics") {
@@ -705,7 +703,7 @@ SExpr SmtEngine::getInfo(const std::string& key) const
void SmtEngine::setOption(const std::string& key, const SExpr& value)
throw(BadOptionException, ModalException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
if(Dump.isOn("benchmark")) {
@@ -757,7 +755,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
SExpr SmtEngine::getOption(const std::string& key) const
throw(BadOptionException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT getOption(" << key << ")" << endl;
if(Dump.isOn("benchmark")) {
@@ -804,7 +802,7 @@ void SmtEngine::defineFunction(Expr func,
<< func;
Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula);
}
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
// type check body
Type formulaType = formula.getType(Options::current()->typeChecking);
@@ -1606,7 +1604,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
Assert(e.isNull() || e.getExprManager() == d_exprManager);
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
@@ -1669,7 +1667,7 @@ Result SmtEngine::query(const BoolExpr& e) {
Assert(!e.isNull());
Assert(e.getExprManager() == d_exprManager);
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
@@ -1725,7 +1723,7 @@ Result SmtEngine::query(const BoolExpr& e) {
Result SmtEngine::assertFormula(const BoolExpr& e) {
Assert(e.getExprManager() == d_exprManager);
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl;
ensureBoolean(e);
@@ -1738,7 +1736,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
Expr SmtEngine::simplify(const Expr& e) {
Assert(e.getExprManager() == d_exprManager);
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
if( Options::current()->typeChecking ) {
e.getType(true);// ensure expr is type-checked at this point
@@ -1753,7 +1751,7 @@ Expr SmtEngine::simplify(const Expr& e) {
Expr SmtEngine::getValue(const Expr& e)
throw(ModalException, AssertionException) {
Assert(e.getExprManager() == d_exprManager);
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
// ensure expr is type-checked at this point
Type type = e.getType(Options::current()->typeChecking);
@@ -1799,7 +1797,7 @@ Expr SmtEngine::getValue(const Expr& e)
}
bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
Type type = e.getType(Options::current()->typeChecking);
// must be Boolean
@@ -1828,7 +1826,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
Trace("smt") << "SMT getAssignment()" << endl;
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetAssignmentCommand();
@@ -1890,7 +1888,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
void SmtEngine::addToModelType( Type& t ){
Trace("smt") << "SMT addToModelType(" << t << ")" << endl;
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
if( Options::current()->produceModels ) {
d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) );
}
@@ -1898,7 +1896,7 @@ void SmtEngine::addToModelType( Type& t ){
void SmtEngine::addToModelFunction( Expr& e ){
Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl;
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
if( Options::current()->produceModels ) {
d_theoryEngine->getModel()->addDefineFunction( e.getNode() );
}
@@ -1907,7 +1905,7 @@ void SmtEngine::addToModelFunction( Expr& e ){
Model* SmtEngine::getModel() throw(ModalException, AssertionException){
Trace("smt") << "SMT getModel()" << endl;
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
if(!Options::current()->produceModels) {
const char* msg =
@@ -1928,7 +1926,7 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){
Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
Trace("smt") << "SMT getProof()" << endl;
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetProofCommand();
@@ -1958,7 +1956,7 @@ vector<Expr> SmtEngine::getAssertions()
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetAssertionsCommand();
}
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT getAssertions()" << endl;
if(!Options::current()->interactive) {
const char* msg =
@@ -1970,13 +1968,13 @@ vector<Expr> SmtEngine::getAssertions()
}
size_t SmtEngine::getStackLevel() const {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT getStackLevel()" << endl;
return d_context->getLevel();
}
void SmtEngine::push() {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
Trace("smt") << "SMT push()" << endl;
d_private->processAssertions();
@@ -2000,7 +1998,7 @@ void SmtEngine::push() {
}
void SmtEngine::pop() {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
Trace("smt") << "SMT pop()" << endl;
if(Dump.isOn("benchmark")) {
@@ -2108,11 +2106,11 @@ unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) {
}
StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
- return d_exprManager->d_nodeManager->getStatisticsRegistry();
+ return d_statisticsRegistry;
}
void SmtEngine::printModel( std::ostream& out, Model* m ){
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
m->toStream(out);
}
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index aef98d75b..4df9054a7 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -76,6 +76,7 @@ namespace smt {
class DefinedFunction;
class SmtEnginePrivate;
+ class SmtScope;
}/* CVC4::smt namespace */
// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
@@ -248,6 +249,9 @@ class CVC4_PUBLIC SmtEngine {
void setLogicInternal() throw(AssertionException);
friend class ::CVC4::smt::SmtEnginePrivate;
+ friend class ::CVC4::smt::SmtScope;
+
+ StatisticsRegistry* d_statisticsRegistry;
// === STATISTICS ===
/** time spent in definition-expansion */
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
new file mode 100644
index 000000000..03298e99a
--- /dev/null
+++ b/src/smt/smt_engine_scope.cpp
@@ -0,0 +1,10 @@
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+
+namespace CVC4 {
+namespace smt {
+
+CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current = NULL;
+
+}
+}
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
new file mode 100644
index 000000000..bcdaefd9f
--- /dev/null
+++ b/src/smt/smt_engine_scope.h
@@ -0,0 +1,40 @@
+#include "smt/smt_engine.h"
+#include "util/tls.h"
+#include "util/Assert.h"
+#include "expr/node_manager.h"
+#include "util/output.h"
+
+#pragma once
+
+namespace CVC4 {
+namespace smt {
+
+extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
+
+inline SmtEngine* currentSmtEngine() {
+ Assert(s_smtEngine_current != NULL);
+ return s_smtEngine_current;
+}
+
+class SmtScope : public NodeManagerScope {
+ /** The old NodeManager, to be restored on destruction. */
+ SmtEngine* d_oldSmtEngine;
+
+public:
+
+ SmtScope(const SmtEngine* smt) :
+ NodeManagerScope(smt->d_nodeManager),
+ d_oldSmtEngine(s_smtEngine_current) {
+ Assert(smt != NULL);
+ s_smtEngine_current = const_cast<SmtEngine*>(smt);
+ Debug("current") << "smt scope: " << s_smtEngine_current << std::endl;
+ }
+
+ ~SmtScope() {
+ s_smtEngine_current = d_oldSmtEngine;
+ Debug("current") << "smt scope: returning to " << s_smtEngine_current << std::endl;
+ }
+};/* class SmtScope */
+
+}
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback