diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5aa1e53e4..638c64a69 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1124,6 +1124,11 @@ indexedFunctionName[CVC4::Expr& op] { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); } | DIVISIBLE_TOK n=INTEGER_LITERAL { op = MK_CONST(Divisible(AntlrInput::tokenToUnsigned($n))); } + | INT2BV_TOK n=INTEGER_LITERAL + { op = MK_CONST(IntToBitVector(AntlrInput::tokenToUnsigned($n))); + if(PARSER_STATE->strictModeEnabled()) { + PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode"); + } } | badIndexedFunctionName ) RPAREN_TOK @@ -1234,6 +1239,11 @@ builtinOp[CVC4::Kind& kind] | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; } | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; } + | BV2NAT_TOK { $kind = CVC4::kind::BITVECTOR_TO_NAT; + if(PARSER_STATE->strictModeEnabled()) { + PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode"); + } } + | STRCON_TOK { $kind = CVC4::kind::STRING_CONCAT; } | STRLEN_TOK { $kind = CVC4::kind::STRING_LENGTH; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } @@ -1601,6 +1611,8 @@ BVSLT_TOK : 'bvslt'; BVSLE_TOK : 'bvsle'; BVSGT_TOK : 'bvsgt'; BVSGE_TOK : 'bvsge'; +BV2NAT_TOK : 'bv2nat'; +INT2BV_TOK : 'int2bv'; //STRING STRCST_TOK : 'str.const'; |