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 | |
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')
-rw-r--r-- | src/parser/smt/Smt.g | 24 | ||||
-rw-r--r-- | src/theory/arith/kinds | 8 |
2 files changed, 27 insertions, 5 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. */ ; diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 3b79192d2..fafa33a68 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -8,7 +8,8 @@ theory ::CVC4::theory::arith::TheoryArith "theory_arith.h" operator PLUS 2: "arithmetic addition" operator MULT 2: "arithmetic multiplication" -operator UMINUS 1 "arithmetic negation" +operator MINUS 2 "arithmetic binary subtraction operator" +operator UMINUS 1 "arithmetic unary negation" constant CONST_RATIONAL \ ::CVC4::Rational \ @@ -21,3 +22,8 @@ constant CONST_INTEGER \ ::CVC4::IntegerHashStrategy \ "util/integer.h" \ "a multiple-precision integer constant" + +operator LT 2 "less than, x < y" +operator LEQ 2 "less than or equal, x <= y" +operator GT 2 "greater than, x > y" +operator GEQ 2 "greater than or equal, x >= y" |