Initial import of SMTCoq v1.2

10 files changed, 2124 insertions, 0 deletions

diff --git a/src/verit/smtlib2_ast.ml b/src/verit/smtlib2_ast.ml
new file mode 100644
index 0000000..cce4625
--- /dev/null
+++ b/src/verit/smtlib2_ast.ml
@@ -0,0 +1,189 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq, originally belong to The Alt-ergo theorem prover           *)
+(*     Copyright (C) 2006-2010                                            *)
+(*                                                                        *)
+(*     Sylvain Conchon                                                    *)
+(*     Evelyne Contejean                                                  *)
+(*     Stephane Lescuyer                                                  *)
+(*     Mohamed Iguernelala                                                *)
+(*     Alain Mebsout                                                      *)
+(*                                                                        *)
+(*     CNRS - INRIA - Universite Paris Sud                                *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Smtlib2_util
+
+type loc = Lexing.position * Lexing.position
+
+type specconstant =
+  | SpecConstsDec of loc * string
+  | SpecConstNum of loc * string
+  | SpecConstString of loc * string
+  | SpecConstsHex of loc * string
+  | SpecConstsBinary of loc * string
+
+type symbol =
+  | Symbol of loc * string
+  | SymbolWithOr of loc * string
+
+type sexpr =
+  | SexprSpecConst of loc * specconstant
+  | SexprSymbol of loc * symbol
+  | SexprKeyword of loc * string
+  | SexprInParen of loc * (loc * sexpr list)
+
+type attributevalue =
+  | AttributeValSpecConst of loc * specconstant
+  | AttributeValSymbol of loc * symbol
+  | AttributeValSexpr of loc * (loc * sexpr list)
+
+type attribute =
+  | AttributeKeyword of loc * string
+  | AttributeKeywordValue of loc * string * attributevalue
+
+type an_option = AnOptionAttribute of loc * attribute
+
+type infoflag = InfoFlagKeyword of loc * string
+
+type identifier =
+  | IdSymbol of loc * symbol
+  | IdUnderscoreSymNum of loc * symbol * (loc * string list)
+
+type sort =
+  | SortIdentifier of loc * identifier
+  | SortIdSortMulti of loc * identifier * (loc * sort list)
+
+type qualidentifier =
+  | QualIdentifierId of loc * identifier
+  | QualIdentifierAs of loc * identifier * sort
+
+type sortedvar =
+  | SortedVarSymSort of loc * symbol * sort
+
+type varbinding = VarBindingSymTerm of loc * symbol * term
+
+and term =
+  | TermSpecConst of loc * specconstant
+  | TermQualIdentifier of loc * qualidentifier
+  | TermQualIdTerm of loc * qualidentifier * (loc * term list)
+  | TermLetTerm of loc * (loc * varbinding list) * term
+  | TermForAllTerm of loc * (loc * sortedvar list) * term
+  | TermExistsTerm of loc * (loc * sortedvar list) * term
+  | TermExclimationPt of loc * term * (loc * attribute list)
+
+type command =
+  | CSetLogic of loc * symbol
+  | CSetOption of loc * an_option
+  | CSetInfo of loc * attribute
+  | CDeclareSort of loc * symbol * string
+  | CDefineSort of loc * symbol * (loc * symbol list) * sort
+  | CDeclareFun of loc * symbol * (loc * sort list) * sort
+  | CDefineFun of loc * symbol * (loc * sortedvar list) * sort * term
+  | CPush of loc * string
+  | CPop of loc * string
+  | CAssert of loc * term
+  | CCheckSat of loc
+  | CGetAssert of loc
+  | CGetProof of loc
+  | CGetUnsatCore of loc
+  | CGetValue of loc * (loc * term list)
+  | CGetAssign of loc
+  | CGetOption of loc * string
+  | CGetInfo of loc * infoflag
+  | CExit of loc
+
+type commands = Commands of loc * (loc * command list)
+
+
+(* loc stands for pos (position) and extradata *)
+
+let loc_an_option = function
+  | AnOptionAttribute(d,_) -> d
+
+let loc_attribute = function
+  | AttributeKeyword(d,_) -> d
+  | AttributeKeywordValue(d,_,_) -> d
+
+let loc_attributevalue = function
+  | AttributeValSpecConst(d,_) -> d
+  | AttributeValSymbol(d,_) -> d
+  | AttributeValSexpr(d,_) -> d
+
+let loc_command = function
+  | CSetLogic(d,_) -> d
+  | CSetOption(d,_) -> d
+  | CSetInfo(d,_) -> d
+  | CDeclareSort(d,_,_) -> d
+  | CDefineSort(d,_,_,_) -> d
+  | CDeclareFun(d,_,_,_) -> d
+  | CDefineFun(d,_,_,_,_) -> d
+  | CPush(d,_) -> d
+  | CPop(d,_) -> d
+  | CAssert(d,_) -> d
+  | CCheckSat(d) -> d
+  | CGetAssert(d) -> d
+  | CGetProof(d) -> d
+  | CGetUnsatCore(d) -> d
+  | CGetValue(d,_) -> d
+  | CGetAssign(d) -> d
+  | CGetOption(d,_) -> d
+  | CGetInfo(d,_) -> d
+  | CExit(d) -> d
+
+let loc_commands = function
+  | Commands(d,_) -> d
+
+let loc_identifier = function
+  | IdSymbol(d,_) -> d
+  | IdUnderscoreSymNum(d,_,_) -> d
+
+let loc_infoflag = function
+  | InfoFlagKeyword(d,_) -> d
+
+let loc_qualidentifier = function
+  | QualIdentifierId(d,_) -> d
+  | QualIdentifierAs(d,_,_) -> d
+
+let loc_sexpr = function
+  | SexprSpecConst(d,_) -> d
+  | SexprSymbol(d,_) -> d
+  | SexprKeyword(d,_) -> d
+  | SexprInParen(d,_) -> d
+
+let loc_sort = function
+  | SortIdentifier(d,_) -> d
+  | SortIdSortMulti(d,_,_) -> d
+
+let loc_sortedvar = function
+  | SortedVarSymSort(d,_,_) -> d
+
+let loc_specconstant = function
+  | SpecConstsDec(d,_) -> d
+  | SpecConstNum(d,_) -> d
+  | SpecConstString(d,_) -> d
+  | SpecConstsHex(d,_) -> d
+  | SpecConstsBinary(d,_) -> d
+
+let loc_symbol = function
+  | Symbol(d,_) -> d
+  | SymbolWithOr(d,_) -> d
+
+let loc_term = function
+  | TermSpecConst(d,_) -> d
+  | TermQualIdentifier(d,_) -> d
+  | TermQualIdTerm(d,_,_) -> d
+  | TermLetTerm(d,_,_) -> d
+  | TermForAllTerm(d,_,_) -> d
+  | TermExistsTerm(d,_,_) -> d
+  | TermExclimationPt(d,_,_) -> d
+
+let loc_varbinding = function
+  | VarBindingSymTerm(d,_,_) -> d
+
+let loc_couple = fst
+
+let loc_of e = loc_commands e;;
diff --git a/src/verit/smtlib2_genConstr.ml b/src/verit/smtlib2_genConstr.ml
new file mode 100644
index 0000000..f11d650
--- /dev/null
+++ b/src/verit/smtlib2_genConstr.ml
@@ -0,0 +1,226 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Smtlib2_ast
+open SmtAtom
+open SmtForm
+open SmtMisc
+open CoqTerms
+
+
+(* For debugging *)
+
+let pp_symbol s =
+  let pp_position p = "{pos_fname = "^p.Lexing.pos_fname^"; pos_lnum = "^(string_of_int p.Lexing.pos_lnum)^"; pos_bol = "^(string_of_int p.Lexing.pos_bol)^"; pos_cnum = "^(string_of_int p.Lexing.pos_cnum)^"}" in
+
+  let pp_loc (p1,p2) = "("^(pp_position p1)^", "^(pp_position p2)^")" in
+
+  match s with
+    | Symbol (l,s) -> "Symbol ("^(pp_loc l)^", "^s^")"
+    | SymbolWithOr (l,s) -> "SymbolWithOr ("^(pp_loc l)^", "^s^")"
+
+
+(* Main functions *)
+
+let string_of_symbol = function | Symbol (_,s) | SymbolWithOr (_,s) -> s
+
+
+let identifier_of_qualidentifier = function
+  | QualIdentifierId (_,id) | QualIdentifierAs (_,id,_) -> id
+
+
+let string_type s = match s with
+  | "Bool" -> Tbool
+  | "Int" -> TZ
+  | _ -> VeritSyntax.get_btype s
+
+
+let sort_of_string s = (string_type s, [])
+
+
+let sort_of_symbol s = sort_of_string (string_of_symbol s)
+
+
+let string_of_identifier = function
+  | IdSymbol (_,s) -> (string_of_symbol s)
+  | IdUnderscoreSymNum (_,s,(_,l)) ->
+    List.fold_left (fun c c' -> c^"_"^c') (string_of_symbol s) l
+
+
+let string_of_qualidentifier id = string_of_identifier (identifier_of_qualidentifier id)
+
+
+let rec sort_of_sort = function
+  | SortIdentifier (_,id) -> sort_of_string (string_of_identifier id)
+  | SortIdSortMulti (_,id,(_,l)) ->
+    (string_type (string_of_identifier id), List.map sort_of_sort l)
+
+
+let declare_sort rt sym =
+  let s = string_of_symbol sym in
+  let cons_t = declare_new_type (Names.id_of_string ("Smt_sort_"^s)) in
+  let eq_t = declare_new_variable (Names.id_of_string ("eq_"^s)) (Term.mkArrow cons_t (Term.mkArrow cons_t (Lazy.force cbool))) in
+  let x = mkName "x" in
+  let y = mkName "y" in
+  let rx = Term.mkRel 2 in
+  let ry = Term.mkRel 1 in
+  let eq_refl = Term.mkProd (x,cons_t,Term.mkProd (y,cons_t,mklApp creflect [|mklApp ceq [|cons_t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in
+  let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl_"^s)) eq_refl in
+  let ce = mklApp cTyp_eqb [|cons_t;eq_t;eq_refl_v|] in
+  let res = Btype.declare rt cons_t ce in
+  VeritSyntax.add_btype s res;
+  res
+
+
+let declare_fun rt ro sym arg cod =
+  let s = string_of_symbol sym in
+  let tyl = List.map sort_of_sort arg in
+  let ty = sort_of_sort cod in
+
+  let coqTy = List.fold_right (fun typ c -> Term.mkArrow (Btype.interp_to_coq rt (fst typ)) c) tyl (Btype.interp_to_coq rt (fst ty)) in
+  let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in
+
+  let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) in
+  VeritSyntax.add_fun s op;
+  op
+
+
+let make_root_specconstant ra = function
+  | SpecConstsDec _ -> failwith "Smtlib2_genConstr.make_root_specconstant: decimals not implemented yet"
+  | SpecConstNum (_,s) ->
+    (try
+      let i = int_of_string s in
+      Atom.hatom_Z_of_int ra i
+    with
+      | Failure _ ->
+        let i = Big_int.big_int_of_string s in
+        Atom.hatom_Z_of_bigint ra i)
+  | SpecConstString _ -> failwith "Smtlib2_genConstr.make_root_specconstant: strings not implemented yet"
+  | SpecConstsHex _ -> failwith "Smtlib2_genConstr.make_root_specconstant: hexadecimals not implemented yet"
+  | SpecConstsBinary _ -> failwith "Smtlib2_genConstr.make_root_specconstant: binaries not implemented yet"
+
+
+type atom_form = | Atom of SmtAtom.Atom.t | Form of SmtAtom.Form.t
+
+
+let make_root ra rf t =
+
+  let hlets = Hashtbl.create 17 in
+
+  let rec make_root_term = function
+    | TermSpecConst (_,c) -> Atom (make_root_specconstant ra c)
+    | TermQualIdentifier (_,id) ->
+      let v = string_of_qualidentifier id in
+      (try Hashtbl.find hlets v with
+        | Not_found ->
+          make_root_app v [])
+    | TermQualIdTerm (_,id,(_,l)) ->
+      let v = string_of_qualidentifier id in
+      make_root_app v l
+    | TermLetTerm (_,(_,l),t) ->
+      List.iter (fun (VarBindingSymTerm (_, sym, u)) ->
+        let u' = make_root_term u in
+        let s' = string_of_symbol sym in
+        Hashtbl.add hlets s' u') l;
+      make_root_term t
+    | TermForAllTerm _ -> failwith "Smtlib2_genConstr.make_root_term: ForAll not implemented yet"
+    | TermExistsTerm _ -> failwith "Smtlib2_genConstr.make_root_term: Exists not implemented yet"
+    | TermExclimationPt (_,t,_) -> make_root_term t
+
+  and make_root_app v l =
+    match (v,l) with
+      | "=", [a;b] ->
+        (match make_root_term a, make_root_term b with
+          | Atom a', Atom b' ->
+            (match Atom.type_of a' with
+              | Tbool -> Form (Form.get rf (Fapp (Fiff, [|Form.get rf (Fatom a'); Form.get rf (Fatom b')|])))
+              | ty -> Atom (Atom.mk_eq ra ty a' b'))
+          | _, _ -> assert false)
+      | "<", [a;b] ->
+        (match make_root_term a, make_root_term b with
+          | Atom a', Atom b' -> Atom (Atom.mk_lt ra a' b')
+          | _, _ -> assert false)
+      | "<=", [a;b] ->
+        (match make_root_term a, make_root_term b with
+          | Atom a', Atom b' -> Atom (Atom.mk_le ra a' b')
+          | _, _ -> assert false)
+      | ">", [a;b] ->
+        (match make_root_term a, make_root_term b with
+          | Atom a', Atom b' -> Atom (Atom.mk_gt ra a' b')
+          | _, _ -> assert false)
+      | ">=", [a;b] ->
+        (match make_root_term a, make_root_term b with
+          | Atom a', Atom b' -> Atom (Atom.mk_ge ra a' b')
+          | _, _ -> assert false)
+      | "+", [a;b] ->
+        (match make_root_term a, make_root_term b with
+          | Atom a', Atom b' -> Atom (Atom.mk_plus ra a' b')
+          | _, _ -> assert false)
+      | "-", [a;b] ->
+        (match make_root_term a, make_root_term b with
+          | Atom a', Atom b' -> Atom (Atom.mk_minus ra a' b')
+          | _, _ -> assert false)
+      | "*", [a;b] ->
+        (match make_root_term a, make_root_term b with
+          | Atom a', Atom b' -> Atom (Atom.mk_mult ra a' b')
+          | _, _ -> assert false)
+      | "-", [a] ->
+        (match make_root_term a with
+          | Atom a' -> Atom (Atom.mk_opp ra a')
+          | _ -> assert false)
+      | "distinct", _ ->
+        let make_h h =
+          match make_root_term h with
+            | Atom h' -> h'
+            | _ -> assert false in
+        let a = Array.make (List.length l) (make_h (List.hd l)) in
+        let i = ref (-1) in
+        List.iter (fun h ->
+          incr i;
+          a.(!i) <- make_h h) l;
+        Atom (Atom.mk_distinct ra (Atom.type_of a.(0)) a)
+      | "true", _ -> Form (Form.get rf Form.pform_true)
+      | "false", _ -> Form (Form.get rf Form.pform_false)
+      | "and", _ ->
+        Form (Form.get rf (Fapp (Fand, Array.of_list (List.map make_root l))))
+      | "or", _ ->
+        Form (Form.get rf (Fapp (For, Array.of_list (List.map make_root l))))
+      | "xor", _ ->
+        Form (Form.get rf (Fapp (Fxor, Array.of_list (List.map make_root l))))
+      | "=>", _ ->
+        Form (Form.get rf (Fapp (Fimp, Array.of_list (List.map make_root l))))
+      | "ite", _ ->
+        Form (Form.get rf (Fapp (Fite, Array.of_list (List.map make_root l))))
+      | "not", [a] -> Form (Form.neg (make_root a))
+      | _, _ ->
+        let op = VeritSyntax.get_fun v in
+        let l' = List.map (fun t -> match make_root_term t with
+          | Atom h -> h | Form _ -> assert false) l in
+        Atom (Atom.get ra (Aapp (op, Array.of_list l')))
+
+  and make_root t =
+    match make_root_term t with
+      | Atom h -> Form.get rf (Fatom h)
+      | Form f -> f in
+
+  make_root t
+
+
+let declare_commands rt ro ra rf acc = function
+  | CDeclareSort (_,sym,_) -> let _ = declare_sort rt sym in acc
+  | CDeclareFun (_,sym, (_, arg), cod) ->
+    let _ = declare_fun rt ro sym arg cod in acc
+  | CAssert (_, t) -> (make_root ra rf t)::acc
+  | _ -> acc
diff --git a/src/verit/smtlib2_lex.mll b/src/verit/smtlib2_lex.mll
new file mode 100644
index 0000000..f235403
--- /dev/null
+++ b/src/verit/smtlib2_lex.mll
@@ -0,0 +1,88 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq, originally belong to The Alt-ergo theorem prover           *)
+(*     Copyright (C) 2006-2010                                            *)
+(*                                                                        *)
+(*     Sylvain Conchon                                                    *)
+(*     Evelyne Contejean                                                  *)
+(*     Stephane Lescuyer                                                  *)
+(*     Mohamed Iguernelala                                                *)
+(*     Alain Mebsout                                                      *)
+(*                                                                        *)
+(*     CNRS - INRIA - Universite Paris Sud                                *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+{
+open Lexing
+open Smtlib2_parse
+
+
+let newline lexbuf =
+    let pos = lexbuf.lex_curr_p in
+    lexbuf.lex_curr_p <-
+      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum;
+        pos_cnum=0 }
+
+}
+
+rule token = parse
+| ['\t' ' ' ]+
+    { token lexbuf }
+| ';'  (_ # '\n')*
+     { token lexbuf }
+| ['\n']+ as str
+     { newline lexbuf;
+       Smtlib2_util.line := (!Smtlib2_util.line + (String.length str));
+       token lexbuf }
+| "_"              { UNDERSCORE }
+| "("              { LPAREN }
+| ")"              { RPAREN }
+| "as"             { AS }
+| "let"            { LET }
+| "forall"         { FORALL }
+| "exists"         { EXISTS }
+| "!"              { EXCLIMATIONPT }
+| "set-logic"      { SETLOGIC }
+| "set-option"     { SETOPTION }
+| "set-info"       { SETINFO }
+| "declare-sort"   { DECLARESORT }
+| "define-sort"    { DEFINESORT }
+| "declare-fun"    { DECLAREFUN }
+| "define-fun"     { DEFINEFUN }
+| "push"           { PUSH }
+| "pop"            { POP }
+| "assert"         { ASSERT }
+| "check-sat"      { CHECKSAT }
+| "get-assertions" { GETASSERT }
+| "get-proof"      { GETPROOF }
+| "get-unsat-core" { GETUNSATCORE }
+| "get-value"      { GETVALUE }
+| "get-assignment" { GETASSIGN }
+| "get-option"     { GETOPTION }
+| "get-info"       { GETINFO }
+| "exit"           { EXIT }
+|  '#' 'x' ['0'-'9' 'A'-'F' 'a'-'f']+  as str
+    { HEXADECIMAL(str) }
+|  '#' 'b' ['0'-'1']+  as str
+    { BINARY(str) }
+|  '|' ([ '!'-'~' ' ' '\n' '\t' '\r'] # ['\\' '|'])* '|'  as str
+    { ASCIIWOR(str) }
+|  ':' ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=' '%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']+  as str
+    { KEYWORD(str) }
+|  ['a'-'z' 'A'-'Z' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@'] ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']*  as str
+    { SYMBOL(str) }
+|  '"' (([ '!'-'~' ' ' '\n' '\t' '\r' ] # ['\\' '"']) | ('\\' ['!'-'~' ' ' '\n' '\t' '\r'] ))* '"' as str
+    { STRINGLIT(str) }
+|  ( '0' | ['1'-'9'] ['0'-'9']* )  as str
+    { NUMERAL(str) }
+|  ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+ as str
+    { DECIMAL(str) }
+| eof
+    { EOF }
+| _
+    {failwith(
+      (Lexing.lexeme lexbuf) ^
+	": lexing error on line "^(string_of_int !Smtlib2_util.line))}{}
diff --git a/src/verit/smtlib2_parse.mly b/src/verit/smtlib2_parse.mly
new file mode 100644
index 0000000..b4e02a7
--- /dev/null
+++ b/src/verit/smtlib2_parse.mly
@@ -0,0 +1,299 @@
+/**************************************************************************/
+/*                                                                        */
+/*     SMTCoq, originally belong to The Alt-ergo theorem prover           */
+/*     Copyright (C) 2006-2010                                            */
+/*                                                                        */
+/*     Sylvain Conchon                                                    */
+/*     Evelyne Contejean                                                  */
+/*     Stephane Lescuyer                                                  */
+/*     Mohamed Iguernelala                                                */
+/*     Alain Mebsout                                                      */
+/*                                                                        */
+/*     CNRS - INRIA - Universite Paris Sud                                */
+/*                                                                        */
+/*   This file is distributed under the terms of the CeCILL-C licence     */
+/*                                                                        */
+/**************************************************************************/
+
+%{
+   open Smtlib2_ast
+
+   let loc () = symbol_start_pos (), symbol_end_pos ()
+
+%}
+
+%start main
+
+/* general */
+%token EXCLIMATIONPT
+%token UNDERSCORE
+%token AS
+%token EXISTS
+%token FORALL
+%token LET
+
+/* commands */
+%token SETLOGIC
+%token SETOPTION
+%token SETINFO
+%token DECLARESORT
+%token DEFINESORT
+%token DECLAREFUN
+%token DEFINEFUN
+%token PUSH
+%token POP
+%token ASSERT
+%token CHECKSAT
+%token GETASSERT
+%token GETPROOF
+%token GETUNSATCORE
+%token GETVALUE
+%token GETASSIGN
+%token GETOPTION
+%token GETINFO
+%token EXIT
+
+/* Other tokens */
+%token LPAREN
+%token RPAREN
+%token EOF
+
+%token <string> NUMERAL
+%token <string> DECIMAL
+%token <string> HEXADECIMAL
+%token <string> BINARY
+%token <string> STRINGLIT
+%token <string> ASCIIWOR
+%token <string> KEYWORD
+%token <string> SYMBOL
+
+
+%type <Smtlib2_ast.commands option> main
+%type <Smtlib2_ast.an_option> an_option
+%type <Smtlib2_ast.attribute> attribute
+%type <Smtlib2_ast.attributevalue> attributevalue
+%type <Smtlib2_ast.command> command
+%type <Smtlib2_ast.commands> commands
+%type <Smtlib2_ast.identifier> identifier
+%type <Smtlib2_ast.infoflag> infoflag
+%type <Smtlib2_ast.qualidentifier> qualidentifier
+%type <Smtlib2_ast.sexpr> sexpr
+%type <Smtlib2_ast.sort> sort
+%type <Smtlib2_ast.sortedvar> sortedvar
+%type <Smtlib2_ast.specconstant> specconstant
+%type <Smtlib2_ast.symbol> symbol
+%type <Smtlib2_ast.term> term
+%type <Smtlib2_ast.varbinding> varbinding
+
+/* %type <Smtlib2_ast.attributevalsexpr_attributevalue_sexpr5> attributevalsexpr_attributevalue_sexpr5 */
+/* %type <Smtlib2_ast.commanddeclarefun_command_sort13> commanddeclarefun_command_sort13 */
+/* %type <Smtlib2_ast.commanddefinefun_command_sortedvar15> commanddefinefun_command_sortedvar15 */
+/* %type <Smtlib2_ast.commanddefinesort_command_symbol11> commanddefinesort_command_symbol11 */
+/* %type <Smtlib2_ast.commandgetvalue_command_term24> commandgetvalue_command_term24 */
+/* %type <Smtlib2_ast.commands_commands_command30> commands_commands_command30 */
+/* %type <Smtlib2_ast.sexprinparen_sexpr_sexpr41> sexprinparen_sexpr_sexpr41 */
+/* %type <Smtlib2_ast.sortidsortmulti_sort_sort44> sortidsortmulti_sort_sort44 */
+/* %type <Smtlib2_ast.termexclimationpt_term_attribute64> termexclimationpt_term_attribute64 */
+/* %type <Smtlib2_ast.termexiststerm_term_sortedvar62> termexiststerm_term_sortedvar62 */
+/* %type <Smtlib2_ast.termforallterm_term_sortedvar60> termforallterm_term_sortedvar60 */
+/* %type <Smtlib2_ast.termletterm_term_varbinding58> termletterm_term_varbinding58 */
+/* %type <Smtlib2_ast.termqualidterm_term_term56> termqualidterm_term_term56 */
+/* %type <Smtlib2_ast.idunderscoresymnum_identifier_numeral33> idunderscoresymnum_identifier_numeral33 */
+%%
+
+main:
+| commands { Some($1) }
+| EOF { None }
+;
+
+an_option:
+| attribute { AnOptionAttribute(loc_attribute $1, $1) }
+;
+
+attribute:
+| KEYWORD { AttributeKeyword(loc (), $1) }
+| KEYWORD attributevalue { AttributeKeywordValue(loc (), $1, $2) }
+;
+
+sexpr_list:
+/*sexprinparen_sexpr_sexpr41:*/
+/*attributevalsexpr_attributevalue_sexpr5:*/
+| { (loc (), []) }
+| sexpr sexpr_list { let (_, l1) = $2 in (loc_sexpr $1, ($1)::(l1)) }
+;
+
+attributevalue:
+| specconstant { AttributeValSpecConst(loc_specconstant $1, $1) }
+| symbol { AttributeValSymbol(loc_symbol $1, $1) }
+| LPAREN sexpr_list RPAREN { AttributeValSexpr(loc (), $2) }
+;
+
+symbol_list: /*commanddefinesort_command_symbol11:*/
+| { (loc (), []) }
+| symbol symbol_list { let (_, l1) = $2 in (loc_symbol $1, ($1)::(l1)) }
+;
+
+sort_list0: /*commanddeclarefun_command_sort13:*/
+| { (loc (), []) }
+| sort sort_list0 { let (_, l1) = $2 in (loc_sort $1, ($1)::(l1)) }
+;
+
+sortedvar_list: /*commanddefinefun_command_sortedvar15:*/
+| { (loc (), []) }
+| sortedvar sortedvar_list
+    { let (_, l1) = $2 in (loc_sortedvar $1, ($1)::(l1)) }
+;
+
+command:
+| LPAREN SETLOGIC symbol RPAREN
+    { CSetLogic(loc (), $3) }
+| LPAREN SETOPTION an_option RPAREN
+    { CSetOption(loc (), $3) }
+| LPAREN SETINFO attribute RPAREN
+    { CSetInfo(loc (), $3) }
+| LPAREN DECLARESORT symbol NUMERAL RPAREN
+    { CDeclareSort(loc (), $3, $4) }
+| LPAREN DEFINESORT symbol LPAREN symbol_list RPAREN sort RPAREN
+    { CDefineSort(loc (), $3, $5, $7) }
+| LPAREN DECLAREFUN symbol LPAREN sort_list0 RPAREN sort RPAREN
+    { CDeclareFun(loc (), $3, $5, $7) }
+| LPAREN DEFINEFUN symbol LPAREN sortedvar_list RPAREN sort term RPAREN
+    { CDefineFun(loc (), $3, $5, $7, $8) }
+| LPAREN PUSH NUMERAL RPAREN
+    { CPush(loc (), $3) }
+| LPAREN POP NUMERAL RPAREN
+    { CPop(loc (), $3) }
+| LPAREN ASSERT term RPAREN
+    { CAssert(loc (), $3) }
+| LPAREN CHECKSAT RPAREN
+    { CCheckSat(loc ()) }
+| LPAREN GETASSERT RPAREN
+    { CGetAssert(loc ()) }
+| LPAREN GETPROOF RPAREN
+    { CGetProof(loc ()) }
+| LPAREN GETUNSATCORE RPAREN
+    { CGetUnsatCore(loc ()) }
+| LPAREN GETVALUE LPAREN term_list1 RPAREN RPAREN
+    { CGetValue(loc (), $4) }
+| LPAREN GETASSIGN RPAREN
+    { CGetAssign(loc ()) }
+| LPAREN GETOPTION KEYWORD RPAREN
+    { CGetOption(loc (), $3) }
+| LPAREN GETINFO infoflag RPAREN
+    { CGetInfo(loc (), $3) }
+| LPAREN EXIT RPAREN
+    { CExit(loc ()) }
+;
+
+
+command_list: /*commands_commands_command30:*/
+| { (loc (), []) }
+| command command_list { let (_, l1) = $2 in (loc_command $1, ($1)::(l1)) }
+;
+
+commands:
+| command_list { Commands(loc_couple $1, $1) }
+;
+
+numeral_list: /*idunderscoresymnum_identifier_numeral33:*/
+| NUMERAL { (loc (), ($1)::[]) }
+| NUMERAL numeral_list { let (_, l1) = $2 in (loc (), ($1)::(l1)) }
+;
+
+identifier:
+| symbol { IdSymbol(loc_symbol $1, $1) }
+| LPAREN UNDERSCORE symbol numeral_list RPAREN
+    { IdUnderscoreSymNum(loc (), $3, $4) }
+;
+
+infoflag:
+| KEYWORD { InfoFlagKeyword(loc (), $1) }
+;
+
+qualidentifier:
+| identifier { QualIdentifierId(loc_identifier $1, $1) }
+| LPAREN AS identifier sort RPAREN { QualIdentifierAs(loc (), $3, $4) }
+;
+
+sexpr:
+| specconstant { SexprSpecConst(loc_specconstant $1, $1) }
+| symbol { SexprSymbol(loc_symbol $1, $1) }
+| KEYWORD { SexprKeyword(loc (), $1) }
+| LPAREN sexpr_list RPAREN { SexprInParen(loc (), $2) }
+;
+
+
+sort_list1: /*sortidsortmulti_sort_sort44:*/
+| sort { (loc_sort $1, ($1)::[]) }
+| sort sort_list1 { let (_, l1) = $2 in (loc_sort $1, ($1)::(l1)) }
+;
+
+sort:
+| identifier { SortIdentifier(loc_identifier $1, $1) }
+| LPAREN identifier sort_list1 RPAREN { SortIdSortMulti(loc (), $2, $3) }
+;
+
+sortedvar:
+| LPAREN symbol sort RPAREN { SortedVarSymSort(loc (), $2, $3) }
+;
+
+specconstant:
+| DECIMAL { SpecConstsDec(loc (), $1) }
+| NUMERAL { SpecConstNum(loc (), $1) }
+| STRINGLIT { SpecConstString(loc (), $1) }
+| HEXADECIMAL { SpecConstsHex(loc (), $1) }
+| BINARY { SpecConstsBinary(loc (), $1) }
+;
+
+symbol:
+| SYMBOL { Symbol(loc (), $1) }
+| ASCIIWOR { SymbolWithOr(loc (), $1) }
+;
+
+term_list1:
+/*termqualidterm_term_term56:*/
+/*commandgetvalue_command_term24:*/
+| term { (loc_term $1, ($1)::[]) }
+| term term_list1 { let (_, l1) = $2 in (loc_term $1, ($1)::(l1)) }
+;
+
+varbinding_list1: /*termletterm_term_varbinding58:*/
+| varbinding { (loc_varbinding $1, ($1)::[]) }
+| varbinding varbinding_list1
+    { let (_, l1) = $2 in (loc_varbinding $1, ($1)::(l1)) }
+;
+
+sortedvar_list1:
+/*termforallterm_term_sortedvar60:*/
+/*termexiststerm_term_sortedvar62:*/
+| sortedvar { (loc_sortedvar $1, ($1)::[]) }
+| sortedvar sortedvar_list1
+    { let (_, l1) = $2 in (loc_sortedvar $1, ($1)::(l1)) }
+;
+
+attribute_list1: /*termexclimationpt_term_attribute64:*/
+| attribute { (loc_attribute $1, ($1)::[]) }
+| attribute attribute_list1
+    { let (_, l1) = $2 in (loc_attribute $1, ($1)::(l1)) }
+;
+
+term:
+| specconstant
+    { TermSpecConst(loc_specconstant $1, $1) }
+| qualidentifier
+    { TermQualIdentifier(loc_qualidentifier $1, $1) }
+| LPAREN qualidentifier term_list1 RPAREN
+    { TermQualIdTerm(loc (), $2, $3) }
+| LPAREN LET LPAREN varbinding_list1 RPAREN term RPAREN
+    { TermLetTerm(loc (), $4, $6) }
+| LPAREN FORALL LPAREN sortedvar_list1 RPAREN term RPAREN
+    { TermForAllTerm(loc (), $4, $6) }
+| LPAREN EXISTS LPAREN sortedvar_list1 RPAREN term RPAREN
+    { TermExistsTerm(loc (), $4, $6) }
+| LPAREN EXCLIMATIONPT term attribute_list1 RPAREN
+    { TermExclimationPt(loc (), $3, $4) }
+;
+
+varbinding:
+| LPAREN symbol term RPAREN { VarBindingSymTerm(loc (), $2, $3) }
+;
diff --git a/src/verit/smtlib2_util.ml b/src/verit/smtlib2_util.ml
new file mode 100644
index 0000000..1ce5e46
--- /dev/null
+++ b/src/verit/smtlib2_util.ml
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq, originally belong to The Alt-ergo theorem prover           *)
+(*     Copyright (C) 2006-2010                                            *)
+(*                                                                        *)
+(*     Sylvain Conchon                                                    *)
+(*     Evelyne Contejean                                                  *)
+(*     Stephane Lescuyer                                                  *)
+(*     Mohamed Iguernelala                                                *)
+(*     Alain Mebsout                                                      *)
+(*                                                                        *)
+(*     CNRS - INRIA - Universite Paris Sud                                *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* auto-generated by gt *)
+
+(* no extra data from grammar file. *)
+type extradata = unit;;
+let initial_data() = ();;
+
+let file = ref "stdin";;
+let line = ref 1;;
+type pos = int;;
+let string_of_pos p = "line "^(string_of_int p);;
+let cur_pd() = (!line, initial_data());;   (* "pd": pos + extradata *)
+type pd = pos * extradata;;
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
new file mode 100644
index 0000000..87e74a6
--- /dev/null
+++ b/src/verit/verit.ml
@@ -0,0 +1,542 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+open Entries
+open Declare
+open Decl_kinds
+
+open SmtMisc
+open CoqTerms
+open SmtForm
+open SmtCertif
+open SmtTrace
+open SmtAtom
+
+
+let debug = false
+
+
+(* Interpretation tables *)
+
+let mk_ftype cod dom =
+  let typeb = Lazy.force ctype in
+  let typea = mklApp clist [|typeb|] in
+  let a = Array.fold_right (fun bt acc -> mklApp ccons [|typeb; Btype.to_coq bt; acc|]) cod (mklApp cnil [|typeb|]) in
+  let b = Btype.to_coq dom in
+  mklApp cpair [|typea;typeb;a;b|]
+
+let make_t_i rt = Btype.interp_tbl rt
+let make_t_func ro t_i = Op.interp_tbl (mklApp ctval [|t_i|]) (fun cod dom value -> mklApp cTval [|t_i; mk_ftype cod dom; value|]) ro
+
+
+(******************************************************************************)
+(** Given a SMT-LIB2 file and a verit trace build                      *)
+(*  the corresponding object                                                  *)
+(******************************************************************************)
+
+
+let import_smtlib2 rt ro ra rf filename =
+  let chan = open_in filename in
+  let lexbuf = Lexing.from_channel chan in
+  let commands = Smtlib2_parse.main Smtlib2_lex.token lexbuf in
+  close_in chan;
+  match commands with
+    | None -> []
+    | Some (Smtlib2_ast.Commands (_,(_,res))) ->
+      List.rev (List.fold_left (Smtlib2_genConstr.declare_commands rt ro ra rf) [] res)
+
+
+let import_trace filename first =
+  let chan = open_in filename in
+  let lexbuf = Lexing.from_channel chan in
+  let confl_num = ref (-1) in
+  let first_num = ref (-1) in
+  let is_first = ref true in
+  let line = ref 1 in
+  (* let _ = Parsing.set_trace true in *)
+  try
+    while true do
+      confl_num := VeritParser.line VeritLexer.token lexbuf;
+      if !is_first then (
+        is_first := false;
+        first_num := !confl_num
+      );
+      incr line
+    done;
+    raise VeritLexer.Eof
+  with
+    | VeritLexer.Eof ->
+      close_in chan;
+      let first =
+        let aux = VeritSyntax.get_clause !first_num in
+        match first, aux.value with
+          | Some (root,l), Some (fl::nil) ->
+            if Form.equal l fl then
+              aux
+            else (
+              aux.kind <- Other (ImmFlatten(root,fl));
+              SmtTrace.link root aux;
+              root
+            )
+          | _,_ -> aux in
+      let confl = VeritSyntax.get_clause !confl_num in
+      SmtTrace.select confl;
+      (* Trace.share_prefix first (2 * last.id); *)
+      occur confl;
+      (alloc first, confl)
+    | Parsing.Parse_error -> failwith ("Verit.import_trace: parsing error line "^(string_of_int !line))
+
+
+let euf_checker_modules = [ ["SMTCoq";"Trace";"Euf_Checker"] ]
+
+let certif_ops = CoqTerms.make_certif_ops euf_checker_modules
+let cCertif = gen_constant euf_checker_modules "Certif"
+
+
+let clear_all () =
+  SmtTrace.clear ();
+  VeritSyntax.clear ()
+
+
+let compute_roots roots last_root =
+  let r = ref last_root in
+  while (has_prev !r) do
+    r := prev !r
+  done;
+
+  let rec find_root i root = function
+    | [] -> assert false
+    | t::q -> if Form.equal t root then (i,q) else find_root (i+1) root q in
+
+  let rec used_roots acc i roots r =
+    if isRoot r.kind then
+      match r.value with
+        | Some [root] ->
+          let (j,roots') = find_root i root roots in
+          used_roots (j::acc) (j+1) roots' (next r)
+        | _ -> assert false
+    else
+      acc in
+
+  used_roots [] 0 roots !r
+
+
+let parse_certif t_i t_func t_atom t_form root used_root trace fsmt fproof =
+  clear_all ();
+  let rt = Btype.create () in
+  let ro = Op.create () in
+  let ra = VeritSyntax.ra in
+  let rf = VeritSyntax.rf in
+  let roots = import_smtlib2 rt ro ra rf fsmt in
+  let (max_id, confl) = import_trace fproof None in
+  let (tres, last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in
+  let certif =
+   mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+  let ce4 =
+    { const_entry_body = certif;
+      const_entry_type = None;
+      const_entry_secctx = None;
+      const_entry_opaque = false;
+      const_entry_inline_code = false} in
+  let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in
+  let used_roots = compute_roots roots last_root in
+  let roots =
+    let res = Array.make (List.length roots + 1) (mkInt 0) in
+    let i = ref 0 in
+    List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
+    Term.mkArray (Lazy.force cint, res) in
+  let used_roots =
+    let l = List.length used_roots in
+    let res = Array.make (l + 1) (mkInt 0) in
+    let i = ref (l-1) in
+    List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; Term.mkArray (Lazy.force cint, res)|] in
+  let ce3 =
+    { const_entry_body = roots;
+      const_entry_type = None;
+      const_entry_secctx = None;
+      const_entry_opaque = false;
+      const_entry_inline_code = false} in
+  let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in
+  let ce3' =
+    { const_entry_body = used_roots;
+      const_entry_type = None;
+      const_entry_secctx = None;
+      const_entry_opaque = false;
+      const_entry_inline_code = false} in
+  let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in
+  let t_i' = make_t_i rt in
+  let t_func' = make_t_func ro t_i' in
+  let ce5 =
+    { const_entry_body = t_i';
+      const_entry_type = None;
+      const_entry_secctx = None;
+      const_entry_opaque = false;
+      const_entry_inline_code = false} in
+  let _ = declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition) in
+  let ce6 =
+    { const_entry_body = t_func';
+      const_entry_type = None;
+      const_entry_secctx = None;
+      const_entry_opaque = false;
+      const_entry_inline_code = false} in
+  let _ = declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition) in
+  let ce1 =
+    { const_entry_body = Atom.interp_tbl ra;
+      const_entry_type = None;
+      const_entry_secctx = None;
+      const_entry_opaque = false;
+      const_entry_inline_code = false} in
+  let _ = declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition) in
+  let ce2 =
+    { const_entry_body = snd (Form.interp_tbl rf);
+      const_entry_type = None;
+      const_entry_secctx = None;
+      const_entry_opaque = false;
+      const_entry_inline_code = false} in
+  let _ = declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition) in
+  ()
+
+
+let ccertif = gen_constant euf_checker_modules "certif"
+let cchecker = gen_constant euf_checker_modules "checker"
+let cchecker_correct = gen_constant euf_checker_modules "checker_correct"
+
+let interp_roots roots =
+  let interp = Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17) in
+  match roots with
+    | [] -> Lazy.force ctrue
+    | f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots
+
+let theorem name fsmt fproof =
+  clear_all ();
+  let rt = Btype.create () in
+  let ro = Op.create () in
+  let ra = VeritSyntax.ra in
+  let rf = VeritSyntax.rf in
+  let roots = import_smtlib2 rt ro ra rf fsmt in
+  let (max_id, confl) = import_trace fproof None in
+  let (tres,last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in
+  let certif =
+    mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+  let used_roots = compute_roots roots last_root in
+  let used_rootsCstr =
+    let l = List.length used_roots in
+    let res = Array.make (l + 1) (mkInt 0) in
+    let i = ref (l-1) in
+    List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; Term.mkArray (Lazy.force cint, res)|] in
+  let rootsCstr =
+    let res = Array.make (List.length roots + 1) (mkInt 0) in
+    let i = ref 0 in
+    List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
+    Term.mkArray (Lazy.force cint, res) in
+
+  let t_atom = Atom.interp_tbl ra in
+  let t_form = snd (Form.interp_tbl rf) in
+  let t_i = make_t_i rt in
+  let t_func = make_t_func ro t_i in
+
+  let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots roots|]|] in
+  let theorem_proof =
+   Term.mkLetIn (mkName "used_roots", used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], (*7*)
+   Term.mkLetIn (mkName "t_atom", t_atom, mklApp carray [|Lazy.force catom|], (*6*)
+   Term.mkLetIn (mkName "t_form", t_form, mklApp carray [|Lazy.force cform|], (*5*)
+   Term.mkLetIn (mkName "d", rootsCstr, mklApp carray [|Lazy.force cint|], (*4*)
+   Term.mkLetIn (mkName "c", certif, Lazy.force ccertif, (*3*)
+   Term.mkLetIn (mkName "t_i", t_i, mklApp carray [|Lazy.force ctyp_eqb|], (*2*)
+   Term.mkLetIn (mkName "t_func", t_func, mklApp carray [|mklApp ctval [|t_i|]|], (*1*)
+   mklApp cchecker_correct
+     [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3;
+	vm_cast_true
+	  (mklApp cchecker [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3|])|]))))))) in
+  let ce =
+    { const_entry_body = theorem_proof;
+      const_entry_type = Some theorem_concl;
+      const_entry_secctx = None;
+      const_entry_opaque = true;
+      const_entry_inline_code = false} in
+  let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in
+    ()
+
+
+let checker fsmt fproof =
+  let t1 = Unix.time () in  (* for debug *)
+  clear_all ();
+  let t2 = Unix.time () in  (* for debug *)
+  let rt = Btype.create () in
+  let ro = Op.create () in
+  let ra = VeritSyntax.ra in
+  let rf = VeritSyntax.rf in
+  let t3 = Unix.time () in  (* for debug *)
+  let roots = import_smtlib2 rt ro ra rf fsmt in
+  let t4 = Unix.time () in  (* for debug *)
+  let (max_id, confl) = import_trace fproof None in
+  let t5 = Unix.time () in  (* for debug *)
+  let (tres,last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in
+  let t6 = Unix.time () in  (* for debug *)
+  let certif =
+    mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+  let t7 = Unix.time () in  (* for debug *)
+  let used_roots = compute_roots roots last_root in
+  let t8 = Unix.time () in  (* for debug *)
+  let used_rootsCstr =
+    let l = List.length used_roots in
+    let res = Array.make (l + 1) (mkInt 0) in
+    let i = ref (l-1) in
+    List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; Term.mkArray (Lazy.force cint, res)|] in
+  let t9 = Unix.time () in  (* for debug *)
+  let rootsCstr =
+    let res = Array.make (List.length roots + 1) (mkInt 0) in
+    let i = ref 0 in
+    List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
+    Term.mkArray (Lazy.force cint, res) in
+  let t10 = Unix.time () in  (* for debug *)
+
+  let t_i = make_t_i rt in
+  let t11 = Unix.time () in  (* for debug *)
+  let t_func = make_t_func ro t_i in
+  let t12 = Unix.time () in  (* for debug *)
+  let t_atom = Atom.interp_tbl ra in
+  let t13 = Unix.time () in  (* for debug *)
+  let t_form = snd (Form.interp_tbl rf) in
+  let t14 = Unix.time () in  (* for debug *)
+
+  let tm = mklApp cchecker [|t_i; t_func; t_atom; t_form; rootsCstr; used_rootsCstr; certif|] in
+  let t15 = Unix.time () in  (* for debug *)
+
+  let res = Vnorm.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
+  let t16 = Unix.time () in  (* for debug *)
+  Format.eprintf "     = %s\n     : bool@."
+    (if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then
+        "true" else "false");
+  let t17 = Unix.time () in  (* for debug *)
+
+  (* let expr = Constrextern.extern_constr true Environ.empty_env tm in *)
+  (* let t16 = Unix.time () in  (\* for debug *\) *)
+  (* let res_aux1 = Glob_term.CbvVm None in *)
+  (* let t17 = Unix.time () in  (\* for debug *\) *)
+  (* let res_aux2 = Vernacexpr.VernacCheckMayEval(Some res_aux1, None, expr) in *)
+  (* let t18 = Unix.time () in  (\* for debug *\) *)
+  (* Vernacentries.interp res_aux2; *)
+  (* let t19 = Unix.time () in  (\* for debug *\) *)
+
+  if debug then (
+    Printf.printf"Clear: %f
+Create hashtables: %f
+Import SMT-LIB: %f
+Import trace: %f
+Compute trace: %f
+Build certif: %f
+Build roots: %f
+Compute used roots: %f
+Build used roots: %f
+Build  t_i: %f
+Build t_func: %f
+Build t_atom: %f
+Build t_form: %f
+Build checker call: %f
+Compute checker call: %f
+Print result: %f\n" (t2-.t1) (t3-.t2) (t4-.t3) (t5-.t4) (t6-.t5) (t7-.t6) (t8-.t7) (t9-.t8) (t10-.t9) (t11-.t10) (t12-.t11) (t13-.t12) (t14-.t13) (t15-.t14) (t16-.t15) (t17-.t16);
+(*     Printf.printf"Clear: %f *)
+(* Create hashtables: %f *)
+(* Import SMT-LIB: %f *)
+(* Import trace: %f *)
+(* Compute trace: %f *)
+(* Build certif: %f *)
+(* Build roots: %f *)
+(* Compute used roots: %f *)
+(* Build used roots: %f *)
+(* Build  t_i: %f *)
+(* Build t_func: %f *)
+(* Build t_atom: %f *)
+(* Build t_form: %f *)
+(* Build checker call: %f *)
+(* Build constr: %f *)
+(* Build conclusion1: %f *)
+(* Build conclusion2: %f *)
+(* Build conclusion: %f\n" (t2-.t1) (t3-.t2) (t4-.t3) (t5-.t4) (t6-.t5) (t7-.t6) (t8-.t7) (t9-.t8) (t10-.t9) (t11-.t10) (t12-.t11) (t13-.t12) (t14-.t13) (t15-.t14) (t16-.t15) (t17-.t16) (t18-.t17) (t19-.t18); *)
+    flush stdout)
+
+
+(******************************************************************************)
+(** Given a Coq formula build the proof                                       *)
+(******************************************************************************)
+
+let export out_channel rt ro l =
+  let fmt = Format.formatter_of_out_channel out_channel in
+  Format.fprintf fmt "(set-logic QF_UFLIA)@.";
+
+  List.iter (fun (i,t) ->
+    let s = "Tindex_"^(string_of_int i) in
+    VeritSyntax.add_btype s (Tindex t);
+    Format.fprintf fmt "(declare-sort %s 0)@." s
+  ) (Btype.to_list rt);
+
+  List.iter (fun (i,cod,dom,op) ->
+    let s = "op_"^(string_of_int i) in
+    VeritSyntax.add_fun s op;
+    Format.fprintf fmt "(declare-fun %s (" s;
+    let is_first = ref true in
+    Array.iter (fun t -> if !is_first then is_first := false else Format.fprintf fmt " "; Btype.to_smt fmt t) cod;
+    Format.fprintf fmt ") ";
+    Btype.to_smt fmt dom;
+    Format.fprintf fmt ")@."
+  ) (Op.to_list ro);
+
+  Format.fprintf fmt "(assert ";
+  Form.to_smt Atom.to_smt fmt l;
+  Format.fprintf fmt ")@\n(check-sat)@\n(exit)@."
+
+
+let call_verit rt ro fl root =
+  let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in
+  export outchan rt ro fl;
+  close_out outchan;
+  let logfilename = (Filename.chop_extension filename)^".vtlog" in
+
+  let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof="^logfilename^" "^filename in
+  Format.eprintf "%s@." command;
+  let t0 = Sys.time () in
+  let exit_code = Sys.command command in
+  let t1 = Sys.time () in
+  Format.eprintf "Verit = %.5f@." (t1-.t0);
+  if exit_code <> 0 then
+    failwith ("Verit.call_verit: command "^command^
+	      " exited with code "^(string_of_int exit_code));
+  try
+    import_trace logfilename (Some root)
+  with
+    | VeritSyntax.Sat -> Errors.error "veriT can't prove this"
+
+
+let cchecker_b_correct =
+  gen_constant euf_checker_modules "checker_b_correct"
+let cchecker_b = gen_constant euf_checker_modules "checker_b"
+let cchecker_eq_correct =
+  gen_constant euf_checker_modules "checker_eq_correct"
+let cchecker_eq = gen_constant euf_checker_modules "checker_eq"
+
+
+let build_body rt ro ra rf l b (max_id, confl) =
+  let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in
+  let certif =
+    mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+
+  let t_atom = Atom.interp_tbl ra in
+  let t_form = snd (Form.interp_tbl rf) in
+  let t_i = make_t_i rt in
+  let t_func = make_t_func ro t_i in
+
+  let ntatom = mkName "t_atom" in
+  let ntform = mkName "t_form" in
+  let nc = mkName "c" in
+  let nti = mkName "t_i" in
+  let ntfunc = mkName "t_func" in
+
+  let vtatom = Term.mkRel 5 in
+  let vtform = Term.mkRel 4 in
+  let vc = Term.mkRel 3 in
+  let vti = Term.mkRel 2 in
+  let vtfunc = Term.mkRel 1 in
+
+  Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+  Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+  Term.mkLetIn (nc, certif, Lazy.force ccertif,
+  Term.mkLetIn (nti, Term.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+  Term.mkLetIn (ntfunc, Term.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|],
+  mklApp cchecker_b_correct
+	 [|vti;vtfunc;vtatom; vtform; l; b; vc;
+	   vm_cast_true (mklApp cchecker_b [|vti;vtfunc;vtatom;vtform;l;b;vc|])|])))))
+
+
+let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
+  let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in
+  let certif =
+    mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+
+  let t_atom = Atom.interp_tbl ra in
+  let t_form = snd (Form.interp_tbl rf) in
+  let t_i = make_t_i rt in
+  let t_func = make_t_func ro t_i in
+
+  let ntatom = mkName "t_atom" in
+  let ntform = mkName "t_form" in
+  let nc = mkName "c" in
+  let nti = mkName "t_i" in
+  let ntfunc = mkName "t_func" in
+
+  let vtatom = Term.mkRel 5 in
+  let vtform = Term.mkRel 4 in
+  let vc = Term.mkRel 3 in
+  let vti = Term.mkRel 2 in
+  let vtfunc = Term.mkRel 1 in
+
+  Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+  Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+  Term.mkLetIn (nc, certif, Lazy.force ccertif,
+  Term.mkLetIn (nti, Term.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+  Term.mkLetIn (ntfunc, Term.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|],
+  mklApp cchecker_eq_correct
+	 [|vti;vtfunc;vtatom; vtform; l1; l2; l; vc;
+	   vm_cast_true (mklApp cchecker_eq [|vti;vtfunc;vtatom;vtform;l1;l2;l;vc|])|])))))
+
+
+let get_arguments concl =
+  let f, args = Term.decompose_app concl in
+  match args with
+  | [ty;a;b] when f = Lazy.force ceq && ty = Lazy.force cbool -> a, b
+  | [a] when f = Lazy.force cis_true -> a, Lazy.force ctrue
+  | _ -> failwith ("Verit.tactic: can only deal with equality over bool")
+
+
+let make_proof rt ro rf l =
+  let fl = Form.flatten rf l in
+  let root = SmtTrace.mkRootV [l] in
+  call_verit rt ro fl (root,l)
+
+
+let tactic gl =
+  clear_all ();
+  let rt = Btype.create () in
+  let ro = Op.create () in
+  let ra = VeritSyntax.ra in
+  let rf = VeritSyntax.rf in
+
+  let env = Tacmach.pf_env gl in
+  let sigma = Tacmach.project gl in
+  let t = Tacmach.pf_concl gl in
+
+  let (forall_let, concl) = Term.decompose_prod_assum t in
+  let env = Environ.push_rel_context forall_let env in
+  let a, b = get_arguments concl in
+  let body =
+    if (b = Lazy.force ctrue || b = Lazy.force cfalse) then
+      let l = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
+      let l' = if b = Lazy.force ctrue then Form.neg l else l in
+      let max_id_confl = make_proof rt ro rf l' in
+      build_body rt ro ra rf (Form.to_coq l) b max_id_confl
+    else
+      let l1 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
+      let l2 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf b in
+      let l = Form.neg (Form.get rf (Fapp(Fiff,[|l1;l2|]))) in
+      let max_id_confl = make_proof rt ro rf l in
+      build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in
+  let compose_lam_assum forall_let body =
+    List.fold_left (fun t rd -> Term.mkLambda_or_LetIn rd t) body forall_let in
+  let res = compose_lam_assum forall_let body in
+  Tactics.exact_no_check res gl
diff --git a/src/verit/veritLexer.mll b/src/verit/veritLexer.mll
new file mode 100644
index 0000000..3314fae
--- /dev/null
+++ b/src/verit/veritLexer.mll
@@ -0,0 +1,148 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+{
+  open VeritParser
+  exception Eof
+
+  let typ_table = Hashtbl.create 53
+  let _ =
+    List.iter (fun (kwd, tok) -> Hashtbl.add typ_table kwd tok)
+      [ "input", INPU;
+        "deep_res", DEEP;
+        "true", TRUE;
+        "false", FALS;
+        "and_pos", ANDP;
+        "and_neg", ANDN;
+        "or_pos", ORP;
+        "or_neg", ORN;
+        "xor_pos1", XORP1;
+        "xor_pos2", XORP2;
+        "xor_neg1", XORN1;
+        "xor_neg2", XORN2;
+        "implies_pos", IMPP;
+        "implies_neg1", IMPN1;
+        "implies_neg2", IMPN2;
+        "equiv_pos1", EQUP1;
+        "equiv_pos2", EQUP2;
+        "equiv_neg1", EQUN1;
+        "equiv_neg2", EQUN2;
+        "ite_pos1", ITEP1;
+        "ite_pos2", ITEP2;
+        "ite_neg1", ITEN1;
+        "ite_neg2", ITEN2;
+        "eq_reflexive", EQRE;
+        "eq_transitive", EQTR;
+        "eq_congruent", EQCO;
+        "eq_congruent_pred", EQCP;
+        "dl_generic", DLGE;
+        "lia_generic", LAGE;
+        "la_generic", LAGE;
+        "la_tautology", LATA;
+        "dl_disequality", DLDE;
+        "la_disequality", LADE;
+        "forall_inst", FINS;
+        "exists_inst", EINS;
+        "skolem_ex_ax", SKEA;
+        "skolem_all_ax", SKAA;
+        "qnt_simplify_ax", QNTS;
+        "qnt_merge_ax", QNTM;
+        "resolution", RESO;
+        "and", AND;
+        "not_or", NOR;
+        "or", OR;
+        "not_and", NAND;
+        "xor1", XOR1;
+        "xor2", XOR2;
+        "not_xor1", NXOR1;
+        "not_xor2", NXOR2;
+        "implies", IMP;
+        "not_implies1", NIMP1;
+        "not_implies2", NIMP2;
+        "equiv1", EQU1;
+        "equiv2", EQU2;
+        "not_equiv1", NEQU1;
+        "not_equiv2", NEQU2;
+        "ite1", ITE1;
+        "ite2", ITE2;
+        "not_ite1", NITE1;
+        "not_ite2", NITE2;
+        "tmp_alphaconv", TPAL;
+        "tmp_LA_pre", TLAP;
+        "tmp_let_elim", TPLE;
+        "tmp_nary_elim", TPNE;
+        "tmp_distinct_elim", TPDE;
+        "tmp_simp_arith", TPSA;
+        "tmp_ite_elim", TPIE;
+        "tmp_macrosubst", TPMA;
+        "tmp_betared", TPBR;
+        "tmp_bfun_elim", TPBE;
+        "tmp_sk_connector", TPSC;
+        "tmp_pm_process", TPPP;
+        "tmp_qnt_tidy", TPQT;
+        "tmp_qnt_simplify", TPQS;
+        "tmp_skolemize", TPSK;
+        "subproof", SUBP ]
+}
+
+
+let digit = [ '0'-'9' ]
+let alpha = [ 'a'-'z' 'A' - 'Z' ]
+let blank = [' ' '\t']
+let newline = ['\n' '\r']
+let var = alpha (alpha|digit|'_')*
+let bindvar = '?' var+
+let int = '-'? digit+
+
+
+rule token = parse
+  | blank +                    { token lexbuf }
+  | newline +                  { EOL }
+
+  | ":"                        { COLON }
+  | "#"                        { SHARP }
+
+  | "("                        { LPAR }
+  | ")"                        { RPAR }
+
+  | "not"                      { NOT }
+  | "xor"                      { XOR }
+  | "ite"                      { ITE }
+  | "="                        { EQ }
+  | "<"                        { LT }
+  | "<="                       { LEQ }
+  | ">"                        { GT }
+  | ">="                       { GEQ }
+  | "+"                        { PLUS }
+  | "-"                        { MINUS }
+  | "~"                        { OPP }
+  | "*"                        { MULT }
+  | "=>"                       { IMP }
+  | "let"                      { LET }
+  | "distinct"                 { DIST }
+
+  | "Formula is Satisfiable"   { SAT }
+
+  | int                        { try INT (int_of_string (Lexing.lexeme lexbuf))
+	                         with _ -> 
+                                   BIGINT 
+                                     (Big_int.big_int_of_string 
+					(Lexing.lexeme lexbuf)) }
+  | var                        { let v = Lexing.lexeme lexbuf in
+                                 try Hashtbl.find typ_table v with
+                                   | Not_found -> VAR v }
+  | bindvar                    { BINDVAR (Lexing.lexeme lexbuf) }
+
+  | eof                        { raise Eof }
diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly
new file mode 100644
index 0000000..f36b857
--- /dev/null
+++ b/src/verit/veritParser.mly
@@ -0,0 +1,204 @@
+/**************************************************************************/
+/*                                                                        */
+/*     SMTCoq                                                             */
+/*     Copyright (C) 2011 - 2015                                          */
+/*                                                                        */
+/*     Michaël Armand                                                     */
+/*     Benjamin Grégoire                                                  */
+/*     Chantal Keller                                                     */
+/*                                                                        */
+/*     Inria - École Polytechnique - MSR-Inria Joint Lab                  */
+/*                                                                        */
+/*   This file is distributed under the terms of the CeCILL-C licence     */
+/*                                                                        */
+/**************************************************************************/
+
+%{
+  open SmtAtom
+  open SmtForm
+  open VeritSyntax
+%}
+
+
+/*
+  définition des lexèmes
+*/
+
+%token EOL SAT
+%token COLON SHARP
+%token LPAR RPAR
+%token NOT XOR ITE EQ LT LEQ GT GEQ PLUS MINUS MULT OPP LET DIST
+%token 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
+%token <int> INT
+%token <Big_int.big_int> BIGINT
+%token <string> VAR BINDVAR
+
+/* type de "retour" du parseur : une clause */
+%type <int> line
+%start line
+
+
+%%
+
+line:
+  | SAT                                                    { raise Sat }
+  | INT COLON LPAR typ clause                   RPAR EOL   { mk_clause ($1,$4,$5,[]) }
+  | INT COLON LPAR typ clause clause_ids_params RPAR EOL   { mk_clause ($1,$4,$5,$6) }
+;
+
+typ:
+  | INPU                                                   { Inpu  }
+  | DEEP                                                   { Deep  }
+  | TRUE                                                   { True  }
+  | FALS                                                   { Fals  }
+  | ANDP                                                   { Andp  }
+  | ANDN                                                   { Andn  }
+  | ORP                                                    { Orp   }
+  | ORN                                                    { Orn   }
+  | XORP1                                                  { Xorp1 }
+  | XORP2                                                  { Xorp2 }
+  | XORN1                                                  { Xorn1 }
+  | XORN2                                                  { Xorn2 }
+  | IMPP                                                   { Impp  }
+  | IMPN1                                                  { Impn1 }
+  | IMPN2                                                  { Impn2 }
+  | EQUP1                                                  { Equp1 }
+  | EQUP2                                                  { Equp2 }
+  | EQUN1                                                  { Equn1 }
+  | EQUN2                                                  { Equn2 }
+  | ITEP1                                                  { Itep1 }
+  | ITEP2                                                  { Itep2 }
+  | ITEN1                                                  { Iten1 }
+  | ITEN2                                                  { Iten2 }
+  | EQRE                                                   { Eqre  }
+  | EQTR                                                   { Eqtr  }
+  | EQCO                                                   { Eqco  }
+  | EQCP                                                   { Eqcp  }
+  | DLGE                                                   { Dlge  }
+  | LAGE                                                   { Lage  }
+  | LATA                                                   { Lata  }
+  | DLDE                                                   { Dlde  }
+  | LADE                                                   { Lade  }
+  | FINS                                                   { Fins  }
+  | EINS                                                   { Eins  }
+  | SKEA                                                   { Skea  }
+  | SKAA                                                   { Skaa  }
+  | QNTS                                                   { Qnts  }
+  | QNTM                                                   { Qntm  }
+  | RESO                                                   { Reso  }
+  | AND                                                    { And   }
+  | NOR                                                    { Nor   }
+  | OR                                                     { Or    }
+  | NAND                                                   { Nand  }
+  | XOR1                                                   { Xor1  }
+  | XOR2                                                   { Xor2  }
+  | NXOR1                                                  { Nxor1 }
+  | NXOR2                                                  { Nxor2 }
+  | IMP                                                    { Imp   }
+  | NIMP1                                                  { Nimp1 }
+  | NIMP2                                                  { Nimp2 }
+  | EQU1                                                   { Equ1  }
+  | EQU2                                                   { Equ2  }
+  | NEQU1                                                  { Nequ1 }
+  | NEQU2                                                  { Nequ2 }
+  | ITE1                                                   { Ite1  }
+  | ITE2                                                   { Ite2  }
+  | NITE1                                                  { Nite1 }
+  | NITE2                                                  { Nite2 }
+  | TPAL                                                   { Tpal  }
+  | TLAP                                                   { Tlap  }
+  | TPLE                                                   { Tple  }
+  | TPNE                                                   { Tpne  }
+  | TPDE                                                   { Tpde  }
+  | TPSA                                                   { Tpsa  }
+  | TPIE                                                   { Tpie  }
+  | TPMA                                                   { Tpma  }
+  | TPBR                                                   { Tpbr  }
+  | TPBE                                                   { Tpbe  }
+  | TPSC                                                   { Tpsc  }
+  | TPPP                                                   { Tppp  }
+  | TPQT                                                   { Tpqt  }
+  | TPQS                                                   { Tpqs  }
+  | TPSK                                                   { Tpsk  }
+  | SUBP                                                   { Subp  }
+;
+
+clause:
+  | LPAR          RPAR                                     { [] }
+  | LPAR lit_list RPAR                                     { $2 }
+;
+
+lit_list:
+  | lit                                                    { [$1] }
+  | lit lit_list                                           { $1::$2 }
+;
+
+lit:   /* returns a SmtAtom.Form.t */
+  | name_term                                              { lit_of_atom_form_lit rf $1 }
+  | LPAR NOT lit RPAR                                      { Form.neg $3 }
+;
+
+name_term:   /* returns a SmtAtom.Form.pform or a SmtAtom.hatom */
+  | SHARP INT                                              { get_solver $2 }
+  | SHARP INT COLON LPAR term RPAR                         { let res = $5 in add_solver $2 res; res }
+  | TRUE                                                   { Form Form.pform_true }
+  | FALS                                                   { Form Form.pform_false }
+  | VAR                                                    { Atom (Atom.get ra (Aapp (get_fun $1,[||]))) }
+  | BINDVAR                                                { Hashtbl.find hlets $1 }
+  | INT                                                    { Atom (Atom.hatom_Z_of_int ra $1) }
+  | BIGINT                                                 { Atom (Atom.hatom_Z_of_bigint ra $1) }
+;
+
+term:   /* returns a SmtAtom.Form.pform or a SmtAtom.hatom */
+  | LPAR term RPAR                                         { $2 }
+
+  /* Formulae */
+  | TRUE                                                   { Form Form.pform_true }
+  | FALS                                                   { Form Form.pform_false }
+  | AND lit_list                                           { Form (Fapp (Fand, Array.of_list $2)) }
+  | OR lit_list                                            { Form (Fapp (For, Array.of_list $2)) }
+  | IMP lit_list                                           { Form (Fapp (Fimp, Array.of_list $2)) }
+  | XOR lit_list                                           { Form (Fapp (Fxor, Array.of_list $2)) }
+  | ITE lit_list                                           { Form (Fapp (Fite, Array.of_list $2)) }
+
+  /* Atoms */
+  | INT                                                    { Atom (Atom.hatom_Z_of_int ra $1) }
+  | BIGINT                                                 { Atom (Atom.hatom_Z_of_bigint ra $1) }
+  | LT name_term name_term                                 { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_lt ra h1 h2) | _,_ -> assert false }
+  | LEQ name_term name_term                                { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_le ra h1 h2) | _,_ -> assert false }
+  | GT name_term name_term                                 { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_gt ra h1 h2) | _,_ -> assert false }
+  | GEQ name_term name_term                                { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_ge ra h1 h2) | _,_ -> assert false }
+  | PLUS name_term name_term                               { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_plus ra h1 h2) | _,_ -> assert false }
+  | MULT name_term name_term                               { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_mult ra h1 h2) | _,_ -> assert false }
+  | MINUS name_term name_term                              { match $2,$3 with |Atom h1, Atom h2 -> Atom (Atom.mk_minus ra h1 h2) | _,_ -> assert false }
+  | MINUS name_term                                        { match $2 with | Atom h -> Atom (Atom.mk_opp ra h) | _ -> assert false }
+  | OPP name_term                                          { match $2 with | Atom h -> Atom (Atom.mk_opp ra h) | _ -> assert false }
+  | DIST args                                              { let a = Array.of_list $2 in Atom (Atom.mk_distinct ra (Atom.type_of a.(0)) a) }
+  | VAR                                                    { Atom (Atom.get ra (Aapp (get_fun $1, [||]))) }
+  | VAR args                                               { Atom (Atom.get ra (Aapp (get_fun $1, Array.of_list $2))) }
+
+  /* Both */
+  | EQ name_term name_term                                 { let t1 = $2 in let t2 = $3 in match t1,t2 with | Atom h1, Atom h2 when (match Atom.type_of h1 with | Tbool -> false | _ -> true) -> Atom (Atom.mk_eq ra (Atom.type_of h1) h1 h2) | _, _ -> Form (Fapp (Fiff, [|lit_of_atom_form_lit rf t1; lit_of_atom_form_lit rf t2|])) }
+  | LET LPAR bindlist RPAR name_term                       { $3; $5 }
+  | BINDVAR                                                { Hashtbl.find hlets $1 }
+;
+
+bindlist:
+  | LPAR BINDVAR name_term RPAR                            { Hashtbl.add hlets $2 $3 }
+  | LPAR BINDVAR lit RPAR                                  { Hashtbl.add hlets $2 (Lit $3) }
+  | LPAR BINDVAR name_term RPAR bindlist                   { Hashtbl.add hlets $2 $3; $5 }
+  | LPAR BINDVAR lit RPAR bindlist                         { Hashtbl.add hlets $2 (Lit $3); $5 }
+
+args:
+  | name_term                                              { match $1 with Atom h -> [h] | _ -> assert false }
+  | name_term args                                         { match $1 with Atom h -> h::$2 | _ -> assert false }
+;
+
+clause_ids_params:
+  | int_list                                               { $1 }
+;
+
+int_list:
+  | INT                                                    { [$1] }
+  | INT int_list                                           { let x1 = $1 in let x2 = $2 in x1::x2 }
+;
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
new file mode 100644
index 0000000..c60d34f
--- /dev/null
+++ b/src/verit/veritSyntax.ml
@@ -0,0 +1,355 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+open SmtAtom
+open SmtForm
+open SmtCertif
+open SmtTrace
+
+
+(*** Syntax of veriT proof traces ***)
+
+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
+
+
+(* About equality *)
+
+let get_eq l =
+  match Form.pform l with
+    | Fatom ha ->
+      (match Atom.atom ha with
+        | Abop (BO_eq _,a,b) -> (a,b)
+        | _ -> failwith "VeritSyntax.get_eq: equality was expected")
+    | _ -> failwith "VeritSyntax.get_eq: equality was expected"
+
+let get_at l =
+  match Form.pform l with
+    | Fatom ha -> ha
+    | _ -> failwith "VeritSyntax.get_eq: equality was expected"
+
+let is_eq l =
+  match Form.pform l with
+    | Fatom ha ->
+      (match Atom.atom ha with
+        | Abop (BO_eq _,_,_) -> true
+        | _ -> false)
+    | _ -> failwith "VeritSyntax.get_eq: atom was expected"
+
+
+(* Transitivity *)
+
+let rec process_trans a b prem res =
+  try
+    let (l,(c,c')) = List.find (fun (l,(a',b')) -> (a' = b || b' = b)) prem in
+    let prem = List.filter (fun l' -> l' <> (l,(c,c'))) prem in
+    let c = if c = b then c' else c in
+    if a = c
+    then List.rev (l::res)
+    else process_trans a c prem (l::res)
+  with
+    |Not_found -> if a = b then [] else assert false
+
+
+let mkTrans p =
+  let (concl,prem) = List.partition Form.is_pos p in
+  match concl with
+    |[c] ->
+      let a,b = get_eq c in
+      let prem_val = List.map (fun l -> (l,get_eq l)) prem in
+      let cert = (process_trans a b prem_val []) in
+      Other (EqTr (c,cert))
+    |_ -> failwith "VeritSyntax.mkTrans: no conclusion or more than one conclusion in transitivity"
+
+
+(* Congruence *)
+
+let rec process_congr a_args b_args prem res =
+  match a_args,b_args with
+    | a::a_args,b::b_args ->
+      (* if a = b *)
+      (* then process_congr a_args b_args prem (None::res) *)
+      (* else *)
+        let (l,(a',b')) = List.find (fun (l,(a',b')) -> (a = a' && b = b')||(a = b' && b = a')) prem in
+        process_congr a_args b_args prem ((Some l)::res)
+    | [],[] -> List.rev res
+    | _ -> failwith "VeritSyntax.process_congr: incorrect number of arguments in function application"
+
+
+let mkCongr p =
+  let (concl,prem) = List.partition Form.is_pos p in
+  match concl with
+    |[c] ->
+      let a,b = get_eq c in
+      let prem_val = List.map (fun l -> (l,get_eq l)) prem in
+      (match Atom.atom a, Atom.atom b with
+        | Abop(aop,a1,a2), Abop(bop,b1,b2) when (aop = bop) ->
+          let a_args = [a1;a2] in
+          let b_args = [b1;b2] in
+          let cert = process_congr a_args b_args prem_val [] in
+          Other (EqCgr (c,cert))
+        | Auop (aop,a), Auop (bop,b) when (aop = bop) ->
+          let a_args = [a] in
+          let b_args = [b] in
+          let cert = process_congr a_args b_args prem_val [] in
+          Other (EqCgr (c,cert))
+        | Aapp (a_f,a_args), Aapp (b_f,b_args) ->
+          if a_f = b_f then
+            let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in
+            Other (EqCgr (c,cert))
+          else failwith "VeritSyntax.mkCongr: left function is different from right fucntion"
+        | _, _ -> failwith "VeritSyntax.mkCongr: atoms are not applications")
+    |_ -> failwith "VeritSyntax.mkCongr: no conclusion or more than one conclusion in congruence"
+
+
+let mkCongrPred p =
+  let (concl,prem) = List.partition Form.is_pos p in
+  let (prem,prem_P) = List.partition is_eq prem in
+  match concl with
+    |[c] ->
+      (match prem_P with
+        |[p_p] ->
+          let prem_val = List.map (fun l -> (l,get_eq l)) prem in
+          (match Atom.atom (get_at c), Atom.atom (get_at p_p) with
+            | Abop(aop,a1,a2), Abop(bop,b1,b2) when (aop = bop) ->
+              let a_args = [a1;a2] in
+              let b_args = [b1;b2] in
+              let cert = process_congr a_args b_args prem_val [] in
+              Other (EqCgrP (p_p,c,cert))
+            | Aapp (a_f,a_args), Aapp (b_f,b_args) ->
+              if a_f = b_f then
+                let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in
+                Other (EqCgrP (p_p,c,cert))
+              else failwith "VeritSyntax.mkCongrPred: unmatching predicates"
+            | _ -> failwith "VeritSyntax.mkCongrPred : not pred app")
+        |_ ->  failwith "VeritSyntax.mkCongr: no or more than one predicate app premice in congruence")
+    |[] ->  failwith "VeritSyntax.mkCongrPred: no conclusion in congruence"
+    |_ -> failwith "VeritSyntax.mkCongrPred: more than one conclusion in congruence"
+
+
+(* Linear arithmetic *)
+
+let mkMicromega cl =
+  let _tbl, _f, cert = Lia.build_lia_certif cl in
+  let c =
+    match cert with
+      | None -> failwith "VeritSyntax.mkMicromega: micromega can't solve this"
+      | Some c -> c in
+  Other (LiaMicromega (cl,c))
+
+
+let mkSplArith orig cl =
+  let res =
+    match cl with
+      | res::nil -> res
+      | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the resulting clause" in
+  try
+    let orig' =
+      match orig.value with
+        | Some [orig'] -> orig'
+        | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the premise clause" in
+    let _tbl, _f, cert = Lia.build_lia_certif [Form.neg orig';res] in
+    let c =
+      match cert with
+        | None -> failwith "VeritSyntax.mkSplArith: micromega can't solve this"
+        | Some c -> c in
+    Other (SplArith (orig,res,c))
+  with
+    | _ -> Other (ImmFlatten (orig, res))
+
+
+(* Elimination of operators *)
+
+let mkDistinctElim old value =
+  let rec find_res l1 l2 =
+    match l1,l2 with
+      | t1::q1,t2::q2 -> if t1 == t2 then find_res q1 q2 else t2
+      | _, _ -> assert false in
+  let l1 = match old.value with
+    | Some l -> l
+    | None -> assert false in
+  Other (SplDistinctElim (old,find_res l1 value))
+
+
+(* Generating clauses *)
+
+let clauses : (int,Form.t clause) Hashtbl.t = Hashtbl.create 17
+let get_clause id =
+  try Hashtbl.find clauses id
+  with | Not_found -> failwith ("VeritSyntax.get_clause : clause number "^(string_of_int id)^" not found\n")
+let add_clause id cl = Hashtbl.add clauses id cl
+let clear_clauses () = Hashtbl.clear clauses
+
+let mk_clause (id,typ,value,ids_params) =
+  let kind =
+    match typ with
+      (* 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 | Or | 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)
+      (* Resolution *)
+      | Reso ->
+        (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
+          | _ -> 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)
+       (* Not implemented *)
+      | Deep -> failwith "VeritSyntax.ml: rule deep_res not implemented yet"
+      | Fins -> failwith "VeritSyntax.ml: rule forall_inst 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"
+      | Tpbr -> failwith "VeritSyntax.ml: rule tmp_betared 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"
+      | Tpqt -> failwith "VeritSyntax.ml: rule tmp_qnt_tidy 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 *)
+    if SmtTrace.isRoot kind then SmtTrace.mkRootV value
+    else SmtTrace.mk_scertif kind (Some value) in
+  add_clause id cl;
+  if id > 1 then SmtTrace.link (get_clause (id-1)) cl;
+  id
+
+
+type atom_form_lit =
+  | Atom of SmtAtom.Atom.t
+  | Form of SmtAtom.Form.pform
+  | Lit of SmtAtom.Form.t
+
+let lit_of_atom_form_lit rf = function
+  | Atom a -> Form.get rf (Fatom a)
+  | Form f -> Form.get rf f
+  | Lit l -> l
+
+let solver : (int,atom_form_lit) Hashtbl.t = Hashtbl.create 17
+let get_solver id =
+  try Hashtbl.find solver id
+  with | Not_found -> failwith ("VeritSyntax.get_solver : solver variable number "^(string_of_int id)^" not found\n")
+let add_solver id cl = Hashtbl.add solver id cl
+let clear_solver () = Hashtbl.clear solver
+
+let btypes : (string,btype) Hashtbl.t = Hashtbl.create 17
+let get_btype id =
+  try Hashtbl.find btypes id
+  with | Not_found -> failwith ("VeritSyntax.get_btype : sort symbol \""^id^"\" not found\n")
+let add_btype id cl = Hashtbl.add btypes id cl
+let clear_btypes () = Hashtbl.clear btypes
+
+let funs : (string,indexed_op) Hashtbl.t = Hashtbl.create 17
+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 clear_funs () = Hashtbl.clear funs
+
+
+let ra = Atom.create ()
+let rf = Form.create ()
+
+let hlets : (string, atom_form_lit) Hashtbl.t = Hashtbl.create 17
+
+
+let clear () =
+  clear_clauses ();
+  clear_solver ();
+  clear_btypes ();
+  clear_funs ();
+  Atom.clear ra;
+  Form.clear rf;
+  Hashtbl.clear hlets
diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli
new file mode 100644
index 0000000..9813b54
--- /dev/null
+++ b/src/verit/veritSyntax.mli
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+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
+
+val get_clause : int -> SmtAtom.Form.t SmtCertif.clause
+val add_clause : int -> SmtAtom.Form.t SmtCertif.clause -> unit
+
+val mk_clause : SmtCertif.clause_id * typ * SmtAtom.Form.t list * SmtCertif.clause_id list -> SmtCertif.clause_id
+
+type atom_form_lit =
+  | Atom of SmtAtom.Atom.t
+  | Form of SmtAtom.Form.pform
+  | Lit of SmtAtom.Form.t
+val lit_of_atom_form_lit : SmtAtom.Form.reify -> atom_form_lit -> SmtAtom.Form.t
+val get_solver : int -> atom_form_lit
+val add_solver : int -> atom_form_lit -> unit
+
+val get_btype : string -> SmtAtom.btype
+val add_btype : string -> SmtAtom.btype -> unit
+
+val get_fun : string -> SmtAtom.indexed_op
+val add_fun : string -> SmtAtom.indexed_op -> unit
+
+val ra : SmtAtom.Atom.reify_tbl
+val rf : SmtAtom.Form.reify
+
+val hlets : (string, atom_form_lit) Hashtbl.t
+
+val clear : unit -> unit