Merge from LFSC (#26)

* Showing models as coq counter examples in tactic without constructing coq terms

* also read models when calling cvc4 with a file (deactivated because cvc4 crashes)

* Show counter examples with variables in the order they are quantified in the Coq goal

* Circumvent issue with ocamldep

* fix issue with dependencies

* fix issue with dependencies

* Translation and OCaml support for extract, zero_extend, sign_extend

* Show run times of components

* print time on stdout instead

* Tests now work with new version (master) of CVC4

* fix small printing issue

* look for date on mac os x

* proof of valid_check_bbShl: some cases to prove.

* full proof of "left shift checker".

*  full proof of "rigth shift checker".

* Support translation of terms bvlshr, bvshl but LFSC rules do not exists at the moment
Bug fix for bitvector extract (inverted arguments)

* Typo

* More modularity on the format of traces depending on the version of coq

* More straightforward definitions in Int63Native_standard

* Use the Int31 library with coq-8.5

* Use the most efficient operations of Int31

* Improved performance with coq-8.5

* Uniform treatment of sat and smt tactics

* Hopefully solved the problem with universes for the tactic

* Updated the installation instructions

* Holes for unsupported bit blasting rules

* Cherry-picking from smtcoq/smtcoq

* bug fix hole for bitblast

* Predefined arrays are not required anymore

* fix issue with coq bbT and bitof construction from ocaml

* bug fix in smtAtom for uninterpreted functions
fix verit test file

* fix issue with smtlib2 extract parsing

* It looks like we still need the PArray function instances for some examples (see vmcai_bytes.smt2)

* Solver specific reification:
Each solver has a list of supported theories which is passed to Atom.of_coq, this function creates uninterpreted functions / sorts for unsupported features.

* show counter-examples with const_farray instead of const for constant array definitions

* Vernacular commands to debug checkers.
Verit/Lfsc_Checker_Debug will always fail, reporting the first proof step of the certificate that failed be checked

* Update INSTALL.md

* show smtcoq proof when converting

* (Hopefully) repared the universes problems

* Corrected a bug with holes in proofs

* scripts for tests:
create a folder "work" under "lfsc/tests/", locate the benchmarks there.
create a folder "results" under "lfsc/tests/work/" in which you'll find the results of ./cvc4tocoq.

* make sure to give correct path for your benchs...

* Checker for array extensionality modulo symmetry of equality

* fix oversight with bitvectors larger than 63 bits

* some printing functions for smt2 ast

* handle smtlib2 files with more complicated equivalence with (= ... )

* revert: ./cvc4tocoq does not output lfsc proofs...

* bug fix one input was ignored

* Don't show verit translation of LFSC proof if environment variable DONTSHOWVERIT is set
(e.g. put export DONTSHOWVERIT="" in your .bashrc or .bashprofile)

* Also sort names of introduced variables when showing counter-example

* input files for which SMTCoq retuns false.

* input files for which SMTCoq retuns false.

* use debug checker for debug file

* More efficient debug checker

* better approximate number of failing step of certificate in debug checker

* fix mistake in ml4

* very first attempt to support goals in Prop

* bvs: comparison predicates in Prop and their <-> proofs with the ones in bool
farrays: equality predicate in Prop and its <-> proof with the one in bool.

* unit, Bool, Z, Pos: comparison and equality predicates in Prop.

* a typo fixed.

* an example of array equality in  Prop (converted into Bool by hand)...
TODO: enhance the search space of cvc4 tactic.

* first version of cvc4' tactic: "solves" the goals in Prop.
WARNING: supports only bv and array goals and might not be complete
TODO: add support for lia goals

* cvc4' support for lia
WARNING: might not be complete!

* small fix in cvc4' and some variations of examples

* small fix + support for goals in Bool and Bool = true + use of solve tactical
WARNING: does not support UF and INT63 goals in Prop

* cvc4': better arrangement

* cvc4': Prop2Bool by context search...

* cvc4': solve tactial added -> do not modify unsolved goals.

* developer documentation for the smtcoq repo

* cvc4': rudimentary support for uninterpreted function goals in Prop.

* cvc4': support for goals with Leibniz equality...
WARNING: necessary use of "Grab Existential Variables." to instantiate variable types for farrays!

* cvc4': Z.lt adapted + better support from verit...

* cvc4': support for Z.le, Z.ge, Z.gt.

* Try arrays with default value (with a constructor for constant arrays), but extensionality is not provable

* cvc4': support for equality over uninterpreted types

* lfsc demo: goals in Coq's Prop.

* lfsc demo: goals in Bool.

* Fix issue with existential variables generated by prop2bool.
- prop2bool tactic exported by SMTCoq
- remove useless stuff

* update usage and installation instructions

* Update INSTALL.md

* highlighting

* the tactic: bool2prop.

* clean up

* the tactic smt: very first version.

* smt: return unsolved goals in Prop.

* Show when a certificate cannot be checked when running the tactic instead of at Qed

* Tactic improvements
- Handle negation/True/False in prop/bool conversions tactic.
- Remove alias for farray (this caused problem for matching on this type in tactics).
- Tactic `smt` that combines cvc4 and veriT.
- return subgoals in prop

* test change header

* smt: support for negated goals + some reorganization.

* conflicts resolved + some reorganization.

* a way to solve the issue with ambiguous coercions.

* reorganization.

* small change.

* another small change.

* developer documentation of the tactics.

* developer guide: some improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* pass correct environment for conversion + better error messages

* cleaning

* ReflectFacts added.

* re-organizing developers' guide.

* re-organizing developers' guide.

* re-organizing developers' guide.

* removing unused maps.

* headers.

* artifact readme getting started...

* first attempt

* second...

* third...

* 4th...

* 5th...

* 6th...

* 7th...

* 8th...

* 9th...

* 10th...

* 11th...

* 12th...

* 13th...

* 14th...

* 15th...

* 16th...

* 17th...

* Update artifact.md

Use links to lfsc repository like in the paper

* 18th...

* 19th...

* 20th...

* 21st...

* 22nd...

* 23rd...

* 24th...

* 25th...

* 26th...

* 27th...

* 28th...

* Update artifact.md

Small reorganization

* minor edits

* More minor edits

* revised description of tactics

* Final pass

* typo

* name changed: artifact-readme.md

* file added...

* passwd chaged...

* links...

* removal

* performance statement...

* typos...

* the link to the artifact image updated...

* suggestions by Guy...

* aux files removed...

* clean-up...

* clean-up...

* some small changes...

* small fix...

* additional information on newly created files after running cvc4tocoq script...

* some small fix...

* another small fix...

* typo...

* small fix...

* another small fix...

* fix...

* link to the artifact image...

* We do not want to force vm_cast for the Theorem commands

* no_check variants of the tactics

* TODO: a veriT test does not work anymore

* Compiles with both versions of Coq

* Test of the tactics in real conditions

* Comment on this case study

* an example for the FroCoS paper.

* Fix smt tactic that doesn't return cvc4's subgoals

* readme modifications

* readme modifications 2

* small typo in readme.

* small changes in readme.

* small changes in readme.

* typo in readme.

* Sync with https://github.com/LFSC/smtcoq

* Port to Coq 8.6

* README

* README

* INSTALL

* Missing file

* Yves' proposition for installation instructions

* Updated link to CVC4

* Compiles again with native-coq

* Compiles with both versions of Coq

* Command to bypass typechecking when generating a zchaff theorem

* Solved bug on cuts from Hole

* Counter-models for uninterpreted sorts (improves issue #13)

* OCaml version note (#15)

* update .gitignore

* needs OCaml 4.04.0

* Solving merge issues (under progress)

* Make SmtBtype compile

* Compilation of SmtForm under progress

* Make SmtForm compile

* Make SmtCertif compile

* Make SmtTrace compile

* Make SatAtom compile

* Make smtAtom compile

* Make CnfParser compile

* Make Zchaff compile

* Make VeritSyntax compile

* Make VeritParser compile

* Make lfsc/tosmtcoq compile

* Make smtlib2_genconstr compile

* smtCommand under progress

* smtCommands and verit compile again

* lfsc compiles

* ml4 compiles

* Everything compiles

* All ZChaff unit tests and most verit unit tests (but taut5 and un_menteur) go through

* Most LFSC tests ok; some fail due to the problem of verit; a few fail due to an error "Not_found" to investigate

* Authors and headings

* Compiles with native-coq

* Typo

2 files changed, 918 insertions, 0 deletions

diff --git a/doc/artifact-readme.md b/doc/artifact-readme.md
new file mode 100644
index 0000000..47c6332
--- /dev/null
+++ b/doc/artifact-readme.md
@@ -0,0 +1,257 @@
+# SMTCoq artifact
+
+SMTCoq is a Coq tool that can be used to dispatch goals to external SAT and SMT solvers
+or simply to check proof witnesses produced by them.
+It currenly supports the quantifier free fragments of the SMT-LIB theories of fixed-sized bit-vectors (`QF_BV`),
+functional arrays (`QF_A`), linear integer arithmetic (`QF_LIA`), equality over uninterpreted functions
+(`QF_EUF`), and their combinations.
+
+This document describes the organization of the SMTCoq artifact submission for CAV 2017.
+
+## How to download the artifact
+
+To get the artifact, please browse [here](https://drive.google.com/file/d/0BzDtBR99eKp9WVNNLTlBQy1Lc28/view)
+and download the `SMTCoq.ova` which is an image of an 
+Ubuntu 16.04 LTS running virtual machine with approximately 3.6GB size 
+(using 8GB memory, single processor which runs at the same frequency with the host processor,
+and approximately 63GB virtual disk space once imported).
+Then, please run [VirtualBox](https://www.virtualbox.org/wiki/VirtualBox);
+from the `File` top-down menu click on `Import Appliance...` and locate the `SMTCoq.ova`
+image. This will create you a virtual machine named `SMTCoq`. To run it, simply click on `Start`.
+The login (and super user) password is `123`.
+
+
+## How to install the artifact
+
+Once logged into the virtual machine, you will find SMTCoq installed. 
+If you want to install it on a separate machine, please check the SMTCoq
+[installation guide](https://github.com/lfsc/smtcoq/blob/master/INSTALL.md).
+
+
+## How to run the artifact
+
+There are two use-cases of SMTCoq:
+ - `within a Coq tactic`: we can give a Coq goal to an external solver and get a
+proof certificate for it. If the checker can validate the certificate, 
+the soundness of the checker allow us to establish a proof of the initial goal
+(by `computational reflection`).
+In this use case, the trusted base consists only of Coq: if something else goes wrong
+(e.g., the checker cannot validate the certificate), the tactic will fail, but
+nothing unsound will be added to the system.
+ - `correct-by-construction checker`: the idea is to check the
+validity of a proof witness, or proof certificate, produced by an external SMT solver
+for some input problem. In this use case, the
+trusted base is both Coq and the parser of the input problem.
+
+### Within a Coq tactic
+
+Once logged into the virtual machine, open a terminal and go to `unit-tests` directory
+by typing `cd Desktop/smtcoq/unit-tests` from home. It contains a test file (`Tests_lfsc.v`) which makes
+use of the new SMTCoq tactics inside Coq, to discharge goals with the aid of various SMT
+solvers.
+
+#### Running everything with a single command
+
+You can run Coq in batch mode on our test file (once you are in the correct
+directory) by simply running the following command:
+
+```
+coqc Tests_lfsc.v
+```
+
+The return code should be 0 to indicate that Coq typed-checked everything correctly. The batch
+compiler `coqc` tries to compile `Tests_lfsc.v` file into `Test_lfsc.vo`. Please refer to
+[Coq reference manual](https://coq.inria.fr/refman/Reference-Manual008.html#compiled) for details.
+
+#### Interactive session through CoqIDE
+
+In the `unit-test` directory, open the test file by running
+
+```
+coqide Tests_lfsc.v
+```
+
+in the terminal. This will load in `CoqIDE` (the Coq interactive development environment)
+the file where we use SMTCoq within a Coq tactic called `smt`.
+Within the CoqIDE, use `Forward one command` button (downarrow on the top-left corner) to
+navigate through the source since `Go to end` button uses a parallelization strategy
+which is not yet supported by SMTCoq.
+
+If the background becomes green after going one command forward, this means
+that Coq has accepted the statement. At the end of the session the whole file should be green.
+If Coq fails to accept any statement, you will see a brief reason of the failure in the
+bottom-right rectangle within the `Errors` tab.
+
+
+
+#### Understanding the test file
+
+```coq
+Require Import SMTCoq.
+```
+
+loads the SMTCoq module. It might be interesting to check out the implementation
+details (with pointers to source codes) of the module
+[here](https://github.com/lfsc/smtcoq/blob/master/doc/sources.md). 
+
+Similarly,
+
+```coq
+Require Import Bool PArray Int63 List ZArith Logic.
+```
+
+loads above-mentioned modules from the Coq standard library.
+
+```coq
+Infix "-->" := implb (at level 60, right associativity) : bool_scope.
+```
+
+introduces a new notation `-->` for the boolean implication.
+
+Using 
+
+```coq
+Section BV.
+```
+we open a new section to prove theorems from the theory of fixed-size bitvectors. 
+
+```coq
+Import BVList.BITVECTOR_LIST.
+Local Open Scope bv_scope.
+```
+
+are to load our own [bitvector module](https://github.com/lfsc/smtcoq/blob/master/src/bva/BVList.v)
+(called BITVECTOR_LIST in BVList.v file)
+to be able to use theorems proven and notations introduced there. Note that to end a
+section `XX` you need to type
+
+```coq
+End XX.
+```
+
+Now, we can state goals and prove them automatically. For instance, the goal
+
+```coq
+  Goal forall (a b c: bitvector 4),
+                                 (c = (bv_and a b)) ->
+                                 ((bv_and (bv_and c a) b) = c).
+```
+
+is proven by the `smt` tactic which subsumes the powers of the tactics `cvc4` and `verit`:
+```coq
+  Proof.
+    smt.
+  Qed.
+```
+
+Here are some more detailed explanation of the tactics: 
+
+ - `verit` -> applies to Coq goals of type `Prop`: 
+ it first calls `prop2bool` on the goal, converting the goal to a term of type `bool`, 
+ it then calls the reification tactic `verit_bool` (which applies only to Boolean goals),
+ and it finally converts the goals back to `Prop`, by calling `bool2prop`, if it is not
+ solved.
+ 
+- `cvc4` -> applies to Coq goals of type `Prop`: 
+ it first calls `prop2bool` on the goal, converting the goal to a term of type `bool`, 
+ it then calls the reification tactic `cvc4_bool` (which applies only to Boolean goals),
+ and it finally converts any unsolved subgoals returned by CVC4 back to `Prop`, 
+ by calling `bool2prop`.
+ 
+- `smt` -> has the combined effect of the `cvc4` and `verit` tactics: 
+ it first calls `prop2bool` on the goal, it then calls either of the `cvc4_bool` and 
+ `verit_bool` tactics, and it finally converts any unsolved subgoals back to `Prop`, 
+ by calling `bool2prop`.
+
+The reification tactics `cvc4_bool` and `verit_bool`, implemented in OCaml, do most of the work:
+calling the external solvers (`CVC4` and `veriT` respectively), getting a
+proof certificate, and if SMTCoq's checker can validate the certificate, establishing the proof
+of the initial goal. The translation tactics `prop2bool` and `bool2prop` are implemented in Coq using
+the Ltac language. 
+
+NB: all of the above tactics perform better on a "standard" machine compared to the VM.
+
+Another example of a goal in the theory of bit-vectors is the following:
+
+```coq
+  Goal forall (bv1 bv2 bv3: bitvector 4),
+      bv1 = #b|0|0|0|0|  /\
+      bv2 = #b|1|0|0|0|  /\
+      bv3 = #b|1|1|0|0|  ->
+      bv_ultP bv1 bv2 /\ bv_ultP bv2 bv3.
+  Proof. 
+     smt.
+  Qed.
+```
+
+This goal uses three bit-vectors of size four: `bv1`, `bv2` and `bv3` then sets them to
+`0000`, `1000` and `1100` in the given order (`#b|1|0|...|` is the notation for bit-vector
+constants, where `0` stands for `false` and `1` is for `true`). Finally, it states
+that `bv1` is less than (unsigned less than over bit-vectors) `bv2` and (propositional)
+`bv2` is less than `bv3`. The tactic `smt` suffices to solve the goal. 
+
+
+The following sections `Arrays`, `LIA`, `EUF`, `PR`and `A_BV_EUF_LIA_PR` in the Coq file include goals that
+can be proven by the `smt` tactic from the theories of functional arrays; linear integer
+arithmetic; uninterpreted functions; propositional reasoning and the combination of functional
+arrays, fixed-size bit-vectors, uninterpreted functions, linear integer arithmetic and
+propositional reasoning; respectively.
+
+
+The example that appears in the paper can be found in the section `A_BV_EUF_LIA_PR`:
+
+```coq
+Goal forall (a b: farray Z Z) (v w x y: Z)
+            (r s: bitvector 4)
+            (f: Z -> Z)
+            (g: farray Z Z -> Z)
+            (h: bitvector 4 -> Z),
+            a[x <- v] = b /\ a[y <- w] = b ->
+            r = s /\ h r = v /\ h s = y ->
+            v < x + 1 /\ v > x - 1 ->
+            f (h r) = f (h s) \/ g a = g b.
+  Proof.
+    smt. (** "cvc4. verit." also solves the goal *)
+  Qed.
+```
+
+It introduces two arrays `a` and `b` of type `farray Z Z` (the type of integer arrays
+with integer indices); four integers `v`, `w`, `x` and `y`; three uninterpreted fuctions
+`f`, `g` and `h`. 
+Notice that `a[i]` is used to select the value stored in the `i^th^` index of the array `a`
+while `a[x <- v]` is used to store the value `v` in `a[x]`, `x^th^` index of array `a`. 
+
+
+
+### Correct-by-construction checker
+
+Using SMTCoq as a `correct-by-construction checker` means that it is possible to start with
+a problem in SMT-LIB standard, call an external solver (CVC4 or veriT) on it, get the
+unsatisfiability proof and certify it using the certified "small checkers" of SMTCoq.
+
+To test that, in a terminal go to `tests` directory (from home) by typing 
+`cd Desktop/smtcoq/src/lfsc/tests`. Run the shell script `cvc4tocoq` providing
+an input file (i.e., `uf1.smt2`) by typing `./cvc4tocoq uf1.smt2`. 
+This will call `CVC4`, get the proof in `LFSC` format, type check and convert it (using a converter
+written in OCaml) into SMTCoq format (which is very close to the proof format of `veriT`) and call
+the SMTCoq checker. If the checker returns `true` that means that SMTCoq indeed agreed that the proof of
+the input problem is correct. If it returns `false`, that means either that the proof is incorrect
+or that the OCaml converter is mistaken/incomplete. Note that you can replace `uf1.smt2`
+with any `.smt2` extended file under
+`tests` directory (`/home/Desktop/smtcoq/src/lfsc/tests`).
+
+Feel free to generate your own problem files but please recall that the input problems should be from the
+supported theories: `QF_A`, `QF_BV`, `QF_LIA`, `QF_EUF`, and their combinations.
+
+NB: The successful execution of the `./cvc4tocoq XX.smt2` script outputs some new
+files:
+- `XX.lfsc` -> the file includes the `LFSC` style unsatisfiability proof of the input problem `XX.smt2`.
+- `XX_lfsc.v`    -> Coq source file that calls the Coq checkers to validate the proof`XX.lfsc`.
+- `XX_lfsc.glob` -> the file includes the globals of the source `XX_lfsc.v`.
+- `XX_lfsc.vo`   -> compliled module file of the source `XX_lfsc.v`, it is used when to load the modules from the source `XX_lfsc.v`.
+
+ 
+
+
+
+
diff --git a/doc/sources.md b/doc/sources.md
new file mode 100644
index 0000000..55d2cec
--- /dev/null
+++ b/doc/sources.md
@@ -0,0 +1,661 @@
+# SMTCoq sources
+
+This document describes the organization of the SMTCoq repository and locations
+of source code and modules.
+
+Sources are contained in the directory [src](../src) which can be found at
+top-level. The directories [examples](../examples) and
+[unit-tests](../unit-tests) contain respectively example files of usage for
+SMTCoq and regression tests for the different tactics and vernacular commands
+that the plugin provides.
+
+The rest of the document describes the organization of `src`.
+
+
+## Top-level architecture of SMTCoq
+
+SMTCoq sources are contained in this directory. A few Coq files can be found at
+top-level.
+
+### [configure.sh](../src/configure.sh)
+
+This script is meant to be run when compiling SMTCoq for the first time. It
+should also be run every time the Makefile is modified. It takes as argument an
+optional flag `-native` which, when present, will set up the sources to use the
+*native Coq* libraries. Otherwise the standard version 8.5 of Coq is used. See
+section [versions](#versions).
+
+### [SMTCoq.v](../src/SMTCoq.v)
+
+This is the main SMTCoq entry point, it is meant to be imported by users that
+want to use SMTCoq in their Coq developments. It provides (exports) the other
+SMTCoq modules as well as declares the OCaml plugin for adding the new
+vernacular commands and tactics.
+
+### [Trace.v](../src/Trace.v)
+
+This file defines the types of certificates and steps (atomic certificate
+pieces) as well as the *main checkers*.
+
+The first section `trace` gives a generic definition of a main checker
+parameterized by the type of individual steps and a function to check
+individual steps `check_step` (small checkers). Correctness of the main checker
+is proved under the assumption that the small checker is correct.
+
+These generic definitions are applied to construct main checkers for resolution
+(module `Sat_Checker`), CNF conversion (module `Cnf_Checker`) and
+satisfiability modulo theories (module `Euf_Checker`). They each define an
+inductive type `step` to represent certificate steps. For instance, in the case
+of the resolution checker, the only possible step is to apply the resolution
+rule so steps are defined as:
+
+```coq
+Inductive step :=
+   | Res (_:int) (_:resolution).
+```
+
+The main theorems for these modules are named `checker_*correct`. For instance
+the main result for the SMT checker (`Euf_Checker`) is formulated as follows:
+
+```coq
+Lemma checker_correct : forall d used_roots c,
+    checker d used_roots c = true ->
+    ~ valid t_func t_atom t_form d.
+```
+
+which means that if the checker returns true on the formula `d` and the
+certificate `c` then `d` is not valid (*i.e.* `c` is a refutation proof
+certificate for `d`).
+
+
+
+### [State.v](../src/State.v)
+
+This module is used to define representations for the global state of the
+checker. 
+
+A state is an array of clauses:
+
+```coq
+Module S.
+  Definition t := array C.t.
+...
+End S.
+```
+
+on which we define resolution chain operations `set_resolve` that modify the
+state.
+
+Variables, literals and clauses are defined respectively in modules `Var`,
+`Lit` and `C`. Binary resolution is defined between two clauses in `C.resolve`.
+
+
+
+### [SMT_terms.v](../src/SMT_terms.v)
+
+This Coq module defines reification types for formulas (`Form.form`), types
+(`Typ.type`) and atoms/terms (`Atom.atom`). Formulas are given an
+interpretation in Coq's Booleans, types are interpreted in Coq types (for
+instance, type `TZ` is interpreted as Coq's mathematical integers `Z`) and
+atoms are interpreted as Coq terms of type the interpretation of their type
+(for instance an atom whose type is `TZ` is interpreted as an integer of `Z`).
+
+
+**Some important lemmas:**
+
+A function `cast` allows to change the encoded type of a term of type
+`Typ.type` when we know two types are equal (the inductive `cast_result`
+provides the conversion function).
+
+```coq
+Fixpoint cast_refl A:
+      cast A A = Cast (fun P (H : P A) => H).
+```
+
+This is the lemma to use to remove cast constructions during the proofs.
+
+
+
+```coq
+Lemma i_eqb_spec : forall t x y, i_eqb t x y <-> x = y.
+```
+
+This other lemma says that Boolean equality over interpretation of types is the
+equivalent to Leibniz equality. This is useful to allow rewriting.
+
+
+Atom (as well as formulas) are encoded by integers, and mapping is preserved by
+an array `t_atom`. Another array maintains interpretations of encodings. The
+following lemma states that these two relates:
+
+```coq
+Lemma t_interp_wf : forall i,
+   t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]).
+```
+
+
+
+
+### [Misc.v](../src/Misc.v)
+
+This module contains miscellaneous general lemmas that are used in several
+places throughout the development of SMTCoq.
+
+
+### [versions](../src/versions)
+
+This directory contains everything that is dependent on the version of Coq that
+one wants to use. `standard` contains libraries for the standard version of Coq
+and `native` contains everything related to native Coq. Note that some
+libraries are already present in the default libraries of native Coq, in this
+case they have a counterpart in `standard` that replicates the functionality
+(without using native integers or native arrays).
+
+A particular point of interest is the files
+[smtcoq_plugin_standard.ml4](../src/versions/standard/smtcoq_plugin_standard.ml4)
+and
+[smtcoq_plugin_native.ml4](../src/versions/native/smtcoq_plugin_native.ml4). They
+provide extension points for Coq by defining new vernacular commands and new
+tactics. For instance the tactic `verit` tells Coq to call the OCaml function
+`verit.tactic` (which in turns uses the Coq API to manipulate the goals and
+call the certified checkers).
+
+```ocaml
+TACTIC EXTEND Tactic_verit
+| [ "verit" ] -> [ Verit.tactic () ]
+END
+```
+
+
+
+### [spl](../src/spl)
+
+This directory contains everything related to simplifications of input
+formulas as well as the Coq machinery to handle step checkers that use
+assumptions (and generate sub-goals).
+
+- [Arithmetic.v](../src/spl/Arithmetic.v): Arithmetic simplifications
+- [Operators.v](../src/spl/Operators.v): Simplifications of SMT-LIB 2 operators
+  (atomic disequalities and distinct operators)
+- [Syntactic.v](../src/spl/Syntactic.v): Flattening and normalization of
+  propositional structures
+- [Assumptions.v](../src/spl/Assumptions.v): Small checker for assumptions
+
+
+
+### [extraction](../src/extraction)
+
+This is the extracted version of the SMTCoq checker, that can be run outside
+Coq. It still needs to be fixed for the new additions and extensions.
+
+
+
+### [classes](../src/classes)
+
+
+The definitions of interpretations of terms and types of SMTCoq requires some
+additional constraints that are encoded as Coq type-classes. This directory
+contains definitions and properties of these classes
+[SMT_classes.v](../src/classes/SMT_classes.v) as well as predefined useful
+instances of these classes
+[SMT_classes_instances.v](../src/classes/SMT_classes_instances.v).
+
+These classes are:
+
+- `EqbType`: types with a Boolean equality that reflects in Leibniz equality
+- `DecType`: types with a decidable equality
+- `OrdType`: class of types with a partial order 
+- `Comparable`: augmentation of class of partial order with a compare function
+  to obtain a total order
+- `Inhabited`: class of inhabited types (used to obtain default values for
+  types)
+- `CompDec`: a class that merges all previous classes
+
+
+
+## Small checkers
+
+Small Coq checkers are organized in sub-directories that reflect the theories
+they handle. Small checkers for propositional logic, equality over
+uninterpreted functions and linear integer arithmetic all use preexisting
+standard Coq libraries (Bool, Arith, Z, BinPos, ...) to formalize the
+underlying interpretation of these theories. The theories of fixed-width
+bit-vectors and functional unbounded arrays are formalized in new custom Coq
+libraries (that are distributed with SMTCoq).
+
+
+Computational small checkers have the following signature:
+
+```coq
+Definition checker (s : S.t) (p1 ... pn : int) (l1 ... lm : lit) : C.t := ...
+```
+
+where `s` is the state of the main checker, `p1`, ..., `pn` are positions
+(there can be none) of deduced clauses that appear in the state `s` and `l1`,
+..., `lm` are literals. The function `checker` returns a clause that is
+`deducible` from the already deduced clauses in the state `s`.
+
+Correctness of checkers are specified (and proven) through lemmas of the form:
+
+```coq
+Lemma valid_checker : forall s rho p1 ... pm l1 ... lm,
+                      C.valid rho (checker s p1 ... pm l1 ... lm).
+```
+
+It states that the clause returned by `checker` is valid. In most cases for the
+small checkers, when they fail they return a trivially true clause (`C._true`).
+
+
+### [cnf](../src/cnf)
+
+Small checkers for CNF (conjunctive normal form) are defined in the module
+[Cnf.v](../src/cnf/Cnf.v). In essence they implement a Tseitin conversion.
+
+For instance, the checker `check_BuildDef` returns a tautology in clausal form
+(the validity of the clause is not dependent on the validity of the state) and
+the checker `check_ImmBuildDef` is a generic encoding of conversion rules that
+have a premise (which appears in the state).
+
+
+
+### [euf](../src/euf)
+
+The checkers for EUF (equality over uninterpreted functions) are defined in the
+module [Euf.v](../src/euf/Euf.v).
+
+The first one checks application of the rule of transitivity. `check_trans`
+takes as argument the result of the rule application as well as list of
+equalities of the form `a = b`, `b = c`, ..., `x = y`, `y = z`.
+
+The other checker takes care of applications of the congruence rule. Functions
+in SMT-LIB have a given arity and they are interpreted as Coq functions. The
+checker for congruence can check rule applications with a number of equalities
+corresponding to the arity of the function.
+
+
+### [lia](../src/lia)
+
+Checking linear arithmetic lemmas that come from the SMT solver is performed
+using the already existing `Micromega` solver of Coq. The corresponding
+checker is implemented in module [Lia.v](../src/lia/Lia.v).
+
+
+
+
+
+### [bva](../src/bva)
+
+The small checkers for bit-vector operations can be found in module
+[Bva_checker.v](../src/bva/Bva_checker.v). They implement the rules for
+bit-blasting operators of the theory of fixed width bit-vector.
+
+There are small checkers for:
+
+- bit-wise operators (`bvand`, `bvor`, `bvxor`, `bvnot`)
+- equality
+- variables
+- constants
+- extraction
+- concatenation
+- arithmetic operations (addition, negation, multiplication)
+- comparison predicates (signed/unsigned)
+- extensions (zero/signed)
+
+
+The theory of fixed width is realized by an implementation provided in
+[BVList.v](../src/bva/BVList.v). There, bit-vectors are interpreted by lists of
+Booleans. The type of bit-vectors is a dependent type:
+
+```coq
+Parameter bitvector : N -> Type.
+```
+
+In the implementation, a bit-vector is a record that contains a list of
+Booleans `bv`, *i.e.* the lists of its bits, as well as a proof of well
+formedness `wf`, *i.e.* a proof that the size of the list `bv` is the parameter
+`n` of the type.
+
+```coq
+Record bitvector_ (n:N) : Type :=
+    MkBitvector
+      { bv :> M.bitvector;
+        wf : M.size bv = n
+      }.
+```
+
+
+
+### [array](../src/array)
+
+The theory of unbounded functional arrays with extensionality is realized in
+Coq by a custom type that can be found in [FArray.v](../src/array/FArray.v).
+
+```coq
+Definition farray (key elt : Type) _ _  :=
+```
+
+The type `farray` is parameterized by the type of keys (or indexes) of the
+array and the type of the elements. `key` must be a type equipped with a
+partial order and `elt` must be inhabited. 
+
+
+```coq
+Record slist :=
+  {this :> Raw.farray key elt;
+   sorted : sort (Raw.ltk key_ord) this;
+   nodefault : NoDefault this
+   }.
+   
+Definition farray := slist.
+```
+
+An array is represented internally by an association list for its mappings with
+additional constraints that encode the fact that the list is sorted and that
+there are no mapping to the default value.
+
+Computable equality and comparison functions require additional constraints on
+the types `key` and `elt` (for instance they need to have a total order,
+*etc.*).
+
+This library also provides useful properties on these arrays. Notably
+extensionality which is required by the theory of arrays in SMT solvers:
+
+```coq
+Lemma extensionnality : forall a b, (forall i, select a i = select b i) -> a = b.
+```
+
+The extensionality rule that is used by the checker is a bit different and
+requires classical axioms to be proven. This is done in section
+```Classical_extensionnality``` which provides an alternative version without
+contaminating uses of the library.
+
+There are three small checkers for arrays. They check application of the axioms
+(in the theory sense) of the theory of arrays, two for *read over write* and
+one for *extensionality*
+
+
+## OCaml implementation of the plugin
+
+Part of SMTCoq is implemented in OCaml. These concern functionality which are
+not certified such as the reification mechanism, the parsers, pre-processors
+and the definitions of tactics.
+
+This part communicates directly with Coq by using the OCaml Coq API.
+
+
+### [trace](../src/trace)
+
+This directory contain the implementation of certificates and the
+representation of SMT-LIB formulas in SMTCoq.
+
+[coqTerms.ml](../src/trace/coqTerms.ml) contains imports from Coq of terms to
+be used directly in OCaml. These include usual Coq terms but also ones specific
+to SMTCoq.
+
+[smtAtom.mli](../src/trace/smtAtom.mli) contains the definitions for the types
+of atoms in SMTCoq but also provides smart constructors for them. The modules
+defined in this file have functions to reify Coq terms in OCaml and to
+translate back OCaml atoms and types to their Coq counterpart interpretation.
+
+[smtForm.mli](../src/trace/smtForm.mli) plays the same role as `smtAtom` but on
+the level of formulas.
+
+[smtCertif.ml](../src/trace/smtCertif.ml) contains definitions for an OCaml
+version of the steps of the certificate. These are the objects that are
+constructed when importing a certificate from an SMT solver for instance.
+
+[smtTrace.ml](../src/trace/smtTrace.ml) contains functions to build the Coq
+version of the certificate from the OCaml one.
+
+[smtCommands.ml](../src/trace/smtCommands.ml) constitute the bulk of the
+implementation of the plugin. It contains the OCaml functions that are used to
+build the Coq vernacular commands (`Verit_checker`, `Lfsc_checker`, ...) and
+the tactics. It also contains functions to reconstruct Coq counter-examples
+from models returned by the SMT solver.
+
+[smtCnf.ml](../src/trace/smtCnf.ml) implements a CNF conversion on the type of
+SMTCoq formulas.
+
+[smtMisc.ml](../src/trace/smtMisc.ml) contains miscellaneous functions used in
+the previous modules.
+
+
+
+### [smtlib2](../src/smtlib2)
+
+This directory contains utilities to communicate directly with SMT
+solvers. This includes a lexer/parser for the SMT-LIB 2 format
+([smtlib2_parse.mly](../src/smtlib2/smtlib2_parse.mly)) a conversion module
+from SMT-LIB 2 to formulas and atoms of SMTCoq
+([smtlib2_genConstr.ml](../src/smtlib2/smtlib2_genConstr.ml)) and a way to call
+and communicate with SMT solvers through pipes
+([smtlib2_solver.mli](../src/smtlib2/smtlib2_solver.mli)).
+
+
+
+### [zchaff](../src/zchaff)
+
+Files in this directory allow to call the SAT solver ZChaff. It contains a
+parser for the sat solver input files and ZChaff certificates. The
+implementation for the Coq tactic `zchaff` can be found in
+[zchaff.ml](../src/zchaff/zchaff.ml).
+
+
+
+### [verit](../src/verit)
+
+This directory contains the necessary modules to support the SMT solver veriT.
+In particular it contains a parser for the format of certificates of veriT
+([veritParser.mly](../src/verit/veritParser.mly)) and an intermediate
+representation of those certificates
+([veritSyntax.mli](../src/verit/veritSyntax.mli)). This module also implements
+a conversion function from veriT certificates to SMTCoq format of
+certificates. This pre-processor is a simple one-to-one conversion.
+
+The file ([verit.ml](../src/verit/verit.ml)) contains the functions to invoke
+veritT and create SMT-LIB 2 scripts. This is used by the definition of the
+tactic `verit` of the same file.
+
+
+
+### [lfsc](../src/lfsc)
+
+This directory contains the pre-processor for LFSC proofs to SMTCoq
+certificates (as well as veriT certificates). The files
+[ast.ml](../src/lfsc/ast.ml) and [builtin.ml](../src/lfsc/builtin.ml) contain
+an OCaml implementation of a type checker for LFSC proofs. This directory also
+contains a parser and lexer for LFSC (*c.f.*,
+[lfscParser.mly](../src/lfsc/lfscParser.mly)).
+
+The pre-processor is implemented in the module
+[converter.ml](../src/lfsc/converter.ml)) as a *functor*. Depending on the
+module (for terms and clauses conversions) that is passed in the functor
+application, we obtain either a pre-processor from LFSC proofs to SMTCoq
+certificates directly or a converter from LFSC proofs to veriT certificates.
+
+> **Note:** You can obtain a standalone version of the converter by issuing
+> `make` in this directory. This produces a binary `lfsctosmtcoq.native` that
+> can be run with an LFSC proof as argument and produces a veriT certificate
+> on the standard output.
+
+Finally, the tactic `cvc4_bool` is implemented in the file
+[lfsc.ml](../src/lfsc/lfsc.ml)). It contains functions to call the SMT solver
+CVC4, convert its proof and call the base tactic of `smtCommands`.
+
+
+## Tactics: proof search
+
+### [BoolToProp.v](../src/BoolToProp.v)
+This module includes the tactic `bool2prop` that converts a goal, if Boolean, into
+a goal in Coq's `Prop`, after introducing universally quantified variables into the
+context. 
+
+It simply performs a search in the goal and does the mentioned conversion step by step
+benefitting the `reflect` predicate popularized by the `SSReflect` library:
+
+```coq
+Inductive reflect (P : Prop) : bool -> Set :=
+   | ReflectT :   P -> reflect P true 
+   | ReflectF : ~ P -> reflect P false.
+```
+
+In fact, the predicate `reflect` returns the Boolean counterpart of a proposition.
+Besides, it makes below lemma easily provable:
+
+```coq
+Lemma reflect_iff : forall P b, (P<->b=true) -> reflect P b.
+```
+
+This simply says that if a Coq proposition `P` is equivalent to some Boolean 
+`b` being `true` then `b` is indeed the Boolean counterpart of `P`.
+
+Now, let's exemplify how the tactic `bool2prop` benefits above steps:
+
+Imagine a very simple goal that embodies the `or` connective
+
+```coq
+G0 || G1
+```
+
+for some Booleans `G0` and `G1`. Then, the tactic performes the following 
+rewrite step on the goal 
+
+```coq
+rewrite <- (@reflect_iff (G0 = true \/ G1 = true) (G0 || G1)).
+```
+
+which turns it into:
+
+```coq
+G0 = true \/ G1 = true
+```
+
+together with introducing an additional goal:
+
+```coq
+reflect (G0 = true \/ G1 = true) (G0 || G1)
+```
+
+The first goal is indeed the intended one. However, the tactic can still go a step further 
+putting the goal into the following shape:
+
+```coq
+H0 \/ H1
+```
+
+for some propositions `H0` and `H1`. This is indeed the case for Boolean equality and comparison over bit-vectors,
+Boolean equality and  comparison over Coq intergers `Z`, and Boolean equality over fuctional arrays;
+since the corresponding propositional predicates are proven to be equivalent. E.g., 
+
+```coq
+Lemma bv_ult_B2P: forall n (a b: bitvector n), bv_ult a b = true <-> bv_ultP a b.
+```
+where `bv_ult: bitvector n -> bitvector n -> bool` and `bv_ultP: bitvector n -> bitvector n -> Prop`. 
+
+However, the second one must somehow be solved. This is indeed not so hard:
+it suffices to apply the below lemma which has already been proven again by benefitting the `reflect` predicate:
+
+
+```coq
+Lemma orP : forall (a b: bool), reflect (a = true \/ b = true) (a || b).
+```
+
+Notice that the same sort of conversion steps for the other Boolean connectives are also handled
+by the tactic `bool2prop`.
+
+### [PropToBool.v](../src/PropToBool.v)
+This module includes the tactic `prop2bool` that converts a goal, if in Coq's `Prop`, into
+a Boolean goal, after introducing universally quantified variables into the context.
+It is, in fact, the inverse of the above explained `bool2prop` tactic.
+
+It simply performs a search in the goal and does the mentioned conversion step by step
+benefitting the `reflect` predicate (see above `BoolToProp.v`). The predicate `reflect`
+makes the following goal easily proveable:
+
+```coq
+Lemma reflect_iff : forall P b, reflect P b -> (P<->b=true).
+```
+
+This basically tells us that if `b` is the Boolean counterpart of some proposition `P`,
+then `P` is indeed equivalent to `b` being `true`.
+
+Now, let's exemplify how the tactic `prop2bool` benefits above steps:
+
+Imagine a very simple goal that embodies the `or` connective as
+
+```coq
+H0 \/ H1
+```
+
+for some propositions `H0` and `H1`. At this point, the tactic needs to go a step further and
+puts the goal into the following shape to be able to make use of the `reflect_iff` fact:
+
+```coq
+G0 = true \/ G1 = true
+```
+
+for some Booleans `G0` and `G1`. This step is indeed doable for propositional equality and comparison over
+bit-vectors, propsitional equality and comparison over Coq intergers `Z`, and propositional equality over
+fuctional arrays, since the corresponding Boolean predicates are proven to be equivalent. E.g.,
+
+```coq
+Lemma bv_ult_B2P: forall n (a b: bitvector n), bv_ult a b = true <-> bv_ultP a b.
+```
+where `bv_ult: bitvector n -> bitvector n -> bool` and `bv_ultP: bitvector n -> bitvector n -> Prop`.
+
+
+Then, the tactic performes the following rewrite step on the goal 
+
+```coq
+rewrite (@reflect_iff (G0 = true \/ G1 = true) (G0 || G1))
+```
+
+which turns it into:
+
+```coq
+G0 || G1 = true
+```
+
+together with introducing an additional goal:
+
+```coq
+reflect (G0 = true \/ G1 = true) (G0 || G1)
+```
+
+The first goal is indeed the intended one. So that the tactic leaves the goal as it is. But the second
+one must somehow be solved. In fact, this not so hard: it suffices to apply the below lemma which
+has already been proven again by benefitting the `reflect` predicate:
+
+```coq
+Lemma orP : forall (a b: bool), reflect (a = true \/ b = true) (a || b).
+```
+
+Notice that the same sort of conversion steps for the other propositional connectives are also handled
+by the tactic `prop2bool`.
+
+### [Tactics.v](../src/Tactics.v)
+This file includes four tactics that are written in `Ltac` language:
+
+ - `zchaff` -> can function on the goals in Coq's `Prop`: 
+ first calls `prop2bool` on the goal, getting the goal in `bool`, 
+ then calls the reificiation tactic `zchaff_bool` (which can only function on Boolean goals),
+ and finally puts the goal back in Coq's `Prop`, by calling `bool2prop`, if not solved.
+ 
+ - `verit` -> can function on the goals in Coq's `Prop`: 
+ first calls `prop2bool` on the goal, getting the goal in `bool`, 
+ then calls the reificiation tactic `verit_bool` (can only function on Boolean goals),
+ and finally puts the goal back in Coq's `Prop`, by calling `bool2prop`, if not solved.
+ 
+ - `cvc4` -> can function on the goals in Coq's `Prop`: 
+ first calls `prop2bool` on the goal, getting the goal in `bool`, 
+ then calls the reificiation tactic `cvc4_bool` (can only function on Boolean goals),
+ and finally puts the goal(s) back in Coq's `Prop`, by calling `bool2prop`, in case it is not solved or additional goals returned.
+ 
+ - `smt` -> subsumes the powers of `cvc4` and `verit` tactics: 
+ first calls `prop2bool` on the goal, getting the goal in `bool`, 
+ then calls either of the reificiation tactics `cvc4_bool`, `verit_bool` (can only function on Boolean goals),
+ and finally puts the goal(s) back in Coq's `Prop`, by calling `bool2prop`, in case it is not solved or additional goals returned.
+
+
+
+