Scalable Fine-Grained Proofs for Formula Processing

Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine

We provide here the binary, options and experimental data for our CADE paper and the companion report.

Setup

The tarball containing the source code of veriT used in our experiments is available here. The command line parameters of veriT used in each of the configurations described in the paper are:

• Basic: "--old-processing --disable-sym --disable-simp --disable-unit-simp --disable-unit-subst-simp --disable-ackermann --disable-bclause"
• Extended: "--old-processing --disable-sym --disable-unit-simp --disable-unit-subst-simp --disable-ackermann --disable-bclause"
• Complete: "--old-processing"
• with proofs: "--proof=/dev/null --proof-with-sharing"
• with new code: remove parameter "--old-processing"

The benchmarks can be found here, divided according to the categories in SMT-LIB.

Our experiments were conducted on servers equipped with two Intel Xeon E5-2630 v3 processors, with eight cores per processor, and 126 GB of memory. The time limit was set to 30 s.

Results

The experimental data for each configuration:

qf_complete_no-proofs_new qf_complete_no-proofs_old qf_extended_no-proofs_new qf_extended_no-proofs_old qf_basic_no-proofs_new qf_basic_no-proofs_old	complete_no-proofs_new complete_no-proofs_old extended_no-proofs_new extended_no-proofs_old basic_no-proofs_new basic_no-proofs_old
qf_extended_proofs_new qf_basic_proofs_new qf_basic_proofs_old	extended_proofs_new basic_proofs_new basic_proofs_old