Datatypes with Shared Selectors

Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark Barrett

This site provides our paper Datatypes with Shared Selectors and related material at IJCAR 2018.

An extended version of our paper at IJCAR 2018 can be found below.

Downloads

• Paper at IJCAR 2018
• Extended version of our paper at IJCAR 2018
• Benchmarks:
  • SyGuS Benchmarks [zip]
  • SMTLib full benchmark suite [zip]
  • SMTLib filtered benchmark suite [zip]
• Binaries:
  • CVC4 1.5 Binary [zip]
    The CVC4 version used for our experiments.
  • CVC4 1.5 (modified) Binary [tzip]
    We also used this modified version of CVC4 that prints out selector statistics for SyGuS and SMT files.
  • Z3 Binary [zip]
    Used in default configuration without any options.
  • Vampire Binary [zip]
    The Vampire solver from StarExec's SMT Comp 2017.
  • EUSolver Binary [zip]
    The EUSolver from StarExec's SyGuS Comp 2017.

CVC4 configurations

The following are the individual configurations we used on CVC4 in our experiments:

• CVC4 with shared selectors on SMTLib benchmarks is enabled by --finite-model-find.
• CVC4 without shared selectors on SMTLib benchmarks is enabled by --finite-model-find --no-dt-share-sel.
• CVC4 with shared selectors and enumerative solving methods on SyGuS benchmarks is enabled by --lang=sygus --dump-synth --default-dag-thresh=0 --cegqi-si=none.
• CVC4 without shared selectors and enumerative solving methods on SyGuS benchmarks is enabled by --lang=sygus --dump-synth --default-dag-thresh=0 --cegqi-si=none --no-dt-share-sel.
• CVC4 with single invocation solving methods on SyGuS benchmarks is enabled by --lang=sygus --dump-synth --default-dag-thresh=0 --cegqi-si=all.

The modified version of CVC4 supports all the above configurations; additionally, when used with the --stats option, it provides the number of selectors and shared selectors generated by the solver.

Experimental Setup

SyGuS

We ran CVC4 (with enumerative methods) with and without selectors on the SyGuS benchmark suite. We noted how many benchmarks were solved by each configuration. For benchmarks that didn’t time out on both versions of CVC4, we compared the time taken, the number of SAT decisions made, the number of terms generated, and the number of selectors used by either configuration of the solver.

We also compared the total number of benchmarks CVC4 could solve (with both enumerative methods and single invocation methods) with those that the EUSolver could solve.

SMTLib

We preprocessed the SMTLib benchmarks to check how many of them actually shared selectors. We eliminated all benchmarks that didn’t share benchmarks. We checked the difference in time and other statistics on these eliminated benchmarks with CVC4 with and without shared selectors; we found the difference to be insignificant.

From the filtered benchmarks we ran CVC4 with and without shared selectors to find out how many benchmarks each configuration could solve. On benchmarks that didn’t time out on both configurations, we compared the time taken, the number of SAT decisions made, the number of terms generated, and the number of selectors used by either configuration of the solver.

Results

The data from our SyGuS experiment can be found here. This spreadsheet contains the data from the final SMTLib evaluation on benchmarks that share selectors. The comparison of statistics on benchmarks that were eliminated from the SMTLib benchmarks we considered can be found here.