From 5435942228bcfd8d482da0140b0a2c619ab651fd Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 9 Aug 2019 15:10:24 -0700
Subject: [PATCH] add statistics on horner's heuristic

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/horner.cpp    | 7 +++++--
 src/math/lp/lp_settings.h | 3 +++
 src/smt/theory_lra.cpp    | 3 +++
 3 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 4c6996327..0d87a728b 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -72,6 +72,7 @@ bool horner::lemmas_on_expr(nex& e) {
                            TRACE("nla_horner", tout << "callback n = " << n << "\ni="; m_intervals.display(tout, i) << "\n";);
                            
                            conflict = m_intervals.check_interval_for_conflict_on_zero(i);
+                           c().lp_settings().st().m_cross_nested_forms++;
                            m_intervals.reset(); // clean the memory allocated by the interval bound dependencies
                            return conflict;
                        },
@@ -94,7 +95,7 @@ void horner::horner_lemmas() {
         TRACE("nla_solver", tout << "not generating horner lemmas\n";);
         return;
     }
-
+    c().lp_settings().st().m_horner_calls++;
     const auto& matrix = c().m_lar_solver.A_r();
     // choose only rows that depend on m_to_refine variables
     std::set<unsigned> rows_to_check; // we need it to be determenistic: cannot work with the unordered_set
@@ -112,8 +113,10 @@ void horner::horner_lemmas() {
     unsigned sz = rows.size();
     for (unsigned i = 0; i < sz; i++) {
         unsigned row_index = rows[(i + r) % sz];
-        if (lemmas_on_row(matrix.m_rows[row_index]))
+        if (lemmas_on_row(matrix.m_rows[row_index])) {
+            c().lp_settings().st().m_horner_conflicts++;
             break;
+        }
     }
 }
 
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index a7c619498..9a10b7731 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -107,6 +107,9 @@ struct stats {
     unsigned m_hnf_cutter_calls;
     unsigned m_hnf_cuts;
     unsigned m_nla_calls;
+    unsigned m_horner_calls;
+    unsigned m_horner_conflicts;
+    unsigned m_cross_nested_forms;
     stats() { reset(); }
     void reset() { memset(this, 0, sizeof(*this)); }
 };
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index da82c350f..e57b6d6f3 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3784,6 +3784,9 @@ public:
         st.update("arith-patches", lp().settings().st().m_patches);
         st.update("arith-patches-success", lp().settings().st().m_patches_success);
         st.update("arith-hnf-calls", lp().settings().st().m_hnf_cutter_calls);
+        st.update("horner-calls", lp().settings().st().m_horner_calls);
+        st.update("horner-conflicts", lp().settings().st().m_horner_conflicts);
+        st.update("horner-cross-nested-forms", lp().settings().st().m_cross_nested_forms);
         st.update("nla-explanations", m_stats.m_nla_explanations);
         st.update("nla-lemmas", m_stats.m_nla_lemmas);
     }