diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-07 07:16:49 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-07 07:16:49 +0000 |
commit | 2d7ff62cd52c5c56f29b6567489310cc45767236 (patch) | |
tree | afb975f93b219e7b7a670a4dfc2897e425fd9bf7 /src/smt | |
parent | ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 (diff) |
SMT-LIBv2 (define-fun...) command now functional; does eager expansion at preprocessing time
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/Makefile.am | 3 | ||||
-rw-r--r-- | src/smt/bad_option_exception.h (renamed from src/smt/bad_option.h) | 18 | ||||
-rw-r--r-- | src/smt/no_such_function_exception.h | 44 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 175 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 68 |
5 files changed, 242 insertions, 66 deletions
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 192915152..319b25576 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -9,4 +9,5 @@ libsmt_la_SOURCES = \ smt_engine.cpp \ smt_engine.h \ noninteractive_exception.h \ - bad_option.h + bad_option_exception.h \ + no_such_function_exception.h diff --git a/src/smt/bad_option.h b/src/smt/bad_option_exception.h index 800d8e68a..13e5d96d0 100644 --- a/src/smt/bad_option.h +++ b/src/smt/bad_option_exception.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file bad_option.h +/*! \file bad_option_exception.h ** \verbatim ** Original author: mdeters ** Major contributors: none @@ -21,28 +21,28 @@ #include "cvc4_public.h" -#ifndef __CVC4__SMT__BAD_OPTION_H -#define __CVC4__SMT__BAD_OPTION_H +#ifndef __CVC4__SMT__BAD_OPTION_EXCEPTION_H +#define __CVC4__SMT__BAD_OPTION_EXCEPTION_H #include "util/exception.h" namespace CVC4 { -class CVC4_PUBLIC BadOption : public CVC4::Exception { +class CVC4_PUBLIC BadOptionException : public CVC4::Exception { public: - BadOption() : + BadOptionException() : Exception("Unrecognized informational or option key or setting") { } - BadOption(const std::string& msg) : + BadOptionException(const std::string& msg) : Exception(msg) { } - BadOption(const char* msg) : + BadOptionException(const char* msg) : Exception(msg) { } -};/* class BadOption */ +};/* class BadOptionException */ }/* CVC4 namespace */ -#endif /* __CVC4__SMT__BAD_OPTION_H */ +#endif /* __CVC4__SMT__BAD_OPTION_EXCEPTION_H */ diff --git a/src/smt/no_such_function_exception.h b/src/smt/no_such_function_exception.h new file mode 100644 index 000000000..0a5f2889c --- /dev/null +++ b/src/smt/no_such_function_exception.h @@ -0,0 +1,44 @@ +/********************* */ +/*! \file no_such_function_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 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__NO_SUCH_FUNCTION_EXCEPTION_H +#define __CVC4__SMT__NO_SUCH_FUNCTION_EXCEPTION_H + +#include "util/exception.h" + +namespace CVC4 { + +class CVC4_PUBLIC NoSuchFunctionException : public CVC4::Exception { +public: + NoSuchFunctionException(Expr name) : + Exception(std::string("Undefined function: `") + name.toString() + "': ") { + } + + NoSuchFunctionException(Expr name, const std::string& msg) : + Exception(std::string("Undefined function: `") + name.toString() + "': " + msg) { + } +};/* class NoSuchFunctionException */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT__NO_SUCH_FUNCTION_EXCEPTION_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index be4abb8ab..c41737028 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -16,10 +16,16 @@ ** The main entry point into the CVC4 library's SMT interface. **/ +#include <vector> +#include <string> + #include "smt/smt_engine.h" #include "smt/noninteractive_exception.h" +#include "smt/bad_option_exception.h" +#include "smt/no_such_function_exception.h" #include "context/context.h" #include "context/cdlist.h" +#include "expr/expr.h" #include "expr/command.h" #include "expr/node_builder.h" #include "util/output.h" @@ -28,6 +34,7 @@ #include "prop/prop_engine.h" #include "theory/theory_engine.h" +using namespace std; using namespace CVC4; using namespace CVC4::smt; using namespace CVC4::prop; @@ -38,6 +45,28 @@ namespace CVC4 { namespace smt { /** + * Representation of a defined function. We keep these around in + * SmtEngine to permit expanding definitions late (and lazily), to + * support getValue() over defined functions, to support user output + * in terms of defined functions, etc. + */ +class DefinedFunction { + Node d_func; + std::vector<Node> d_formals; + Node d_formula; +public: + DefinedFunction() {} + DefinedFunction(Node func, vector<Node> formals, Node formula) : + d_func(func), + d_formals(formals), + d_formula(formula) { + } + Node getFunction() const { return d_func; } + vector<Node> getFormals() const { return d_formals; } + Node getFormula() const { return d_formula; } +};/* class DefinedFunction */ + +/** * This is an inelegant solution, but for the present, it will work. * The point of this is to separate the public and private portions of * the SmtEngine class, so that smt_engine.h doesn't @@ -60,19 +89,27 @@ public: * passes over the Node. TODO: may need to specify a LEVEL of * preprocessing (certain contexts need more/less ?). */ - static Node preprocess(SmtEngine& smt, TNode n); + static Node preprocess(SmtEngine& smt, TNode n) + throw(NoSuchFunctionException, AssertionException); /** * Adds a formula to the current context. */ - static void addFormula(SmtEngine& smt, TNode n); + static void addFormula(SmtEngine& smt, TNode n) + throw(NoSuchFunctionException, AssertionException); + + /** + * Expand definitions in n. + */ + static Node expandDefinitions(SmtEngine& smt, TNode n) + throw(NoSuchFunctionException, AssertionException); };/* class SmtEnginePrivate */ }/* namespace CVC4::smt */ -using ::CVC4::smt::SmtEnginePrivate; +using namespace CVC4::smt; -SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : +SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() : d_context(em->getContext()), d_exprManager(em), d_nodeManager(em->getNodeManager()), @@ -94,7 +131,7 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : d_theoryEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); - d_functions = new(true) FunctionMap(d_context); + d_definedFunctions = new(true) DefinedFunctionMap(d_context); if(d_options->interactive) { d_assertionList = new(true) AssertionList(d_context); @@ -116,46 +153,125 @@ SmtEngine::~SmtEngine() { d_assertionList->deleteSelf(); } - d_functions->deleteSelf(); + d_definedFunctions->deleteSelf(); delete d_theoryEngine; delete d_propEngine; delete d_decisionEngine; } -void SmtEngine::doCommand(Command* c) { - NodeManagerScope nms(d_nodeManager); - c->invoke(this); -} - -void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOption) { +void SmtEngine::setInfo(const string& key, const SExpr& value) + throw(BadOptionException) { + if(key == ":status") { + return; + } // FIXME implement me + throw BadOptionException(); } -const SExpr& SmtEngine::getInfo(const std::string& key) const throw(BadOption) { +const SExpr& SmtEngine::getInfo(const string& key) const + throw(BadOptionException) { // FIXME implement me - throw BadOption(); + throw BadOptionException(); } -void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOption) { +void SmtEngine::setOption(const string& key, const SExpr& value) + throw(BadOptionException) { // FIXME implement me + throw BadOptionException(); } -const SExpr& SmtEngine::getOption(const std::string& key) const throw(BadOption) { +const SExpr& SmtEngine::getOption(const string& key) const + throw(BadOptionException) { // FIXME implement me - throw BadOption(); + throw BadOptionException(); } -void SmtEngine::defineFunction(const string& name, - const vector<pair<string, Type> >& args, - Type type, +void SmtEngine::defineFunction(Expr func, + const vector<Expr>& formals, Expr formula) { NodeManagerScope nms(d_nodeManager); - d_functions->insert(name, make_pair(make_pair(args, type), formula)); + TNode funcNode = func.getTNode(); + vector<Node> formalsNodes; + for(vector<Expr>::const_iterator i = formals.begin(), + iend = formals.end(); + i != iend; + ++i) { + formalsNodes.push_back((*i).getNode()); + } + TNode formulaNode = formula.getTNode(); + DefinedFunction def(funcNode, formalsNodes, formulaNode); + d_definedFunctions->insert(funcNode, def); } -Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) { - return smt.d_theoryEngine->preprocess(n); +Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n) + throw(NoSuchFunctionException, AssertionException) { + if(n.getKind() == kind::APPLY) { + TNode func = n.getOperator(); + SmtEngine::DefinedFunctionMap::const_iterator i = + smt.d_definedFunctions->find(func); + DefinedFunction def = (*i).second; + vector<Node> formals = def.getFormals(); + + if(Debug.isOn("expand")) { + Debug("expand") << "found: " << n << endl; + Debug("expand") << " func: " << func << endl; + string name = func.getAttribute(expr::VarNameAttr()); + Debug("expand") << " : \"" << name << "\"" << endl; + if(i == smt.d_definedFunctions->end()) { + throw NoSuchFunctionException(Expr(smt.d_exprManager, new Node(func))); + } + Debug("expand") << " defn: " << def.getFunction() << endl + << " ["; + if(formals.size() > 0) { + copy( formals.begin(), formals.end() - 1, + ostream_iterator<Node>(Debug("expand"), ", ") ); + Debug("expand") << formals.back(); + } + Debug("expand") << "]" << endl + << " " << def.getFunction().getType() << endl + << " " << def.getFormula() << endl; + } + + TNode fm = def.getFormula(); + Node instance = fm.substitute(formals.begin(), formals.end(), + n.begin(), n.end()); + Debug("expand") << "made : " << instance << endl; + + Node expanded = expandDefinitions(smt, instance); + return expanded; + } else if(n.getNumChildren() == 0) { + return n; + } else { + Debug("expand") << "cons : " << n << endl; + NodeBuilder<> nb(n.getKind()); + if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { + Debug("expand") << "op : " << n.getOperator() << endl; + nb << n.getOperator(); + } + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + Node expanded = expandDefinitions(smt, *i); + Debug("expand") << "exchld: " << expanded << endl; + nb << expanded; + } + Node node = nb; + return node; + } +} + +Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) + throw(NoSuchFunctionException, AssertionException) { + if(!smt.d_options->lazyDefinitionExpansion) { + Node node = expandDefinitions(smt, n); + Debug("expand") << "have: " << n << endl + << "made: " << node << endl; + return smt.d_theoryEngine->preprocess(node); + } else { + return smt.d_theoryEngine->preprocess(n); + } } Result SmtEngine::check() { @@ -168,7 +284,8 @@ Result SmtEngine::quickCheck() { return Result(Result::VALIDITY_UNKNOWN); } -void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) { +void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) + throw(NoSuchFunctionException, AssertionException) { Debug("smt") << "push_back assertion " << n << endl; smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n)); } @@ -209,8 +326,16 @@ Model SmtEngine::getModel() { Unimplemented(); } -Expr SmtEngine::getValue(Expr term) { +Expr SmtEngine::getValue(Expr term) + throw(NoninteractiveException, AssertionException) { + if(!d_options->interactive) { + const char* msg = + "Cannot query the current assertion list when not in interactive mode."; + throw NoninteractiveException(msg); + } + NodeManagerScope nms(d_nodeManager); + Unimplemented(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 97772273d..c9bf321b9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -31,7 +31,8 @@ #include "util/sexpr.h" #include "util/hash.h" #include "smt/noninteractive_exception.h" -#include "smt/bad_option.h" +#include "smt/no_such_function_exception.h" +#include "smt/bad_option_exception.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -39,21 +40,33 @@ namespace CVC4 { -namespace context { - class Context; - template <class T> class CDList; -}/* CVC4::context namespace */ - +template <bool ref_count> class NodeTemplate; +typedef NodeTemplate<true> Node; +typedef NodeTemplate<false> TNode; +class NodeHashFunction; class Command; class Options; class TheoryEngine; class DecisionEngine; +namespace context { + class Context; + template <class T> class CDList; +}/* CVC4::context namespace */ + namespace prop { class PropEngine; }/* CVC4::prop namespace */ namespace smt { + /** + * Representation of a defined function. We keep these around in + * SmtEngine to permit expanding definitions late (and lazily), to + * support getValue() over defined functions, to support user output + * in terms of defined functions, etc. + */ + class DefinedFunction; + class SmtEnginePrivate; }/* CVC4::smt namespace */ @@ -69,17 +82,10 @@ namespace smt { // The CNF conversion can go on in PropEngine. class CVC4_PUBLIC SmtEngine { -private: - /** A name/type pair, used for signatures */ - typedef std::pair<std::string, Type> TypedArg; - /** A vector of typed formals, and a return type */ - typedef std::pair<std::vector<TypedArg>, Type> FunctionSignature; /** The type of our internal map of defined functions */ - typedef context::CDMap<std::string, std::pair<FunctionSignature, Expr>, - StringHashFunction> - FunctionMap; - + typedef context::CDMap<Node, smt::DefinedFunction, NodeHashFunction> + DefinedFunctionMap; /** The type of our internal assertion list */ typedef context::CDList<Expr> AssertionList; @@ -98,7 +104,7 @@ private: /** The propositional engine */ prop::PropEngine* d_propEngine; /** An index of our defined functions */ - FunctionMap* d_functions; + DefinedFunctionMap* d_definedFunctions; /** * The assertion list (before any conversion) for supporting * getAssertions(). Only maintained if in interactive mode. @@ -141,29 +147,28 @@ public: ~SmtEngine(); /** - * Execute a command. - */ - void doCommand(Command*); - - /** * Set information about the script executing. */ - void setInfo(const std::string& key, const SExpr& value) throw(BadOption); + void setInfo(const std::string& key, const SExpr& value) + throw(BadOptionException); /** * Query information about the SMT environment. */ - const SExpr& getInfo(const std::string& key) const throw(BadOption); + const SExpr& getInfo(const std::string& key) const + throw(BadOptionException); /** * Set an aspect of the current SMT execution environment. */ - void setOption(const std::string& key, const SExpr& value) throw(BadOption); + void setOption(const std::string& key, const SExpr& value) + throw(BadOptionException); /** * Get an aspect of the current SMT execution environment. */ - const SExpr& getOption(const std::string& key) const throw(BadOption); + const SExpr& getOption(const std::string& key) const + throw(BadOptionException); /** * Add a formula to the current context: preprocess, do per-theory @@ -171,9 +176,8 @@ public: * 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, + void defineFunction(Expr func, + const std::vector<Expr>& formals, Expr formula); /** @@ -209,12 +213,14 @@ public: /** * Get the assigned value of a term (only if preceded by a SAT or - * INVALID query). + * INVALID query). Only permitted if the SmtEngine is set to + * operate interactively. */ - Expr getValue(Expr term); + Expr getValue(Expr term) throw(NoninteractiveException, AssertionException); /** - * Get the current set of assertions. + * Get the current set of assertions. Only permitted if the + * SmtEngine is set to operate interactively. */ std::vector<Expr> getAssertions() throw(NoninteractiveException); |