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] 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