Merge branch 'NeuralNetworkVerification:master' into Backward-Forward…

…-Algorithm

src/common/Statistics.cpp

@@ -42,6 +42,8 @@ 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;
     _longAttributes[NUM_SIMPLEX_STEPS] = 0;
@@ -425,6 +427,7 @@ 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

src/common/Statistics.h

@@ -67,9 +67,13 @@ 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,
     };
 
     enum StatisticsLongAttribute {

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 );

src/engine/Engine.cpp

@@ -3660,6 +3660,7 @@ bool Engine::certifyUNSATCertificate()
     if ( certificationSucceeded )
     {
         printf( "Certified\n" );
+        _statistics.incUnsignedAttribute( Statistics::CERTIFIED_UNSAT );
         if ( _statistics.getUnsignedAttribute( Statistics::NUM_DELEGATED_LEAVES ) )
             printf( "Some leaves were delegated and need to be certified separately by an SMT "
                     "solver\n" );
@@ -3794,3 +3795,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 );
+}

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,

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__

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__