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

src/qe/qe_lite.cpp

@@ -20,7 +20,6 @@ Revision History:
 #include "qe/qe_lite.h"
 #include "ast/expr_abstract.h"
 #include "ast/used_vars.h"
-#include "ast/occurs.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
@@ -39,6 +38,30 @@ Revision History:
 #include "qe/qe_vartest.h"
 
 namespace eq {
+
+    bool occurs_var(unsigned idx, expr* e) {
+        ptr_buffer<expr> todo;
+        todo.push_back(e);        
+        ast_mark mark;
+        while (!todo.empty()) {
+            expr* e = todo.back();
+            todo.pop_back();
+            if (mark.is_marked(e)) continue;
+            mark.mark(e, true);
+            if (is_var(e)) {
+                if (to_var(e)->get_idx() == idx) return true;
+            }
+            else if (is_app(e)) {
+                todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+            }
+            else if (is_quantifier(e)) {
+                quantifier* q = to_quantifier(e);
+                if (occurs_var(idx + q->get_num_decls(), q->get_expr())) return true;
+            }
+        }
+        return false;
+    }
+
     class der {
         ast_manager &   m;
         arith_util      a;
@@ -65,7 +88,7 @@ namespace eq {
             for (unsigned i = 0; i < definitions.size(); i++) {
                 var * v  = vars[i];
                 expr * t = definitions[i];
-                if (t == 0 || has_quantifiers(t) || occurs(v, t))
+                if (t == 0 || has_quantifiers(t) || occurs_var(v->get_idx(), t))
                     definitions[i] = 0;
                 else
                     found = true; // found at least one candidate
@@ -679,9 +702,9 @@ namespace eq {
         }
 
         bool is_unconstrained(var* x, expr* t, unsigned i, expr_ref_vector const& conjs) {
-            bool occ = occurs(x, t);
+            bool occ = occurs_var(x->get_idx(), t);
             for (unsigned j = 0; !occ && j < conjs.size(); ++j) {
-                occ = (i != j) && occurs(x, conjs[j]);
+                occ = (i != j) && occurs_var(x->get_idx(), conjs[j]);
             }
             return !occ;
         }

src/smt/smt_context.cpp

@@ -4373,7 +4373,7 @@ namespace smt {
     void context::add_rec_funs_to_model() {
         ast_manager& m = m_manager;
         SASSERT(m_model);
-        for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) {
+        for (unsigned i = 0; !get_cancel_flag() && i < m_asserted_formulas.get_num_formulas(); ++i) {
             expr* e = m_asserted_formulas.get_formula(i);
             if (is_quantifier(e)) {
                 TRACE("context", tout << mk_pp(e, m) << "\n";);

src/smt/smt_context.h

@@ -209,7 +209,12 @@ namespace smt {
             ~scoped_mk_model() {
                 if (m_ctx.m_proto_model.get() != 0) {
                     m_ctx.m_model = m_ctx.m_proto_model->mk_model();
-                    m_ctx.add_rec_funs_to_model();
+                    try {
+                        m_ctx.add_rec_funs_to_model();
+                    }
+                    catch (...) {
+                        // no op
+                    }
                     m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
                 }
             }

src/smt/theory_str.cpp

@@ -47,6 +47,8 @@ namespace smt {
         sLevel(0),
         finalCheckProgressIndicator(false),
         m_trail(m),
+        m_factory(nullptr),
+        m_unused_id(0),
         m_delayed_axiom_setup_terms(m),
         tmpStringVarCount(0),
         tmpXorVarCount(0),
@@ -61,8 +63,8 @@ namespace smt {
         cacheHitCount(0),
         cacheMissCount(0),
         m_fresh_id(0),
-        m_find(*this),
-        m_trail_stack(*this)
+        m_trail_stack(*this),
+        m_find(*this)
     {
         initialize_charset();
     }
@@ -279,7 +281,7 @@ namespace smt {
         } else {
             theory_var v = theory::mk_var(n);
             m_find.mk_var();
-            TRACE("str", tout << "new theory var v#" << v << std::endl;);
+            TRACE("str", tout << "new theory var v#" << v << " find " << m_find.find(v) << std::endl;);
             get_context().attach_th_var(n, this, v);
             get_context().mark_as_relevant(n);
             return v;
@@ -1903,8 +1905,8 @@ namespace smt {
 
     // support for user_smt_theory-style EQC handling
 
-    app * theory_str::get_ast(theory_var i) {
-        return get_enode(i)->get_owner();
+    app * theory_str::get_ast(theory_var v) {
+        return get_enode(v)->get_owner();
     }
 
     theory_var theory_str::get_var(expr * n) const {
@@ -4648,14 +4650,20 @@ namespace smt {
     // We only check m_find for a string constant.
 
     expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) {
-        expr * curr = n;
-        do {
-            if (u.str.is_string(curr)) {
-                hasEqcValue = true;
-                return curr;
-            }
-            curr = get_eqc_next(curr);
-        } while (curr != n);
+        theory_var curr = get_var(n);
+        if (curr != null_theory_var) {
+            curr = m_find.find(curr);
+            theory_var first = curr;
+            do {
+                expr* a = get_ast(curr);
+                if (u.str.is_string(a)) {
+                    hasEqcValue = true;
+                    return a;
+                }
+                curr = m_find.next(curr);
+            } 
+            while (curr != first && curr != null_theory_var);
+        }
         hasEqcValue = false;
         return n;
     }
@@ -10584,7 +10592,9 @@ namespace smt {
             return alloc(expr_wrapper_proc, val);
         } else {
             TRACE("str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;);
-            return alloc(expr_wrapper_proc, to_app(mk_string("**UNUSED**")));
+            std::ostringstream unused;
+            unused << "**UNUSED**" << (m_unused_id++);
+            return alloc(expr_wrapper_proc, to_app(mk_string(unused.str().c_str())));
         }
     }
 

src/smt/theory_str.h

@@ -267,6 +267,10 @@ protected:
 
     str_value_factory * m_factory;
 
+    // Unique identifier appended to unused variables to ensure that model construction
+    // does not introduce equalities when they weren't enforced.
+    unsigned m_unused_id;
+
     // terms we couldn't go through set_up_axioms() with because they weren't internalized
     expr_ref_vector m_delayed_axiom_setup_terms;
 
@@ -358,8 +362,8 @@ protected:
     // cache mapping each string S to Length(S)
     obj_map<expr, app*> length_ast_map;
 
-    th_union_find m_find;
     th_trail_stack m_trail_stack;
+    th_union_find m_find;
     theory_var get_var(expr * n) const;
     expr * get_eqc_next(expr * n);
     app * get_ast(theory_var i);

src/tactic/arith/diff_neq_tactic.cpp

@@ -95,13 +95,13 @@ class diff_neq_tactic : public tactic {
             if (is_uninterp_const(lhs) && u.is_numeral(rhs, k) && m_max_neg_k <= k && k <= m_max_k) {
                 var x  = mk_var(lhs);
                 int _k = static_cast<int>(k.get_int64());
-                m_upper[x] = _k;
+                m_upper[x] = std::min(m_upper[x], _k);
                 
             }
             else if (is_uninterp_const(rhs) && u.is_numeral(lhs, k) && m_max_neg_k <= k && k <= m_max_k) {
                 var x  = mk_var(rhs);
                 int _k = static_cast<int>(k.get_int64()); 
-                m_lower[x] = _k;
+                m_lower[x] = std::max(m_lower[x], _k);
             }
             else {
                 throw_not_supported();

src/util/union_find.h

@@ -102,6 +102,7 @@ public:
 
     unsigned find(unsigned v) const {
         while (true) {
+            SASSERT(v < m_find.size());
             unsigned new_v = m_find[v];
             if (new_v == v)
                 return v;