From f828933ce297f228d6b3c386d3ec7538da0a4ca9 Mon Sep 17 00:00:00 2001
From: omriisack <39183763+omriisack@users.noreply.github.com>
Date: Tue, 3 Dec 2024 12:14:28 +0200
Subject: [PATCH] Add statistics for lemma counting

---
 src/common/Statistics.cpp     |  3 +++
 src/common/Statistics.h       |  3 ++-
 src/engine/BoundManager.cpp   |  2 +-
 src/engine/Engine.cpp         | 10 ++++++++++
 src/engine/Engine.h           |  5 +++++
 src/engine/IEngine.h          |  7 +++++++
 src/engine/tests/MockEngine.h |  4 ++++
 7 files changed, 32 insertions(+), 2 deletions(-)

diff --git a/src/common/Statistics.cpp b/src/common/Statistics.cpp
index e750a7973..f7efa15e7 100644
--- a/src/common/Statistics.cpp
+++ b/src/common/Statistics.cpp
@@ -42,6 +42,7 @@ Statistics::Statistics()
     _unsignedAttributes[TOTAL_NUMBER_OF_VALID_CASE_SPLITS] = 0;
     _unsignedAttributes[NUM_CERTIFIED_LEAVES] = 0;
     _unsignedAttributes[NUM_DELEGATED_LEAVES] = 0;
+    _unsignedAttributes[NUM_LEMMAS] = 0;
     _unsignedAttributes[CERTIFIED_UNSAT] = 0;
 
     _longAttributes[NUM_MAIN_LOOP_ITERATIONS] = 0;
@@ -426,6 +427,8 @@ void Statistics::print()
             getUnsignedAttribute( Statistics::NUM_CERTIFIED_LEAVES ) );
     printf( "\tNumber of leaves to delegate: %u\n",
             getUnsignedAttribute( Statistics::NUM_DELEGATED_LEAVES ) );
+    printf( "\tNumber of lemmas: %u\n",
+            getUnsignedAttribute( Statistics::NUM_LEMMAS ) );
 }
 
 unsigned long long Statistics::getTotalTimeInMicro() const
diff --git a/src/common/Statistics.h b/src/common/Statistics.h
index 03795187c..4761594b4 100644
--- a/src/common/Statistics.h
+++ b/src/common/Statistics.h
@@ -67,9 +67,10 @@ class Statistics
         // branches of the search tree, that have since been popped)
         TOTAL_NUMBER_OF_VALID_CASE_SPLITS,
 
-        // Total number of delegated and certified leaves in the search tree
+        // Total number of delegated leaves, certified leaves and lemmas in the search tree
         NUM_CERTIFIED_LEAVES,
         NUM_DELEGATED_LEAVES,
+        NUM_LEMMAS,
 
         // 1 if returned UNSAT and proof was certified by proof checker, 0 otherwise.
         CERTIFIED_UNSAT,
diff --git a/src/engine/BoundManager.cpp b/src/engine/BoundManager.cpp
index 6b6200cc5..5c8c9d156 100644
--- a/src/engine/BoundManager.cpp
+++ b/src/engine/BoundManager.cpp
@@ -469,7 +469,7 @@ bool BoundManager::addLemmaExplanationAndTightenBound( unsigned var,
                                                                         affectedVarBound,
                                                                         allExplanations,
                                                                         constraintType );
-        _engine->getUNSATCertificateCurrentPointer()->addPLCLemma( PLCExpl );
+        _engine->addPLCLemma( PLCExpl );
         affectedVarBound == Tightening::UB ? _engine->updateGroundUpperBound( var, value )
                                            : _engine->updateGroundLowerBound( var, value );
         resetExplanation( var, affectedVarBound );
diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp
index 753efa45c..ee3afa241 100644
--- a/src/engine/Engine.cpp
+++ b/src/engine/Engine.cpp
@@ -3793,3 +3793,13 @@ void Engine::extractBounds( IQuery &inputQuery )
         }
     }
 }
+
+void Engine::addPLCLemma( std::shared_ptr<PLCLemma> &explanation )
+{
+    if ( !_produceUNSATProofs )
+        return;
+
+    ASSERT( explanation && _UNSATCertificate && _UNSATCertificateCurrentPointer )
+    _statistics.incUnsignedAttribute( Statistics::NUM_LEMMAS );
+    _UNSATCertificateCurrentPointer->get()->addPLCLemma( explanation );
+}
\ No newline at end of file
diff --git a/src/engine/Engine.h b/src/engine/Engine.h
index 15521a56e..167fcac46 100644
--- a/src/engine/Engine.h
+++ b/src/engine/Engine.h
@@ -300,6 +300,11 @@ class Engine
     */
     void propagateBoundManagerTightenings();
 
+    /*
+      Add lemma to the UNSAT Certificate
+    */
+    void addPLCLemma( std::shared_ptr<PLCLemma> &explanation );
+
 private:
     enum BasisRestorationRequired {
         RESTORATION_NOT_NEEDED = 0,
diff --git a/src/engine/IEngine.h b/src/engine/IEngine.h
index 9b9108b20..ea592bb4e 100644
--- a/src/engine/IEngine.h
+++ b/src/engine/IEngine.h
@@ -19,6 +19,7 @@
 #include "BoundExplainer.h"
 #include "DivideStrategy.h"
 #include "List.h"
+#include "PlcLemma.h"
 #include "SnCDivideStrategy.h"
 #include "TableauStateStorageLevel.h"
 #include "Vector.h"
@@ -31,6 +32,7 @@
 class EngineState;
 class Equation;
 class PiecewiseLinearCaseSplit;
+class PLCLemma;
 class SmtState;
 class String;
 class PiecewiseLinearConstraint;
@@ -184,6 +186,11 @@ class IEngine
       Propagate bound tightenings stored in the BoundManager
     */
     virtual void propagateBoundManagerTightenings() = 0;
+
+    /*
+      Add lemma to the UNSAT Certificate
+    */
+    virtual void addPLCLemma( std::shared_ptr<PLCLemma> &explanation ) = 0;
 };
 
 #endif // __IEngine_h__
diff --git a/src/engine/tests/MockEngine.h b/src/engine/tests/MockEngine.h
index eaeee8b89..4bab58130 100644
--- a/src/engine/tests/MockEngine.h
+++ b/src/engine/tests/MockEngine.h
@@ -286,6 +286,10 @@ class MockEngine : public IEngine
     {
         return true;
     }
+
+    void addPLCLemma( std::shared_ptr<PLCLemma> & /*explanation*/ )
+    {
+    }
 };
 
 #endif // __MockEngine_h__