From c038e792db9d7551ce7634f0b9ba31ab0e03e5d9 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Thu, 30 Apr 2015 17:45:33 +0200 Subject: More details on extraction --- README.md | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index fff1054..ed2b053 100644 --- a/README.md +++ b/README.md @@ -8,8 +8,8 @@ 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. +Since version 1.2, SMTCoq also provides an extracted version of the +checker, available only with native-coq. The current stable version is the version 1.2. @@ -159,9 +159,11 @@ terms. The theories that are currently supported are `QF_UF`, `QF_LIA`, 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). +`smtcoq` that can be run independently of SMTCoq in this way: +- `smtcoq -zchaff foo.cnf foo.zlog` runs the ZChaff checker on a DIMACS + file and the corresponding ZChaff certificate +- `smtcoq -verit foo.smt2 foo.vtlog` runs the veriT checker on a SMTLIB2 + file and the corresponding veriT certificate. + +Note that even the extracted version of SMTCoq requires both native-coq +and SMTCoq to be compiled (mainly since it relies on other Coq plugins). -- cgit