diff options
Diffstat (limited to 'src')
32 files changed, 127 insertions, 163 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, diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index c88f368d2..2f12aea03 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -67,7 +67,7 @@ public: /** Create a file input. * - * @param filename the path of the file to read + * @param name the path of the file to read * @param useMmap <code>true</code> if the input should use memory-mapped I/O; otherwise, the * input will use the standard ANTLR3 I/O implementation. */ diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index cce935c0b..a3de3a61f 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -50,18 +50,7 @@ public: */ CvcInput(AntlrInputStream& inputStream); - /** Create a string input. - * - * @param exprManager the manager to use when building expressions from the input - * @param input the string to read - * @param name the "filename" to use when reporting errors - */ -/* - CvcInput(ExprManager* exprManager, const std::string& input, - const std::string& name); -*/ - - /* Destructor. Frees the lexer and the parser. */ + /** Destructor. Frees the lexer and the parser. */ ~CvcInput(); protected: diff --git a/src/parser/parser.h b/src/parser/parser.h index f7adb2b89..9765f352b 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -135,11 +135,13 @@ class CVC4_PUBLIC Parser { Expr getSymbol(const std::string& var_name, SymbolType type); protected: - /** Create a parser state. NOTE: The parser takes "ownership" of the given + /** + * Create a parser state. NOTE: The parser takes "ownership" of the given * input and will delete it on destruction. * * @param exprManager the expression manager to use when creating expressions * @param input the parser input + * @param strictMode whether to incorporate strict(er) compliance checks */ Parser(ExprManager* exprManager, Input* input, bool strictMode = false); @@ -207,13 +209,14 @@ public: /** * Returns a function, given a name. * - * @param var_name the name of the variable + * @param name the name of the variable * @return the variable expression */ Expr getFunction(const std::string& name); /** * Returns a sort, given a name. + * @param sort_name the name to look up */ Type getSort(const std::string& sort_name); @@ -267,7 +270,7 @@ public: * @param kind the built-in operator to check * @param numArgs the number of actual arguments * @throws ParserException if the parser mode is strict and the - * operator <code>kind</kind> has not been enabled + * operator <code>kind</code> has not been enabled */ void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException); diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index 7ff738dd7..da6638ea8 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -73,12 +73,6 @@ void Smt::addArithmeticOperators() { addOperator(kind::GEQ); } -/** - * Add theory symbols to the parser state. - * - * @param parser the CVC4 Parser object - * @param theory the theory to open (e.g., Core, Ints) - */ void Smt::addTheory(Theory theory) { switch(theory) { case THEORY_ARRAYS: @@ -128,12 +122,6 @@ inline void Smt::addUf() { addOperator(kind::APPLY_UF); } -/** - * Sets the logic for the current benchmark. Declares any logic and theory symbols. - * - * @param parser the CVC4 Parser object - * @param name the name of the logic (e.g., QF_UF, AUFLIA) - */ void Smt::setLogic(const std::string& name) { d_logicSet = true; d_logic = toLogic(name); @@ -148,7 +136,7 @@ void Smt::setLogic(const std::string& name) { case QF_NIA: addTheory(THEORY_INTS); break; - + case QF_LRA: case QF_RDL: addTheory(THEORY_REALS); diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index ffc113574..388b4cd6d 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -84,7 +84,6 @@ public: /** * Add theory symbols to the parser state. * - * @param parser the CVC4 Parser object * @param theory the theory to open (e.g., Core, Ints) */ void addTheory(Theory theory); @@ -94,7 +93,6 @@ public: /** * Sets the logic for the current benchmark. Declares any logic and theory symbols. * - * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ void setLogic(const std::string& name); diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index dda4d6348..c5b147b71 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -52,15 +52,6 @@ public: */ SmtInput(AntlrInputStream& inputStream); - /** - * Create a string input. - * - * @param exprManager the manager to use when building expressions from the input - * @param input the string to read - * @param name the "filename" to use when reporting errors - */ -// SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name); - /** Destructor. Frees the lexer and the parser. */ ~SmtInput(); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 308f45ed0..e41e0e26a 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -44,12 +44,6 @@ void Smt2::addArithmeticOperators() { addOperator(kind::GEQ); } -/** - * Add theory symbols to the parser state. - * - * @param parser the CVC4 Parser object - * @param theory the theory to open (e.g., Core, Ints) - */ void Smt2::addTheory(Theory theory) { switch(theory) { case THEORY_CORE: @@ -97,13 +91,6 @@ bool Smt2::logicIsSet() { return d_logicSet; } -/** - * Sets the logic for the current benchmark. Declares any logic and - * theory symbols. - * - * @param parser the CVC4 Parser object - * @param name the name of the logic (e.g., QF_UF, AUFLIA) - */ void Smt2::setLogic(const std::string& name) { d_logicSet = true; d_logic = Smt::toLogic(name); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 6398fa735..ef5f5e729 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -54,7 +54,6 @@ public: /** * Add theory symbols to the parser state. * - * @param parser the CVC4 Parser object * @param theory the theory to open (e.g., Core, Ints) */ void addTheory(Theory theory); @@ -65,7 +64,6 @@ public: * Sets the logic for the current benchmark. Declares any logic and * theory symbols. * - * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ void setLogic(const std::string& name); diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 02a480971..836472107 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -61,16 +61,6 @@ public: */ Smt2Input(AntlrInputStream& inputStream); - /** - * Create a string input. - * - * @param exprManager the manager to use when building expressions - * from the input - * @param input the string to read - * @param name the "filename" to use when reporting errors - */ -// Smt2Input(ExprManager* exprManager, const std::string& input, const std::string& name); - /** Destructor. Frees the lexer and the parser. */ virtual ~Smt2Input(); diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 7b986cf83..da41b1de4 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -71,9 +71,9 @@ bool CnfStream::isCached(TNode n) const { return d_translationCache.find(n) != d_translationCache.end(); } -SatLiteral CnfStream::lookupInCache(TNode n) const { - Assert(isCached(n), "Node is not in CNF translation cache"); - return d_translationCache.find(n)->second; +SatLiteral CnfStream::lookupInCache(TNode node) const { + Assert(isCached(node), "Node is not in CNF translation cache"); + return d_translationCache.find(node)->second; } void CnfStream::cacheTranslation(TNode node, SatLiteral lit) { diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 919214f9b..e307732f4 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -24,8 +24,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__CNF_STREAM_H -#define __CVC4__CNF_STREAM_H +#ifndef __CVC4__PROP__CNF_STREAM_H +#define __CVC4__PROP__CNF_STREAM_H #include "expr/node.h" #include "prop/sat.h" @@ -35,6 +35,7 @@ namespace CVC4 { namespace prop { + class PropEngine; /** @@ -70,18 +71,21 @@ protected: /** * Asserts the given clause to the sat solver. + * @param node the node giving rise to this clause * @param clause the clasue to assert */ void assertClause(TNode node, SatClause& clause); /** * Asserts the unit clause to the sat solver. + * @param node the node giving rise to this clause * @param a the unit literal of the clause */ void assertClause(TNode node, SatLiteral a); /** * Asserts the binary clause to the sat solver. + * @param node the node giving rise to this clause * @param a the first literal in the clause * @param b the second literal in the clause */ @@ -89,6 +93,7 @@ protected: /** * Asserts the ternary clause to the sat solver. + * @param node the node giving rise to this clause * @param a the first literal in the clause * @param b the second literal in the clause * @param c the thirs literal in the clause @@ -96,33 +101,33 @@ protected: void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c); /** - * Returns true if the node has been cashed in the translation cache. + * Returns true if the node has been cached in the translation cache. * @param node the node * @return true if the node has been cached */ bool isCached(TNode node) const; /** - * Returns the cashed literal corresponding to the given node. + * Returns the cached literal corresponding to the given node. * @param node the node to lookup * @return returns the corresponding literal */ - SatLiteral lookupInCache(TNode n) const; + SatLiteral lookupInCache(TNode node) const; /** * Caches the pair of the node and the literal corresponding to the * translation. - * @param node node - * @param lit + * @param node the node + * @param lit the literal */ void cacheTranslation(TNode node, SatLiteral lit); /** - * Acquires a new variable from the SAT solver to represent the node and - * inserts the necessary data it into the mapping tables. + * Acquires a new variable from the SAT solver to represent the node + * and inserts the necessary data it into the mapping tables. * @param node a formula - * @param theoryLiteral is this literal a theory literal (i.e. theory to be - * informed when set to true/false + * @param theoryLiteral whether this literal a theory literal (and + * therefore the theory is to be informed when set to true/false) * @return the literal corresponding to the formula */ SatLiteral newLiteral(TNode node, bool theoryLiteral = false); @@ -140,8 +145,8 @@ protected: public: /** - * Constructs a CnfStream that sends constructs an equi-satisfiable set of clauses - * and sends them to the given sat solver. + * Constructs a CnfStream that sends constructs an equi-satisfiable + * set of clauses and sends them to the given sat solver. * @param satSolver the sat solver to use */ CnfStream(SatInputInterface* satSolver); @@ -157,7 +162,7 @@ public: /** * Converts and asserts a formula. * @param node node to convert and assert - * @param whether the sat solver can choose to remove the clauses + * @param lemma whether the sat solver can choose to remove the clauses * @param negated wheather we are asserting the node negated */ virtual void convertAndAssert(TNode node, bool lemma, bool negated = false) = 0; @@ -184,8 +189,10 @@ public: const NodeCache& getNodeCache() const { return d_nodeCache; } + };/* class CnfStream */ + /** * TseitinCnfStream is based on the following recursive algorithm * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf @@ -249,9 +256,10 @@ private: */ SatLiteral toCNF(TNode node, bool negated = false); -}; /* class TseitinCnfStream */ +};/* class TseitinCnfStream */ + -}/* prop namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__CNF_STREAM_H */ +#endif /* __CVC4__PROP__CNF_STREAM_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 81930a5ea..5fc846a6c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -180,7 +180,7 @@ SmtEngine::~SmtEngine() { delete d_decisionEngine; } -void SmtEngine::setInfo(const string& key, const SExpr& value) +void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOptionException) { Debug("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; if(key == ":name" || @@ -206,7 +206,7 @@ void SmtEngine::setInfo(const string& key, const SExpr& value) throw BadOptionException(); } -SExpr SmtEngine::getInfo(const string& key) const +SExpr SmtEngine::getInfo(const std::string& key) const throw(BadOptionException) { Debug("smt") << "SMT getInfo(" << key << ")" << endl; if(key == ":all-statistics") { @@ -244,7 +244,7 @@ SExpr SmtEngine::getInfo(const string& key) const } } -void SmtEngine::setOption(const string& key, const SExpr& value) +void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOptionException) { Debug("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; if(key == ":print-success") { @@ -274,7 +274,7 @@ void SmtEngine::setOption(const string& key, const SExpr& value) } } -SExpr SmtEngine::getOption(const string& key) const +SExpr SmtEngine::getOption(const std::string& key) const throw(BadOptionException) { Debug("smt") << "SMT getOption(" << key << ")" << endl; if(key == ":print-success") { @@ -305,7 +305,7 @@ SExpr SmtEngine::getOption(const string& key) const } void SmtEngine::defineFunction(Expr func, - const vector<Expr>& formals, + const std::vector<Expr>& formals, Expr formula) { Debug("smt") << "SMT defineFunction(" << func << ")" << endl; NodeManagerScope nms(d_nodeManager); diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 7c3e5ba93..766a8fc0a 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -128,7 +128,7 @@ Monomial Monomial::operator*(const Monomial& mono) const { return Monomial::mkMonomial(newConstant, newVL); } -vector<Monomial> Monomial::sumLikeTerms(const vector<Monomial> & monos) { +vector<Monomial> Monomial::sumLikeTerms(const std::vector<Monomial> & monos) { Assert(isSorted(monos)); Debug("blah") << "start sumLikeTerms" << std::endl; @@ -161,7 +161,7 @@ void Monomial::print() const { Debug("normal-form") << getNode() << std::endl; } -void Monomial::printList(const vector<Monomial>& list) { +void Monomial::printList(const std::vector<Monomial>& list) { for(vector<Monomial>::const_iterator i = list.begin(), end = list.end(); i != end; ++i) { const Monomial& m =*i; m.print(); diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp index f3b979bfd..01131c4c9 100644 --- a/src/theory/arith/row_vector.cpp +++ b/src/theory/arith/row_vector.cpp @@ -30,8 +30,8 @@ bool RowVector::noZeroCoefficients(const VarCoeffArray& arr){ return true; } -void RowVector::zip(const vector< ArithVar >& variables, - const vector< Rational >& coefficients, +void RowVector::zip(const std::vector< ArithVar >& variables, + const std::vector< Rational >& coefficients, VarCoeffArray& output){ Assert(coefficients.size() == variables.size() ); @@ -48,8 +48,8 @@ void RowVector::zip(const vector< ArithVar >& variables, } } -RowVector::RowVector(const vector< ArithVar >& variables, - const vector< Rational >& coefficients, +RowVector::RowVector(const std::vector< ArithVar >& variables, + const std::vector< Rational >& coefficients, std::vector<uint32_t>& counts): d_rowCount(counts) { @@ -135,8 +135,8 @@ void RowVector::printRow(){ } ReducedRowVector::ReducedRowVector(ArithVar basic, - const vector<ArithVar>& variables, - const vector<Rational>& coefficients, + const std::vector<ArithVar>& variables, + const std::vector<Rational>& coefficients, std::vector<uint32_t>& count): RowVector(variables, coefficients, count), d_basic(basic){ diff --git a/src/theory/shared_term_manager.cpp b/src/theory/shared_term_manager.cpp index 564fb776f..8103a149a 100644 --- a/src/theory/shared_term_manager.cpp +++ b/src/theory/shared_term_manager.cpp @@ -183,7 +183,7 @@ void SharedTermManager::addEq(TNode eq, Theory* thReason) { } -void SharedTermManager::collectExplanations(SharedData* pData, set<Node>& s) const { +void SharedTermManager::collectExplanations(SharedData* pData, std::set<Node>& s) const { Theory* expTh = pData->getExplainingTheory(); if(expTh == NULL) { // This equality is directly from SAT, no need to ask a theory for an explanation diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp index 210391555..7641472f8 100644 --- a/src/util/decision_engine.cpp +++ b/src/util/decision_engine.cpp @@ -11,8 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief . + ** \brief A decision engine for CVC4 ** + ** A decision engine for CVC4. **/ #include "util/decision_engine.h" diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index e1d9e21b7..3eee8aeb6 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief A decision engine for CVC4. + ** \brief A decision engine for CVC4 ** ** A decision engine for CVC4. **/ diff --git a/src/util/options.cpp b/src/util/options.cpp index f6d3c3092..1d2e4ed8b 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -79,7 +79,7 @@ string Options::getDescription() const { return optionsDescription; } -void Options::printUsage(const string msg, std::ostream& out) { +void Options::printUsage(const std::string msg, std::ostream& out) { out << msg << optionsDescription << endl << flush; // printf(usage + options.getDescription(), options.binary_name.c_str()); // printf(usage, binary_name.c_str()); diff --git a/src/util/output.cpp b/src/util/output.cpp index 10db4f723..34a3af93e 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -63,7 +63,7 @@ void DebugC::printf(const char* tag, const char* fmt, ...) { } } -void DebugC::printf(string tag, const char* fmt, ...) { +void DebugC::printf(std::string tag, const char* fmt, ...) { if(d_tags.find(tag) != d_tags.end()) { // chop off output after 1024 bytes char buf[1024]; @@ -127,7 +127,7 @@ void TraceC::printf(const char* tag, const char* fmt, ...) { } } -void TraceC::printf(string tag, const char* fmt, ...) { +void TraceC::printf(std::string tag, const char* fmt, ...) { if(d_tags.find(tag) != d_tags.end()) { // chop off output after 1024 bytes char buf[1024]; diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index c675ab6c9..057100d10 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -30,7 +30,7 @@ using namespace CVC4; /* Computes a rational given a decimal string. The rational * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>. */ -Rational Rational::fromDecimal(const string& dec) { +Rational Rational::fromDecimal(const std::string& dec) { // Find the decimal point, if there is one string::size_type i( dec.find(".") ); if( i != string::npos ) { diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index aad1f8b2d..5921b8fd3 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -30,7 +30,7 @@ using namespace CVC4; /* Computes a rational given a decimal string. The rational * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>. */ -Rational Rational::fromDecimal(const string& dec) { +Rational Rational::fromDecimal(const std::string& dec) { // Find the decimal point, if there is one string::size_type i( dec.find(".") ); if( i != string::npos ) { diff --git a/src/util/result.cpp b/src/util/result.cpp index 9760eaefb..8e1db27c4 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -28,7 +28,7 @@ using namespace std; namespace CVC4 { -Result::Result(const string& instr) : +Result::Result(const std::string& instr) : d_sat(SAT_UNKNOWN), d_validity(VALIDITY_UNKNOWN), d_which(TYPE_NONE), |