diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-04-28 14:52:22 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-04-28 14:52:22 +0000 |
| commit | 7a8454030fdbb1e6c2a6db7ce18eafe0764eaf4a (patch) | |
| tree | 1c2044783b304516f67a1355bf16b0af7ec42a06 /src/parser/smt/Smt.g | |
| parent | 0c4a6edae95b3ffc76cb82604a3d1694d42625bb (diff) | |
Added theory/arith/kind and enabled the smt parser to read in these symbols. Also a bug fix to a couple of unit tests.
Diffstat (limited to 'src/parser/smt/Smt.g')
| -rw-r--r-- | src/parser/smt/Smt.g | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 83e3447ac..4539a6d43 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -33,9 +33,11 @@ options { } @lexer::includes { -/** This suppresses warnings about the redefinition of token symbols between different - * parsers. The redefinitions should be harmless as long as no client: (a) #include's - * the lexer headers for two grammars AND (b) uses the token symbol definitions. */ +/** This suppresses warnings about the redefinition of token symbols between + * different parsers. The redefinitions should be harmless as long as no + * client: (a) #include's the lexer headers for two grammars AND (b) uses the + * token symbol definitions. + */ #pragma GCC system_header /* This improves performance by ~10 percent on big inputs. @@ -90,7 +92,9 @@ void setLogic(ParserState *parserState, const std::string& name) { if( name == "QF_UF" ) { parserState->mkSort("U"); - } else { + } else if(name == "QF_LRA"){ + parserState->mkSort("Real"); + } else{ // NOTE: Theory types go here Unhandled(name); } @@ -269,6 +273,18 @@ builtinOp[CVC4::Kind& kind] | IFF_TOK { $kind = CVC4::kind::IFF; } | EQUAL_TOK { $kind = CVC4::kind::EQUAL; } | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; } + | GREATER_THAN_TOK + { $kind = CVC4::kind::GT; } + | GREATER_THAN_TOK EQUAL_TOK + { $kind = CVC4::kind::GEQ; } + | LESS_THAN_TOK EQUAL_TOK + { $kind = CVC4::kind::LEQ; } + | LESS_THAN_TOK + { $kind = CVC4::kind::LT; } + | PLUS_TOK { $kind = CVC4::kind::PLUS; } + | STAR_TOK { $kind = CVC4::kind::MULT; } + | TILDE_TOK { $kind = CVC4::kind::UMINUS; } + | MINUS_TOK { $kind = CVC4::kind::MINUS; } // NOTE: Theory operators go here /* TODO: lt, gt, plus, minus, etc. */ ; |