From 276fdd0e972d9f6c7d78b9eb093fc2b27bb212d7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Aug 2017 08:51:24 -0700 Subject: [PATCH] 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) {