diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-04 22:16:21 -0500 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-05 14:53:42 -0500 |
| commit | 831feca5415d7da807542cb1820909f09675b31b (patch) | |
| tree | 528f36366dabe994aa62630a63519031b33221f8 /src/parser/smt2/smt2.h | |
| parent | df554608cc47684be08d8be7c427027b7c5e8eb2 (diff) | |
Don't tokenize SET_THEORY operators in smt2 parser
Diffstat (limited to 'src/parser/smt2/smt2.h')
| -rw-r--r-- | src/parser/smt2/smt2.h | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 837adb15c..969892c5f 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -44,12 +44,15 @@ public: THEORY_REALS, THEORY_REALS_INTS, THEORY_QUANTIFIERS, - THEORY_STRINGS + THEORY_SETS, + THEORY_STRINGS, + THEORY_UF }; private: bool d_logicSet; LogicInfo d_logic; + std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap; protected: Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); @@ -62,6 +65,14 @@ public: */ void addTheory(Theory theory); + void addOperator(Kind k, const std::string& name); + + Kind getOperatorKind(const std::string& name) const; + + bool isOperatorEnabled(const std::string& name) const; + + bool isTheoryEnabled(Theory theory) const; + bool logicIsSet(); /** |