From a4057420372ec269b6356d6309f0ecd2bdf9459f Mon Sep 17 00:00:00 2001
From: nilsbecker <nbecker@student.ethz.ch>
Date: Fri, 6 Jul 2018 12:43:46 +0200
Subject: [PATCH] Adding comments

---
 src/smt/mam.cpp            | 8 ++++++--
 src/smt/smt_context.h      | 2 +-
 src/smt/smt_quantifier.cpp | 6 ++++++
 src/smt/smt_quantifier.h   | 2 +-
 4 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 51c39f9e2..a39fe96ed 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -1847,6 +1847,9 @@ namespace smt {
         enode *             m_n2;
         enode *             m_app;
         const bind *        m_b;
+
+        // equalities used for pattern match. The first element of the tuple gives the argument (or null) of some term that was matched against some higher level
+        // structure of the trigger, the second element gives the term that argument is replaced with in order to match the trigger. Used for logging purposes only.
         vector<std::tuple<enode *, enode *>> m_used_enodes;
         unsigned            m_curr_used_enodes_size;
         ptr_vector<enode>   m_pattern_instances; // collect the pattern instances... used for computing min_top_generation and max_top_generation
@@ -2275,7 +2278,7 @@ namespace smt {
 
         if (m_ast_manager.has_trace_stream()) {
             m_used_enodes.reset();
-            m_used_enodes.push_back(std::make_tuple(nullptr, n));
+            m_used_enodes.push_back(std::make_tuple(nullptr, n)); // null indicates that n was matched against the trigger at the top-level
         }
 
         m_pc             = t->get_root();
@@ -2381,6 +2384,7 @@ namespace smt {
             if (m_n1->get_root() != m_n2->get_root())
                 goto backtrack;
 
+            // we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log
             m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
 
             m_pc = m_pc->m_next;
@@ -2777,7 +2781,7 @@ namespace smt {
                     m_pattern_instances.pop_back();
                     m_pattern_instances.push_back(m_app);
                     // continue succeeded
-                    update_max_generation(m_app, nullptr);
+                    update_max_generation(m_app, nullptr); // null indicates a top-level match
                     TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager););
                     m_num_args = c->m_num_args;
                     m_oreg     = c->m_oreg;
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 45d5f15d3..f3c3fc69f 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -959,7 +959,7 @@ namespace smt {
         bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings);
 
         bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation,
-                          unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes);
+                          unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
 
         void set_global_generation(unsigned generation) { m_generation = generation; }
 
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 63297f829..0a522c072 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -204,9 +204,13 @@ namespace smt {
             if (f) {
                 if (has_trace_stream()) {
                     std::ostream & out = trace_stream();
+
+                    // 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]);
                     }
+
                     for (auto n : used_enodes) {
                         enode *orig = std::get<0>(n);
                         enode *substituted = std::get<1>(n);
@@ -215,6 +219,8 @@ namespace smt {
                             log_justification_to_root(out, substituted);
                         }
                     }
+
+                    // 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.
diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h
index 1b1c3547e..3c95d1e23 100644
--- a/src/smt/smt_quantifier.h
+++ b/src/smt/smt_quantifier.h
@@ -58,7 +58,7 @@ namespace smt {
                           unsigned max_generation,
                           unsigned min_top_generation,
                           unsigned max_top_generation,
-                          vector<std::tuple<enode *, enode *>> & used_enodes);
+                          vector<std::tuple<enode *, enode *>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
         bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0);
 
         void init_search_eh();