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

diff --git a/src/lfsc/lfsc.ml b/src/lfsc/lfsc.ml
new file mode 100644
index 0000000..0f9fd8d
--- /dev/null
+++ b/src/lfsc/lfsc.ml
@@ -0,0 +1,506 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     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     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+open Format
+open Entries
+open Declare
+open Decl_kinds
+
+open SmtMisc
+open CoqTerms
+open SmtForm
+open SmtCertif
+open SmtTrace
+open SmtAtom
+
+
+(******************************************************************************)
+(* Given a lfsc trace build the corresponding certif and theorem             *)
+(******************************************************************************)
+
+(* Instantiate Converter with translator for SMTCoq *)
+module C = Converter.Make (Tosmtcoq)
+
+exception No_proof
+
+(* Hard coded signatures *)
+let signatures =
+  let sigdir = try Sys.getenv "LFSCSIGS" with Not_found -> Sys.getcwd () in
+  ["sat.plf";
+   "smt.plf";
+   "th_base.plf";
+   "th_int.plf";
+   "th_bv.plf";
+   "th_bv_bitblast.plf";
+   "th_bv_rewrites.plf";
+   "th_arrays.plf" ]
+  |> List.map (Filename.concat sigdir)
+
+
+let process_signatures_once =
+  let don = ref false in
+  fun () ->
+    if !don then ()
+    else
+      try
+        (* don := true; *)
+        List.iter (fun f ->
+            let chan = open_in f in
+            let lexbuf = Lexing.from_channel chan in
+            LfscParser.ignore_commands LfscLexer.main lexbuf;
+            close_in chan
+          ) signatures
+      with
+      | Ast.TypingError (t1, t2) ->
+        Structures.error
+          (asprintf "@[<hov>LFSC typing error: expected %a, got %a@]@."
+             Ast.print_term t1
+             Ast.print_term t2)
+
+
+let lfsc_parse_last lb =
+  printf "Type-checking LFSC proof...@?";
+  let t0 = Sys.time () in
+  let r = LfscParser.last_command LfscLexer.main lb in
+  let t1 = Sys.time () in
+  printf " Done [%.3f s]@." (t1 -. t0);
+  r
+
+let lfsc_parse_one lb =
+  printf "Type-checking LFSC proof...@?";
+  let t0 = Sys.time () in
+  let r = LfscParser.one_command LfscLexer.main lb in
+  let t1 = Sys.time () in
+  printf " Done [%.3f s]@." (t1 -. t0);
+  r
+  
+
+let import_trace first parse lexbuf =
+  Printexc.record_backtrace true;
+  process_signatures_once ();
+  try
+    match parse lexbuf with
+
+    | Some (Ast.Check p) ->
+      (* Ast.flatten_term p; *)
+      let confl_num = C.convert_pt p in
+      (* Afterwards, the SMTCoq libraries will produce the remaining, you do
+         not have to care *)
+      let first =
+        let aux = VeritSyntax.get_clause 1 in
+        match first, aux.value with
+        | Some (root,l), Some (fl::nil) ->
+          (* Format.eprintf "Root: %a ,,,,,,\n\ *)
+          (*                 input: %a@." *)
+          (*   (Form.to_smt Atom.to_smt) l (Form.to_smt Atom.to_smt) fl; *)
+          if Form.equal l fl then
+            aux
+          else (
+            (* eprintf "ADDING Flatten rule@."; *)
+            aux.kind <- Other (ImmFlatten(root,fl));
+            SmtTrace.link root aux;
+            root
+          )
+        | _,_ -> aux in
+      let confl = VeritSyntax.get_clause confl_num in
+      SmtTrace.select confl;
+      occur confl;
+      (alloc first, confl)
+
+    | _ -> raise No_proof
+
+  with
+  | Ast.TypingError (t1, t2) ->
+    Structures.error
+      (asprintf "@[<hov>LFSC typing error: expected %a, got %a@]@."
+         Ast.print_term t1
+         Ast.print_term t2)
+
+
+
+let import_trace_from_file first filename =
+  let chan = open_in filename in
+  let lexbuf = Lexing.from_channel chan in
+  let p = import_trace first lfsc_parse_last lexbuf in
+  close_in chan;
+  p
+
+
+
+let clear_all () =
+  SmtTrace.clear ();
+  VeritSyntax.clear ();
+  C.clear ()
+
+
+let import_all fsmt fproof =
+  clear_all ();
+  let rt = SmtBtype.create () in
+  let ro = Op.create () in
+  let ra = VeritSyntax.ra in
+  let rf = VeritSyntax.rf in
+  let roots = Smtlib2_genConstr.import_smtlib2 rt ro ra rf fsmt in
+  let (max_id, confl) = import_trace_from_file None fproof in
+  (rt, ro, ra, rf, roots, max_id, confl)
+
+
+let parse_certif t_i t_func t_atom t_form root used_root trace fsmt fproof =
+  SmtCommands.parse_certif t_i t_func t_atom t_form root used_root trace
+    (import_all fsmt fproof)
+
+let checker_debug fsmt fproof =
+  SmtCommands.checker_debug (import_all fsmt fproof)
+
+let theorem name fsmt fproof =
+  SmtCommands.theorem name (import_all fsmt fproof)
+
+let checker fsmt fproof =
+  SmtCommands.checker (import_all fsmt fproof)
+
+(* Same but print runtime *)
+let checker fsmt fproof =
+  let c = import_all fsmt fproof in
+  printf "Coq checker...@.";
+  let t0 = Sys.time () in
+  let r = SmtCommands.checker c in
+  let t1 = Sys.time () in
+  printf "Done (Coq) [%.3f s]@." (t1 -. t0);
+  r
+
+
+
+(******************************************************************************)
+(** Given a Coq formula build the proof                                       *)
+(******************************************************************************)
+
+
+(* module Form2 = struct *)
+(*   (\* Just for printing *\) *)
+
+(*   open Form *)
+
+(*   let rec to_smt atom_to_smt fmt f = *)
+(*     if is_pos f then to_smt_pform atom_to_smt fmt (pform f) *)
+(*     else fprintf fmt "(not %a)" (to_smt_pform atom_to_smt) (pform f) *)
+
+(*   and to_smt_pform atom_to_smt fmt = function *)
+(*     | Fatom a -> atom_to_smt fmt a *)
+(*     | Fapp (op,args) -> to_smt_op atom_to_smt op fmt (Array.to_list args) *)
+(*     | _ -> assert false *)
+
+(*   and to_smt_op atom_to_smt op fmt args = *)
+(*     match op, args with *)
+(*       | Ftrue, [] -> fprintf fmt "true" *)
+(*       | Ffalse, [] -> fprintf fmt "false" *)
+(*       | Fand, [x; y] -> *)
+(*         fprintf fmt "(and %a %a)" (to_smt atom_to_smt) x (to_smt atom_to_smt) y *)
+(*       | For, [x; y] -> *)
+(*         fprintf fmt "(or %a %a)" (to_smt atom_to_smt) x (to_smt atom_to_smt) y *)
+(*       | Fand, x :: rargs -> *)
+(*         fprintf fmt "(and %a %a)" (to_smt atom_to_smt) x *)
+(*           (to_smt_op atom_to_smt Fand) rargs *)
+(*       | For, x :: rargs -> *)
+(*         fprintf fmt "(or %a %a)" (to_smt atom_to_smt) x *)
+(*           (to_smt_op atom_to_smt For) rargs *)
+(*       (\* andb and orb are left-associative in Coq *\) *)
+(*       (\* | Fand, _ -> left_assoc atom_to_smt Fand fmt (List.rev args) *\) *)
+(*       (\* | For, _ -> left_assoc atom_to_smt For fmt (List.rev args) *\) *)
+(*       | Fxor, _ -> *)
+(*         fprintf fmt "(xor%a)" *)
+(*           (fun fmt -> List.iter (fprintf fmt " %a" (to_smt atom_to_smt))) args *)
+(*       | Fimp, _ -> *)
+(*         fprintf fmt "(=>%a)" *)
+(*           (fun fmt -> List.iter (fprintf fmt " %a" (to_smt atom_to_smt))) args *)
+(*       | Fiff, _ -> *)
+(*         fprintf fmt "(=%a)" *)
+(*           (fun fmt -> List.iter (fprintf fmt " %a" (to_smt atom_to_smt))) args *)
+(*       | Fite, _ -> *)
+(*         fprintf fmt "(ite%a)" *)
+(*           (fun fmt -> List.iter (fprintf fmt " %a" (to_smt atom_to_smt))) args *)
+(*       | Fnot2 _, _ -> *)
+(*         fprintf fmt "(not (not %a))" *)
+(*           (fun fmt -> List.iter (fprintf fmt " %a" (to_smt atom_to_smt))) args *)
+(*       | _ -> assert false *)
+
+(*   and left_assoc atom_to_smt op fmt args = *)
+(*     (\* args is reversed *\) *)
+(*     match op, args with *)
+(*     | Fand, [x; y] -> *)
+(*       fprintf fmt "(and %a %a)" (to_smt atom_to_smt) y (to_smt atom_to_smt) x *)
+(*     | For, [x; y] -> *)
+(*       fprintf fmt "(or %a %a)" (to_smt atom_to_smt) y (to_smt atom_to_smt) x *)
+(*     | Fand, last :: rargs -> *)
+(*       fprintf fmt "(and %a %a)" *)
+(*         (left_assoc atom_to_smt Fand) rargs (to_smt atom_to_smt) last *)
+(*     | For, last :: rargs -> *)
+(*       fprintf fmt "(or %a %a)" *)
+(*         (left_assoc atom_to_smt For) rargs (to_smt atom_to_smt) last *)
+(*     | _ -> assert false *)
+
+(* end *)
+
+
+(* module Atom2 = struct *)
+(*   (\* Just for printing *\) *)
+
+(*   open Atom *)
+  
+(*   let distrib x l = List.map (fun y -> (x,y)) l *)
+
+(*   let rec cross acc l = match l with *)
+(*     | [] | [_] -> List.rev acc *)
+(*     | x :: r -> *)
+(*       cross (List.rev_append (distrib x r) acc) r *)
+
+(*   let cross = cross [] *)
+  
+(*   let rec compute_int = function *)
+(*     | Acop c -> *)
+(*       (match c with *)
+(*        | CO_xH -> 1 *)
+(*        | CO_Z0 -> 0 *)
+(*        | CO_BV _ -> assert false) *)
+(*     | Auop (op,h) -> *)
+(*       (match op with *)
+(*        | UO_xO -> 2*(compute_hint h) *)
+(*        | UO_xI -> 2*(compute_hint h) + 1 *)
+(*        | UO_Zpos -> compute_hint h *)
+(*        | UO_Zneg -> - (compute_hint h) *)
+(*        | _ -> assert false) *)
+(*     | _ -> assert false *)
+
+(*   and compute_hint h = compute_int (atom h) *)
+
+(*   let to_smt_int fmt i = *)
+(*     let s1 = if i < 0 then "(- " else "" in *)
+(*     let s2 = if i < 0 then ")" else "" in *)
+(*     let j = if i < 0 then -i else i in *)
+(*     fprintf fmt "%s%i%s" s1 j s2 *)
+
+(*   let rec to_smt fmt h = to_smt_atom fmt (atom h) *)
+
+(*   and to_smt_atom fmt = function *)
+(*     | Acop _ as a -> to_smt_int fmt (compute_int a) *)
+(*     | Auop (UO_Zopp,h) -> *)
+(*       fprintf fmt "(- "; *)
+(*       to_smt fmt h; *)
+(*       fprintf fmt ")" *)
+(*     | Auop _ as a -> to_smt_int fmt (compute_int a) *)
+(*     | Abop (op,h1,h2) -> to_smt_bop fmt op h1 h2 *)
+(*     | Atop (op,h1,h2,h3) -> to_smt_bop fmt op h1 h2 h3 *)
+(*     | Anop (op,a) -> to_smt_nop fmt op a *)
+(*     | Aapp (op,a) -> *)
+(*       if Array.length a = 0 then ( *)
+(*         fprintf fmt "op_%i" (indexed_op_index op); *)
+(*       ) else ( *)
+(*         fprintf fmt "(op_%i" (indexed_op_index op); *)
+(*         Array.iter (fun h -> fprintf fmt " "; to_smt fmt h) a; *)
+(*         fprintf fmt ")" *)
+(*       ) *)
+
+(*   and str_op = function *)
+(*       | BO_Zplus -> "+" *)
+(*       | BO_Zminus -> "-" *)
+(*       | BO_Zmult -> "*" *)
+(*       | BO_Zlt -> "<" *)
+(*       | BO_Zle -> "<=" *)
+(*       | BO_Zge -> ">=" *)
+(*       | BO_Zgt -> ">" *)
+(*       | BO_eq _ -> "=" *)
+  
+(*   and to_smt_bop fmt op h1 h2 = *)
+(*     match op with *)
+(*     | BO_Zlt -> fprintf fmt "(not (>= %a %a)" to_smt h1 to_smt h2 *)
+(*     | BO_Zle -> fprintf fmt "(not (>= %a (+ %a 1))" to_smt h1 to_smt h2 *)
+(*     | BO_Zgt -> fprintf fmt "(>= %a (+ %a 1)" to_smt h1 to_smt h2 *)
+(*     | _ -> fprintf fmt "(%s %a %a)" (str_op op) to_smt h1 to_smt h2 *)
+
+(*   and to_smt_nop fmt op a = *)
+(*     let rec pp fmt = function *)
+(*       | [] -> assert false *)
+(*       | [x, y] -> fprintf fmt "(not (= %a %a))" to_smt x to_smt y *)
+(*       | (x, y) :: r -> *)
+(*         fprintf fmt "(and (not (= %a %a)) %a)" to_smt x to_smt y pp r *)
+(*     in *)
+(*     let pairs = cross (Array.to_list a) in *)
+(*     pp fmt pairs *)
+
+(* end *)
+
+let string_logic ro f =
+  let l = SL.union (Op.logic_ro ro) (Form.logic f) in
+  if SL.is_empty l then "QF_SAT"
+  else
+    sprintf "QF_%s%s%s%s"
+    (if SL.mem LArrays l then "A" else "")
+    (if SL.mem LUF l || SL.mem LLia l then "UF" else "")
+    (if SL.mem LBitvectors l then "BV" else "")
+    (if SL.mem LLia l then "LIA" else "")
+
+
+
+let call_cvc4 env rt ro ra rf root _ =
+  let open Smtlib2_solver in
+  let fl = snd root in
+
+  let cvc4 = create [|
+      "cvc4";
+      "--lang"; "smt2";
+      "--proof";
+      "--no-simplification"; "--fewer-preprocessing-holes";
+      "--no-bv-eq"; "--no-bv-ineq"; "--no-bv-algebraic" |] in
+
+  set_option cvc4 "print-success" true;
+  set_option cvc4 "produce-assignments" true;
+  set_option cvc4 "produce-proofs" true;
+  set_logic cvc4 (string_logic ro fl);
+
+  List.iter (fun (i,t) ->
+    let s = "Tindex_"^(string_of_int i) in
+    VeritSyntax.add_btype s (SmtBtype.Tindex t);
+    declare_sort cvc4 s 0;
+  ) (SmtBtype.to_list rt);
+  
+  List.iter (fun (i,cod,dom,op) ->
+    let s = "op_"^(string_of_int i) in
+    VeritSyntax.add_fun s op;
+    let args =
+      Array.fold_right
+        (fun t acc -> asprintf "%a" SmtBtype.to_smt t :: acc) cod [] in
+    let ret = asprintf "%a" SmtBtype.to_smt dom in
+    declare_fun cvc4 s args ret
+  ) (Op.to_list ro);
+
+  assume cvc4 (asprintf "%a" (Form.to_smt Atom.to_smt) fl);
+
+  let proof =
+    match check_sat cvc4 with
+    | Unsat ->
+      begin
+        try get_proof cvc4 (import_trace (Some root) lfsc_parse_one)
+        with
+        | Ast.CVC4Sat -> Structures.error "CVC4 returned SAT"
+        | No_proof -> Structures.error "CVC4 did not generate a proof"
+        | Failure s -> Structures.error ("Importing of proof failed: " ^ s)
+      end
+    | Sat ->
+      let smodel = get_model cvc4 in
+      Structures.error
+        ("CVC4 returned sat. Here is the model:\n\n" ^
+         SmtCommands.model_string env rt ro ra rf smodel)
+        (* (asprintf "CVC4 returned sat. Here is the model:\n%a" SExpr.print smodel) *)
+  in
+
+  quit cvc4;
+  proof
+
+
+
+let export out_channel rt ro l =
+  let fmt = formatter_of_out_channel out_channel in
+  fprintf fmt "(set-logic %s)@." (string_logic ro l);
+
+  List.iter (fun (i,t) ->
+    let s = "Tindex_"^(string_of_int i) in
+    VeritSyntax.add_btype s (SmtBtype.Tindex t);
+    fprintf fmt "(declare-sort %s 0)@." s
+  ) (SmtBtype.to_list rt);
+
+  List.iter (fun (i,cod,dom,op) ->
+    let s = "op_"^(string_of_int i) in
+    VeritSyntax.add_fun s op;
+    fprintf fmt "(declare-fun %s (" s;
+    let is_first = ref true in
+    Array.iter (fun t ->
+        if !is_first then is_first := false
+        else fprintf fmt " "; SmtBtype.to_smt fmt t
+      ) cod;
+    fprintf fmt ") %a)@." SmtBtype.to_smt dom;
+  ) (Op.to_list ro);
+
+  fprintf fmt "(assert %a)@\n(check-sat)@\n(exit)@."
+    (Form.to_smt Atom.to_smt) l
+
+
+
+let get_model_from_file filename =
+  let chan = open_in filename in
+  let lexbuf = Lexing.from_channel chan in
+  match SExprParser.sexps SExprLexer.main lexbuf with
+  | [SExpr.Atom "sat"; m] -> m
+  | _ -> Structures.error "CVC4 returned SAT but no model"
+
+
+let call_cvc4_file env rt ro ra rf root =
+  let fl = snd root in
+  let (filename, outchan) = Filename.open_temp_file "cvc4_coq" ".smt2" in
+  export outchan rt ro fl;
+  close_out outchan;
+  let bf = Filename.chop_extension filename in
+  let prooffilename = bf ^ ".lfsc" in
+
+  (* let cvc4_cmd = *)
+  (*   "cvc4 --proof --dump-proof -m --dump-model \ *)
+  (*    --no-simplification --fewer-preprocessing-holes \ *)
+  (*    --no-bv-eq --no-bv-ineq --no-bv-algebraic " *)
+  (*   ^ filename ^ " > " ^ prooffilename in *)
+  (* CVC4 crashes when asking for both models and proofs *)
+  
+  let cvc4_cmd =
+    "cvc4 --proof --dump-proof \
+     --no-simplification --fewer-preprocessing-holes \
+     --no-bv-eq --no-bv-ineq --no-bv-algebraic "
+    ^ filename ^ " > " ^ prooffilename in
+  (* let clean_cmd = "sed -i -e '1d' " ^ prooffilename in *)
+  eprintf "%s@." cvc4_cmd;
+  let t0 = Sys.time () in
+  let exit_code = Sys.command cvc4_cmd in
+  
+  let t1 = Sys.time () in
+  eprintf "CVC4 = %.5f@." (t1-.t0);
+
+  if exit_code <> 0 then
+    Structures.error ("CVC4 crashed: return code "^string_of_int exit_code);
+
+  (* ignore (Sys.command clean_cmd); *)
+
+  try import_trace_from_file (Some root) prooffilename
+  with
+  | No_proof -> Structures.error "CVC4 did not generate a proof"
+  | Failure s -> Structures.error ("Importing of proof failed: " ^ s)
+  | Ast.CVC4Sat ->
+    let smodel = get_model_from_file prooffilename in
+    Structures.error
+      ("CVC4 returned sat. Here is the model:\n\n" ^
+       SmtCommands.model_string env rt ro ra rf smodel)
+
+
+let cvc4_logic = 
+  SL.of_list [LUF; LLia; LBitvectors; LArrays]
+
+
+let tactic_gen vm_cast =
+  clear_all ();
+  let rt = SmtBtype.create () in
+  let ro = Op.create () in
+  let ra = VeritSyntax.ra in
+  let rf = VeritSyntax.rf in
+  let ra' = VeritSyntax.ra in
+  let rf' = VeritSyntax.rf in
+  SmtCommands.tactic call_cvc4 cvc4_logic rt ro ra rf ra' rf' vm_cast [] []
+  (* let ra = VeritSyntax.ra in
+   * let rf = VeritSyntax.rf in
+   * (\* Currently, quantifiers are not handled by the cvc4 tactic: we pass
+   *    the same ra and rf twice to have everything reifed *\)
+   * SmtCommands.tactic call_cvc4 cvc4_logic rt ro ra rf ra rf vm_cast [] [] *)
+let tactic () = tactic_gen vm_cast_true
+let tactic_no_check () = tactic_gen (fun _ -> vm_cast_true_no_check)