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/smt | |
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/smt')
-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 |
3 files changed, 1 insertions, 24 deletions
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(); |