From 280e0275dce0d8c10da425f4d856df07cfa3506e Mon Sep 17 00:00:00 2001 From: yuvaljacoby Date: Thu, 2 Apr 2020 19:27:58 +0300 Subject: [PATCH 1/4] Add python trouble shooting for windows --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 23391036f..5e6219894 100644 --- a/README.md +++ b/README.md @@ -148,6 +148,8 @@ cd build cmake .. -G"Visual Studio 15 2017 Win64" -DBUILD_PYTHON=ON cmake --build . --config Release ``` +Make sure the detected python ("Found PythonInterp: ....") is a windows python and not cygwin or something like that (if it is cygwin, use -DPYTHON_EXECUTABLE flag to override the default python, or manuialy download the linux pybind and locate it in the tools directory) + This process will produce the binary file and the shared library for the Python API. The shared library will be in the maraboupy folder for Linux and MacOS. On Windows, the shared library is written to a Release subfolder in maraboupy, From 742247769565f433a18bcadbc2ecfbc514c275de Mon Sep 17 00:00:00 2001 From: yuvaljacoby Date: Mon, 6 Apr 2020 11:33:14 +0300 Subject: [PATCH 2/4] Optimize floatutils (#191) Move most of FloatUtils implementation to .h (to enable compiler inline optimization) AVG CPU results (on acas xu properties) p1: original: 140421.1 inline: 139222.3 p2: original: 63249.9 inline: 61641.4 p3: original: 23690.4 inline: 22135.7 p4: original: 10303.6 inline: 9252.6 --- src/common/FloatUtils.cpp | 81 ----------------------------- src/common/FloatUtils.h | 107 +++++++++++++++++++++++++++++++------- 2 files changed, 89 insertions(+), 99 deletions(-) diff --git a/src/common/FloatUtils.cpp b/src/common/FloatUtils.cpp index d19b536ac..5fc82baa8 100644 --- a/src/common/FloatUtils.cpp +++ b/src/common/FloatUtils.cpp @@ -15,7 +15,6 @@ #include "FloatUtils.h" #include -#include #include // https://randomascii.wordpress.com/2012/02/25/comparing-floating-point-numbers-2012-edition/ @@ -39,81 +38,6 @@ bool FloatUtils::areEqual( double x, double y, double epsilon ) return false; } -double FloatUtils::abs( double x ) -{ - return fabs( x ); -} - -bool FloatUtils::areDisequal( double x, double y, double epsilon ) -{ - return !areEqual( x, y, epsilon ); -} - -bool FloatUtils::isZero( double x, double epsilon ) -{ - return ( -epsilon <= x ) && ( x <= epsilon ); -} - -double FloatUtils::roundToZero( double x, double epsilon ) -{ - return isZero( x, epsilon ) ? 0.0 : x; -} - -bool FloatUtils::isPositive( double x, double epsilon ) -{ - return ( !isZero( x, epsilon ) ) && ( x > 0.0 ); -} - -bool FloatUtils::isNegative( double x, double epsilon ) -{ - return ( !isZero( x, epsilon ) ) && ( x < 0.0 ); -} - -bool FloatUtils::isFinite( double x ) -{ - return ( x != infinity() ) && ( x != negativeInfinity() ); -} - -bool FloatUtils::gt( double x, double y, double epsilon ) -{ - return isPositive( x - y, epsilon ); -} - -bool FloatUtils::gte( double x, double y, double epsilon ) -{ - return !isNegative( x - y, epsilon ); -} - -bool FloatUtils::lt( double x, double y, double epsilon ) -{ - return gt( y, x, epsilon ); -} - -bool FloatUtils::lte( double x, double y, double epsilon ) -{ - return gte( y, x, epsilon ); -} - -double FloatUtils::min( double x, double y, double epsilon ) -{ - return lt( x, y, epsilon ) ? x : y; -} - -double FloatUtils::max( double x, double y, double epsilon ) -{ - return gt( x, y, epsilon ) ? x : y; -} - -double FloatUtils::infinity() -{ - return DBL_MAX; -} - -double FloatUtils::negativeInfinity() -{ - return -DBL_MAX; -} - String FloatUtils::doubleToString( double x, unsigned precision ) { std::ostringstream strout; @@ -128,11 +52,6 @@ String FloatUtils::doubleToString( double x, unsigned precision ) return str; } -bool FloatUtils::wellFormed( double x ) -{ - return !isNan( x ) && !isInf( x ); -} - bool FloatUtils::isNan( double x ) { return isnan( x ); diff --git a/src/common/FloatUtils.h b/src/common/FloatUtils.h index aa62572d0..ed1d9075a 100644 --- a/src/common/FloatUtils.h +++ b/src/common/FloatUtils.h @@ -16,10 +16,12 @@ #ifndef __FloatUtils_h__ #define __FloatUtils_h__ +#include "Debug.h" #include "GlobalConfiguration.h" #include "MString.h" #include +#include #ifdef _WIN32 #undef max @@ -30,28 +32,97 @@ class FloatUtils { public: static bool areEqual( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static double abs( double x ); - static bool areDisequal( double x, - double y, - double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static bool isZero( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static double roundToZero( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static bool isPositive( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static bool isNegative( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static bool gt( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static bool gte( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static bool lt( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static bool lte( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static double min( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static double max( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); - static double infinity(); - static double negativeInfinity(); - static bool isFinite( double x ); static String doubleToString( double x, unsigned precision = GlobalConfiguration::DEFAULT_DOUBLE_TO_STRING_PRECISION ); - static bool wellFormed( double x ); + static bool isNan( double x ); + static bool isInf( double x ); + + static bool isZero( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ) + { + return ( -epsilon <= x ) && ( x <= epsilon ); + } + + static bool isPositive( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ) + { + ASSERT( epsilon > 0 ); + return x > epsilon; + } + + static bool isNegative( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ) + { + ASSERT( epsilon > 0 ); + return x < -epsilon; + } + + static double abs( double x ) + { + return fabs( x ); + } + + static bool areDisequal( double x, + double y, + double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ) + { + return !areEqual( x, y, epsilon ); + } + + static double roundToZero( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ) + { + return isZero( x, epsilon ) ? 0.0 : x; + } + + static bool gt( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ) + { + return isPositive( x - y, epsilon ); + } + + static bool gte( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ) + { + return !isNegative( x - y, epsilon ); + } + + static bool lt( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ) + { + return gt( y, x, epsilon ); + } + + static bool lte( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ) + { + return gte( y, x, epsilon ); + } + + static double min( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ) + { + return lt( x, y, epsilon ) ? x : y; + } + + static double max( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ) + { + return gt( x, y, epsilon ) ? x : y; + } + + static double infinity() + { + return DBL_MAX; + } + + static double negativeInfinity() + { + return -DBL_MAX; + } + + static bool isFinite( double x ) + { + return ( x != infinity() ) && ( x != negativeInfinity() ); + } + + static bool wellFormed( double x ) + { + return !isNan( x ) && !isInf( x ); + } + }; #endif // __FloatUtils_h__ From 41ccc59a1bcadd99b8038317e25cdba34a017677 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> Date: Tue, 7 Apr 2020 13:29:07 -0700 Subject: [PATCH 3/4] use sat/unsat instead of SAT/UNSAT (#237) * use sat/unsat instead of SAT/UNSAT * missing cases --- README.md | 2 +- maraboupy/Marabou.py | 4 +- maraboupy/MarabouNetwork.py | 4 +- maraboupy/examples/Example Notebook.ipynb | 6 +- maraboupy/examples/MarabouCoreExample.py | 4 +- regress/regress0/CMakeLists.txt | 18 +- regress/regress1/CMakeLists.txt | 208 +++++++++++----------- regress/regress2/CMakeLists.txt | 18 +- regress/run_regression.py | 20 +-- src/engine/DnCManager.cpp | 8 +- src/engine/DnCWorker.cpp | 4 +- src/engine/Engine.cpp | 6 +- src/engine/Marabou.cpp | 8 +- src/input_parsers/mps_example/main.cpp | 4 +- 14 files changed, 157 insertions(+), 157 deletions(-) diff --git a/README.md b/README.md index 5e6219894..078e3d18c 100644 --- a/README.md +++ b/README.md @@ -209,7 +209,7 @@ We have three types of tests: * regression tests - test end to end functionality thorugh the API, each test is defined by: * network_file - description of the "neural network" supporting nnet and mps formats (using the extension to decdie on the format) * property_file - optional, constraint on the input and output variables - * expected_result - SAT/UNSAT + * expected_result - sat/unsat The tests are divided into 5 levels to allow variability in running time, to add a new regression tests: * add the description of the network and property to the _resources_ sub-folder diff --git a/maraboupy/Marabou.py b/maraboupy/Marabou.py index 09a07d6ea..9f5afa555 100644 --- a/maraboupy/Marabou.py +++ b/maraboupy/Marabou.py @@ -100,9 +100,9 @@ def solve_query(ipq, filename="", verbose=True, timeout=0, verbosity=2): if stats.hasTimedOut(): print ("TIMEOUT") elif len(vals)==0: - print("UNSAT") + print("unsat") else: - print("SAT") + print("sat") for i in range(ipq.getNumInputVariables()): print("input {} = {}".format(i, vals[ipq.inputVariableByIndex(i)])) for i in range(ipq.getNumOutputVariables()): diff --git a/maraboupy/MarabouNetwork.py b/maraboupy/MarabouNetwork.py index 451efe825..b0cd78583 100644 --- a/maraboupy/MarabouNetwork.py +++ b/maraboupy/MarabouNetwork.py @@ -201,9 +201,9 @@ def solve(self, filename="", verbose=True, options=None): if stats.hasTimedOut(): print("TO") elif len(vals)==0: - print("UNSAT") + print("unsat") else: - print("SAT") + print("sat") for j in range(len(self.inputVars)): for i in range(self.inputVars[j].size): print("input {} = {}".format(i, vals[self.inputVars[j].item(i)])) diff --git a/maraboupy/examples/Example Notebook.ipynb b/maraboupy/examples/Example Notebook.ipynb index f4a9e645c..13de4f9b2 100644 --- a/maraboupy/examples/Example Notebook.ipynb +++ b/maraboupy/examples/Example Notebook.ipynb @@ -94,7 +94,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "SAT\n", + "sat\n", "input 0 = -0.32842287715105956\n", "input 1 = 0.18470882292589386\n", "input 2 = -0.015568802288230335\n", @@ -177,7 +177,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "SAT\n", + "sat\n", "input 0 = -0.32842287715105956\n", "input 1 = 0.18470882292589386\n", "input 2 = -0.015568802288230335\n", @@ -245,7 +245,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "SAT\n", + "sat\n", "input 0 = -0.328422874212265\n", "input 1 = 0.40932923555374146\n", "input 2 = -0.017379289492964745\n", diff --git a/maraboupy/examples/MarabouCoreExample.py b/maraboupy/examples/MarabouCoreExample.py index 715236840..4af92fb26 100644 --- a/maraboupy/examples/MarabouCoreExample.py +++ b/maraboupy/examples/MarabouCoreExample.py @@ -88,7 +88,7 @@ options = createOptions() vars1, stats1 = MarabouCore.solve(inputQuery, options, "") if len(vars1) > 0: - print("SAT") + print("sat") print(vars1) else: - print("UNSAT") + print("unsat") diff --git a/regress/regress0/CMakeLists.txt b/regress/regress0/CMakeLists.txt index 5c7659a44..427f74d14 100644 --- a/regress/regress0/CMakeLists.txt +++ b/regress/regress0/CMakeLists.txt @@ -1,11 +1,11 @@ -marabou_add_regress_mps_test(0 "lp_feasible_1.mps" "SAT" "" "mps") -marabou_add_regress_mps_test(0 "lp_infeasible_1.mps" "UNSAT" "" "mps") +marabou_add_regress_mps_test(0 "lp_feasible_1.mps" "sat" "" "mps") +marabou_add_regress_mps_test(0 "lp_infeasible_1.mps" "unsat" "" "mps") -marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_1_7.nnet" "3" SAT) -marabou_add_acasxu_dnc_test(0 "ACASXU_experimental_v2a_1_9.nnet" "4" SAT) -marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_4_1.nnet" "4" UNSAT) +marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_1_7.nnet" "3" sat) +marabou_add_acasxu_dnc_test(0 "ACASXU_experimental_v2a_1_9.nnet" "4" sat) +marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_4_1.nnet" "4" unsat) -marabou_add_coav_test(0 "reluBenchmark0.067841053009s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(0 "reluBenchmark0.0518190860748s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(0 "reluBenchmark0.536728143692s_SAT.nnet" SAT) -marabou_add_coav_test(0 "reluBenchmark0.899523973465s_SAT.nnet" SAT) +marabou_add_coav_test(0 "reluBenchmark0.067841053009s_UNSAT.nnet" unsat) +marabou_add_coav_test(0 "reluBenchmark0.0518190860748s_UNSAT.nnet" unsat) +marabou_add_coav_test(0 "reluBenchmark0.536728143692s_SAT.nnet" sat) +marabou_add_coav_test(0 "reluBenchmark0.899523973465s_SAT.nnet" sat) diff --git a/regress/regress1/CMakeLists.txt b/regress/regress1/CMakeLists.txt index 9c57eaf64..f83b1310c 100644 --- a/regress/regress1/CMakeLists.txt +++ b/regress/regress1/CMakeLists.txt @@ -1,111 +1,111 @@ -marabou_add_coav_test(1 "reluBenchmark1.30941200256s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.94518494606s_SAT.nnet" SAT) -marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_8.nnet" "3" SAT) -marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_2_9.nnet" "3" UNSAT) -marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_6.nnet" "3" UNSAT) -marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_6.nnet" "4" UNSAT) -marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_7.nnet" "4" SAT) -marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_8.nnet" "4" SAT) -marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_9.nnet" "4" SAT) +marabou_add_coav_test(1 "reluBenchmark1.30941200256s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.94518494606s_SAT.nnet" sat) +marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_8.nnet" "3" sat) +marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_2_9.nnet" "3" unsat) +marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_6.nnet" "3" unsat) +marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_6.nnet" "4" unsat) +marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_7.nnet" "4" sat) +marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_8.nnet" "4" sat) +marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_9.nnet" "4" sat) -marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_5_7.nnet" "3" UNSAT) -marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_4_7.nnet" "4" UNSAT) +marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_5_7.nnet" "3" unsat) +marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_4_7.nnet" "4" unsat) -marabou_add_coav_test(1 "reluBenchmark0.453322172165s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.30711388588s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.00512099266052s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.725997209549s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.919886112213s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0352051258087s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.97177696228s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.36359000206s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0990879535675s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.20350694656s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.221790075302s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.048150062561s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.781363010406s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.0492730140686s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0494029521942s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.499482154846s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.674989938736s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark1.15705108643s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.0606548786163s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.21319699287s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.0064799785614s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0780329704285s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.454473018646s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.00568509101868s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.930528879166s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.0380239486694s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.764842987061s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.385080099106s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark1.07406687737s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0645151138306s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.04137301445s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.505765914917s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.07428097725s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.734488964081s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.326423883438s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.398984909058s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.379405975342s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.479170084s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0386769771576s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.4906899929s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark2.79231500626s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.345348119736s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.780378818512s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.32709693909s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.287177085876s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0374069213867s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0594508647919s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0918869972229s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.983299016953s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0842049121857s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.213617086411s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.666516065598s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.149944067s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.165054798126s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.00636315345764s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0596628189087s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0065929889679s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.30961179733s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0715999603271s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.29426407814s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.294414997101s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.124088048935s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0637600421906s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.00662088394165s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.276684999466s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.271136045456s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.101797103882s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.836799860001s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.907590150833s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.54942297935s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.692045211792s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.04315304756s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.213303089142s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.09928894043s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark1.21413683891s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.183997154236s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.514003992081s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.047042131424s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0507640838623s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.83825802803s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.262641906738s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.434634923935s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.950109958649s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.62436914444s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.73387503624s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.0452961921692s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.828888177872s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.996887922287s_SAT.nnet" SAT) -marabou_add_coav_test(1 "reluBenchmark0.0575940608978s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.213079929352s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark1.81178617477s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.956095933914s_UNSAT.nnet" UNSAT) -marabou_add_coav_test(1 "reluBenchmark0.00601387023926s_UNSAT.nnet" UNSAT) +marabou_add_coav_test(1 "reluBenchmark0.453322172165s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.30711388588s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.00512099266052s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.725997209549s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.919886112213s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0352051258087s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.97177696228s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.36359000206s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0990879535675s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.20350694656s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.221790075302s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.048150062561s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.781363010406s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.0492730140686s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0494029521942s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.499482154846s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.674989938736s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark1.15705108643s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.0606548786163s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.21319699287s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.0064799785614s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0780329704285s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.454473018646s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.00568509101868s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.930528879166s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.0380239486694s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.764842987061s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.385080099106s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark1.07406687737s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0645151138306s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.04137301445s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.505765914917s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.07428097725s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.734488964081s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.326423883438s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.398984909058s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.379405975342s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.479170084s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0386769771576s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.4906899929s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark2.79231500626s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.345348119736s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.780378818512s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.32709693909s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.287177085876s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0374069213867s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0594508647919s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0918869972229s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.983299016953s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0842049121857s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.213617086411s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.666516065598s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.149944067s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.165054798126s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.00636315345764s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0596628189087s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0065929889679s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.30961179733s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0715999603271s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.29426407814s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.294414997101s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.124088048935s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0637600421906s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.00662088394165s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.276684999466s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.271136045456s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.101797103882s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.836799860001s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.907590150833s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.54942297935s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.692045211792s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.04315304756s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.213303089142s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.09928894043s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark1.21413683891s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.183997154236s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.514003992081s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.047042131424s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0507640838623s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.83825802803s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.262641906738s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.434634923935s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.950109958649s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.62436914444s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.73387503624s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.0452961921692s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.828888177872s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.996887922287s_SAT.nnet" sat) +marabou_add_coav_test(1 "reluBenchmark0.0575940608978s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.213079929352s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark1.81178617477s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.956095933914s_UNSAT.nnet" unsat) +marabou_add_coav_test(1 "reluBenchmark0.00601387023926s_UNSAT.nnet" unsat) diff --git a/regress/regress2/CMakeLists.txt b/regress/regress2/CMakeLists.txt index 306ae5a29..9402ad74b 100644 --- a/regress/regress2/CMakeLists.txt +++ b/regress/regress2/CMakeLists.txt @@ -1,11 +1,11 @@ -marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_7.nnet" "4" UNSAT) -marabou_add_coav_test(2 "reluBenchmark2.66962385178s_UNSAT.nnet" UNSAT) #25 sec -marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_9.nnet" "3" UNSAT) # +marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_7.nnet" "4" unsat) +marabou_add_coav_test(2 "reluBenchmark2.66962385178s_UNSAT.nnet" unsat) #25 sec +marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_9.nnet" "3" unsat) # - marabou_add_coav_test(2 "reluBenchmark2.64361000061s_SAT.nnet" SAT) # 25sec -# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_5_1.nnet" "2" SAT) # 480sec -# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_2_4.nnet" "2" SAT) # 300sec -# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_7.nnet" "4" UNSAT) # 150sec -# marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_5.nnet" "2" SAT) # timeout -# marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_9.nnet" "3" UNSAT) # 200sec + marabou_add_coav_test(2 "reluBenchmark2.64361000061s_SAT.nnet" sat) # 25sec +# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_5_1.nnet" "2" sat) # 480sec +# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_2_4.nnet" "2" sat) # 300sec +# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_7.nnet" "4" unsat) # 150sec +# marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_5.nnet" "2" sat) # timeout +# marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_9.nnet" "3" unsat) # 200sec diff --git a/regress/run_regression.py b/regress/run_regression.py index 08223c62c..5346dd541 100755 --- a/regress/run_regression.py +++ b/regress/run_regression.py @@ -5,7 +5,7 @@ import threading DEFAULT_TIMEOUT = 600 -EXPECTED_RESULT_OPTIONS = ('SAT', 'UNSAT') +EXPECTED_RESULT_OPTIONS = ('sat', 'unsat') def run_process(args, cwd, timeout, s_input=None): @@ -50,19 +50,19 @@ def analyze_process_result(out, err, exit_status, expected_result): print("err: {}".format(err)) return False - # If the output is UNSAT there is no \n after the UNSAT statement - if expected_result == 'UNSAT': + # If the output is unsat there is no \n after the unsat statement + if expected_result == 'unsat': out_lines = out.splitlines() if out_lines[-1] == expected_result: return True else: - print("Expected UNSAT, but last line is in output is: ", out_lines[-1]) + print("Expected unsat, but last line is in output is: ", out_lines[-1]) return False else: - if '\nSAT' in out: + if '\nsat' in out: return True else: - print('expected SAT, but \'\\nSAT\' is not in the output. tail of the output:\n', out[-1500:]) + print('expected sat, but \'\\nSAT\' is not in the output. tail of the output:\n', out[-1500:]) return False @@ -72,7 +72,7 @@ def run_marabou(marabou_binary, network_path, property_path, expected_result, ti :param marabou_binary: path to marabou executable :param network_path: path to nnet file to pass too marabou :param property_path: path to property file to pass to marabou to verify - :param expected_result: SAT / UNSAT + :param expected_result: sat / unsat :param arguments list of arguments to pass to Marabou (for example DnC mode) :return: True / False if test pass or not ''' @@ -83,7 +83,7 @@ def run_marabou(marabou_binary, network_path, property_path, expected_result, ti sys.exit('"{}" does not exist or is not a file'.format(network_path)) if not os.path.isfile(property_path): sys.exit('"{}" does not exist or is not a file'.format(property_path)) - if expected_result not in {'SAT', 'UNSAT'}: + if expected_result not in {'sat', 'unsat'}: sys.exit('"{}" is not a marabou supported result'.format(expected_result)) args = [marabou_binary, network_path, property_path] @@ -100,7 +100,7 @@ def run_mpsparser(mps_binary, network_path, expected_result, arguments=None): :param marabou_binary: path to marabou executable :param network_path: path to nnet file to pass too marabou :param property_path: path to property file to pass to marabou to verify - :param expected_result: SAT / UNSAT + :param expected_result: sat / unsat :param arguments list of arguments to pass to Marabou (for example DnC mode) :return: True / False if test pass or not ''' @@ -109,7 +109,7 @@ def run_mpsparser(mps_binary, network_path, expected_result, arguments=None): '"{}" does not exist or is not executable'.format(mps_binary)) if not os.path.isfile(network_path): sys.exit('"{}" does not exist or is not a file'.format(network_path)) - if expected_result not in {'SAT', 'UNSAT'}: + if expected_result not in {'sat', 'unsat'}: sys.exit('"{}" is not a marabou supported result'.format(expected_result)) args = [mps_binary, network_path] diff --git a/src/engine/DnCManager.cpp b/src/engine/DnCManager.cpp index a6ad65c8a..b8dcfd814 100644 --- a/src/engine/DnCManager.cpp +++ b/src/engine/DnCManager.cpp @@ -215,9 +215,9 @@ String DnCManager::getResultString() switch ( _exitCode ) { case DnCManager::SAT: - return "SAT"; + return "sat"; case DnCManager::UNSAT: - return "UNSAT"; + return "unsat"; case DnCManager::ERROR: return "ERROR"; case DnCManager::NOT_DONE: @@ -252,7 +252,7 @@ void DnCManager::printResult() { case DnCManager::SAT: { - std::cout << "SAT\n" << std::endl; + std::cout << "sat\n" << std::endl; ASSERT( _engineWithSATAssignment != nullptr ); @@ -288,7 +288,7 @@ void DnCManager::printResult() break; } case DnCManager::UNSAT: - std::cout << "UNSAT" << std::endl; + std::cout << "unsat" << std::endl; break; case DnCManager::ERROR: std::cout << "ERROR" << std::endl; diff --git a/src/engine/DnCWorker.cpp b/src/engine/DnCWorker.cpp index 58f456c7b..17bea6ec0 100644 --- a/src/engine/DnCWorker.cpp +++ b/src/engine/DnCWorker.cpp @@ -170,9 +170,9 @@ String DnCWorker::exitCodeToString( IEngine::ExitCode result ) switch ( result ) { case IEngine::UNSAT: - return "UNSAT"; + return "unsat"; case IEngine::SAT: - return "SAT"; + return "sat"; case IEngine::ERROR: return "ERROR"; case IEngine::TIMEOUT: diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index fc48b43e8..606643c91 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -217,7 +217,7 @@ bool Engine::solve( unsigned timeoutInSeconds ) { if ( _verbosity > 0 ) { - printf( "Before declaring SAT, recomputing...\n" ); + printf( "Before declaring sat, recomputing...\n" ); } // Make sure that the assignment is precise before declaring success _tableau->computeAssignment(); @@ -225,7 +225,7 @@ bool Engine::solve( unsigned timeoutInSeconds ) } if ( _verbosity > 0 ) { - printf( "\nEngine::solve: SAT assignment found\n" ); + printf( "\nEngine::solve: sat assignment found\n" ); _statistics.print(); } _exitCode = Engine::SAT; @@ -287,7 +287,7 @@ bool Engine::solve( unsigned timeoutInSeconds ) { if ( _verbosity > 0 ) { - printf( "\nEngine::solve: UNSAT query\n" ); + printf( "\nEngine::solve: unsat query\n" ); _statistics.print(); } _exitCode = Engine::UNSAT; diff --git a/src/engine/Marabou.cpp b/src/engine/Marabou.cpp index 2ddd52ab3..3419656a2 100644 --- a/src/engine/Marabou.cpp +++ b/src/engine/Marabou.cpp @@ -135,13 +135,13 @@ void Marabou::displayResults( unsigned long long microSecondsElapsed ) const if ( result == Engine::UNSAT ) { - resultString = "UNSAT"; - printf( "UNSAT\n" ); + resultString = "unsat"; + printf( "unsat\n" ); } else if ( result == Engine::SAT ) { - resultString = "SAT"; - printf( "SAT\n" ); + resultString = "sat"; + printf( "sat\n" ); printf( "Input assignment:\n" ); for ( unsigned i = 0; i < _inputQuery.getNumInputVariables(); ++i ) diff --git a/src/input_parsers/mps_example/main.cpp b/src/input_parsers/mps_example/main.cpp index 4dff63b15..bf856773f 100644 --- a/src/input_parsers/mps_example/main.cpp +++ b/src/input_parsers/mps_example/main.cpp @@ -41,11 +41,11 @@ int main( int argc, char *argv[] ) if ( !preprocess || !engine.solve() ) { - printf( "UNSAT\n" ); + printf( "unsat\n" ); return 0; } - printf( "SAT\n" ); + printf( "sat\n" ); // Uncomment the below to print the solution From 98a0fdedf24493f52eb448e48fe76124825fa41b Mon Sep 17 00:00:00 2001 From: kjulian3 Date: Sun, 12 Apr 2020 23:22:10 -0700 Subject: [PATCH 4/4] fix typo (#241) Co-authored-by: Guy Katz Co-authored-by: Kyle Julian --- maraboupy/MarabouNetworkONNX.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/maraboupy/MarabouNetworkONNX.py b/maraboupy/MarabouNetworkONNX.py index 1c2eecf1e..4b6e2b983 100644 --- a/maraboupy/MarabouNetworkONNX.py +++ b/maraboupy/MarabouNetworkONNX.py @@ -342,7 +342,7 @@ def transpose(self, node): if inputName in self.varMap: self.varMap[nodeName] = np.transpose(self.varMap[node.input[0]], perm) elif inputName in self.constantMap: - self.constantMap[nodeName] = np.transpose(self.constant[inputName], perm) + self.constantMap[nodeName] = np.transpose(self.constantMap[inputName], perm) def maxpoolEquations(self, node, makeEquations): """ @@ -812,4 +812,4 @@ def evaluateWithoutMarabou(self, inputValues): printf("Not sure how to cast input to graph input of type %s" % onnxType) raise NotImplementedError input_dict[inputName] = inputValues[i].reshape(self.inputVars[i].shape).astype(inputType) - return sess.run([self.outputName],input_dict)[0] \ No newline at end of file + return sess.run([self.outputName],input_dict)[0]