From c92a63690d96c20ded688c2eab5363d05928e598 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 May 2020 17:47:24 -0700 Subject: [PATCH] enable parsing (_ char ..) Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 9 +++++++++ src/ast/seq_decl_plugin.h | 1 + src/parsers/smt2/smt2parser.cpp | 3 ++- 3 files changed, 12 insertions(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index cdcee87f3..9bcb856f6 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -631,6 +631,7 @@ void seq_decl_plugin::init() { #endif m_sigs[_OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT); m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); + m_sigs[_OP_STRING_FROM_CHAR] = alloc(psig, m, "char", 1, 0, nullptr, strT); m_sigs[OP_STRING_ITOS] = alloc(psig, m, "str.from_int", 0, 1, &intT, strT); m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to_int", 0, 1, &strT, intT); m_sigs[OP_STRING_LT] = alloc(psig, m, "str.<", 0, 2, str2T, boolT); @@ -867,6 +868,14 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case _OP_STRING_CONCAT: return mk_assoc_fun(k, arity, domain, range, OP_SEQ_CONCAT, k); + case _OP_STRING_FROM_CHAR: { + if (!(num_parameters == 1 && parameters[0].is_int())) + m.raise_exception("character literal expects integer parameter"); + zstring zs(parameters[0].get_int()); + parameter p(zs.encode().c_str()); + return m.mk_const_decl(m_stringc_sym, m_string,func_decl_info(m_family_id, OP_STRING_CONST, 1, &p)); + } + case OP_SEQ_REPLACE: return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRREPL); case _OP_STRING_STRREPL: diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 39c09287f..d131bfeb7 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -94,6 +94,7 @@ enum seq_op_kind { OP_CHAR_LE, // Unicode comparison #endif // internal only operators. Converted to SEQ variants. + _OP_STRING_FROM_CHAR, _OP_STRING_STRREPL, _OP_STRING_CONCAT, _OP_STRING_LENGTH, diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 085e6298a..b58c3cd3b 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -408,6 +408,7 @@ namespace smt2 { bool curr_is_rparen() const { return curr() == scanner::RIGHT_PAREN; } bool curr_is_int() const { return curr() == scanner::INT_TOKEN; } bool curr_is_float() const { return curr() == scanner::FLOAT_TOKEN; } + bool curr_is_bv() const { return curr() == scanner::BV_TOKEN; } bool curr_id_is_underscore() const { SASSERT(curr_is_identifier()); return curr_id() == m_underscore; } bool curr_id_is_as() const { SASSERT(curr_is_identifier()); return curr_id() == m_as; } @@ -1551,7 +1552,7 @@ namespace smt2 { symbol r = curr_id(); next(); while (!curr_is_rparen()) { - if (curr_is_int()) { + if (curr_is_int() || curr_is_bv()) { if (!curr_numeral().is_unsigned()) { m_param_stack.push_back(parameter(curr_numeral())); }