From 503bedbc7a7c597a04ec3b39431b03bcdd505d21 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Nov 2018 21:12:47 -0800 Subject: [PATCH] fix #1967: Signed-off-by: Nikolaj Bjorner --- src/smt/smt_quantifier.cpp | 110 ++++++++++++++++++++----------------- src/smt/theory_seq.cpp | 71 +++++++++++++----------- src/smt/theory_seq.h | 2 +- 3 files changed, 99 insertions(+), 84 deletions(-) diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 14dc27c79..ce621144e 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -109,15 +109,14 @@ namespace smt { \brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its equivalence class are in the log and up-to-date. */ - void log_justification_to_root(std::ostream & log, enode *en, obj_hashtable &already_visited) { + void log_justification_to_root(std::ostream & out, enode *en, obj_hashtable &visited) { enode* root = en->get_root(); - for (enode *it = en; it != root; it = it->get_trans_justification().m_target) { - if (already_visited.contains(it)) - break; - already_visited.insert(it); + for (enode *it = en; it != root && !visited.contains(it); it = it->get_trans_justification().m_target) { + + visited.insert(it); if (!it->m_proof_is_logged) { - log_single_justification(log, it, already_visited); + log_single_justification(out, it, visited); it->m_proof_is_logged = true; } else if (it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) { @@ -128,14 +127,14 @@ namespace smt { enode *target = it->get_trans_justification().m_target; for (unsigned i = 0; i < num_args; ++i) { - log_justification_to_root(log, it->get_arg(i), already_visited); - log_justification_to_root(log, target->get_arg(i), already_visited); + log_justification_to_root(out, it->get_arg(i), visited); + log_justification_to_root(out, target->get_arg(i), visited); } SASSERT(it->m_proof_is_logged); } } if (!root->m_proof_is_logged) { - log << "[eq-expl] #" << root->get_owner_id() << " root\n"; + out << "[eq-expl] #" << root->get_owner_id() << " root\n"; root->m_proof_is_logged = true; } } @@ -144,7 +143,7 @@ namespace smt { \brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log equalities needed by the step (e.g. argument equalities for congruence steps). */ - void log_single_justification(std::ostream & out, enode *en, obj_hashtable &already_visited) { + void log_single_justification(std::ostream & out, enode *en, obj_hashtable &visited) { smt::literal lit; unsigned num_args; enode *target = en->get_trans_justification().m_target; @@ -163,8 +162,8 @@ namespace smt { num_args = en->get_num_args(); for (unsigned i = 0; i < num_args; ++i) { - log_justification_to_root(out, en->get_arg(i), already_visited); - log_justification_to_root(out, target->get_arg(i), already_visited); + log_justification_to_root(out, en->get_arg(i), visited); + log_justification_to_root(out, target->get_arg(i), visited); } out << "[eq-expl] #" << en->get_owner_id() << " cg"; @@ -193,6 +192,53 @@ namespace smt { } } + void log_add_instance( + fingerprint* f, + quantifier * q, app * pat, + unsigned num_bindings, + enode * const * bindings, + vector> & used_enodes) { + + std::ostream & out = trace_stream(); + + obj_hashtable visited; + + // In the term produced by the quantifier instantiation the root of + // the equivalence class of the terms bound to the quantified variables + // is used. We need to make sure that all of these equalities appear in the log. + for (unsigned i = 0; i < num_bindings; ++i) { + log_justification_to_root(out, bindings[i], visited); + } + + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig != nullptr) { + log_justification_to_root(out, orig, visited); + log_justification_to_root(out, substituted, visited); + } + } + + // At this point all relevant equalities for the match are logged. + out << "[new-match] " << static_cast(f) << " #" << q->get_id() << " #" << pat->get_id(); + for (unsigned i = 0; i < num_bindings; i++) { + // I don't want to use mk_pp because it creates expressions for pretty printing. + // This nasty side-effect may change the behavior of Z3. + out << " #" << bindings[i]->get_owner_id(); + } + out << " ;"; + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig == nullptr) + out << " #" << substituted->get_owner_id(); + else { + out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")"; + } + } + out << "\n"; + } + bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, @@ -209,43 +255,7 @@ namespace smt { fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def); if (f) { if (has_trace_stream()) { - std::ostream & out = trace_stream(); - - obj_hashtable already_visited; - - // In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables - // is used. We need to make sure that all of these equalities appear in the log. - for (unsigned i = 0; i < num_bindings; ++i) { - log_justification_to_root(out, bindings[i], already_visited); - } - - for (auto n : used_enodes) { - enode *orig = std::get<0>(n); - enode *substituted = std::get<1>(n); - if (orig != nullptr) { - log_justification_to_root(out, orig, already_visited); - log_justification_to_root(out, substituted, already_visited); - } - } - - // At this point all relevant equalities for the match are logged. - out << "[new-match] " << static_cast(f) << " #" << q->get_id() << " #" << pat->get_id(); - for (unsigned i = 0; i < num_bindings; i++) { - // I don't want to use mk_pp because it creates expressions for pretty printing. - // This nasty side-effect may change the behavior of Z3. - out << " #" << bindings[i]->get_owner_id(); - } - out << " ;"; - for (auto n : used_enodes) { - enode *orig = std::get<0>(n); - enode *substituted = std::get<1>(n); - if (orig == nullptr) - out << " #" << substituted->get_owner_id(); - else { - out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")"; - } - } - out << "\n"; + log_add_instance(f, q, pat, num_bindings, bindings, used_enodes); } m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO m_num_instances++; @@ -256,7 +266,7 @@ namespace smt { tout << mk_pp(bindings[i]->get_owner(), m()) << " "; } tout << "\n"; - tout << "inserted: " << (f != 0) << "\n"; + tout << "inserted: " << (f != nullptr) << "\n"; ); return f != nullptr; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 5a85628e8..f3a88c5b1 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1487,8 +1487,7 @@ bool theory_seq::enforce_length(expr_ref_vector const& es, vector & le bool all_have_length = true; rational val; zstring s; - for (unsigned i = 0; i < es.size(); ++i) { - expr* e = es[i]; + for (expr* e : es) { if (m_util.str.is_unit(e)) { len.push_back(rational(1)); } @@ -3397,6 +3396,7 @@ bool theory_seq::check_int_string() { bool theory_seq::check_int_string(expr* e) { return + get_context().inconsistent() || (m_util.str.is_itos(e) && add_itos_val_axiom(e)) || (m_util.str.is_stoi(e) && add_stoi_val_axiom(e)); } @@ -3410,9 +3410,33 @@ void theory_seq::add_stoi_axiom(expr* e) { // stoi(s) >= -1 literal l = mk_simplified_literal(m_autil.mk_ge(e, m_autil.mk_int(-1))); add_axiom(l); - + + // stoi("") = -1 + add_axiom(mk_eq(m_util.str.mk_stoi(m_util.str.mk_empty(m.get_sort(s))), m_autil.mk_int(-1), false)); } +void theory_seq::add_itos_axiom(expr* e) { + rational val; + expr* n = nullptr; + TRACE("seq", tout << mk_pp(e, m) << "\n";); + VERIFY(m_util.str.is_itos(e, n)); + + // itos(n) = "" <=> n < 0 + expr_ref zero(m_autil.mk_int(0), m); + literal eq1 = mk_literal(m_util.str.mk_is_empty(e)); + literal ge0 = mk_literal(m_autil.mk_ge(n, zero)); + // n >= 0 => itos(n) != "" + // itos(n) = "" or n >= 0 + add_axiom(~eq1, ~ge0); + add_axiom(eq1, ge0); + + // n >= 0 => stoi(itos(n)) = n + app_ref stoi(m_util.str.mk_stoi(e), m); + add_axiom(~ge0, mk_preferred_eq(stoi, n)); + +} + + void theory_seq::ensure_digit_axiom() { if (m_si_axioms.empty()) { @@ -3425,7 +3449,7 @@ void theory_seq::ensure_digit_axiom() { } bool theory_seq::add_itos_val_axiom(expr* e) { - rational val; + rational val, val2; expr* n = nullptr; TRACE("seq", tout << mk_pp(e, m) << "\n";); VERIFY(m_util.str.is_itos(e, n)); @@ -3435,11 +3459,11 @@ bool theory_seq::add_itos_val_axiom(expr* e) { } enforce_length(e); - if (get_length(e, val) && val.is_pos() && val.is_unsigned() && !m_si_axioms.contains(e)) { + if (get_length(e, val) && val.is_pos() && val.is_unsigned() && (!m_si_axioms.find(e, val2) || val != val2)) { add_si_axiom(e, n, val.get_unsigned()); - m_si_axioms.insert(e); + m_si_axioms.insert(e, val); m_trail_stack.push(push_replay(alloc(replay_is_axiom, m, e))); - m_trail_stack.push(insert_map, expr*>(m_si_axioms, e)); + m_trail_stack.push(insert_map, expr*>(m_si_axioms, e)); return true; } @@ -3449,20 +3473,21 @@ bool theory_seq::add_itos_val_axiom(expr* e) { bool theory_seq::add_stoi_val_axiom(expr* e) { context& ctx = get_context(); expr* n = nullptr; - rational val; - TRACE("seq", tout << mk_pp(e, m) << " " << ctx.get_scope_level () << "\n";); + rational val, val2; VERIFY(m_util.str.is_stoi(e, n)); + TRACE("seq", tout << mk_pp(e, m) << " " << ctx.get_scope_level () << " " << get_length(n, val) << " " << val << "\n";); + if (m_util.str.is_itos(n)) { return false; } enforce_length(n); - if (get_length(n, val) && val.is_pos() && val.is_unsigned() && !m_si_axioms.contains(e)) { + if (get_length(n, val) && val.is_pos() && val.is_unsigned() && (!m_si_axioms.find(e, val2) || val2 != val)) { add_si_axiom(n, e, val.get_unsigned()); - m_si_axioms.insert(e); + m_si_axioms.insert(e, val); m_trail_stack.push(push_replay(alloc(replay_is_axiom, m, e))); - m_trail_stack.push(insert_map, expr*>(m_si_axioms, e)); + m_trail_stack.push(insert_map, expr*>(m_si_axioms, e)); return true; } @@ -3487,26 +3512,6 @@ expr_ref theory_seq::digit2int(expr* ch) { return expr_ref(mk_skolem(symbol("seq.digit2int"), ch, nullptr, nullptr, nullptr, m_autil.mk_int()), m); } -void theory_seq::add_itos_axiom(expr* e) { - rational val; - expr* n = nullptr; - TRACE("seq", tout << mk_pp(e, m) << "\n";); - VERIFY(m_util.str.is_itos(e, n)); - - // itos(n) = "" <=> n < 0 - expr_ref zero(arith_util(m).mk_int(0), m); - literal eq1 = mk_literal(m_util.str.mk_is_empty(e)); - literal ge0 = mk_literal(m_autil.mk_ge(n, zero)); - // n >= 0 => itos(n) != "" - // itos(n) = "" or n >= 0 - add_axiom(~eq1, ~ge0); - add_axiom(eq1, ge0); - - // n >= 0 => stoi(itos(n)) = n - app_ref stoi(m_util.str.mk_stoi(e), m); - add_axiom(~ge0, mk_preferred_eq(stoi, n)); - -} // n >= 0 & len(e) = k => is_digit(e_i) for i = 0..k-1 @@ -3550,7 +3555,7 @@ void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) { SASSERT(k > 0); rational lb = power(rational(10), k - 1); rational ub = power(rational(10), k) - 1; - arith_util a (m); + arith_util& a = m_autil; literal lbl = mk_literal(a.mk_ge(n, a.mk_int(lb))); literal ubl = mk_literal(a.mk_le(n, a.mk_int(ub))); literal ge_k = mk_literal(a.mk_ge(len, a.mk_int(k))); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index aa278e972..75ba54381 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -343,7 +343,7 @@ namespace smt { unsigned m_axioms_head; // index of first axiom to add. bool m_incomplete; // is the solver (clearly) incomplete for the fragment. expr_ref_vector m_int_string; - obj_hashtable m_si_axioms; + obj_map m_si_axioms; obj_hashtable m_length; // is length applied scoped_ptr_vector m_replay; // set of actions to replay model_generator* m_mg;