diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-06 20:07:56 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-06 20:07:56 +0000 |
commit | 1e8c9ae990adc55570298d1ffc5d8c55fbc71237 (patch) | |
tree | 8c8c0243a44a75ee471e7a477ed2391279df419c /src/parser | |
parent | e909abcaf122e7c426d2b078728679f43a8ca442 (diff) |
Adding bit-vector constants in SMT2
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_input.h | 6 | ||||
-rw-r--r-- | src/parser/parser.cpp | 3 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 42 |
3 files changed, 36 insertions, 15 deletions
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index f52467ad9..38fe1bce8 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -29,6 +29,7 @@ #include "expr/expr.h" #include "expr/expr_manager.h" #include "util/Assert.h" +#include "util/bitvector.h" #include "util/integer.h" #include "util/rational.h" @@ -148,8 +149,6 @@ public: static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token ); /** Retrieve a Rational from the text of a token */ static Rational tokenToRational(pANTLR3_COMMON_TOKEN token); - /** Retrive a Bitvector from the text of a token */ -// static Bitvector tokenToBitvector(pANTLR3_COMMON_TOKEN token, int base); protected: /** Create an input. This input takes ownership of the given input stream, @@ -201,8 +200,7 @@ inline unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) { } inline Integer AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) { - Integer i( tokenText(token) ); - return i; + return Integer( tokenText(token) ); } inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) { diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 01cc99c3d..d788a2c3f 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -241,8 +241,9 @@ Expr Parser::nextExpression() throw(ParserException) { if(!done()) { try { result = d_input->parseExpr(); - if(result.isNull()) + if(result.isNull()) { setDone(); + } } catch(ParserException& e) { setDone(); throw; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 19997cdd0..4f65fa5e7 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -259,6 +259,14 @@ term[CVC4::Expr& expr] | RATIONAL { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL) ); } + | HEX_LITERAL + { std::string hexString = AntlrInput::tokenText($HEX_LITERAL); + AlwaysAssert( hexString.find("#x") == 0 ); + expr = MK_CONST( BitVector(hexString.erase(0,2), 16) ); } + | BINARY_LITERAL + { std::string binString = AntlrInput::tokenText($BINARY_LITERAL); + AlwaysAssert( binString.find("#b") == 0 ); + expr = MK_CONST( BitVector(binString.erase(0,2), 2) ); } // NOTE: Theory constants go here ; @@ -352,15 +360,6 @@ sortSymbol[CVC4::Type& t] ; /** - * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. - */ -benchmarkStatus[ CVC4::BenchmarkStatus& status ] - : SAT_TOK { $status = SMT_SATISFIABLE; } - | UNSAT_TOK { $status = SMT_UNSATISFIABLE; } - | UNKNOWN_TOK { $status = SMT_UNKNOWN; } - ; - -/** * Matches an symbol and sets the string reference parameter id. * @param id string to hold the symbol * @param check what kinds of check to do on the symbol @@ -459,17 +458,38 @@ WHITESPACE ; /** - * Matches a numeral from the input (non-empty sequence of digits). + * Matches an integer constant from the input (non-empty sequence of digits). + * This is a bit looser than what the standard allows, because it accepts + * leading zeroes. */ NUMERAL : DIGIT+ ; +/** + * Matches a rational constant from the input. This is a bit looser + * than what the standard allows, because it accepts leading zeroes. + */ RATIONAL : DIGIT+ '.' DIGIT+ ; /** + * Matches a hexadecimal constant. + */ + HEX_LITERAL + : '#x' HEX_DIGIT+ + ; + +/** + * Matches a binary constant. + */ + BINARY_LITERAL + : '#b' ('0' | '1')+ + ; + + +/** * Matches a double quoted string literal. Escaping is supported, and escape * character '\' has to be escaped. */ @@ -499,6 +519,8 @@ ALPHA */ fragment DIGIT : '0'..'9'; +fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; + /** Matches the characters that may appear in a "symbol" (i.e., an identifier) */ fragment SYMBOL_CHAR |