Revisiting Enumerative Instantiation
We provide here the experimental data used in
our paper. A version of the paper with corrected typos is
available here.
The .zip containing the binary of CVC4 used in our experiments can be downloaded here: cvc4.
The latest version of CVC4 can be downloaded here: CVC4.
The .tgz containing the binary of Z3 used in our experiments can be downloaded here: z3.
To enable individual configurations of CVC4:
- Configuration u is enabled by --sort-inference --no-e-matching --full-saturate-quant.
- Configuration e;u is enabled by --sort-inference --full-saturate-quant.
- Configuration e+u is enabled by --sort-inference --fs-interleave --full-saturate-quant.
- Configuration e is enabled by --sort-inference.
- Configuration m is enabled by --sort-inference --finite-model-find --mbqi-one-inst-per-round --uf-ss=none.
- Configuration e;m is enabled by --sort-inference --finite-model-find --mbqi-one-inst-per-round --uf-ss=none --fmf-inst-engine.
- Configuration e+m is enabled by --sort-inference --finite-model-find --mbqi-one-inst-per-round --uf-ss=none --fmf-inst-engine --mbqi-interleave --inst-when=last-call.
To enable individual configurations of Z3:
- Configuration z3 m is enabled by
- for SMT-LIB:
auto_config=false smt.ematching=false -smt2
- for TPTP: -auto_config:false -smt.ematching:false -file:
- Configuration z3 e is enabled by
- for SMT-LIB:
auto_config=false smt.mbqi=false -smt2
- for TPTP: -auto_config:false -smt.mbqi:false -file:
Configuration z3 e;m is enabled by
- for SMT-LIB:
-smt2
- for TPTP: -file:
- The SMT-LIB benchmarks can be found here.
- The TPTP benchmarks can be found here. We used the benchmarks of the CNF and FOF sublibraries.
Our evaluation used the StarExec cluster for evaluation https://www.starexec.org. The experiments on SMT-LIB can be found here and on TPTP here.
We provide a spreadsheet containing detailed results of the experiments.