modular Axiom Profiler (#4619)

* Rocco first commit

* Rocco: clean the log

* Rocco: version 0.1 beta of the causality graph

* Rocco: minimal fix to separate lines

* Rocco: fix the enodes

* Rocco: our trace has to reflect same behaviour of the native trace for what concern used_enodes

* Rocco: disable trace when dummy instantiations

* Rocco: fix to enodes

* Update README.md

* Rocco: remove causality details and add the pattern (trigger)

* Rocco: add ; at the end of the bindings

* Rocco: add triggers as separate trace

* Rocco README file

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Update README.md

* Rocco: bug in tout flush

* Update README.md

* Update README.md

* Rocco: clean code

* Ready for pull request

* Remove commented line bindings

* Add space between // and first char

* Substitute or with || for compatibility; Add space around >

src/ast/rewriter/rewriter_def.h

@@ -654,10 +654,9 @@ void rewriter_tpl<Config>::cleanup() {
 
 template<typename Config>
 void rewriter_tpl<Config>::display_bindings(std::ostream& out) {
-    out << "bindings:\n";
     for (unsigned i = 0; i < m_bindings.size(); i++) {
         if (m_bindings[i])
-            out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";
+            out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << ";\n";
     }
 }
 
@@ -674,6 +673,7 @@ void rewriter_tpl<Config>::set_bindings(unsigned num_bindings, expr * const * bi
         m_shifts.push_back(num_bindings);
     }
     TRACE("rewriter", display_bindings(tout););
+    SCTRACE("bindings", is_trace_enabled("coming_from_quant"), display_bindings(tout););
 }
 
 template<typename Config>
@@ -687,6 +687,7 @@ void rewriter_tpl<Config>::set_inv_bindings(unsigned num_bindings, expr * const
         m_shifts.push_back(num_bindings);
     }
     TRACE("rewriter", display_bindings(tout););
+    SCTRACE("bindings", is_trace_enabled("coming_from_quant"), display_bindings(tout););
 }
 
 template<typename Config>

src/ast/rewriter/var_subst.cpp

@@ -27,6 +27,17 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args)
     expr_ref result(m_reducer.m());
     if (is_ground(n)) {
         result = n;
+        //application does not have free variables or nested quantifiers.
+        //There is no need to print the bindings here?
+        SCTRACE("bindings", is_trace_enabled("coming_from_quant"),
+                tout << "(ground)\n";
+                        for (unsigned i = 0; i < num_args; i++) {
+                            if (args[i]) {
+                                tout << i << ": " << mk_ismt2_pp(args[i], result.m()) << ";\n";
+                            }
+                        }
+                        tout.flush(););
+
         return result;
     }
     SASSERT(is_well_sorted(result.m(), n));

src/smt/cached_var_subst.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include "smt/cached_var_subst.h"
+#include "ast/rewriter/rewriter_def.h"
 
 bool cached_var_subst::key_eq_proc::operator()(cached_var_subst::key * k1, cached_var_subst::key * k2) const {
     if (k1->m_qa != k2->m_qa)
@@ -58,6 +59,13 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e
         // entry was already there
         m_new_keys[num_bindings] = new_key; // recycle key
         result = entry->get_data().m_value;
+        SCTRACE("bindings", is_trace_enabled("coming_from_quant"),tout << "(cache)\n";
+            for (unsigned i = 0; i < num_bindings; i++) {
+                if (new_key->m_bindings[i]) {
+                    tout << i << ": " << mk_ismt2_pp(new_key->m_bindings[i], result.m()) << ";\n";
+                }
+            }
+            tout.flush(););
         return;
     }
 

src/smt/mam.cpp

@@ -1893,7 +1893,7 @@ namespace {
         void update_max_generation(enode * n, enode * prev) {
             m_max_generation = std::max(m_max_generation, n->get_generation());
 
-            if (m.has_trace_stream())
+            if (m.has_trace_stream() || is_trace_enabled("causality"))
                 m_used_enodes.push_back(std::make_tuple(prev, n));
         }
 
@@ -2309,7 +2309,7 @@ namespace {
         m_pattern_instances.push_back(n);
         m_max_generation = n->get_generation();
 
-        if (m.has_trace_stream()) {
+        if (m.has_trace_stream() || is_trace_enabled("causality")) {
             m_used_enodes.reset();
             m_used_enodes.push_back(std::make_tuple(nullptr, n)); // null indicates that n was matched against the trigger at the top-level
         }
@@ -2408,7 +2408,7 @@ namespace {
                 goto backtrack;
             
             // We will use the common root when instantiating the quantifier => log the necessary equalities
-            if (m.has_trace_stream()) {
+            if (m.has_trace_stream() || is_trace_enabled("causality")) {
                 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()));
             }
@@ -2425,7 +2425,7 @@ namespace {
                 goto backtrack;
 
             // we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log
-            if (m.has_trace_stream()) {
+            if (m.has_trace_stream() || is_trace_enabled("causality")) {
                 m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
             }
 
@@ -2611,7 +2611,7 @@ namespace {
             if (m_n1 == 0 || !m_context.is_relevant(m_n1))                                                                                                              \
                 goto backtrack;                                                                                                                                         \
             update_max_generation(m_n1, nullptr);                                                                                                                       \
-            if (m.has_trace_stream()) {                                                                                                                     \
+            if (m.has_trace_stream() || is_trace_enabled("causality")) {                                                                                                                     \
                 for (unsigned i = 0; i < static_cast<const get_cgr *>(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()));                                                           \
                 }                                                                                                                                                       \
@@ -2707,7 +2707,7 @@ namespace {
         backtrack_point & bp = m_backtrack_stack[m_top - 1];
         m_max_generation     = bp.m_old_max_generation;
 
-        if (m.has_trace_stream())
+        if (m.has_trace_stream() || is_trace_enabled("causality"))
             m_used_enodes.shrink(bp.m_old_used_enodes_size);
 
         TRACE("mam_int", tout << "backtrack top: " << bp.m_instr << " " << *(bp.m_instr) << "\n";);

src/smt/qi_queue.cpp

@@ -202,11 +202,26 @@ namespace smt {
         ent.m_instantiated = true;
 
         TRACE("qi_queue_profile", tout << q->get_qid() << ", gen: " << generation << " " << *f << " cost: " << ent.m_cost << "\n";);
+        // NEVER remove coming_from_quant
+        // "coming_from_quant" allows the logging of bindings and enodes
+        // only when they come from instantiations
+        enable_trace("coming_from_quant");
+        quantifier_stat * stat = m_qm.get_stat(q);
 
         if (m_checker.is_sat(q->get_expr(), num_bindings, bindings)) {
             TRACE("checker", tout << "instance already satisfied\n";);
+            // we log the "dummy" instantiations separately from "instance"
+            STRACE("dummy", tout << "### " << static_cast<void*>(f) <<", " << q->get_qid() << "\n";);
+            STRACE("dummy", tout << "Instance already satisfied (dummy)\n";);
+            // a dummy instantiation is still an instantiation.
+            // in this way smt.qi.profile=true coincides with the axiom profiler
+            stat->inc_num_instances_checker_sat();
+            disable_trace("coming_from_quant");
             return;
         }
+
+        STRACE("instance", tout << "### " << static_cast<void*>(f) <<", " << q->get_qid()  << "\n";);
+
         expr_ref instance(m);
         m_subst(q, num_bindings, bindings, instance);
 
@@ -219,15 +234,17 @@ namespace smt {
         if (m.is_true(s_instance)) {
             TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m););
 
+            STRACE("instance", tout <<  "Instance reduced to true\n";);
+            stat -> inc_num_instances_simplify_true();
             if (m.has_trace_stream()) {
                 display_instance_profile(f, q, num_bindings, bindings, pr ? pr->get_id() : 0, generation);
                 m.trace_stream() << "[end-of-instance]\n";
             }
 
+            disable_trace("coming_from_quant");
             return;
         }
         TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";);
-        quantifier_stat * stat = m_qm.get_stat(q);
         stat->inc_num_instances();
         if (stat->get_num_instances() % m_params.m_qi_profile_freq == 0) {
             m_qm.display_stats(verbose_stream(), q);
@@ -312,6 +329,8 @@ namespace smt {
         if (m.has_trace_stream())
             m.trace_stream() << "[end-of-instance]\n";
 
+        // NEVER remove coming_from_quant
+        disable_trace("coming_from_quant");
     }
 
     void qi_queue::push_scope() {

src/smt/smt_internalizer.cpp

@@ -1011,9 +1011,10 @@ namespace smt {
         m_stats.m_num_mk_enode++;
         TRACE("mk_enode", tout << "created enode: #" << e->get_owner_id() << " for:\n" << mk_pp(n, m) << "\n";
               if (e->get_num_args() > 0) {
-                  tout << "is_true_eq: " << e->is_true_eq() << " in cg_table: " << m_cg_table.contains_ptr(e) << " is_cgr: " 
+                  tout << "is_true_eq: " << e->is_true_eq() << " in cg_table: " << m_cg_table.contains_ptr(e) << " is_cgr: "
                        << e->is_cgr() << "\n";
               });
+        SCTRACE("causality", is_trace_enabled("coming_from_quant"), tout << "EN: #" << e->get_owner_id() << "\n";);
 
         if (m.has_trace_stream())
             m.trace_stream() << "[attach-enode] #" << n->get_id() << " " << m_generation << "\n";        

src/smt/smt_quantifier.cpp

@@ -170,15 +170,21 @@ namespace smt {
         void display_stats(std::ostream & out, quantifier * q) {
             quantifier_stat * s     = get_stat(q);
             unsigned num_instances  = s->get_num_instances();
+            unsigned num_instances_simplify_true = s->get_num_instances_simplify_true();
+            unsigned num_instances_checker_sat  = s->get_num_instances_checker_sat();
             unsigned max_generation = s->get_max_generation();
             float max_cost          = s->get_max_cost();
-            if (num_instances > 0) {
+            if (num_instances > 0 || num_instances_simplify_true>0 || num_instances_checker_sat>0) {
                 out << "[quantifier_instances] ";
                 out.width(10);
                 out << q->get_qid().str() << " : ";
                 out.width(6);
                 out << num_instances << " : ";
                 out.width(3);
+                out << num_instances_simplify_true << " : ";
+                out.width(3);
+                out << num_instances_checker_sat << " : ";
+                out.width(3);
                 out << max_generation << " : " << max_cost << "\n";
             }
         }
@@ -199,6 +205,33 @@ namespace smt {
             return m_plugin->is_shared(n);
         }
 
+        void log_causality(
+                fingerprint* f,
+                app * pat,
+                vector<std::tuple<enode *, enode *>> & used_enodes) {
+
+            if (pat != nullptr) {
+                if (used_enodes.size() > 0) {
+                    STRACE("causality", tout << "New-Match: "<< static_cast<void*>(f););
+                    STRACE("triggers",  tout <<", Pat: "<< expr_ref(pat, m()););
+                    STRACE("causality", tout <<", Father:";);
+                }
+                for (auto n : used_enodes) {
+                    enode *orig = std::get<0>(n);
+                    enode *substituted = std::get<1>(n);
+                    if (orig == nullptr) {
+                        STRACE("causality", tout << " #" << substituted->get_owner_id(););
+                    }
+                    else {
+                        STRACE("causality", tout << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";);
+                    }
+                }
+                if (used_enodes.size() > 0) {
+                    STRACE("causality", tout << "\n";);
+                }
+            }
+        }
+
         void log_add_instance(
              fingerprint* f,
              quantifier * q, app * pat,
@@ -261,6 +294,7 @@ namespace smt {
                           unsigned min_top_generation,
                           unsigned max_top_generation,
                           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;
@@ -268,6 +302,9 @@ namespace smt {
             get_stat(q)->update_max_generation(max_generation);
             fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def);
             if (f) {
+                if (is_trace_enabled("causality")) {
+                    log_causality(f,pat,used_enodes);
+                }
                 if (has_trace_stream()) {
                     log_add_instance(f, q, pat, num_bindings, bindings, used_enodes);
                 }

src/smt/smt_quantifier_stat.cpp

@@ -27,6 +27,8 @@ namespace smt {
         m_case_split_factor(1),
         m_num_nested_quantifiers(0),
         m_num_instances(0),
+        m_num_instances_checker_sat(0),
+        m_num_instances_simplify_true(0),
         m_num_instances_curr_search(0),
         m_num_instances_curr_branch(0),
         m_max_generation(0),

src/smt/smt_quantifier_stat.h

@@ -36,6 +36,8 @@ namespace smt {
         unsigned m_case_split_factor; //!< the product of the size of the clauses created by this quantifier.
         unsigned m_num_nested_quantifiers;
         unsigned m_num_instances;
+        unsigned m_num_instances_checker_sat;
+        unsigned m_num_instances_simplify_true;
         unsigned m_num_instances_curr_search;
         unsigned m_num_instances_curr_branch; //!< only updated if QI_TRACK_INSTANCES is true
         unsigned m_max_generation; //!< max. generation of an instance
@@ -69,6 +71,12 @@ namespace smt {
         unsigned get_num_instances() const {
             return m_num_instances;
         }
+        unsigned get_num_instances_simplify_true() const {
+            return m_num_instances_simplify_true;
+        }
+        unsigned get_num_instances_checker_sat() const {
+            return m_num_instances_checker_sat;
+        }
 
         unsigned get_num_instances_curr_search() const {
             return m_num_instances_curr_search;
@@ -77,6 +85,14 @@ namespace smt {
         unsigned & get_num_instances_curr_branch() {
             return m_num_instances_curr_branch;
         }
+
+        void inc_num_instances_simplify_true() {
+            m_num_instances_simplify_true++;
+        }
+
+        void inc_num_instances_checker_sat() {
+            m_num_instances_checker_sat++;
+        }
         
         void inc_num_instances() {
             m_num_instances++;

src/util/trace.h

@@ -52,4 +52,6 @@ static inline void finalize_trace() {}
 
 #define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { CODE tout.flush(); })
 
+#define SCTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { CODE tout.flush(); })
+
 #define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })