diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-01 00:30:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-31 22:30:44 -0700 |
| commit | 936e9c442443799c866a65c6ca3fbdcd3ac9aab8 (patch) | |
| tree | b953269087d78261c6a5d81e4d32e4cce70d5f41 /src/parser | |
| parent | 6d43ef828f5cc84f05b2c52a1991f3fb8505db84 (diff) | |
Support char smt-lib syntax (#4188)
Towards support for the strings standard.
Adds support to (_ char #x ... ) syntax for characters.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d0a73ce6a..1d0fb71cb 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2083,6 +2083,11 @@ termAtomic[CVC4::api::Term& atomTerm] api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2"); atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2); } + | CHAR_TOK HEX_LITERAL + { + std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); + atomTerm = SOLVER->mkChar(hexStr); + } | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] { atomTerm = @@ -2094,10 +2099,10 @@ termAtomic[CVC4::api::Term& atomTerm] // Bit-vector constants | HEX_LITERAL - { - assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0); - std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); - atomTerm = SOLVER->mkBitVector(hexStr, 16); + { + assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0); + std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); + atomTerm = SOLVER->mkBitVector(hexStr, 16); } | BINARY_LITERAL { @@ -2686,6 +2691,7 @@ FORALL_TOK : 'forall'; CHOICE_TOK : { !PARSER_STATE->strictModeEnabled() }? 'choice'; EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp'; +CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple'; TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel'; |