diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/Makefile.am | 2 | ||||
-rw-r--r-- | src/smt/command_list.cpp | 33 | ||||
-rw-r--r-- | src/smt/command_list.h | 41 | ||||
-rw-r--r-- | src/smt/options_handlers.h | 11 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 103 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 27 |
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. |