From ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 6 Oct 2010 08:31:35 +0000 Subject: [PATCH] declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand) --- src/context/cdmap.h | 9 +- src/context/cdmap_forward.h | 42 ++++ src/context/cdset.h | 17 ++ src/expr/Makefile.am | 3 +- src/expr/declaration_scope.cpp | 137 +++++++++++-- src/expr/declaration_scope.h | 123 ++++++++--- src/expr/expr_manager_template.cpp | 51 +++-- src/expr/expr_manager_template.h | 15 +- src/expr/expr_template.cpp | 6 + src/expr/expr_template.h | 32 ++- src/expr/mkmetakind | 2 +- src/expr/node.cpp | 11 +- src/expr/node.h | 13 +- src/expr/node_manager.cpp | 3 + src/expr/node_manager.h | 58 +++++- src/expr/type.cpp | 191 ++++++++++++------ src/expr/type.h | 87 ++++++-- src/expr/type_node.cpp | 77 +++++-- src/expr/type_node.h | 91 ++++++--- src/parser/parser.cpp | 82 ++++++-- src/parser/parser.h | 64 +++--- src/parser/smt/smt.cpp | 4 +- src/parser/smt2/Smt2.g | 77 ++++--- src/smt/smt_engine.cpp | 12 +- src/smt/smt_engine.h | 31 +-- src/theory/builtin/kinds | 10 +- .../builtin/theory_builtin_type_rules.h | 27 +++ src/theory/bv/kinds | 12 +- src/theory/uf/kinds | 4 +- src/util/hash.h | 2 + 30 files changed, 956 insertions(+), 337 deletions(-) create mode 100644 src/context/cdmap_forward.h diff --git a/src/context/cdmap.h b/src/context/cdmap.h index 76c05fd4d..1e7e931da 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -92,20 +92,19 @@ #ifndef __CVC4__CONTEXT__CDMAP_H #define __CVC4__CONTEXT__CDMAP_H -#include "context/context.h" -#include "util/Assert.h" - #include #include #include +#include "context/context.h" +#include "util/Assert.h" +#include "context/cdmap_forward.h" + namespace CVC4 { namespace context { // Auxiliary class: almost the same as CDO (see cdo.h) -template > class CDMap; - template > class CDOmap : public ContextObj { friend class CDMap; diff --git a/src/context/cdmap_forward.h b/src/context/cdmap_forward.h new file mode 100644 index 000000000..1024f0b54 --- /dev/null +++ b/src/context/cdmap_forward.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file cdmap_forward.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 This is a forward declaration header to declare the CDMap<> + ** template + ** + ** This is a forward declaration header to declare the CDMap<> + ** template. It's useful if you want to forward-declare CDMap<> + ** without including the full cdmap.h header, for example, in a + ** public header context. + ** + ** For CDMap<> in particular, it's difficult to forward-declare it + ** yourself, becase it has a default template argument. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CONTEXT__CDMAP_FORWARD_H +#define __CVC4__CONTEXT__CDMAP_FORWARD_H + +namespace __gnu_cxx { + template class hash; +}/* __gnu_cxx namespace */ + +namespace CVC4 { + namespace context { + template > + class CDMap; + }/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDMAP_FORWARD_H */ diff --git a/src/context/cdset.h b/src/context/cdset.h index 7032f76ba..47848c26f 100644 --- a/src/context/cdset.h +++ b/src/context/cdset.h @@ -34,6 +34,23 @@ class CDSet : protected CDMap { public: + // ensure these are publicly accessible + static void* operator new(size_t size, bool b) { + return ContextObj::operator new(size, b); + } + + static void operator delete(void* pMem, bool b) { + return ContextObj::operator delete(pMem, b); + } + + void deleteSelf() { + this->ContextObj::deleteSelf(); + } + + static void operator delete(void* pMem) { + AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); + } + CDSet(Context* context) : super(context) { } diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 5f2453898..50ce4141e 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -26,7 +26,8 @@ libexpr_la_SOURCES = \ command.cpp \ declaration_scope.h \ declaration_scope.cpp \ - expr_manager_scope.h + expr_manager_scope.h \ + sort.h nodist_libexpr_la_SOURCES = \ kind.h \ metakind.h \ diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index edc4c5fa8..bd128267a 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -11,69 +11,162 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Convenience class for scoping variable and type declarations (implementation). + ** \brief Convenience class for scoping variable and type + ** declarations (implementation). ** - ** Convenience class for scoping variable and type declarations (implementation) + ** Convenience class for scoping variable and type declarations + ** (implementation). **/ -#include "declaration_scope.h" -#include "expr.h" -#include "type.h" - +#include "expr/declaration_scope.h" +#include "expr/expr.h" +#include "expr/type.h" #include "context/cdmap.h" +#include "context/cdset.h" #include "context/context.h" #include +#include -namespace CVC4 { +using namespace CVC4; +using namespace CVC4::context; +using namespace std; -using namespace context; +namespace CVC4 { DeclarationScope::DeclarationScope() : - d_context(new Context()), - d_exprMap(new (true) CDMap(d_context)), - d_typeMap(new (true) CDMap(d_context)) { + d_context(new Context), + d_exprMap(new(true) CDMap(d_context)), + d_typeMap(new(true) CDMap, Type>, StringHashFunction>(d_context)), + d_functions(new(true) CDSet(d_context)) { } DeclarationScope::~DeclarationScope() { d_exprMap->deleteSelf(); d_typeMap->deleteSelf(); + d_functions->deleteSelf(); delete d_context; } -void DeclarationScope::bind(const std::string& name, const Expr& obj) throw () { - d_exprMap->insert(name,obj); +void DeclarationScope::bind(const std::string& name, Expr obj) throw() { + d_exprMap->insert(name, obj); } -bool DeclarationScope::isBound(const std::string& name) const throw () { +void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj) throw() { + d_exprMap->insert(name, obj); + d_functions->insert(obj); +} + +bool DeclarationScope::isBound(const std::string& name) const throw() { return d_exprMap->find(name) != d_exprMap->end(); } -Expr DeclarationScope::lookup(const std::string& name) const throw () { +bool DeclarationScope::isBoundDefinedFunction(const std::string& name) const throw() { + CDMap::iterator found = + d_exprMap->find(name); + return found != d_exprMap->end() && d_functions->contains((*found).second); +} + +Expr DeclarationScope::lookup(const std::string& name) const throw(AssertionException) { return (*d_exprMap->find(name)).second; } -void DeclarationScope::bindType(const std::string& name, const Type& t) throw () { - d_typeMap->insert(name,t); +void DeclarationScope::bindType(const std::string& name, Type t) throw() { + d_typeMap->insert(name, make_pair(vector(), t)); } -bool DeclarationScope::isBoundType(const std::string& name) const throw () { +void DeclarationScope::bindType(const std::string& name, + const vector& params, + Type t) throw() { + if(Debug.isOn("sort")) { + Debug("sort") << "bindType(" << name << ", ["; + if(params.size() > 0) { + copy( params.begin(), params.end() - 1, + ostream_iterator(Debug("sort"), ", ") ); + Debug("sort") << params.back(); + } + Debug("sort") << "], " << t << ")" << endl; + } + d_typeMap->insert(name, make_pair(params, t)); +} + +bool DeclarationScope::isBoundType(const std::string& name) const throw() { return d_typeMap->find(name) != d_typeMap->end(); } -Type DeclarationScope::lookupType(const std::string& name) const throw () { - return (*d_typeMap->find(name)).second; +Type DeclarationScope::lookupType(const std::string& name) const throw(AssertionException) { + pair, Type> p = (*d_typeMap->find(name)).second; + Assert(p.first.size() == 0, + "type constructor arity is wrong: " + "`%s' requires %u parameters but was provided 0", + name.c_str(), p.first.size()); + return p.second; } +Type DeclarationScope::lookupType(const std::string& name, + const vector& params) const throw(AssertionException) { + pair, Type> p = (*d_typeMap->find(name)).second; + Assert(p.first.size() == params.size(), + "type constructor arity is wrong: " + "`%s' requires %u parameters but was provided %u", + name.c_str(), p.first.size(), params.size()); + if(p.first.size() == 0) { + Assert(p.second.isSort()); + return p.second; + } + if(p.second.isSortConstructor()) { + if(Debug.isOn("sort")) { + Debug("sort") << "instantiating using a sort constructor" << endl; + Debug("sort") << "have formals ["; + copy( p.first.begin(), p.first.end() - 1, + ostream_iterator(Debug("sort"), ", ") ); + Debug("sort") << p.first.back() << "]" << endl + << "parameters ["; + copy( params.begin(), params.end() - 1, + ostream_iterator(Debug("sort"), ", ") ); + Debug("sort") << params.back() << "]" << endl + << "type ctor " << name << endl + << "type is " << p.second << endl; + } + + Type instantiation = + SortConstructorType(p.second).instantiate(params); + + Debug("sort") << "instance is " << instantiation << endl; + + return instantiation; + } else { + Assert(p.second.isSort()); + if(Debug.isOn("sort")) { + Debug("sort") << "instantiating using a sort substitution" << endl; + Debug("sort") << "have formals ["; + copy( p.first.begin(), p.first.end() - 1, + ostream_iterator(Debug("sort"), ", ") ); + Debug("sort") << p.first.back() << "]" << endl + << "parameters ["; + copy( params.begin(), params.end() - 1, + ostream_iterator(Debug("sort"), ", ") ); + Debug("sort") << params.back() << "]" << endl + << "type ctor " << name << endl + << "type is " << p.second << endl; + } + + Type instantiation = p.second.substitute(p.first, params); + + Debug("sort") << "instance is " << instantiation << endl; + + return instantiation; + } +} -void DeclarationScope::popScope() throw (ScopeException) { +void DeclarationScope::popScope() throw(ScopeException) { if( d_context->getLevel() == 0 ) { throw ScopeException(); } d_context->pop(); } -void DeclarationScope::pushScope() throw () { +void DeclarationScope::pushScope() throw() { d_context->push(); } diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 74869bae7..a402a9139 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -19,6 +19,8 @@ #ifndef DECLARATION_SCOPE_H #define DECLARATION_SCOPE_H +#include +#include #include #include "expr/expr.h" @@ -29,16 +31,17 @@ namespace CVC4 { class Type; namespace context { + class Context; -class Context; + template + class CDMap; -template -class CDMap; - -} //namespace context + template + class CDSet; +}/* CVC4::context namespace */ class CVC4_PUBLIC ScopeException : public Exception { -}; +};/* class ScopeException */ /** * A convenience class for handling scoped declarations. Implements the usual @@ -50,10 +53,13 @@ class CVC4_PUBLIC DeclarationScope { context::Context *d_context; /** A map for expressions. */ - context::CDMap *d_exprMap; + context::CDMap *d_exprMap; /** A map for types. */ - context::CDMap *d_typeMap; + context::CDMap, Type>, StringHashFunction> *d_typeMap; + + /** A set of defined functions. */ + context::CDSet *d_functions; public: /** Create a declaration scope. */ @@ -62,68 +68,119 @@ public: /** Destroy a declaration scope. */ ~DeclarationScope(); - /** Bind an expression to a name in the current scope level. - * If name is already bound in the current level, then the + /** + * Bind an expression to a name in the current scope level. If + * name is already bound in the current level, then the * binding is replaced. If name is bound in a previous - * level, then the binding is "covered" by this one until the current - * scope is popped. + * level, then the binding is "covered" by this one until the + * current scope is popped. * * @param name an identifier * @param obj the expression to bind to name */ - void bind(const std::string& name, const Expr& obj) throw (); - - /** Bind a type to a name in the current scope. - * If name is already bound to a type in the current level, - * then the binding is replaced. If name is bound in a - * previous level, then the binding is "covered" by this one until the - * current scope is popped. + void bind(const std::string& name, Expr obj) throw(); + + /** + * Bind a type to a name in the current scope. If name + * is already bound to a type in the current level, then the binding + * is replaced. If name is bound in a previous level, + * then the binding is "covered" by this one until the current scope + * is popped. + * + * @param name an identifier + * @param t the type to bind to name + */ + void bindDefinedFunction(const std::string& name, Expr obj) throw(); + + /** + * Bind a type to a name in the current scope. If name + * is already bound to a type in the current level, then the binding + * is replaced. If name is bound in a previous level, + * then the binding is "covered" by this one until the current scope + * is popped. + * + * @param name an identifier + * @param t the type to bind to name + */ + void bindType(const std::string& name, Type t) throw(); + + /** + * Bind a type to a name in the current scope. If name + * is already bound to a type or type constructor in the current + * level, then the binding is replaced. If name is + * bound in a previous level, then the binding is "covered" by this + * one until the current scope is popped. * * @param name an identifier * @param t the type to bind to name */ - void bindType(const std::string& name, const Type& t) throw (); + void bindType(const std::string& name, + const std::vector& params, + Type t) throw(); - /** Check whether a name is bound to an expression. + /** + * Check whether a name is bound to an expression with either bind() + * or bindDefinedFunction(). * * @param name the identifier to check. * @returns true iff name is bound in the current scope. */ - bool isBound(const std::string& name) const throw (); + bool isBound(const std::string& name) const throw(); + + /** + * Check whether a name was bound to a function with bindDefinedFunction(). + */ + bool isBoundDefinedFunction(const std::string& name) const throw(); - /** Check whether a name is bound to a type. + /** + * Check whether a name is bound to a type (or type constructor). * * @param name the identifier to check. * @returns true iff name is bound to a type in the current scope. */ - bool isBoundType(const std::string& name) const throw (); + bool isBoundType(const std::string& name) const throw(); - /** Lookup a bound expression. + /** + * Lookup a bound expression. * * @param name the identifier to lookup * @returns the expression bound to name in the current scope. */ - Expr lookup(const std::string& name) const throw (); + Expr lookup(const std::string& name) const throw(AssertionException); - /** Lookup a bound type. + /** + * Lookup a bound type. * - * @param name the identifier to lookup + * @param name the type identifier to lookup * @returns the type bound to name in the current scope. */ - Type lookupType(const std::string& name) const throw (); + Type lookupType(const std::string& name) const throw(AssertionException); - /** Pop a scope level. Deletes all bindings since the last call to + /** + * Lookup a bound parameterized type. + * + * @param name the type-constructor identifier to lookup + * @param params the types to use to parameterize the type + * @returns the type bound to name(params) in + * the current scope. + */ + Type lookupType(const std::string& name, + const std::vector& params) const throw(AssertionException); + + /** + * Pop a scope level. Deletes all bindings since the last call to * pushScope. Calls to pushScope and * popScope must be "properly nested." I.e., a call to * popScope is only legal if the number of prior calls to * pushScope on this DeclarationScope is strictly * greater than then number of prior calls to popScope. */ - void popScope() throw (ScopeException); + void popScope() throw(ScopeException); /** Push a scope level. */ - void pushScope() throw (); + void pushScope() throw(); + };/* class DeclarationScope */ -}/* namespace CVC4 */ +}/* CVC4 namespace */ #endif /* DECLARATION_SCOPE_H */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 56b89c125..55b59d13c 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -88,11 +88,11 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { - return Expr(this, d_nodeManager->mkNodePtr(kind, + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), child2.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), + throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); } } @@ -107,12 +107,12 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { - return Expr(this, d_nodeManager->mkNodePtr(kind, - child1.getNode(), - child2.getNode(), + return Expr(this, d_nodeManager->mkNodePtr(kind, + child1.getNode(), + child2.getNode(), child3.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), + throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); } } @@ -127,13 +127,13 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { - return Expr(this, d_nodeManager->mkNodePtr(kind, + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), - child2.getNode(), + child2.getNode(), child3.getNode(), child4.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), + throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); } } @@ -149,14 +149,14 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { - return Expr(this, d_nodeManager->mkNodePtr(kind, + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), - child2.getNode(), + child2.getNode(), child3.getNode(), child4.getNode(), child5.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), + throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); } } @@ -181,7 +181,7 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector& children) { try { return Expr(this, d_nodeManager->mkNodePtr(kind, nodes)); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), + throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); } } @@ -219,8 +219,8 @@ FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) /** Make a function type with input types from argTypes. */ FunctionType ExprManager::mkFunctionType(const std::vector& argTypes, const Type& range) { - Assert( argTypes.size() >= 1 ); NodeManagerScope nms(d_nodeManager); + Assert( argTypes.size() >= 1 ); std::vector argTypeNodes; for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) { argTypeNodes.push_back(*argTypes[i].d_typeNode); @@ -229,8 +229,8 @@ FunctionType ExprManager::mkFunctionType(const std::vector& argTypes, cons } FunctionType ExprManager::mkFunctionType(const std::vector& sorts) { - Assert( sorts.size() >= 2 ); NodeManagerScope nms(d_nodeManager); + Assert( sorts.size() >= 2 ); std::vector sortNodes; for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { sortNodes.push_back(*sorts[i].d_typeNode); @@ -239,8 +239,8 @@ FunctionType ExprManager::mkFunctionType(const std::vector& sorts) { } FunctionType ExprManager::mkPredicateType(const std::vector& sorts) { - Assert( sorts.size() >= 1 ); NodeManagerScope nms(d_nodeManager); + Assert( sorts.size() >= 1 ); std::vector sortNodes; for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { sortNodes.push_back(*sorts[i].d_typeNode); @@ -249,8 +249,8 @@ FunctionType ExprManager::mkPredicateType(const std::vector& sorts) { } TupleType ExprManager::mkTupleType(const std::vector& types) { - Assert( types.size() >= 2 ); NodeManagerScope nms(d_nodeManager); + Assert( types.size() >= 2 ); std::vector typeNodes; for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { typeNodes.push_back(*types[i].d_typeNode); @@ -268,9 +268,16 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))); } -SortType ExprManager::mkSort(const std::string& name, size_t arity) const { +SortType ExprManager::mkSort(const std::string& name) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))); +} + +SortConstructorType ExprManager::mkSortConstructor(const std::string& name, + size_t arity) const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, arity))); + return Type(d_nodeManager, + new TypeNode(d_nodeManager->mkSortConstructor(name, arity))); } /** @@ -295,7 +302,7 @@ SortType ExprManager::mkSort(const std::string& name, size_t arity) const { * amount of checking required to return a valid result. * * @param n the Expr for which we want a type - * @param check whether we should check the type as we compute it + * @param check whether we should check the type as we compute it * (default: false) */ Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingException) { @@ -333,7 +340,7 @@ Expr ExprManager::mkAssociative(Kind kind, /* If the number of children is within bounds, then there's nothing to do. */ if( numChildren <= max ) { return mkExpr(kind,children); - } + } std::vector::const_iterator it = children.begin() ; std::vector::const_iterator end = children.end() ; @@ -379,7 +386,7 @@ Expr ExprManager::mkAssociative(Kind kind, /* It would be really weird if this happened (it would require * min > 2, for one thing), but let's make sure. */ - AlwaysAssert( newChildren.size() >= min, + AlwaysAssert( newChildren.size() >= min, "Too few new children in mkAssociative" ); return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) ); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 316a9b7b1..92d039bd3 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -173,7 +173,8 @@ public: template Expr mkConst(const T&); - /** Create an Expr by applying an associative operator to the children. + /** + * Create an Expr by applying an associative operator to the children. * If children.size() is greater than the max arity for * kind, then the expression will be broken up into * suitably-sized chunks, taking advantage of the associativity of @@ -224,8 +225,16 @@ public: /** Make the type of arrays with the given parameterization */ ArrayType mkArrayType(Type indexType, Type constituentType) const; - /** Make a new sort with the given name and arity. */ - SortType mkSort(const std::string& name, size_t arity = 0) const; + /** Make a new sort with the given name. */ + SortType mkSort(const std::string& name) const; + + /** Make a new sort from a constructor */ + SortType mkSort(SortConstructorType constructor, + const std::vector& children) const; + + /** Make a sort constructor from a name and arity */ + SortConstructorType mkSortConstructor(const std::string& name, + size_t arity) const; /** Get the type of an expression */ Type getType(const Expr& e, bool check = false) diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 83d5dc47f..803808b0f 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -151,6 +151,12 @@ bool Expr::operator>(const Expr& e) const { return *d_node > *e.d_node; } +unsigned Expr::getId() const { + ExprManagerScope ems(*this); + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + return d_node->getId(); +} + Kind Expr::getKind() const { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index fee8e70db..8fab13b37 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -75,6 +75,7 @@ public: /** * Get the Expr that caused the type-checking to fail. + * * @return the expr */ Expr getExpression() const; @@ -103,6 +104,7 @@ protected: /** * Constructor for internal purposes. + * * @param em the expression manager that handles this expression * @param node the actual expression node pointer */ @@ -115,6 +117,7 @@ public: /** * Copy constructor, makes a copy of a given expression + * * @param e the expression to copy */ Expr(const Expr& e); @@ -134,6 +137,7 @@ public: * Assignment operator, makes a copy of the given expression. If the * expression managers of the two expressions differ, the expression of * the given expression will be used. + * * @param e the expression to assign * @return the reference to this expression after assignment */ @@ -142,13 +146,15 @@ public: /** * Syntactic comparison operator. Returns true if expressions belong to the * same expression manager and are syntactically identical. + * * @param e the expression to compare to * @return true if expressions are syntactically the same, false otherwise */ bool operator==(const Expr& e) const; /** - * Syntactic dis-equality operator. + * Syntactic disequality operator. + * * @param e the expression to compare to * @return true if expressions differ syntactically, false otherwise */ @@ -160,6 +166,7 @@ public: * ordering than all the expressions created later. Null expression is the * smallest element of the ordering. The behavior of the operator is * undefined if the expressions come from two different expression managers. + * * @param e the expression to compare to * @return true if this expression is smaller than the given one */ @@ -171,6 +178,7 @@ public: * ordering than all the expressions created later. Null expression is the * smallest element of the ordering. The behavior of the operator is * undefined if the expressions come from two different expression managers. + * * @param e the expression to compare to * @return true if this expression is greater than the given one */ @@ -182,6 +190,7 @@ public: * ordering than all the expressions created later. Null expression is the * smallest element of the ordering. The behavior of the operator is * undefined if the expressions come from two different expression managers. + * * @param e the expression to compare to * @return true if this expression is smaller or equal to the given one */ @@ -193,25 +202,37 @@ public: * ordering than all the expressions created later. Null expression is the * smallest element of the ordering. The behavior of the operator is * undefined if the expressions come from two different expression managers. + * * @param e the expression to compare to * @return true if this expression is greater or equal to the given one */ bool operator>=(const Expr& e) const { return !(*this < e); } + /** + * Get the ID of this expression (used for the comparison operators). + * + * @return an identifier uniquely identifying the value this + * expression holds. + */ + unsigned getId() const; + /** * Returns the kind of the expression (AND, PLUS ...). + * * @return the kind of the expression */ Kind getKind() const; /** * Returns the number of children of this expression. + * * @return the number of children */ size_t getNumChildren() const; /** * Returns the i'th child of this expression. + * * @param i the index of the child to retrieve * @return the child */ @@ -219,12 +240,14 @@ public: /** * Check if this is an expression that has an operator. + * * @return true if this expression has an operator */ bool hasOperator() const; /** * Get the operator of this expression. + * * @throws IllegalArgumentException if it has no operator * @return the operator of this expression */ @@ -599,6 +622,13 @@ inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) { }/* CVC4::expr namespace */ +// for hash_maps, hash_sets.. +struct ExprHashFunction { + size_t operator()(CVC4::Expr e) const { + return (size_t) e.getId(); + } +};/* struct ExprHashFunction */ + }/* CVC4 namespace */ #endif /* __CVC4__EXPR_H */ diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 89e2861d6..aaecff800 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -227,7 +227,7 @@ function register_metakind { exit 1 fi - if [ $mk = OPERATOR -o $mk = PARAMETERIZED ]; then + if [ $mk = OPERATOR ] || [ $mk = PARAMETERIZED -a "$k" != SORT_TYPE ]; then if [ $lb = 0 ]; then echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2 exit 1 diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 6b689034a..d9933689d 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -25,17 +25,18 @@ using namespace std; namespace CVC4 { -TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, std::string message) -: Exception(message), d_node(new Node(node)) -{ +TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, + string message) : + Exception(message), + d_node(new Node(node)) { } TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () { delete d_node; } -std::string TypeCheckingExceptionPrivate::toString() const { - std::stringstream ss; +string TypeCheckingExceptionPrivate::toString() const { + stringstream ss; ss << "Error type-checking " << d_node << ": " << d_msg; return ss.str(); } diff --git a/src/expr/node.h b/src/expr/node.h index b5f6307ed..67d46a977 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -342,11 +342,14 @@ public: /** * Returns a node representing the operator of this expression. * If this is an APPLY, then the operator will be a functional term. - * Otherwise, it will be a node with kind BUILTIN + * Otherwise, it will be a node with kind BUILTIN. */ NodeTemplate getOperator() const; - /** Returns true if the node has an operator (i.e., it's not a variable or a constant). */ + /** + * Returns true if the node has an operator (i.e., it's not a + * variable or a constant). + */ inline bool hasOperator() const; /** @@ -721,14 +724,14 @@ struct NodeHashFunction { size_t operator()(const CVC4::Node& node) const { return (size_t) node.getId(); } -}; +};/* struct NodeHashFunction */ // for hash_maps, hash_sets.. struct TNodeHashFunction { size_t operator()(CVC4::TNode node) const { return (size_t) node.getId(); } -}; +};/* struct TNodeHashFunction */ template inline size_t NodeTemplate::getNumChildren() const { @@ -976,7 +979,7 @@ NodeTemplate::printAst(std::ostream& out, int indent) const { /** * Returns a node representing the operator of this expression. * If this is an APPLY, then the operator will be a functional term. - * Otherwise, it will be a node with kind BUILTIN + * Otherwise, it will be a node with kind BUILTIN. */ template NodeTemplate NodeTemplate::getOperator() const { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 942906fbd..4653ee95f 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -198,6 +198,9 @@ TypeNode NodeManager::getType(TNode n, bool check) case kind::SORT_TYPE: typeNode = kindType(); break; + case kind::APPLY: + typeNode = CVC4::theory::builtin::ApplyTypeRule::computeType(this, n, check); + break; case kind::EQUAL: typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n, check); break; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index ca93473db..c0f489d7a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -48,9 +48,11 @@ namespace expr { // TODO: hide this attribute behind a NodeManager interface. namespace attr { struct VarNameTag {}; + struct SortArityTag {}; }/* CVC4::expr::attr namespace */ typedef expr::Attribute VarNameAttr; +typedef expr::Attribute SortArityAttr; }/* CVC4::expr namespace */ @@ -508,7 +510,14 @@ public: inline TypeNode mkSort(); /** Make a new sort with the given name and arity. */ - inline TypeNode mkSort(const std::string& name, size_t arity = 0); + inline TypeNode mkSort(const std::string& name); + + /** Make a new sort with the given name and arity. */ + inline TypeNode mkSort(TypeNode constructor, + const std::vector& children); + + /** Make a new sort with the given name and arity. */ + inline TypeNode mkSortConstructor(const std::string& name, size_t arity); /** * Get the type for the given node and optionally do type checking. @@ -762,16 +771,55 @@ inline bool NodeManager::hasOperator(Kind k) { } inline TypeNode NodeManager::mkSort() { - return NodeBuilder<0>(this, kind::SORT_TYPE).constructTypeNode(); + NodeBuilder<1> nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); + nb << sortTag; + return nb.constructTypeNode(); } -inline TypeNode NodeManager::mkSort(const std::string& name, size_t arity) { - Assert(arity == 0, "parameterized sorts not yet supported."); +inline TypeNode NodeManager::mkSort(const std::string& name) { TypeNode type = mkSort(); type.setAttribute(expr::VarNameAttr(), name); return type; } +inline TypeNode NodeManager::mkSort(TypeNode constructor, + const std::vector& children) { + Assert(constructor.getKind() == kind::SORT_TYPE && + constructor.getNumChildren() == 0, + "expected a sort constructor"); + Assert(children.size() > 0, "expected non-zero # of children"); + uint64_t arity; + std::string name; + bool hasArityAttribute = + getAttribute(constructor.d_nv, expr::SortArityAttr(), arity); + Assert(hasArityAttribute, "expected a sort constructor"); + bool hasNameAttribute = + getAttribute(constructor.d_nv, expr::VarNameAttr(), name); + Assert(hasNameAttribute, "expected a sort constructor"); + Assert(arity == children.size(), + "arity mismatch in application of sort constructor"); + NodeBuilder<> nb(this, kind::SORT_TYPE); + Node sortTag = Node(constructor.d_nv->d_children[0]); + nb << sortTag; + nb.append(children); + TypeNode type = nb.constructTypeNode(); + type.setAttribute(expr::VarNameAttr(), name); + return type; +} + +inline TypeNode NodeManager::mkSortConstructor(const std::string& name, + size_t arity) { + Assert(arity > 0); + NodeBuilder<> nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); + nb << sortTag; + TypeNode type = nb.constructTypeNode(); + type.setAttribute(expr::VarNameAttr(), name); + type.setAttribute(expr::SortArityAttr(), arity); + return type; +} + inline Node NodeManager::mkNode(Kind kind, TNode child1) { NodeBuilder<1> nb(this, kind); nb << child1; @@ -832,7 +880,7 @@ inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, - TNode child3, TNode child4, TNode child5) { + TNode child3, TNode child4, TNode child5) { NodeBuilder<5> nb(this, kind); nb << child1 << child2 << child3 << child4 << child5; return nb.constructNodePtr(); diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 43325d6cc..05b69f6f4 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -11,21 +11,25 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Implementation of expression types . + ** \brief Implementation of expression types ** - ** Implementation of expression types + ** Implementation of expression types. **/ +#include #include +#include #include "expr/node_manager.h" #include "expr/type.h" #include "expr/type_node.h" #include "util/Assert.h" +using namespace std; + namespace CVC4 { -std::ostream& operator<<(std::ostream& out, const Type& e) { +ostream& operator<<(ostream& out, const Type& e) { e.toStream(out); return out; } @@ -34,8 +38,8 @@ Type Type::makeType(const TypeNode& typeNode) const { return Type(d_nodeManager, new TypeNode(typeNode)); } -Type::Type(NodeManager* nm, TypeNode* node) -: d_typeNode(node), +Type::Type(NodeManager* nm, TypeNode* node) : + d_typeNode(node), d_nodeManager(nm) { } @@ -44,22 +48,20 @@ Type::~Type() { delete d_typeNode; } -Type::Type() -: d_typeNode(new TypeNode()), - d_nodeManager(NULL) -{ +Type::Type() : + d_typeNode(new TypeNode), + d_nodeManager(NULL) { } -Type::Type(uintptr_t n) -: d_typeNode(new TypeNode()), +Type::Type(uintptr_t n) : + d_typeNode(new TypeNode), d_nodeManager(NULL) { AlwaysAssert(n == 0); } -Type::Type(const Type& t) -: d_typeNode(new TypeNode(*t.d_typeNode)), - d_nodeManager(t.d_nodeManager) -{ +Type::Type(const Type& t) : + d_typeNode(new TypeNode(*t.d_typeNode)), + d_nodeManager(t.d_nodeManager) { } bool Type::isNull() const { @@ -68,7 +70,7 @@ bool Type::isNull() const { Type& Type::operator=(const Type& t) { NodeManagerScope nms(d_nodeManager); - if (this != &t) { + if(this != &t) { *d_typeNode = *t.d_typeNode; d_nodeManager = t.d_nodeManager; } @@ -83,7 +85,36 @@ bool Type::operator!=(const Type& t) const { return *d_typeNode != *t.d_typeNode; } -void Type::toStream(std::ostream& out) const { +Type Type::substitute(const Type& type, const Type& replacement) const { + NodeManagerScope nms(d_nodeManager); + return makeType(d_typeNode->substitute(*type.d_typeNode, + *replacement.d_typeNode)); +} + +Type Type::substitute(const vector& types, + const vector& replacements) const { + NodeManagerScope nms(d_nodeManager); + + vector typesNodes, replacementsNodes; + + for(vector::const_iterator i = types.begin(), + iend = types.end(); + i != iend; + ++i) { + typesNodes.push_back(*(*i).d_typeNode); + } + + for(vector::const_iterator i = replacements.begin(), + iend = replacements.end(); + i != iend; + ++i) { + replacementsNodes.push_back(*(*i).d_typeNode); + } + + return makeType(d_typeNode->substitute(typesNodes, replacementsNodes)); +} + +void Type::toStream(ostream& out) const { NodeManagerScope nms(d_nodeManager); out << *d_typeNode; return; @@ -96,7 +127,7 @@ bool Type::isBoolean() const { } /** Cast to a Boolean type */ -Type::operator BooleanType() const throw (AssertionException) { +Type::operator BooleanType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isBoolean()); return BooleanType(*this); @@ -109,7 +140,7 @@ bool Type::isInteger() const { } /** Cast to a integer type */ -Type::operator IntegerType() const throw (AssertionException) { +Type::operator IntegerType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isInteger()); return IntegerType(*this); @@ -122,7 +153,7 @@ bool Type::isReal() const { } /** Cast to a real type */ -Type::operator RealType() const throw (AssertionException) { +Type::operator RealType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isReal()); return RealType(*this); @@ -135,7 +166,7 @@ bool Type::isBitVector() const { } /** Cast to a bit-vector type */ -Type::operator BitVectorType() const throw (AssertionException) { +Type::operator BitVectorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isBitVector()); return BitVectorType(*this); @@ -157,7 +188,7 @@ bool Type::isPredicate() const { } /** Cast to a function type */ -Type::operator FunctionType() const throw (AssertionException) { +Type::operator FunctionType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isFunction()); return FunctionType(*this); @@ -170,7 +201,7 @@ bool Type::isTuple() const { } /** Cast to a tuple type */ -Type::operator TupleType() const throw (AssertionException) { +Type::operator TupleType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isTuple()); return TupleType(*this); @@ -183,7 +214,7 @@ bool Type::isArray() const { } /** Cast to an array type */ -Type::operator ArrayType() const throw (AssertionException) { +Type::operator ArrayType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); return ArrayType(*this); } @@ -195,12 +226,25 @@ bool Type::isSort() const { } /** Cast to a sort type */ -Type::operator SortType() const throw (AssertionException) { +Type::operator SortType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isSort()); return SortType(*this); } +/** Is this a sort constructor kind */ +bool Type::isSortConstructor() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isSortConstructor(); +} + +/** Cast to a sort type */ +Type::operator SortConstructorType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isSortConstructor()); + return SortConstructorType(*this); +} + /** Is this a kind type (i.e., the type of a type)? */ bool Type::isKind() const { NodeManagerScope nms(d_nodeManager); @@ -208,18 +252,18 @@ bool Type::isKind() const { } /** Cast to a kind type */ -Type::operator KindType() const throw (AssertionException) { +Type::operator KindType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isKind()); return KindType(*this); } -std::vector FunctionType::getArgTypes() const { +vector FunctionType::getArgTypes() const { NodeManagerScope nms(d_nodeManager); - std::vector args; - std::vector argNodes = d_typeNode->getArgTypes(); - std::vector::iterator it = argNodes.begin(); - std::vector::iterator it_end = argNodes.end(); + vector args; + vector argNodes = d_typeNode->getArgTypes(); + vector::iterator it = argNodes.begin(); + vector::iterator it_end = argNodes.end(); for(; it != it_end; ++ it) { args.push_back(makeType(*it)); } @@ -232,77 +276,96 @@ Type FunctionType::getRangeType() const { return makeType(d_typeNode->getRangeType()); } -std::vector TupleType::getTypes() const { +vector TupleType::getTypes() const { NodeManagerScope nms(d_nodeManager); - std::vector types; - std::vector typeNodes = d_typeNode->getTupleTypes(); - std::vector::iterator it = typeNodes.begin(); - std::vector::iterator it_end = typeNodes.end(); + vector types; + vector typeNodes = d_typeNode->getTupleTypes(); + vector::iterator it = typeNodes.begin(); + vector::iterator it_end = typeNodes.end(); for(; it != it_end; ++ it) { types.push_back(makeType(*it)); } return types; } -std::string SortType::getName() const { +string SortType::getName() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->getAttribute(expr::VarNameAttr()); } -BooleanType::BooleanType(const Type& t) throw (AssertionException) -: Type(t) -{ +string SortConstructorType::getName() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getAttribute(expr::VarNameAttr()); +} + +size_t SortConstructorType::getArity() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getAttribute(expr::SortArityAttr()); +} + +SortType SortConstructorType::instantiate(const vector& params) const { + NodeManagerScope nms(d_nodeManager); + vector paramsNodes; + for(vector::const_iterator i = params.begin(), + iend = params.end(); + i != iend; + ++i) { + paramsNodes.push_back(*getTypeNode(*i)); + } + return SortType(makeType(d_nodeManager->mkSort(*d_typeNode, paramsNodes))); +} + +BooleanType::BooleanType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isBoolean()); } -IntegerType::IntegerType(const Type& t) throw (AssertionException) -: Type(t) -{ +IntegerType::IntegerType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isInteger()); } -RealType::RealType(const Type& t) throw (AssertionException) -: Type(t) -{ +RealType::RealType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isReal()); } -BitVectorType::BitVectorType(const Type& t) throw (AssertionException) -: Type(t) -{ +BitVectorType::BitVectorType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isBitVector()); } -FunctionType::FunctionType(const Type& t) throw (AssertionException) -: Type(t) -{ +FunctionType::FunctionType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isFunction()); } -TupleType::TupleType(const Type& t) throw (AssertionException) -: Type(t) -{ +TupleType::TupleType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isTuple()); } -ArrayType::ArrayType(const Type& t) throw (AssertionException) -: Type(t) -{ +ArrayType::ArrayType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isArray()); } -KindType::KindType(const Type& t) throw (AssertionException) -: Type(t) -{ +KindType::KindType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isKind()); } -SortType::SortType(const Type& t) throw (AssertionException) -: Type(t) -{ +SortType::SortType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isSort()); } +SortConstructorType::SortConstructorType(const Type& t) + throw(AssertionException) : + Type(t) { + Assert(isSortConstructor()); +} + unsigned BitVectorType::getSize() const { return d_typeNode->getBitVectorSize(); } diff --git a/src/expr/type.h b/src/expr/type.h index 3e3fbd368..57ec3bf5c 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -46,6 +46,7 @@ class FunctionType; class TupleType; class KindType; class SortType; +class SortConstructorType; class Type; /** Strategy for hashing Types */ @@ -85,6 +86,9 @@ protected: */ Type(NodeManager* em, TypeNode* typeNode); + /** Accessor for derived classes */ + static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; } + public: /** @@ -113,6 +117,17 @@ public: */ bool isNull() const; + /** + * Substitution of Types. + */ + Type substitute(const Type& type, const Type& replacement) const; + + /** + * Simultaneous substitution of Types. + */ + Type substitute(const std::vector& types, + const std::vector& replacements) const; + /** * Assignment operator. * @param t the type to assign to this type @@ -144,7 +159,7 @@ public: * Cast this type to a Boolean type * @return the BooleanType */ - operator BooleanType() const throw (AssertionException); + operator BooleanType() const throw(AssertionException); /** * Is this the integer type? @@ -156,7 +171,7 @@ public: * Cast this type to a integer type * @return the IntegerType */ - operator IntegerType() const throw (AssertionException); + operator IntegerType() const throw(AssertionException); /** * Is this the real type? @@ -168,7 +183,7 @@ public: * Cast this type to a real type * @return the RealType */ - operator RealType() const throw (AssertionException); + operator RealType() const throw(AssertionException); /** * Is this the bit-vector type? @@ -180,7 +195,7 @@ public: * Cast this type to a bit-vector type * @return the BitVectorType */ - operator BitVectorType() const throw (AssertionException); + operator BitVectorType() const throw(AssertionException); /** * Is this a function type? @@ -199,7 +214,7 @@ public: * Cast this type to a function type * @return the FunctionType */ - operator FunctionType() const throw (AssertionException); + operator FunctionType() const throw(AssertionException); /** * Is this a tuple type? @@ -211,7 +226,7 @@ public: * Cast this type to a tuple type * @return the TupleType */ - operator TupleType() const throw (AssertionException); + operator TupleType() const throw(AssertionException); /** * Is this an array type? @@ -223,7 +238,7 @@ public: * Cast this type to an array type * @return the ArrayType */ - operator ArrayType() const throw (AssertionException); + operator ArrayType() const throw(AssertionException); /** * Is this a sort kind? @@ -233,9 +248,21 @@ public: /** * Cast this type to a sort type - * @return the function Type + * @return the sort type + */ + operator SortType() const throw(AssertionException); + + /** + * Is this a sort constructor kind? + * @return true if this is a sort constructor kind + */ + bool isSortConstructor() const; + + /** + * Cast this type to a sort constructor type + * @return the sort constructor type */ - operator SortType() const throw (AssertionException); + operator SortConstructorType() const throw(AssertionException); /** * Is this a kind type (i.e., the type of a type)? @@ -247,7 +274,7 @@ public: * Cast to a kind type * @return the kind type */ - operator KindType() const throw (AssertionException); + operator KindType() const throw(AssertionException); /** * Outputs a string representation of this type to the stream. @@ -264,7 +291,7 @@ class CVC4_PUBLIC BooleanType : public Type { public: /** Construct from the base type */ - BooleanType(const Type& type) throw (AssertionException); + BooleanType(const Type& type) throw(AssertionException); }; /** @@ -275,7 +302,7 @@ class CVC4_PUBLIC IntegerType : public Type { public: /** Construct from the base type */ - IntegerType(const Type& type) throw (AssertionException); + IntegerType(const Type& type) throw(AssertionException); }; /** @@ -286,7 +313,7 @@ class CVC4_PUBLIC RealType : public Type { public: /** Construct from the base type */ - RealType(const Type& type) throw (AssertionException); + RealType(const Type& type) throw(AssertionException); }; @@ -298,7 +325,7 @@ class CVC4_PUBLIC FunctionType : public Type { public: /** Construct from the base type */ - FunctionType(const Type& type) throw (AssertionException); + FunctionType(const Type& type) throw(AssertionException); /** Get the argument types */ std::vector getArgTypes() const; @@ -315,7 +342,7 @@ class CVC4_PUBLIC TupleType : public Type { public: /** Construct from the base type */ - TupleType(const Type& type) throw (AssertionException); + TupleType(const Type& type) throw(AssertionException); /** Get the constituent types */ std::vector getTypes() const; @@ -329,7 +356,7 @@ class CVC4_PUBLIC ArrayType : public Type { public: /** Construct from the base type */ - ArrayType(const Type& type) throw (AssertionException); + ArrayType(const Type& type) throw(AssertionException); /** Get the index type */ Type getIndexType() const; @@ -346,12 +373,32 @@ class CVC4_PUBLIC SortType : public Type { public: /** Construct from the base type */ - SortType(const Type& type) throw (AssertionException); + SortType(const Type& type) throw(AssertionException); /** Get the name of the sort */ std::string getName() const; }; +/** + * Class encapsulating a user-defined sort constructor. + */ +class CVC4_PUBLIC SortConstructorType : public Type { + +public: + + /** Construct from the base type */ + SortConstructorType(const Type& type) throw(AssertionException); + + /** Get the name of the sort constructor */ + std::string getName() const; + + /** Get the arity of the sort constructor */ + size_t getArity() const; + + /** Instantiate a sort using this sort constructor */ + SortType instantiate(const std::vector& params) const; +}; + /** * Class encapsulating the kind type (the type of types). */ @@ -360,7 +407,7 @@ class CVC4_PUBLIC KindType : public Type { public: /** Construct from the base type */ - KindType(const Type& type) throw (AssertionException); + KindType(const Type& type) throw(AssertionException); }; @@ -372,7 +419,7 @@ class CVC4_PUBLIC BitVectorType : public Type { public: /** Construct from the base type */ - BitVectorType(const Type& type) throw (AssertionException); + BitVectorType(const Type& type) throw(AssertionException); /** * Returns the size of the bit-vector type. @@ -384,7 +431,7 @@ public: /** * Output operator for types * @param out the stream to output to - * @param e the type to output + * @param t the type to output * @return the stream */ std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 94213d941..a55c05c5a 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -16,23 +16,67 @@ ** Reference-counted encapsulation of a pointer to node information. **/ +#include + #include "expr/type_node.h" +using namespace std; + namespace CVC4 { -TypeNode TypeNode::s_null(&expr::NodeValue::s_null); +TypeNode TypeNode::s_null( &expr::NodeValue::s_null ); + +TypeNode TypeNode::substitute(const TypeNode& type, + const TypeNode& replacement) const { + 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) { + if(*i == type) { + nb << replacement; + } else { + (*i).substitute(type, replacement); + } + } + 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; + return getKind() == kind::TYPE_CONSTANT && + getConst() == BOOLEAN_TYPE; } bool TypeNode::isInteger() const { - return getKind() == kind::TYPE_CONSTANT && getConst() == INTEGER_TYPE; + return getKind() == kind::TYPE_CONSTANT && + getConst() == INTEGER_TYPE; } bool TypeNode::isReal() const { return getKind() == kind::TYPE_CONSTANT - && (getConst() == REAL_TYPE || getConst() == INTEGER_TYPE); + && ( getConst() == REAL_TYPE || + getConst() == INTEGER_TYPE ); } bool TypeNode::isArray() const { @@ -60,10 +104,10 @@ bool TypeNode::isPredicate() const { return isFunction() && getRangeType().isBoolean(); } -std::vector TypeNode::getArgTypes() const { +vector TypeNode::getArgTypes() const { Assert(isFunction()); - std::vector args; - for (unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { + vector args; + for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { args.push_back((*this)[i]); } return args; @@ -80,10 +124,10 @@ bool TypeNode::isTuple() const { } /** Is this a tuple type? */ -std::vector TypeNode::getTupleTypes() const { +vector TypeNode::getTupleTypes() const { Assert(isTuple()); - std::vector types; - for (unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) { + vector types; + for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) { types.push_back((*this)[i]); } return types; @@ -91,12 +135,18 @@ std::vector TypeNode::getTupleTypes() const { /** Is this a sort kind */ bool TypeNode::isSort() const { - return getKind() == kind::SORT_TYPE; + return getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()); +} + +/** Is this a sort constructor kind */ +bool TypeNode::isSortConstructor() const { + return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); } /** Is this a kind type (i.e., the type of a type)? */ bool TypeNode::isKind() const { - return getKind() == kind::TYPE_CONSTANT && getConst() == KIND_TYPE; + return getKind() == kind::TYPE_CONSTANT && + getConst() == KIND_TYPE; } /** Is this a bit-vector type */ @@ -106,7 +156,8 @@ bool TypeNode::isBitVector() const { /** Is this a bit-vector type of size size */ bool TypeNode::isBitVector(unsigned size) const { - return getKind() == kind::BITVECTOR_TYPE && getConst() == size; + return getKind() == kind::BITVECTOR_TYPE && + getConst() == size; } /** Get the size of this bit-vector type */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 30359495f..6780b08f7 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -70,9 +70,9 @@ class TypeNode { friend class NodeBuilder; /** - * Assigns the expression value and does reference counting. No assumptions - * are made on the expression, and should only be used if we know what we - * are doing. + * Assigns the expression value and does reference counting. No + * assumptions are made on the expression, and should only be used + * if we know what we are doing. * * @param ev the expression value to assign */ @@ -86,41 +86,56 @@ public: /** Copy constructor */ TypeNode(const TypeNode& node); + /** + * Destructor. If ref_count is true it will decrement the reference count + * and, if zero, collect the NodeValue. + */ + ~TypeNode() throw(AssertionException); + /** * Assignment operator for nodes, copies the relevant information from node * to this node. + * * @param node the node to copy * @return reference to this node */ TypeNode& operator=(const TypeNode& typeNode); - /** - * Destructor. If ref_count is true it will decrement the reference count - * and, if zero, collect the NodeValue. - */ - ~TypeNode() throw(AssertionException); - /** * Return the null node. + * * @return the null node */ static TypeNode null() { return s_null; } + /** + * Substitution of TypeNodes. + */ + TypeNode substitute(const TypeNode& type, const TypeNode& replacement) const; + + /** + * Simultaneous substitution of TypeNodes. + */ + TypeNode substitute(const std::vector& types, + const std::vector& replacements) const; + /** * Structural comparison operator for expressions. + * * @param typeNode the type node to compare to * @return true if expressions are equal, false otherwise */ bool operator==(const TypeNode& typeNode) const { return - d_nv == typeNode.d_nv - || (typeNode.isReal() && this->isReal()); + d_nv == typeNode.d_nv || + (typeNode.isReal() && this->isReal()); } /** * Structural comparison operator for expressions. + * * @param typeNode the type node to compare to * @return true if expressions are equal, false otherwise */ @@ -131,6 +146,7 @@ public: /** * We compare by expression ids so, keeping things deterministic and having * that subexpressions have to be smaller than the enclosing expressions. + * * @param node the node to compare to * @return true if this expression is smaller */ @@ -140,23 +156,26 @@ public: /** * Returns the i-th child of this node. + * * @param i the index of the child * @return the node representing the i-th child */ - TypeNode operator[](int i) const { + inline TypeNode operator[](int i) const { return TypeNode(d_nv->getChild(i)); } /** * Returns the unique id of this node + * * @return the id */ - unsigned getId() const { + inline unsigned getId() const { return d_nv->getId(); } /** * Returns the kind of this type node. + * * @return the kind */ inline Kind getKind() const { @@ -165,6 +184,7 @@ public: /** * Returns the metakind of this type node. + * * @return the metakind */ inline kind::MetaKind getMetaKind() const { @@ -173,6 +193,7 @@ public: /** * Returns the number of children this node has. + * * @return the number of children */ inline size_t getNumChildren() const; @@ -185,11 +206,13 @@ public: /** * Returns the value of the given attribute that this has been attached. + * * @param attKind the kind of the attribute * @return the value of the attribute */ template - inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const; + inline typename AttrKind::value_type + getAttribute(const AttrKind& attKind) const; // Note that there are two, distinct hasAttribute() declarations for // a reason (rather than using a pointer-valued argument with a @@ -197,9 +220,11 @@ public: // hasAttribute() implementations. /** - * Returns true if this node has been associated an attribute of given kind. - * Additionaly, if a pointer to the value_kind is give, and the attribute - * value has been set for this node, it will be returned. + * Returns true if this node has been associated an attribute of + * given kind. Additionally, if a pointer to the value_kind is + * give, and the attribute value has been set for this node, it will + * be returned. + * * @param attKind the kind of the attribute * @return true if this node has the requested attribute */ @@ -210,6 +235,7 @@ public: * Returns true if this node has been associated an attribute of given kind. * Additionaly, if a pointer to the value_kind is give, and the attribute * value has been set for this node, it will be returned. + * * @param attKind the kind of the attribute * @param value where to store the value if it exists * @return true if this node has the requested attribute @@ -220,6 +246,7 @@ public: /** * Sets the given attribute of this node to the given value. + * * @param attKind the kind of the atribute * @param value the value to set the attribute to */ @@ -234,6 +261,7 @@ public: /** * Returns the iterator pointing to the first child. + * * @return the iterator */ inline iterator begin() { @@ -241,8 +269,9 @@ public: } /** - * Returns the iterator pointing to the end of the children (one beyond the - * last one. + * Returns the iterator pointing to the end of the children (one + * beyond the last one. + * * @return the end of the children iterator. */ inline iterator end() { @@ -251,6 +280,7 @@ public: /** * Returns the const_iterator pointing to the first child. + * * @return the const_iterator */ inline const_iterator begin() const { @@ -258,8 +288,9 @@ public: } /** - * Returns the const_iterator pointing to the end of the children (one - * beyond the last one. + * Returns the const_iterator pointing to the end of the children + * (one beyond the last one. + * * @return the end of the children const_iterator. */ inline const_iterator end() const { @@ -267,8 +298,9 @@ public: } /** - * Converts this node into a string representation. - * @return the string representation of this node. + * Converts this type into a string representation. + * + * @return the string representation of this type. */ inline std::string toString() const { return d_nv->toString(); @@ -277,6 +309,7 @@ public: /** * Converst this node into a string representation and sends it to the * given stream + * * @param out the sream to serialise this node to */ inline void toStream(std::ostream& out, int toDepth = -1, @@ -286,6 +319,7 @@ public: /** * Very basic pretty printer for Node. + * * @param o output stream to print to. * @param indent number of spaces to indent the formula by. */ @@ -293,6 +327,7 @@ public: /** * Returns true if this type is a null type. + * * @return true if null */ bool isNull() const { @@ -350,6 +385,9 @@ public: /** Is this a sort kind */ bool isSort() const; + /** Is this a sort constructor kind */ + bool isSortConstructor() const; + /** Is this a kind type (i.e., the type of a type)? */ bool isKind() const; @@ -357,6 +395,7 @@ private: /** * Indents the given stream a given amount of spaces. + * * @param out the stream to indent * @param indent the numer of spaces */ @@ -370,6 +409,7 @@ private: /** * Serializes a given node to the given stream. + * * @param out the output stream to use * @param node the node to output to the stream * @return the changed stream. @@ -383,7 +423,7 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { // for hash_maps, hash_sets.. struct TypeNodeHashStrategy { - static inline size_t hash(const CVC4::TypeNode& node) { + static inline size_t hash(const TypeNode& node) { return (size_t) node.getId(); } };/* struct TypeNodeHashStrategy */ @@ -429,7 +469,8 @@ inline void TypeNode::assignNodeValue(expr::NodeValue* ev) { inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) { Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); - Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value on RHS!"); + Assert(typeNode.d_nv != NULL, + "Expecting a non-NULL expression value on RHS!"); if(EXPECT_TRUE( d_nv != typeNode.d_nv )) { d_nv->dec(); d_nv = typeNode.d_nv; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 39f61c16d..297a2d804 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -66,11 +66,15 @@ Expr Parser::getVariable(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } +Expr Parser::getFunction(const std::string& name) { + return getSymbol(name, SYM_VARIABLE); +} + Type Parser::getType(const std::string& var_name, SymbolType type) { Assert( isDeclared(var_name, type) ); - Type t = getSymbol(var_name,type).getType(); + Type t = getSymbol(var_name, type).getType(); return t; } @@ -83,8 +87,7 @@ Type Parser::getSort(const std::string& name) { Type Parser::getSort(const std::string& name, const std::vector& params) { Assert( isDeclared(name, SYM_SORT) ); - Type t = d_declScope.lookupType(name); - Warning() << "FIXME use params to realize parameterized sort\n"; + Type t = d_declScope.lookupType(name, params); return t; } @@ -98,6 +101,11 @@ bool Parser::isFunction(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction(); } +/* Returns true if name is bound to a defined function. */ +bool Parser::isDefinedFunction(const std::string& name) { + return isFunction(name) && d_declScope.isBoundDefinedFunction(name); +} + /* Returns true if name is bound to a function returning boolean. */ bool Parser::isPredicate(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); @@ -105,32 +113,54 @@ bool Parser::isPredicate(const std::string& name) { Expr Parser::mkVar(const std::string& name, const Type& type) { - Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl; + Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; Expr expr = d_exprManager->mkVar(name, type); - defineVar(name,expr); + defineVar(name, expr); + return expr; +} + +Expr +Parser::mkFunction(const std::string& name, const Type& type) { + Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; + Expr expr = d_exprManager->mkVar(name, type); + defineFunction(name, expr); return expr; } const std::vector Parser::mkVars(const std::vector names, - const Type& type) { + const Type& type) { std::vector vars; for(unsigned i = 0; i < names.size(); ++i) { - vars.push_back(mkVar(names[i],type)); + vars.push_back(mkVar(names[i], type)); } return vars; } void Parser::defineVar(const std::string& name, const Expr& val) { - d_declScope.bind(name,val); - Assert(isDeclared(name)); + d_declScope.bind(name, val); + Assert( isDeclared(name) ); +} + +void +Parser::defineFunction(const std::string& name, const Expr& val) { + d_declScope.bindDefinedFunction(name, val); + Assert( isDeclared(name) ); } void Parser::defineType(const std::string& name, const Type& type) { - d_declScope.bindType(name,type); - Assert( isDeclared(name, SYM_SORT) ) ; + d_declScope.bindType(name, type); + Assert( isDeclared(name, SYM_SORT) ); +} + +void +Parser::defineType(const std::string& name, + const std::vector& params, + const Type& type) { + d_declScope.bindType(name, params, type); + Assert( isDeclared(name, SYM_SORT) ); } void @@ -139,20 +169,30 @@ Parser::defineParameterizedType(const std::string& name, const Type& type) { if(Debug.isOn("parser")) { Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", ["; - copy(params.begin(), params.end() - 1, - ostream_iterator(Debug("parser"), ", ") ); - Debug("parser") << params.back(); + if(params.size() > 0) { + copy(params.begin(), params.end() - 1, + ostream_iterator(Debug("parser"), ", ") ); + Debug("parser") << params.back(); + } Debug("parser") << "], " << type << ")" << std::endl; } - Warning("defineSort unimplemented\n"); - defineType(name,type); + defineType(name, params, type); +} + +Type +Parser::mkSort(const std::string& name) { + Debug("parser") << "newSort(" << name << ")" << std::endl; + Type type = d_exprManager->mkSort(name); + defineType(name, type); + return type; } Type -Parser::mkSort(const std::string& name, size_t arity) { - Debug("parser") << "newSort(" << name << ", " << arity << ")" << std::endl; - Type type = d_exprManager->mkSort(name, arity); - defineType(name,type); +Parser::mkSortConstructor(const std::string& name, size_t arity) { + Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" + << std::endl; + Type type = d_exprManager->mkSortConstructor(name, arity); + defineType(name, vector(arity), type); return type; } @@ -239,7 +279,7 @@ void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserExcepti if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) { parseError( "Operator is not defined in the current logic: " + kindToString(kind) ); } - checkArity(kind,numArgs); + checkArity(kind, numArgs); } void Parser::addOperator(Kind kind) { diff --git a/src/parser/parser.h b/src/parser/parser.h index 0faf9bebf..1c492c843 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -186,26 +186,21 @@ public: bool strictModeEnabled() { return d_strictMode; } - /** Get the name of the input file. */ -/* - inline const std::string getFilename() { - return d_filename; - } -*/ - /** - * Sets the logic for the current benchmark. Declares any logic symbols. + * Returns a variable, given a name. * - * @param name the name of the logic (e.g., QF_UF, AUFLIA) + * @param name the name of the variable + * @return the variable expression */ -// void setLogic(const std::string& name); + Expr getVariable(const std::string& name); /** - * Returns a variable, given a name and a type. + * Returns a function, given a name. + * * @param var_name the name of the variable * @return the variable expression */ - Expr getVariable(const std::string& var_name); + Expr getFunction(const std::string& name); /** * Returns a sort, given a name. @@ -213,7 +208,7 @@ public: Type getSort(const std::string& sort_name); /** - * Returns a sort, given a name and args. + * Returns a (parameterized) sort, given a name and args. */ Type getSort(const std::string& sort_name, const std::vector& params); @@ -240,7 +235,8 @@ public: /** * Checks whether the given name is bound to a function. * @param name the name to check - * @throws ParserException if checks are enabled and name is not bound to a function + * @throws ParserException if checks are enabled and name is not + * bound to a function */ void checkFunction(const std::string& name) throw (ParserException); @@ -248,23 +244,26 @@ public: * Check that kind can accept numArgs arguments. * @param kind the built-in operator to check * @param numArgs the number of actual arguments - * @throws ParserException if checks are enabled and the operator kind cannot be - * applied to numArgs arguments. + * @throws ParserException if checks are enabled and the operator + * kind cannot be applied to numArgs + * arguments. */ void checkArity(Kind kind, unsigned int numArgs) throw (ParserException); - /** Check that kind is a legal operator in the current logic and - * that it can accept numArgs arguments. + /** + * Check that kind is a legal operator in the current + * logic and that it can accept numArgs arguments. * * @param kind the built-in operator to check * @param numArgs the number of actual arguments - * @throws ParserException if the parser mode is strict and the operator kind - * has not been enabled + * @throws ParserException if the parser mode is strict and the + * operator kind has not been enabled */ void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException); /** * Returns the type for the variable with the given name. + * * @param var_name the symbol to lookup * @param type the (namespace) type of the symbol */ @@ -274,27 +273,41 @@ public: Expr mkVar(const std::string& name, const Type& type); /** - * Create a set of new CVC4 variable expressions of the given - * type. + * Create a set of new CVC4 variable expressions of the given type. */ const std::vector mkVars(const std::vector names, const Type& type); + /** Create a new CVC4 function expression of the given type. */ + Expr mkFunction(const std::string& name, const Type& type); + /** Create a new variable definition (e.g., from a let binding). */ void defineVar(const std::string& name, const Expr& val); + /** Create a new function definition (e.g., from a define-fun). */ + void defineFunction(const std::string& name, const Expr& val); + /** Create a new type definition. */ void defineType(const std::string& name, const Type& type); + /** Create a new (parameterized) type definition. */ + void defineType(const std::string& name, + const std::vector& params, const Type& type); + /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */ void defineParameterizedType(const std::string& name, const std::vector& params, const Type& type); /** - * Creates a new sort with the given name and arity. + * Creates a new sort with the given name. + */ + Type mkSort(const std::string& name); + + /** + * Creates a new sort constructor with the given name and arity. */ - Type mkSort(const std::string& name, size_t arity = 0); + Type mkSortConstructor(const std::string& name, size_t arity); /** * Creates new sorts with the given names (all of arity 0). @@ -314,6 +327,9 @@ public: /** Is the symbol bound to a function? */ bool isFunction(const std::string& name); + /** Is the symbol bound to a defined function? */ + bool isDefinedFunction(const std::string& name); + /** Is the symbol bound to a predicate? */ bool isPredicate(const std::string& name); diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index da352c226..7ff738dd7 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -85,8 +85,8 @@ void Smt::addTheory(Theory theory) { case THEORY_ARRAYS_EX: { Type indexType = mkSort("Index"); Type elementType = mkSort("Element"); - - defineType("Array",getExprManager()->mkArrayType(indexType,elementType)); + + defineType("Array", getExprManager()->mkArrayType(indexType,elementType)); addOperator(kind::SELECT); addOperator(kind::STORE); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4c742adfc..9ad8c3177 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -19,8 +19,8 @@ grammar Smt2; options { - language = 'C'; // C output for antlr -// defaultErrorHandler = false; // Skip the default error handling, just break with exceptions + language = 'C'; // C output for antlr + //defaultErrorHandler = false; // Skip the default error handling, just break with exceptions k = 2; } @@ -162,8 +162,15 @@ command returns [CVC4::Command* cmd] DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl; - PARSER_STATE->mkSort(name, AntlrInput::tokenToUnsigned(n)); - $cmd = new DeclarationCommand(name,EXPR_MANAGER->kindType()); } + unsigned arity = AntlrInput::tokenToUnsigned(n); + if(arity == 0) { + PARSER_STATE->mkSort(name); + $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType()); + } else { + PARSER_STATE->mkSortConstructor(name, arity); + $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType()); + } + } | /* sort definition */ DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK @@ -223,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->mkVar(name, t); - $cmd = new DefineFunctionCommand(name,sortedVars,t,expr); + PARSER_STATE->mkFunction(name, t); + $cmd = new DefineFunctionCommand(name, sortedVars, t, expr); } | /* value query */ GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK @@ -315,22 +322,18 @@ term[CVC4::Expr& expr] | /* A non-built-in function application */ LPAREN_TOK - functionSymbol[expr] - { args.push_back(expr); } + functionName[name,CHECK_DECLARED] + { args.push_back(Expr()); } termList[args,expr] RPAREN_TOK - // TODO: check arity - { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); } - - // | /* An ite expression */ - // LPAREN_TOK ITE_TOK - // term[expr] - // { args.push_back(expr); } - // term[expr] - // { args.push_back(expr); } - // term[expr] - // { args.push_back(expr); } - // RPAREN_TOK - // { expr = MK_EXPR(CVC4::kind::ITE, args); } + { PARSER_STATE->checkFunction(name); + const bool isDefinedFunction = + PARSER_STATE->isDefinedFunction(name); + expr = isDefinedFunction ? + PARSER_STATE->getFunction(name) : + PARSER_STATE->getVariable(name); + args[0] = expr; + // TODO: check arity + expr = MK_EXPR(isDefinedFunction ? CVC4::kind::APPLY : CVC4::kind::APPLY_UF, args); } | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK @@ -479,7 +482,7 @@ sortSymbol[CVC4::Type& t] } t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); } else { - PARSER_STATE->parseError("Unhandled parameterized type."); + t = PARSER_STATE->getSort(name, args); } } ; @@ -516,9 +519,7 @@ symbol[std::string& id, // Base SMT-LIB tokens ASSERT_TOK : 'assert'; -//CATEGORY_TOK : ':category'; CHECKSAT_TOK : 'check-sat'; -//DIFFICULTY_TOK : ':difficulty'; DECLARE_FUN_TOK : 'declare-fun'; DECLARE_SORT_TOK : 'declare-sort'; DEFINE_FUN_TOK : 'define-fun'; @@ -526,23 +527,15 @@ DEFINE_SORT_TOK : 'define-sort'; GET_VALUE_TOK : 'get-value'; GET_ASSERTIONS_TOK : 'get-assertions'; EXIT_TOK : 'exit'; -//FALSE_TOK : 'false'; ITE_TOK : 'ite'; LET_TOK : 'let'; LPAREN_TOK : '('; -//NOTES_TOK : ':notes'; RPAREN_TOK : ')'; -//SAT_TOK : 'sat'; SET_LOGIC_TOK : 'set-logic'; SET_INFO_TOK : 'set-info'; +GET_INFO_TOK : 'get-info'; SET_OPTION_TOK : 'set-option'; GET_OPTION_TOK : 'get-option'; -//SMT_VERSION_TOK : ':smt-lib-version'; -//SOURCE_TOK : ':source'; -//STATUS_TOK : ':status'; -//TRUE_TOK : 'true'; -//UNKNOWN_TOK : 'unknown'; -//UNSAT_TOK : 'unsat'; // operators (NOTE: theory symbols go here) AMPERSAND_TOK : '&'; @@ -605,15 +598,18 @@ WHITESPACE ; /** - * Matches an integer constant from the input (non-empty sequence of digits, with - * no leading zeroes). + * Matches an integer constant from the input (non-empty sequence of + * digits, with no leading zeroes). */ INTEGER_LITERAL : NUMERAL ; -/** Match an integer constant. In non-strict mode, this is any sequence of - * digits. In strict mode, non-zero integers can't have leading zeroes. */ +/** + * Match an integer constant. In non-strict mode, this is any sequence + * of digits. In strict mode, non-zero integers can't have leading + * zeroes. + */ fragment NUMERAL @init { char *start = (char*) GETCHARINDEX(); @@ -631,8 +627,8 @@ fragment NUMERAL ; /** - * Matches a decimal constant from the input. - */ + * Matches a decimal constant from the input. + */ DECIMAL_LITERAL : NUMERAL '.' DIGIT+ ; @@ -684,7 +680,8 @@ fragment DIGIT : '0'..'9'; fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; -/** Matches the characters that may appear in a "symbol" (i.e., an identifier) +/** + * Matches the characters that may appear in a "symbol" (i.e., an identifier) */ fragment SYMBOL_CHAR : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~' diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c4eceeb24..be4abb8ab 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -94,8 +94,10 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : d_theoryEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); + d_functions = new(true) FunctionMap(d_context); + if(d_options->interactive) { - d_assertionList = new(true) CDList(d_context); + d_assertionList = new(true) AssertionList(d_context); } } @@ -110,7 +112,11 @@ SmtEngine::~SmtEngine() { shutdown(); - ::delete d_assertionList; + if(d_assertionList != NULL) { + d_assertionList->deleteSelf(); + } + + d_functions->deleteSelf(); delete d_theoryEngine; delete d_propEngine; @@ -145,7 +151,7 @@ void SmtEngine::defineFunction(const string& name, Type type, Expr formula) { NodeManagerScope nms(d_nodeManager); - Unimplemented(); + d_functions->insert(name, make_pair(make_pair(args, type), formula)); } Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 56e38af7a..97772273d 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -25,9 +25,11 @@ #include "expr/expr.h" #include "expr/expr_manager.h" +#include "context/cdmap_forward.h" #include "util/result.h" #include "util/model.h" #include "util/sexpr.h" +#include "util/hash.h" #include "smt/noninteractive_exception.h" #include "smt/bad_option.h" @@ -69,36 +71,39 @@ namespace smt { 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; + + /** The type of our internal assertion list */ + typedef context::CDList AssertionList; + /** 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; - + /** An index of our defined functions */ + FunctionMap* d_functions; /** - * The assertion list, before any conversion, for supporting + * The assertion list (before any conversion) for supporting * getAssertions(). Only maintained if in interactive mode. */ - context::CDList* d_assertionList; - - // preprocess() and addFormula() used to be housed here; they are - // now in an SmtEnginePrivate class. See the comment in - // smt_engine.cpp. + AssertionList* d_assertionList; /** * This is called by the destructor, just before destroying the diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index d3b9d12fb..47ee8cbfc 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -112,8 +112,14 @@ theory builtin ::CVC4::theory::builtin::TheoryBuiltin "theory_builtin.h" # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's # not stored that way. If you ask for the operator of (EQUAL a b), # you'll get a special, singleton (BUILTIN EQUAL) Node. -constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \ - "expr/kind.h" "The kind of nodes representing built-in operators" +constant BUILTIN \ + ::CVC4::Kind \ + ::CVC4::kind::KindHashStrategy \ + "expr/kind.h" \ + "The kind of nodes representing built-in operators" + +variable FUNCTION "function" +parameterized APPLY FUNCTION 1: "defined function application" operator EQUAL 2 "equality" operator DISTINCT 2: "disequality" diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 2ff92e788..aee147eff 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -31,6 +31,33 @@ namespace CVC4 { namespace theory { namespace builtin { +class ApplyTypeRule { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate) { + TNode f = n.getOperator(); + TypeNode fType = f.getType(check); + if( !fType.isFunction() ) { + throw TypeCheckingExceptionPrivate(n, "operator does not have function type"); + } + if( check ) { + if (n.getNumChildren() != fType.getNumChildren() - 1) { + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); + } + TNode::iterator argument_it = n.begin(); + TNode::iterator argument_it_end = n.end(); + TypeNode::iterator argument_type_it = fType.begin(); + for(; argument_it != argument_it_end; ++argument_it) { + if((*argument_it).getType() != *argument_type_it) { + throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + } + } + } + return fType.getRangeType(); + } +};/* class ApplyTypeRule */ + + class EqualityTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index cc6fe0c20..e7374284e 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -17,11 +17,11 @@ constant CONST_BITVECTOR \ ::CVC4::BitVectorHashStrategy \ "util/bitvector.h" \ "a fixed-width bit-vector constant" - + operator BITVECTOR_CONCAT 2: "bit-vector concatenation" operator BITVECTOR_AND 2 "bitwise and" -operator BITVECTOR_OR 2 "bitwise or" -operator BITVECTOR_XOR 2 "bitwise xor" +operator BITVECTOR_OR 2 "bitwise or" +operator BITVECTOR_XOR 2 "bitwise xor" operator BITVECTOR_NOT 2 "bitwise not" operator BITVECTOR_NAND 2 "bitwise nand" operator BITVECTOR_NOR 2 "bitwise nor" @@ -31,8 +31,8 @@ operator BITVECTOR_MULT 2 "bit-vector multiplication" operator BITVECTOR_PLUS 2 "bit-vector addition" operator BITVECTOR_SUB 2 "bit-vector subtraction" operator BITVECTOR_NEG 1 "bit-vector unary negation" -operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)" -operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)" +operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)" +operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)" operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division" operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)" operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)" @@ -83,7 +83,7 @@ constant BITVECTOR_ROTATE_RIGHT_OP \ "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateRight >" \ "util/bitvector.h" \ "operator for the bit-vector rotate right" - + parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract" parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat" parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend" diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 13cd5e91b..8cd6aec70 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -7,4 +7,6 @@ theory ::CVC4::theory::uf::TheoryUF "theory_uf.h" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" -variable SORT_TYPE "sort type" + +variable SORT_TAG "sort tag" +parameterized SORT_TYPE SORT_TAG 0: "sort type" diff --git a/src/util/hash.h b/src/util/hash.h index 2ce2d2941..cca60ce76 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -17,6 +17,8 @@ ** \todo document this file **/ +#include "cvc4_public.h" + #ifndef __CVC4__HASH_H #define __CVC4__HASH_H -- 2.30.2