From 936e9c442443799c866a65c6ca3fbdcd3ac9aab8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Apr 2020 00:30:44 -0500 Subject: Support char smt-lib syntax (#4188) Towards support for the strings standard. Adds support to (_ char #x ... ) syntax for characters. --- src/parser/smt2/Smt2.g | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'src/parser/smt2/Smt2.g') 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'; -- cgit v1.2.3