Merge branch 'master' into multiple-split-onnx

NeuralNetworkVerification · Jan 4, 2024 · e09704a · e09704a
2 parents f59d01d + c2bf020
commit e09704a
Show file tree

Hide file tree

Showing 64 changed files with 23,384 additions and 583 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,9 +1,8 @@
 # Changelog
 
-## Version 1.1.0
-
-* Added support for onnx networks with `tanh` nodes to command-line interface.
+## Next Release
+* Added support for onnx networks with tanh nodes to command-line interface.
+* Added proof producing versions of Sign, Max, Absolute Value and Disjunction constraints
 
 ## Version 1.0.0
-
 * Initial versioned release
diff --git a/maraboupy/Marabou.py b/maraboupy/Marabou.py
@@ -70,6 +70,7 @@ def read_onnx(filename, inputNames=None, outputNames=None, reindexOutputVars=Tru
         filename (str): Path to the ONNX file
         inputNames (list of str, optional): List of node names corresponding to inputs
         outputNames (list of str, optional): List of node names corresponding to outputs
+        reindexOutputVars (bool): Reindex the variables so that the output variables are immediate after input variables
 
     Returns:
         :class:`~maraboupy.MarabouNetworkONNX.MarabouNetworkONNX`
@@ -144,7 +145,7 @@ def createOptions(numWorkers=1, initialTimeout=5, initialSplits=0, onlineSplits=
                   preprocessorBoundTolerance=0.0000000001, dumpBounds=False,
                   tighteningStrategy="deeppoly", milpTightening="none", milpSolverTimeout=0,
                   numSimulations=10, numBlasThreads=1, performLpTighteningAfterSplit=False,
-                  lpSolver=""):
+                  lpSolver="", produceProofs=False):
     """Create an options object for how Marabou should solve the query
 
     Args:
@@ -197,4 +198,5 @@ def createOptions(numWorkers=1, initialTimeout=5, initialSplits=0, onlineSplits=
     options._numBlasThreads = numBlasThreads
     options._performLpTighteningAfterSplit = performLpTighteningAfterSplit
     options._lpSolver = lpSolver
+    options._produceProofs = produceProofs
     return options
diff --git a/maraboupy/MarabouCore.cpp b/maraboupy/MarabouCore.cpp
@@ -231,7 +231,7 @@ struct MarabouOptions {
         , _tighteningStrategyString( Options::get()->getString( Options::SYMBOLIC_BOUND_TIGHTENING_TYPE ).ascii() )
         , _milpTighteningString( Options::get()->getString( Options::MILP_SOLVER_BOUND_TIGHTENING_TYPE ).ascii() )
         , _lpSolverString( Options::get()->getString( Options::LP_SOLVER ).ascii() )
-        , _produceProofs( Options::get()->getBool( Options::PRODUCE_PROOFS ))
+        , _produceProofs( Options::get()->getBool( Options::PRODUCE_PROOFS ) )
     {};
 
   void setOptions()

diff --git a/regress/regress1/CMakeLists.txt b/regress/regress1/CMakeLists.txt
@@ -140,6 +140,8 @@ foreach(file ${unsat_ipqs})
 endforeach()
 
 # Proof production tests
+
+# ReLU
 marabou_add_acasxu_proof_test(1 "ACASXU_experimental_v2a_5_9" "3" unsat)
 marabou_add_acasxu_proof_test(1 "ACASXU_experimental_v2a_5_7" "3" unsat)
 marabou_add_acasxu_proof_test(1 "ACASXU_experimental_v2a_3_7" "3" unsat)
@@ -150,3 +152,17 @@ marabou_add_coav_proof_test(1 "reluBenchmark0.453322172165s_UNSAT.nnet" unsat)
 marabou_add_coav_proof_test(1 "reluBenchmark0.30711388588s_UNSAT.nnet" unsat)
 marabou_add_coav_proof_test(1 "reluBenchmark0.725997209549s_UNSAT.nnet" unsat)
 marabou_add_coav_proof_test(1 "reluBenchmark1.81178617477s_UNSAT.nnet" unsat)
+
+# Absolute value
+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
+marabou_add_input_query_test(1 deep_6_index_5566.ipq unsat "--prove-unsat" "ipq")
+marabou_add_input_query_test(1 deep_6_index_5567.ipq unsat "--prove-unsat" "ipq")
+marabou_add_input_query_test(1 deep_6_index_5525.ipq unsat "--prove-unsat" "ipq")
+marabou_add_input_query_test(1 deep_6_index_7779.ipq unsat "--prove-unsat" "ipq")