SMTCoq
SMTCoq is a Coq tool that
checks proof witnesses coming from external SAT and SMT solvers.
It provides:
- a certified checker for proof witnesses coming from the SAT
solver zChaff
and the SMT
solver veriT. This checker
increases the confidence in these tools by checking their
answers a posteriori;
- decision procedures through new tactics
named verit, that calls veriT on any Coq goal,
and zchaff, that calls zChaff on any Coq goal.
It is mainly developed
by Michaël
Armand
and Benjamin
Grégoire at INRIA Sophia-Antipolis,
and Chantal
Keller at École Polytechnique and INRIA Saclay-Île-de-France, with
some help
from Germain
Faure
and Laurent
Thery.
Sources
The source code is distributed under the terms of the CeCILL-C
licence.
Download:
To install it, please report to the installation instructions available
in the archive. We provide
a snapshot
of the version of Coq required to compile it, and
a snapshot of the version of veriT used for it.
Top of the page
Use
SMTCoq is designed to be used with versions of zChaff and veriT that can
deliver proof witnesses. Such versions can be downloaded at:
Please follow the instructions available for each solver in order to
compile them in a proof production mode. In the following, we consider
that the commands "veriT" or "zchaff" is in your PATH variable
environment (depending on the one you want to use).
Examples
Examples are given in the file examples/Example.v available in the
archive. They are meant to be easily re-usable for your own usage.
Since version 1.2, extraction to OCaml is available.
Checking zChaff answers of unsatisfiability
If you want to check the result given by zChaff on an unsatisfiable
dimacs file file.cnf:
- Produce a zChaff proof witness: zchaff file.cnf. This
produces a proof witness file named resolve_trace.
- In a Coq file file.v, put:
Require Import SMTCoq.
Zchaff_Checker "file.cnf" "resolve_trace".
- Compile file.v: coqc file.v. If it
returns true then zChaff indeed proved that the problem was
unsatisfiable.
- You can also produce Coq theorems from zChaff proof witnesses:
the commands
Require Import SMTCoq.
Zchaff_Theorem theo "file.cnf" "resolve_trace".
will produce a Coq term theo whose type is the theorem
stated in file.cnf.
Checking veriT answers of unsatisfiability
If you want to check the result given by veriT on an unsatisfiable file file.smt:
- Produce a veriT proof witness: veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-e --disable-ackermann --input=smtlib2 --proof=file.log file.smt2. This produces a proof witness file
named file.log.
- In a Coq file file.v, put:
Require Import SMTCoq.
Section File.
Verit_Checker "file.smt2" "file.log".
End File.
- Compile file.v: coqc file.v. If it
returns true then veriT indeed proved that the problem was
unsatisfiable.
- You can also produce Coq theorems from veriT proof witnesses:
the commands
Require Import SMTCoq.
Section File.
Verit_Theorem theo "file.smt2" "file.log".
End File.
will produce a Coq term theo whose type is the theorem
stated in file.smt2.
The theories that are currently supported are QF_UF, QF_LIA, QF_IDL and their combinations.
zChaff as a Coq decision procedure
The zchaff tactic can be used for any goal of the form:
forall l, b1 = b2
where l is a list of booleans (that can be concrete terms).
veriT as a Coq decision procedure
The verit tactic can be used for any goal of the form:
forall l, b1 = b2
where l is a list of booleans. Those booleans can be any
concrete terms. The theories that are currently supported are QF_UF,
QF_LIA, QF_IDL and their combinations.
Extraction
The src/extraction directory contains the OCaml extracted checker, as
well as additional files to make use of it. You can compile it using the
given Makefile (after compiling SMTCoq): it will produce an executable
in the example directory for testing.
To use it, you can inspire from the file example/example.ml. Edit the
first two lines of src/extraction/Makefile to compile your own files.
Note that even the extracted version of SMTCoq requires both Coq and
SMTCoq to be compiled (mainly since it relies on other Coq plugins).
Top of the page
Suggestions and bugs report
Do not hesitate to make any suggestion or to report bugs to
Chantal
Keller (remove the anti-spam at).
Top of the page
Publications about SMTCoq
-
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses,
Armand, Michaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Thery, Laurent; Werner, Benjamin,
CPP - Certified Programs and Proofs
- First International Conference -
2011. PDF, BIBTEX
-
Verifying SAT and SMT in Coq for a fully automated decision procedure,
Armand, Mickaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Wener, Benjamin,
PSATTT - International Workshop on Proof-Search in Axiomatic
Theories and Type Theories - 2011. PDF, BIBTEX
Top of the page
Old versions
Old stable versions of SMTCoq are available (but not maintained):
Top of the page
Last update: July, 2nd 2014