diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/attribute.h | 28 | ||||
-rw-r--r-- | src/expr/declaration_scope.cpp | 4 | ||||
-rw-r--r-- | src/expr/declaration_scope.h | 22 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 3 | ||||
-rw-r--r-- | src/expr/expr_template.h | 15 | ||||
-rw-r--r-- | src/expr/node.cpp | 2 | ||||
-rw-r--r-- | src/expr/node.h | 20 | ||||
-rw-r--r-- | src/expr/type.cpp | 8 | ||||
-rw-r--r-- | src/expr/type_node.h | 17 |
10 files changed, 67 insertions, 56 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h index f5ecf84c5..9b21184d0 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -112,62 +112,52 @@ public: * Get a particular attribute on a particular node. * * @param nv the node about which to inquire - * - * @param const AttrKind& the attribute kind to get - * + * @param attr the attribute kind to get * @return the attribute value, if set, or a default-constructed * AttrKind::value_type if not. */ template <class AttrKind> typename AttrKind::value_type getAttribute(NodeValue* nv, - const AttrKind&) const; + const AttrKind& attr) const; /** * Determine if a particular attribute exists for a particular node. * * @param nv the node about which to inquire - * - * @param const AttrKind& the attribute kind to inquire about - * + * @param attr the attribute kind to inquire about * @return true if the given node has the given attribute */ template <class AttrKind> bool hasAttribute(NodeValue* nv, - const AttrKind&) const; + const AttrKind& attr) const; /** * Determine if a particular attribute exists for a particular node, * and get it if it does. * * @param nv the node about which to inquire - * - * @param const AttrKind& the attribute kind to inquire about - * + * @param attr the attribute kind to inquire about * @param ret a pointer to a return value, set in case the node has * the attribute - * * @return true if the given node has the given attribute */ template <class AttrKind> bool getAttribute(NodeValue* nv, - const AttrKind&, + const AttrKind& attr, typename AttrKind::value_type& ret) const; /** * Set a particular attribute on a particular node. * * @param nv the node for which to set the attribute - * - * @param const AttrKind& the attribute kind to set - * - * @param ret a pointer to a return value, set in case the node has + * @param attr the attribute kind to set + * @param value a pointer to a return value, set in case the node has * the attribute - * * @return true if the given node has the given attribute */ template <class AttrKind> void setAttribute(NodeValue* nv, - const AttrKind&, + const AttrKind& attr, const typename AttrKind::value_type& value); /** diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index 0c76ea845..f36c8a6e3 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -76,7 +76,7 @@ void DeclarationScope::bindType(const std::string& name, Type t) throw() { } void DeclarationScope::bindType(const std::string& name, - const vector<Type>& params, + const std::vector<Type>& params, Type t) throw() { if(Debug.isOn("sort")) { Debug("sort") << "bindType(" << name << ", ["; @@ -104,7 +104,7 @@ Type DeclarationScope::lookupType(const std::string& name) const throw(Assertion } Type DeclarationScope::lookupType(const std::string& name, - const vector<Type>& params) const throw(AssertionException) { + const std::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: " diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 76d85bcd7..65574b6c9 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -67,10 +67,10 @@ public: /** * 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. + * <code>name</code> is already bound to an expression 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 obj the expression to bind to <code>name</code> @@ -78,14 +78,15 @@ public: 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. + * Bind a function body to a name in the current scope. If + * <code>name</code> is already bound to an expression 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. Same as bind() but registers + * this as a function (so that isBoundDefinedFunction() returns true). * * @param name an identifier - * @param t the type to bind to <code>name</code> + * @param obj the expression to bind to <code>name</code> */ void bindDefinedFunction(const std::string& name, Expr obj) throw(); @@ -109,6 +110,7 @@ public: * one until the current scope is popped. * * @param name an identifier + * @param params the parameters to the type * @param t the type to bind to <code>name</code> */ void bindType(const std::string& name, diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index b0951b954..c59be7749 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -27,7 +27,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 30 "${template}" +#line 31 "${template}" using namespace std; using namespace CVC4::context; @@ -302,7 +302,7 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name, * type checking is not requested, getType() will do the minimum * amount of checking required to return a valid result. * - * @param n the Expr for which we want a type + * @param e the Expr for which we want a type * @param check whether we should check the type as we compute it * (default: false) */ diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 21526809e..e5df3ced3 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -114,6 +114,7 @@ public: /** * Make a unary expression of a given kind (NOT, BVNOT, ...). + * @param kind the kind of expression * @param child1 kind the kind of expression * @return the expression */ @@ -192,7 +193,7 @@ public: * suitably-sized chunks, taking advantage of the associativity of * <code>kind</code>. For example, if kind <code>FOO</code> has max arity * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return - * <code>(FOO (FOO a b) c)</code> or code>(FOO a (FOO b c))</code>. + * <code>(FOO (FOO a b) c)</code> or <code>(FOO a (FOO b c))</code>. * The order of the arguments will be preserved in a left-to-right * traversal of the resulting tree. */ diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 2eac4ab62..be089bca8 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -309,10 +309,17 @@ public: /** * Outputs the string representation of the expression to the stream. - * @param out the output stream - */ - void toStream(std::ostream& out, int depth = -1, bool types = false, - OutputLanguage lang = language::output::LANG_AST) const; + * + * @param out the stream to serialize this expression to + * @param toDepth the depth to which to print this expression, or -1 + * to print it fully + * @param types set to true to ascribe types to the output + * expressions (might break language compliance, but good for + * debugging expressions) + * @param language the language in which to output + */ + void toStream(std::ostream& out, int toDepth = -1, bool types = false, + OutputLanguage language = language::output::LANG_AST) const; /** * Check if this is a null expression. diff --git a/src/expr/node.cpp b/src/expr/node.cpp index d9933689d..efcd42999 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -26,7 +26,7 @@ using namespace std; namespace CVC4 { TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, - string message) : + std::string message) : Exception(message), d_node(new Node(node)) { } diff --git a/src/expr/node.h b/src/expr/node.h index 6089eea4d..c30e2e856 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -565,7 +565,7 @@ public: * PLUSes don't exist---begin(PLUS) will give an iterator over the * children if the node's a PLUS node, otherwise give an iterator * over the node itself, as if it were a unary PLUS. - * @param the kind to match + * @param kind the kind to match * @return the kinded_iterator iterating over this Node (if its kind * is not the passed kind) or its children */ @@ -583,7 +583,7 @@ public: * don't exist---begin(PLUS) will give an iterator over the children * if the node's a PLUS node, otherwise give an iterator over the * node itself, as if it were a unary PLUS. - * @param the kind to match + * @param kind the kind to match * @return the kinded_iterator pointing off-the-end of this Node (if * its kind is not the passed kind) or off-the-end of its children */ @@ -619,7 +619,7 @@ public: * PLUSes don't exist---begin(PLUS) will give an iterator over the * children if the node's a PLUS node, otherwise give an iterator * over the node itself, as if it were a unary PLUS. - * @param the kind to match + * @param kind the kind to match * @return the kinded_iterator iterating over this Node (if its kind * is not the passed kind) or its children */ @@ -637,7 +637,7 @@ public: * don't exist---begin(PLUS) will give an iterator over the children * if the node's a PLUS node, otherwise give an iterator over the * node itself, as if it were a unary PLUS. - * @param the kind to match + * @param kind the kind to match * @return the kinded_iterator pointing off-the-end of this Node (if * its kind is not the passed kind) or off-the-end of its children */ @@ -658,7 +658,13 @@ public: /** * Converst this node into a string representation and sends it to the * given stream + * * @param out the stream to serialize this node to + * @param toDepth the depth to which to print this expression, or -1 to + * print it fully + * @param types set to true to ascribe types to the output expressions + * (might break language compliance, but good for debugging expressions) + * @param language the language in which to output */ inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, OutputLanguage language = language::output::LANG_AST) const { @@ -700,7 +706,7 @@ public: /** * Very basic pretty printer for Node. - * @param o output stream to print to. + * @param out output stream to print to. * @param indent number of spaces to indent the formula by. */ inline void printAst(std::ostream& out, int indent = 0) const; @@ -721,8 +727,8 @@ public: /** * 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. + * @param n the node to output to the stream + * @return the stream */ inline std::ostream& operator<<(std::ostream& out, TNode n) { n.toStream(out, diff --git a/src/expr/type.cpp b/src/expr/type.cpp index b8b2e4754..0d12e7011 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -91,8 +91,8 @@ Type Type::substitute(const Type& type, const Type& replacement) const { *replacement.d_typeNode)); } -Type Type::substitute(const vector<Type>& types, - const vector<Type>& replacements) const { +Type Type::substitute(const std::vector<Type>& types, + const std::vector<Type>& replacements) const { NodeManagerScope nms(d_nodeManager); vector<TypeNode> typesNodes, replacementsNodes; @@ -117,7 +117,7 @@ Type Type::substitute(const vector<Type>& types, replacementsNodes.end())); } -void Type::toStream(ostream& out) const { +void Type::toStream(std::ostream& out) const { NodeManagerScope nms(d_nodeManager); out << *d_typeNode; return; @@ -313,7 +313,7 @@ size_t SortConstructorType::getArity() const { return d_typeNode->getAttribute(expr::SortArityAttr()); } -SortType SortConstructorType::instantiate(const vector<Type>& params) const { +SortType SortConstructorType::instantiate(const std::vector<Type>& params) const { NodeManagerScope nms(d_nodeManager); vector<TypeNode> paramsNodes; for(vector<Type>::const_iterator i = params.begin(), diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 27cedf00d..ead85cd19 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -96,7 +96,7 @@ public: * Assignment operator for nodes, copies the relevant information from node * to this node. * - * @param node the node to copy + * @param typeNode the node to copy * @return reference to this node */ TypeNode& operator=(const TypeNode& typeNode); @@ -150,7 +150,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 + * @param typeNode the node to compare to * @return true if this expression is smaller */ inline bool operator<(const TypeNode& typeNode) const { @@ -314,6 +314,11 @@ public: * given stream * * @param out the stream to serialize this node to + * @param toDepth the depth to which to print this expression, or -1 to + * print it fully + * @param types set to true to ascribe types to the output expressions + * (might break language compliance, but good for debugging expressions) + * @param language the language in which to output */ inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, OutputLanguage language = language::output::LANG_AST) const { @@ -323,7 +328,7 @@ public: /** * Very basic pretty printer for Node. * - * @param o output stream to print to. + * @param out output stream to print to. * @param indent number of spaces to indent the formula by. */ void printAst(std::ostream& out, int indent = 0) const; @@ -400,7 +405,7 @@ private: * Indents the given stream a given amount of spaces. * * @param out the stream to indent - * @param indent the numer of spaces + * @param indent the number of spaces */ static void indent(std::ostream& out, int indent) { for(int i = 0; i < indent; i++) { @@ -414,8 +419,8 @@ 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. + * @param n the node to output to the stream + * @return the stream */ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { n.toStream(out, |