From 276fdd0e972d9f6c7d78b9eb093fc2b27bb212d7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Aug 2017 08:51:24 -0700 Subject: [PATCH 1/7] register auxiliary constants from projection operation Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 10 +++--- src/model/model_core.cpp | 2 +- src/smt/proto_model/proto_model.cpp | 56 +++++++++++++---------------- src/smt/proto_model/proto_model.h | 1 + src/smt/smt_model_checker.cpp | 5 +-- src/smt/smt_model_finder.cpp | 21 +++++------ src/smt/theory_seq.cpp | 10 ++++-- src/smt/theory_str.cpp | 49 ++++++++++--------------- 8 files changed, 68 insertions(+), 86 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 36a99c592..70eddcea1 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -864,11 +864,11 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { expr_ref_vector as(m()), bs(m()); if (a1 != b1 && isc1 && isc2) { - TRACE("seq", tout << s1 << " " << s2 << "\n";); if (s1.length() <= s2.length()) { if (s1.prefixof(s2)) { if (a == a1) { result = m().mk_true(); + TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";); return BR_DONE; } m_util.str.get_concat(a, as); @@ -878,10 +878,12 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { bs[0] = m_util.str.mk_string(s2); result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size()-1, as.c_ptr()+1), m_util.str.mk_concat(bs.size(), bs.c_ptr())); + TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";); return BR_REWRITE_FULL; } else { result = m().mk_false(); + TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";); return BR_DONE; } } @@ -889,6 +891,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { if (s2.prefixof(s1)) { if (b == b1) { result = m().mk_false(); + TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";); return BR_DONE; } m_util.str.get_concat(a, as); @@ -898,10 +901,12 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { as[0] = m_util.str.mk_string(s1); result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size(), as.c_ptr()), m_util.str.mk_concat(bs.size()-1, bs.c_ptr()+1)); + TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";); return BR_REWRITE_FULL; } else { result = m().mk_false(); + TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";); return BR_DONE; } } @@ -930,9 +935,6 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { if (i == as.size()) { result = mk_and(eqs); TRACE("seq", tout << result << "\n";); - if (m().is_true(result)) { - return BR_DONE; - } return BR_REWRITE3; } SASSERT(i < as.size()); diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 9da1e76f9..684d1b3c2 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -94,7 +94,7 @@ void model_core::unregister_decl(func_decl * d) { m_manager.dec_ref(ec->get_data().m_value); m_interp.remove(d); m_const_decls.erase(d); - return; + return; } decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index f14034601..1eed4d0dd 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -42,6 +42,11 @@ proto_model::proto_model(ast_manager & m, params_ref const & p): void proto_model::register_aux_decl(func_decl * d, func_interp * fi) { model_core::register_decl(d, fi); + TRACE("cleanup_bug", tout << "register " << d->get_name() << "\n";); + m_aux_decls.insert(d); +} + +void proto_model::register_aux_decl(func_decl * d) { m_aux_decls.insert(d); } @@ -220,31 +225,29 @@ void proto_model::remove_aux_decls_not_in_set(ptr_vector & decls, fun */ void proto_model::cleanup() { func_decl_set found_aux_fs; - decl2finterp::iterator it = m_finterp.begin(); - decl2finterp::iterator end = m_finterp.end(); - for (; it != end; ++it) { - func_interp * fi = (*it).m_value; + for (auto const& kv : m_finterp) { + func_interp * fi = kv.m_value; cleanup_func_interp(fi, found_aux_fs); } + TRACE("cleanup_bug", + for (func_decl* faux : m_aux_decls) { + tout << faux->get_name() << "\n"; + }); // remove auxiliary declarations that are not used. if (found_aux_fs.size() != m_aux_decls.size()) { remove_aux_decls_not_in_set(m_decls, found_aux_fs); remove_aux_decls_not_in_set(m_func_decls, found_aux_fs); - func_decl_set::iterator it2 = m_aux_decls.begin(); - func_decl_set::iterator end2 = m_aux_decls.end(); - for (; it2 != end2; ++it2) { - func_decl * faux = *it2; + for (func_decl* faux : m_aux_decls) { if (!found_aux_fs.contains(faux)) { TRACE("cleanup_bug", tout << "eliminating " << faux->get_name() << "\n";); - func_interp * fi = 0; - m_finterp.find(faux, fi); - SASSERT(fi != 0); - m_finterp.erase(faux); - m_manager.dec_ref(faux); - dealloc(fi); + unregister_decl(faux); } + else { + TRACE("cleanup_bug", tout << "not eliminating " << faux->get_name() << "\n";); + } + } m_aux_decls.swap(found_aux_fs); } @@ -270,10 +273,8 @@ ptr_vector const & proto_model::get_universe(sort * s) const { ptr_vector & tmp = const_cast(this)->m_tmp; tmp.reset(); obj_hashtable const & u = get_known_universe(s); - obj_hashtable::iterator it = u.begin(); - obj_hashtable::iterator end = u.end(); - for (; it != end; ++it) - tmp.push_back(*it); + for (expr * e : u) + tmp.push_back(e); return tmp; } @@ -356,10 +357,7 @@ bool proto_model::is_as_array(expr * v) const { } void proto_model::compress() { - ptr_vector::iterator it = m_func_decls.begin(); - ptr_vector::iterator end = m_func_decls.end(); - for (; it != end; ++it) { - func_decl * f = *it; + for (func_decl* f : m_func_decls) { func_interp * fi = get_func_interp(f); SASSERT(fi != 0); fi->compress(); @@ -412,17 +410,13 @@ model * proto_model::mk_model() { TRACE("proto_model", tout << "mk_model\n"; model_v2_pp(tout, *this);); model * m = alloc(model, m_manager); - decl2expr::iterator it1 = m_interp.begin(); - decl2expr::iterator end1 = m_interp.end(); - for (; it1 != end1; ++it1) { - m->register_decl(it1->m_key, it1->m_value); + for (auto const& kv : m_interp) { + m->register_decl(kv.m_key, kv.m_value); } - decl2finterp::iterator it2 = m_finterp.begin(); - decl2finterp::iterator end2 = m_finterp.end(); - for (; it2 != end2; ++it2) { - m->register_decl(it2->m_key, it2->m_value); - m_manager.dec_ref(it2->m_key); + for (auto const& kv : m_finterp) { + m->register_decl(kv.m_key, kv.m_value); + m_manager.dec_ref(kv.m_key); } m_finterp.reset(); // m took the ownership of the func_interp's diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h index 1cee04650..a7ec8d3a9 100644 --- a/src/smt/proto_model/proto_model.h +++ b/src/smt/proto_model/proto_model.h @@ -84,6 +84,7 @@ public: // Primitives for building models // void register_aux_decl(func_decl * f, func_interp * fi); + void register_aux_decl(func_decl * f); void reregister_decl(func_decl * f, func_interp * new_fi, func_decl * f_aux); void compress(); void cleanup(); diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 875e7adf2..13651a63c 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -89,10 +89,7 @@ namespace smt { void model_checker::restrict_to_universe(expr * sk, obj_hashtable const & universe) { SASSERT(!universe.empty()); ptr_buffer eqs; - obj_hashtable::iterator it = universe.begin(); - obj_hashtable::iterator end = universe.end(); - for (; it != end; ++it) { - expr * e = *it; + for (expr * e : universe) { eqs.push_back(m.mk_eq(sk, e)); } expr_ref fml(m.mk_or(eqs.size(), eqs.c_ptr()), m); diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 35a98aa01..68d56ea84 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -628,18 +628,14 @@ namespace smt { ptr_vector const & exceptions = n->get_exceptions(); ptr_vector const & avoid_set = n->get_avoid_set(); - ptr_vector::const_iterator it1 = exceptions.begin(); - ptr_vector::const_iterator end1 = exceptions.end(); - for (; it1 != end1; ++it1) { - expr * val = eval(*it1, true); + for (expr* e : exceptions) { + expr * val = eval(e, true); SASSERT(val != 0); r.push_back(val); } - ptr_vector::const_iterator it2 = avoid_set.begin(); - ptr_vector::const_iterator end2 = avoid_set.end(); - for (; it2 != end2; ++it2) { - node * n = (*it2)->get_root(); + for (node* a : avoid_set) { + node * n = a->get_root(); if (!n->is_mono_proj() && n->get_else() != 0) { expr * val = eval(n->get_else(), true); SASSERT(val != 0); @@ -661,11 +657,9 @@ namespace smt { expr * t_result = 0; unsigned gen_result = UINT_MAX; - obj_map::iterator it1 = elems.begin(); - obj_map::iterator end1 = elems.end(); - for (; it1 != end1; ++it1) { - expr * t = (*it1).m_key; - unsigned gen = (*it1).m_value; + for (auto const& kv : elems) { + expr * t = kv.m_key; + unsigned gen = kv.m_value; expr * t_val = eval(t, true); SASSERT(t_val != 0); ptr_buffer::const_iterator it2 = ex_vals.begin(); @@ -699,6 +693,7 @@ namespace smt { if (m_sort2k.find(s, r)) return r; r = m_manager.mk_fresh_const("k", s); + m_model->register_aux_decl(r->get_decl()); m_sort2k.insert(s, r); m_ks.push_back(r); return r; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index bbd11b4bf..d988da54f 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3224,26 +3224,32 @@ void theory_seq::add_indexof_axiom(expr* i) { /* let r = replace(a, s, t) + a = "" => s = "" or r = a + contains(a, s) or r = a + s = "" => r = t+a + tightest_prefix(s, x) (contains(a, s) -> r = xty & a = xsy) & (!contains(a, s) -> r = a) */ void theory_seq::add_replace_axiom(expr* r) { + context& ctx = get_context(); expr* a = 0, *s = 0, *t = 0; VERIFY(m_util.str.is_replace(r, a, s, t)); expr_ref x = mk_skolem(m_indexof_left, a, s); expr_ref y = mk_skolem(m_indexof_right, a, s); expr_ref xty = mk_concat(x, t, y); expr_ref xsy = mk_concat(x, s, y); + literal a_emp = mk_eq_empty(a, true); + literal s_emp = mk_eq_empty(s, true); literal cnt = mk_literal(m_util.str.mk_contains(a, s)); - literal a_emp = mk_eq_empty(a); - literal s_emp = mk_eq_empty(s); add_axiom(~a_emp, s_emp, mk_seq_eq(r, a)); add_axiom(cnt, mk_seq_eq(r, a)); add_axiom(~s_emp, mk_seq_eq(r, mk_concat(t, a))); add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(a, xsy)); add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(r, xty)); + ctx.force_phase(cnt); tightest_prefix(s, x); } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 052fd705f..92ffd8222 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -166,14 +166,18 @@ namespace smt { } } - void theory_str::assert_axiom(expr * e) { + void theory_str::assert_axiom(expr * _e) { if (opt_VerifyFinalCheckProgress) { finalCheckProgressIndicator = true; } - if (get_manager().is_true(e)) return; - TRACE("str", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;); + if (get_manager().is_true(_e)) return; context & ctx = get_context(); + ast_manager& m = get_manager(); + TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;); + expr_ref e(_e, m); + th_rewriter rw(m); + rw(e); if (!ctx.b_internalized(e)) { ctx.internalize(e, false); } @@ -1419,6 +1423,9 @@ namespace smt { void theory_str::instantiate_axiom_Substr(enode * e) { context & ctx = get_context(); ast_manager & m = get_manager(); + expr* substrBase = 0; + expr* substrPos = 0; + expr* substrLen = 0; app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { @@ -1429,12 +1436,7 @@ namespace smt { TRACE("str", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;); - expr_ref substrBase(expr->get_arg(0), m); - expr_ref substrPos(expr->get_arg(1), m); - expr_ref substrLen(expr->get_arg(2), m); - SASSERT(substrBase); - SASSERT(substrPos); - SASSERT(substrLen); + VERIFY(u.str.is_extract(expr, substrBase, substrPos, substrLen)); expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m); expr_ref minusOne(m_autil.mk_numeral(rational::minus_one(), true), m); @@ -1452,28 +1454,19 @@ namespace smt { // len >= 0 argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero)); - expr_ref argumentsValid(mk_and(argumentsValid_terms), m); - SASSERT(argumentsValid); - ctx.internalize(argumentsValid, false); // (pos+len) >= strlen(base) // --> pos + len + -1*strlen(base) >= 0 expr_ref lenOutOfBounds(m_autil.mk_ge( m_autil.mk_add(substrPos, substrLen, m_autil.mk_mul(minusOne, mk_strlen(substrBase))), zero), m); - SASSERT(lenOutOfBounds); - ctx.internalize(argumentsValid, false); + expr_ref argumentsValid = mk_and(argumentsValid_terms); // Case 1: pos < 0 or pos >= strlen(base) or len < 0 // ==> (Substr ...) = "" expr_ref case1_premise(m.mk_not(argumentsValid), m); - SASSERT(case1_premise); - ctx.internalize(case1_premise, false); expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m); - SASSERT(case1_conclusion); - ctx.internalize(case1_conclusion, false); - expr_ref case1(rewrite_implication(case1_premise, case1_conclusion), m); - SASSERT(case1); + expr_ref case1(m.mk_implies(case1_premise, case1_conclusion), m); // Case 2: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) >= strlen(base) // ==> base = t0.t1 AND len(t0) = pos AND (Substr ...) = t1 @@ -1483,8 +1476,7 @@ namespace smt { ctx.mk_eq_atom(substrBase, mk_concat(t0,t1)), ctx.mk_eq_atom(mk_strlen(t0), substrPos), ctx.mk_eq_atom(expr, t1)), m); - expr_ref case2(rewrite_implication(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m); - SASSERT(case2); + expr_ref case2(m.mk_implies(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m); // Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base) // ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3 @@ -1497,16 +1489,11 @@ namespace smt { case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen)); case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3)); expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m); - expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m); - SASSERT(case3); + expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m); - ctx.internalize(case1, false); - ctx.internalize(case2, false); - ctx.internalize(case3, false); - - expr_ref finalAxiom(m.mk_and(case1, case2, case3), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); + assert_axiom(case1); + assert_axiom(case2); + assert_axiom(case3); } void theory_str::instantiate_axiom_Replace(enode * e) { From 9fe9587a9bef7486036d1bdafc32d1125b5f6c3e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Aug 2017 09:14:08 -0700 Subject: [PATCH 2/7] revert local changes to theory_str Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 110 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 103 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 3417fc798..0d963f8b9 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -166,18 +166,14 @@ namespace smt { } } - void theory_str::assert_axiom(expr * _e) { + void theory_str::assert_axiom(expr * e) { if (opt_VerifyFinalCheckProgress) { finalCheckProgressIndicator = true; } - if (get_manager().is_true(_e)) return; + if (get_manager().is_true(e)) return; + TRACE("str", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;); context & ctx = get_context(); - ast_manager& m = get_manager(); - TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;); - expr_ref e(_e, m); - th_rewriter rw(m); - rw(e); if (!ctx.b_internalized(e)) { ctx.internalize(e, false); } @@ -189,6 +185,7 @@ namespace smt { m_trail.push_back(e); //TRACE("str", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;); + } expr * theory_str::rewrite_implication(expr * premise, expr * conclusion) { @@ -1420,6 +1417,104 @@ namespace smt { assert_axiom(finalAxiom); } + void theory_str::instantiate_axiom_Substr(enode * e) { + context & ctx = get_context(); + ast_manager & m = get_manager(); + + app * expr = e->get_owner(); + if (axiomatized_terms.contains(expr)) { + TRACE("str", tout << "already set up Substr axiom for " << mk_pp(expr, m) << std::endl;); + return; + } + axiomatized_terms.insert(expr); + + TRACE("str", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;); + + expr_ref substrBase(expr->get_arg(0), m); + expr_ref substrPos(expr->get_arg(1), m); + expr_ref substrLen(expr->get_arg(2), m); + SASSERT(substrBase); + SASSERT(substrPos); + SASSERT(substrLen); + + expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m); + expr_ref minusOne(m_autil.mk_numeral(rational::minus_one(), true), m); + SASSERT(zero); + SASSERT(minusOne); + + expr_ref_vector argumentsValid_terms(m); + // pos >= 0 + argumentsValid_terms.push_back(m_autil.mk_ge(substrPos, zero)); + // pos < strlen(base) + // --> pos + -1*strlen(base) < 0 + argumentsValid_terms.push_back(m.mk_not(m_autil.mk_ge( + m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)), + zero))); + + // len >= 0 + argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero)); + + expr_ref argumentsValid(mk_and(argumentsValid_terms), m); + SASSERT(argumentsValid); + ctx.internalize(argumentsValid, false); + + // (pos+len) >= strlen(base) + // --> pos + len + -1*strlen(base) >= 0 + expr_ref lenOutOfBounds(m_autil.mk_ge( + m_autil.mk_add(substrPos, substrLen, m_autil.mk_mul(minusOne, mk_strlen(substrBase))), + zero), m); + SASSERT(lenOutOfBounds); + ctx.internalize(argumentsValid, false); + + // Case 1: pos < 0 or pos >= strlen(base) or len < 0 + // ==> (Substr ...) = "" + expr_ref case1_premise(m.mk_not(argumentsValid), m); + SASSERT(case1_premise); + ctx.internalize(case1_premise, false); + expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m); + SASSERT(case1_conclusion); + ctx.internalize(case1_conclusion, false); + expr_ref case1(rewrite_implication(case1_premise, case1_conclusion), m); + SASSERT(case1); + + // Case 2: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) >= strlen(base) + // ==> base = t0.t1 AND len(t0) = pos AND (Substr ...) = t1 + expr_ref t0(mk_str_var("t0"), m); + expr_ref t1(mk_str_var("t1"), m); + expr_ref case2_conclusion(m.mk_and( + ctx.mk_eq_atom(substrBase, mk_concat(t0,t1)), + ctx.mk_eq_atom(mk_strlen(t0), substrPos), + ctx.mk_eq_atom(expr, t1)), m); + expr_ref case2(rewrite_implication(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m); + SASSERT(case2); + + // Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base) + // ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3 + + expr_ref t2(mk_str_var("t2"), m); + expr_ref t3(mk_str_var("t3"), m); + expr_ref t4(mk_str_var("t4"), m); + expr_ref_vector case3_conclusion_terms(m); + case3_conclusion_terms.push_back(ctx.mk_eq_atom(substrBase, mk_concat(t2, mk_concat(t3, t4)))); + case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t2), substrPos)); + case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen)); + case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3)); + expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m); + expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m); + SASSERT(case3); + + ctx.internalize(case1, false); + ctx.internalize(case2, false); + ctx.internalize(case3, false); + + expr_ref finalAxiom(m.mk_and(case1, case2, case3), m); + SASSERT(finalAxiom); + assert_axiom(finalAxiom); + } + +#if 0 + // rewrite + // requires to add th_rewriter to assert_axiom to enforce normal form. void theory_str::instantiate_axiom_Substr(enode * e) { context & ctx = get_context(); ast_manager & m = get_manager(); @@ -1495,6 +1590,7 @@ namespace smt { assert_axiom(case2); assert_axiom(case3); } +#endif void theory_str::instantiate_axiom_Replace(enode * e) { context & ctx = get_context(); From 359ee818a5800e8f0fa00a6c9ee63c690fc00a1a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Aug 2017 15:35:16 -0700 Subject: [PATCH 3/7] purge iterators Signed-off-by: Nikolaj Bjorner --- src/ast/array_decl_plugin.cpp | 4 +- src/ast/array_decl_plugin.h | 2 +- src/smt/proto_model/datatype_factory.cpp | 16 +- src/smt/proto_model/proto_model.cpp | 306 +-------------- src/smt/proto_model/proto_model.h | 3 - src/smt/smt_model_checker.cpp | 34 +- src/smt/smt_model_finder.cpp | 474 ++++++++--------------- 7 files changed, 180 insertions(+), 659 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index efcad1d5e..6296d344a 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -556,9 +556,9 @@ bool array_decl_plugin::is_fully_interp(sort const * s) const { return m_manager->is_fully_interp(get_array_range(s)); } -func_decl * array_recognizers::get_as_array_func_decl(app * n) const { +func_decl * array_recognizers::get_as_array_func_decl(expr * n) const { SASSERT(is_as_array(n)); - return to_func_decl(n->get_decl()->get_parameter(0).get_ast()); + return to_func_decl(to_app(n)->get_decl()->get_parameter(0).get_ast()); } array_util::array_util(ast_manager& m): diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index e06cb3065..0febb82a4 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -148,7 +148,7 @@ public: bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); } bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); } bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); } - func_decl * get_as_array_func_decl(app * n) const; + func_decl * get_as_array_func_decl(expr * n) const; }; class array_util : public array_recognizers { diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp index f5079b0e5..d738f2cbd 100644 --- a/src/smt/proto_model/datatype_factory.cpp +++ b/src/smt/proto_model/datatype_factory.cpp @@ -19,7 +19,6 @@ Revision History: #include "smt/proto_model/datatype_factory.h" #include "smt/proto_model/proto_model.h" #include "ast/ast_pp.h" -#include "ast/ast_ll_pp.h" #include "ast/expr_functors.h" datatype_factory::datatype_factory(ast_manager & m, proto_model & md): @@ -90,10 +89,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) { // If the argumet is a sibling datatype of s, then // use get_last_fresh_value. ptr_vector const * constructors = m_util.get_datatype_constructors(s); - ptr_vector::const_iterator it = constructors->begin(); - ptr_vector::const_iterator end = constructors->end(); - for (; it != end; ++it) { - func_decl * constructor = *it; + for (func_decl * constructor : *constructors) { expr_ref_vector args(m_manager); bool found_fresh_arg = false; bool recursive = false; @@ -156,10 +152,7 @@ expr * datatype_factory::get_fresh_value(sort * s) { // arguments (if the argument is not a sibling datatype of s). // Two datatypes are siblings if they were defined together in the same mutually recursive definition. ptr_vector const * constructors = m_util.get_datatype_constructors(s); - ptr_vector::const_iterator it = constructors->begin(); - ptr_vector::const_iterator end = constructors->end(); - for (; it != end; ++it) { - func_decl * constructor = *it; + for (func_decl * constructor : *constructors) { expr_ref_vector args(m_manager); bool found_fresh_arg = false; unsigned num = constructor->get_arity(); @@ -197,10 +190,7 @@ expr * datatype_factory::get_fresh_value(sort * s) { ++num_iterations; TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";); ptr_vector const * constructors = m_util.get_datatype_constructors(s); - ptr_vector::const_iterator it = constructors->begin(); - ptr_vector::const_iterator end = constructors->end(); - for (; it != end; ++it) { - func_decl * constructor = *it; + for (func_decl * constructor : *constructors) { expr_ref_vector args(m_manager); bool found_sibling = false; unsigned num = constructor->get_arity(); diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 1eed4d0dd..9a5f2a1ca 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -16,33 +16,27 @@ Author: Revision History: --*/ -#include "smt/proto_model/proto_model.h" -#include "model/model_params.hpp" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "ast/rewriter/var_subst.h" -#include "ast/array_decl_plugin.h" #include "ast/well_sorted.h" #include "ast/used_symbols.h" +#include "model/model_params.hpp" #include "model/model_v2_pp.h" +#include "smt/proto_model/proto_model.h" proto_model::proto_model(ast_manager & m, params_ref const & p): model_core(m), - m_afid(m.mk_family_id(symbol("array"))), m_eval(*this), m_rewrite(m) { register_factory(alloc(basic_factory, m)); m_user_sort_factory = alloc(user_sort_factory, m); register_factory(m_user_sort_factory); - m_model_partial = model_params(p).partial(); } - - void proto_model::register_aux_decl(func_decl * d, func_interp * fi) { model_core::register_decl(d, fi); - TRACE("cleanup_bug", tout << "register " << d->get_name() << "\n";); m_aux_decls.insert(d); } @@ -89,21 +83,11 @@ expr * proto_model::mk_some_interp_for(func_decl * d) { } -bool proto_model::is_select_of_model_value(expr* e) const { - return - is_app_of(e, m_afid, OP_SELECT) && - is_as_array(to_app(e)->get_arg(0)) && - has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0)))); -} - bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { m_eval.set_model_completion(model_completion); m_eval.set_expand_array_equalities(false); try { m_eval(e, result); -#if 0 - std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n"; -#endif return true; } catch (model_evaluator_exception & ex) { @@ -163,12 +147,11 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au app * t = to_app(a); bool visited = true; args.reset(); - unsigned num_args = t->get_num_args(); - for (unsigned i = 0; i < num_args; ++i) { + for (expr* t_arg : *t) { expr * arg = 0; - if (!cache.find(t->get_arg(i), arg)) { + if (!cache.find(t_arg, arg)) { visited = false; - todo.push_back(t->get_arg(i)); + todo.push_back(t_arg); } else { args.push_back(arg); @@ -181,7 +164,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au if (m_aux_decls.contains(f)) found_aux_fs.insert(f); expr_ref new_t(m_manager); - new_t = m_rewrite.mk_app(f, num_args, args.c_ptr()); + new_t = m_rewrite.mk_app(f, args.size(), args.c_ptr()); if (t != new_t.get()) trail.push_back(new_t); todo.pop_back(); @@ -230,10 +213,6 @@ void proto_model::cleanup() { cleanup_func_interp(fi, found_aux_fs); } - TRACE("cleanup_bug", - for (func_decl* faux : m_aux_decls) { - tout << faux->get_name() << "\n"; - }); // remove auxiliary declarations that are not used. if (found_aux_fs.size() != m_aux_decls.size()) { remove_aux_decls_not_in_set(m_decls, found_aux_fs); @@ -244,10 +223,6 @@ void proto_model::cleanup() { TRACE("cleanup_bug", tout << "eliminating " << faux->get_name() << "\n";); unregister_decl(faux); } - else { - TRACE("cleanup_bug", tout << "not eliminating " << faux->get_name() << "\n";); - } - } m_aux_decls.swap(found_aux_fs); } @@ -273,8 +248,9 @@ ptr_vector const & proto_model::get_universe(sort * s) const { ptr_vector & tmp = const_cast(this)->m_tmp; tmp.reset(); obj_hashtable const & u = get_known_universe(s); - for (expr * e : u) + for (expr * e : u) { tmp.push_back(e); + } return tmp; } @@ -352,10 +328,6 @@ void proto_model::register_value(expr * n) { } } -bool proto_model::is_as_array(expr * v) const { - return is_app_of(v, m_afid, OP_AS_ARRAY); -} - void proto_model::compress() { for (func_decl* f : m_func_decls) { func_interp * fi = get_func_interp(f); @@ -371,23 +343,9 @@ void proto_model::compress() { void proto_model::complete_partial_func(func_decl * f) { func_interp * fi = get_func_interp(f); if (fi && fi->is_partial()) { - expr * else_value = 0; -#if 0 - // For UFBV benchmarks, setting the "else" to false is not a good idea. - // TODO: find a permanent solution. A possibility is to add another option. - if (m_manager.is_bool(f->get_range())) { - else_value = m_manager.mk_false(); - } - else { - else_value = fi->get_max_occ_result(); - if (else_value == 0) - else_value = get_some_value(f->get_range()); - } -#else - else_value = fi->get_max_occ_result(); + expr * else_value = fi->get_max_occ_result(); if (else_value == 0) else_value = get_some_value(f->get_range()); -#endif fi->set_else(else_value); } } @@ -401,8 +359,8 @@ void proto_model::complete_partial_funcs() { // m_func_decls may be "expanded" when we invoke get_some_value. // So, we must not use iterators to traverse it. - for (unsigned i = 0; i < m_func_decls.size(); i++) { - complete_partial_func(m_func_decls[i]); + for (func_decl* f : m_func_decls) { + complete_partial_func(f); } } @@ -431,245 +389,3 @@ model * proto_model::mk_model() { return m; } - - -#if 0 - -#include "ast/simplifier/simplifier.h" -#include "ast/simplifier/basic_simplifier_plugin.h" - -// Auxiliary function for computing fi(args[0], ..., args[fi.get_arity() - 1]). -// The result is stored in result. -// Return true if succeeded, and false otherwise. -// It uses the simplifier s during the computation. -bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & result) { - bool actuals_are_values = true; - - if (fi.num_entries() != 0) { - for (unsigned i = 0; actuals_are_values && i < fi.get_arity(); i++) { - actuals_are_values = fi.m().is_value(args[i]); - } - } - - func_entry * entry = fi.get_entry(args); - if (entry != 0) { - result = entry->get_result(); - return true; - } - - TRACE("func_interp", tout << "failed to find entry for: "; - for(unsigned i = 0; i < fi.get_arity(); i++) - tout << mk_pp(args[i], fi.m()) << " "; - tout << "\nis partial: " << fi.is_partial() << "\n";); - - if (!fi.eval_else(args, result)) { - return false; - } - - if (actuals_are_values && fi.args_are_values()) { - // cheap case... we are done - return true; - } - - // build symbolic result... the actuals may be equal to the args of one of the entries. - basic_simplifier_plugin * bs = static_cast(s.get_plugin(fi.m().get_basic_family_id())); - for (unsigned k = 0; k < fi.num_entries(); k++) { - func_entry const * curr = fi.get_entry(k); - SASSERT(!curr->eq_args(fi.m(), fi.get_arity(), args)); - if (!actuals_are_values || !curr->args_are_values()) { - expr_ref_buffer eqs(fi.m()); - unsigned i = fi.get_arity(); - while (i > 0) { - --i; - expr_ref new_eq(fi.m()); - bs->mk_eq(curr->get_arg(i), args[i], new_eq); - eqs.push_back(new_eq); - } - SASSERT(eqs.size() == fi.get_arity()); - expr_ref new_cond(fi.m()); - bs->mk_and(eqs.size(), eqs.c_ptr(), new_cond); - bs->mk_ite(new_cond, curr->get_result(), result, result); - } - } - return true; -} - - -bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { - bool is_ok = true; - SASSERT(is_well_sorted(m_manager, e)); - TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n"; - tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";); - - obj_map eval_cache; - expr_ref_vector trail(m_manager); - sbuffer, 128> todo; - ptr_buffer args; - expr * null = static_cast(0); - todo.push_back(std::make_pair(e, null)); - - simplifier m_simplifier(m_manager); - - expr * a; - expr * expanded_a; - while (!todo.empty()) { - std::pair & p = todo.back(); - a = p.first; - expanded_a = p.second; - if (expanded_a != 0) { - expr * r = 0; - eval_cache.find(expanded_a, r); - SASSERT(r != 0); - todo.pop_back(); - eval_cache.insert(a, r); - TRACE("model_eval", - tout << "orig:\n" << mk_pp(a, m_manager) << "\n"; - tout << "after beta reduction:\n" << mk_pp(expanded_a, m_manager) << "\n"; - tout << "new:\n" << mk_pp(r, m_manager) << "\n";); - } - else { - switch(a->get_kind()) { - case AST_APP: { - app * t = to_app(a); - bool visited = true; - args.reset(); - unsigned num_args = t->get_num_args(); - for (unsigned i = 0; i < num_args; ++i) { - expr * arg = 0; - if (!eval_cache.find(t->get_arg(i), arg)) { - visited = false; - todo.push_back(std::make_pair(t->get_arg(i), null)); - } - else { - args.push_back(arg); - } - } - if (!visited) { - continue; - } - SASSERT(args.size() == t->get_num_args()); - expr_ref new_t(m_manager); - func_decl * f = t->get_decl(); - - if (!has_interpretation(f)) { - // the model does not assign an interpretation to f. - SASSERT(new_t.get() == 0); - if (f->get_family_id() == null_family_id) { - if (model_completion) { - // create an interpretation for f. - new_t = mk_some_interp_for(f); - } - else { - TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";); - is_ok = false; - } - } - if (new_t.get() == 0) { - // t is interpreted or model completion is disabled. - m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t); - TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";); - trail.push_back(new_t); - if (!is_app(new_t) || to_app(new_t)->get_decl() != f || is_select_of_model_value(new_t)) { - // if the result is not of the form (f ...), then assume we must simplify it. - expr * new_new_t = 0; - if (!eval_cache.find(new_t.get(), new_new_t)) { - todo.back().second = new_t; - todo.push_back(std::make_pair(new_t, null)); - continue; - } - else { - new_t = new_new_t; - } - } - } - } - else { - // the model has an interpretaion for f. - if (num_args == 0) { - // t is a constant - new_t = get_const_interp(f); - } - else { - // t is a function application - SASSERT(new_t.get() == 0); - // try to use function graph first - func_interp * fi = get_func_interp(f); - SASSERT(fi->get_arity() == num_args); - expr_ref r1(m_manager); - // fi may be partial... - if (!::eval(*fi, m_simplifier, args.c_ptr(), r1)) { - SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial. - if (model_completion) { - expr * r = get_some_value(f->get_range()); - fi->set_else(r); - SASSERT(!fi->is_partial()); - new_t = r; - } - else { - // f is an uninterpreted function, there is no need to use m_simplifier.mk_app - new_t = m_manager.mk_app(f, num_args, args.c_ptr()); - trail.push_back(new_t); - TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";); - is_ok = false; - } - } - else { - SASSERT(r1); - trail.push_back(r1); - TRACE("model_eval", tout << mk_pp(a, m_manager) << "\nevaluates to: " << r1 << "\n";); - expr * r2 = 0; - if (!eval_cache.find(r1.get(), r2)) { - todo.back().second = r1; - todo.push_back(std::make_pair(r1, null)); - continue; - } - else { - new_t = r2; - } - } - } - } - TRACE("model_eval", - tout << "orig:\n" << mk_pp(t, m_manager) << "\n"; - tout << "new:\n" << mk_pp(new_t, m_manager) << "\n";); - todo.pop_back(); - SASSERT(new_t.get() != 0); - eval_cache.insert(t, new_t); - break; - } - case AST_VAR: - SASSERT(a != 0); - eval_cache.insert(a, a); - todo.pop_back(); - break; - case AST_QUANTIFIER: - TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";); - is_ok = false; // evaluator does not handle quantifiers. - SASSERT(a != 0); - eval_cache.insert(a, a); - todo.pop_back(); - break; - default: - UNREACHABLE(); - break; - } - } - } - - if (!eval_cache.find(e, a)) { - TRACE("model_eval", tout << "FAILED e: " << mk_bounded_pp(e, m_manager) << "\n";); - UNREACHABLE(); - } - - result = a; - std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n"; - TRACE("model_eval", - ast_ll_pp(tout << "original: ", m_manager, e); - ast_ll_pp(tout << "evaluated: ", m_manager, a); - ast_ll_pp(tout << "reduced: ", m_manager, result.get()); - tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n"; - ); - SASSERT(is_well_sorted(m_manager, result.get())); - return is_ok; -} -#endif diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h index a7ec8d3a9..05af0091c 100644 --- a/src/smt/proto_model/proto_model.h +++ b/src/smt/proto_model/proto_model.h @@ -41,7 +41,6 @@ Revision History: class proto_model : public model_core { plugin_manager m_factories; user_sort_factory * m_user_sort_factory; - family_id m_afid; //!< array family id: hack for displaying models in V1.x style func_decl_set m_aux_decls; ptr_vector m_tmp; model_evaluator m_eval; @@ -58,7 +57,6 @@ class proto_model : public model_core { void remove_aux_decls_not_in_set(ptr_vector & decls, func_decl_set const & s); void cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs); - bool is_select_of_model_value(expr* e) const; public: proto_model(ast_manager & m, params_ref const & p = params_ref()); @@ -68,7 +66,6 @@ public: bool eval(expr * e, expr_ref & result, bool model_completion = false); - bool is_as_array(expr * v) const; value_factory * get_factory(family_id fid); diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 13651a63c..f72485d0e 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -17,16 +17,15 @@ Revision History: --*/ -#include "smt/smt_model_checker.h" -#include "smt/smt_context.h" -#include "smt/smt_model_finder.h" #include "ast/normal_forms/pull_quant.h" #include "ast/for_each_expr.h" #include "ast/rewriter/var_subst.h" #include "ast/ast_pp.h" -#include "ast/ast_ll_pp.h" -#include "model/model_pp.h" #include "ast/ast_smt2_pp.h" +#include "smt/smt_model_checker.h" +#include "smt/smt_context.h" +#include "smt/smt_model_finder.h" +#include "model/model_pp.h" namespace smt { @@ -65,11 +64,9 @@ namespace smt { expr * model_checker::get_term_from_ctx(expr * val) { if (m_value2expr.empty()) { // populate m_value2expr - obj_map::iterator it = m_root2value->begin(); - obj_map::iterator end = m_root2value->end(); - for (; it != end; ++it) { - enode * n = (*it).m_key; - expr * val = (*it).m_value; + for (auto const& kv : *m_root2value) { + enode * n = kv.m_key; + expr * val = kv.m_value; n = n->get_eq_enode_with_min_gen(); m_value2expr.insert(val, n->get_owner()); } @@ -198,9 +195,8 @@ namespace smt { void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) { SASSERT(q->get_num_decls() == bindings.size()); - - for (unsigned i = 0; i < bindings.size(); i++) - m_pinned_exprs.push_back(bindings[i]); + for (expr* b : bindings) + m_pinned_exprs.push_back(b); m_pinned_exprs.push_back(q); void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls())); @@ -234,10 +230,8 @@ namespace smt { bool model_checker::add_blocking_clause(model * cex, expr_ref_vector & sks) { SASSERT(cex != 0); - unsigned num_sks = sks.size(); expr_ref_buffer diseqs(m); - for (unsigned i = 0; i < num_sks; i++) { - expr * sk = sks.get(i); + for (expr * sk : sks) { func_decl * sk_d = to_app(sk)->get_decl(); expr_ref sk_value(m); sk_value = cex->get_const_interp(sk_d); @@ -269,8 +263,7 @@ namespace smt { assert_neg_q_m(flat_q, sks); TRACE("model_checker", tout << "skolems:\n"; - for (unsigned i = 0; i < sks.size(); i++) { - expr * sk = sks.get(i); + for (expr* sk : sks) { tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n"; }); @@ -483,10 +476,7 @@ namespace smt { TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";); ptr_buffer bindings; ptr_vector dummy; - ptr_vector::iterator it = m_new_instances.begin(); - ptr_vector::iterator end = m_new_instances.end(); - for (; it != end; ++it) { - instance * inst = *it; + for (instance* inst : m_new_instances) { quantifier * q = inst->m_q; if (m_context->b_internalized(q)) { bindings.reset(); diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 68d56ea84..73d1e9f22 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -16,8 +16,8 @@ Author: Revision History: --*/ -#include "smt/smt_model_finder.h" -#include "smt/smt_context.h" +#include "util/cooperate.h" +#include "util/backtrackable_set.h" #include "ast/ast_util.h" #include "ast/macros/macro_util.h" #include "ast/arith_decl_plugin.h" @@ -27,14 +27,14 @@ Revision History: #include "ast/simplifier/bv_simplifier_plugin.h" #include "ast/normal_forms/pull_quant.h" #include "ast/rewriter/var_subst.h" -#include "util/backtrackable_set.h" #include "ast/for_each_expr.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "ast/well_sorted.h" -#include "model/model_pp.h" #include "ast/ast_smt2_pp.h" -#include "util/cooperate.h" +#include "model/model_pp.h" +#include "smt/smt_model_finder.h" +#include "smt/smt_context.h" #include "tactic/tactic_exception.h" namespace smt { @@ -56,11 +56,9 @@ namespace smt { v1.swap(v2); return; } - typename ptr_vector::iterator it = v2.begin(); - typename ptr_vector::iterator end = v2.end(); - for (; it != end; ++it) { - if (!v1.contains(*it)) - v1.push_back(*it); + for (T* t : v2) { + if (!v1.contains(t)) + v1.push_back(t); } v2.finalize(); } @@ -88,10 +86,8 @@ namespace smt { instantiation_set(ast_manager & m):m_manager(m) {} ~instantiation_set() { - obj_map::iterator it = m_elems.begin(); - obj_map::iterator end = m_elems.end(); - for (; it != end; ++it) { - m_manager.dec_ref((*it).m_key); + for (auto const& kv : m_elems) { + m_manager.dec_ref(kv.m_key); } m_elems.reset(); } @@ -116,16 +112,12 @@ namespace smt { } void display(std::ostream & out) const { - obj_map::iterator it = m_elems.begin(); - obj_map::iterator end = m_elems.end(); - for (; it != end; ++it) { - out << mk_bounded_pp((*it).m_key, m_manager) << " [" << (*it).m_value << "]\n"; + for (auto const& kv : m_elems) { + out << mk_bounded_pp(kv.m_key, m_manager) << " [" << kv.m_value << "]\n"; } out << "inverse:\n"; - obj_map::iterator it2 = m_inv.begin(); - obj_map::iterator end2 = m_inv.end(); - for (; it2 != end2; ++it2) { - out << mk_bounded_pp((*it2).m_key, m_manager) << " -> " << mk_bounded_pp((*it2).m_value, m_manager) << "\n"; + for (auto const& kv : m_inv) { + out << mk_bounded_pp(kv.m_key, m_manager) << " -> " << mk_bounded_pp(kv.m_value, m_manager) << "\n"; } } @@ -142,12 +134,10 @@ namespace smt { } void mk_inverse(evaluator & ev) { - obj_map::iterator it = m_elems.begin(); - obj_map::iterator end = m_elems.end(); - for (; it != end; ++it) { - expr * t = (*it).m_key; + for (auto const& kv : m_elems) { + expr * t = kv.m_key; SASSERT(!contains_model_value(t)); - unsigned gen = (*it).m_value; + unsigned gen = kv.m_value; expr * t_val = ev.eval(t, true); if (!t_val) break; TRACE("model_finder", tout << mk_pp(t, m_manager) << " " << mk_pp(t_val, m_manager) << "\n";); @@ -329,17 +319,13 @@ namespace smt { out << "root node ------\n"; out << "@" << m_id << " mono: " << m_mono_proj << " signed: " << m_signed_proj << ", sort: " << mk_pp(m_sort, m) << "\n"; out << "avoid-set: "; - ptr_vector::const_iterator it1 = m_avoid_set.begin(); - ptr_vector::const_iterator end1 = m_avoid_set.end(); - for (; it1 != end1; ++it1) { - out << "@" << (*it1)->get_root()->get_id() << " "; + for (node* n : m_avoid_set) { + out << "@" << n->get_root()->get_id() << " "; } out << "\n"; out << "exceptions: "; - ptr_vector::const_iterator it2 = m_exceptions.begin(); - ptr_vector::const_iterator end2 = m_exceptions.end(); - for (; it2 != end2; ++it2) { - out << mk_bounded_pp((*it2), m) << " "; + for (expr * e : m_exceptions) { + out << mk_bounded_pp(e, m) << " "; } out << "\n"; if (m_else) @@ -368,10 +354,8 @@ namespace smt { // return true if m_avoid_set.contains(this) bool must_avoid_itself() const { node * r = get_root(); - ptr_vector::const_iterator it = m_avoid_set.begin(); - ptr_vector::const_iterator end = m_avoid_set.end(); - for (; it != end; ++it) { - if (r == (*it)->get_root()) + for (node* n : m_avoid_set) { + if (r == n->get_root()) return true; } return false; @@ -460,23 +444,19 @@ namespace smt { } void display_key2node(std::ostream & out, key2node const & m) const { - key2node::iterator it = m.begin(); - key2node::iterator end = m.end(); - for (; it != end; ++it) { - ast * a = (*it).m_key.first; - unsigned i = (*it).m_key.second; - node * n = (*it).m_value; + for (auto const& kv : m) { + ast * a = kv.m_key.first; + unsigned i = kv.m_key.second; + node * n = kv.m_value; out << "#" << a->get_id() << ":" << i << " -> @" << n->get_id() << "\n"; } } void display_A_f_is(std::ostream & out) const { - key2node::iterator it = m_A_f_is.begin(); - key2node::iterator end = m_A_f_is.end(); - for (; it != end; ++it) { - func_decl * f = static_cast((*it).m_key.first); - unsigned i = (*it).m_key.second; - node * n = (*it).m_value; + for (auto const& kv : m_A_f_is) { + func_decl * f = static_cast(kv.m_key.first); + unsigned i = kv.m_key.second; + node * n = kv.m_value; out << f->get_name() << ":" << i << " -> @" << n->get_id() << "\n"; } } @@ -556,10 +536,7 @@ namespace smt { } void mk_instantiation_sets() { - ptr_vector::const_iterator it = m_nodes.begin(); - ptr_vector::const_iterator end = m_nodes.end(); - for (; it != end; ++it) { - node * curr = *it; + for (node* curr : m_nodes) { if (curr->is_root()) { curr->mk_instantiation_set(m_manager); } @@ -569,22 +546,19 @@ namespace smt { // For each instantiation_set, reemove entries that do not evaluate to values. void cleanup_instantiation_sets() { ptr_vector to_delete; - ptr_vector::const_iterator it = m_nodes.begin(); - ptr_vector::const_iterator end = m_nodes.end(); - for (; it != end; ++it) { - node * curr = *it; + for (node * curr : m_nodes) { if (curr->is_root()) { instantiation_set * s = curr->get_instantiation_set(); to_delete.reset(); obj_map const & elems = s->get_elems(); - for (obj_map::iterator it = elems.begin(); it != elems.end(); it++) { - expr * n = it->m_key; + for (auto const& kv : elems) { + expr * n = kv.m_key; expr * n_val = eval(n, true); if (!n_val || !m_manager.is_value(n_val)) to_delete.push_back(n); } - for (ptr_vector::iterator it = to_delete.begin(); it != to_delete.end(); it++) { - s->remove(*it); + for (expr* e : to_delete) { + s->remove(e); } } } @@ -592,11 +566,9 @@ namespace smt { void display_nodes(std::ostream & out) const { display_key2node(out, m_uvars); - display_A_f_is(out); - ptr_vector::const_iterator it = m_nodes.begin(); - ptr_vector::const_iterator end = m_nodes.end(); - for (; it != end; ++it) { - (*it)->display(out, m_manager); + display_A_f_is(out); + for (node* n : m_nodes) { + n->display(out, m_manager); } } @@ -662,13 +634,14 @@ namespace smt { unsigned gen = kv.m_value; expr * t_val = eval(t, true); SASSERT(t_val != 0); - ptr_buffer::const_iterator it2 = ex_vals.begin(); - ptr_buffer::const_iterator end2 = ex_vals.end(); - for (; it2 != end2; ++it2) { - if (!m_manager.are_distinct(t_val, *it2)) + bool found = false; + for (expr* v : ex_vals) { + if (!m_manager.are_distinct(t_val, v)) { + found = true; break; + } } - if (it2 == end2 && (t_result == 0 || gen < gen_result)) { + if (!found && (t_result == 0 || gen < gen_result)) { t_result = t; gen_result = gen; } @@ -729,14 +702,11 @@ namespace smt { */ bool assert_k_diseq_exceptions(app * k, ptr_vector const & exceptions) { TRACE("assert_k_diseq_exceptions", tout << "assert_k_diseq_exceptions, " << "k: " << mk_pp(k, m_manager) << "\nexceptions:\n"; - for (unsigned i = 0; i < exceptions.size(); i++) tout << mk_pp(exceptions[i], m_manager) << "\n";); + for (expr * e : exceptions) tout << mk_pp(e, m_manager) << "\n";); expr * k_interp = get_k_interp(k); if (k_interp == 0) return false; - ptr_vector::const_iterator it = exceptions.begin(); - ptr_vector::const_iterator end = exceptions.end(); - for (; it != end; ++it) { - expr * ex = *it; + for (expr * ex : exceptions) { expr * ex_val = eval(ex, true); if (!m_manager.are_distinct(k_interp, ex_val)) { SASSERT(m_new_constraints); @@ -801,10 +771,7 @@ namespace smt { expr_ref one(m_manager); one = ps->mk_one(); ptr_vector const & exceptions = n->get_exceptions(); - ptr_vector::const_iterator it = exceptions.begin(); - ptr_vector::const_iterator end = exceptions.end(); - for (; it != end; ++it) { - expr * e = *it; + for (expr * e : exceptions) { expr_ref e_plus_1(m_manager); expr_ref e_minus_1(m_manager); TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m_manager) << "\none:\n" << mk_ismt2_pp(one, m_manager) << "\n";); @@ -820,10 +787,8 @@ namespace smt { instantiation_set const * s = n->get_instantiation_set(); obj_hashtable already_found; obj_map const & elems = s->get_elems(); - obj_map::iterator it = elems.begin(); - obj_map::iterator end = elems.end(); - for (; it != end; ++it) { - expr * t = (*it).m_key; + for (auto const& kv : elems) { + expr * t = kv.m_key; expr * t_val = eval(t, true); if (t_val && !already_found.contains(t_val)) { values.push_back(t_val); @@ -831,10 +796,7 @@ namespace smt { } } TRACE("model_finder_bug", tout << "values for the instantiation_set of @" << n->get_id() << "\n"; - ptr_buffer::const_iterator it = values.begin(); - ptr_buffer::const_iterator end = values.end(); - for (; it != end; ++it) { - expr * v = *it; + for (expr * v : values) { tout << mk_pp(v, m_manager) << "\n"; }); } @@ -936,10 +898,7 @@ namespace smt { } void mk_projections() { - ptr_vector::const_iterator it = m_root_nodes.begin(); - ptr_vector::const_iterator end = m_root_nodes.end(); - for (; it != end; ++it) { - node * n = *it; + for (node * n : m_root_nodes) { SASSERT(n->is_root()); if (n->is_mono_proj()) mk_mono_proj(n); @@ -952,10 +911,8 @@ namespace smt { \brief Store in r the partial functions that have A_f_i nodes. */ void collect_partial_funcs(func_decl_set & r) { - key2node::iterator it = m_A_f_is.begin(); - key2node::iterator end = m_A_f_is.end(); - for (; it != end; ++it) { - func_decl * f = to_func_decl((*it).m_key.first); + for (auto const& kv : m_A_f_is) { + func_decl * f = to_func_decl(kv.m_key.first); if (!r.contains(f)) { func_interp * fi = m_model->get_func_interp(f); if (fi == 0) { @@ -978,10 +935,7 @@ namespace smt { for more details. */ void mk_sorts_finite() { - ptr_vector::const_iterator it = m_root_nodes.begin(); - ptr_vector::const_iterator end = m_root_nodes.end(); - for (; it != end; ++it) { - node * n = *it; + for (node * n : m_root_nodes) { SASSERT(n->is_root()); sort * s = n->get_sort(); if (m_manager.is_uninterp(s) && @@ -993,13 +947,10 @@ namespace smt { } } - void add_elem_to_empty_inst_sets() { - ptr_vector::const_iterator it = m_root_nodes.begin(); - ptr_vector::const_iterator end = m_root_nodes.end(); + void add_elem_to_empty_inst_sets() { obj_map sort2elems; ptr_vector need_fresh; - for (; it != end; ++it) { - node * n = *it; + for (node * n : m_root_nodes) { SASSERT(n->is_root()); instantiation_set const * s = n->get_instantiation_set(); TRACE("model_finder", s->display(tout);); @@ -1042,10 +993,7 @@ namespace smt { */ void collect_root_nodes() { m_root_nodes.reset(); - ptr_vector::const_iterator it = m_nodes.begin(); - ptr_vector::const_iterator end = m_nodes.end(); - for (; it != end; ++it) { - node * n = *it; + for (node * n : m_nodes) { if (n->is_root()) m_root_nodes.push_back(n); } @@ -1080,10 +1028,7 @@ namespace smt { collected in the beginning of fix_model(). */ void complete_partial_funcs(func_decl_set const & partial_funcs) { - func_decl_set::iterator it = partial_funcs.begin(); - func_decl_set::iterator end = partial_funcs.end(); - for (; it != end; ++it) { - func_decl * f = *it; + for (func_decl * f : partial_funcs) { // Complete the current interpretation m_model->complete_partial_func(f); @@ -1124,10 +1069,7 @@ namespace smt { } void mk_inverses() { - ptr_vector::const_iterator it = m_root_nodes.begin(); - ptr_vector::const_iterator end = m_root_nodes.end(); - for (; it != end; ++it) { - node * n = *it; + for (node * n : m_root_nodes) { SASSERT(n->is_root()); mk_inverse(n); } @@ -1355,16 +1297,14 @@ namespace smt { ps = bs; instantiation_set const * from_s = from->get_instantiation_set(); obj_map const & elems_s = from_s->get_elems(); - obj_map::iterator it = elems_s.begin(); - obj_map::iterator end = elems_s.end(); - for (; it != end; ++it) { - expr * n = (*it).m_key; + for (auto const& kv : elems_s) { + expr * n = kv.m_key; expr_ref n_k(m_offset.get_manager()); if (PLUS) ps->mk_add(n, m_offset, n_k); else ps->mk_sub(n, m_offset, n_k); - to->insert(n_k, (*it).m_value); + to->insert(n_k, kv.m_value); } } @@ -1409,10 +1349,7 @@ namespace smt { app * nested_array = to_app(auf_arr->get_arg(0)); ptr_buffer nested_arrays; get_auf_arrays(nested_array, ctx, nested_arrays); - ptr_buffer::const_iterator it = nested_arrays.begin(); - ptr_buffer::const_iterator end = nested_arrays.end(); - for (; it != end; ++it) { - enode * curr = *it; + for (enode * curr : nested_arrays) { enode_vector::iterator it2 = curr->begin_parents(); enode_vector::iterator end2 = curr->end_parents(); for (; it2 != end2; ++it2) { @@ -1428,6 +1365,7 @@ namespace smt { class select_var : public qinfo { protected: ast_manager & m_manager; + array_util m_array; app * m_select; // It must satisfy is_auf_select... see bool is_auf_select(expr * t) const unsigned m_arg_i; unsigned m_var_j; @@ -1436,13 +1374,13 @@ namespace smt { func_decl * get_array_func_decl(app * ground_array, auf_solver & s) { expr * ground_array_interp = s.eval(ground_array, false); - if (ground_array_interp != 0 && s.get_model()->is_as_array(ground_array_interp)) - return to_func_decl(to_app(ground_array_interp)->get_decl()->get_parameter(0).get_ast()); + if (ground_array_interp != 0 && m_array.is_as_array(ground_array_interp)) + return m_array.get_as_array_func_decl(ground_array_interp); return 0; } public: - select_var(ast_manager & m, app * s, unsigned i, unsigned j):m_manager(m), m_select(s), m_arg_i(i), m_var_j(j) {} + select_var(ast_manager & m, app * s, unsigned i, unsigned j):m_manager(m), m_array(m), m_select(s), m_arg_i(i), m_var_j(j) {} virtual ~select_var() {} virtual char const * get_kind() const { @@ -1465,16 +1403,12 @@ namespace smt { get_auf_arrays(get_array(), ctx, arrays); TRACE("select_var", tout << "enodes matching: "; display(tout); tout << "\n"; - ptr_buffer::const_iterator it = arrays.begin(); - ptr_buffer::const_iterator end = arrays.end(); - for (; it != end; ++it) { - tout << "#" << (*it)->get_owner()->get_id() << "\n" << mk_pp((*it)->get_owner(), m_manager) << "\n"; + for (enode* n : arrays) { + tout << "#" << n->get_owner()->get_id() << "\n" << mk_pp(n->get_owner(), m_manager) << "\n"; }); node * n1 = s.get_uvar(q, m_var_j); - ptr_buffer::const_iterator it = arrays.begin(); - ptr_buffer::const_iterator end = arrays.end(); - for (; it != end; ++it) { - app * ground_array = (*it)->get_owner(); + for (enode* n : arrays) { + app * ground_array = n->get_owner(); func_decl * f = get_array_func_decl(ground_array, s); if (f) { SASSERT(m_arg_i >= 1); @@ -1487,10 +1421,7 @@ namespace smt { virtual void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) { ptr_buffer arrays; get_auf_arrays(get_array(), ctx, arrays); - ptr_buffer::const_iterator it = arrays.begin(); - ptr_buffer::const_iterator end = arrays.end(); - for (; it != end; ++it) { - enode * curr = (*it); + for (enode * curr : arrays) { app * ground_array = curr->get_owner(); func_decl * f = get_array_func_decl(ground_array, s); if (f) { @@ -1773,11 +1704,9 @@ namespace smt { void insert_qinfo(qinfo * qi) { // I'm assuming the number of qinfo's per quantifier is small. So, the linear search is not a big deal. scoped_ptr q(qi); - ptr_vector::iterator it = m_qinfo_vect.begin(); - ptr_vector::iterator end = m_qinfo_vect.end(); - for (; it != end; ++it) { + for (qinfo* qi2 : m_qinfo_vect) { checkpoint(); - if (qi->is_equal(*it)) { + if (qi->is_equal(qi2)) { return; } } @@ -1871,22 +1800,16 @@ namespace smt { out << "IS_AUF: " << m_is_auf << ", has x=y: " << m_has_x_eq_y << "\n"; out << "unary function fragment: " << unary_function_fragment() << "\n"; out << "ng decls: "; - func_decl_set::iterator it1 = m_ng_decls.begin(); - func_decl_set::iterator end1 = m_ng_decls.end(); - for (; it1 != end1; ++it1) { - out << (*it1)->get_name() << " "; + for (func_decl * f : m_ng_decls) { + out << f->get_name() << " "; } out << "\ninfo bits:\n"; - ptr_vector::const_iterator it2 = m_qinfo_vect.begin(); - ptr_vector::const_iterator end2 = m_qinfo_vect.end(); - for (; it2 != end2; ++it2) { - out << " "; (*it2)->display(out); out << "\n"; + for (qinfo* qi : m_qinfo_vect) { + out << " "; qi->display(out); out << "\n"; } out << "\nmacros:\n"; - ptr_vector::const_iterator it3 = m_cond_macros.begin(); - ptr_vector::const_iterator end3 = m_cond_macros.end(); - for (; it3 != end3; ++it3) { - out << " "; (*it3)->display(out); out << "\n"; + for (cond_macro* cm : m_cond_macros) { + out << " "; cm->display(out); out << "\n"; } } @@ -1895,23 +1818,19 @@ namespace smt { // make sure a node exists for each variable. s.get_uvar(m_flat_q, i); } - ptr_vector::const_iterator it = m_qinfo_vect.begin(); - ptr_vector::const_iterator end = m_qinfo_vect.end(); - for (; it != end; ++it) { - (*it)->process_auf(m_flat_q, s, ctx); + for (qinfo * qi : m_qinfo_vect) { + qi->process_auf(m_flat_q, s, ctx); } } void populate_inst_sets(auf_solver & s, context * ctx) { - ptr_vector::const_iterator it = m_qinfo_vect.begin(); - ptr_vector::const_iterator end = m_qinfo_vect.end(); - for (; it != end; ++it) - (*it)->populate_inst_sets(m_flat_q, s, ctx); + for (qinfo * qi : m_qinfo_vect) { + qi->populate_inst_sets(m_flat_q, s, ctx); + } // second pass - it = m_qinfo_vect.begin(); - for (; it != end; ++it) { + for (qinfo * qi : m_qinfo_vect) { checkpoint(); - (*it)->populate_inst_sets2(m_flat_q, s, ctx); + qi->populate_inst_sets2(m_flat_q, s, ctx); } } @@ -1924,14 +1843,9 @@ namespace smt { if (m_uvar_inst_sets != 0) return; m_uvar_inst_sets = alloc(ptr_vector); - ptr_vector::const_iterator it = m_qinfo_vect.begin(); - ptr_vector::const_iterator end = m_qinfo_vect.end(); - for (; it != end; ++it) - (*it)->populate_inst_sets(m_flat_q, m_the_one, *m_uvar_inst_sets, ctx); - ptr_vector::iterator it2 = m_uvar_inst_sets->begin(); - ptr_vector::iterator end2 = m_uvar_inst_sets->end(); - for (; it2 != end2; ++it2) { - instantiation_set * s = *it2; + for (qinfo* qi : m_qinfo_vect) + qi->populate_inst_sets(m_flat_q, m_the_one, *m_uvar_inst_sets, ctx); + for (instantiation_set * s : *m_uvar_inst_sets) { if (s != 0) s->mk_inverse(ev); } @@ -2225,9 +2139,7 @@ namespace smt { expr * a = to_app(t)->get_arg(0); if (!is_ground(a) && !is_auf_select(a)) return false; - unsigned num_args = to_app(t)->get_num_args(); - for (unsigned i = 1; i < num_args; i++) { - expr * arg = to_app(t)->get_arg(i); + for (expr * arg : *to_app(t)) { if (!is_ground(arg) && !is_var(arg)) return false; } @@ -2253,9 +2165,9 @@ namespace smt { } } else { - unsigned num_args = t->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - visit_term(t->get_arg(i)); + for (expr * arg : *t) { + visit_term(arg); + } } } @@ -2572,10 +2484,7 @@ namespace smt { \brief Return true if \c f is in (qs\{q}) */ bool contains(func_decl * f, ptr_vector const & qs, quantifier * q) { - ptr_vector::const_iterator it = qs.begin(); - ptr_vector::const_iterator end = qs.end(); - for (; it != end; ++it) { - quantifier * other = *it; + for (quantifier * other : qs) { if (q == other) continue; quantifier_info * other_qi = get_qinfo(other); @@ -2614,13 +2523,11 @@ namespace smt { virtual bool process(ptr_vector const & qs, ptr_vector & new_qs, ptr_vector & residue) { bool removed = false; - ptr_vector::const_iterator it = qs.begin(); - ptr_vector::const_iterator end = qs.end(); - for (; it != end; ++it) { - if (process(*it, qs)) + for (quantifier* q : qs) { + if (process(q, qs)) removed = true; else - new_qs.push_back(*it); + new_qs.push_back(q); } return removed; } @@ -2769,20 +2676,15 @@ namespace smt { void register_decls_as_forbidden(quantifier * q) { quantifier_info * qi = get_qinfo(q); func_decl_set const & ng_decls = qi->get_ng_decls(); - func_decl_set::iterator it = ng_decls.begin(); - func_decl_set::iterator end = ng_decls.end(); - for (; it != end; ++it) { - m_forbidden.insert(*it); + for (func_decl* f : ng_decls) { + m_forbidden.insert(f); } } void preprocess(ptr_vector const & qs, ptr_vector & qcandidates, ptr_vector & non_qcandidates) { ptr_vector curr(qs); while (true) { - ptr_vector::iterator it = curr.begin(); - ptr_vector::iterator end = curr.end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : curr) { if (is_candidate(q)) { qcandidates.push_back(q); } @@ -2800,16 +2702,10 @@ namespace smt { } void mk_q_f_defs(ptr_vector const & qs) { - ptr_vector::const_iterator it = qs.begin(); - ptr_vector::const_iterator end = qs.end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : qs) { quantifier_info * qi = get_qinfo(q); func_decl_set const & ng_decls = qi->get_ng_decls(); - func_decl_set::iterator it2 = ng_decls.begin(); - func_decl_set::iterator end2 = ng_decls.end(); - for (; it2 != end2; ++it2) { - func_decl * f = *it2; + for (func_decl* f : ng_decls) { if (!m_forbidden.contains(f)) insert_q_f(q, f); } @@ -2826,40 +2722,30 @@ namespace smt { } static void display_quantifier_set(std::ostream & out, quantifier_set const * s) { - quantifier_set::iterator it = s->begin(); - quantifier_set::iterator end = s->end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier* q : *s) { out << q->get_qid() << " "; } out << "\n"; } void display_qcandidates(std::ostream & out, ptr_vector const & qcandidates) const { - ptr_vector::const_iterator it1 = qcandidates.begin(); - ptr_vector::const_iterator end1 = qcandidates.end(); - for (; it1 != end1; ++it1) { - quantifier * q = *it1; + for (quantifier * q : qcandidates) { out << q->get_qid() << " ->\n" << mk_pp(q, m_manager) << "\n"; quantifier_info * qi = get_qinfo(q); qi->display(out); out << "------\n"; } out << "Sets Q_f\n"; - q_f::iterator it2 = m_q_f.begin(); - q_f::iterator end2 = m_q_f.end(); - for (; it2 != end2; ++it2) { - func_decl * f = (*it2).m_key; - quantifier_set * s = (*it2).m_value; + for (auto const& kv : m_q_f) { + func_decl * f = kv.m_key; + quantifier_set * s = kv.m_value; out << f->get_name() << " -> "; display_quantifier_set(out, s); } out << "Sets Q_{f = def}\n"; - q_f_def::iterator it3 = m_q_f_def.begin(); - q_f_def::iterator end3 = m_q_f_def.end(); - for (; it3 != end3; ++it3) { - func_decl * f = (*it3).get_key1(); - expr * def = (*it3).get_key2(); - quantifier_set * s = (*it3).get_value(); + for (auto const& kv : m_q_f_def) { + func_decl * f = kv.get_key1(); + expr * def = kv.get_key2(); + quantifier_set * s = kv.get_value(); out << f->get_name() << " " << mk_pp(def, m_manager) << " ->\n"; display_quantifier_set(out, s); } } @@ -2894,32 +2780,23 @@ namespace smt { void display_search_state(std::ostream & out) const { out << "fs:\n"; - f2def::iterator it3 = m_fs.begin(); - f2def::iterator end3 = m_fs.end(); - for (; it3 != end3; ++it3) { - out << (*it3).m_key->get_name() << " "; + for (auto const& kv : m_fs) { + out << kv.m_key->get_name() << " "; } out << "\nsatisfied:\n"; - qsset::iterator it = m_satisfied.begin(); - qsset::iterator end = m_satisfied.end(); - for (; it != end; ++it) { - out << (*it)->get_qid() << " "; + for (auto q : m_satisfied) { + out << q->get_qid() << " "; } out << "\nresidue:\n"; - qset::iterator it2 = m_residue.begin(); - qset::iterator end2 = m_residue.end(); - for (; it2 != end2; ++it2) { - out << (*it2)->get_qid() << " "; + for (auto q : m_residue) { + out << q->get_qid() << " "; } out << "\n"; } bool check_satisfied_residue_invariant() { DEBUG_CODE( - qsset::iterator it = m_satisfied.begin(); - qsset::iterator end = m_satisfied.end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : m_satisfied) { SASSERT(!m_residue.contains(q)); quantifier_info * qi = get_qinfo(q); SASSERT(qi != 0); @@ -2934,10 +2811,7 @@ namespace smt { SASSERT(check_satisfied_residue_invariant()); quantifier_set * q_f = get_q_f(f); quantifier_set * q_f_def = get_q_f_def(f, def); - quantifier_set::iterator it = q_f_def->begin(); - quantifier_set::iterator end = q_f_def->end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : *q_f_def) { if (!m_satisfied.contains(q)) { useful = true; m_residue.erase(q); @@ -2949,10 +2823,7 @@ namespace smt { } if (!useful) return false; - it = q_f->begin(); - end = q_f->end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : *q_f) { if (!m_satisfied.contains(q)) { m_residue.insert(q); } @@ -2966,10 +2837,7 @@ namespace smt { The candidates must not be elements of m_fs. */ void get_candidates_from_residue(func_decl_set & candidates) { - qset::iterator it = m_residue.begin(); - qset::iterator end = m_residue.end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : m_residue) { quantifier_info * qi = get_qinfo(q); quantifier_info::macro_iterator it2 = qi->begin_macros(); @@ -2998,10 +2866,7 @@ namespace smt { display_search_state(tout);); expr_set * s = get_f_defs(f); - expr_set::iterator it = s->begin(); - expr_set::iterator end = s->end(); - for (; it != end; ++it) { - expr * def = *it; + for (expr * def : *s) { SASSERT(!m_fs.contains(f)); @@ -3036,17 +2901,13 @@ namespace smt { get_candidates_from_residue(candidates); TRACE("model_finder_hint", tout << "candidates from residue:\n"; - func_decl_set::iterator it = candidates.begin(); - func_decl_set::iterator end = candidates.end(); - for (; it != end; ++it) { - tout << (*it)->get_name() << " "; + for (func_decl * f : candidates) { + tout << f->get_name() << " "; } tout << "\n";); - func_decl_set::iterator it = candidates.begin(); - func_decl_set::iterator end = candidates.end(); - for (; it != end; ++it) { - greedy(*it, depth); + for (func_decl* f : candidates) { + greedy(f, depth); } } @@ -3066,10 +2927,7 @@ namespace smt { \brief Copy the quantifiers from qcandidates to new_qs that are not in m_satisfied. */ void copy_non_satisfied(ptr_vector const & qcandidates, ptr_vector & new_qs) { - ptr_vector::const_iterator it = qcandidates.begin(); - ptr_vector::const_iterator end = qcandidates.end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : qcandidates) { if (!m_satisfied.contains(q)) new_qs.push_back(q); } @@ -3080,11 +2938,9 @@ namespace smt { quantifiers in m_satisfied. */ void set_interp() { - f2def::iterator it = m_fs.begin(); - f2def::iterator end = m_fs.end(); - for (; it != end; ++it) { - func_decl * f = (*it).m_key; - expr * def = (*it).m_value; + for (auto const& kv : m_fs) { + func_decl * f = kv.m_key; + expr * def = kv.m_value; set_else_interp(f, def); } } @@ -3108,10 +2964,7 @@ namespace smt { } mk_q_f_defs(qcandidates); TRACE("model_finder_hint", tout << "starting hint-solver search using:\n"; display_qcandidates(tout, qcandidates);); - func_decl_set::iterator it = m_candidates.begin(); - func_decl_set::iterator end = m_candidates.end(); - for (; it != end; ++it) { - func_decl * f = *it; + for (func_decl * f : m_candidates) { try { process(f); } @@ -3190,10 +3043,7 @@ namespace smt { typedef std::pair mq_pair; void collect_candidates(ptr_vector const & qs, obj_map & full_macros, func_decl_set & cond_macros) { - ptr_vector::const_iterator it = qs.begin(); - ptr_vector::const_iterator end = qs.end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : qs) { quantifier_info * qi = get_qinfo(q); quantifier_info::macro_iterator it2 = qi->begin_macros(); quantifier_info::macro_iterator end2 = qi->end_macros(); @@ -3216,12 +3066,10 @@ namespace smt { } void process_full_macros(obj_map const & full_macros, obj_hashtable & removed) { - obj_map::iterator it = full_macros.begin(); - obj_map::iterator end = full_macros.end(); - for (; it != end; ++it) { - func_decl * f = (*it).m_key; - cond_macro * m = (*it).m_value.first; - quantifier * q = (*it).m_value.second; + for (auto const& kv : full_macros) { + func_decl * f = kv.m_key; + cond_macro * m = kv.m_value.first; + quantifier * q = kv.m_value.second; SASSERT(m->is_unconditional()); if (add_macro(f, m->get_def())) { get_qinfo(q)->set_the_one(f); @@ -3233,10 +3081,7 @@ namespace smt { void process(func_decl * f, ptr_vector const & qs, obj_hashtable & removed) { expr_ref fi_else(m_manager); ptr_buffer to_remove; - ptr_vector::const_iterator it = qs.begin(); - ptr_vector::const_iterator end = qs.end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : qs) { if (removed.contains(q)) continue; cond_macro * m = get_macro_for(f, q); @@ -3254,20 +3099,16 @@ namespace smt { } } if (fi_else.get() != 0 && add_macro(f, fi_else)) { - ptr_buffer::iterator it2 = to_remove.begin(); - ptr_buffer::iterator end2 = to_remove.end(); - for (; it2 != end2; ++it2) { - get_qinfo(*it2)->set_the_one(f); - removed.insert(*it2); + for (quantifier * q : to_remove) { + get_qinfo(q)->set_the_one(f); + removed.insert(q); } } } void process_cond_macros(func_decl_set const & cond_macros, ptr_vector const & qs, obj_hashtable & removed) { - func_decl_set::iterator it = cond_macros.begin(); - func_decl_set::iterator end = cond_macros.end(); - for (; it != end; ++it) { - process(*it, qs, removed); + for (func_decl * f : cond_macros) { + process(f, qs, removed); } } @@ -3282,10 +3123,7 @@ namespace smt { process_full_macros(full_macros, removed); process_cond_macros(cond_macros, qs, removed); - ptr_vector::const_iterator it = qs.begin(); - ptr_vector::const_iterator end = qs.end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : qs) { if (removed.contains(q)) continue; new_qs.push_back(q); @@ -3404,10 +3242,7 @@ namespace smt { } void model_finder::collect_relevant_quantifiers(ptr_vector & qs) const { - ptr_vector::const_iterator it = m_quantifiers.begin(); - ptr_vector::const_iterator end = m_quantifiers.end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : m_quantifiers) { if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) qs.push_back(q); } @@ -3417,26 +3252,19 @@ namespace smt { m_auf_solver->reset(); m_auf_solver->set_model(m); - ptr_vector::const_iterator it = qs.begin(); - ptr_vector::const_iterator end = qs.end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : qs) { quantifier_info * qi = get_quantifier_info(q); qi->process_auf(*(m_auf_solver.get()), m_context); } m_auf_solver->mk_instantiation_sets(); - it = qs.begin(); - for (; it != end; ++it) { - quantifier * q = *it; + + for (quantifier * q : qs) { quantifier_info * qi = get_quantifier_info(q); qi->populate_inst_sets(*(m_auf_solver.get()), m_context); } m_auf_solver->fix_model(m_new_constraints); TRACE("model_finder", - ptr_vector::const_iterator it = qs.begin(); - ptr_vector::const_iterator end = qs.end(); - for (; it != end; ++it) { - quantifier * q = *it; + for (quantifier * q : qs) { quantifier_info * qi = get_quantifier_info(q); quantifier * fq = qi->get_flat_q(); tout << "#" << fq->get_id() << " ->\n" << mk_pp(fq, m_manager) << "\n"; From e47cd27c8d544178d13379d19c81927d582a6eb5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Aug 2017 16:18:25 -0700 Subject: [PATCH 4/7] compiler warnings Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_generalizers.cpp | 2 +- src/muz/spacer/spacer_qe_project.cpp | 2 +- src/smt/mam.cpp | 3 +-- src/smt/theory_fpa.cpp | 5 +++-- src/smt/theory_str.cpp | 2 +- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp index f16fb10e1..94c419493 100644 --- a/src/muz/spacer/spacer_generalizers.cpp +++ b/src/muz/spacer/spacer_generalizers.cpp @@ -133,7 +133,7 @@ void unsat_core_generalizer::operator()(lemma_ref &lemma) unsigned uses_level; expr_ref_vector core(m); - VERIFY(pt.is_invariant(lemma->level(), lemma->get_expr(), uses_level, &core)); + VERIFY(pt.is_invariant(old_level, lemma->get_expr(), uses_level, &core)); CTRACE("spacer", old_sz > core.size(), tout << "unsat core reduced lemma from: " diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index c06854cb0..0eec500e9 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -98,7 +98,7 @@ peq::peq (app* p, ast_manager& m): m_eq (m), m_arr_u (m) { - SASSERT (is_partial_eq (p)); + VERIFY (is_partial_eq (p)); SASSERT (m_arr_u.is_array (m_lhs) && m_arr_u.is_array (m_rhs) && m_eq_proc (m.get_sort (m_lhs), m.get_sort (m_rhs))); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 73ede7319..2aa9d6095 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -2080,16 +2080,15 @@ namespace smt { */ enode_vector * interpreter::mk_depth1_vector(enode * n, func_decl * f, unsigned i) { enode_vector * v = mk_enode_vector(); - unsigned num_args = n->get_num_args(); n = n->get_root(); enode_vector::const_iterator it = n->begin_parents(); enode_vector::const_iterator end = n->end_parents(); for (; it != end; ++it) { enode * p = *it; if (p->get_decl() == f && + i < p->get_num_args() && m_context.is_relevant(p) && p->is_cgr() && - i < p->get_num_args() && p->get_arg(i)->get_root() == n) { v->push_back(p); } diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 17349ead6..e8edfc7ec 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -237,8 +237,9 @@ namespace smt { if (m_fpa_util.is_fp(e)) { expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) }; - res = m_bv_util.mk_concat(3, cargs); - m_th_rw((expr_ref&)res); + expr_ref tmp(m_bv_util.mk_concat(3, cargs), m); + m_th_rw(tmp); + res = to_app(tmp); } else { sort * es = m.get_sort(e); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 0d963f8b9..88b044a90 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -8567,7 +8567,7 @@ namespace smt { } else { TRACE("str", tout << "integer theory has no assignment for " << mk_pp(a, m) << std::endl;); expr_ref is_zero(ctx.mk_eq_atom(a, m_autil.mk_int(0)), m); - literal is_zero_l = mk_literal(is_zero); + /* literal is_zero_l = */ mk_literal(is_zero); axiomAdd = true; TRACE("str", ctx.display(tout);); // NOT_IMPLEMENTED_YET(); From ebe9db14d58ac3fc3f15009f56becbe69b36e56e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Aug 2017 14:13:43 -0700 Subject: [PATCH 5/7] fix regression exposed by segfault2.smt2 crash Signed-off-by: Nikolaj Bjorner --- src/model/model_core.cpp | 6 +++--- src/smt/proto_model/proto_model.cpp | 6 +++--- src/smt/theory_seq.cpp | 4 ++-- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 684d1b3c2..2f6137172 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -90,18 +90,18 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { void model_core::unregister_decl(func_decl * d) { decl2expr::obj_map_entry * ec = m_interp.find_core(d); if (ec && ec->get_data().m_value != 0) { - m_manager.dec_ref(ec->get_data().m_key); - m_manager.dec_ref(ec->get_data().m_value); m_interp.remove(d); m_const_decls.erase(d); + m_manager.dec_ref(ec->get_data().m_key); + m_manager.dec_ref(ec->get_data().m_value); return; } decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); if (ef && ef->get_data().m_value != 0) { - m_manager.dec_ref(ef->get_data().m_key); dealloc(ef->get_data().m_value); m_finterp.remove(d); m_func_decls.erase(d); + m_manager.dec_ref(ef->get_data().m_key); } } diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 9a5f2a1ca..9b218037e 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -10,7 +10,7 @@ Abstract: Author: - + Leonardo de Moura (leonardo) 2007-03-08. Revision History: @@ -359,8 +359,8 @@ void proto_model::complete_partial_funcs() { // m_func_decls may be "expanded" when we invoke get_some_value. // So, we must not use iterators to traverse it. - for (func_decl* f : m_func_decls) { - complete_partial_func(f); + for (unsigned i = 0; i < m_func_decls.size(); i++) { + complete_partial_func(m_func_decls[i]); } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index d988da54f..c91882dad 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -427,7 +427,7 @@ bool theory_seq::branch_unit_variable() { break; } } - CTRACE("seq", result, "branch unit variable";); + CTRACE("seq", result, tout << "branch unit variable";); return result; } @@ -3552,7 +3552,7 @@ bool theory_seq::get_length(expr* e, rational& val) const { } } } - CTRACE("seq", !val.is_int(), "length is not an integer\n";); + CTRACE("seq", !val.is_int(), tout << "length is not an integer\n";); return val.is_int(); } From e6145fa6df997eae552848914b9ff6f485e18fc7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Aug 2017 14:53:16 -0700 Subject: [PATCH 6/7] fix crash Signed-off-by: Nikolaj Bjorner --- src/model/model_core.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 2f6137172..3d9de1ba1 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -99,9 +99,9 @@ void model_core::unregister_decl(func_decl * d) { decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); if (ef && ef->get_data().m_value != 0) { + m_manager.dec_ref(ef->get_data().m_key); dealloc(ef->get_data().m_value); m_finterp.remove(d); m_func_decls.erase(d); - m_manager.dec_ref(ef->get_data().m_key); } } From 2c8e9aeb9cc6ffa334e6e262c7c56d9941d3fb90 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Aug 2017 15:23:52 -0700 Subject: [PATCH 7/7] another crash fix Signed-off-by: Nikolaj Bjorner --- src/model/model_core.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 3d9de1ba1..5eb1eb00d 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -90,10 +90,10 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { void model_core::unregister_decl(func_decl * d) { decl2expr::obj_map_entry * ec = m_interp.find_core(d); if (ec && ec->get_data().m_value != 0) { + m_manager.dec_ref(ec->get_data().m_key); + m_manager.dec_ref(ec->get_data().m_value); m_interp.remove(d); m_const_decls.erase(d); - m_manager.dec_ref(ec->get_data().m_key); - m_manager.dec_ref(ec->get_data().m_value); return; }