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, 297 insertions, 0 deletions

diff --git a/src/smtlib2/sExprLexer.mll b/src/smtlib2/sExprLexer.mll
new file mode 100644
index 0000000..6d0cd22
--- /dev/null
+++ b/src/smtlib2/sExprLexer.mll
@@ -0,0 +1,297 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+(* Lexer for S-expressions
+   
+   Adapted from the OCaml sexplib, which is part of the ocaml-core
+   alternative standard library for OCaml.
+
+*)
+
+{
+  (** Lexer: Lexer Specification for S-expressions *)
+
+  open Printf
+  open Lexing
+  open SExprParser
+
+  let char_for_backslash = function
+    | 'n' -> '\010'
+    | 'r' -> '\013'
+    | 'b' -> '\008'
+    | 't' -> '\009'
+    | c -> c
+
+  let lf = '\010'
+
+  let dec_code c1 c2 c3 =
+    100 * (Char.code c1 - 48) + 10 * (Char.code c2 - 48) + (Char.code c3 - 48)
+
+  let hex_code c1 c2 =
+    let d1 = Char.code c1 in
+    let val1 =
+      if d1 >= 97 then d1 - 87
+      else if d1 >= 65 then d1 - 55
+      else d1 - 48 in
+    let d2 = Char.code c2 in
+    let val2 =
+      if d2 >= 97 then d2 - 87
+      else if d2 >= 65 then d2 - 55
+      else d2 - 48 in
+    val1 * 16 + val2
+
+  let found_newline ({ lex_curr_p; _ } as lexbuf) diff =
+    lexbuf.lex_curr_p <-
+      {
+        lex_curr_p with
+        pos_lnum = lex_curr_p.pos_lnum + 1;
+        pos_bol = lex_curr_p.pos_cnum - diff;
+      }
+
+  (* same length computation as in [Lexing.lexeme] *)
+  let lexeme_len { lex_start_pos; lex_curr_pos; _ } = lex_curr_pos - lex_start_pos
+
+  let main_failure lexbuf msg =
+    let { pos_lnum; pos_bol; pos_cnum; pos_fname = _ } = lexeme_start_p lexbuf in
+    let msg =
+      sprintf
+        "Sexplib.Lexer.main: %s at line %d char %d"
+        msg pos_lnum (pos_cnum - pos_bol)
+    in
+    failwith msg
+}
+
+let lf = '\010'
+let lf_cr = ['\010' '\013']
+let dos_newline = "\013\010"
+let blank = [' ' '\009' '\012']
+let unquoted = [^ ';' '(' ')' '"'] # blank # lf_cr
+let digit = ['0'-'9']
+let hexdigit = digit | ['a'-'f' 'A'-'F']
+
+let unquoted_start =
+  unquoted # ['#' '|'] | '#' unquoted # ['|'] | '|' unquoted # ['#']
+
+rule main buf = parse
+  | lf | dos_newline { found_newline lexbuf 0; main buf lexbuf }
+  | blank+ | ';' (_ # lf_cr)* { main buf lexbuf }
+  | '(' { LPAREN }
+  | ')' { RPAREN }
+  | '"'
+      {
+        scan_string buf (lexeme_start_p lexbuf) lexbuf;
+        let str = Buffer.contents buf in
+        Buffer.clear buf;
+        STRING str
+      }
+  | "#;" { HASH_SEMI }
+  | "#|"
+      {
+        scan_block_comment buf [lexeme_start_p lexbuf] lexbuf;
+        main buf lexbuf
+      }
+  | "|#" { main_failure lexbuf "illegal end of comment" }
+  | '|'
+    {
+      scan_quoted buf (lexeme_start_p lexbuf) lexbuf;
+      let str = Buffer.contents buf in
+      Buffer.clear buf;
+      STRING ("|"^ str ^"|")
+    }
+  | unquoted_start unquoted* ("#|" | "|#") unquoted*
+      { main_failure lexbuf "comment tokens in unquoted atom" }
+  | "#" | unquoted_start unquoted* as str { STRING str }
+  | eof { EOF }
+
+and scan_string buf start = parse
+  | '"' { () }
+  | '\\' lf [' ' '\t']*
+      {
+        found_newline lexbuf (lexeme_len lexbuf - 2);
+        scan_string buf start lexbuf
+      }
+  | '\\' dos_newline [' ' '\t']*
+      {
+        found_newline lexbuf (lexeme_len lexbuf - 3);
+        scan_string buf start lexbuf
+      }
+  | '\\' (['\\' '\'' '"' 'n' 't' 'b' 'r' ' '] as c)
+      {
+        Buffer.add_char buf (char_for_backslash c);
+        scan_string buf start lexbuf
+      }
+  | '\\' (digit as c1) (digit as c2) (digit as c3)
+      {
+        let v = dec_code c1 c2 c3 in
+        if v > 255 then (
+          let { pos_lnum; pos_bol; pos_cnum; _ } = lexeme_end_p lexbuf in
+          let msg =
+            sprintf
+              "Sexplib.Lexer.scan_string: \
+               illegal escape at line %d char %d: `\\%c%c%c'"
+              pos_lnum (pos_cnum - pos_bol - 3)
+              c1 c2 c3 in
+          failwith msg);
+        Buffer.add_char buf (Char.chr v);
+        scan_string buf start lexbuf
+      }
+  | '\\' 'x' (hexdigit as c1) (hexdigit as c2)
+      {
+        let v = hex_code c1 c2 in
+        Buffer.add_char buf (Char.chr v);
+        scan_string buf start lexbuf
+      }
+  | '\\' (_ as c)
+      {
+        Buffer.add_char buf '\\';
+        Buffer.add_char buf c;
+        scan_string buf start lexbuf
+      }
+  | lf
+      {
+        found_newline lexbuf 0;
+        Buffer.add_char buf lf;
+        scan_string buf start lexbuf
+      }
+  | ([^ '\\' '"'] # lf)+
+      {
+        Buffer.add_string buf (lexeme lexbuf);
+        scan_string buf start lexbuf
+      }
+  | eof
+      {
+        let msg =
+          sprintf
+            "Sexplib.Lexer.scan_string: unterminated string at line %d char %d"
+            start.pos_lnum (start.pos_cnum - start.pos_bol)
+        in
+        failwith msg
+      }
+
+and scan_quoted buf start = parse
+  | '|' { () }
+  | '\\' lf [' ' '\t']*
+      {
+        found_newline lexbuf (lexeme_len lexbuf - 2);
+        scan_quoted buf start lexbuf
+      }
+  | '\\' dos_newline [' ' '\t']*
+      {
+        found_newline lexbuf (lexeme_len lexbuf - 3);
+        scan_quoted buf start lexbuf
+      }
+  | '\\' (['\\' '\'' '"' 'n' 't' 'b' 'r' ' ' '|'] as c)
+      {
+        Buffer.add_char buf (char_for_backslash c);
+        scan_quoted buf start lexbuf
+      }
+  | '\\' (digit as c1) (digit as c2) (digit as c3)
+      {
+        let v = dec_code c1 c2 c3 in
+        if v > 255 then (
+          let { pos_lnum; pos_bol; pos_cnum; _ } = lexeme_end_p lexbuf in
+          let msg =
+            sprintf
+              "Sexplib.Lexer.scan_quoted: \
+               illegal escape at line %d char %d: `\\%c%c%c'"
+              pos_lnum (pos_cnum - pos_bol - 3)
+              c1 c2 c3 in
+          failwith msg);
+        Buffer.add_char buf (Char.chr v);
+        scan_quoted buf start lexbuf
+      }
+  | '\\' 'x' (hexdigit as c1) (hexdigit as c2)
+      {
+        let v = hex_code c1 c2 in
+        Buffer.add_char buf (Char.chr v);
+        scan_quoted buf start lexbuf
+      }
+  | '\\' (_ as c)
+      {
+        Buffer.add_char buf '\\';
+        Buffer.add_char buf c;
+        scan_quoted buf start lexbuf
+      }
+  | lf
+      {
+        found_newline lexbuf 0;
+        Buffer.add_char buf lf;
+        scan_quoted buf start lexbuf
+      }
+  | ([^ '\\' '|'] # lf)+
+      {
+        Buffer.add_string buf (lexeme lexbuf);
+        scan_quoted buf start lexbuf
+      }
+  | eof
+      {
+        let msg =
+          sprintf
+            "Sexplib.Lexer.scan_quoted: unterminated ident at line %d char %d"
+            start.pos_lnum (start.pos_cnum - start.pos_bol)
+        in
+        failwith msg
+      }
+
+and scan_block_comment buf locs = parse
+  | ('#'* | '|'*) lf
+      { found_newline lexbuf 0; scan_block_comment buf locs lexbuf }
+  | (('#'* | '|'*) [^ '"' '#' '|'] # lf)+ { scan_block_comment buf locs lexbuf }
+  | ('#'* | '|'*) '"'
+      {
+        let cur = lexeme_end_p lexbuf in
+        let start = { cur with pos_cnum = cur.pos_cnum - 1 } in
+        scan_string buf start lexbuf;
+        Buffer.clear buf;
+        scan_block_comment buf locs lexbuf
+      }
+  | '#'+ '|'
+    {
+      let cur = lexeme_end_p lexbuf in
+      let start = { cur with pos_cnum = cur.pos_cnum - 2 } in
+      scan_block_comment buf (start :: locs) lexbuf
+    }
+  | '|'+ '#'
+      {
+        match locs with
+        | [_] -> ()
+        | _ :: t -> scan_block_comment buf t lexbuf
+        | [] -> assert false  (* impossible *)
+      }
+  | eof
+      {
+        match locs with
+        | [] -> assert false
+        | { pos_lnum; pos_bol; pos_cnum; _ } :: _ ->
+            let msg =
+              sprintf "Sexplib.Lexer.scan_block_comment: \
+                unterminated block comment at line %d char %d"
+                pos_lnum (pos_cnum - pos_bol)
+            in
+            failwith msg
+      }
+
+and ruleTail acc = parse
+  | eof { acc }
+  | _* as str { ruleTail (acc ^ str) lexbuf }
+
+  
+{
+  let main ?buf =
+    let buf =
+      match buf with
+      | None -> Buffer.create 64
+      | Some buf -> Buffer.clear buf; buf
+    in
+    main buf
+}
+