|
|
|
|
|
|
by saurabh20n
2696 days ago
|
|
|
About the benchmarks, SMT-LIB has had my instances for close to a decade now :) [1,2] We are now generating non-bitvector benchmarks, and maybe in the Fall we will submit newer instances. Back in the day, I was foolish enough to implement my own (bitvector) solver. Hoping to outcompete with the assumption that I could encode heuristics informed by the domain (i.e., synthesis-specific). Turned out Z3's "general" heuristics were just faster. You could say, I let Nikolaj and Leonardo take it from there. For completeness, I also did experiment with a bunch of other solvers that were considered good at the time [3]. (Have to caveat with the fact that CVC3, now CVC4, has always been on my list of future-to-try.) --- [1] VS3: QF_BV (bitvector benchmarks) https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B... -- apologies for the unimaginative name. VS3 stands for "(V)erification and (S)ynthesis using (S)MT (S)olvers" [2] Example SMT instance: https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B... [3] Engineering for synthesis using SMT solvers: Chapter 6 of PhD: http://saurabh-srivastava.com/pubs/saurabh-srivastava-thesis... |
|
|