search

NTU-ALComLab / ssatABC

Stochastic SAT solver within ABC
Other
5 stars 2 forks source link

Fix parseFloat overflow issue #5 #7

Closed yen-shi closed 4 years ago

yen-shi commented 4 years ago

Fix parseFloat() to parse any floating-point numbers. Now, our program accepts prob = 1.0 for random quantifiers. Need to further check whether it will cause an issue.

Link to the issue: https://github.com/nianzelee/ssatABC/issues/5

nianzelee commented 4 years ago

Need to further check whether it will cause an issue.

Thanks for the revision!

Could you please test the revised code with some examples? Preferably with those test cases shown in the paper.

(This should actually be done automatically with CI, but unfortunately I don't have time to set it up now.)

yen-shi commented 4 years ago

Sure, but I might only have time during the weekend.

nianzelee commented 4 years ago

Sure, but I might only have time during the weekend.

No problem. It is not urgent.

yen-shi commented 4 years ago

I'm running the experiments for ER benchmarks, and I'll update the results here tomorrow.

yen-shi commented 4 years ago

I created a list of benchmarks used in the ssatER paper.

./benchmarks/ssatER/planning/ToiletA/sdimacs/toilet_a_10_01.3.sdimacs
./benchmarks/ssatER/planning/ToiletA/sdimacs/toilet_a_10_01.5.sdimacs
./benchmarks/ssatER/planning/ToiletA/sdimacs/toilet_a_10_01.7.sdimacs
./benchmarks/ssatER/planning/ToiletA/sdimacs/toilet_a_10_05.2.sdimacs
./benchmarks/ssatER/planning/ToiletA/sdimacs/toilet_a_10_05.3.sdimacs
./benchmarks/ssatER/planning/ToiletA/sdimacs/toilet_a_10_05.4.sdimacs
./benchmarks/ssatER/planning/ToiletA/sdimacs/toilet_a_10_10.2.sdimacs
./benchmarks/ssatER/planning/conformant/sdimacs/blocks_enc_2_b4_ser--opt-26_.sdimacs
./benchmarks/ssatER/planning/conformant/sdimacs/cube_c7_ser---23_.sdimacs
./benchmarks/ssatER/planning/conformant/sdimacs/cube_c7_ser--opt-24_.sdimacs
./benchmarks/ssatER/planning/conformant/sdimacs/cube_c9_par---10_.sdimacs
./benchmarks/ssatER/planning/conformant/sdimacs/cube_c9_par--opt-11_.sdimacs
./benchmarks/ssatER/planning/conformant/sdimacs/emptyroom_e3_ser--opt-20_.sdimacs
./benchmarks/ssatER/planning/conformant/sdimacs/ring_r4_ser--opt-11_.sdimacs
./benchmarks/ssatER/planning/sand-castle/sdimacs/SC-11.sdimacs
./benchmarks/ssatER/planning/sand-castle/sdimacs/SC-12.sdimacs
./benchmarks/ssatER/planning/sand-castle/sdimacs/SC-13.sdimacs
./benchmarks/ssatER/planning/sand-castle/sdimacs/SC-14.sdimacs
./benchmarks/ssatER/planning/sand-castle/sdimacs/SC-15.sdimacs
./benchmarks/ssatER/planning/sand-castle/sdimacs/SC-16.sdimacs
./benchmarks/ssatER/planning/sand-castle/sdimacs/SC-17.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/MaxSAT-keller4.clq.wcnf.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/QIF-backdoor-2x16-8.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/QIF-backdoor-32-24.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/QIF-bin-search-16.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/QIF-CVE-2007-2875.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/QIF-pwd-backdoor.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/QIF-reverse.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/QIF-reverse2.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/SyGuS-ConcreteActivityService.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/SyGuS-IssueServiceImpl.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/SyGuS-IterationService.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/SyGuS-LoginService.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/SyGuS-PhaseService.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/SyGuS-ProcessBean.sdimacs
./benchmarks/ssatER/MaxCount/sdimacs/SyGuS-UserServiceImpl.sdimacs
./benchmarks/ssatER/MPEC/sdimacs-0.5/c1355-er.sdimacs
./benchmarks/ssatER/MPEC/sdimacs-0.5/c1908-er.sdimacs
./benchmarks/ssatER/MPEC/sdimacs-0.5/c3540-er.sdimacs
./benchmarks/ssatER/MPEC/sdimacs-0.5/c499-er.sdimacs
./benchmarks/ssatER/MPEC/sdimacs-0.5/c5315-er.sdimacs
./benchmarks/ssatER/MPEC/sdimacs-0.5/c7552-er.sdimacs
./benchmarks/ssatER/MPEC/sdimacs-0.5/c880-er.sdimacs

Maybe we would like to include it somewhere in the repo, so the experimental results are easier to be reproduced.

For re-running experiments (only conducted for ssatER), only 11 tests out of 43 tests did not time out on my laptop (with 1000s), and for those tests, the probabilities are the same.

nianzelee commented 4 years ago

Maybe we would like to include it somewhere in the repo, so the experimental results are easier to be reproduced.

Yes sure, this list will work as our CI checks later. Thanks for the effort.

For re-running experiments (only conducted for ssatER), only 11 tests out of 43 tests did not time out on my laptop (with 1000s), and for those tests, the probabilities are the same.

Great. Then I will merge the pull request.