Merge branch 'master' of https://github.com/Z3Prover/z3

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 mk_or(expr_vector const& args);
-        friend expr and(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<Z3_ast> _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<Z3_ast> _args(args);
         Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
         args.check_error();

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;

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<expr*>& 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) {

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

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);

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)) {
+        else if (m_util.str.is_stoi(e, n) && add_stoi_axiom(e)) {
-            // not (yet) handled.
+            change = true;
-            // we would check that in the current proto-model
-            // the string at 'n', when denoting integer would map to the
-            // proper integer.
         }
     }
     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<theory_seq, rational_set, rational>(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;

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<expr> m_length;             // is length applied
         scoped_ptr_vector<apply> 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);