summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/attribute.h28
-rw-r--r--src/expr/declaration_scope.cpp4
-rw-r--r--src/expr/declaration_scope.h22
-rw-r--r--src/expr/expr_manager_template.cpp4
-rw-r--r--src/expr/expr_manager_template.h3
-rw-r--r--src/expr/expr_template.h15
-rw-r--r--src/expr/node.cpp2
-rw-r--r--src/expr/node.h20
-rw-r--r--src/expr/type.cpp8
-rw-r--r--src/expr/type_node.h17
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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback