From 2d7ff62cd52c5c56f29b6567489310cc45767236 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 7 Oct 2010 07:16:49 +0000 Subject: [PATCH] SMT-LIBv2 (define-fun...) command now functional; does eager expansion at preprocessing time --- src/expr/command.cpp | 35 ++-- src/expr/command.h | 11 +- src/expr/expr_template.cpp | 6 +- src/expr/expr_template.h | 14 +- src/expr/node.h | 67 +++++++ src/expr/node_value.h | 64 ++++++- src/expr/type.cpp | 5 +- src/expr/type.h | 4 +- src/expr/type_node.cpp | 25 +-- src/expr/type_node.h | 36 +++- src/main/getopt.cpp | 6 + src/parser/smt2/Smt2.g | 18 +- src/smt/Makefile.am | 3 +- .../{bad_option.h => bad_option_exception.h} | 18 +- src/smt/no_such_function_exception.h | 44 +++++ src/smt/smt_engine.cpp | 175 +++++++++++++++--- src/smt/smt_engine.h | 68 +++---- src/util/options.h | 4 + test/regress/regress0/Makefile.am | 1 + .../regress0/simple-rdl-definefun.smt2 | 14 ++ 20 files changed, 491 insertions(+), 127 deletions(-) rename src/smt/{bad_option.h => bad_option_exception.h} (73%) create mode 100644 src/smt/no_such_function_exception.h create mode 100644 test/regress/regress0/simple-rdl-definefun.smt2 diff --git a/src/expr/command.cpp b/src/expr/command.cpp index a1486fcab..8c90f337e 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -23,6 +23,7 @@ #include "expr/command.h" #include "smt/smt_engine.h" +#include "smt/bad_option_exception.h" #include "util/output.h" using namespace std; @@ -217,26 +218,26 @@ void DeclarationCommand::toStream(std::ostream& out) const { /* class DefineFunctionCommand */ -DefineFunctionCommand::DefineFunctionCommand(const std::string& name, - const std::vector >& args, - Type type, - Expr formula) : - d_name(name), - d_args(args), - d_type(type), +DefineFunctionCommand::DefineFunctionCommand(Expr func, + const std::vector& formals, + Expr formula) : + d_func(func), + d_formals(formals), d_formula(formula) { } void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { - smtEngine->defineFunction(d_name, d_args, d_type, d_formula); + smtEngine->defineFunction(d_func, d_formals, d_formula); } void DefineFunctionCommand::toStream(std::ostream& out) const { - out << "DefineFunction( \"" << d_name << "\", ["; - copy( d_args.begin(), d_args.end() - 1, - ostream_iterator >(out, ", ") ); - out << d_args.back(); - out << "], << " << d_type << " >>, << " << d_formula << " >> )"; + out << "DefineFunction( \"" << d_func << "\", ["; + if(d_formals.size() > 0) { + copy( d_formals.begin(), d_formals.end() - 1, + ostream_iterator(out, ", ") ); + out << d_formals.back(); + } + out << "], << " << d_formula << " >> )"; } /* class GetValueCommand */ @@ -324,7 +325,7 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setInfo(d_flag, d_sexpr); //d_result = "success"; - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } @@ -352,7 +353,7 @@ GetInfoCommand::GetInfoCommand(std::string flag) : void GetInfoCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getInfo(d_flag).getValue(); - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } @@ -382,7 +383,7 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setOption(d_flag, d_sexpr); //d_result = "success"; - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } @@ -410,7 +411,7 @@ GetOptionCommand::GetOptionCommand(std::string flag) : void GetOptionCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getOption(d_flag).getValue(); - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } diff --git a/src/expr/command.h b/src/expr/command.h index 0c78dd1c6..4c74cfd6c 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -111,14 +111,13 @@ public: class CVC4_PUBLIC DefineFunctionCommand : public Command { protected: - std::string d_name; - std::vector > d_args; - Type d_type; + Expr d_func; + std::vector d_formals; Expr d_formula; public: - DefineFunctionCommand(const std::string& name, - const std::vector >& args, - Type type, Expr formula); + DefineFunctionCommand(Expr func, + const std::vector& formals, + Expr formula); void invoke(SmtEngine* smtEngine); void toStream(std::ostream& out) const; };/* class DefineFunctionCommand */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 803808b0f..5fb931a65 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -223,7 +223,11 @@ void Expr::toStream(std::ostream& out, int depth, bool types) const { d_node->toStream(out, depth, types); } -Node Expr::getNode() const { +Node Expr::getNode() const throw() { + return *d_node; +} + +TNode Expr::getTNode() const throw() { return *d_node; } diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 8fab13b37..bb227f92f 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -43,8 +43,13 @@ class NodeTemplate; class Expr; class ExprManager; +class SmtEngine; class Type; +namespace smt { + class SmtEnginePrivate; +}/* CVC4::smt namespace */ + namespace expr { class CVC4_PUBLIC ExprSetDepth; class CVC4_PUBLIC ExprPrintTypes; @@ -383,10 +388,17 @@ protected: * Returns the actual internal node. * @return the internal node */ - NodeTemplate getNode() const; + NodeTemplate getNode() const throw(); + + /** + * Returns the actual internal node as a TNode. + * @return the internal node + */ + NodeTemplate getTNode() const throw(); // Friend to access the actual internal expr information and private methods friend class SmtEngine; + friend class smt::SmtEnginePrivate; friend class ExprManager; }; diff --git a/src/expr/node.h b/src/expr/node.h index 67d46a977..bd6b53522 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -379,6 +379,20 @@ public: TypeNode getType(bool check = false) const throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException); + /** + * Substitution of Nodes. + */ + Node substitute(TNode node, TNode replacement) const; + + /** + * Simultaneous substitution of Nodes. + */ + template + Node substitute(Iterator1 nodesBegin, + Iterator1 nodesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const; + /** * Returns the kind of this node. * @return the kind @@ -1035,6 +1049,59 @@ TypeNode NodeTemplate::getType(bool check) const return NodeManager::currentNM()->getType(*this, check); } +template +Node NodeTemplate::substitute(TNode node, + TNode replacement) const { + NodeBuilder<> nb(getKind()); + if(getMetaKind() == kind::metakind::PARAMETERIZED) { + // push the operator + nb << getOperator(); + } + for(TNode::const_iterator i = begin(), + iend = end(); + i != iend; + ++i) { + if(*i == node) { + nb << replacement; + } else { + (*i).substitute(node, replacement); + } + } + Node n = nb; + return n; +} + +template +template +Node NodeTemplate::substitute(Iterator1 nodesBegin, + Iterator1 nodesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const { + Assert( nodesEnd - nodesBegin == replacementsEnd - replacementsBegin, + "Substitution iterator ranges must be equal size" ); + Iterator1 j = find(nodesBegin, nodesEnd, *this); + if(j != nodesEnd) { + return *(replacementsBegin + (j - nodesBegin)); + } else if(getNumChildren() == 0) { + return *this; + } else { + NodeBuilder<> nb(getKind()); + if(getMetaKind() == kind::metakind::PARAMETERIZED) { + // push the operator + nb << getOperator(); + } + for(TNode::const_iterator i = begin(), + iend = end(); + i != iend; + ++i) { + nb << (*i).substitute(nodesBegin, nodesEnd, + replacementsBegin, replacementsEnd); + } + Node n = nb; + return n; + } +} + #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used diff --git a/src/expr/node_value.h b/src/expr/node_value.h index e4fc479b7..658cb1e2d 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -171,8 +171,48 @@ private: return iterator(d_i++); } - typedef std::input_iterator_tag iterator_category; - }; + iterator& operator--() { + --d_i; + return *this; + } + + iterator operator--(int) { + return iterator(d_i--); + } + + iterator& operator+=(difference_type p) { + d_i += p; + return *this; + } + + iterator& operator-=(difference_type p) { + d_i -= p; + return *this; + } + + iterator operator+(difference_type p) { + return iterator(d_i + p); + } + + iterator operator-(difference_type p) { + return iterator(d_i - p); + } + + difference_type operator-(iterator i) { + return d_i - i.d_i; + } + + typedef std::random_access_iterator_tag iterator_category; + };/* class NodeValue::iterator */ + + // operator+ (as a function) cannot be a template, so we have to + // define two versions + friend NodeValue::iterator > + operator+(NodeValue::iterator >::difference_type p, + NodeValue::iterator > i); + friend NodeValue::iterator > + operator+(NodeValue::iterator >::difference_type p, + NodeValue::iterator > i); /** Decrement ref counts of children */ inline void decrRefCounts(); @@ -258,6 +298,26 @@ private: };/* class NodeValue */ +/** + * Provides a symmetric addition operator to that already defined in + * the iterator class. + */ +inline NodeValue::iterator > +operator+(NodeValue::iterator >::difference_type p, + NodeValue::iterator > i) { + return i + p; +} + +/** + * Provides a symmetric addition operator to that already defined in + * the iterator class. + */ +inline NodeValue::iterator > +operator+(NodeValue::iterator >::difference_type p, + NodeValue::iterator > i) { + return i + p; +} + /** * For hash_maps, hash_sets, etc.. but this is for expr package * internal use only at present! This is likely to be POORLY diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 05b69f6f4..8cf555eb0 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -111,7 +111,10 @@ Type Type::substitute(const vector& types, replacementsNodes.push_back(*(*i).d_typeNode); } - return makeType(d_typeNode->substitute(typesNodes, replacementsNodes)); + return makeType(d_typeNode->substitute(typesNodes.begin(), + typesNodes.end(), + replacementsNodes.begin(), + replacementsNodes.end())); } void Type::toStream(ostream& out) const { diff --git a/src/expr/type.h b/src/expr/type.h index 57ec3bf5c..19c3d27f3 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -60,6 +60,8 @@ struct CVC4_PUBLIC TypeHashStrategy { */ class CVC4_PUBLIC Type { + friend class SmtEngine; + friend class SmtEnginePrivate; friend class ExprManager; friend class TypeNode; friend class TypeHashStrategy; @@ -87,7 +89,7 @@ protected: Type(NodeManager* em, TypeNode* typeNode); /** Accessor for derived classes */ - static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; } + static TypeNode* getTypeNode(const Type& t) throw() { return t.d_typeNode; } public: diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index a55c05c5a..badc3b72f 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -33,7 +33,10 @@ TypeNode TypeNode::substitute(const TypeNode& type, // push the operator nb << TypeNode(d_nv->d_children[0]); } - for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) { + for(TypeNode::const_iterator i = begin(), + iend = end(); + i != iend; + ++i) { if(*i == type) { nb << replacement; } else { @@ -43,26 +46,6 @@ TypeNode TypeNode::substitute(const TypeNode& type, return nb.constructTypeNode(); } -TypeNode TypeNode::substitute(const vector& types, - const vector& replacements) const { - vector::const_iterator j = find(types.begin(), types.end(), *this); - if(j != types.end()) { - return replacements[j - types.begin()]; - } else if(getNumChildren() == 0) { - return *this; - } else { - NodeBuilder<> nb(getKind()); - if(getMetaKind() == kind::metakind::PARAMETERIZED) { - // push the operator - nb << TypeNode(d_nv->d_children[0]); - } - for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) { - nb << (*i).substitute(types, replacements); - } - return nb.constructTypeNode(); - } -} - bool TypeNode::isBoolean() const { return getKind() == kind::TYPE_CONSTANT && getConst() == BOOLEAN_TYPE; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 6780b08f7..0e763128f 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -118,8 +118,11 @@ public: /** * Simultaneous substitution of TypeNodes. */ - TypeNode substitute(const std::vector& types, - const std::vector& replacements) const; + template + TypeNode substitute(Iterator1 typesBegin, + Iterator1 typesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const; /** * Structural comparison operator for expressions. @@ -436,6 +439,35 @@ struct TypeNodeHashStrategy { namespace CVC4 { +template +TypeNode TypeNode::substitute(Iterator1 typesBegin, + Iterator1 typesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const { + Assert( typesEnd - typesBegin == replacementsEnd - replacementsBegin, + "Substitution iterator ranges must be equal size" ); + Iterator1 j = find(typesBegin, typesEnd, *this); + if(j != typesEnd) { + return *(replacementsBegin + (j - typesBegin)); + } else if(getNumChildren() == 0) { + return *this; + } else { + NodeBuilder<> nb(getKind()); + if(getMetaKind() == kind::metakind::PARAMETERIZED) { + // push the operator + nb << TypeNode(d_nv->d_children[0]); + } + for(TypeNode::const_iterator i = begin(), + iend = end(); + i != iend; + ++i) { + nb << (*i).substitute(typesBegin, typesEnd, + replacementsBegin, replacementsEnd); + } + return nb.constructTypeNode(); + } +} + inline size_t TypeNode::getNumChildren() const { return d_nv->getNumChildren(); } diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 4af882aa1..82214bed3 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -71,6 +71,7 @@ enum OptionValue { DEFAULT_EXPR_DEPTH, PRINT_EXPR_TYPES, UF_THEORY, + LAZY_DEFINITION_EXPANSION, INTERACTIVE, NO_INTERACTIVE };/* enum OptionValue */ @@ -119,6 +120,7 @@ static struct option cmdlineOptions[] = { { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH }, { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES }, { "uf" , required_argument, NULL, UF_THEORY }, + { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION }, { "interactive", no_argument , NULL, INTERACTIVE }, { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { NULL , no_argument , NULL, '\0' } @@ -272,6 +274,10 @@ throw(OptionException) { } break; + case LAZY_DEFINITION_EXPANSION: + opts->lazyDefinitionExpansion = true; + break; + case INTERACTIVE: opts->interactive = true; opts->interactiveSetByUser = true; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 9ad8c3177..a2792eaac 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -131,7 +131,7 @@ command returns [CVC4::Command* cmd] Type t; std::vector terms; std::vector sorts; - std::vector > sortedVars; + std::vector > sortedVarNames; SExpr sexpr; } : /* set the logic */ @@ -202,15 +202,15 @@ command returns [CVC4::Command* cmd] $cmd = new DeclarationCommand(name,t); } | /* function definition */ DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] - LPAREN_TOK sortedVarList[sortedVars] RPAREN_TOK + LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK sortSymbol[t] { /* add variables to parser state before parsing term */ Debug("parser") << "define fun: '" << name << "'" << std::endl; - if( sortedVars.size() > 0 ) { + if( sortedVarNames.size() > 0 ) { std::vector sorts; - sorts.reserve(sortedVars.size()); + sorts.reserve(sortedVarNames.size()); for(std::vector >::const_iterator i = - sortedVars.begin(), iend = sortedVars.end(); + sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { sorts.push_back((*i).second); @@ -219,10 +219,10 @@ command returns [CVC4::Command* cmd] } PARSER_STATE->pushScope(); for(std::vector >::const_iterator i = - sortedVars.begin(), iend = sortedVars.end(); + sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { - PARSER_STATE->mkVar((*i).first, (*i).second); + terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second)); } } term[expr] @@ -230,8 +230,8 @@ command returns [CVC4::Command* cmd] // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) - PARSER_STATE->mkFunction(name, t); - $cmd = new DefineFunctionCommand(name, sortedVars, t, expr); + Expr func = PARSER_STATE->mkFunction(name, t); + $cmd = new DefineFunctionCommand(func, terms, expr); } | /* value query */ GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK 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 similarity index 73% rename from src/smt/bad_option.h rename to 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 +#include + #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; @@ -37,6 +44,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 d_formals; + Node d_formula; +public: + DefinedFunction() {} + DefinedFunction(Node func, vector formals, Node formula) : + d_func(func), + d_formals(formals), + d_formula(formula) { + } + Node getFunction() const { return d_func; } + vector 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 @@ -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 >& args, - Type type, +void SmtEngine::defineFunction(Expr func, + const vector& formals, Expr formula) { NodeManagerScope nms(d_nodeManager); - d_functions->insert(name, make_pair(make_pair(args, type), formula)); + TNode funcNode = func.getTNode(); + vector formalsNodes; + for(vector::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 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(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 CDList; -}/* CVC4::context namespace */ - +template class NodeTemplate; +typedef NodeTemplate Node; +typedef NodeTemplate TNode; +class NodeHashFunction; class Command; class Options; class TheoryEngine; class DecisionEngine; +namespace context { + class Context; + template 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 TypedArg; - /** A vector of typed formals, and a return type */ - typedef std::pair, Type> FunctionSignature; /** The type of our internal map of defined functions */ - typedef context::CDMap, - StringHashFunction> - FunctionMap; - + typedef context::CDMap + DefinedFunctionMap; /** The type of our internal assertion list */ typedef context::CDList 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. @@ -140,30 +146,29 @@ 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 >& args, - Type type, + void defineFunction(Expr func, + const std::vector& 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 getAssertions() throw(NoninteractiveException); diff --git a/src/util/options.h b/src/util/options.h index c504177bf..9bb0b0a38 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -65,6 +65,9 @@ struct CVC4_PUBLIC Options { /** Should we strictly enforce the language standard while parsing? */ bool strictParsing; + /** Should we expand function definitions lazily? */ + bool lazyDefinitionExpansion; + /** Whether we're in interactive mode or not */ bool interactive; @@ -86,6 +89,7 @@ struct CVC4_PUBLIC Options { semanticChecks(true), memoryMap(false), strictParsing(false), + lazyDefinitionExpansion(false), interactive(false), interactiveSetByUser(false) { } diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index cdd347962..9bc8991ab 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -33,6 +33,7 @@ SMT2_TESTS = \ ite4.smt2 \ simple-lra.smt2 \ simple-rdl.smt2 \ + simple-rdl-definefun.smt2 \ simple-uf.smt2 # Regression tests for PL inputs diff --git a/test/regress/regress0/simple-rdl-definefun.smt2 b/test/regress/regress0/simple-rdl-definefun.smt2 new file mode 100644 index 000000000..08e99867a --- /dev/null +++ b/test/regress/regress0/simple-rdl-definefun.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_RDL) +(set-info :status unsat) +(declare-fun x () Real) +(declare-fun y () Real) +(declare-sort U 0) +(declare-sort A 2) +(define-sort F (x) (A Real Real)) +(declare-fun x2 () (F Real)) +(define-fun minus ((x Real) (z Real)) Real (- x z)) +(define-fun less ((x Real) (z Real)) Bool (< x z)) +(define-fun foo ((x Real) (z Real)) Bool (less x z)) +(assert (not (=> (foo (minus x y) 0) (less x y)))) +(check-sat) +(exit) -- 2.30.2