diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
commit | ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 (patch) | |
tree | 4ff6643e38469ceb84cd6791c5cbc295f625a735 /src/expr | |
parent | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (diff) |
declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 3 | ||||
-rw-r--r-- | src/expr/declaration_scope.cpp | 137 | ||||
-rw-r--r-- | src/expr/declaration_scope.h | 123 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 51 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 15 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 6 | ||||
-rw-r--r-- | src/expr/expr_template.h | 32 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 2 | ||||
-rw-r--r-- | src/expr/node.cpp | 11 | ||||
-rw-r--r-- | src/expr/node.h | 13 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 3 | ||||
-rw-r--r-- | src/expr/node_manager.h | 58 | ||||
-rw-r--r-- | src/expr/type.cpp | 191 | ||||
-rw-r--r-- | src/expr/type.h | 87 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 77 | ||||
-rw-r--r-- | src/expr/type_node.h | 91 |
16 files changed, 680 insertions, 220 deletions
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 <string> +#include <utility> -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<std::string,Expr,StringHashFunction>(d_context)), - d_typeMap(new (true) CDMap<std::string,Type,StringHashFunction>(d_context)) { + d_context(new Context), + d_exprMap(new(true) CDMap<std::string, Expr, StringHashFunction>(d_context)), + d_typeMap(new(true) CDMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)), + d_functions(new(true) CDSet<Expr, ExprHashFunction>(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<std::string, Expr, StringHashFunction>::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<Type>(), t)); } -bool DeclarationScope::isBoundType(const std::string& name) const throw () { +void DeclarationScope::bindType(const std::string& name, + const vector<Type>& params, + Type t) throw() { + if(Debug.isOn("sort")) { + Debug("sort") << "bindType(" << name << ", ["; + if(params.size() > 0) { + copy( params.begin(), params.end() - 1, + ostream_iterator<Type>(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<vector<Type>, 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<Type>& params) const throw(AssertionException) { + pair<vector<Type>, 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<Type>(Debug("sort"), ", ") ); + Debug("sort") << p.first.back() << "]" << endl + << "parameters ["; + copy( params.begin(), params.end() - 1, + ostream_iterator<Type>(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<Type>(Debug("sort"), ", ") ); + Debug("sort") << p.first.back() << "]" << endl + << "parameters ["; + copy( params.begin(), params.end() - 1, + ostream_iterator<Type>(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 <vector> +#include <utility> #include <ext/hash_map> #include "expr/expr.h" @@ -29,16 +31,17 @@ namespace CVC4 { class Type; namespace context { + class Context; -class Context; + template <class Key, class Data, class HashFcn> + class CDMap; -template <class Key, class Data, class HashFcn> -class CDMap; - -} //namespace context + template <class V, class HashFcn> + 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<std::string,Expr,StringHashFunction> *d_exprMap; + context::CDMap<std::string, Expr, StringHashFunction> *d_exprMap; /** A map for types. */ - context::CDMap<std::string,Type,StringHashFunction> *d_typeMap; + context::CDMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap; + + /** A set of defined functions. */ + context::CDSet<Expr, ExprHashFunction> *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 <code>name</code> is already bound in the current level, then the + /** + * Bind an expression to a name in the current scope level. If + * <code>name</code> is already bound in the current level, then the * binding is replaced. If <code>name</code> 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 <code>name</code> */ - void bind(const std::string& name, const Expr& obj) throw (); - - /** Bind a type to a name in the current scope. - * If <code>name</code> is already bound to a type in the current level, - * then the binding is replaced. If <code>name</code> 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 <code>name</code> + * is already bound to a type in the current level, then the binding + * is replaced. If <code>name</code> 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 <code>name</code> + */ + void bindDefinedFunction(const std::string& name, Expr obj) throw(); + + /** + * Bind a type to a name in the current scope. If <code>name</code> + * is already bound to a type in the current level, then the binding + * is replaced. If <code>name</code> 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 <code>name</code> + */ + void bindType(const std::string& name, Type t) throw(); + + /** + * Bind a type to a name in the current scope. If <code>name</code> + * is already bound to a type or type constructor in the current + * level, then the binding is replaced. If <code>name</code> 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 <code>name</code> */ - void bindType(const std::string& name, const Type& t) throw (); + void bindType(const std::string& name, + const std::vector<Type>& 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 <code>name</code> 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 <code>name</code> 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 <code>name(<i>params</i>)</code> in + * the current scope. + */ + Type lookupType(const std::string& name, + const std::vector<Type>& params) const throw(AssertionException); + + /** + * Pop a scope level. Deletes all bindings since the last call to * <code>pushScope</code>. Calls to <code>pushScope</code> and * <code>popScope</code> must be "properly nested." I.e., a call to * <code>popScope</code> is only legal if the number of prior calls to * <code>pushScope</code> on this <code>DeclarationScope</code> is strictly * greater than then number of prior calls to <code>popScope</code>. */ - 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<Expr>& 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<Type>& argTypes, const Type& range) { - Assert( argTypes.size() >= 1 ); NodeManagerScope nms(d_nodeManager); + Assert( argTypes.size() >= 1 ); std::vector<TypeNode> 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<Type>& argTypes, cons } FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) { - Assert( sorts.size() >= 2 ); NodeManagerScope nms(d_nodeManager); + Assert( sorts.size() >= 2 ); std::vector<TypeNode> 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<Type>& sorts) { } FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { - Assert( sorts.size() >= 1 ); NodeManagerScope nms(d_nodeManager); + Assert( sorts.size() >= 1 ); std::vector<TypeNode> 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<Type>& sorts) { } TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { - Assert( types.size() >= 2 ); NodeManagerScope nms(d_nodeManager); + Assert( types.size() >= 2 ); std::vector<TypeNode> 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<Expr>::const_iterator it = children.begin() ; std::vector<Expr>::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 <class T> 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 <code>children.size()</code> is greater than the max arity for * <code>kind</code>, 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<TypeNode>& 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<true> 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 <bool ref_count> inline size_t NodeTemplate<ref_count>::getNumChildren() const { @@ -976,7 +979,7 @@ NodeTemplate<ref_count>::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 <bool ref_count> NodeTemplate<true> NodeTemplate<ref_count>::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<attr::VarNameTag, std::string> VarNameAttr; +typedef expr::Attribute<attr::SortArityTag, uint64_t> 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<TypeNode>& 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<TypeNode>& 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 <iostream> #include <string> +#include <vector> #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<Type>& types, + const vector<Type>& replacements) const { + NodeManagerScope nms(d_nodeManager); + + vector<TypeNode> typesNodes, replacementsNodes; + + for(vector<Type>::const_iterator i = types.begin(), + iend = types.end(); + i != iend; + ++i) { + typesNodes.push_back(*(*i).d_typeNode); + } + + for(vector<Type>::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<Type> FunctionType::getArgTypes() const { +vector<Type> FunctionType::getArgTypes() const { NodeManagerScope nms(d_nodeManager); - std::vector<Type> args; - std::vector<TypeNode> argNodes = d_typeNode->getArgTypes(); - std::vector<TypeNode>::iterator it = argNodes.begin(); - std::vector<TypeNode>::iterator it_end = argNodes.end(); + vector<Type> args; + vector<TypeNode> argNodes = d_typeNode->getArgTypes(); + vector<TypeNode>::iterator it = argNodes.begin(); + vector<TypeNode>::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<Type> TupleType::getTypes() const { +vector<Type> TupleType::getTypes() const { NodeManagerScope nms(d_nodeManager); - std::vector<Type> types; - std::vector<TypeNode> typeNodes = d_typeNode->getTupleTypes(); - std::vector<TypeNode>::iterator it = typeNodes.begin(); - std::vector<TypeNode>::iterator it_end = typeNodes.end(); + vector<Type> types; + vector<TypeNode> typeNodes = d_typeNode->getTupleTypes(); + vector<TypeNode>::iterator it = typeNodes.begin(); + vector<TypeNode>::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<Type>& params) const { + NodeManagerScope nms(d_nodeManager); + vector<TypeNode> paramsNodes; + for(vector<Type>::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: /** @@ -114,6 +118,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<Type>& types, + const std::vector<Type>& replacements) const; + + /** * Assignment operator. * @param t the type to assign to this type * @return this type after assignment. @@ -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<Type> 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<Type> 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,13 +373,33 @@ 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<Type>& params) const; +}; + +/** * Class encapsulating the kind type (the type of types). */ class CVC4_PUBLIC KindType : public Type { @@ -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 <vector> + #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<TypeNode>& types, + const vector<TypeNode>& replacements) const { + vector<TypeNode>::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<TypeConstant>() == BOOLEAN_TYPE; + return getKind() == kind::TYPE_CONSTANT && + getConst<TypeConstant>() == BOOLEAN_TYPE; } bool TypeNode::isInteger() const { - return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE; + return getKind() == kind::TYPE_CONSTANT && + getConst<TypeConstant>() == INTEGER_TYPE; } bool TypeNode::isReal() const { return getKind() == kind::TYPE_CONSTANT - && (getConst<TypeConstant>() == REAL_TYPE || getConst<TypeConstant>() == INTEGER_TYPE); + && ( getConst<TypeConstant>() == REAL_TYPE || + getConst<TypeConstant>() == INTEGER_TYPE ); } bool TypeNode::isArray() const { @@ -60,10 +104,10 @@ bool TypeNode::isPredicate() const { return isFunction() && getRangeType().isBoolean(); } -std::vector<TypeNode> TypeNode::getArgTypes() const { +vector<TypeNode> TypeNode::getArgTypes() const { Assert(isFunction()); - std::vector<TypeNode> args; - for (unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { + vector<TypeNode> 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> TypeNode::getTupleTypes() const { +vector<TypeNode> TypeNode::getTupleTypes() const { Assert(isTuple()); - std::vector<TypeNode> types; - for (unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) { + vector<TypeNode> 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> 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<TypeConstant>() == KIND_TYPE; + return getKind() == kind::TYPE_CONSTANT && + getConst<TypeConstant>() == KIND_TYPE; } /** Is this a bit-vector type */ @@ -106,7 +156,8 @@ bool TypeNode::isBitVector() const { /** Is this a bit-vector type of size <code>size</code> */ bool TypeNode::isBitVector(unsigned size) const { - return getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size; + return getKind() == kind::BITVECTOR_TYPE && + getConst<BitVectorSize>() == 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 */ @@ -87,21 +87,23 @@ public: 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() { @@ -109,18 +111,31 @@ public: } /** + * Substitution of TypeNodes. + */ + TypeNode substitute(const TypeNode& type, const TypeNode& replacement) const; + + /** + * Simultaneous substitution of TypeNodes. + */ + TypeNode substitute(const std::vector<TypeNode>& types, + const std::vector<TypeNode>& 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 <class AttrKind> - 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; |