diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-31 15:26:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-31 15:26:19 +0000 |
commit | 39031822cf3f9faab7b5b9e6cbce46a5194503b1 (patch) | |
tree | 7f95265819554a20a2ef4637a4a8a6a83a7cfc0b /src/parser | |
parent | d4bfaa103d56d5c0172bf1457343a75ddea8a9b5 (diff) |
enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some documentation, and make it possible to "make doc" on a clean source tree (post-configure)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_input.h | 2 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.h | 13 | ||||
-rw-r--r-- | src/parser/parser.h | 9 | ||||
-rw-r--r-- | src/parser/smt/smt.cpp | 14 | ||||
-rw-r--r-- | src/parser/smt/smt.h | 2 | ||||
-rw-r--r-- | src/parser/smt/smt_input.h | 9 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 13 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.h | 10 |
9 files changed, 9 insertions, 65 deletions
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(); |