From 3d2bf13577547588cf22a197dbd020324596daa2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 13 Nov 2022 20:30:00 -0800
Subject: [PATCH] streamline statistics, fix bug in updating goals
---
src/ast/simplifiers/elim_unconstrained.cpp | 5 ++++-
src/ast/simplifiers/elim_unconstrained.h | 2 +-
src/tactic/core/elim_uncnstr_tactic.cpp | 5 +++--
3 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 3d94cb0ef..d0eb2a53f 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -96,6 +96,7 @@ void elim_unconstrained::eliminate() {
SASSERT(r->get_sort() == t->get_sort());
m_stats.m_num_eliminated++;
n.m_refcount = 0;
+ m_trail.push_back(r);
SASSERT(r);
gc(e);
@@ -250,7 +251,9 @@ void elim_unconstrained::reconstruct_terms() {
}
void elim_unconstrained::assert_normalized(vector<dependent_expr>& old_fmls) {
- for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+
+ unsigned sz = m_fmls.size();
+ for (unsigned i = m_qhead; i < sz; ++i) {
auto [f, d] = m_fmls[i]();
node& n = get_node(f);
expr* g = n.m_term;
diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h
index 964c56244..b32ab367b 100644
--- a/src/ast/simplifiers/elim_unconstrained.h
+++ b/src/ast/simplifiers/elim_unconstrained.h
@@ -72,7 +72,7 @@ public:
void reduce() override;
- void collect_statistics(statistics& st) const override { st.update("elim-unconstr", m_stats.m_num_eliminated); }
+ void collect_statistics(statistics& st) const override { st.update("elim-unconstrained", m_stats.m_num_eliminated); }
void reset_statistics() override { m_stats.reset(); }
};
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 5f0963bfd..60bdd2710 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -867,6 +867,8 @@ class elim_uncnstr_tactic : public tactic {
void run(goal_ref const & g, goal_ref_buffer & result) {
bool produce_proofs = g->proofs_enabled();
TRACE("goal", g->display(tout););
+ std::function<void(statistics&)> coll = [&](statistics& st) { collect_statistics(st); };
+ statistics_report sreport(coll);
tactic_report report("elim-uncnstr", *g);
m_vars.reset();
collect_occs p;
@@ -959,7 +961,6 @@ public:
void operator()(goal_ref const & g,
goal_ref_buffer & result) override {
run(g, result);
- report_tactic_progress(":num-elim-apps", m_num_elim_apps);
}
void cleanup() override {
@@ -969,7 +970,7 @@ public:
}
void collect_statistics(statistics & st) const override {
- st.update("eliminated applications", m_num_elim_apps);
+ st.update("elim-unconstrained", m_num_elim_apps);
}
void reset_statistics() override {