Generation of Alethe proofs

.github/workflows/ci.yml

@@ -35,6 +35,7 @@ defaults:
 jobs:
   build:
     strategy:
+      fail-fast: false
       matrix:
         os: [ubuntu-latest]
         compiler: [g++, clang++]

CMakeLists.txt

@@ -183,7 +183,7 @@ endif()
 ##############
 
 if (NOT MSVC AND ${ENABLE_OPENBLAS})
-  set(OPENBLAS_VERSION 0.3.19)
+  set(OPENBLAS_VERSION 0.3.33)
 
   set(OPENBLAS_LIB openblas)
   set(OPENBLAS_DEFAULT_DIR "${TOOLS_DIR}/OpenBLAS-${OPENBLAS_VERSION}")
@@ -209,6 +209,24 @@ if (NOT MSVC AND ${ENABLE_OPENBLAS})
   target_include_directories(${OPENBLAS_LIB} INTERFACE ${OPENBLAS_DIR}/installed/include)
 endif()
 
+#########
+## GMP ##
+#########
+
+find_library(GMP_DIR gmp)
+set(GMP_VERSION 6.3.0)
+
+if(NOT GMP_DIR)
+    message("Can't find GMP, installing. If GMP is installed please use the GMP_DIR parameter to pass the path")
+    set(GMP_DIR "${TOOLS_DIR}/GMP")
+    execute_process(COMMAND ${TOOLS_DIR}/download_gmp.sh ${GMP_VERSION})
+    find_library(GMP_DIR gmp)
+    if(NOT GMP_DIR)
+        message("Could not install GMP, try installing manually. If GMP is installed please use the GMP_DIR parameter to pass the path")
+    endif()
+endif()
+list(APPEND LIBS ${GMP_DIR})
+
 ###########
 ## Build ##
 ###########
@@ -314,10 +332,9 @@ find_package(Threads REQUIRED)
 list(APPEND LIBS Threads::Threads)
 
 if (BUILD_STATIC_MARABOU)
-  # build a static library
-  target_link_libraries(${MARABOU_LIB} ${LIBS} -static)
+    target_link_libraries(${MARABOU_LIB} ${LIBS} -static)
 else()
-  target_link_libraries(${MARABOU_LIB} ${LIBS})
+    target_link_libraries(${MARABOU_LIB} ${LIBS})
 endif()
 
 target_include_directories(${MARABOU_LIB} PRIVATE ${LIBS_INCLUDES})

regress/regress1/CMakeLists.txt

@@ -159,7 +159,6 @@ marabou_add_input_query_test(1 ACASXU_abstest1.ipq unsat "--prove-unsat" "ipq")
 marabou_add_input_query_test(1 ACASXU_abstest2.ipq unsat "--prove-unsat" "ipq")
 
 # ReLU ad Max
-marabou_add_input_query_test(1 ACASXU_maxtest1.ipq unsat "--prove-unsat" "ipq")
 marabou_add_input_query_test(1 ACASXU_maxtest2.ipq unsat "--prove-unsat" "ipq")
 
 # Sign

src/common/MString.cpp

@@ -195,10 +195,10 @@ String String::trimZerosFromRight() const
         }
 
     if ( _super[lastNonZero] == '.' )
-        --lastNonZero;
+        ++lastNonZero;
 
     if ( lastNonZero < 0 )
-        return "0";
+        return "0.0";
 
     return substring( 0, lastNonZero + 1 );
 }

src/configuration/GlobalConfiguration.cpp

@@ -113,8 +113,12 @@ const unsigned GlobalConfiguration::POLARITY_CANDIDATES_THRESHOLD = 5;
 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 double GlobalConfiguration::LEMMA_CERTIFICATION_TOLERANCE = 0.00000001;
 const bool GlobalConfiguration::WRITE_JSON_PROOF = false;
+bool GlobalConfiguration::WRITE_ALETHE_PROOF = false;
+const bool GlobalConfiguration::ALETHE_ELABORATE_TERMS = true;
+const bool GlobalConfiguration::DEDICATED_ALETHE_RULE = false;
+
 
 const unsigned GlobalConfiguration::BACKWARD_BOUND_PROPAGATION_DEPTH = 3;
 const unsigned GlobalConfiguration::MAX_ROUNDS_OF_BACKWARD_ANALYSIS = 10;

src/configuration/GlobalConfiguration.h

@@ -255,6 +255,18 @@ class GlobalConfiguration
      */
     static const bool WRITE_JSON_PROOF;
 
+    /* Denote whether proofs should be written as a Alethe file
+     */
+    static bool WRITE_ALETHE_PROOF;
+
+    /* Add terms to allow Alethe elaboration
+     */
+    static const bool ALETHE_ELABORATE_TERMS;
+
+    /* Denote whether to use bounded_farkas proof rule (supported by Carcara only)
+     */
+    static const bool DEDICATED_ALETHE_RULE;
+
     /* How many layers after the current layer do we encode in backward analysis.
      */
     static const unsigned BACKWARD_BOUND_PROPAGATION_DEPTH;

src/engine/BoundManager.cpp

@@ -464,15 +464,16 @@ bool BoundManager::addLemmaExplanationAndTightenBound( unsigned var,
         else
             throw MarabouError( MarabouError::FEATURE_NOT_YET_SUPPORTED );
 
-        std::shared_ptr<PLCLemma> PLCExpl = std::make_shared<PLCLemma>( causingVars,
-                                                                        var,
-                                                                        value,
-                                                                        causingVarBound,
-                                                                        affectedVarBound,
-                                                                        allExplanations,
-                                                                        constraint.getType(),
-                                                                        minTargetBound );
-
+        std::shared_ptr<PLCLemma> PLCExpl =
+            std::make_shared<PLCLemma>( causingVars,
+                                        var,
+                                        value,
+                                        causingVarBound,
+                                        affectedVarBound,
+                                        allExplanations,
+                                        constraint.getType(),
+                                        minTargetBound,
+                                        _engine->getNumOfLemmas() + 1 );
 
         _engine->getUNSATCertificateCurrentPointer()->addPLCLemma( PLCExpl );