mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

enable parsing (_ char ..)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-29 17:47:24 -07:00
parent d41ecda03e
commit c92a63690d
3 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/ast/seq_decl_plugin.cpp
View file

@ -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:

1
src/ast/seq_decl_plugin.h
View file

@ -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,

3
src/parsers/smt2/smt2parser.cpp
View file

@ -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()));
}