diff options
Diffstat (limited to 'README.md')
-rw-r--r-- | README.md | 182 |
1 files changed, 180 insertions, 2 deletions
@@ -1,2 +1,180 @@ -# smtcoq -Communication between Coq and SAT/SMT solvers +# SMTCoq + +SMTCoq is a Coq tool that checks proof witnesses coming from external +SAT and SMT solvers. + +It relies on a certified checker for such witnesses. On top of it, +vernacular commands and tactics to interface with the SAT solver zChaff +and the SMT solver veriT are provided. It is designed in a modular way +allowing to extend it easily to other solvers. + +Since version 1.2, SMTCoq also provides the possibility to extract the +checker to OCaml. + +The current stable version is the version 1.2. + + +### Installation + +To come. + +<!-- See the INSTALL.md file for instructions. --> + + +### License + +SMTCoq is released under the CeCILL-C license; see LICENSE for more +details. + + +### Use + +Examples are given in the file examples/Example.v. They are meant to be +easily re-usable for your own usage. + + +#### Overview + +The SMTCoq module can be used in Coq files via the `Require Import +SMTCoq.` command. For each supported solver, it provides: + +- a vernacular command to check answers: + `XXX_Checker "problem_file" "witness_file"` returns `true` only if + `witness_file` contains a zChaff proof of the unsatisfiability of the + problem stated in `problem_file`; + +- a vernacular command to safely import theorems: + `XXX_Theorem theo "problem_file" "witness_file"` produces a Coq term + `teo` whose type is the theorem stated in `problem_file` if + `witness_file` is a proof of the unsatisfiability of it, and fails + otherwise. + +- a safe tactic to try to solve a Coq goal using the chosen solver. + +The SMTCoq checker can also be extracted to OCaml and then used +independently from Coq. + +We now give more details for each solver, and explanations on +extraction. + + +#### zChaff + +Compile and install zChaff as explained in the installation +instructions. In the following, we consider that the command `zchaff` is +in your `PATH` variable environment. + + +##### Checking zChaff answers of unsatisfiability and importing theorems + +To check the result given by zChaff on an unsatisfiable dimacs file +`file.cnf`: + +- Produce a zChaff proof witness: `zchaff file.cnf`. This command + 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`. + + +##### zChaff as a Coq decision procedure + +The `zchaff` tactic can be used to solve any goal of the form: + +``` +forall l, b1 = b2 +``` + +where `l` is a list of Booleans (that can be concrete terms). + + +#### veriT + +Compile and install veriT as explained in the installation instructions. +In the following, we consider that the command `veriT` is in your `PATH` +variable environment. + + +##### Checking veriT answers of unsatisfiability and importing theorems + +To check the result given by veriT on an unsatisfiable SMT-LIB2 file +`file.smt2`: + +- 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 command 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 zChaff 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. + + +##### veriT as a Coq decision procedure + +The `verit` tactic can be used to solve 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). |