Benchmark results "Unexpected"

[baigd]

Hi Zhoulai,

I had a trial of Xsat on the Benchmarks (Table 1 of Xsat paper), but got incorrect (unexpected) results on (6), (7), (8), (14), (16), (17), (18), (19), (23), (29), (30). I have looked into the generated foo.c and found the floating-point constants are not parsed correctly. I anticipate there may be some problem in the parsing process. I have tried to run Xsat with Docker, and the problem remains. Do you have any suggestion on the location I can fix it?

Thanks!

[zhoulaifu]

Thanks for pointing out the issue. It looks like a regression. Not sure if it has anything to do with the new Z3 or sympy frontends.

I hacked the FP parsing parts here: https://github.com/zhoulaifu/xsat/blob/master/xsat_gen.py#L147. It was quick and dirty; a more robust parsing should have be used. I am working on other projects now, but will maintain the repo later.