diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 70741fa67..a6b5e5515 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -2376,6 +2376,13 @@ namespace smt { SASSERT(m_n2 != 0); if (m_n1->get_root() != m_n2->get_root()) goto backtrack; + + // We will use the common root when instantiating the quantifier => log the necessary equalities + if (m_ast_manager.has_trace_stream()) { + m_used_enodes.push_back(std::make_tuple(m_n1, m_n1->get_root())); + m_used_enodes.push_back(std::make_tuple(m_n2, m_n2->get_root())); + } + m_pc = m_pc->m_next; goto main_loop; @@ -2572,6 +2579,11 @@ namespace smt { if (m_n1 == 0 || !m_context.is_relevant(m_n1)) \ goto backtrack; \ update_max_generation(m_n1, nullptr); \ + if (m_ast_manager.has_trace_stream()) { \ + for (unsigned i = 0; i < static_cast(m_pc)->m_num_args; ++i) { \ + m_used_enodes.push_back(std::make_tuple(m_n1->get_arg(i), m_n1->get_arg(i)->get_root())); \ + } \ + } \ m_registers[static_cast(m_pc)->m_oreg] = m_n1; \ m_pc = m_pc->m_next; \ goto main_loop; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6e132ff71..7ee6d4a92 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -563,7 +563,7 @@ namespace smt { invert_trans(n1); n1->m_trans.m_target = n2; n1->m_trans.m_justification = js; - n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED; + n1->m_proof_is_logged = false; SASSERT(r1->trans_reaches(n1)); // --------------- // r1 -> .. -> n1 -> n2 -> ... -> r2 @@ -743,14 +743,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; + prev->m_proof_is_logged = false; 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_logged_status = smt::logged_status::NOT_LOGGED; + curr->m_proof_is_logged = false; prev = curr; js = new_js; curr = new_curr; @@ -1044,7 +1044,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_logged_status = smt::logged_status::NOT_LOGGED; + n1->m_proof_is_logged = false; invert_trans(r1); // --------------- // n1 -> ... -> r1 diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index ca646974d..d9477e95d 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_logged_status = smt::logged_status::NOT_LOGGED; + n->m_proof_is_logged = false; 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 74fcbfb45..f7dfda83b 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -38,15 +38,6 @@ namespace smt { } }; - /** - \brief Indicates whether the proof for membership in an equivalence class is already logged. - */ - enum logged_status { - NOT_LOGGED, //!< Proof is not logged or logged information is not up-to-date. - BEING_LOGGED, //!< We are currently in the process of logging all relevant information. This is used to prevent looping when logging congruence steps. - LOGGED //!< Proof is logged and logged information is still up-to-date. - }; - /** \ brief Use sparse maps in SMT solver. Define this to use hash maps rather than vectors over ast @@ -114,7 +105,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. - logged_status m_proof_logged_status; //!< Indicates that the proof for the enode being equal to its root is in the log. + bool m_proof_is_logged; //!< 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_internalizer.cpp b/src/smt/smt_internalizer.cpp index 618450f9d..4a6cd086c 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1018,8 +1018,17 @@ namespace smt { void context::apply_sort_cnstr(app * term, enode * e) { sort * s = term->get_decl()->get_range(); theory * th = m_theories.get_plugin(s->get_family_id()); - if (th) + if (th) { + if (m_manager.has_trace_stream()) { + m_manager.trace_stream() << "[theory-constraints] " << m_manager.get_family_name(s->get_family_id()) << "\n"; + } + th->apply_sort_cnstr(e, s); + + if (m_manager.has_trace_stream()) { + m_manager.trace_stream() << "[end-theory-constraints]\n"; + } + } } /** diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 885157ab3..f74c9d4c9 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -26,6 +26,7 @@ Revision History: #include "smt/smt_quick_checker.h" #include "smt/mam.h" #include "smt/qi_queue.h" +#include "util/obj_hashtable.h" namespace smt { @@ -108,30 +109,31 @@ 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) { + void log_justification_to_root(std::ostream & log, enode *en, obj_hashtable &already_visited) { enode *root = en->get_root(); for (enode *it = en; it != root; it = it->get_trans_justification().m_target) { - if (it->m_proof_logged_status == smt::logged_status::NOT_LOGGED) { - it->m_proof_logged_status = smt::logged_status::BEING_LOGGED; - log_single_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) { + if (already_visited.find(it) == already_visited.end()) already_visited.insert(it); + else break; - // 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; + if (!it->m_proof_is_logged) { + log_single_justification(log, it, already_visited); + it->m_proof_is_logged = true; + } else if (it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) { + + // When the justification of an argument changes m_proof_is_logged is not reset => We need to check if the proofs of all arguments are 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_justification_to_root(log, it->get_arg(i)); - log_justification_to_root(log, target->get_arg(i)); + log_justification_to_root(log, it->get_arg(i), already_visited); + log_justification_to_root(log, target->get_arg(i), already_visited); } - it->m_proof_logged_status = smt::logged_status::LOGGED; + it->m_proof_is_logged = true; } } - if (root->m_proof_logged_status == smt::logged_status::NOT_LOGGED) { + if (!root->m_proof_is_logged) { log << "[eq-expl] #" << root->get_owner_id() << " root\n"; - root->m_proof_logged_status = smt::logged_status::LOGGED; + root->m_proof_is_logged = true; } } @@ -139,7 +141,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) { + void log_single_justification(std::ostream & out, enode *en, obj_hashtable &already_visited) { smt::literal lit; unsigned num_args; enode *target = en->get_trans_justification().m_target; @@ -158,8 +160,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)); - log_justification_to_root(out, target->get_arg(i)); + log_justification_to_root(out, en->get_arg(i), already_visited); + log_justification_to_root(out, target->get_arg(i), already_visited); } out << "[eq-expl] #" << en->get_owner_id() << " cg"; @@ -206,18 +208,20 @@ namespace smt { 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]); + 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); - log_justification_to_root(out, substituted); + log_justification_to_root(out, orig, already_visited); + log_justification_to_root(out, substituted, already_visited); } }