differentiate fixed from offset-eq in statistics

Z3Prover · Apr 18, 2023 · a2bac11 · a2bac11
1 parent ec1480b
commit a2bac11
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
@@ -578,8 +578,12 @@ class lp_bound_propagator {
               );
 
         bool added = m_imp.add_eq(je, ke, exp, is_fixed);
-        if (added)
-            lp().stats().m_offset_eqs++;
+        if (added) {
+            if (is_fixed)
+                lp().stats().m_fixed_eqs++;
+            else
+                lp().stats().m_offset_eqs++;
+        }
         return added;
     }
 

diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
@@ -121,6 +121,7 @@ struct statistics {
     unsigned m_grobner_calls;
     unsigned m_grobner_conflicts;
     unsigned m_offset_eqs;
+    unsigned m_fixed_eqs;
     statistics() { reset(); }
     void reset() { memset(this, 0, sizeof(*this)); }
     void collect_statistics(::statistics& st) const {
@@ -142,6 +143,7 @@ struct statistics {
         st.update("arith-grobner-calls", m_grobner_calls);
         st.update("arith-grobner-conflicts", m_grobner_conflicts);
         st.update("arith-offset-eqs", m_offset_eqs);
+        st.update("arith-fixed-eqs", m_fixed_eqs);
 
     }
 };