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

1 files changed, 162 insertions, 25 deletions

diff --git a/INSTALL.md b/INSTALL.md
index c578b83..0eac582 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -4,42 +4,109 @@
 
 SMTCoq is designed to work on computers equipped with a POSIX (Unix or a
 clone) operating system. It is known to work under GNU/Linux (i386 and
-amd64).
+amd64) and Mac OS X.
 
-You can install it from the sources, using two different versions
-  of Coq (depending on the efficiency you want).
-In either case, you will also need to install the provers you want to
-use (see below).
+For now you have to install it from the sources. (We plan on releasing
+an updated opam package soon with the latest additions.)
 
+You will also need to [install the provers](#installation-of-the-provers)
+you want to use and make some [small configuration
+changes](#setting-up-environment-for-smtcoq).
 
-## Installation from the sources (uses Coq-8.6 or native-coq)
+## Requirements
 
-You can also build SMTCoq from the sources, using either Coq 8.6 or the
-[version of Coq with native data-structures](https://github.com/smtcoq/native-coq).
-We recommend Coq 8.6 for standard use, and native-coq for uses that
-require very efficient computation (such as checking big certificates).
+You need to have OCaml version >= 4.04.0 and Coq version 8.6 or 8.6.1.
+The easiest way to install these two pieces of software is through opam.
 
+> **Warning**: The version of Coq that you plan to use must have been compiled
+> with the same version of OCaml that you are going to use to compile
+> SMTCoq. In particular this means you want a version of Coq that was compiled
+> with OCaml version >= 4.04.0.
 
-### Installation with Coq 8.6
+If you want to use SMTCoq with high performance, you need to use the
+[version of Coq with native
+data-structures](https://github.com/smtcoq/native-coq) instead of
+Coq-8.6.
 
-It requires OCaml between versions 4.02 and 4.05 (included). OCaml
-4.04.0 is reported to work with Coq 8.6.1 and SMTCoq df1a51d.
 
-1. Download the last stable version of Coq 8.6:
+### Installation with Coq and OCaml opam packages
+
+#### Install opam
+
+We recommended to install the required packages from
+[opam](https://opam.ocaml.org). Once you have installed opam on your system you
+should issue the following command:
+
+```bash
+opam init
+```
+
+which will initialize the opam installation and prompt for modifying the shell
+init file.
+
+Once opam is installed you should still issue
+
+```bash
+eval `opam config env`
 ```
+
+(this is not necessary if you start another session in your shell).
+
+#### Install OCaml
+
+Now you can install an OCaml compiler (we recommend 4.04.0 or the latest
+release):
+
+```bash
+opam switch 4.04.0
+```
+
+#### Install Coq
+
+After OCaml is installed, you can install Coq through opam (we recommend 8.6.1).
+
+```bash
+opam install coq.8.6.1
+```
+
+If you also want to install CoqIDE at the same time you can do
+
+```bash
+opam install coq.8.6.1 coqide.8.6.1
+```
+
+but you might need to install some extra packages and libraries for your system
+(such as GTK2, gtksourceview2, etc.).
+
+
+#### Install SMTCoq
+
+Compile and install SMTCoq by using the following commands in the src directory.
+
+```bash
+./configure.sh
+make
+make install
+```
+
+
+### Installation with official Coq 8.6 release
+
+1. Download the last stable version of Coq 8.6:
+```bash
 wget https://coq.inria.fr/distrib/8.6.1/files/coq-8.6.1.tar.gz
 ```
    and compile it by following the instructions available in the
-   repository. We recommand that you do not install it, but only compile
-   it in local:
-```
+   repository (make sure you use OCaml 4.04.0 for that). We recommand
+   that you do not install it, but only compile it in local:
+```bash
 ./configure -local
 make
 ```
 
 2. Set an environment variable COQBIN to the directory where Coq's
    binaries are; for instance:
-```
+```bash
 export COQBIN=/home/jdoe/coq-8.6.1/bin/
 ```
    (the final slash is mandatory).
@@ -50,25 +117,26 @@ export COQBIN=/home/jdoe/coq-8.6.1/bin/
 make
 make install
 ```
+```
 
 
 ### Installation with native-coq
 
 1. Download the git version of Coq with native compilation:
-```
+```bash
 git clone https://github.com/smtcoq/native-coq.git
 ```
    and compile it by following the instructions available in the
    repository. We recommand that you do not install it, but only compile
    it in local:
-```
+```bash
 ./configure -local
 make
 ```
 
 2. Set an environment variable COQBIN to the directory where Coq's
    binaries are; for instance:
-```
+```bash
 export COQBIN=/home/jdoe/native-coq/bin/
 ```
    (the final slash is mandatory).
@@ -81,16 +149,15 @@ make install
 ```
 
 
-## Deprecated: installation via opam (uses Coq-8.5)
+### Deprecated: installation via opam (uses Coq-8.5)
 
 Simply add the coq-extra-dev repo to opam:
-```
+```bash
 opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
 ```
 and install smtcoq:
-```
+```bash
 opam install coq-smtcoq
-```
 
 
 ## Installation of the provers
@@ -102,12 +169,24 @@ Currently, these solvers are:
 
 - [zChaff](http://www.princeton.edu/~chaff/zchaff.html)
 
+- [CVC4](http://cvc4.cs.nyu.edu)
+
 Please download the solvers you would like to use via the above links
 (since SMTCoq might not support other versions), and follow the
 instructions available for each solver in order to compile them **in a
 proof production mode**, as detailed below.
 
 
+### CVC4
+
+Use the version of CVC4 that is available in the master branch of its
+[git repository](https://github.com/CVC4/CVC4) or one of the **development**
+versions available at [http://cvc4.cs.stanford.edu/downloads] (we recommend using
+the latest version available).
+
+The `cvc4` binary must be present in your PATH to use it through SMTCoq.
+
+
 ### veriT
 
 The
@@ -135,3 +214,61 @@ please report an issue.
 
 To turn proof production on, you need to uncomment the line
 `// #define VERIFY_ON ` in `zchaff_solver.cpp`.
+
+The `zchaff` binary must be present in your PATH to use it through SMTCoq.
+
+
+## Setting up environment for SMTCoq
+
+To use the latest features of SMTCoq, you need to make these configuration
+changes:
+
+In your `.bashrc` (or `.bash_profile`, or any other initialization file read by
+your shell), export the following environment variable to make it point at the
+`signatures` directory distributed with SMTCoq.
+
+> Don't use `~` in the path but rather `$HOME`.
+
+```bash
+export LFSCSIGS="$HOME/path/to/smtcoq/src/lfsc/tests/signatures/"
+```
+
+If you don't want SMTCoq to spit the translated proof in your proof environment
+window, add the following optional definition (in the same file).
+
+```bash
+export DONTSHOWVERIT="yes"
+```
+
+### Using SMTCoq without installing
+
+If you want to use SMTCoq without installing it your Coq installation, you can
+tell Coq where to find SMTCoq by adding the following line in the file
+`~/.config/coqrc`:
+
+```coq
+Add Rec LoadPath "~/path/to/smtcoq/src" as SMTCoq.
+```
+
+
+### Emacs and ProofGeneral
+
+If you use Emacs and ProofGeneral for Coq development, we recommend to use the
+package [exec-path-from-shell](https://github.com/purcell/exec-path-from-shell)
+(which can be installed with `M-x package-install exec-path-from-shell`) and to
+add the following in your `.emacs`:
+
+```elisp
+(exec-path-from-shell-initialize)
+```
+
+This will make emacs use the same environment as your shell. This is also
+particularly useful if you have installed Coq and OCaml from opam.
+
+
+### Warning about CoqIDE
+
+The latest versions of CoqIDE can now check Coq scripts in parallel. This
+feature is very useful but it seems SMTCoq doesn't work with it. This means
+that if you use any of the SMTCoq tactics or vernacular commands, we suggest to
+instruct CoqIDE to go through the script step-by-step.