diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
commit | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (patch) | |
tree | 8db12e260b24978bbbed3363846f6daf7c0da04f /src/smt | |
parent | 5e2f381b26d683691d9a040589536dc39c5831e0 (diff) |
parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/Makefile.am | 4 | ||||
-rw-r--r-- | src/smt/bad_option.h | 48 | ||||
-rw-r--r-- | src/smt/noninteractive_exception.h | 49 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 92 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 147 |
5 files changed, 274 insertions, 66 deletions
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 90d58904a..192915152 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -7,4 +7,6 @@ noinst_LTLIBRARIES = libsmt.la libsmt_la_SOURCES = \ smt_engine.cpp \ - smt_engine.h + smt_engine.h \ + noninteractive_exception.h \ + bad_option.h diff --git a/src/smt/bad_option.h b/src/smt/bad_option.h new file mode 100644 index 000000000..800d8e68a --- /dev/null +++ b/src/smt/bad_option.h @@ -0,0 +1,48 @@ +/********************* */ +/*! \file bad_option.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, 2010 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 An exception that is thrown when an option setting is not + ** understood. + ** + ** An exception that is thrown when an interactive-only feature while + ** CVC4 is being used in a non-interactive setting (for example, the + ** "(get-assertions)" command in an SMT-LIBv2 script). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SMT__BAD_OPTION_H +#define __CVC4__SMT__BAD_OPTION_H + +#include "util/exception.h" + +namespace CVC4 { + +class CVC4_PUBLIC BadOption : public CVC4::Exception { +public: + BadOption() : + Exception("Unrecognized informational or option key or setting") { + } + + BadOption(const std::string& msg) : + Exception(msg) { + } + + BadOption(const char* msg) : + Exception(msg) { + } +};/* class BadOption */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT__BAD_OPTION_H */ diff --git a/src/smt/noninteractive_exception.h b/src/smt/noninteractive_exception.h new file mode 100644 index 000000000..4cf97ab3e --- /dev/null +++ b/src/smt/noninteractive_exception.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file noninteractive_exception.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, 2010 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 An exception that is thrown when an interactive-only + ** feature while CVC4 is being used in a non-interactive setting + ** + ** An exception that is thrown when an interactive-only feature while + ** CVC4 is being used in a non-interactive setting (for example, the + ** "(get-assertions)" command in an SMT-LIBv2 script). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H +#define __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H + +#include "util/exception.h" + +namespace CVC4 { + +class CVC4_PUBLIC NoninteractiveException : public CVC4::Exception { +public: + NoninteractiveException() : + Exception("Interactive feature used while operating in " + "non-interactive mode") { + } + + NoninteractiveException(const std::string& msg) : + Exception(msg) { + } + + NoninteractiveException(const char* msg) : + Exception(msg) { + } +};/* class NoninteractiveException */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cb97d7f4c..c4eceeb24 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -17,6 +17,9 @@ **/ #include "smt/smt_engine.h" +#include "smt/noninteractive_exception.h" +#include "context/context.h" +#include "context/cdlist.h" #include "expr/command.h" #include "expr/node_builder.h" #include "util/output.h" @@ -25,9 +28,10 @@ #include "prop/prop_engine.h" #include "theory/theory_engine.h" - +using namespace CVC4; +using namespace CVC4::smt; using namespace CVC4::prop; -using CVC4::context::Context; +using namespace CVC4::context; namespace CVC4 { @@ -69,19 +73,30 @@ public: using ::CVC4::smt::SmtEnginePrivate; SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : - d_ctxt(em->getContext()), + d_context(em->getContext()), d_exprManager(em), d_nodeManager(em->getNodeManager()), - d_options(opts) { + d_options(opts), + /* These next few are initialized below, after we have a NodeManager + * in scope. */ + d_decisionEngine(NULL), + d_theoryEngine(NULL), + d_propEngine(NULL), + d_assertionList(NULL) { NodeManagerScope nms(d_nodeManager); d_decisionEngine = new DecisionEngine; // We have mutual dependancy here, so we add the prop engine to the theory // engine later (it is non-essential there) - d_theoryEngine = new TheoryEngine(d_ctxt, opts); - d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt); + d_theoryEngine = new TheoryEngine(d_context, opts); + d_propEngine = new PropEngine(opts, d_decisionEngine, + d_theoryEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); + + if(d_options->interactive) { + d_assertionList = new(true) CDList<Expr>(d_context); + } } void SmtEngine::shutdown() { @@ -95,6 +110,8 @@ SmtEngine::~SmtEngine() { shutdown(); + ::delete d_assertionList; + delete d_theoryEngine; delete d_propEngine; delete d_decisionEngine; @@ -105,53 +122,79 @@ void SmtEngine::doCommand(Command* c) { c->invoke(this); } +void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOption) { + // FIXME implement me +} + +const SExpr& SmtEngine::getInfo(const std::string& key) const throw(BadOption) { + // FIXME implement me + throw BadOption(); +} + +void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOption) { + // FIXME implement me +} + +const SExpr& SmtEngine::getOption(const std::string& key) const throw(BadOption) { + // FIXME implement me + throw BadOption(); +} + +void SmtEngine::defineFunction(const string& name, + const vector<pair<string, Type> >& args, + Type type, + Expr formula) { + NodeManagerScope nms(d_nodeManager); + Unimplemented(); +} + Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) { return smt.d_theoryEngine->preprocess(n); } Result SmtEngine::check() { - Debug("smt") << "SMT check()" << std::endl; + Debug("smt") << "SMT check()" << endl; return d_propEngine->checkSat(); } Result SmtEngine::quickCheck() { - Debug("smt") << "SMT quickCheck()" << std::endl; + Debug("smt") << "SMT quickCheck()" << endl; return Result(Result::VALIDITY_UNKNOWN); } void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) { - Debug("smt") << "push_back assertion " << n << std::endl; + Debug("smt") << "push_back assertion " << n << endl; smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n)); } Result SmtEngine::checkSat(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT checkSat(" << e << ")" << std::endl; + Debug("smt") << "SMT checkSat(" << e << ")" << endl; SmtEnginePrivate::addFormula(*this, e.getNode()); Result r = check().asSatisfiabilityResult(); - Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << std::endl; + Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl; return r; } Result SmtEngine::query(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT query(" << e << ")" << std::endl; + Debug("smt") << "SMT query(" << e << ")" << endl; SmtEnginePrivate::addFormula(*this, e.getNode().notNode()); Result r = check().asValidityResult(); - Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl; + Debug("smt") << "SMT query(" << e << ") ==> " << r << endl; return r; } Result SmtEngine::assertFormula(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl; + Debug("smt") << "SMT assertFormula(" << e << ")" << endl; SmtEnginePrivate::addFormula(*this, e.getNode()); return quickCheck().asValidityResult(); } Expr SmtEngine::simplify(const Expr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT simplify(" << e << ")" << std::endl; + Debug("smt") << "SMT simplify(" << e << ")" << endl; Unimplemented(); } @@ -160,15 +203,30 @@ Model SmtEngine::getModel() { Unimplemented(); } +Expr SmtEngine::getValue(Expr term) { + NodeManagerScope nms(d_nodeManager); + Unimplemented(); +} + +vector<Expr> SmtEngine::getAssertions() throw(NoninteractiveException) { + if(!d_options->interactive) { + const char* msg = + "Cannot query the current assertion list when not in interactive mode."; + throw NoninteractiveException(msg); + } + Assert(d_assertionList != NULL); + return vector<Expr>(d_assertionList->begin(), d_assertionList->end()); +} + void SmtEngine::push() { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT push()" << std::endl; + Debug("smt") << "SMT push()" << endl; Unimplemented(); } void SmtEngine::pop() { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT pop()" << std::endl; + Debug("smt") << "SMT pop()" << endl; Unimplemented(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index b5807852b..56e38af7a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -27,6 +27,9 @@ #include "expr/expr_manager.h" #include "util/result.h" #include "util/model.h" +#include "util/sexpr.h" +#include "smt/noninteractive_exception.h" +#include "smt/bad_option.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -36,6 +39,7 @@ namespace CVC4 { namespace context { class Context; + template <class T> class CDList; }/* CVC4::context namespace */ class Command; @@ -63,6 +67,61 @@ namespace smt { // The CNF conversion can go on in PropEngine. class CVC4_PUBLIC SmtEngine { +private: + + /** Our Context */ + context::Context* d_context; + + /** Our expression manager */ + ExprManager* d_exprManager; + + /** Out internal expression/node manager */ + NodeManager* d_nodeManager; + + /** User-level options */ + const Options* d_options; + + /** The decision engine */ + DecisionEngine* d_decisionEngine; + + /** The decision engine */ + TheoryEngine* d_theoryEngine; + + /** The propositional engine */ + prop::PropEngine* d_propEngine; + + /** + * The assertion list, before any conversion, for supporting + * getAssertions(). Only maintained if in interactive mode. + */ + context::CDList<Expr>* d_assertionList; + + // preprocess() and addFormula() used to be housed here; they are + // now in an SmtEnginePrivate class. See the comment in + // smt_engine.cpp. + + /** + * This is called by the destructor, just before destroying the + * PropEngine, TheoryEngine, and DecisionEngine (in that order). It + * is important because there are destruction ordering issues + * between PropEngine and Theory. + */ + void shutdown(); + + /** + * Full check of consistency in current context. Returns true iff + * consistent. + */ + Result check(); + + /** + * Quick check of consistency in current context: calls + * processAssertionList() then look for inconsistency (based only on + * that). + */ + Result quickCheck(); + + friend class ::CVC4::smt::SmtEnginePrivate; public: @@ -82,6 +141,37 @@ public: void doCommand(Command*); /** + * Set information about the script executing. + */ + void setInfo(const std::string& key, const SExpr& value) throw(BadOption); + + /** + * Query information about the SMT environment. + */ + const SExpr& getInfo(const std::string& key) const throw(BadOption); + + /** + * Set an aspect of the current SMT execution environment. + */ + void setOption(const std::string& key, const SExpr& value) throw(BadOption); + + /** + * Get an aspect of the current SMT execution environment. + */ + const SExpr& getOption(const std::string& key) const throw(BadOption); + + /** + * Add a formula to the current context: preprocess, do per-theory + * setup, use processAssertionList(), asserting to T-solver for + * literals and conjunction of literals. Returns false iff + * inconsistent. + */ + void defineFunction(const std::string& name, + const std::vector<std::pair<std::string, Type> >& args, + Type type, + Expr formula); + + /** * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for * literals and conjunction of literals. Returns false iff @@ -113,64 +203,25 @@ public: Model getModel(); /** - * Push a user-level context. - */ - void push(); - - /** - * Pop a user-level context. Throws an exception if nothing to pop. + * Get the assigned value of a term (only if preceded by a SAT or + * INVALID query). */ - void pop(); - -private: - - /** Our Context */ - CVC4::context::Context* d_ctxt; - - /** Our expression manager */ - ExprManager* d_exprManager; - - /** Out internal expression/node manager */ - NodeManager* d_nodeManager; - - /** User-level options */ - const Options* d_options; - - /** The decision engine */ - DecisionEngine* d_decisionEngine; - - /** The decision engine */ - TheoryEngine* d_theoryEngine; - - /** The propositional engine */ - prop::PropEngine* d_propEngine; - - // preprocess() and addFormula() used to be housed here; they are - // now in an SmtEnginePrivate class. See the comment in - // smt_engine.cpp. + Expr getValue(Expr term); /** - * This is called by the destructor, just before destroying the - * PropEngine, TheoryEngine, and DecisionEngine (in that order). It - * is important because there are destruction ordering issues - * between PropEngine and Theory. + * Get the current set of assertions. */ - void shutdown(); + std::vector<Expr> getAssertions() throw(NoninteractiveException); /** - * Full check of consistency in current context. Returns true iff - * consistent. + * Push a user-level context. */ - Result check(); + void push(); /** - * Quick check of consistency in current context: calls - * processAssertionList() then look for inconsistency (based only on - * that). + * Pop a user-level context. Throws an exception if nothing to pop. */ - Result quickCheck(); - - friend class ::CVC4::smt::SmtEnginePrivate; + void pop(); };/* class SmtEngine */ |