From 1aeffa2e013e7b0d9ec00bf914ee7ad4e16cea1d Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Thu, 24 May 2018 19:25:59 +0200 Subject: [PATCH] fixing issue where argument equalities for congruence explanations were not updated explaining equalities added by theories --- src/smt/smt_context.cpp | 7 ++++--- src/smt/smt_enode.cpp | 2 +- src/smt/smt_enode.h | 11 +++++++++- src/smt/smt_quantifier.cpp | 42 ++++++++++++++++++++++++++++++-------- 4 files changed, 49 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c378c401b..5b0b3eacd 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -562,7 +562,7 @@ namespace smt { invert_trans(n1); n1->m_trans.m_target = n2; n1->m_trans.m_justification = js; - n1->m_proof_is_logged = false; + n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED; SASSERT(r1->trans_reaches(n1)); // --------------- // r1 -> .. -> n1 -> n2 -> ... -> r2 @@ -748,13 +748,14 @@ namespace smt { eq_justification js = n->m_trans.m_justification; prev->m_trans.m_target = nullptr; prev->m_trans.m_justification = null_eq_justification; + prev->m_proof_logged_status = smt::logged_status::NOT_LOGGED; while (curr != nullptr) { SASSERT(prev->trans_reaches(n)); enode * new_curr = curr->m_trans.m_target; eq_justification new_js = curr->m_trans.m_justification; curr->m_trans.m_target = prev; curr->m_trans.m_justification = js; - curr->m_proof_is_logged = false; + curr->m_proof_logged_status = smt::logged_status::NOT_LOGGED; prev = curr; js = new_js; curr = new_curr; @@ -1051,7 +1052,7 @@ namespace smt { SASSERT(r1->trans_reaches(n1)); n1->m_trans.m_target = nullptr; n1->m_trans.m_justification = null_eq_justification; - n1->m_proof_is_logged = false; + n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED; invert_trans(r1); // --------------- // n1 -> ... -> r1 diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index d14c37906..ca646974d 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -47,7 +47,7 @@ namespace smt { n->m_cgc_enabled = cgc_enabled; n->m_iscope_lvl = iscope_lvl; n->m_lbl_hash = -1; - n->m_proof_is_logged = false; + n->m_proof_logged_status = smt::logged_status::NOT_LOGGED; unsigned num_args = n->get_num_args(); for (unsigned i = 0; i < num_args; i++) { enode * arg = app2enode[owner->get_arg(i)->get_id()]; diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 7c1bb3e4d..3e7f0984d 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -38,6 +38,15 @@ namespace smt { } }; + /** + \brief Indicates whether the proof for membership in an equivalence class is already logged. + */ + enum logged_status { + NOT_LOGGED, + BEING_LOGGED, + LOGGED + }; + /** \ brief Use sparse maps in SMT solver. Define this to use hash maps rather than vectors over ast @@ -105,7 +114,7 @@ namespace smt { enode_vector m_parents; //!< Parent enodes of the equivalence class. theory_var_list m_th_var_list; //!< List of theories that 'care' about this enode. trans_justification m_trans; //!< A justification for the enode being equal to its root. - bool m_proof_is_logged; //!< Indicates that the proof for the enode being equal to its root is in the log. + logged_status m_proof_logged_status; //!< Indicates that the proof for the enode being equal to its root is in the log. signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern approx_set m_lbls; approx_set m_plbls; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 2b134a23f..d8795c0cf 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -104,24 +104,38 @@ namespace smt { return m_plugin->is_shared(n); } - inline void log_transitive_justification(std::ostream & log, enode *en) { + void log_transitive_justification(std::ostream & log, enode *en) { enode *root = en->get_root(); for (enode *it = en; it != root; it = it->get_trans_justification().m_target) { - if (!it->m_proof_is_logged) { - it->m_proof_is_logged = true; + if (it->m_proof_logged_status == smt::logged_status::NOT_LOGGED) { + it->m_proof_logged_status = smt::logged_status::BEING_LOGGED; print_justification(log, it); + it->m_proof_logged_status = smt::logged_status::LOGGED; + } else if (it->m_proof_logged_status != smt::logged_status::BEING_LOGGED && it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) { + + // When the justification of an argument changes m_proof_logged_status is not reset => We need to check if the proofs of all arguments are logged. + it->m_proof_logged_status = smt::logged_status::BEING_LOGGED; + const unsigned num_args = it->get_num_args(); + enode *target = it->get_trans_justification().m_target; + + for (unsigned i = 0; i < num_args; ++i) { + log_transitive_justification(log, it->get_arg(i)); + log_transitive_justification(log, target->get_arg(i)); + } + it->m_proof_logged_status = smt::logged_status::LOGGED; } } - if (!root->m_proof_is_logged) { - root->m_proof_is_logged = true; + if (root->m_proof_logged_status == smt::logged_status::NOT_LOGGED) { log << "[eq-expl] #" << root->get_owner_id() << " root\n"; + root->m_proof_logged_status = smt::logged_status::LOGGED; } } - inline void print_justification(std::ostream & out, enode *en) { + void print_justification(std::ostream & out, enode *en) { smt::literal lit; unsigned num_args; enode *target = en->get_trans_justification().m_target; + theory_id th_id; switch (en->get_trans_justification().m_justification.get_kind()) { case smt::eq_justification::kind::EQUATION: @@ -142,15 +156,27 @@ namespace smt { } out << "[eq-expl] #" << en->get_owner_id() << " cg"; - for (unsigned i = 0; i < num_args; i++) { + for (unsigned i = 0; i < num_args; ++i) { out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")"; } out << " ; #" << target->get_owner_id() << "\n"; + break; + } else { + out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n"; break; } + case smt::eq_justification::kind::JUSTIFICATION: + th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory(); + if (th_id != null_theory_id) { + symbol const theory = m().get_family_name(th_id); + out << "[eq-expl] #" << en->get_owner_id() << " th:" << theory.str() << " ; #" << target->get_owner_id() << "\n"; + } else { + out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n"; + } + break; default: - out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n"; + out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n"; break; } }