Improved quantifier instantiation logging

src/smt/mam.cpp

@@ -1866,7 +1866,7 @@ namespace smt {
         enode *             m_n2;
         enode *             m_app;
         const bind *        m_b;
-        ptr_vector<enode>   m_used_enodes;
+        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
         unsigned_vector     m_min_top_generation, m_max_top_generation;
@@ -1883,11 +1883,11 @@ namespace smt {
             m_pool.recycle(v);
         }
 
-        void update_max_generation(enode * n) {
+        void update_max_generation(enode * n, enode * prev) {
             m_max_generation = std::max(m_max_generation, n->get_generation());
 
             if (m_ast_manager.has_trace_stream())
-                m_used_enodes.push_back(n);
+                m_used_enodes.push_back(std::make_tuple(prev, n));
         }
 
         // We have to provide the number of expected arguments because we have flat-assoc applications such as +.
@@ -1896,7 +1896,7 @@ namespace smt {
             enode * first = curr;
             do {
                 if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
-                    update_max_generation(curr);
+                    update_max_generation(curr, first);
                     return curr;
                 }
                 curr = curr->get_next();
@@ -1909,7 +1909,7 @@ namespace smt {
             curr = curr->get_next();
             while (curr != first) {
                 if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
-                    update_max_generation(curr);
+                    update_max_generation(curr, first);
                     return curr;
                 }
                 curr = curr->get_next();
@@ -1933,7 +1933,7 @@ namespace smt {
                 do {
                     if (n->get_decl() == f &&
                         n->get_arg(0)->get_root() == m_args[0]) {
-                        update_max_generation(n);
+                        update_max_generation(n, first);
                         return true;
                     }
                     n = n->get_next();
@@ -1948,7 +1948,7 @@ namespace smt {
                     if (n->get_decl() == f &&
                         n->get_arg(0)->get_root() == m_args[0] &&
                         n->get_arg(1)->get_root() == m_args[1]) {
-                        update_max_generation(n);
+                        update_max_generation(n, first);
                         return true;
                     }
                     n = n->get_next();
@@ -1968,7 +1968,7 @@ namespace smt {
                                 break;
                         }
                         if (i == num_args) {
-                            update_max_generation(n);
+                            update_max_generation(n, first);
                             return true;
                         }
                     }
@@ -2213,7 +2213,7 @@ namespace smt {
         if (bp.m_it == bp.m_end)
             return nullptr;
         m_top++;
-        update_max_generation(*(bp.m_it));
+        update_max_generation(*(bp.m_it), nullptr);
         return *(bp.m_it);
     }
 
@@ -2294,7 +2294,7 @@ namespace smt {
 
         if (m_ast_manager.has_trace_stream()) {
             m_used_enodes.reset();
-            m_used_enodes.push_back(n);
+            m_used_enodes.push_back(std::make_tuple(nullptr, n));
         }
 
         m_pc             = t->get_root();
@@ -2399,6 +2399,9 @@ namespace smt {
             SASSERT(m_n2 != 0);
             if (m_n1->get_root() != m_n2->get_root())
                 goto backtrack;
+            
+            m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
+
             m_pc = m_pc->m_next;
             goto main_loop;
 
@@ -2793,7 +2796,7 @@ namespace smt {
                     m_pattern_instances.pop_back();
                     m_pattern_instances.push_back(m_app);
                     // continue succeeded
-                    update_max_generation(m_app);
+                    update_max_generation(m_app, nullptr);
                     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;
@@ -3932,7 +3935,7 @@ namespace smt {
         }
 #endif
 
-        void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) override {
+        void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector<std::tuple<enode *, enode *>> & used_enodes) override {
             TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";);
 #ifdef Z3DEBUG
             if (m_check_missing_instances) {

src/smt/mam.h

@@ -21,6 +21,7 @@ Revision History:
 
 #include "ast/ast.h"
 #include "smt/smt_types.h"
+#include <tuple>
 
 namespace smt {
     /**
@@ -57,7 +58,7 @@ namespace smt {
 
         virtual void display(std::ostream& out) = 0;
         
-        virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) = 0;
+        virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector<std::tuple<enode *, enode *>> & used_enodes) = 0;
         
         virtual bool is_shared(enode * n) const = 0;
 

src/smt/smt_context.cpp

@@ -558,6 +558,7 @@ namespace smt {
             invert_trans(n1);
             n1->m_trans.m_target        = n2;
             n1->m_trans.m_justification = js;
+            n1->m_proof_is_logged       = false;
             SASSERT(r1->trans_reaches(n1));
             // ---------------
             // r1 -> ..  -> n1 -> n2 -> ... -> r2
@@ -749,6 +750,7 @@ namespace smt {
             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;
             prev                          = curr;
             js                            = new_js;
             curr                          = new_curr;
@@ -1045,6 +1047,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;
         invert_trans(r1);
         // ---------------
         // n1 -> ... -> r1
@@ -1809,7 +1812,7 @@ namespace smt {
     }
 
     bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation,
-                               unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes) {
+                               unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode *>> & used_enodes) {
         return m_qmanager->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_top_generation, used_enodes);
     }
 

src/smt/smt_context.h

@@ -49,6 +49,7 @@ Revision History:
 #include "util/timer.h"
 #include "util/statistics.h"
 #include "solver/progress_callback.h"
+#include <tuple>
 
 // there is a significant space overhead with allocating 1000+ contexts in
 // the case that each context only references a few expressions.
@@ -946,7 +947,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, ptr_vector<enode> & used_enodes);
+                          unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes);
 
         void set_global_generation(unsigned generation) { m_generation = generation; }
 

src/smt/smt_enode.cpp

@@ -47,6 +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;
         unsigned num_args     = n->get_num_args();
         for (unsigned i = 0; i < num_args; i++) {
             enode * arg  = app2enode[owner->get_arg(i)->get_id()];

src/smt/smt_enode.h

@@ -105,6 +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.
+        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;
@@ -113,6 +114,7 @@ namespace smt {
         friend class context;
         friend class euf_manager;
         friend class conflict_resolution;
+        friend class quantifier_manager;
         
 
         theory_var_list * get_th_var_list() { 
@@ -317,6 +319,10 @@ namespace smt {
 
         theory_var get_th_var(theory_id th_id) const;
 
+        trans_justification get_trans_justification() {
+            return m_trans;
+        }
+
         unsigned get_generation() const {
             return m_generation;
         }

src/smt/smt_model_checker.cpp

@@ -26,6 +26,7 @@ Revision History:
 #include "smt/smt_context.h"
 #include "smt/smt_model_finder.h"
 #include "model/model_pp.h"
+#include <tuple>
 
 namespace smt {
 
@@ -476,7 +477,7 @@ namespace smt {
     void model_checker::assert_new_instances() {
         TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";);
         ptr_buffer<enode> bindings;
-        ptr_vector<enode> dummy;
+        vector<std::tuple<enode *, enode *>> dummy;
         for (instance* inst : m_new_instances) {
             quantifier * q  = inst->m_q;
             if (m_context->b_internalized(q)) {

src/smt/smt_quantifier.cpp

@@ -104,13 +104,64 @@ namespace smt {
             return m_plugin->is_shared(n);
         }
 
+        inline 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;
+                    print_justification(log, it);
+                }
+            }
+            if (!root->m_proof_is_logged) {
+                root->m_proof_is_logged = true;
+                log << "[eq-expl] #" << root->get_owner_id() << " root\n";
+            }
+        }
+
+        inline void print_justification(std::ostream & out, enode *en) {
+            smt::literal lit;
+            unsigned num_args;
+            enode *target = en->get_trans_justification().m_target;
+
+            switch (en->get_trans_justification().m_justification.get_kind()) {
+            case smt::eq_justification::kind::EQUATION:
+                lit = en->get_trans_justification().m_justification.get_literal();
+                out << "[eq-expl] #" << en->get_owner_id() << " lit #" << m_context.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n";
+                break;
+            case smt::eq_justification::kind::AXIOM:
+                out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n";
+                break;
+            case smt::eq_justification::kind::CONGRUENCE:
+                if (!en->get_trans_justification().m_justification.used_commutativity()) {
+                    num_args = en->get_num_args();
+
+                    for (unsigned i = 0; i < num_args; i++) {
+                        
+                        log_transitive_justification(out, en->get_arg(i));
+                        log_transitive_justification(out, target->get_arg(i));
+                    }
+
+                    out << "[eq-expl] #" << en->get_owner_id() << " cg";
+                    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;
+                }
+            default:
+                out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n";
+                break;
+            }
+        }
+
         bool add_instance(quantifier * q, app * pat,
                           unsigned num_bindings,
                           enode * const * bindings,
                           unsigned max_generation,
                           unsigned min_top_generation,
                           unsigned max_top_generation,
-                          ptr_vector<enode> & used_enodes) {
+                          vector<std::tuple<enode *, enode *>> & used_enodes) {
             max_generation = std::max(max_generation, get_generation(q));
             if (m_num_instances > m_params.m_qi_max_instances) {
                 return false;
@@ -120,15 +171,30 @@ namespace smt {
             if (f) {
                 if (has_trace_stream()) {
                     std::ostream & out = trace_stream();
-                    out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id();
+                    for (auto n : used_enodes) {
+                        enode *orig = std::get<0>(n);
+                        enode *substituted = std::get<1>(n);
+                        if (orig != nullptr) {
+                            log_transitive_justification(out, orig);
+                            log_transitive_justification(out, substituted);
+                        }
+                    }
+                    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 (enode* n : used_enodes) 
+                    for (auto n : used_enodes) {
-                        out << " #" << n->get_owner_id();
+                        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
@@ -294,12 +360,12 @@ namespace smt {
                                           unsigned max_generation,
                                           unsigned min_top_generation,
                                           unsigned max_top_generation,
-                                          ptr_vector<enode> & used_enodes) {
+                                          vector<std::tuple<enode *, enode *>> & used_enodes) {
         return m_imp->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_generation, used_enodes);
     }
 
     bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation) {
-        ptr_vector<enode> tmp;
+        vector<std::tuple<enode *, enode *>> tmp;
         return add_instance(q, nullptr, num_bindings, bindings, generation, generation, generation, tmp);
     }
 

src/smt/smt_quantifier.h

@@ -23,6 +23,7 @@ Revision History:
 #include "util/statistics.h"
 #include "util/params.h"
 #include "smt/smt_types.h"
+#include <tuple>
 
 class proto_model;
 struct smt_params;
@@ -57,7 +58,7 @@ namespace smt {
                           unsigned max_generation,
                           unsigned min_top_generation,
                           unsigned max_top_generation,
-                          ptr_vector<enode> & used_enodes);
+                          vector<std::tuple<enode *, enode *>> & used_enodes);
         bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0);
 
         void init_search_eh();

src/smt/smt_quick_checker.cpp

@@ -19,6 +19,7 @@ Revision History:
 #include "smt/smt_context.h"
 #include "smt/smt_quick_checker.h"
 #include "ast/ast_pp.h"
+#include <tuple>
 
 namespace smt {
 
@@ -211,7 +212,7 @@ namespace smt {
     }
 
     bool quick_checker::process_candidates(quantifier * q, bool unsat) {
-        ptr_vector<enode> empty_used_enodes;
+        vector<std::tuple<enode *, enode *>> empty_used_enodes;
         buffer<unsigned> szs;
         buffer<unsigned> it;
         for (unsigned i = 0; i < m_num_bindings; i++) {