Separate verit input (smtlib2) from output

5 files changed, 831 insertions, 0 deletions

diff --git a/src/smtlib2/smtlib2_ast.ml b/src/smtlib2/smtlib2_ast.ml
new file mode 100644
index 0000000..cce4625
--- /dev/null
+++ b/src/smtlib2/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/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
new file mode 100644
index 0000000..f11d650
--- /dev/null
+++ b/src/smtlib2/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/smtlib2/smtlib2_lex.mll b/src/smtlib2/smtlib2_lex.mll
new file mode 100644
index 0000000..f235403
--- /dev/null
+++ b/src/smtlib2/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/smtlib2/smtlib2_parse.mly b/src/smtlib2/smtlib2_parse.mly
new file mode 100644
index 0000000..b4e02a7
--- /dev/null
+++ b/src/smtlib2/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/smtlib2/smtlib2_util.ml b/src/smtlib2/smtlib2_util.ml
new file mode 100644
index 0000000..1ce5e46
--- /dev/null
+++ b/src/smtlib2/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;;