From 18b07e568d67964b15a575a3512b197b647ddc18 Mon Sep 17 00:00:00 2001 From: Chronosymbolic Date: Mon, 11 Sep 2023 14:00:54 -0400 Subject: [PATCH] upd readme, log and purge some redundant code --- README.md | 14 +- experiment/README.md | 6 +- ...lt_summary.log => result_safe_summary.log} | 0 experiment/result_unsafe_summary.log | 803 ++++++++++++++++++ learner/learner.py | 168 ---- 5 files changed, 812 insertions(+), 179 deletions(-) rename experiment/{result_summary.log => result_safe_summary.log} (100%) create mode 100644 experiment/result_unsafe_summary.log diff --git a/README.md b/README.md index f74f109..94490ba 100644 --- a/README.md +++ b/README.md @@ -6,22 +6,18 @@ Artifact for the paper "Chronosymbolic Learning: Efficient CHC Solving with Symb - See `./examples` for examples of how our tool works ## Requirement (To set up our environment) -Python (3.7.0 or higher, and anaconda recommended) +Python (3.7.0 or higher, and [Anaconda](https://www.anaconda.com/) recommended) -Install packages in `requirements.txt`: +- Install packages in `requirements.txt`: `pip install -r requirements.txt` -``` -pip install -r requirements.txt -``` +- May have to manually set up `PYTHONPATH` and `PATH` properly, `PYTHONPATH=$Z3_BIN/python`, `PATH=$PATH:$Z3_BIN` -May have to manually set up `PYTHONPATH` and `PATH` properly, `PYTHONPATH=$Z3_BIN/python`, `PATH=$PATH:$Z3_BIN` - -Then, prepare the dataset following the instructions in `data/` folder. +- If the C5.0/LIBSVM binary cannot executed properly, may have to recompile them in your OS and specify the binary executable files in `utils/dt/dt.py` in `class C5DT`, `C5_exec_path` and `utils/svm/svm.py` in `class LibSVMLearner`, `svm_exec_path` ## Chronosymbolic Learning - Support SMT-LIB2 format (check-sat) and Datalog format (rule-query) -- Have executable binaries of decision tree and SVM for Linux and MacOS, and can automatically adapt to the OS +- Have executable binaries of decision tree and SVM for Linux and MacOS, and can automatically adapt to the OS (Linux/Mac) - Control flow implemented in `learner/run_agent.py` `run_Agent` function diff --git a/experiment/README.md b/experiment/README.md index c6a4635..90653be 100644 --- a/experiment/README.md +++ b/experiment/README.md @@ -1,5 +1,7 @@ -## result_summary_safe.log -The log shows the running log of our reported experiment on ``Chronosymbolic-single''. This experiment runs a suite of instances using a fixed set of hyperparameters. The structure of the log is as follows: +## result_safe_summary.log and result_unsafe_summary.log +The logs are the running logs of our reported experiment on ``Chronosymbolic-single''. This experiment runs a suite of instances using a fixed set of hyperparameters. + +The structure of the log is as follows: 1. The first 2 lines are the modules used. diff --git a/experiment/result_summary.log b/experiment/result_safe_summary.log similarity index 100% rename from experiment/result_summary.log rename to experiment/result_safe_summary.log diff --git a/experiment/result_unsafe_summary.log b/experiment/result_unsafe_summary.log new file mode 100644 index 0000000..b6ea6a3 --- /dev/null +++ b/experiment/result_unsafe_summary.log @@ -0,0 +1,803 @@ +Chronosymbolic + +C5DT + +--------- Hyperparameters --------- +ClearBodyAppsDP: false +DIV: [] +DIVFind: false +Dataset: + QueueLenNeg: 50 + QueueLenPos: 50 + QueueModeNeg: true + QueueModePos: true + QueueRealNegProp: 0.5 + QueueTentNegProp: 0.5 +EnableMatchFact: true +Expansion: + BodyCstrExpUB: 700 + ForceExp: false + FreeVarUB: 500 + InitExpMaxIter: 10 + InitExpMinIter: 5 + NewZoneExpUB: 1500 + UseExpansion: true +FILE_NAME: tmp/FromCmd +FactSampleMaxRound: 10 +InitPhase: true +LC: 0 +LOGGING: true +MOD: [] +MODFind: true +OCT: true +OverflowLimit: 214748364900 +QuerySampleMaxRound: 2 +RelationUpperBound: 500 +RuleSampleLen: 2 +RuleSampleLenNeg: 1 +RuleSampleWidth: 1 +RuleSampleWidthNeg: 1 +SVM: + EnableSVM: true + SVMAHyperplane: 0 + SVMCParameter: 1 + SVMCoeffBound: 5 + SVMFreqNeg: 30 + SVMFreqPos: 0 +SampleBatchSize: 0 +Stretegy: + SafeZoneUsage: (self.total_iter // 100) % 2 == 0 + UnsafeZoneUsage: (self.total_iter // 50) % 2 == 0 +UseSafeZone: true +UseUnsafeZone: true +ValIterMode: false +Verbosity: + PrintCex: 5 + PrintCstr: false + PrintNewCandFreq: 50 +Z3_Global_Timeout: 10000 +Z3_Solver_Timeout: 360000 + +--------- CHC Solving --------- + +======== File No.1/53 (0 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/count_by_1_true-unreach-call_true-termination_cex.c.smt2 ======== +********* SMT2 Loading time: 0.002241849899291992 secs, Size: 0.52KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/count_by_1_true-unreach-call_true-termination_cex.c.smt2.log +Solving instance timeout! +************** Finished in 360.0233209133148 (secs) in 3 epochs ************** +Total SVM Calls: 350, DT Calls: 9480, Z3 Calls: 10781 +Total SVM Time: 79.91859245300293, DT Time: 35.54766297340393, Z3 Time: 74.47741556167603 +Others: 170.07964992523193, Init Phase Time: 0.033089637756347656, Simplifier Solver Time: 1.0988035202026367 +************** Auxiliary Info ************** +max_len_exp_fwd: 886 +max_len_exp_bwd: 821 +len_exp_zone_fwd: [(36, 53), (112, 184), (241, 438), (495, 827), (886, 1360)] +len_exp_zone_bwd: [(66, 113), (220, 342), (460, 686), (821, 1159)] +Total Iter: 9487 +QE Time: 0.0015141963958740234 +************** Program Verification Failed ************** + + + +======== File No.2/53 (0 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/menlo_park_cex_simpl_1.smt2 ======== +********* SMT2 Loading time: 0.0033566951751708984 secs, Size: 0.55KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/menlo_park_cex_simpl_1.smt2.log +************** Finished in 0.03143167495727539 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.0045969486236572266 +Others: 0.026834726333618164, Init Phase Time: 0.031222820281982422, Simplifier Solver Time: 0.0006961822509765625 +************** Program is BUGGY ************** + + + +======== File No.3/53 (1 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_multiple_inv_01_cex.smt2 ======== +********* SMT2 Loading time: 0.0026407241821289062 secs, Size: 0.38KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_multiple_inv_01_cex.smt2.log +************** Finished in 0.20434188842773438 (secs) in 1 epochs ************** +Total SVM Calls: 1, DT Calls: 2, Z3 Calls: 24 +Total SVM Time: 0.0026464462280273438, DT Time: 0.005766391754150391, Z3 Time: 0.12301039695739746 +Others: 0.07291865348815918, Init Phase Time: 0.04389452934265137, Simplifier Solver Time: 0.002044200897216797 +************** Auxiliary Info ************** +max_len_exp_fwd: 58 +max_len_exp_bwd: 148 +len_exp_zone_fwd: [(17, 28), (17, 34), (11, 28), (17, 46), (34, 51), (28, 52), (34, 75), (46, 75), (40, 76), (46, 115), (58, 111), (52, 128), (58, 143)] +len_exp_zone_bwd: [(23, 34), (13, 32), (42, 61), (42, 80), (32, 60), (56, 97), (56, 85), (46, 108), (70, 129), (70, 99), (60, 144), (89, 222), (89, 173), (74, 180), (148, 267)] +Total Iter: 4 +QE Time: 0.0006866455078125 +************** Program is BUGGY ************** + + + +======== File No.4/53 (2 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_multiple_inv_02_cex.smt2 ======== +********* SMT2 Loading time: 0.002941608428955078 secs, Size: 0.43KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_multiple_inv_02_cex.smt2.log +************** Finished in 0.02975916862487793 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.002904653549194336 +Others: 0.026854515075683594, Init Phase Time: 0.02953648567199707, Simplifier Solver Time: 0.001779794692993164 +************** Program is BUGGY ************** + + + +======== File No.5/53 (3 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_multiple_inv_03_cex.smt2 ======== +********* SMT2 Loading time: 0.0035631656646728516 secs, Size: 0.48KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_multiple_inv_03_cex.smt2.log +************** Finished in 0.03842496871948242 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.005623579025268555 +Others: 0.03280138969421387, Init Phase Time: 0.03817868232727051, Simplifier Solver Time: 0.0025703907012939453 +************** Program is BUGGY ************** + + + +======== File No.6/53 (4 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_multiple_inv_04_cex.smt2 ======== +********* SMT2 Loading time: 0.0038661956787109375 secs, Size: 0.56KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_multiple_inv_04_cex.smt2.log +************** Finished in 0.31877732276916504 (secs) in 1 epochs ************** +Total SVM Calls: 1, DT Calls: 1, Z3 Calls: 37 +Total SVM Time: 0.0026636123657226562, DT Time: 0.0030517578125, Z3 Time: 0.19514250755310059 +Others: 0.1179194450378418, Init Phase Time: 0.0781242847442627, Simplifier Solver Time: 0.003225088119506836 +************** Auxiliary Info ************** +max_len_exp_fwd: 208 +max_len_exp_bwd: 677 +len_exp_zone_fwd: [(19, 30), (13, 32), (19, 30), (13, 32), (38, 71), (32, 60), (13, 32), (52, 93), (46, 108), (52, 147), (46, 108), (60, 144), (139, 272), (108, 216), (66, 215), (60, 144), (162, 324), (208, 461), (162, 324), (80, 335), (74, 180)] +len_exp_zone_bwd: [(19, 44), (54, 85), (44, 96), (126, 201), (96, 192), (44, 96), (74, 219), (120, 240), (242, 537), (216, 432), (64, 144), (126, 403), (216, 432), (387, 867), (336, 672), (96, 192), (155, 573), (336, 672), (532, 1197), (456, 912), (120, 240), (184, 743), (456, 912), (677, 1527), (528, 1056)] +Total Iter: 5 +QE Time: 0.002320528030395508 +************** Program is BUGGY ************** + + + +======== File No.7/53 (5 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_multiple_inv_05_cex.smt2 ======== +********* SMT2 Loading time: 0.003151416778564453 secs, Size: 0.44KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_multiple_inv_05_cex.smt2.log +************** Finished in 0.031007051467895508 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.0029478073120117188 +Others: 0.02805924415588379, Init Phase Time: 0.030750274658203125, Simplifier Solver Time: 0.001725912094116211 +************** Program is BUGGY ************** + + + +======== File No.8/53 (6 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_only_01_cex.smt2 ======== +********* SMT2 Loading time: 0.002357006072998047 secs, Size: 0.40KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_only_01_cex.smt2.log +************** Finished in 0.011860370635986328 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.002819538116455078 +Others: 0.00904083251953125, Init Phase Time: 0.011638879776000977, Simplifier Solver Time: 0.0002646446228027344 +************** Program is BUGGY ************** + + + +======== File No.9/53 (7 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_only_02_cex.smt2 ======== +********* SMT2 Loading time: 0.003311634063720703 secs, Size: 0.73KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_only_02_cex.smt2.log +************** Finished in 0.017706871032714844 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.0032618045806884766 +Others: 0.014445066452026367, Init Phase Time: 0.01735520362854004, Simplifier Solver Time: 0.0004417896270751953 +************** Program is BUGGY ************** + + + +======== File No.10/53 (8 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_only_03_cex.smt2 ======== +********* SMT2 Loading time: 0.0029020309448242188 secs, Size: 0.56KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_only_03_cex.smt2.log +************** Finished in 15.96593976020813 (secs) in 2 epochs ************** +Total SVM Calls: 84, DT Calls: 423, Z3 Calls: 737 +Total SVM Time: 2.7591629028320312, DT Time: 1.499995470046997, Z3 Time: 4.48321008682251 +Others: 7.223571300506592, Init Phase Time: 0.028674840927124023, Simplifier Solver Time: 0.049072980880737305 +************** Auxiliary Info ************** +max_len_exp_fwd: 304 +max_len_exp_bwd: 240 +len_exp_zone_fwd: [(33, 68), (72, 148), (152, 300), (228, 452), (304, 604)] +len_exp_zone_bwd: [(43, 98), (96, 194), (144, 290), (192, 386), (240, 482)] +Total Iter: 429 +QE Time: 0.0009541511535644531 +************** Program is BUGGY ************** + + + +======== File No.11/53 (9 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_only_04_cex.smt2 ======== +********* SMT2 Loading time: 0.0031435489654541016 secs, Size: 0.55KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_only_04_cex.smt2.log +************** Finished in 0.014500141143798828 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.003161907196044922 +Others: 0.011338233947753906, Init Phase Time: 0.01427602767944336, Simplifier Solver Time: 0.00029921531677246094 +************** Program is BUGGY ************** + + + +======== File No.12/53 (10 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_only_05_cex.smt2 ======== +********* SMT2 Loading time: 0.0027947425842285156 secs, Size: 0.43KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_only_05_cex.smt2.log +Solving instance timeout! +************** Finished in 360.010614156723 (secs) in 1 epochs ************** +Total SVM Calls: 7230, DT Calls: 7893, Z3 Calls: 8336 +Total SVM Time: 132.64167261123657, DT Time: 26.607959508895874, Z3 Time: 56.96370601654053 +Others: 143.79727602005005, Init Phase Time: 0.02815985679626465, Simplifier Solver Time: 0.9644773006439209 +************** Auxiliary Info ************** +max_len_exp_fwd: 296 +max_len_exp_bwd: 202 +len_exp_zone_fwd: [(30, 70), (70, 148), (148, 296), (222, 444), (296, 592)] +len_exp_zone_bwd: [(37, 80), (78, 166), (122, 246), (162, 326), (202, 406)] +Total Iter: 7895 +************** Program Verification Failed ************** + + + +======== File No.13/53 (10 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_only_06_cex.smt2 ======== +********* SMT2 Loading time: 0.0029952526092529297 secs, Size: 0.48KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_only_06_cex.smt2.log +************** Finished in 0.03272056579589844 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.0037076473236083984 +Others: 0.02901291847229004, Init Phase Time: 0.032480716705322266, Simplifier Solver Time: 0.0008535385131835938 +************** Program is BUGGY ************** + + + +======== File No.14/53 (11 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_only_07_cex.smt2 ======== +********* SMT2 Loading time: 0.0023500919342041016 secs, Size: 0.38KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_only_07_cex.smt2.log +************** Finished in 0.08446025848388672 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 8 +Total SVM Time: 7.772445678710938e-05, DT Time: 0, Z3 Time: 0.04104304313659668 +Others: 0.04333949089050293, Init Phase Time: 0.023679018020629883, Simplifier Solver Time: 0.0006890296936035156 +************** Auxiliary Info ************** +max_len_exp_fwd: 102 +max_len_exp_bwd: 668 +len_exp_zone_fwd: [(11, 28), (102, 180)] +len_exp_zone_bwd: [(37, 55), (149, 212), (310, 465), (483, 712), (668, 949)] +Total Iter: 2 +QE Time: 0.0006926059722900391 +************** Program is BUGGY ************** + + + +======== File No.15/53 (12 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_only_08_cex.smt2 ======== +********* SMT2 Loading time: 0.0026340484619140625 secs, Size: 0.46KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_only_08_cex.smt2.log +************** Finished in 0.017995834350585938 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.0030913352966308594 +Others: 0.014904499053955078, Init Phase Time: 0.017787456512451172, Simplifier Solver Time: 0.00039124488830566406 +************** Program is BUGGY ************** + + + +======== File No.16/53 (13 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_01_cex.smt2 ======== +********* SMT2 Loading time: 0.0024209022521972656 secs, Size: 0.38KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_01_cex.smt2.log +************** Finished in 128.38813996315002 (secs) in 1 epochs ************** +Total SVM Calls: 46, DT Calls: 199, Z3 Calls: 335 +Total SVM Time: 121.89711117744446, DT Time: 0.8137259483337402, Z3 Time: 2.1470017433166504 +Others: 3.530301094055176, Init Phase Time: 0.02877020835876465, Simplifier Solver Time: 0.025638103485107422 +************** Auxiliary Info ************** +max_len_exp_fwd: 373 +max_len_exp_bwd: 179 +len_exp_zone_fwd: [(42, 79), (150, 243), (224, 343), (298, 433), (373, 524)] +len_exp_zone_bwd: [(26, 48), (64, 120), (105, 194), (142, 268), (179, 342)] +Total Iter: 201 +QE Time: 0.001081228256225586 +************** Program is BUGGY ************** + + + +======== File No.17/53 (14 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_02_cex.smt2 ======== +********* SMT2 Loading time: 0.0033042430877685547 secs, Size: 0.58KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_02_cex.smt2.log +Solving instance timeout! +************** Finished in 360.0027074813843 (secs) in 4 epochs ************** +Total SVM Calls: 236, DT Calls: 1311, Z3 Calls: 2031 +Total SVM Time: 315.43128418922424, DT Time: 5.7890143394470215, Z3 Time: 13.481751680374146 +Others: 25.300657272338867, Init Phase Time: 0.03386425971984863, Simplifier Solver Time: 0.19289302825927734 +************** Auxiliary Info ************** +max_len_exp_fwd: 1226 +max_len_exp_bwd: 287 +len_exp_zone_fwd: [(65, 128), (396, 534), (800, 970), (1226, 1428)] +len_exp_zone_bwd: [(37, 59), (102, 165), (163, 264), (225, 354), (287, 444)] +Total Iter: 1318 +QE Time: 0.0012142658233642578 +************** Program Verification Failed ************** + + + +======== File No.18/53 (14 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_03_cex.smt2 ======== +********* SMT2 Loading time: 0.003001689910888672 secs, Size: 0.53KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_03_cex.smt2.log +************** Finished in 0.01381540298461914 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.0030260086059570312 +Others: 0.01078939437866211, Init Phase Time: 0.013585329055786133, Simplifier Solver Time: 0.0002980232238769531 +************** Program is BUGGY ************** + + + +======== File No.19/53 (15 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_04_cex.smt2 ======== +********* SMT2 Loading time: 0.002624034881591797 secs, Size: 0.41KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_04_cex.smt2.log +************** Finished in 6.906497955322266 (secs) in 1 epochs ************** +Total SVM Calls: 44, DT Calls: 210, Z3 Calls: 390 +Total SVM Time: 0.13519501686096191, DT Time: 0.7177348136901855, Z3 Time: 2.4025261402130127 +Others: 3.6510419845581055, Init Phase Time: 0.028867006301879883, Simplifier Solver Time: 0.02651810646057129 +************** Auxiliary Info ************** +max_len_exp_fwd: 312 +max_len_exp_bwd: 241 +len_exp_zone_fwd: [(34, 75), (74, 157), (156, 313), (234, 469), (312, 625)] +len_exp_zone_bwd: [(40, 86), (94, 180), (143, 278), (192, 376), (241, 474)] +Total Iter: 212 +QE Time: 0.0010342597961425781 +************** Program is BUGGY ************** + + + +======== File No.20/53 (16 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_05_cex.smt2 ======== +********* SMT2 Loading time: 0.003168344497680664 secs, Size: 0.41KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_05_cex.smt2.log +Solving instance timeout! +************** Finished in 360.0089545249939 (secs) in 24 epochs ************** +Total SVM Calls: 374, DT Calls: 5428, Z3 Calls: 6486 +Total SVM Time: 199.0523521900177, DT Time: 21.226152658462524, Z3 Time: 42.341872453689575 +Others: 97.3885772228241, Init Phase Time: 0.0292971134185791, Simplifier Solver Time: 0.6618120670318604 +************** Auxiliary Info ************** +max_len_exp_fwd: 451 +max_len_exp_bwd: 206 +len_exp_zone_fwd: [(36, 86), (108, 204), (226, 369), (338, 534), (451, 700)] +len_exp_zone_bwd: [(37, 80), (79, 167), (124, 249), (165, 331), (206, 413)] +Total Iter: 5453 +QE Time: 0.001005411148071289 +************** Program Verification Failed ************** + + + +======== File No.21/53 (16 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_06_cex.smt2 ======== +********* SMT2 Loading time: 0.0031690597534179688 secs, Size: 0.46KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_06_cex.smt2.log +************** Finished in 0.02596592903137207 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.003301858901977539 +Others: 0.02266407012939453, Init Phase Time: 0.025747060775756836, Simplifier Solver Time: 0.0007967948913574219 +************** Program is BUGGY ************** + + + +======== File No.22/53 (17 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_07_cex.smt2 ======== +********* SMT2 Loading time: 0.003142118453979492 secs, Size: 0.64KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_07_cex.smt2.log +************** Finished in 0.014222860336303711 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.003027200698852539 +Others: 0.011195659637451172, Init Phase Time: 0.014001607894897461, Simplifier Solver Time: 0.00031757354736328125 +************** Program is BUGGY ************** + + + +======== File No.23/53 (18 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_08_cex.smt2 ======== +********* SMT2 Loading time: 0.0025196075439453125 secs, Size: 0.40KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_08_cex.smt2.log +************** Finished in 7.708892822265625 (secs) in 1 epochs ************** +Total SVM Calls: 44, DT Calls: 243, Z3 Calls: 422 +Total SVM Time: 0.1193380355834961, DT Time: 0.8632330894470215, Z3 Time: 2.575920343399048 +Others: 4.15040135383606, Init Phase Time: 0.024896860122680664, Simplifier Solver Time: 0.0282135009765625 +************** Auxiliary Info ************** +max_len_exp_fwd: 207 +max_len_exp_bwd: 208 +len_exp_zone_fwd: [(48, 103), (207, 400)] +len_exp_zone_bwd: [(31, 68), (72, 148), (120, 232), (164, 320), (208, 408)] +Total Iter: 245 +QE Time: 0.0007817745208740234 +************** Program is BUGGY ************** + + + +======== File No.24/53 (19 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_09_cex.smt2 ======== +********* SMT2 Loading time: 0.002626180648803711 secs, Size: 0.39KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_09_cex.smt2.log +************** Finished in 0.01169443130493164 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.0030128955841064453 +Others: 0.008681535720825195, Init Phase Time: 0.011471748352050781, Simplifier Solver Time: 0.0002090930938720703 +************** Program is BUGGY ************** + + + +======== File No.25/53 (20 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_10_cex.smt2 ======== +********* SMT2 Loading time: 0.0024547576904296875 secs, Size: 0.42KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_10_cex.smt2.log +************** Finished in 0.011991739273071289 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.0027778148651123047 +Others: 0.009213924407958984, Init Phase Time: 0.011770486831665039, Simplifier Solver Time: 0.00026154518127441406 +************** Program is BUGGY ************** + + + +======== File No.26/53 (21 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_11_cex.smt2 ======== +********* SMT2 Loading time: 0.0032079219818115234 secs, Size: 0.55KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_11_cex.smt2.log +Solving instance timeout! +************** Finished in 360.0011661052704 (secs) in 69 epochs ************** +Total SVM Calls: 701, DT Calls: 5550, Z3 Calls: 7203 +Total SVM Time: 192.21223640441895, DT Time: 22.488650798797607, Z3 Time: 46.01645612716675 +Others: 99.28382277488708, Init Phase Time: 0.025946617126464844, Simplifier Solver Time: 0.6506857872009277 +************** Auxiliary Info ************** +max_len_exp_fwd: 220 +max_len_exp_bwd: 200 +len_exp_zone_fwd: [(41, 92), (220, 385)] +len_exp_zone_bwd: [(35, 117), (76, 207), (120, 291), (160, 375), (200, 459)] +Total Iter: 5663 +QE Time: 0.0007832050323486328 +************** Program Verification Failed ************** + + + +======== File No.27/53 (21 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_12_cex.smt2 ======== +********* SMT2 Loading time: 0.004124641418457031 secs, Size: 0.72KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_12_cex.smt2.log +************** Finished in 0.02655482292175293 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.005781412124633789 +Others: 0.02077341079711914, Init Phase Time: 0.02629995346069336, Simplifier Solver Time: 0.0008091926574707031 +************** Program is BUGGY ************** + + + +======== File No.28/53 (22 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_13_cex.smt2 ======== +********* SMT2 Loading time: 0.0036780834197998047 secs, Size: 0.76KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_13_cex.smt2.log +************** Finished in 0.017374277114868164 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.004084110260009766 +Others: 0.013290166854858398, Init Phase Time: 0.017152070999145508, Simplifier Solver Time: 0.0003876686096191406 +************** Program is BUGGY ************** + + + +======== File No.29/53 (23 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_14_cex.smt2 ======== +********* SMT2 Loading time: 0.00359344482421875 secs, Size: 0.73KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_14_cex.smt2.log +************** Finished in 0.01604485511779785 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.0029897689819335938 +Others: 0.013055086135864258, Init Phase Time: 0.015825271606445312, Simplifier Solver Time: 0.00033164024353027344 +************** Program is BUGGY ************** + + + +======== File No.30/53 (24 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_15_cex.smt2 ======== +********* SMT2 Loading time: 0.0038459300994873047 secs, Size: 0.73KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_15_cex.smt2.log +************** Finished in 0.01723766326904297 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.003916263580322266 +Others: 0.013321399688720703, Init Phase Time: 0.017017364501953125, Simplifier Solver Time: 0.00040912628173828125 +************** Program is BUGGY ************** + + + +======== File No.31/53 (25 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_disj_ite_01_cex.smt2 ======== +********* SMT2 Loading time: 0.002893686294555664 secs, Size: 0.47KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_disj_ite_01_cex.smt2.log +************** Finished in 0.2394261360168457 (secs) in 1 epochs ************** +Total SVM Calls: 4, DT Calls: 3, Z3 Calls: 21 +Total SVM Time: 0.010687589645385742, DT Time: 0.010200738906860352, Z3 Time: 0.12368655204772949 +Others: 0.09485125541687012, Init Phase Time: 0.02901482582092285, Simplifier Solver Time: 0.001134634017944336 +************** Auxiliary Info ************** +max_len_exp_fwd: 253 +max_len_exp_bwd: 679 +len_exp_zone_fwd: [(80, 117), (253, 481)] +len_exp_zone_bwd: [(138, 185), (277, 341), (411, 491), (545, 641), (679, 791)] +Total Iter: 5 +QE Time: 0.0009891986846923828 +************** Program is BUGGY ************** + + + +======== File No.32/53 (26 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_disj_ite_02_cex.smt2 ======== +********* SMT2 Loading time: 0.0027942657470703125 secs, Size: 0.46KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_disj_ite_02_cex.smt2.log +************** Finished in 2.067319393157959 (secs) in 2 epochs ************** +Total SVM Calls: 11, DT Calls: 63, Z3 Calls: 113 +Total SVM Time: 0.028020858764648438, DT Time: 0.21556329727172852, Z3 Time: 0.70719313621521 +Others: 1.116542100906372, Init Phase Time: 0.020917415618896484, Simplifier Solver Time: 0.006136894226074219 +************** Auxiliary Info ************** +max_len_exp_fwd: 308 +max_len_exp_bwd: 175 +len_exp_zone_fwd: [(69, 135), (308, 602)] +len_exp_zone_bwd: [(175, 286)] +Total Iter: 66 +QE Time: 0.0004405975341796875 +************** Program is BUGGY ************** + + + +======== File No.33/53 (27 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_disj_ite_03_cex.smt2 ======== +********* SMT2 Loading time: 0.0028667449951171875 secs, Size: 0.42KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_disj_ite_03_cex.smt2.log +************** Finished in 14.969561100006104 (secs) in 1 epochs ************** +Total SVM Calls: 73, DT Calls: 463, Z3 Calls: 682 +Total SVM Time: 0.6767323017120361, DT Time: 1.6150786876678467, Z3 Time: 4.490983009338379 +Others: 8.186767101287842, Init Phase Time: 0.029053449630737305, Simplifier Solver Time: 0.05419111251831055 +************** Auxiliary Info ************** +max_len_exp_fwd: 170 +max_len_exp_bwd: 843 +len_exp_zone_fwd: [(36, 79), (170, 315)] +len_exp_zone_bwd: [(93, 135), (270, 349), (454, 577), (640, 813), (843, 1045)] +Total Iter: 465 +QE Time: 0.000881195068359375 +************** Program is BUGGY ************** + + + +======== File No.34/53 (28 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_disj_ite_04_cex.smt2 ======== +********* SMT2 Loading time: 0.002842426300048828 secs, Size: 0.56KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_disj_ite_04_cex.smt2.log +************** Finished in 0.9414050579071045 (secs) in 1 epochs ************** +Total SVM Calls: 7, DT Calls: 25, Z3 Calls: 55 +Total SVM Time: 0.01797628402709961, DT Time: 0.09053587913513184, Z3 Time: 0.3543820381164551 +Others: 0.47851085662841797, Init Phase Time: 0.028515338897705078, Simplifier Solver Time: 0.0033597946166992188 +************** Auxiliary Info ************** +max_len_exp_fwd: 157 +max_len_exp_bwd: 1095 +len_exp_zone_fwd: [(29, 66), (157, 288)] +len_exp_zone_bwd: [(88, 130), (266, 345), (458, 577), (739, 904), (1095, 1289)] +Total Iter: 27 +QE Time: 0.000993490219116211 +************** Program is BUGGY ************** + + + +======== File No.35/53 (29 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_disj_ite_05_cex.smt2 ======== +********* SMT2 Loading time: 0.0028274059295654297 secs, Size: 0.42KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_disj_ite_05_cex.smt2.log +************** Finished in 11.59440302848816 (secs) in 2 epochs ************** +Total SVM Calls: 51, DT Calls: 363, Z3 Calls: 566 +Total SVM Time: 0.3749666213989258, DT Time: 1.2962946891784668, Z3 Time: 3.575744867324829 +Others: 6.3473968505859375, Init Phase Time: 0.024071693420410156, Simplifier Solver Time: 0.04306197166442871 +************** Auxiliary Info ************** +max_len_exp_fwd: 260 +max_len_exp_bwd: 843 +len_exp_zone_fwd: [(63, 103), (260, 480)] +len_exp_zone_bwd: [(53, 97), (420, 526), (843, 999)] +Total Iter: 368 +QE Time: 0.0007562637329101562 +************** Program is BUGGY ************** + + + +======== File No.36/53 (30 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_disj_ite_06_cex.smt2 ======== +********* SMT2 Loading time: 0.0028569698333740234 secs, Size: 0.41KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_search_disj_ite_06_cex.smt2.log +************** Finished in 193.5532193183899 (secs) in 1 epochs ************** +Total SVM Calls: 274, DT Calls: 5070, Z3 Calls: 6022 +Total SVM Time: 43.46053743362427, DT Time: 19.10193634033203, Z3 Time: 39.99265456199646 +Others: 90.99809098243713, Init Phase Time: 0.02531909942626953, Simplifier Solver Time: 0.5663297176361084 +************** Auxiliary Info ************** +max_len_exp_fwd: 248 +max_len_exp_bwd: 980 +len_exp_zone_fwd: [(66, 107), (248, 448)] +len_exp_zone_bwd: [(267, 346), (621, 704), (980, 1134)] +Total Iter: 5072 +QE Time: 0.0007412433624267578 +************** Program is BUGGY ************** + + + +======== File No.37/53 (31 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_shrink_big_numbers_1024_cex.smt2 ======== +********* SMT2 Loading time: 0.004181623458862305 secs, Size: 14.20KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_shrink_big_numbers_1024_cex.smt2.log +************** Finished in 0.0841512680053711 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.029120445251464844 +Others: 0.05503082275390625, Init Phase Time: 0.08391952514648438, Simplifier Solver Time: 0.0008504390716552734 +************** Program is BUGGY ************** + + + +======== File No.38/53 (32 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_shrink_big_numbers_2048_cex.smt2 ======== +********* SMT2 Loading time: 0.0053980350494384766 secs, Size: 29.45KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_shrink_big_numbers_2048_cex.smt2.log +************** Finished in 0.36706995964050293 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.2867143154144287 +Others: 0.08035564422607422, Init Phase Time: 0.36685872077941895, Simplifier Solver Time: 0.0012173652648925781 +************** Program is BUGGY ************** + + + +======== File No.39/53 (33 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_shrink_big_numbers_4096_cex.smt2 ======== +********* SMT2 Loading time: 0.008140325546264648 secs, Size: 59.71KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_shrink_big_numbers_4096_cex.smt2.log +************** Finished in 0.5201935768127441 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.34474897384643555 +Others: 0.1754446029663086, Init Phase Time: 0.5199534893035889, Simplifier Solver Time: 0.0019381046295166016 +************** Program is BUGGY ************** + + + +======== File No.40/53 (34 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_shrink_big_numbers_8192_cex.smt2 ======== +********* SMT2 Loading time: 0.01590251922607422 secs, Size: 92.20KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_shrink_big_numbers_8192_cex.smt2.log +************** Finished in 2.135303497314453 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 1.849890947341919 +Others: 0.2854125499725342, Init Phase Time: 2.1350741386413574, Simplifier Solver Time: 0.0032682418823242188 +************** Program is BUGGY ************** + + + +======== File No.41/53 (35 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_triv_01_cex.smt2 ======== +********* SMT2 Loading time: 0.0028476715087890625 secs, Size: 0.34KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_triv_01_cex.smt2.log +************** Finished in 0.018039226531982422 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.004957914352416992 +Others: 0.01308131217956543, Init Phase Time: 0.017760276794433594, Simplifier Solver Time: 0.0004153251647949219 +************** Program is BUGGY ************** + + + +======== File No.42/53 (36 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_triv_02_cex.smt2 ======== +********* SMT2 Loading time: 0.002626180648803711 secs, Size: 0.32KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_triv_02_cex.smt2.log +************** Finished in 0.011332511901855469 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.006401538848876953 +Others: 0.004930973052978516, Init Phase Time: 0.0031614303588867188, Simplifier Solver Time: 0.0002148151397705078 +************** Auxiliary Info ************** +max_len_exp_fwd: 0 +max_len_exp_bwd: 0 +len_exp_zone_fwd: [] +len_exp_zone_bwd: [] +QE Time: 0.00022745132446289062 +************** Program is BUGGY ************** + + + +======== File No.43/53 (37 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_triv_03_cex.smt2 ======== +********* SMT2 Loading time: 0.002557039260864258 secs, Size: 0.33KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_triv_03_cex.smt2.log +************** Finished in 0.3448920249938965 (secs) in 1 epochs ************** +Total SVM Calls: 5, DT Calls: 4, Z3 Calls: 32 +Total SVM Time: 0.012397050857543945, DT Time: 0.013676166534423828, Z3 Time: 0.20492935180664062 +Others: 0.11388945579528809, Init Phase Time: 0.036940574645996094, Simplifier Solver Time: 0.0015823841094970703 +************** Auxiliary Info ************** +max_len_exp_fwd: 64 +max_len_exp_bwd: 180 +len_exp_zone_fwd: [(11, 28), (28, 52), (40, 76), (52, 128), (64, 160)] +len_exp_zone_bwd: [(31, 68), (68, 144), (108, 216), (144, 288), (180, 360)] +Total Iter: 6 +QE Time: 0.0014982223510742188 +************** Program is BUGGY ************** + + + +======== File No.44/53 (38 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_triv_04_cex.smt2 ======== +********* SMT2 Loading time: 0.0024030208587646484 secs, Size: 0.32KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_triv_04_cex.smt2.log +************** Finished in 0.08763337135314941 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.07067251205444336 +Others: 0.016960859298706055, Init Phase Time: 0.08739566802978516, Simplifier Solver Time: 0.0008070468902587891 +************** Program is BUGGY ************** + + + +======== File No.45/53 (39 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_triv_05_cex.smt2 ======== +********* SMT2 Loading time: 0.002299785614013672 secs, Size: 0.32KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_triv_05_cex.smt2.log +************** Finished in 0.013648271560668945 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.003926992416381836 +Others: 0.00972127914428711, Init Phase Time: 0.013424158096313477, Simplifier Solver Time: 0.00024580955505371094 +************** Program is BUGGY ************** + + + +======== File No.46/53 (40 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_triv_06_cex.smt2 ======== +********* SMT2 Loading time: 0.0022711753845214844 secs, Size: 0.26KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_triv_06_cex.smt2.log +************** Finished in 0.02141737937927246 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.004355430603027344 +Others: 0.017061948776245117, Init Phase Time: 0.021165132522583008, Simplifier Solver Time: 0.0007891654968261719 +************** Program is BUGGY ************** + + + +======== File No.47/53 (41 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_triv_07_cex.smt2 ======== +********* SMT2 Loading time: 0.002495288848876953 secs, Size: 0.37KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_triv_07_cex.smt2.log +************** Finished in 0.010929584503173828 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.002877473831176758 +Others: 0.00805211067199707, Init Phase Time: 0.010692358016967773, Simplifier Solver Time: 0.00020384788513183594 +************** Program is BUGGY ************** + + + +======== File No.48/53 (42 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_triv_08_cex.smt2 ======== +********* SMT2 Loading time: 0.0030629634857177734 secs, Size: 0.53KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_triv_08_cex.smt2.log +************** Finished in 0.04192709922790527 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 2 +Total SVM Time: 6.985664367675781e-05, DT Time: 0, Z3 Time: 0.010324954986572266 +Others: 0.03153228759765625, Init Phase Time: 0.020161867141723633, Simplifier Solver Time: 0.0002269744873046875 +************** Auxiliary Info ************** +max_len_exp_fwd: 197 +max_len_exp_bwd: 166 +len_exp_zone_fwd: [(197, 327)] +len_exp_zone_bwd: [(166, 279)] +Total Iter: 1 +QE Time: 0.0002193450927734375 +************** Program is BUGGY ************** + + + +======== File No.49/53 (43 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_triv_09_cex.smt2 ======== +********* SMT2 Loading time: 0.002937793731689453 secs, Size: 0.35KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_triv_09_cex.smt2.log +************** Finished in 0.019893646240234375 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.0045926570892333984 +Others: 0.015300989151000977, Init Phase Time: 0.019665956497192383, Simplifier Solver Time: 0.0006177425384521484 +************** Program is BUGGY ************** + + + +======== File No.50/53 (44 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_triv_10_cex.smt2 ======== +********* SMT2 Loading time: 0.00767207145690918 secs, Size: 1.25KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_triv_10_cex.smt2.log +************** Finished in 0.06771063804626465 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.002667665481567383 +Others: 0.06504297256469727, Init Phase Time: 0.06746721267700195, Simplifier Solver Time: 0.005326032638549805 +************** Program is BUGGY ************** + + + +======== File No.51/53 (45 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_triv_11_cex.smt2 ======== +********* SMT2 Loading time: 0.007764339447021484 secs, Size: 1.23KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/samples_triv_11_cex.smt2.log +************** Finished in 0.0917205810546875 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.002629995346069336 +Others: 0.08909058570861816, Init Phase Time: 0.09145975112915039, Simplifier Solver Time: 0.006609439849853516 +************** Program is BUGGY ************** + + + +======== File No.52/53 (46 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/vac_1.smt2 ======== +********* SMT2 Loading time: 0.00431513786315918 secs, Size: 0.45KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/vac_1.smt2.log +************** Finished in 0.06152772903442383 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 1 +Total SVM Time: 0, DT Time: 0, Z3 Time: 0.0032939910888671875 +Others: 0.05823373794555664, Init Phase Time: 0.061269521713256836, Simplifier Solver Time: 0.004086971282958984 +************** Program is BUGGY ************** + + + +======== File No.53/53 (47 succeeded): /home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/vac_2.smt2 ======== +********* SMT2 Loading time: 0.004103422164916992 secs, Size: 0.55KB ********** +Log File Name: /home/ssr/PyCHC/log/bench_horn_cex/vac_2.smt2.log +************** Finished in 0.13146233558654785 (secs) in 1 epochs ************** +Total SVM Calls: 0, DT Calls: 0, Z3 Calls: 2 +Total SVM Time: 7.843971252441406e-05, DT Time: 0, Z3 Time: 0.03237414360046387 +Others: 0.09900975227355957, Init Phase Time: 0.13119935989379883, Simplifier Solver Time: 0.005447864532470703 +************** Program is BUGGY ************** + + + +********* Total time elapsed: 36.000000 mins 28.634071 secs ********** +********* Successfully solved: 48/53 ********** +Fail to solve: +/home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/count_by_1_true-unreach-call_true-termination_cex.c.smt2 +/home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_only_05_cex.smt2 +/home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_02_cex.smt2 +/home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_05_cex.smt2 +/home/ssr/PyCHC/tests/freqhorn/bench_horn_cex/samples_search_11_cex.smt2 diff --git a/learner/learner.py b/learner/learner.py index a8a14cf..719e721 100644 --- a/learner/learner.py +++ b/learner/learner.py @@ -43,15 +43,6 @@ def __init__(self, db: HornClauseDb, params, ClassDT, log_path='log.txt', file_n self.cex_counter = 0 self.aux_info = {} # additional stats can be put here as strs - # C5 and SVM binary - if sys.platform == 'linux': - self.svm_exec_path = 'utils/svm/libsvm/svm-invgen' - # self.svm_exec_path = '/dev/shm/svm-invgen' - elif sys.platform == 'darwin': - self.svm_exec_path = 'utils/svm/libsvm/svm-invgen-macos' - else: - self.svm_exec_path = 'utils/svm/libsvm/svm-invgen' - # init self.set_logger() self.solver = z3.Solver() @@ -82,7 +73,6 @@ def __init__(self, db: HornClauseDb, params, ClassDT, log_path='log.txt', file_n self.cand_map = {} self.rel_to_c5_rel_map = {} self.c5_rel_to_rel_map = {} - # self.arg_name_to_expr_map = {} self.svm_name_to_expr_map = {} self.svm_name_to_coeff_map = {} # {svm_name: [coeff]} self.svm_name_to_str_map = {} # for C5 "*.names" input @@ -612,164 +602,6 @@ def svm_learn(self, target=None): if not self.params['SVM']['EnableSVM']: return start_time = time.time() - # if target is None: - # self.svm_name_to_expr_map.clear() - # self.svm_name_to_str_map.clear() - # self.svm_name_to_coeff_map.clear() - # else: # delete all keys that is related to rels in target - # rel_names = [self.rel_to_c5_rel_map[t.decl()] for t in target] - # ks = list(self.svm_name_to_expr_map.keys()) - # for rel_name in rel_names: - # self.svm_name_to_coeff_map.pop(rel_name, 0) - # for k in ks: - # if rel_name in k: - # # self.logger.debug(f'Attr {k} for rel {rel_name} purged') - # self.svm_name_to_expr_map.pop(k, 0) # if pop fails, default val = 0 - # self.svm_name_to_str_map.pop(k, 0) - - # for rel in self.rels: - # if target is None or rel in target: - # args = self.get_rel_args(rel) - # num_svm_vars = 0 - # for i, arg in enumerate(args): - # # if z3.is_bool(arg) or self.unknowns[rel.decl()][i]: - # if z3.is_bool(arg): - # continue - # num_svm_vars += 1 - - # if len(args) == 0: # skip trivial rels - # continue - # if num_svm_vars >= 69: - # self.logger.error('Too many vars, SVM does not support') - # continue - - # svm_str = '' - # pn = nn = 0 - # C5_rel_name = self.rel_to_c5_rel_map[rel.decl()] - # dp_no_bool_dataset_p = OrderedSet() - # dp_no_bool_dataset_n = OrderedSet() - # if self.pos_data_set.is_empty(rel) or self.neg_data_set.is_empty(rel): - # # only pos/neg dps are inputted - # continue - - # for dp in self.pos_data_set.get_dps(rel): - # dp_no_bool = [] - # for i, d in enumerate(dp): - # # if not isinstance(d, bool) and not self.unknowns[rel.decl()][i]: - # if not isinstance(d, bool): - # dp_no_bool.append(d) - # dp_no_bool_dataset_p.add(tuple(dp_no_bool)) - - # for dp in self.neg_data_set.get_dps(rel): - # dp_no_bool = [] - # for i, d in enumerate(dp): - # # if not not isinstance(d, bool) and not self.unknowns[rel.decl()][i]: - # if not isinstance(d, bool): - # dp_no_bool.append(d) - # dp_no_bool_dataset_n.add(tuple(dp_no_bool)) - - # for dp in dp_no_bool_dataset_p: - # if dp in dp_no_bool_dataset_n: - # # except for bool and unknowns, other vars are the same, no need for SVM to learn - # self.logger.info(f'Rel: {rel.decl()} dp: {dp} conflict, no need for SVM to learn') - # return - - # # a[:, ~np.all(a[1:] == a[:-1], axis=0)] - # pn = len(dp_no_bool_dataset_p) - # nn = len(dp_no_bool_dataset_n) - # for dp in dp_no_bool_dataset_p: - # svm_str += '1' - # for d in dp: - # svm_str += ' ' + str(d) - # svm_str += '\n' - - # for dp in dp_no_bool_dataset_n: - # svm_str += '0' - # for d in dp: - # svm_str += ' ' + str(d) - # svm_str += '\n' - - # f_svm = open(self.file_name+'.svm.data', 'w') - # f_svm.write(svm_str) - # f_svm.close() - - # if self.cand_counter % self.params['Verbosity']['PrintNewCandFreq'] == 0: - # self.logger.debug(f'SVM data input:\n{svm_str}') - - # cmd = self.svm_exec_path + \ - # " -c " + str(self.params['SVM']['SVMCParameter']) + \ - # " -t " + str(self.params['SVM']['SVMCoeffBound']) + \ - # " -a " + str(self.params['SVM']['SVMAHyperplane']) + \ - # " -v " + str(num_svm_vars) + \ - # " -p " + str(pn) + \ - # " -n " + str(nn) + \ - # " -g " + str(self.params['LC']) + \ - # " -f " + C5_rel_name + ' ' + self.file_name + '.svm.data' + ' 2>&1' - - # self.logger.info(f'SVM cmd: {cmd}') - - # p = os.popen(cmd, 'r') - # if p is None: - # self.logger.error("popen failed!") - # raise Exception("popen failed!") - # buf = p.read() - # p.close() - # self.logger.debug(f'SVM out buffer: {buf}') - # # f = open('tmp/svm_temp', 'w+') - # # f.write(buf) - # # f.close() - # if buf.find('Segmentation fault') != -1 or buf.find('Kill') != -1: - # self.logger.error('SVM does not properly execute') - # continue - # self.svm_calls += 1 - - # f = open(self.file_name + '.attr', 'r') - # svm_out_lines = f.read().splitlines() - # f.close() - # self.logger.debug(f'SVM data output:\n{svm_out_lines}') - - # svm_i = 0 - # self.svm_name_to_coeff_map[C5_rel_name] = [] - # # self.logger.debug(f'svm_name_to_coeff_map {C5_rel_name} purged') - # for line_num, line in enumerate(svm_out_lines): - # if line == 'true' or line == 'false': - # continue - - # coeff_args = [] - # expr_line = None - # str_line = '' - # thetas = line.split(' ')[1:] # skip the first output of each line - # i = 0 - # for j, arg in enumerate(args): - # if z3.is_bool(arg): - # # if z3.is_bool(arg) or self.unknowns[rel.decl()][j]: # skip boolean/unknown variables in SVM learning - # continue - - # if i >= len(thetas): - # raise IndexError(f'list index {i} out of range {len(thetas)} at iter {j}, \ - # len(args):{len(args)},\nthetas:{thetas},\nargs:{args}') - # theta = thetas[i] - - # if int(theta) == 0: # skip coeff = 0 cases - # i += 1 # non-bool args - # continue - - # expr = int(theta) * arg - # coeff_args.append(expr) - # expr_line = expr if expr_line is None else expr_line + expr - # str_line += '(' + theta + '*' + \ - # C5_rel_name + '!V_' + str(j) + ')+' - # i += 1 - # str_line = str_line[:-1] - - # if len(coeff_args) > 1: # Non-octogon - # name = C5_rel_name + '!SVM_' + str(svm_i) - # self.svm_name_to_expr_map[name] = expr_line - # self.svm_name_to_str_map[name] = str_line - # self.svm_name_to_coeff_map[C5_rel_name].append(thetas) - # self.logger.debug( - # f"SVM inferred a hyperlane for rel {C5_rel_name}({rel.decl()}): {str(str_line)}") - # svm_i += 1 calls, maps = self.svm.learn(self.pos_data_set, self.neg_data_set, target) self.svm_calls += calls