diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-12 20:29:24 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-12 20:29:24 +0000 |
commit | a358ed3b520919acbb72fb9bcd2974ee4165f495 (patch) | |
tree | 52a9dd03f5735114cf196bafbc6a5ee6f5a40b22 /src/parser/smt2/smt2.h | |
parent | 8d691eac8e478576ebceb6406a8e372db5e3f7f1 (diff) |
Adding ParserBuilder, reducing visibility of Parser and Input constructors
Adding Smt2 subclass of Parser
Checking for multiple calls to set-logic in SMT v2
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 31 |
1 files changed, 21 insertions, 10 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 715d3199f..0bb3020a3 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -22,6 +22,7 @@ namespace std { using namespace __gnu_cxx; } #include "util/hash.h" +#include "parser/parser.h" namespace CVC4 { @@ -29,9 +30,8 @@ class SExpr; namespace parser { -class Parser; - -class Smt2 { +class Smt2 : public Parser { + friend class ParserBuilder; public: enum Logic { @@ -51,14 +51,25 @@ public: THEORY_REALS_INTS, }; +private: + bool d_logicSet; + Logic d_logic; + +protected: + Smt2(ExprManager* exprManager, Input* input, bool strictMode = false); + +public: /** * Add theory symbols to the parser state. * * @param parser the CVC4 Parser object * @param theory the theory to open (e.g., Core, Ints) */ - static void - addTheory(Parser& parser, Theory theory); + void + addTheory(Theory theory); + + bool + logicIsSet(); /** * Sets the logic for the current benchmark. Declares any logic and theory symbols. @@ -66,17 +77,17 @@ public: * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ - static void - setLogic(Parser& parser, const std::string& name); + void + setLogic(const std::string& name); - static void - setInfo(Parser& parser, const std::string& flag, const SExpr& sexpr); + void + setInfo(const std::string& flag, const SExpr& sexpr); static Logic toLogic(const std::string& name); private: - static void addArithmeticOperators(Parser& parser); + void addArithmeticOperators(); static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap(); }; }/* CVC4::parser namespace */ |