From 58be77730746a357bf3d7123df9d5ceac49cc40f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 20:32:37 -0800 Subject: [PATCH 1/5] fix #1358 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/diff_neq_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index 651000297..c66483750 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/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(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(k.get_int64()); - m_lower[x] = _k; + m_lower[x] = std::max(m_lower[x], _k); } else { throw_not_supported(); From c3f67f3b5f77bb7ea984baf2fa6117874d5aff44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 21:17:00 -0800 Subject: [PATCH 2/5] fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- src/smt/smt_context.h | 7 ++++++- src/smt/theory_str.cpp | 19 +++++++++++++------ src/smt/theory_str.h | 4 ++++ 4 files changed, 24 insertions(+), 8 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 7b508c7d8..2e65fddc9 100644 --- a/src/smt/smt_context.cpp +++ b/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";); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 3cc577b29..c6cca2c43 100644 --- a/src/smt/smt_context.h +++ b/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. } } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index a1f0f9777..17f889946 100644 --- a/src/smt/theory_str.cpp +++ b/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), @@ -4648,14 +4650,17 @@ 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; + theory_var curr = m_find.find(get_var(n)); + theory_var first = curr; do { - if (u.str.is_string(curr)) { + expr* a = get_ast(curr); + if (u.str.is_string(a)) { hasEqcValue = true; - return curr; + return a; } - curr = get_eqc_next(curr); - } while (curr != n); + curr = m_find.next(curr); + } + while (curr != first && curr != null_theory_var); hasEqcValue = false; return n; } @@ -10584,7 +10589,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()))); } } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index acac8cad1..b478808d2 100644 --- a/src/smt/theory_str.h +++ b/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; From c3364f17fa5058903ce4e606da21a9d0e781d23a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 21:19:22 -0800 Subject: [PATCH 3/5] fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 17f889946..2ed8c578f 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4652,15 +4652,17 @@ namespace smt { expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) { theory_var curr = m_find.find(get_var(n)); 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); + if (curr != null_theory_var) { + 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; } From 2e6ae8cfd24bea46bbc9c2fd54ce7eb611d12caa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 23:06:05 -0800 Subject: [PATCH 4/5] fix crash Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 15 ++++++++------- src/smt/theory_str.h | 2 +- src/util/union_find.h | 1 + 3 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 2ed8c578f..ed926a50d 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -63,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(); } @@ -281,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; @@ -1905,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 { @@ -4650,9 +4650,10 @@ namespace smt { // We only check m_find for a string constant. expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) { - theory_var curr = m_find.find(get_var(n)); - theory_var first = curr; + 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)) { diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index b478808d2..03fd31162 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -362,8 +362,8 @@ protected: // cache mapping each string S to Length(S) obj_map 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); diff --git a/src/util/union_find.h b/src/util/union_find.h index 7a99b149e..416b653af 100644 --- a/src/util/union_find.h +++ b/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; From 07031798ecf70edf76175195b55fef849d7099f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Nov 2017 01:43:35 -0800 Subject: [PATCH 5/5] fix occurs function used in qe_lite #1241 Signed-off-by: Nikolaj Bjorner --- src/qe/qe_lite.cpp | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 257331161..01806bc24 100644 --- a/src/qe/qe_lite.cpp +++ b/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 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; }