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/command_list.cpp33
-rw-r--r--src/smt/command_list.h41
-rw-r--r--src/smt/options_handlers.h11
-rw-r--r--src/smt/smt_engine.cpp103
-rw-r--r--src/smt/smt_engine.h27
6 files changed, 187 insertions, 30 deletions
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 333c887ee..8aa3e1630 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -10,6 +10,8 @@ libsmt_la_SOURCES = \
smt_engine.h \
smt_engine_scope.cpp \
smt_engine_scope.h \
+ command_list.cpp \
+ command_list.h \
modal_exception.h \
simplification_mode.h \
simplification_mode.cpp \
diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp
new file mode 100644
index 000000000..7fb6cf013
--- /dev/null
+++ b/src/smt/command_list.cpp
@@ -0,0 +1,33 @@
+/********************* */
+/*! \file command_list.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A context-sensitive list of Commands, and their cleanup
+ **
+ ** A context-sensitive list of Commands, and their cleanup.
+ **/
+
+// we include both of these to make sure they agree on the typedef
+#include "smt/command_list.h"
+#include "smt/smt_engine.h"
+
+#include "expr/command.h"
+
+namespace CVC4 {
+namespace smt {
+
+void CommandCleanup::operator()(Command** c) {
+ delete *c;
+}
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
diff --git a/src/smt/command_list.h b/src/smt/command_list.h
new file mode 100644
index 000000000..954ef9629
--- /dev/null
+++ b/src/smt/command_list.h
@@ -0,0 +1,41 @@
+/********************* */
+/*! \file command_list.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A context-sensitive list of Commands, and their cleanup
+ **
+ ** A context-sensitive list of Commands, and their cleanup.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__SMT__COMMAND_LIST_H
+#define __CVC4__SMT__COMMAND_LIST_H
+
+#include "context/cdlist.h"
+
+namespace CVC4 {
+
+class Command;
+
+namespace smt {
+
+struct CommandCleanup {
+ void operator()(Command** c);
+};/* struct CommandCleanup */
+
+typedef context::CDList<Command*, CommandCleanup> CommandList;
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__COMMAND_LIST_H */
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 2c20e06bb..4f214ddd1 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -73,7 +73,7 @@ benchmark\n\
modes.\n\
\n\
declarations\n\
-+ Dump declarations. Implied by all following modes.\n\
++ Dump user declarations. Implied by all following modes.\n\
\n\
assertions\n\
+ Output the assertions after non-clausal simplification and static\n\
@@ -82,6 +82,11 @@ assertions\n\
(--simplification=none --no-static-learning), the output\n\
will closely resemble the input (with term-level ITEs removed).\n\
\n\
+skolems\n\
++ Dump internally-created skolem variable declarations. These can\n\
+ arise from preprocessing simplifications, existential elimination,\n\
+ and a number of other things. Implied by all following modes.\n\
+\n\
learned\n\
+ Output the assertions after non-clausal simplification, static\n\
learning, and presolve-time T-lemmas. This should include all eager\n\
@@ -172,6 +177,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
if(!strcmp(optargPtr, "benchmark")) {
} else if(!strcmp(optargPtr, "declarations")) {
} else if(!strcmp(optargPtr, "assertions")) {
+ } else if(!strcmp(optargPtr, "skolems")) {
} else if(!strcmp(optargPtr, "learned")) {
} else if(!strcmp(optargPtr, "clauses")) {
} else if(!strcmp(optargPtr, "t-conflicts") ||
@@ -219,6 +225,9 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
Dump.on("benchmark");
if(strcmp(optargPtr, "benchmark")) {
Dump.on("declarations");
+ if(strcmp(optargPtr, "declarations") && strcmp(optargPtr, "assertions")) {
+ Dump.on("skolems");
+ }
}
}
free(optargPtr);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 55ea09de4..e28520e70 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -47,6 +47,7 @@
#include "util/boolean_simplification.h"
#include "util/configuration.h"
#include "util/exception.h"
+#include "smt/command_list.h"
#include "smt/options.h"
#include "options/option_exception.h"
#include "util/output.h"
@@ -110,7 +111,7 @@ public:
* one) becomes an "interface shell" which simply acts as a forwarder
* of method calls.
*/
-class SmtEnginePrivate {
+class SmtEnginePrivate : public NodeManagerListener {
SmtEngine& d_smt;
/** The assertions yet to be preprocessed */
@@ -198,6 +199,51 @@ public:
d_propagator(d_nonClausalLearnedLiterals, true, true),
d_topLevelSubstitutions(smt.d_userContext),
d_lastSubstitutionPos(smt.d_userContext, d_topLevelSubstitutions.end()) {
+ d_smt.d_nodeManager->subscribeEvents(this);
+ }
+
+ void nmNotifyNewSort(TypeNode tn) {
+ DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
+ 0,
+ tn.toType());
+ Dump("declarations") << c;
+ d_smt.addToModelCommand(c.clone());
+ }
+
+ void nmNotifyNewSortConstructor(TypeNode tn) {
+ DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
+ tn.getAttribute(expr::SortArityAttr()),
+ tn.toType());
+ Dump("declarations") << c;
+ d_smt.addToModelCommand(c.clone());
+ }
+
+ void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) {
+ DatatypeDeclarationCommand c(dtts);
+ Dump("declarations") << c;
+ d_smt.addToModelCommand(c.clone());
+ }
+
+ void nmNotifyNewVar(TNode n) {
+ DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()),
+ n.toExpr(),
+ n.getType().toType());
+ Dump("declarations") << c;
+ d_smt.addToModelCommand(c.clone());
+ }
+
+ void nmNotifyNewSkolem(TNode n, std::string comment) {
+ std::string id = n.getAttribute(expr::VarNameAttr());
+ DeclareFunctionCommand c(id,
+ n.toExpr(),
+ n.getType().toType());
+ if(Dump.isOn("skolems")) {
+ if(comment != "") {
+ Dump("skolems") << CommentCommand(id + " is " + comment);
+ }
+ Dump("skolems") << c;
+ }
+ d_smt.addToModelCommand(c.clone());
}
Node applySubstitutions(TNode node) const {
@@ -254,6 +300,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
d_definedFunctions(NULL),
d_assertionList(NULL),
d_assignments(NULL),
+ d_modelCommands(NULL),
d_logic(),
d_pendingPops(0),
d_fullyInited(false),
@@ -316,6 +363,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
d_context->push();
d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
+ d_modelCommands = new(true) smt::CommandList(d_userContext);
}
void SmtEngine::finishInit() {
@@ -388,33 +436,33 @@ void SmtEngine::finalOptionsAreSet() {
}
void SmtEngine::shutdown() {
- if(Dump.isOn("benchmark")) {
- Dump("benchmark") << QuitCommand();
- }
-
doPendingPops();
+ while(options::incrementalSolving() && d_userContext->getLevel() > 1) {
+ internalPop(true);
+ }
+
// check to see if a postsolve() is pending
if(d_needPostsolve) {
d_theoryEngine->postsolve();
d_needPostsolve = false;
}
- if(d_propEngine != NULL) d_propEngine->shutdown();
- if(d_theoryEngine != NULL) d_theoryEngine->shutdown();
- if(d_decisionEngine != NULL) d_decisionEngine->shutdown();
+ if(d_propEngine != NULL) {
+ d_propEngine->shutdown();
+ }
+ if(d_theoryEngine != NULL) {
+ d_theoryEngine->shutdown();
+ }
+ if(d_decisionEngine != NULL) {
+ d_decisionEngine->shutdown();
+ }
}
SmtEngine::~SmtEngine() throw() {
SmtScope smts(this);
try {
- doPendingPops();
-
- while(options::incrementalSolving() && d_userContext->getLevel() > 1) {
- internalPop(true);
- }
-
shutdown();
// global push/pop around everything, to ensure proper destruction
@@ -430,6 +478,10 @@ SmtEngine::~SmtEngine() throw() {
d_assertionList->deleteSelf();
}
+ if(d_modelCommands != NULL) {
+ d_modelCommands->deleteSelf();
+ }
+
d_definedFunctions->deleteSelf();
StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
@@ -1918,13 +1970,20 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException)
}
-void SmtEngine::addToModelCommand( Command* c, int c_type ){
- Trace("smt") << "SMT addToModelCommand(" << c << ", " << c_type << ")" << endl;
+void SmtEngine::addToModelCommand(Command* c) {
+ Trace("smt") << "SMT addToModelCommand(" << c << ")" << endl;
SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
- if( options::produceModels() ) {
- d_theoryEngine->getModel()->addCommand( c, c_type );
+ // If we aren't yet fully inited, the user might still turn on
+ // produce-models. So let's keep any commands around just in
+ // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
+ // sort "U" in QF_UF before setLogic() is run and we still want to
+ // support finding card(U) with --finite-model-find, and (2) to
+ // decouple SmtEngine and ExprManager if the user does a few
+ // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
+ // and expects to find their cardinalities in the model.
+ if( ! d_fullyInited || options::produceModels() ) {
+ doPendingPops();
+ d_modelCommands->push_back(c);
}
}
@@ -1978,7 +2037,7 @@ void SmtEngine::checkModel() throw(InternalErrorException) {
theory::SubstitutionMap substitutions(&fakeContext);
for(size_t k = 0; k < m->getNumCommands(); ++k) {
- DeclareFunctionCommand* c = dynamic_cast<DeclareFunctionCommand*>(m->getCommand(k));
+ const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k));
Notice() << "SmtEngine::checkModel(): model command " << k << " : " << m->getCommand(k) << endl;
if(c == NULL) {
// we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
@@ -2015,7 +2074,7 @@ void SmtEngine::checkModel() throw(InternalErrorException) {
// [func->func2] and checking equality of the Nodes.
// (this just a way to check if func is in n.)
theory::SubstitutionMap subs(&fakeContext);
- Node func2 = NodeManager::currentNM()->mkSkolem(TypeNode::fromType(func.getType()));
+ Node func2 = NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func.getType()), "", NodeManager::SKOLEM_NO_NOTIFY);
subs.addSubstitution(func, func2);
if(subs.apply(n) != n) {
Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 9614c8ced..2fa60104c 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -44,12 +44,13 @@
namespace CVC4 {
-
template <bool ref_count> class NodeTemplate;
typedef NodeTemplate<true> Node;
typedef NodeTemplate<false> TNode;
class NodeHashFunction;
+class Command;
+
class DecisionEngine;
class TheoryEngine;
@@ -77,6 +78,9 @@ namespace smt {
class SmtScope;
void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
+
+ struct CommandCleanup;
+ typedef context::CDList<Command*, CommandCleanup> CommandList;
}/* CVC4::smt namespace */
// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
@@ -132,6 +136,12 @@ class CVC4_PUBLIC SmtEngine {
AssignmentSet* d_assignments;
/**
+ * A list of commands that should be in the Model. Only maintained
+ * if produce-models option is on.
+ */
+ smt::CommandList* d_modelCommands;
+
+ /**
* The logic we're in.
*/
LogicInfo d_logic;
@@ -264,6 +274,9 @@ class CVC4_PUBLIC SmtEngine {
friend class ::CVC4::smt::SmtEnginePrivate;
friend class ::CVC4::smt::SmtScope;
friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
+ // to access d_modelCommands
+ friend size_t ::CVC4::Model::getNumCommands() const;
+ friend const Command* ::CVC4::Model::getCommand(size_t) const;
StatisticsRegistry* d_statisticsRegistry;
@@ -293,6 +306,12 @@ class CVC4_PUBLIC SmtEngine {
/** time spent in checkModel() */
TimerStat d_checkModelTime;
+ /**
+ * Add to Model command. This is used for recording a command that should be reported
+ * during a get-model call.
+ */
+ void addToModelCommand(Command* c);
+
public:
/**
@@ -413,12 +432,6 @@ public:
CVC4::SExpr getAssignment() throw(ModalException, AssertionException);
/**
- * Add to Model command. This is used for recording a command that should be reported
- * during a get-model call.
- */
- void addToModelCommand( Command* c, int c_type );
-
- /**
* Get the model (only if immediately preceded by a SAT
* or INVALID query). Only permitted if CVC4 was built with model
* support and produce-models is on.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback