diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 98a1a76ea..e0c520f5b 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -802,8 +802,8 @@ namespace z3 { friend expr implies(expr const & a, bool b); friend expr implies(bool a, expr const & b); - friend expr or(expr_vector const& args); - friend expr and(expr_vector const& args); + friend expr mk_or(expr_vector const& args); + friend expr mk_and(expr_vector const& args); friend expr ite(expr const & c, expr const & t, expr const & e); @@ -1501,13 +1501,13 @@ namespace z3 { return expr(ctx, r); } - inline expr or(expr_vector const& args) { + inline expr mk_or(expr_vector const& args) { array _args(args); Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr()); args.check_error(); return expr(args.ctx(), r); } - inline expr and(expr_vector const& args) { + inline expr mk_and(expr_vector const& args) { array _args(args); Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr()); args.check_error(); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 29bfe25e5..3a447d0f5 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1515,6 +1515,11 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_ unsigned szl = ls.size() - head1, szr = rs.size() - head2; expr* const* _ls = ls.c_ptr() + head1, * const* _rs = rs.c_ptr() + head2; + if (solve_itos(szl, _ls, szr, _rs, lhs, rhs, is_sat)) { + ls.reset(); rs.reset(); + change = true; + return is_sat; + } if (length_constrained(szl, _ls, szr, _rs, lhs, rhs, is_sat)) { ls.reset(); rs.reset(); @@ -1679,6 +1684,56 @@ bool seq_rewriter::min_length(unsigned n, expr* const* es, unsigned& len) { return bounded; } +bool seq_rewriter::is_string(unsigned n, expr* const* es, zstring& s) const { + zstring s1; + expr* e; + bv_util bv(m()); + rational val; + unsigned sz; + for (unsigned i = 0; i < n; ++i) { + if (m_util.str.is_string(es[i], s1)) { + s = s + s1; + } + else if (m_util.str.is_unit(es[i], e) && bv.is_numeral(e, val, sz)) { + s = s + zstring(val.get_unsigned()); + } + else { + return false; + } + } + return true; +} + +bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs, + expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) { + + expr* l, *r; + if (szl == 1 && m_util.str.is_itos(ls[0], l)) { + if (szr == 1 && m_util.str.is_itos(rs[0], r)) { + lhs.push_back(l); + rhs.push_back(r); + is_sat = true; + return true; + } + zstring s; + if (is_string(szr, rs, s)) { + std::string s1 = s.encode(); + rational r(s1.c_str()); + if (s1 == r.to_string()) { + lhs.push_back(l); + rhs.push_back(m_autil.mk_numeral(r, true)); + return true; + } + } + } + + if (szr == 1 && m_util.str.is_itos(rs[0], r)) { + return solve_itos(szr, rs, szl, ls, rhs, lhs, is_sat); + } + + return false; +} + bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr, expr* const* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) { is_sat = true; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 040bae1b4..82579d53a 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -125,15 +125,20 @@ class seq_rewriter { expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat); bool length_constrained(unsigned n, expr* const* l, unsigned m, expr* const* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat); + bool solve_itos(unsigned n, expr* const* l, unsigned m, expr* const* r, + expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat); bool min_length(unsigned n, expr* const* es, unsigned& len); expr* concat_non_empty(unsigned n, expr* const* es); + bool is_string(unsigned n, expr* const* es, zstring& s) const; + void add_next(u_map& next, expr_ref_vector& trail, unsigned idx, expr* cond); bool is_sequence(expr* e, expr_ref_vector& seq); bool is_sequence(eautomaton& aut, expr_ref_vector& seq); bool is_epsilon(expr* e) const; void split_units(expr_ref_vector& lhs, expr_ref_vector& rhs); + public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m), m_autil(m), m_re2aut(m), m_es(m), m_lhs(m), m_rhs(m) { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 21af0773a..dc7307741 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -822,16 +822,6 @@ app* seq_util::str::mk_char(char ch) { return mk_char(s, 0); } -bool seq_util::str::is_char(expr* n, zstring& c) const { - if (u.is_char(n)) { - c = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str()); - return true; - } - else { - return false; - } -} - bool seq_util::str::is_string(expr const* n, zstring& s) const { if (is_string(n)) { s = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str()); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 78672182a..fbbcba5de 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -250,7 +250,6 @@ public: } bool is_string(expr const* n, zstring& s) const; - bool is_char(expr* n, zstring& s) const; bool is_empty(expr const* n) const { symbol s; return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 609181538..0702bac69 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2197,16 +2197,37 @@ bool theory_seq::check_int_string() { if (m_util.str.is_itos(e) && add_itos_axiom(e)) { change = true; } - else if (m_util.str.is_stoi(e, n)) { - // not (yet) handled. - // we would check that in the current proto-model - // the string at 'n', when denoting integer would map to the - // proper integer. + else if (m_util.str.is_stoi(e, n) && add_stoi_axiom(e)) { + change = true; } } return change; } +bool theory_seq::add_stoi_axiom(expr* e) { + context& ctx = get_context(); + expr* n; + rational val; + VERIFY(m_util.str.is_stoi(e, n)); + if (get_value(e, val) && !m_stoi_axioms.contains(val)) { + m_stoi_axioms.insert(val); + if (!val.is_minus_one()) { + app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m); + expr_ref n1(arith_util(m).mk_numeral(val, true), m); + literal eq1 = mk_eq(e, n1, false); + literal eq2 = mk_eq(n, e1, false); + add_axiom(~eq1, eq2); + add_axiom(~eq2, eq1); + ctx.force_phase(eq1); + ctx.force_phase(eq2); + m_trail_stack.push(insert_map(m_stoi_axioms, val)); + m_trail_stack.push(push_replay(alloc(replay_axiom, m, e))); + return true; + } + } + return false; +} + bool theory_seq::add_itos_axiom(expr* e) { context& ctx = get_context(); rational val; diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 136a84520..c1e179f67 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -308,6 +308,7 @@ namespace smt { bool m_incomplete; // is the solver (clearly) incomplete for the fragment. expr_ref_vector m_int_string; rational_set m_itos_axioms; + rational_set m_stoi_axioms; obj_hashtable m_length; // is length applied scoped_ptr_vector m_replay; // set of actions to replay model_generator* m_mg; @@ -493,6 +494,7 @@ namespace smt { void add_elim_string_axiom(expr* n); void add_at_axiom(expr* n); void add_in_re_axiom(expr* n); + bool add_stoi_axiom(expr* n); bool add_itos_axiom(expr* n); void add_itos_length_axiom(expr* n); literal mk_literal(expr* n);