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, 278 insertions, 149 deletions

diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index a45fb63..c4427b7 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -1,13 +1,9 @@
 (**************************************************************************)
 (*                                                                        *)
 (*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2016                                          *)
+(*     Copyright (C) 2011 - 2019                                          *)
 (*                                                                        *)
-(*     Michaël Armand                                                     *)
-(*     Benjamin Grégoire                                                  *)
-(*     Chantal Keller                                                     *)
-(*                                                                        *)
-(*     Inria - École Polytechnique - Université Paris-Sud                 *)
+(*     See file "AUTHORS" for the list of authors                         *)
 (*                                                                        *)
 (*   This file is distributed under the terms of the CeCILL-C licence     *)
 (*                                                                        *)
@@ -24,7 +20,8 @@ open SmtTrace
 
 exception Sat
 
-type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2 | Xorn1 | Xorn2 | Impp | Impn1 | Impn2 | Equp1 | Equp2 | Equn1 | Equn2 | Itep1 | Itep2 | Iten1 | Iten2 | Eqre | Eqtr | Eqco | Eqcp | Dlge | Lage | Lata | Dlde | Lade | Fins | Eins | Skea | Skaa | Qnts | Qntm | Reso | And | Nor | Or | Nand | Xor1 | Xor2 | Nxor1 | Nxor2 | Imp | Nimp1 | Nimp2 | Equ1 | Equ2 | Nequ1 | Nequ2 | Ite1 | Ite2 | Nite1 | Nite2 | Tpal | Tlap | Tple | Tpne | Tpde | Tpsa | Tpie | Tpma | Tpbr | Tpbe | Tpsc | Tppp | Tpqt | Tpqs | Tpsk | Subp | Hole
+type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2 | Xorn1 | Xorn2 | Impp | Impn1 | Impn2 | Equp1 | Equp2 | Equn1 | Equn2 | Itep1 | Itep2 | Iten1 | Iten2 | Eqre | Eqtr | Eqco | Eqcp | Dlge | Lage | Lata | Dlde | Lade | Fins | Eins | Skea | Skaa | Qnts | Qntm | Reso | Weak | And | Nor | Or | Nand | Xor1 | Xor2 | Nxor1 | Nxor2 | Imp | Nimp1 | Nimp2 | Equ1 | Equ2 | Nequ1 | Nequ2 | Ite1 | Ite2 | Nite1 | Nite2 | Tpal | Tlap | Tple | Tpne | Tpde | Tpsa | Tpie | Tpma | Tpbr | Tpbe | Tpsc | Tppp | Tpqt | Tpqs | Tpsk | Subp | Flat | Hole | Bbva | Bbconst | Bbeq | Bbdis | Bbop | Bbadd | Bbmul | Bbult | Bbslt | Bbnot | Bbneg | Bbconc | Bbextr | Bbzext | Bbsext | Bbshl | Bbshr | Row1 | Row2 | Exte
+
 
 
 (* About equality *)
@@ -194,6 +191,23 @@ let mkDistinctElim old value =
   Other (SplDistinctElim (old,find_res l1 value))
 
 
+(* Clause difference (wrt to their sets of literals) *)
+
+let clause_diff c1 c2 =
+  let r =
+    List.filter (fun t1 -> not (List.exists (SmtAtom.Form.equal t1) c2)) c1
+  in
+  Format.eprintf "[";
+  List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c1;
+  Format.eprintf "] -- [";
+  List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c2;
+  Format.eprintf "] ==\n [";
+  List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) r;
+  Format.eprintf "] @.";
+  r
+
+
+
 (* Generating clauses *)
 
 let clauses : (int,Form.t clause) Hashtbl.t = Hashtbl.create 17
@@ -211,7 +225,7 @@ let add_ref i j = Hashtbl.add ref_cl i j
 let clear_ref () = Hashtbl.clear ref_cl
 
 (* Recognizing and modifying clauses depending on a forall_inst clause. *)
-                                 
+
 let rec fins_lemma ids_params =
   match ids_params with
     [] -> raise Not_found
@@ -222,9 +236,9 @@ let rec fins_lemma ids_params =
 
 let rec find_remove_lemma lemma ids_params =
   let eq_lemma h = eq_clause lemma (get_clause h) in
-  list_find_remove eq_lemma ids_params 
+  list_find_remove eq_lemma ids_params
 
-(* Removes the lemma in a list of ids containing an instance of this lemma *)                   
+(* Removes the lemma in a list of ids containing an instance of this lemma *)
 let rec merge ids_params =
   let rest_opt = try let lemma = fins_lemma ids_params in
                      let _, rest = find_remove_lemma lemma ids_params in
@@ -235,136 +249,237 @@ let rec merge ids_params =
   | Some r -> merge r
 
 let to_add = ref []
-                     
+
 let rec mk_clause (id,typ,value,ids_params) =
   let kind =
     match typ with
-    | Tpbr ->
-       begin match ids_params with
-       | [id] ->
-          Same (get_clause id)
-       | _ -> failwith "unexpected form of tmp_betared" end
-    | Tpqt ->
-       begin match ids_params with
-       | [id] ->
-          Same (get_clause id)
-       | _ -> failwith "unexpected form of tmp_qnt_tidy" end
-    | Fins ->
-       begin match value, ids_params with
-        | [inst], [ref_th] ->
-           let cl_th = get_clause ref_th in
-           Other (Forall_inst (repr cl_th, inst))
-        | _ -> failwith "unexpected form of forall_inst" end
-    | Or ->
-       (match ids_params with
-        | [id_target] ->
-           let cl_target = get_clause id_target in
-           begin match cl_target.kind with
-           | Other (Forall_inst _) -> Same cl_target
-           | _ -> Other (ImmBuildDef cl_target) end
-        | _ -> assert false)
-    (* Resolution *)
-    | Reso ->
-       let ids_params = merge ids_params in
-       (match ids_params with
-        | cl1::cl2::q ->
-           let res = {rc1 = get_clause cl1; rc2 = get_clause cl2; rtail = List.map get_clause q} in
-           Res res
-        | [fins_id] -> Same (get_clause fins_id)
-        | [] -> assert false)
-
-    (* Roots *)
-    | Inpu -> Root
-    (* Cnf conversion *)
-    | True -> Other SmtCertif.True
-    | Fals -> Other False
-    | Andn | Orp | Impp | Xorp1 | Xorn1 | Equp1 | Equn1 | Itep1 | Iten1 ->
-       (match value with
-        | l::_ -> Other (BuildDef l)
-        | _ -> assert false)
-    | Xorp2 | Xorn2 | Equp2 | Equn2 | Itep2 | Iten2 ->
-       (match value with
-        | l::_ -> Other (BuildDef2 l)
-        | _ -> assert false)
-    | Orn | Andp ->
-       (match value,ids_params with
-        | l::_, [p] -> Other (BuildProj (l,p))
-        | _ -> assert false)
-    | Impn1 ->
-       (match value with
-        | l::_ -> Other (BuildProj (l,0))
-        | _ -> assert false)
-    | Impn2 ->
-       (match value with
-        | l::_ -> Other (BuildProj (l,1))
-        | _ -> assert false)
-    | Nand | Imp | Xor1 | Nxor1 | Equ2 | Nequ2 | Ite1 | Nite1 ->
-       (match ids_params with
-        | [id] -> Other (ImmBuildDef (get_clause id))
-        | _ -> assert false)
-    | Xor2 | Nxor2 | Equ1 | Nequ1 | Ite2 | Nite2 ->
-       (match ids_params with
-        | [id] -> Other (ImmBuildDef2 (get_clause id))
-        | _ -> assert false)
-    | And | Nor ->
-       (match ids_params with
-        | [id;p] -> Other (ImmBuildProj (get_clause id,p))
-        | _ -> assert false)
-    | Nimp1 ->
-       (match ids_params with
-        | [id] -> Other (ImmBuildProj (get_clause id,0))
-        | _ -> assert false)
-    | Nimp2 ->
-       (match ids_params with
-        | [id] -> Other (ImmBuildProj (get_clause id,1))
-        | _ -> assert false)
-    (* Equality *)
-    | Eqre -> mkTrans value
-    | Eqtr -> mkTrans value
-    | Eqco -> mkCongr value
-    | Eqcp -> mkCongrPred value
-    (* Linear integer arithmetic *)
-    | Dlge | Lage | Lata -> mkMicromega value
-    | Lade               -> mkMicromega value (* TODO: utiliser un solveur plus simple *)
-    | Dlde ->
-       (match value with
-        | l::_ -> Other (LiaDiseq l)
-        | _ -> assert false)
-    (* Simplifications *)
-    | Tpal ->
-       (match ids_params with
-        | id::_ -> Same (get_clause id)
-        | _ -> assert false)
-    | Tple ->
-       (match ids_params with
-        | id::_ -> Same (get_clause id)
-        | _ -> assert false)
-    | Tpde ->
-       (match ids_params with
-        | id::_ -> mkDistinctElim (get_clause id) value
-        | _ -> assert false)
-    | Tpsa | Tlap ->
-       (match ids_params with
-        | id::_ -> mkSplArith (get_clause id) value
-        | _ -> assert false)
-    (* Holes in proofs *)
-    | Hole -> Other (SmtCertif.Hole (List.map get_clause ids_params, value))
-    (* Not implemented *)
-    | Deep -> failwith "VeritSyntax.ml: rule deep_res not implemented yet"
-    | Eins -> failwith "VeritSyntax.ml: rule exists_inst not implemented yet"
-    | Skea -> failwith "VeritSyntax.ml: rule skolem_ex_ax not implemented yet"
-    | Skaa -> failwith "VeritSyntax.ml: rule skolem_all_ax not implemented yet"
-    | Qnts -> failwith "VeritSyntax.ml: rule qnt_simplify_ax not implemented yet"
-    | Qntm -> failwith "VeritSyntax.ml: rule qnt_merge_ax not implemented yet"
-    | Tpne -> failwith "VeritSyntax.ml: rule tmp_nary_elim not implemented yet"
-    | Tpie -> failwith "VeritSyntax.ml: rule tmp_ite_elim not implemented yet"
-    | Tpma -> failwith "VeritSyntax.ml: rule tmp_macrosubst not implemented yet"
-    | Tpbe -> failwith "VeritSyntax.ml: rule tmp_bfun_elim not implemented yet"
-    | Tpsc -> failwith "VeritSyntax.ml: rule tmp_sk_connector not implemented yet"
-    | Tppp -> failwith "VeritSyntax.ml: rule tmp_pm_process not implemented yet"
-    | Tpqs -> failwith "VeritSyntax.ml: rule tmp_qnt_simplify not implemented yet"
-    | Tpsk -> failwith "VeritSyntax.ml: rule tmp_skolemize not implemented yet"
-    | Subp -> failwith "VeritSyntax.ml: rule subproof not implemented yet"
+      (* Roots *)
+      | Inpu -> Root
+      (* Cnf conversion *)
+      | True -> Other SmtCertif.True
+      | Fals -> Other False
+      | Andn | Orp | Impp | Xorp1 | Xorn1 | Equp1 | Equn1 | Itep1 | Iten1 ->
+        (match value with
+          | l::_ -> Other (BuildDef l)
+          | _ -> assert false)
+      | Xorp2 | Xorn2 | Equp2 | Equn2 | Itep2 | Iten2 ->
+        (match value with
+          | l::_ -> Other (BuildDef2 l)
+          | _ -> assert false)
+      | Orn | Andp ->
+        (match value,ids_params with
+          | l::_, [p] -> Other (BuildProj (l,p))
+          | _ -> assert false)
+      | Impn1 ->
+        (match value with
+          | l::_ -> Other (BuildProj (l,0))
+          | _ -> assert false)
+      | Impn2 ->
+        (match value with
+          | l::_ -> Other (BuildProj (l,1))
+          | _ -> assert false)
+      | Nand | Imp | Xor1 | Nxor1 | Equ2 | Nequ2 | Ite1 | Nite1 ->
+        (match ids_params with
+          | [id] -> Other (ImmBuildDef (get_clause id))
+          | _ -> assert false)
+      | Or ->
+         (match ids_params with
+            | [id_target] ->
+               let cl_target = get_clause id_target in
+               begin match cl_target.kind with
+                 | Other (Forall_inst _) -> Same cl_target
+                 | _ -> Other (ImmBuildDef cl_target) end
+            | _ -> assert false)
+      | Xor2 | Nxor2 | Equ1 | Nequ1 | Ite2 | Nite2 ->
+        (match ids_params with
+          | [id] -> Other (ImmBuildDef2 (get_clause id))
+          | _ -> assert false)
+      | And | Nor ->
+        (match ids_params with
+          | [id;p] -> Other (ImmBuildProj (get_clause id,p))
+          | _ -> assert false)
+      | Nimp1 ->
+        (match ids_params with
+          | [id] -> Other (ImmBuildProj (get_clause id,0))
+          | _ -> assert false)
+      | Nimp2 ->
+        (match ids_params with
+          | [id] -> Other (ImmBuildProj (get_clause id,1))
+          | _ -> assert false)
+      (* Equality *)
+      | Eqre -> mkTrans value
+      | Eqtr -> mkTrans value
+      | Eqco -> mkCongr value
+      | Eqcp -> mkCongrPred value
+      (* Linear integer arithmetic *)
+      | Dlge | Lage | Lata -> mkMicromega value
+      | Lade               -> mkMicromega value (* TODO: utiliser un solveur plus simple *)
+      | Dlde ->
+        (match value with
+          | l::_ -> Other (LiaDiseq l)
+          | _ -> assert false)
+      (* Resolution *)
+      | Reso ->
+         let ids_params = merge ids_params in
+         (match ids_params with
+            | cl1::cl2::q ->
+               let res = {rc1 = get_clause cl1; rc2 = get_clause cl2; rtail = List.map get_clause q} in
+               Res res
+            | [fins_id] -> Same (get_clause fins_id)
+            | [] -> assert false)
+      (* Clause weakening *)
+      | Weak ->
+        (match ids_params with
+         | [id] -> (* Other (Weaken (get_clause id, value)) *)
+           let cid = get_clause id in
+           (match cid.value with
+           | None -> Other (Weaken (cid, value))
+           | Some c -> Other (Weaken (cid, value))
+            (* need to add c, otherwise dosen't terminate or returns false,
+               we would like instead: clause_diff value c *)
+           )
+          | _ -> assert false)
+      (* Simplifications *)
+      | Tpal ->
+        (match ids_params with
+          | id::_ -> Same (get_clause id)
+          | _ -> assert false)
+      | Tple ->
+        (match ids_params with
+          | id::_ -> Same (get_clause id)
+          | _ -> assert false)
+      | Tpde ->
+        (match ids_params with
+          | id::_ -> mkDistinctElim (get_clause id) value
+          | _ -> assert false)
+      | Tpsa | Tlap ->
+        (match ids_params with
+          | id::_ -> mkSplArith (get_clause id) value
+          | _ -> assert false)
+      | Flat ->
+        (match ids_params, value with
+         | id::_, f :: _ -> Other (ImmFlatten(get_clause id, f))
+         | _ -> assert false)
+      (* Bit blasting *)
+      | Bbva ->
+         (match value with
+           | [f] -> Other (BBVar f)
+           | _ -> assert false)
+      | Bbconst ->
+         (match value with
+           | [f] -> Other (BBConst f)
+           | _ -> assert false)
+      | Bbeq ->
+         (match ids_params, value with
+           | [id1;id2], [f] -> Other (BBEq (get_clause id1, get_clause id2, f))
+           | _, _ -> assert false)
+      | Bbdis ->
+         (match value with
+           | [f] -> Other (BBDiseq f)
+           | __ -> assert false)
+      | Bbop ->
+         (match ids_params, value with
+           | [id1;id2], [f] -> Other (BBOp (get_clause id1, get_clause id2, f))
+           | _, _ -> assert false)
+      | Bbadd ->
+         (match ids_params, value with
+           | [id1;id2], [f] -> Other (BBAdd (get_clause id1, get_clause id2, f))
+           | _, _ -> assert false)
+      | Bbmul ->
+         (match ids_params, value with
+           | [id1;id2], [f] -> Other (BBMul (get_clause id1, get_clause id2, f))
+           | _, _ -> assert false)
+      | Bbult ->
+         (match ids_params, value with
+           | [id1;id2], [f] -> Other (BBUlt (get_clause id1, get_clause id2, f))
+           | _, _ -> assert false)
+      | Bbslt ->
+         (match ids_params, value with
+           | [id1;id2], [f] -> Other (BBSlt (get_clause id1, get_clause id2, f))
+           | _, _ -> assert false)
+      | Bbconc ->
+         (match ids_params, value with
+           | [id1;id2], [f] ->
+             Other (BBConc (get_clause id1, get_clause id2, f))
+           | _, _ -> assert false)
+      | Bbextr ->
+         (match ids_params, value with
+           | [id], [f] -> Other (BBExtr (get_clause id, f))
+           | _, _ -> assert false)
+      | Bbzext ->
+         (match ids_params, value with
+           | [id], [f] -> Other (BBZextn (get_clause id, f))
+           | _, _ -> assert false)
+      | Bbsext ->
+         (match ids_params, value with
+           | [id], [f] -> Other (BBSextn (get_clause id, f))
+           | _, _ -> assert false)
+      | Bbshl ->
+         (match ids_params, value with
+           | [id1;id2], [f] -> Other (BBShl (get_clause id1, get_clause id2, f))
+           | _, _ -> assert false)
+      | Bbshr ->
+         (match ids_params, value with
+           | [id1;id2], [f] -> Other (BBShr (get_clause id1, get_clause id2, f))
+           | _, _ -> assert false)
+      | Bbnot ->
+         (match ids_params, value with
+           | [id], [f] -> Other (BBNot (get_clause id, f))
+           | _, _ -> assert false)
+      | Bbneg ->
+         (match ids_params, value with
+           | [id], [f] -> Other (BBNeg (get_clause id, f))
+           | _, _ -> assert false)
+
+      | Row1 ->
+         (match value with
+           | [f] -> Other (RowEq f)
+           | _ -> assert false)
+
+      | Exte ->
+         (match value with
+           | [f] -> Other (Ext f)
+           | _ -> assert false)
+
+      | Row2 -> Other (RowNeq value)
+
+      (* Holes in proofs *)
+      | Hole -> Other (SmtCertif.Hole (List.map get_clause ids_params, value))
+
+      (* Quantifier instanciation *)
+      | Fins ->
+         begin match value, ids_params with
+           | [inst], [ref_th] ->
+              let cl_th = get_clause ref_th in
+              Other (Forall_inst (repr cl_th, inst))
+           | _ -> failwith "unexpected form of forall_inst" end
+      | Tpbr ->
+         begin match ids_params with
+           | [id] ->
+              Same (get_clause id)
+           | _ -> failwith "unexpected form of tmp_betared" end
+      | Tpqt ->
+         begin match ids_params with
+           | [id] ->
+              Same (get_clause id)
+           | _ -> failwith "unexpected form of tmp_qnt_tidy" end
+
+      (* Not implemented *)
+      | Deep -> failwith "VeritSyntax.ml: rule deep_res not implemented yet"
+      | Eins -> failwith "VeritSyntax.ml: rule exists_inst not implemented yet"
+      | Skea -> failwith "VeritSyntax.ml: rule skolem_ex_ax not implemented yet"
+      | Skaa -> failwith "VeritSyntax.ml: rule skolem_all_ax not implemented yet"
+      | Qnts -> failwith "VeritSyntax.ml: rule qnt_simplify_ax not implemented yet"
+      | Qntm -> failwith "VeritSyntax.ml: rule qnt_merge_ax not implemented yet"
+      | Tpne -> failwith "VeritSyntax.ml: rule tmp_nary_elim not implemented yet"
+      | Tpie -> failwith "VeritSyntax.ml: rule tmp_ite_elim not implemented yet"
+      | Tpma -> failwith "VeritSyntax.ml: rule tmp_macrosubst not implemented yet"
+      | Tpbe -> failwith "VeritSyntax.ml: rule tmp_bfun_elim not implemented yet"
+      | Tpsc -> failwith "VeritSyntax.ml: rule tmp_sk_connector not implemented yet"
+      | Tppp -> failwith "VeritSyntax.ml: rule tmp_pm_process not implemented yet"
+      | Tpqs -> failwith "VeritSyntax.ml: rule tmp_qnt_simplify not implemented yet"
+      | Tpsk -> failwith "VeritSyntax.ml: rule tmp_skolemize not implemented yet"
+      | Subp -> failwith "VeritSyntax.ml: rule subproof not implemented yet"
   in
   let cl =
     (* TODO: change this into flatten when necessary *)
@@ -375,6 +490,12 @@ let rec mk_clause (id,typ,value,ids_params) =
   id
 
 
+let mk_clause cl =
+  try mk_clause cl
+  with Failure f ->
+    Structures.error ("SMTCoq was not able to check the certificate \
+                       for the following reason.\n"^f)
+
 type atom_form_lit =
   | Atom of SmtAtom.Atom.t
   | Form of SmtAtom.Form.pform
@@ -396,16 +517,23 @@ let rec list_dec = function
   | (decl_h, h) :: t ->
      let decl_t, l_t = list_dec t in
      decl_h && decl_t, h :: l_t
-    
-let apply_dec_atom f = function
-  | decl, Atom h -> decl, Atom (f decl h)
+
+let apply_dec_atom (f:?declare:bool -> SmtAtom.hatom -> SmtAtom.hatom) = function
+  | decl, Atom h -> decl, Atom (f ~declare:decl h)
   | _ -> assert false
 
-let apply_bdec_atom f o1 o2 =
+let apply_bdec_atom (f:?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) o1 o2 =
   match o1, o2 with
   | (decl1, Atom h1), (decl2, Atom h2) ->
      let decl = decl1 && decl2 in
-     decl, Atom (f decl h1 h2)
+     decl, Atom (f ~declare:decl h1 h2)
+  | _ -> assert false
+
+let apply_tdec_atom (f:?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) o1 o2 o3 =
+  match o1, o2, o3 with
+  | (decl1, Atom h1), (decl2, Atom h2), (decl3, Atom h3) ->
+     let decl = decl1 && decl2 && decl3 in
+     decl, Atom (f ~declare:decl h1 h2 h3)
   | _ -> assert false
 
 
@@ -428,6 +556,7 @@ let get_fun id =
   try Hashtbl.find funs id
   with | Not_found -> failwith ("VeritSyntax.get_fun : function symbol \""^id^"\" not found\n")
 let add_fun id cl = Hashtbl.add funs id cl
+let remove_fun id = Hashtbl.remove funs id
 let clear_funs () = Hashtbl.clear funs
 
 let qvar_tbl : (string, SmtBtype.btype) Hashtbl.t = Hashtbl.create 10
@@ -436,9 +565,9 @@ let find_opt_qvar s = try Some (Hashtbl.find qvar_tbl s)
 let add_qvar s bt = Hashtbl.add qvar_tbl s bt
 let clear_qvar () = Hashtbl.clear qvar_tbl
 
-let string_hform = Form.to_string ~pi:true (Atom.to_string ~pi:true )
+let hform_to_smt = Form.to_smt ~pi:true Atom.to_smt
 
-(* Finding the index of a root in <lsmt> modulo the <re_hash> function. 
+(* Finding the index of a root in <lsmt> modulo the <re_hash> function.
    This function is used by SmtTrace.order_roots *)
 let init_index lsmt re_hash =
   let form_index_init_rank : (int, int) Hashtbl.t = Hashtbl.create 20 in
@@ -453,9 +582,9 @@ let init_index lsmt re_hash =
             try find (Form.to_lit re_hf)
             with Not_found ->
               let oc = open_out "/tmp/input_not_found.log" in
-              (List.map string_hform lsmt)
-              |> List.iter (Printf.fprintf oc "%s\n");
-              Printf.fprintf oc "\n%s\n" (string_hform re_hf);
+              let fmt = Format.formatter_of_out_channel oc in
+              List.iter (fun h -> Format.fprintf fmt "%a\n" hform_to_smt h) lsmt;
+              Format.fprintf fmt "\n%a\n" hform_to_smt re_hf;
               flush oc; close_out oc;
               failwith "not found: log available"
 
@@ -469,7 +598,7 @@ let qf_to_add lr =
        (Other (Qf_lemma (r, l)), r.value, r) :: qf_lemmas t
     | _::t -> qf_lemmas t in
   qf_lemmas lr
-                       
+
 let ra = Atom.create ()
 let rf = Form.create ()
 let ra' = Atom.create ()
@@ -477,7 +606,7 @@ let rf' = Form.create ()
 
 let hlets : (string, atom_form_lit) Hashtbl.t = Hashtbl.create 17
 
-let clear_mk_clause () = 
+let clear_mk_clause () =
   to_add := [];
   clear_ref ()