mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 03:12:03 +00:00
Code Activity

fix #1967:

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-26 21:12:47 -08:00
parent e026f96ed4
commit 503bedbc7a
3 changed files with 99 additions and 84 deletions
Download patch file Download diff file Expand all files Collapse all files

110
src/smt/smt_quantifier.cpp
View file

@ -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 \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. equivalence class are in the log and up-to-date.
*/ */
void log_justification_to_root(std::ostream & log, enode *en, obj_hashtable<enode> &already_visited) { void log_justification_to_root(std::ostream & out, enode *en, obj_hashtable<enode> &visited) {
enode* root = en->get_root(); enode* root = en->get_root();
for (enode *it = en; it != root; it = it->get_trans_justification().m_target) { for (enode *it = en; it != root && !visited.contains(it); it = it->get_trans_justification().m_target) {
if (already_visited.contains(it))
break; visited.insert(it);
already_visited.insert(it);
if (!it->m_proof_is_logged) { 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; it->m_proof_is_logged = true;
} }
else if (it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) { 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; enode *target = it->get_trans_justification().m_target;
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
log_justification_to_root(log, it->get_arg(i), already_visited); log_justification_to_root(out, it->get_arg(i), visited);
log_justification_to_root(log, target->get_arg(i), already_visited); log_justification_to_root(out, target->get_arg(i), visited);
} }
SASSERT(it->m_proof_is_logged); SASSERT(it->m_proof_is_logged);
} }
} }
if (!root->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; 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 \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). equalities needed by the step (e.g. argument equalities for congruence steps).
*/ */
void log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &already_visited) { void log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &visited) {
smt::literal lit; smt::literal lit;
unsigned num_args; unsigned num_args;
enode *target = en->get_trans_justification().m_target; enode *target = en->get_trans_justification().m_target;
@ -163,8 +162,8 @@ namespace smt {
num_args = en->get_num_args(); num_args = en->get_num_args();
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
log_justification_to_root(out, en->get_arg(i), already_visited); log_justification_to_root(out, en->get_arg(i), visited);
log_justification_to_root(out, target->get_arg(i), already_visited); log_justification_to_root(out, target->get_arg(i), visited);
} }
out << "[eq-expl] #" << en->get_owner_id() << " cg"; 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<std::tuple<enode *, enode *>> & used_enodes) {
std::ostream & out = trace_stream();
obj_hashtable<enode> 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<void*>(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, bool add_instance(quantifier * q, app * pat,
unsigned num_bindings, unsigned num_bindings,
enode * const * bindings, enode * const * bindings,
@ -209,43 +255,7 @@ namespace smt {
fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def); fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def);
if (f) { if (f) {
if (has_trace_stream()) { if (has_trace_stream()) {
std::ostream & out = trace_stream(); log_add_instance(f, q, pat, num_bindings, bindings, used_enodes);
obj_hashtable<enode> 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<void*>(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";
} }
m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
m_num_instances++; m_num_instances++;
@ -256,7 +266,7 @@ namespace smt {
tout << mk_pp(bindings[i]->get_owner(), m()) << " "; tout << mk_pp(bindings[i]->get_owner(), m()) << " ";
} }
tout << "\n"; tout << "\n";
tout << "inserted: " << (f != 0) << "\n"; tout << "inserted: " << (f != nullptr) << "\n";
); );
return f != nullptr; return f != nullptr;

69
src/smt/theory_seq.cpp
View file

@ -1487,8 +1487,7 @@ bool theory_seq::enforce_length(expr_ref_vector const& es, vector<rational> & le
bool all_have_length = true; bool all_have_length = true;
rational val; rational val;
zstring s; zstring s;
for (unsigned i = 0; i < es.size(); ++i) { for (expr* e : es) {
expr* e = es[i];
if (m_util.str.is_unit(e)) { if (m_util.str.is_unit(e)) {
len.push_back(rational(1)); len.push_back(rational(1));
} }
@ -3397,6 +3396,7 @@ bool theory_seq::check_int_string() {
bool theory_seq::check_int_string(expr* e) { bool theory_seq::check_int_string(expr* e) {
return return
get_context().inconsistent() ||
(m_util.str.is_itos(e) && add_itos_val_axiom(e)) || (m_util.str.is_itos(e) && add_itos_val_axiom(e)) ||
(m_util.str.is_stoi(e) && add_stoi_val_axiom(e)); (m_util.str.is_stoi(e) && add_stoi_val_axiom(e));
} }
@ -3411,8 +3411,32 @@ void theory_seq::add_stoi_axiom(expr* e) {
literal l = mk_simplified_literal(m_autil.mk_ge(e, m_autil.mk_int(-1))); literal l = mk_simplified_literal(m_autil.mk_ge(e, m_autil.mk_int(-1)));
add_axiom(l); 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() { void theory_seq::ensure_digit_axiom() {
if (m_si_axioms.empty()) { if (m_si_axioms.empty()) {
@ -3425,7 +3449,7 @@ void theory_seq::ensure_digit_axiom() {
} }
bool theory_seq::add_itos_val_axiom(expr* e) { bool theory_seq::add_itos_val_axiom(expr* e) {
rational val; rational val, val2;
expr* n = nullptr; expr* n = nullptr;
TRACE("seq", tout << mk_pp(e, m) << "\n";); TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_itos(e, 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); 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()); 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(push_replay(alloc(replay_is_axiom, m, e)));
m_trail_stack.push(insert_map<theory_seq, obj_hashtable<expr>, expr*>(m_si_axioms, e)); m_trail_stack.push(insert_map<theory_seq, obj_map<expr, rational>, expr*>(m_si_axioms, e));
return true; return true;
} }
@ -3449,20 +3473,21 @@ bool theory_seq::add_itos_val_axiom(expr* e) {
bool theory_seq::add_stoi_val_axiom(expr* e) { bool theory_seq::add_stoi_val_axiom(expr* e) {
context& ctx = get_context(); context& ctx = get_context();
expr* n = nullptr; expr* n = nullptr;
rational val; rational val, val2;
TRACE("seq", tout << mk_pp(e, m) << " " << ctx.get_scope_level () << "\n";);
VERIFY(m_util.str.is_stoi(e, n)); 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)) { if (m_util.str.is_itos(n)) {
return false; return false;
} }
enforce_length(n); 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()); 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(push_replay(alloc(replay_is_axiom, m, e)));
m_trail_stack.push(insert_map<theory_seq, obj_hashtable<expr>, expr*>(m_si_axioms, e)); m_trail_stack.push(insert_map<theory_seq, obj_map<expr, rational>, expr*>(m_si_axioms, e));
return true; 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); 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 // 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); SASSERT(k > 0);
rational lb = power(rational(10), k - 1); rational lb = power(rational(10), k - 1);
rational ub = 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 lbl = mk_literal(a.mk_ge(n, a.mk_int(lb)));
literal ubl = mk_literal(a.mk_le(n, a.mk_int(ub))); 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))); literal ge_k = mk_literal(a.mk_ge(len, a.mk_int(k)));

2
src/smt/theory_seq.h
View file

@ -343,7 +343,7 @@ namespace smt {
unsigned m_axioms_head; // index of first axiom to add. unsigned m_axioms_head; // index of first axiom to add.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment. bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
expr_ref_vector m_int_string; expr_ref_vector m_int_string;
obj_hashtable<expr> m_si_axioms; obj_map<expr, rational> m_si_axioms;
obj_hashtable<expr> m_length; // is length applied obj_hashtable<expr> m_length; // is length applied
scoped_ptr_vector<apply> m_replay; // set of actions to replay scoped_ptr_vector<apply> m_replay; // set of actions to replay
model_generator* m_mg; model_generator* m_mg;