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

src/ast/seq_decl_plugin.h

@@ -240,6 +240,8 @@ public:
         app* mk_index(expr* a, expr* b, expr* i) { expr* es[3] = { a, b, i}; return m.mk_app(m_fid, OP_SEQ_INDEX, 3, es); }
         app* mk_unit(expr* u) { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); }
         app* mk_char(zstring const& s, unsigned idx);
+        app* mk_itos(expr* i) { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); }
+        app* mk_stoi(expr* s) { return m.mk_app(m_fid, OP_STRING_STOI, 1, &s); }
 
         bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
 

src/model/func_interp.cpp

@@ -107,13 +107,10 @@ void func_interp::reset_interp_cache() {
 
 bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
     args.reset();
-    if (!is_app(e) || !m().is_ite(to_app(e)))
+    expr* c, *t, *f;
+    if (!m().is_ite(e, c, t, f)) {
         return false;
-
+    }
-    app * a = to_app(e);
-    expr * c = a->get_arg(0);
-    expr * t = a->get_arg(1);
-    expr * f = a->get_arg(2);
 
     if ((m_arity == 0) ||
         (m_arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) ||

src/qe/qe_arith.cpp

@@ -32,7 +32,6 @@ namespace qe {
 
     bool is_divides(arith_util& a, expr* e1, expr* e2, rational& k, expr_ref& p) {  
         expr* t1, *t2;
-        ast_manager& m = a.get_manager();
         if (a.is_mod(e2, t1, t2) && 
             a.is_numeral(e1, k) && 
             k.is_zero() &&

src/qe/qe_datatypes.cpp

@@ -87,7 +87,6 @@ namespace qe {
         }
 
         void project_rec(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
-            func_decl* f = m_val->get_decl();
             expr_ref rhs(m);
             expr_ref_vector eqs(m);
             for (unsigned i = 0; i < lits.size(); ++i) {

src/sat/tactic/goal2sat.cpp

@@ -324,6 +324,7 @@ struct goal2sat::imp {
     }
     
     void process(expr * n) {
+        //SASSERT(m_result_stack.empty());
         TRACE("goal2sat", tout << "converting: " << mk_ismt2_pp(n, m) << "\n";);
         if (visit(n, true, false)) {
             SASSERT(m_result_stack.empty());
@@ -342,8 +343,7 @@ struct goal2sat::imp {
             bool sign  = fr.m_sign;
             TRACE("goal2sat_bug", tout << "result stack\n";
                   tout << mk_ismt2_pp(t, m) << " root: " << root << " sign: " << sign << "\n";
-                  for (unsigned i = 0; i < m_result_stack.size(); i++) tout << m_result_stack[i] << " ";
+                  tout << m_result_stack << "\n";);
-                  tout << "\n";);
             if (fr.m_idx == 0 && process_cached(t, root, sign)) {
                 m_frame_stack.pop_back();
                 continue;
@@ -362,11 +362,11 @@ struct goal2sat::imp {
             }
             TRACE("goal2sat_bug", tout << "converting\n";
                   tout << mk_ismt2_pp(t, m) << " root: " << root << " sign: " << sign << "\n";
-                  for (unsigned i = 0; i < m_result_stack.size(); i++) tout << m_result_stack[i] << " ";
+                  tout << m_result_stack << "\n";);
-                  tout << "\n";);
             convert(t, root, sign);
             m_frame_stack.pop_back();
         }
+        CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";);
         SASSERT(m_result_stack.empty());
     }
 

src/smt/theory_seq.cpp

@@ -202,6 +202,7 @@ theory_seq::theory_seq(ast_manager& m):
     m_exclude(m),
     m_axioms(m),
     m_axioms_head(0),
+    m_int_string(m),
     m_mg(0),
     m_rewrite(m),
     m_seq_rewrite(m),
@@ -257,6 +258,11 @@ final_check_status theory_seq::final_check_eh() {
         TRACE("seq", tout << ">>fixed_length\n";);
         return FC_CONTINUE;
     }
+    if (check_int_string()) {
+        ++m_stats.m_int_string;
+        TRACE("seq", tout << ">>int_string\n";);
+        return FC_CONTINUE;
+    }
     if (reduce_length_eq() || branch_unit_variable() || branch_binary_variable() || branch_variable_mb() ||  branch_variable()) {
         ++m_stats.m_branch_variable;
         TRACE("seq", tout << ">>branch_variable\n";);
@@ -292,7 +298,6 @@ final_check_status theory_seq::final_check_eh() {
 
 bool theory_seq::reduce_length_eq() {
     context& ctx = get_context();
-    unsigned sz = m_eqs.size();
     int start = ctx.get_random_value();
 
     for (unsigned i = 0; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
@@ -451,7 +456,6 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
 }
 
 bool theory_seq::branch_variable_mb() {
-    context& ctx = get_context();
     bool change = false;
     for (unsigned i = 0; i < m_eqs.size(); ++i) {
         eq const& e = m_eqs[i];
@@ -2160,6 +2164,7 @@ void theory_seq::add_length(expr* e) {
     m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_length, e));
 }
 
+
 /*
   ensure that all elements in equivalence class occur under an applicatin of 'length'
 */
@@ -2177,6 +2182,48 @@ void theory_seq::enforce_length(enode* n) {
     while (n1 != n);
 }
 
+
+void theory_seq::add_int_string(expr* e) {
+    m_int_string.push_back(e);
+    m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_int_string));
+}
+
+bool theory_seq::check_int_string() {
+    bool change = false;
+    for (unsigned i = 0; i < m_int_string.size(); ++i) {
+        expr* e = m_int_string[i].get(), *n;
+        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.
+        }
+    }
+    return change;
+}
+
+bool theory_seq::add_itos_axiom(expr* e) {
+    rational val;
+    expr* n;
+    VERIFY(m_util.str.is_itos(e, n));
+    if (get_value(n, val)) {
+        if (!m_itos_axioms.contains(val)) {
+            m_itos_axioms.insert(val);
+
+            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);
+            add_axiom(mk_eq(m_util.str.mk_itos(n1), e1, false));
+            m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_itos_axioms, val));
+            m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
+            return true;
+        }            
+    }
+    return false;
+}
+
 void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
     mk_var(n);
 }
@@ -2317,6 +2364,7 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq add axiom", m_stats.m_add_axiom);
     st.update("seq extensionality", m_stats.m_extensionality);
     st.update("seq fixed length", m_stats.m_fixed_length);
+    st.update("seq int.to.str", m_stats.m_int_string);
 }
 
 void theory_seq::init_model(expr_ref_vector const& es) {
@@ -2627,6 +2675,9 @@ void theory_seq::deque_axiom(expr* n) {
     else if (m_util.str.is_string(n)) {
         add_elim_string_axiom(n);
     }
+    else if (m_util.str.is_itos(n)) {
+        add_itos_axiom(n);
+    }
 }
 
 
@@ -2890,6 +2941,14 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
     }
 }
 
+bool theory_seq::get_value(expr* e, rational& val) const {
+    context& ctx = get_context();
+    theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
+    expr_ref _val(m);
+    if (!tha || !tha->get_value(ctx.get_enode(e), _val)) return false;
+    return m_autil.is_numeral(_val, val) && val.is_int();
+}
+
 bool theory_seq::lower_bound(expr* _e, rational& lo) const {
     context& ctx = get_context();
     expr_ref e(m_util.str.mk_length(_e), m);
@@ -3525,6 +3584,11 @@ void theory_seq::relevant_eh(app* n) {
         enque_axiom(n);
     }
 
+    if (m_util.str.is_itos(n) ||
+        m_util.str.is_stoi(n)) {
+        add_int_string(n);
+    }
+
     expr* arg;
     if (m_util.str.is_length(n, arg) && !has_length(arg)) {
         enforce_length(get_context().get_enode(arg));

src/smt/theory_seq.h

@@ -287,7 +287,10 @@ namespace smt {
             unsigned m_extensionality;
             unsigned m_fixed_length;
             unsigned m_propagate_contains;
+            unsigned m_int_string;
         };
+        typedef hashtable<rational, rational::hash_proc, rational::eq_proc> rational_set;
+
         ast_manager&               m;
         dependency_manager         m_dm;
         solution_map               m_rep;        // unification representative.
@@ -303,6 +306,8 @@ namespace smt {
         obj_hashtable<expr>        m_axiom_set;
         unsigned                   m_axioms_head; // index of first axiom to add.
         bool            m_incomplete;             // is the solver (clearly) incomplete for the fragment.
+        expr_ref_vector     m_int_string;
+        rational_set        m_itos_axioms;
         obj_hashtable<expr> m_length;             // is length applied
         scoped_ptr_vector<apply> m_replay;        // set of actions to replay
         model_generator* m_mg;
@@ -481,9 +486,14 @@ namespace smt {
         bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
         void enforce_length_coherence(enode* n1, enode* n2);
 
+        // model-check the functions that convert integers to strings and the other way.
+        void add_int_string(expr* e);
+        bool check_int_string();
+
         void add_elim_string_axiom(expr* n);
         void add_at_axiom(expr* n);
         void add_in_re_axiom(expr* n);
+        bool add_itos_axiom(expr* n);
         literal mk_literal(expr* n);
         literal mk_eq_empty(expr* n, bool phase = true);
         literal mk_seq_eq(expr* a, expr* b);
@@ -496,6 +506,7 @@ namespace smt {
 
 
         // arithmetic integration
+        bool get_value(expr* s, rational& val) const;
         bool lower_bound(expr* s, rational& lo) const;
         bool upper_bound(expr* s, rational& hi) const;
         bool get_length(expr* s, rational& val) const;

src/util/vector.h

@@ -457,5 +457,15 @@ template<typename Hash>
 struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
 
 
+// Specialize vector<std::string> to be inaccessible.
+// This will catch any regression of issue #564 and #420.
+// Use std::vector<std::string> instead.
+template <>
+class vector<std::string, true, unsigned> {
+private:
+    vector<std::string, true, unsigned>();
+};
+
+
 #endif /* VECTOR_H_ */