diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-05 07:57:40 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-05 07:57:40 +0200 |
| commit | 287785c8c2fe8031489bdf2d9f56506a8dfe3b48 (patch) | |
| tree | c6cad1e3786ca34963bce597b61163dc9cb110cb /src/parser | |
| parent | 29e0da43933f8b388f3317baf522cb9d32affef2 (diff) | |
Remove support for conversions between uint32/uint16 and string. (#1069)
* Remove support for conversions between uint32/uint16 and string.
* Temporarily disable regression.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 14 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 4 |
2 files changed, 1 insertions, 17 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index efdd328a4..6cc5c29a4 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -226,10 +226,6 @@ tokens { STRING_SUFFIXOF_TOK = 'SUFFIXOF'; STRING_STOI_TOK = 'STRING_TO_INTEGER'; STRING_ITOS_TOK = 'INTEGER_TO_STRING'; - STRING_U16TOS_TOK = 'UINT16_TO_STRING'; - STRING_STOU16_TOK = 'STRING_TO_UINT16'; - STRING_U32TOS_TOK = 'UINT32_TO_STRING'; - STRING_STOU32_TOK = 'STRING_TO_UINT32'; //Regular expressions (TODO) //STRING_IN_REGEXP_TOK //STRING_TO_REGEXP_TOK @@ -1990,15 +1986,7 @@ stringTerm[CVC4::Expr& f] | STRING_STOI_TOK LPAREN formula[f] RPAREN { f = MK_EXPR(CVC4::kind::STRING_STOI, f); } | STRING_ITOS_TOK LPAREN formula[f] RPAREN - { f = MK_EXPR(CVC4::kind::STRING_ITOS, f); } - | STRING_U16TOS_TOK LPAREN formula[f] RPAREN - { f = MK_EXPR(CVC4::kind::STRING_U16TOS, f); } - | STRING_STOU16_TOK LPAREN formula[f] RPAREN - { f = MK_EXPR(CVC4::kind::STRING_STOU16, f); } - | STRING_U32TOS_TOK LPAREN formula[f] RPAREN - { f = MK_EXPR(CVC4::kind::STRING_U32TOS, f); } - | STRING_STOU32_TOK LPAREN formula[f] RPAREN - { f = MK_EXPR(CVC4::kind::STRING_STOU32, f); } + { f = MK_EXPR(CVC4::kind::STRING_ITOS, f); } /* string literal */ | str[s] diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index de3c9aa62..aeabdbac2 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -120,10 +120,6 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_SUFFIX, "str.suffixof" ); addOperator(kind::STRING_ITOS, "int.to.str" ); addOperator(kind::STRING_STOI, "str.to.int" ); - addOperator(kind::STRING_U16TOS, "u16.to.str" ); - addOperator(kind::STRING_STOU16, "str.to.u16" ); - addOperator(kind::STRING_U32TOS, "u32.to.str" ); - addOperator(kind::STRING_STOU32, "str.to.u32" ); addOperator(kind::STRING_IN_REGEXP, "str.in.re"); addOperator(kind::STRING_TO_REGEXP, "str.to.re"); addOperator(kind::REGEXP_CONCAT, "re.++"); |