Relational Constraint Solving in SMT

Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark Barrett

This site provides our paper Relational Constraint Solving in SMT and related material at CADE 2017.

An extended version of our paper at CADE 2017 can be found below.

All materials to reproduce the experimental evaluation in our paper can be found below.

Downloads

• Paper at CADE 2017
• Extended version of our paper at CADE 2017
• Artifact [tgz]
  This artifact provides all benchmarks and binaries used for the experiments. It contains:
  • /data/alloybenchmarks/alloymodels -- the alloy benchmarks
  • /data/alloybenchmarks/cvc4-rel -- cvc4 benchmarks translated using CVC4 built-in relational operators
  • /data/alloybenchmarks/cvc4-ax -- cvc4 benchmarks translated by axiomatizing relational operators
  • /data/owlbenchmarks/owl -- the 6034 owl benchmarks (under 1MB) (The original dataset can be found at here)
  • /data/owlbenchmarks/owl_9 -- the 9 owl benchmarks that CVC4 and Konclude disagree on
  • /data/owlbenchmarks/owl_cvc4 -- 3936 cvc4 benchmarks translated from owl models
  • /data/solvers/cvc4_linux -- cvc4 binary for linux
  • /data/solvers/Alloy4.2.jar -- the Alloy Analyzer

Alloy Experiment

We run CVC4 with two configurations:

• --finite-model-find --fmf-inst-engine --trigger-sel=max
• --finite-model-find

OWL Experiment

We run cvc4 with “–finite-model-find” enabled.