Write proofs as JSON files

src/configuration/GlobalConfiguration.cpp

@@ -103,6 +103,7 @@ const unsigned GlobalConfiguration::DNC_DEPTH_THRESHOLD = 5;
 
 const double GlobalConfiguration::MINIMAL_COEFFICIENT_FOR_TIGHTENING = 0.01;
 const double GlobalConfiguration::LEMMA_CERTIFICATION_TOLERANCE = 0.000001;
+const bool GlobalConfiguration::WRITE_JSON_PROOF = false;
 
 #ifdef ENABLE_GUROBI
 const unsigned GlobalConfiguration::GUROBI_NUMBER_OF_THREADS = 1;

src/configuration/GlobalConfiguration.h

@@ -243,6 +243,10 @@ class GlobalConfiguration
     */
     static const double LEMMA_CERTIFICATION_TOLERANCE;
 
+    /* Denote whether proofs should be written as a JSON file
+    */
+    static const bool WRITE_JSON_PROOF;
+
 #ifdef ENABLE_GUROBI
     /*
       The number of threads Gurobi spawns

src/engine/Engine.cpp

@@ -3555,7 +3555,14 @@ bool Engine::certifyUNSATCertificate()
         groundLowerBounds[i] = _groundBoundManager.getLowerBound( i );
     }
 
-    Checker unsatCertificateChecker( _UNSATCertificate, _tableau->getM(),  _tableau->getSparseA(),
+    if ( GlobalConfiguration::WRITE_JSON_PROOF )
+    {
+        File file ( "proof.json" );
+        JsonWriter::writeProofToJson( _UNSATCertificate, _tableau->getM(), _tableau->getSparseA(),
+                                      groundUpperBounds, groundLowerBounds, _plConstraints, file );
+    }
+
+    Checker unsatCertificateChecker( _UNSATCertificate, _tableau->getM(), _tableau->getSparseA(),
                                      groundUpperBounds, groundLowerBounds, _plConstraints );
     bool certificationSucceeded = unsatCertificateChecker.check();
 

src/engine/Engine.h

@@ -30,6 +30,7 @@
 #include "GurobiWrapper.h"
 #include "IEngine.h"
 #include "InputQuery.h"
+#include "JsonWriter.h"
 #include "LinearExpression.h"
 #include "LPSolverType.h"
 #include "Map.h"

src/engine/PiecewiseLinearConstraint.h

@@ -466,6 +466,14 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher
         return {};
     }
 
+    /*
+      Get the tableau auxiliary vars
+    */
+    virtual const List<unsigned> &getTableauAuxVars() const
+    {
+        return _tableauAuxVars;
+    }
+
 protected:
     unsigned _numCases; // Number of possible cases/phases for this constraint
                         // (e.g. 2 for ReLU, ABS, SIGN; >=2 for Max and Disjunction )