Finite Model Finding in SMT

Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic

This site provides our paper Finite Model Finding in SMT and related material at CAV 2013.

Downloads

• Paper at CAV 2013
• Benchmarks [tgz]
• CVC4 Binary [tgz]

CVC4 Configurations

The following cvc4 configurations are reported in the paper:

• cvc4
• cvc4+f (with finite model finding)
• cvc4+fe (with finite model finding, clique lemmas reported in terms of explanations)
• cvc4+f-r (with finite model finding, without regions optimization)

These configurations can be run using the following commands for a benchmark file.smt2:

• cvc4 file.smt2
• cvc4 --finite-model-find --disable-fmf-mbqi file.smt2
• cvc4 --finite-model-find --disable-fmf-mbqi --uf-ss-explained-cliques file.smt2
• cvc4 --finite-model-find --disable-fmf-mbqi --disable-uf-ss-regions file.smt2

Results

Detailed results can be found here.

---

A detailed description of the quantifier instantiation techniques used with finite model finding can be found here.