Quantifier Instantiation Techniques for Finite Model Finding in SMT

Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark Barrett

This site provides our paper Quantifier Instantiation Techniques for Finite Model Finding in SMT and related material at CADE 2013.

Downloads

• Paper at CADE 2013
• Benchmarks:
  • DVF Benchmarks [tar.gz]
  • Isabelle Experiments Benchmarks with patterns [tgz]
  • Isabelle Experiments Benchmarks without patterns [tgz]
• CVC4 Binary [tgz]

CVC4 configurations

Various cvc4 configurations are reported in the paper, including cvc4, cvc4+f, cvc4+fm, cvc4+fmi, and so on. In the naming convention, configuration whose suffix contains f enable finite model finding, m enable model-based quantifier instantiation, and i enable heuristic instantiation based on E-matching. For a benchmark [FILE], to enable configurations cvc4+f*, use the command:

• cvc4 --finite-model-find [FILE]

By default, cvc4 with finite model finding uses model-based instantiation, i.e., the configuration cvc4+fm. To disable model-based quantifier instantiation (cvc4+f), use:

• cvc4 --finite-model-find --disable-fmf-mbqi[FILE]

To enable configurations cvc4+fi, use the command:

• cvc4 --finite-model-find --fmf-inst-engine [FILE]

DVF Experiments

Some of the DVF benchmarks for these experiments can found above. Detailed results can be found here. In addition to what is described in the paper, these results also show results for the SMT solvers CVC3, Yices, and an additional configuration cvc4+fmo, i.e., cvc4 finite model finding, model-based instantiation, that adds only one instance per instantiation round. This configuration can be enabled by running:

• cvc4 --finite-model-find --fmf-one-inst-per-round [FILE]

TPTP Experiments

We tested all FOF and CNF benchmarks in the TPTP library version 5.4.0. Detailed results can be found here.

Isabelle Experiments

We ran on benchmarks with and benchmarks without user-specified instantiation patterns, as available above. Detailed results can be found here.

---

A description of the finite finding framework in cvc4, including how models of minimal size are found for a set of ground constraints, can be found here.