path: root/src/trace/smtAtom.ml

(**************************************************************************)
(*                                                                        *)
(*     SMTCoq                                                             *)
(*     Copyright (C) 2011 - 2021                                          *)
(*                                                                        *)
(*     See file "AUTHORS" for the list of authors                         *)
(*                                                                        *)
(*   This file is distributed under the terms of the CeCILL-C licence     *)
(*                                                                        *)
(**************************************************************************)


open SmtMisc
open CoqTerms


(** Hashing functions on Btypes *)

module HashBtype = Hashtbl.Make(SmtBtype.HashedBtype)

module HashedBtypePair : Hashtbl.HashedType
       with type t = SmtBtype.btype * SmtBtype.btype = struct
  type t = SmtBtype.btype * SmtBtype.btype

  let equal (t1,s1) (t2,s2) =
    SmtBtype.HashedBtype.equal t1 t2 && SmtBtype.HashedBtype.equal s1 s2

  let hash (t,s) =
    ((SmtBtype.HashedBtype.hash t) lsl 3) land (SmtBtype.HashedBtype.hash s)
end

module HashBtypePair = Hashtbl.Make(HashedBtypePair)


(** Operators *)

type cop =
   | CO_xH
   | CO_Z0
   | CO_BV of bool list

type uop =
   | UO_xO
   | UO_xI
   | UO_Zpos
   | UO_Zneg
   | UO_Zopp
   | UO_BVbitOf of int * int
   | UO_BVnot of int
   | UO_BVneg of int
   | UO_BVextr of int * int * int
   | UO_BVzextn of int * int
   | UO_BVsextn of int * int

type bop =
   | BO_Zplus
   | BO_Zminus
   | BO_Zmult
   | BO_Zlt
   | BO_Zle
   | BO_Zge
   | BO_Zgt
   | BO_eq of SmtBtype.btype
   | BO_BVand of int
   | BO_BVor of int
   | BO_BVxor of int
   | BO_BVadd of int
   | BO_BVmult of int
   | BO_BVult of int
   | BO_BVslt of int
   | BO_BVconcat of int * int
   | BO_BVshl of int
   | BO_BVshr of int
   | BO_select of SmtBtype.btype * SmtBtype.btype
   | BO_diffarray of SmtBtype.btype * SmtBtype.btype


type top =
  | TO_store of SmtBtype.btype * SmtBtype.btype


type nop =
  | NO_distinct of SmtBtype.btype

type op_def = {
    tparams : SmtBtype.btype array;
    tres : SmtBtype.btype;
    op_val : CoqInterface.constr }

type index = Index of int
           | Rel_name of string

type indexed_op = index * op_def

let destruct s (i, hval) = match i with
    | Index index -> index, hval
    | Rel_name _ -> failwith s

let dummy_indexed_op i dom codom =
  (i, {tparams = dom; tres = codom; op_val = CoqInterface.mkProp})

let indexed_op_index i =
  let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in
  index

let debruijn_indexed_op i ty =
  (Index i, {tparams = [||]; tres = ty; op_val = CoqInterface.mkRel i})

module Op =
  struct
    let c_to_coq = function
      | CO_xH -> Lazy.force cCO_xH
      | CO_Z0 -> Lazy.force cCO_Z0
      | CO_BV bv -> mklApp cCO_BV [|mk_bv_list bv; mkN (List.length bv)|]

    let c_type_of = function
      | CO_xH -> SmtBtype.Tpositive
      | CO_Z0 -> SmtBtype.TZ
      | CO_BV bv -> SmtBtype.TBV (List.length bv)

    let interp_cop = function
      | CO_xH -> Lazy.force cxH
      | CO_Z0 -> Lazy.force cZ0
      | CO_BV bv -> mklApp cof_bits [|mk_bv_list bv|]

    let u_to_coq = function
      | UO_xO -> Lazy.force cUO_xO
      | UO_xI -> Lazy.force cUO_xI
      | UO_Zpos -> Lazy.force cUO_Zpos
      | UO_Zneg -> Lazy.force cUO_Zneg
      | UO_Zopp -> Lazy.force cUO_Zopp
      | UO_BVbitOf (s, i) -> mklApp cUO_BVbitOf [|mkN s; mkNat i|]
      | UO_BVnot s -> mklApp cUO_BVnot [|mkN s|]
      | UO_BVneg s -> mklApp cUO_BVneg [|mkN s|]
      | UO_BVextr (i, n, s) -> mklApp cUO_BVextr [|mkN i; mkN n; mkN s|]
      | UO_BVzextn (s, n) -> mklApp cUO_BVzextn [|mkN s; mkN n|]
      | UO_BVsextn (s, n) -> mklApp cUO_BVsextn [|mkN s; mkN n|]

    let u_type_of = function
      | UO_xO | UO_xI -> SmtBtype.Tpositive
      | UO_Zpos | UO_Zneg | UO_Zopp -> SmtBtype.TZ
      | UO_BVbitOf _ -> SmtBtype.Tbool
      | UO_BVnot s | UO_BVneg s -> SmtBtype.TBV s
      | UO_BVextr (_, n, _) -> SmtBtype.TBV n
      | UO_BVzextn (s, n) | UO_BVsextn (s, n) -> SmtBtype.TBV (s + n)

    let u_type_arg = function
      | UO_xO | UO_xI | UO_Zpos | UO_Zneg -> SmtBtype.Tpositive
      | UO_Zopp -> SmtBtype.TZ
      | UO_BVbitOf (s,_) -> SmtBtype.TBV s
      | UO_BVnot s | UO_BVneg s -> SmtBtype.TBV s
      | UO_BVextr (_, _, s) -> SmtBtype.TBV s
      | UO_BVzextn (s, _) | UO_BVsextn (s, _) -> SmtBtype.TBV s


    let interp_uop = function
      | UO_xO -> Lazy.force cxO
      | UO_xI -> Lazy.force cxI
      | UO_Zpos -> Lazy.force cZpos
      | UO_Zneg -> Lazy.force cZneg
      | UO_Zopp -> Lazy.force copp
      | UO_BVbitOf (s,i) -> mklApp cbitOf [|mkN s; mkNat i|]
      | UO_BVnot s -> mklApp cbv_not [|mkN s|]
      | UO_BVneg s -> mklApp cbv_neg [|mkN s|]
      | UO_BVextr (i, n, s) -> mklApp cbv_extr [|mkN i; mkN n; mkN s|]
      | UO_BVzextn (s, n) -> mklApp cbv_zextn [|mkN s; mkN n|]
      | UO_BVsextn (s, n) -> mklApp cbv_sextn [|mkN s; mkN n|]

    let eq_tbl = HashBtype.create 17
    let select_tbl = HashBtypePair.create 17
    let store_tbl = HashBtypePair.create 17
    let diffarray_tbl = HashBtypePair.create 17

    let eq_to_coq t =
      try HashBtype.find eq_tbl t
      with Not_found ->
	let op = mklApp cBO_eq [|SmtBtype.to_coq t|] in
	HashBtype.add eq_tbl t op;
	op

    let select_to_coq ti te =
      try HashBtypePair.find select_tbl (ti, te)
      with Not_found ->
        let op = mklApp cBO_select [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in
        HashBtypePair.add select_tbl (ti, te) op;
        op

    let store_to_coq ti te =
      try HashBtypePair.find store_tbl (ti, te)
      with Not_found ->
        let op = mklApp cTO_store [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in
        HashBtypePair.add store_tbl (ti, te) op;
        op

    let diffarray_to_coq ti te =
      try HashBtypePair.find diffarray_tbl (ti, te)
      with Not_found ->
        let op = mklApp cBO_diffarray [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in
        HashBtypePair.add diffarray_tbl (ti, te) op;
        op

    let b_to_coq = function
      | BO_Zplus -> Lazy.force cBO_Zplus
      | BO_Zminus -> Lazy.force cBO_Zminus
      | BO_Zmult -> Lazy.force cBO_Zmult
      | BO_Zlt -> Lazy.force cBO_Zlt
      | BO_Zle -> Lazy.force cBO_Zle
      | BO_Zge -> Lazy.force cBO_Zge
      | BO_Zgt -> Lazy.force cBO_Zgt
      | BO_eq t -> eq_to_coq t
      | BO_BVand s -> mklApp cBO_BVand [|mkN s|]
      | BO_BVor s -> mklApp cBO_BVor [|mkN s|]
      | BO_BVxor s -> mklApp cBO_BVxor [|mkN s|]
      | BO_BVadd s -> mklApp cBO_BVadd [|mkN s|]
      | BO_BVmult s -> mklApp cBO_BVmult [|mkN s|]
      | BO_BVult s -> mklApp cBO_BVult [|mkN s|]
      | BO_BVslt s -> mklApp cBO_BVslt [|mkN s|]
      | BO_BVconcat (s1, s2) -> mklApp cBO_BVconcat [|mkN s1; mkN s2|]
      | BO_BVshl s -> mklApp cBO_BVshl [|mkN s|]
      | BO_BVshr s -> mklApp cBO_BVshr [|mkN s|]
      | BO_select (ti, te) -> select_to_coq ti te
      | BO_diffarray (ti, te) -> diffarray_to_coq ti te

    let b_type_of = function
      | BO_Zplus | BO_Zminus | BO_Zmult -> SmtBtype.TZ
      | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt | BO_eq _
      | BO_BVult _ | BO_BVslt _ -> SmtBtype.Tbool
      | BO_BVand s | BO_BVor s | BO_BVxor s | BO_BVadd s | BO_BVmult s
      | BO_BVshl s | BO_BVshr s -> SmtBtype.TBV s
      | BO_BVconcat (s1, s2) -> SmtBtype.TBV (s1 + s2)
      | BO_select (_, te) -> te
      | BO_diffarray (ti, _) -> ti

    let b_type_args = function
      | BO_Zplus | BO_Zminus | BO_Zmult
      | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt -> (SmtBtype.TZ,SmtBtype.TZ)
      | BO_eq t -> (t,t)
      | BO_BVand s | BO_BVor s | BO_BVxor s | BO_BVadd s | BO_BVmult s
      | BO_BVult s | BO_BVslt s | BO_BVshl s | BO_BVshr s ->
        (SmtBtype.TBV s,SmtBtype.TBV s)
      | BO_BVconcat (s1, s2) -> (SmtBtype.TBV s1, SmtBtype.TBV s2)
      | BO_select (ti, te) -> (SmtBtype.TFArray (ti, te), ti)
      | BO_diffarray (ti, te) -> (SmtBtype.TFArray (ti, te), SmtBtype.TFArray (ti, te))


    (* let interp_ieq t_i t =
     *   mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|] *)

 (*   let veval_t te =
      let env = Global.env () in
      let evd = Evd.from_env env in
      let evd, ty = Typing.type_of env evd te in
      Vnorm.cbv_vm env te ty


    let interp_ieq_eval t_i t =
      let te = mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|] in
      veval_t te
      *)

    let interp_eqarray t_i ti te =
      mklApp cequalarray
        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
          SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
          SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
          SmtBtype.inh_interp t_i te |]

    let interp_select t_i ti te =
      mklApp cselect
        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
          SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
          SmtBtype.inh_interp t_i te|]

    let interp_diff t_i ti te =
      mklApp cdiff
        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
          SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
          SmtBtype.dec_interp t_i te; SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
          SmtBtype.inh_interp t_i ti; SmtBtype.inh_interp t_i te |]


    let interp_store t_i ti te =
      mklApp cstore
        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
          SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
          SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; SmtBtype.inh_interp t_i te |]


    let interp_eq t_i = function
      | SmtBtype.TZ -> Lazy.force ceqbZ
      | SmtBtype.Tbool -> Lazy.force ceqb
      | SmtBtype.Tpositive -> Lazy.force ceqbP
      | SmtBtype.TBV s -> mklApp cbv_eq [|mkN s|]
      | SmtBtype.Tindex i ->
         let compdec = SmtBtype.indexed_type_compdec i in
         mklApp ceqb_of_compdec [|mklApp cte_carrier [|compdec|];
                                  mklApp cte_compdec [|compdec|]|]
      | SmtBtype.TFArray (ti, te) -> interp_eqarray t_i ti te



    let interp_bop t_i = function
      | BO_Zplus -> Lazy.force cadd
      | BO_Zminus -> Lazy.force csub
      | BO_Zmult -> Lazy.force cmul
      | BO_Zlt -> Lazy.force cltb
      | BO_Zle -> Lazy.force cleb
      | BO_Zge -> Lazy.force cgeb
      | BO_Zgt -> Lazy.force cgtb
      | BO_eq t -> interp_eq t_i t
      | BO_BVand s -> mklApp cbv_and [|mkN s|]
      | BO_BVor s -> mklApp cbv_or [|mkN s|]
      | BO_BVxor s -> mklApp cbv_xor [|mkN s|]
      | BO_BVadd s -> mklApp cbv_add [|mkN s|]
      | BO_BVmult s -> mklApp cbv_mult [|mkN s|]
      | BO_BVult s -> mklApp cbv_ult [|mkN s|]
      | BO_BVslt s -> mklApp cbv_slt [|mkN s|]
      | BO_BVconcat (s1,s2) -> mklApp cbv_concat [|mkN s1; mkN s2|]
      | BO_BVshl s -> mklApp cbv_shl [|mkN s|]
      | BO_BVshr s -> mklApp cbv_shr [|mkN s|]
      | BO_select (ti, te) -> interp_select t_i ti te
      | BO_diffarray (ti, te) -> interp_diff t_i ti te

    let t_to_coq = function
      | TO_store (ti, te) -> store_to_coq ti te

    let t_type_of = function
      | TO_store (ti, te) -> SmtBtype.TFArray (ti, te)

    let t_type_args = function
      | TO_store (ti, te) -> SmtBtype.TFArray (ti, te), ti, te

    let interp_top t_i = function
      | TO_store (ti, te) -> interp_store t_i ti te


    let n_to_coq = function
      | NO_distinct t -> mklApp cNO_distinct [|SmtBtype.to_coq t|]

    let n_type_of = function
      | NO_distinct _ -> SmtBtype.Tbool

    let n_type_args = function
      | NO_distinct ty -> ty

    let interp_nop t_i = function
      | NO_distinct ty ->
        mklApp cdistinct [|SmtBtype.interp t_i ty; interp_eq t_i ty|]

    let i_to_coq i = let index, _ = destruct "destruct on a Rel: called by i_to_coq" i in
                     mkInt index

    let i_type_of (_, hval) = hval.tres

    let i_type_args (_, hval) = hval.tparams

    (* reify table *)
    type reify_tbl =
      { mutable count : int;
	        tbl : (CoqInterface.constr, indexed_op) Hashtbl.t
      }

    let create () =
      { count = 0;
	tbl =  Hashtbl.create 17 }

    let declare reify op tparams tres os =
      assert (not (Hashtbl.mem reify.tbl op));
      let opa = { tparams = tparams; tres = tres; op_val = op } in
      match os with
      | None ->  let res = Index reify.count, opa in
                 Hashtbl.add reify.tbl op res;
                 reify.count <- reify.count + 1;
                 res
      | Some name -> Rel_name name, opa

    let of_coq reify op =
      Hashtbl.find reify.tbl op


    let interp_tbl tval mk_Tval reify =
      let t = Array.make (reify.count + 1)
	        (mk_Tval [||] SmtBtype.Tbool (Lazy.force ctrue)) in
      let set _ op =
        let index, hval = destruct "destruct on a Rel: called by set in interp_tbl" op in
        t.(index) <- mk_Tval hval.tparams hval.tres hval.op_val in
      Hashtbl.iter set reify.tbl;
      CoqTerms.mkArray (tval, t)

    let to_list reify =
      let set _ op acc =
        let index, hval = destruct "destruct on a Rel: called by set in to_list" op in
        (index, hval.tparams, hval.tres, op)::acc in
      Hashtbl.fold set reify.tbl []

    let c_equal op1 op2 = match op1, op2 with
      | CO_BV bv1, CO_BV bv2 ->
        (try List.for_all2 (=) bv1 bv2 with
         | Invalid_argument _ -> false)
      | _ -> op1 == op2

    let c_hash = function
      | CO_xH -> 1
      | CO_Z0 -> 2
      | CO_BV l -> 3 + (List.fold_left (fun acc b -> if b then 2*acc+1 else 2*acc) 0 l)

    let u_equal op1 op2 =
      match op1,op2 with
      | UO_xO, UO_xO
      | UO_xI, UO_xI
      | UO_Zpos, UO_Zpos
      | UO_Zneg, UO_Zneg
      | UO_Zopp, UO_Zopp -> true
      | UO_BVbitOf (s1,i1), UO_BVbitOf (s2,i2) -> s1 == s2 && i1 == i2
      | UO_BVnot s1, UO_BVnot s2 -> s1 == s2
      | UO_BVneg s1, UO_BVneg s2 -> s1 == s2
      | UO_BVextr (i1, n1, s1) , UO_BVextr (i2, n2, s2) ->
        i1 == i2 && n1 == n2 && s1 == s2
      | UO_BVzextn (s1, n1), UO_BVzextn (s2, n2) -> s1 == s2 && n1 == n2
      | UO_BVsextn (s1, n1), UO_BVsextn (s2, n2) -> s1 == s2 && n1 == n2
      | _ -> false

    let u_hash = function
      | UO_xO -> 0
      | UO_xI -> 1
      | UO_Zpos -> 2
      | UO_Zneg -> 3
      | UO_Zopp -> 4
      | UO_BVbitOf (s,n) -> (n land s) lxor 5
      | UO_BVnot s -> s lxor 6
      | UO_BVneg s -> s lxor 7
      | UO_BVextr (s, n0, n1) -> (s land n0 land n1) lxor 8
      | UO_BVzextn (s, n) -> (s land n) lxor 9
      | UO_BVsextn (s, n) -> (s land n) lxor 10

    let b_equal op1 op2 =
      match op1,op2 with
        | BO_eq t1, BO_eq t2 -> SmtBtype.HashedBtype.equal t1 t2
        | BO_BVand n1, BO_BVand n2 -> n1 == n2
        | BO_BVor n1, BO_BVor n2 -> n1 == n2
        | BO_BVxor n1, BO_BVxor n2 -> n1 == n2
        | BO_BVadd n1, BO_BVadd n2 -> n1 == n2
        | BO_BVmult n1, BO_BVmult n2 -> n1 == n2
        | BO_BVult n1, BO_BVult n2 -> n1 == n2
        | BO_BVslt n1, BO_BVslt n2 -> n1 == n2
        | BO_BVconcat (n1,m1), BO_BVconcat (n2,m2) -> n1 == n2 && m1 == m2
        | BO_BVshl n1, BO_BVshl n2 -> n1 == n2
        | BO_BVshr n1, BO_BVshr n2 -> n1 == n2
        | BO_select (ti1, te1), BO_select (ti2, te2)
        | BO_diffarray (ti1, te1), BO_diffarray (ti2, te2) ->
           HashedBtypePair.equal (ti1, te1) (ti2, te2)
        | _ -> op1 == op2

    let b_hash = function
      | BO_Zplus -> 1
      | BO_Zminus -> 2
      | BO_Zmult -> 3
      | BO_Zlt -> 4
      | BO_Zle -> 5
      | BO_Zge -> 6
      | BO_Zgt -> 7
      | BO_eq ty -> ((SmtBtype.HashedBtype.hash ty) lsl 6) lxor 8
      | BO_BVand s -> s lxor 9
      | BO_BVor s -> s lxor 10
      | BO_BVxor s -> s lxor 11
      | BO_BVadd s -> s lxor 12
      | BO_BVmult s -> s lxor 13
      | BO_BVult s -> s lxor 14
      | BO_BVslt s -> s lxor 15
      | BO_BVconcat (s1,s2) -> (s1 land s2) lxor 16
      | BO_BVshl s -> s lxor 17
      | BO_BVshr s -> s lxor 18
      | BO_select (ti, te) -> ((HashedBtypePair.hash (ti, te)) lsl 6) lxor 19
      | BO_diffarray (ti, te) -> ((HashedBtypePair.hash (ti, te)) lsl 6) lxor 20

    let t_equal op1 op2 =
      match op1,op2 with
        | TO_store (ti1, te1), TO_store (ti2, te2) ->
          SmtBtype.HashedBtype.equal ti1 ti2 && SmtBtype.HashedBtype.equal te1 te2

    let t_hash = function
      | TO_store (ti, te) -> HashedBtypePair.hash (ti, te)

    let n_equal op1 op2 =
      match op1,op2 with
      | NO_distinct t1, NO_distinct t2 -> SmtBtype.HashedBtype.equal t1 t2

    let n_hash = function
      | NO_distinct t -> SmtBtype.HashedBtype.hash t

    let i_equal (i1, _) (i2, _) = i1 = i2




    let logic_of_cop = function
      | CO_xH | CO_Z0 -> SL.singleton LLia
      | CO_BV _ -> SL.singleton LBitvectors

    let logic_of_uop = function
      | UO_xO | UO_xI
      | UO_Zpos | UO_Zneg | UO_Zopp -> SL.singleton LLia
      | UO_BVbitOf _ | UO_BVnot _ | UO_BVneg _
      | UO_BVextr _ | UO_BVzextn _ | UO_BVsextn _ -> SL.singleton LBitvectors

    let logic_of_bop = function
      | BO_Zplus
      | BO_Zminus
      | BO_Zmult
      | BO_Zlt
      | BO_Zle
      | BO_Zge
      | BO_Zgt -> SL.singleton LLia
      | BO_eq ty -> SmtBtype.logic ty
      | BO_BVand _
      | BO_BVor _
      | BO_BVxor _
      | BO_BVadd _
      | BO_BVmult _
      | BO_BVult _
      | BO_BVslt _
      | BO_BVshl _
      | BO_BVshr _
      | BO_BVconcat _ -> SL.singleton LBitvectors
      | BO_select (ti, te)
      | BO_diffarray (ti, te) ->
        SL.add LArrays (SL.union (SmtBtype.logic ti) (SmtBtype.logic te))


    let logic_of_top = function
      | TO_store (ti, te) ->
        SL.add LArrays (SL.union (SmtBtype.logic ti) (SmtBtype.logic te))

    let logic_of_nop = function
      | NO_distinct ty -> SmtBtype.logic ty


    let logic_of_indexed t =
      let (_, hval) = destruct "destruct on a Rel: called by logic_of_indexed" t in
      Array.fold_left (fun l ty ->
         SL.union (SmtBtype.logic ty) l
        ) (SmtBtype.logic hval.tres) hval.tparams


    let logic_ro reify =
      Hashtbl.fold (fun _ op -> SL.union (logic_of_indexed op))
        reify.tbl SL.empty

  end


(** Definition of atoms *)

type atom =
  | Acop of cop
  | Auop of uop * hatom
  | Abop of bop * hatom * hatom
  | Atop of top * hatom * hatom * hatom
  | Anop of nop * hatom array
  | Aapp of indexed_op * hatom array

and hatom = atom gen_hashed

(* let pp_acop = function *)
(*   | CO_xH -> "CO_xH" *)
(*   | CO_Z0 -> "CO_Z0" *)

(* let pp_auop = function *)
(*   | UO_xO -> "UO_xO" *)
(*   | UO_xI -> "UO_xI" *)
(*   | UO_Zpos -> "UO_Zpos" *)
(*   | UO_Zneg -> "UO_Zneg" *)
(*   | UO_Zopp -> "UO_Zopp" *)

(* let pp_abop = function *)
(*   | BO_Zplus -> "BO_Zplus" *)
(*   | BO_Zminus -> "BO_Zminus" *)
(*   | BO_Zmult -> "BO_Zmult" *)
(*   | BO_Zlt -> "BO_Zlt" *)
(*   | BO_Zle -> "BO_Zle" *)
(*   | BO_Zge -> "BO_Zge" *)
(*   | BO_Zgt -> "BO_Zgt" *)
(*   | BO_eq _ -> "(BO_eq ??)" *)

(* let rec pp_atom = function *)
(*   | Acop c -> "(Acop "^(pp_acop c)^")" *)
(*   | Auop (u,b) -> "(Auop "^(pp_auop u)^" "^(pp_atom b.hval)^")" *)
(*   | Abop (b,c,d) -> "(Abop "^(pp_abop b)^" "^(pp_atom c.hval)^" "^(pp_atom d.hval)^")" *)
(*   | Aapp (op,a) -> "(Aapp "^(string_of_int op.index)^" ("^(Array.fold_left (fun acc h -> acc^" "^(pp_atom h.hval)) "" a)^"))" *)

module HashedAtom =
  struct
    type t = atom

    let equal a b =
      match a, b with
      | Acop opa, Acop opb -> Op.c_equal opa opb
      | Auop(opa,ha), Auop(opb,hb) -> Op.u_equal opa opb && ha.index == hb.index
      | Abop(opa,ha1,ha2), Abop(opb,hb1,hb2) ->
	Op.b_equal opa opb && ha1.index == hb1.index && ha2.index == hb2.index
      | Atop(opa,ha1,ha2,ha3), Atop(opb,hb1,hb2,hb3) ->
	Op.t_equal opa opb && ha1.index == hb1.index &&
         ha2.index == hb2.index && ha3.index == hb3.index
      | Anop (opa,ha), Anop (opb,hb) ->
        let na = Array.length ha in
        let nb = Array.length hb in
        let i = ref (-1) in
        Op.n_equal opa opb && na == nb &&
        Array.fold_left
          (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
      | Aapp (va,ha), Aapp (vb,hb) ->
        let na = Array.length ha in
        let nb = Array.length hb in
        let i = ref (-1) in
        Op.i_equal va vb && na == nb &&
        Array.fold_left
          (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
      | _, _ -> false

    let hash = function
      |	Acop op -> ((Op.c_hash op) lsl 3) lxor 1
      | Auop (op,h) ->
         (( (h.index lsl 3) + (Op.u_hash op)) lsl 3) lxor 2
      | Abop (op,h1,h2) ->
        (((( (h1.index lsl 2) + h2.index) lsl 3) + Op.b_hash op) lsl 3) lxor 3
      | Atop (op,h1,h2,h3) ->
        (((( ((h1.index lsl 2) + h2.index) lsl 3) + h3.index) lsl 4
          + Op.t_hash op) lsl 4) lxor 4
      | Anop (op, args) ->
          let hash_args =
            match Array.length args with
            | 0 -> 0
            | 1 -> args.(0).index
            | 2 -> args.(1).index lsl 2 + args.(0).index
            | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index
          in
          (hash_args lsl 5 + (Op.n_hash op) lsl 3) lxor 4
      | Aapp (op, args) ->
         let op_index = try fst (destruct "destruct on a Rel: called by hash" op) with _ -> 0 in
          let hash_args =
            match Array.length args with
            | 0 -> 0
            | 1 -> args.(0).index
            | 2 -> args.(1).index lsl 2 + args.(0).index
            | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index
          in
          (hash_args lsl 5 + op_index lsl 3) lxor 4



  end

module HashAtom = Hashtbl.Make(HashedAtom)

module Atom =
  struct

    type t = hatom

    let atom h = h.hval
    let index h = h.index

    let equal h1 h2 = h1.index == h2.index

    let type_of h =
      match h.hval with
      | Acop op -> Op.c_type_of op
      | Auop (op,_) -> Op.u_type_of op
      | Abop (op,_,_) -> Op.b_type_of op
      | Atop (op,_,_,_) -> Op.t_type_of op
      | Anop (op,_) -> Op.n_type_of op
      | Aapp (op,_) -> Op.i_type_of op

    let is_bool_type h = SmtBtype.HashedBtype.equal (type_of h) SmtBtype.Tbool
    let is_bv_type h = match type_of h with | SmtBtype.TBV _ -> true | _ -> false


    let rec compute_int = function
      | Acop c ->
         (match c with
          | CO_xH -> 1
          | CO_Z0 -> 0
          | CO_BV _ -> assert false)
      | Auop (op,h) ->
         (match op with
          | UO_xO -> 2*(compute_hint h)
          | UO_xI -> 2*(compute_hint h) + 1
          | UO_Zpos -> compute_hint h
          | UO_Zneg -> - (compute_hint h)
          | UO_Zopp | UO_BVbitOf _
          | UO_BVnot _ | UO_BVneg _
          | UO_BVextr _ | UO_BVzextn _ | UO_BVsextn _ -> assert false)
      | _ -> assert false

    and compute_hint h = compute_int (atom h)

    let to_smt_int fmt i =
      let s1 = if i < 0 then "(- " else "" in
      let s2 = if i < 0 then ")" else "" in
      let j = if i < 0 then -i else i in
      Format.fprintf fmt "%s%i%s" s1 j s2


    let rec bv_to_smt fmt = function
      | true :: bv -> Format.fprintf fmt "%a1" bv_to_smt bv
      | false :: bv -> Format.fprintf fmt "%a0" bv_to_smt bv
      | [] -> ()


    let to_smt_named ?(debug=false) ?pi:(pi=false) (fmt:Format.formatter) h =
      let rec to_smt fmt h =
        if pi then Format.fprintf fmt "%d:" (index h);
        to_smt_atom ~debug:debug (atom h)

      and to_smt_atom ?(debug=false) = function
        | Acop (CO_BV bv) -> if List.length bv = 0 then CoqInterface.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv
        | Acop _ as a -> to_smt_int fmt (compute_int a)
        | Auop (op,h) -> to_smt_uop op h
        | Abop (op,h1,h2) -> to_smt_bop op h1 h2
        | Atop (op,h1,h2,h3) -> to_smt_top op h1 h2 h3
        | Anop (op,a) -> to_smt_nop op a
        | Aapp ((i,op),a) ->
           let op_smt () =
             (match i with
                | Index index ->
                   (Format.fprintf fmt "op_%i" index;
                    if debug then Format.fprintf fmt " (aka %s)" (Pp.string_of_ppcmds (CoqInterface.pr_constr op.op_val));)
                | Rel_name name -> Format.fprintf fmt "%s" name);
             if pi then to_smt_op op
           in
           if Array.length a = 0 then (
             op_smt ()
           ) else (
             Format.fprintf fmt "(";
             op_smt ();
             Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a;
             Format.fprintf fmt ")"
           )

      and to_smt_op {tparams=bta; tres=bt; op_val=t} =
        Format.fprintf fmt "[(";
        Array.iter (fun bt -> SmtBtype.to_smt fmt bt; Format.fprintf fmt " ") bta;
        Format.fprintf fmt ") ( ";
        SmtBtype.to_smt fmt bt;
        Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (CoqInterface.pr_constr t))

      and to_smt_uop op h =
        match op with
          | UO_Zpos ->
             Format.fprintf fmt "%a" to_smt h
          | UO_Zneg ->
             Format.fprintf fmt "(- %a)" to_smt h
          | UO_Zopp ->
             Format.fprintf fmt "(- %a)" to_smt h
          | UO_BVbitOf (_, i) ->
             Format.fprintf fmt "(bitof %d %a)" i to_smt h
          | UO_BVnot _ ->
             Format.fprintf fmt "(bvnot %a)" to_smt h
          | UO_BVneg _ ->
             Format.fprintf fmt "(bvneg %a)" to_smt h
          | UO_BVextr (i, n, _) ->
             Format.fprintf fmt "((_ extract %d %d) %a)" (i+n-1) i to_smt h
          | UO_BVzextn (_, n) ->
             Format.fprintf fmt "((_ zero_extend %d) %a)" n to_smt h
          | UO_BVsextn (_, n) ->
             Format.fprintf fmt "((_ sign_extend %d) %a)" n to_smt h
          | _ -> to_smt_int fmt (compute_int (Auop (op, h)))

      and to_smt_bop op h1 h2 =
        let s = match op with
            | BO_Zplus -> "+"
            | BO_Zminus -> "-"
            | BO_Zmult -> "*"
            | BO_Zlt -> "<"
            | BO_Zle -> "<="
            | BO_Zge -> ">="
            | BO_Zgt -> ">"
            | BO_eq _ -> "="
            | BO_BVand _ -> "bvand"
            | BO_BVor _ -> "bvor"
            | BO_BVxor _ -> "bvxor"
            | BO_BVadd _ -> "bvadd"
            | BO_BVmult _ -> "bvmul"
            | BO_BVult _ -> "bvult"
            | BO_BVslt _ -> "bvslt"
            | BO_BVconcat _ -> "concat"
            | BO_BVshl _ -> "bvshl"
            | BO_BVshr _ -> "bvlshr"
            | BO_select _ -> "select"
            | BO_diffarray _ -> "diff" (* should not be used in goals *)
        in
        Format.fprintf fmt "(%s %a %a)" s to_smt h1 to_smt h2

      and to_smt_top op h1 h2 h3=
        let s = match op with
            | TO_store _ -> "store"
        in
        Format.fprintf fmt "(%s %a %a %a)" s to_smt h1 to_smt h2 to_smt h3

      and to_smt_nop op a =
        let s = match op with
            | NO_distinct _ -> "distinct" in
        Format.fprintf fmt "(%s" s;
        Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a;
        Format.fprintf fmt ")"

      in
      to_smt fmt h

    let to_smt ?(debug=false) (fmt:Format.formatter) h = to_smt_named ~debug:debug fmt h


    type reify_tbl =
      { mutable count : int;
	tbl : hatom HashAtom.t
      }

    let create () =
      { count = 0;
	tbl =  HashAtom.create 17 }

    let op_coq_terms = Hashtbl.create 17

    let clear reify =
      Hashtbl.clear op_coq_terms;
      reify.count <- 0;
      HashAtom.clear reify.tbl


    let declare reify a =
      let res = {index = reify.count; hval = a} in
      HashAtom.add reify.tbl a res;
      reify.count <- reify.count + 1;
      res

    let rec get ?declare:(decl=true) reify a =
      if decl
      then try HashAtom.find reify.tbl a
           with Not_found ->
             (let a = check reify a in
              try HashAtom.find reify.tbl a
              with Not_found ->
                declare reify a)
      else {index = -1; hval = a}

    and check reify a =
      (* Format.eprintf "Checking %a @." to_smt_atom a; *)

      let check_one t h =
        let th = type_of h in
        if SmtBtype.HashedBtype.equal t th then
          h
        else if t == SmtBtype.TZ && th == SmtBtype.Tpositive then
          (* Special case: the SMT solver cannot distinguish Z from
             positive, we have to add the injection back *)
          get reify (Auop(UO_Zpos, h))
        else (
          Format.eprintf "Incorrect type: wanted %a, got %a@."
            SmtBtype.to_smt t SmtBtype.to_smt th;
          failwith (Format.asprintf "Atom %a is not of the expected type" (to_smt ~debug:true) h)
        )
      in

      let a =
        match a with
          | Acop _ -> a
          | Auop(op,h) ->
             let t = Op.u_type_arg op in
             Auop(op, check_one t h)
          | Abop(op,h1,h2) ->
	     let (t1,t2) = Op.b_type_args op in
             let h1 = check_one t1 h1 in
             let h2 = check_one t2 h2 in
             Abop(op, h1, h2)
          | Atop(op,h1,h2,h3) ->
	     let (t1,t2,t3) = Op.t_type_args op in
             let h1 = check_one t1 h1 in
             let h2 = check_one t2 h2 in
             let h3 = check_one t3 h3 in
             Atop(op, h1, h2, h3)
          | Anop(op,ha) ->
             let ty = Op.n_type_args op in
             Anop(op, Array.map (check_one ty) ha)
          | Aapp(op,args) ->
             let tparams = Op.i_type_args op in
             Aapp(op, Array.mapi (fun i -> check_one tparams.(i)) args)
      in
      a


    (* Identifies two equalities modulo symmetry *)
    let mk_eq_sym reify ?declare:(decl=true) ty h1 h2 =
      let op = BO_eq ty in
      try
        HashAtom.find reify.tbl (Abop (op, h1, h2))
      with Not_found ->
        try
          HashAtom.find reify.tbl (Abop (op, h2, h1))
        with Not_found ->
          get ~declare:decl reify (Abop (op, h1, h2))

    let mk_neg reify ({index = i; hval = a} as ha) =
      try HashAtom.find reify.tbl (Auop (UO_Zopp, ha))
      with Not_found ->
        let na = match a with
          | Auop (UO_Zpos, x) -> Auop (UO_Zneg, x)
          | Auop (UO_Zneg, x) -> Auop (UO_Zpos, x)
          | _ -> failwith "opp not on Z" in
        get reify na

    let rec hash_hatom ra_quant {index = _; hval = a} =
      match a with
      | Acop cop -> get ra_quant a
      | Auop (uop, ha) -> get ra_quant (Auop (uop, hash_hatom ra_quant ha))
      | Abop (bop, ha1, ha2) ->
         let new_ha1 = hash_hatom ra_quant ha1 in
         let new_ha2 = hash_hatom ra_quant ha2 in
         begin match bop with
         | BO_eq ty -> mk_eq_sym ra_quant ty new_ha1 new_ha2
         | _ -> get ra_quant (Abop (bop, new_ha1, new_ha2)) end
      | Atop (top, ha1, ha2, ha3) ->
         let new_ha1 = hash_hatom ra_quant ha1 in
         let new_ha2 = hash_hatom ra_quant ha2 in
         let new_ha3 = hash_hatom ra_quant ha3 in
         get ra_quant (Atop (top, new_ha1, new_ha2, new_ha3))
      | Anop _ -> assert false
      | Aapp (op, arr) -> get ra_quant (Aapp (op, Array.map (hash_hatom ra_quant) arr))

    let copy {count=c; tbl=t} = {count = c; tbl = HashAtom.copy t}

    let print_atoms reify where =
      let oc = open_out where in
      let fmt = Format.formatter_of_out_channel oc in
      let accumulate _ ha acc = ha :: acc in
      let list = HashAtom.fold accumulate reify.tbl [] in
      let compare ha1 ha2 = compare ha1.index ha2.index in
      let slist = List.sort compare list in
      let print ha = Format.fprintf fmt "%i: " ha.index;
                     to_smt fmt ha; Format.fprintf fmt "\n" in
      List.iter print slist;
      Format.fprintf fmt "@.";
      close_out oc


    (** Given a coq term, build the corresponding atom *)
    type coq_cst =
      | CCxH
      | CCZ0
      | CCBV
      | CCxO
      | CCxI
      | CCZpos
      | CCZneg
      | CCZopp
      | CCBVbitOf
      | CCBVnot
      | CCBVneg
      | CCZplus
      | CCZminus
      | CCZmult
      | CCZlt
      | CCZle
      | CCZge
      | CCZgt
      | CCBVand
      | CCBVor
      | CCBVxor
      | CCBVadd
      | CCBVmult
      | CCBVult
      | CCBVslt
      | CCBVconcat
      | CCBVextr
      | CCBVsextn
      | CCBVzextn
      | CCBVshl
      | CCBVshr
      | CCeqb                   (* Equality on bool *)
      | CCeqbP                  (* Equality on positive *)
      | CCeqbZ                  (* Equality on Z *)
      | CCeqbBV                 (* Equality on bit vectors *)
      | CCeqbA                  (* Equality on arrays *)
      | CCeqbU                  (* Equality on uninterpreted types *)
      | CCselect
      | CCdiff
      | CCstore
      | CCunknown
      | CCunknown_deps of int


    let logic_coq_cst = function
      | CCxH
      | CCZ0
      | CCxO
      | CCxI
      | CCZpos
      | CCZneg
      | CCZopp
      | CCZplus
      | CCZminus
      | CCZmult
      | CCZlt
      | CCZle
      | CCZge
      | CCZgt -> SL.singleton LLia

      | CCBV
      | CCBVbitOf
      | CCBVnot
      | CCBVneg
      | CCBVand
      | CCBVor
      | CCBVxor
      | CCBVadd
      | CCBVmult
      | CCBVult
      | CCBVslt
      | CCBVconcat
      | CCBVextr
      | CCBVsextn
      | CCBVzextn
      | CCBVshl
      | CCBVshr -> SL.singleton LBitvectors

      | CCselect | CCdiff | CCstore -> SL.singleton LArrays

      | CCeqb -> SL.empty

      (* | CCeqbP | CCeqbZ -> SL.singleton LLia *)
      (* | CCeqbBV -> SL.singleton LBitvectors *)
      (* | CCeqbA -> SL.singleton LArrays *)

      | CCeqbP | CCeqbZ | CCeqbBV | CCeqbA | CCeqbU
      | CCunknown | CCunknown_deps _  -> SL.singleton LUF


    let gobble_of_coq_cst = function
      | CCBV
      | CCBVbitOf
      | CCBVnot
      | CCBVneg
      | CCBVand
      | CCBVor
      | CCBVxor
      | CCBVadd
      | CCBVmult
      | CCBVult
      | CCBVslt
      | CCBVsextn
      | CCBVzextn
      | CCBVshl
      | CCBVshr -> 1

      | CCBVconcat -> 2
      | CCBVextr -> 3

      | CCselect -> 5
      | CCdiff -> 10
      | CCstore -> 8

      | _ -> 0


    let op_tbl () =
      let tbl = Hashtbl.create 40 in
      let add (c1,c2) = Hashtbl.add tbl (Lazy.force c1) c2 in
      List.iter add
	[ cxH,CCxH; cZ0,CCZ0; cof_bits, CCBV;
          cxO,CCxO; cxI,CCxI; cZpos,CCZpos; cZneg,CCZneg; copp,CCZopp;
          cbitOf, CCBVbitOf; cbv_not, CCBVnot; cbv_neg, CCBVneg;
          cbv_extr, CCBVextr; cbv_zextn, CCBVzextn; cbv_sextn, CCBVsextn;
          cadd,CCZplus; csub,CCZminus; cmul,CCZmult; cltb,CCZlt;
          cleb,CCZle; cgeb,CCZge; cgtb,CCZgt;
          cbv_and, CCBVand; cbv_or, CCBVor; cbv_xor, CCBVxor;
          cbv_add, CCBVadd; cbv_mult, CCBVmult;
          cbv_ult, CCBVult; cbv_slt, CCBVslt; cbv_concat, CCBVconcat;
          cbv_shl, CCBVshl; cbv_shr, CCBVshr;
          ceqb,CCeqb; ceqbP,CCeqbP; ceqbZ, CCeqbZ; cbv_eq, CCeqbBV; ceqb_of_compdec, CCeqbU;
          cselect, CCselect; cdiff, CCdiff;
          cstore, CCstore;
          cequalarray, CCeqbA;
        ];
      tbl

    let op_tbl = lazy (op_tbl ())


    let split_list_at n l =
      let rec aux acc n l = match n, l with
        | 0, _ -> List.rev acc, l
        | _, [] -> assert false
        | _, x :: l -> aux (x :: acc) (n-1) l
      in
      aux [] n l


    let get_coq_term_op =
      Hashtbl.find op_coq_terms


    exception UnknownUnderForall

    let of_coq ?eqsym:(eqsym=false) rt ro reify known_logic env sigma c =
      let op_tbl = Lazy.force op_tbl in
      let get_cst c =
	try
          let cc = Hashtbl.find op_tbl c in
          if SL.subset (logic_coq_cst cc) known_logic then cc
          else CCunknown_deps (gobble_of_coq_cst cc)
        with Not_found -> CCunknown
      in
      let rec mk_hatom (h : CoqInterface.constr) =
        let c, args = CoqInterface.decompose_app h in
	match get_cst c with
        | CCxH -> mk_cop CCxH args
        | CCZ0 -> mk_cop CCZ0 args
        | CCBV -> mk_cop CCBV args
        | CCxO -> mk_uop UO_xO args
        | CCxI -> mk_uop UO_xI args
        | CCZpos -> mk_uop UO_Zpos args
        | CCZneg -> mk_uop UO_Zneg args
        | CCZopp -> mk_uop UO_Zopp args
        | CCBVbitOf -> mk_bvbitof args
        | CCBVnot -> mk_bvnot args
        | CCBVneg -> mk_bvneg args
        | CCZplus -> mk_bop BO_Zplus args
        | CCZminus -> mk_bop BO_Zminus args
        | CCZmult -> mk_bop BO_Zmult args
        | CCZlt -> mk_bop BO_Zlt args
        | CCZle -> mk_bop BO_Zle args
        | CCZge -> mk_bop BO_Zge args
        | CCZgt -> mk_bop BO_Zgt args
        | CCBVand -> mk_bop_bvand args
        | CCBVor -> mk_bop_bvor args
        | CCBVxor -> mk_bop_bvxor args
        | CCBVadd -> mk_bop_bvadd args
        | CCBVmult -> mk_bop_bvmult args
        | CCBVult -> mk_bop_bvult args
        | CCBVslt -> mk_bop_bvslt args
        | CCBVconcat -> mk_bop_bvconcat args
        | CCBVextr -> mk_bvextr args
        | CCBVzextn -> mk_bvzextn args
        | CCBVsextn -> mk_bvsextn args
        | CCBVshl -> mk_bop_bvshl args
        | CCBVshr -> mk_bop_bvshr args
        | CCeqb -> mk_teq SmtBtype.Tbool args
        | CCeqbP -> mk_teq SmtBtype.Tpositive args
        | CCeqbZ -> mk_teq SmtBtype.TZ args
        | CCeqbA -> mk_bop_farray_equal args
        | CCeqbBV -> mk_bop_bveq args
        | CCeqbU -> mk_bop_ueq args
        | CCselect -> mk_bop_select args
        | CCdiff -> mk_bop_diff args
        | CCstore -> mk_top_store args
	| CCunknown -> mk_unknown c args (CoqInterface.retyping_get_type_of env sigma h)
        | CCunknown_deps gobble ->
          mk_unknown_deps c args (CoqInterface.retyping_get_type_of env sigma h) gobble


      and mk_cop op args = match op, args with
        | CCxH, [] -> get reify (Acop CO_xH)
        | CCZ0, [] -> get reify (Acop CO_Z0)
        | CCBV, [bs] -> get reify (Acop (CO_BV (mk_bool_list bs)))
        | _ -> assert false


      and mk_uop op = function
        | [a] -> let h = mk_hatom a in
          get reify (Auop (op,h))
        | _ -> assert false

      and mk_bvbitof = function
        | [s;n;a] ->
          let h = mk_hatom a in
          get reify (Auop (UO_BVbitOf (mk_bvsize s, mk_nat n), h))
        | _ -> assert false

      and mk_bvnot = function
        | [s;a] ->
          let h = mk_hatom a in
          get reify (Auop (UO_BVnot (mk_bvsize s), h))
        | _ -> assert false

      and mk_bvneg = function
        | [s;a] ->
          let h = mk_hatom a in
          get reify (Auop (UO_BVneg (mk_bvsize s), h))
        | _ -> assert false

      and mk_bvextr = function
        | [i;n;s;a] ->
          let h = mk_hatom a in
          get reify (Auop (UO_BVextr (mk_N i, mk_N n, mk_bvsize s), h))
        | _ -> assert false

      and mk_bvzextn = function
        | [s;n;a] ->
          let h = mk_hatom a in
          get reify (Auop (UO_BVzextn (mk_bvsize s, mk_N n), h))
        | _ -> assert false

      and mk_bvsextn = function
        | [s;n;a] ->
          let h = mk_hatom a in
          get reify (Auop (UO_BVsextn (mk_bvsize s, mk_N n), h))
        | _ -> assert false

      and mk_teq ty args =
        if eqsym then match args with
                  | [a1; a2] -> let h1 = mk_hatom a1 in
                                let h2 = mk_hatom a2 in
                                mk_eq_sym reify ty h1 h2
                  | _ -> failwith "unexpected number of arguments for mk_teq"
        else mk_bop (BO_eq ty) args

      and mk_bop_ueq args =
        match args with
          | t::compdec::args ->
             let ty = SmtBtype.of_coq_compdec rt t compdec in
             mk_teq ty args
          | _ -> failwith "unexpected number of arguments for mk_bop_ueq"

      and mk_bop op = function
        | [a1;a2] ->
           let h1 = mk_hatom a1 in
           let h2 = mk_hatom a2 in
           get reify (Abop (op,h1,h2))
        | _ -> failwith "unexpected number of arguments for mk_bop"

      and mk_top op = function
        | [a1;a2;a3] ->
          let h1 = mk_hatom a1 in
          let h2 = mk_hatom a2 in
          let h3 = mk_hatom a3 in
          get reify (Atop (op,h1,h2,h3))
        | _ -> assert false

      and mk_bop_bvand = function
        | [s;a1;a2] ->
           let s' = mk_bvsize s in
           mk_bop (BO_BVand s') [a1;a2]
        | _ -> assert false

      and mk_bop_bvor = function
        | [s;a1;a2] ->
           let s' = mk_bvsize s in
           mk_bop (BO_BVor s') [a1;a2]
        | _ -> assert false

      and mk_bop_bvxor = function
        | [s;a1;a2] ->
          let s' = mk_bvsize s in
          mk_bop (BO_BVxor s') [a1;a2]
        | _ -> assert false

      and mk_bop_bvadd = function
        | [s;a1;a2] ->
           let s' = mk_bvsize s in
           mk_bop (BO_BVadd s') [a1;a2]
        | _ -> assert false

      and mk_bop_bvmult = function
        | [s;a1;a2] ->
           let s' = mk_bvsize s in
           mk_bop (BO_BVmult s') [a1;a2]
        | _ -> assert false

      and mk_bop_bvult = function
        | [s;a1;a2] ->
           let s' = mk_bvsize s in
           mk_bop (BO_BVult s') [a1;a2]
        | _ -> assert false

      and mk_bop_bvslt = function
        | [s;a1;a2] ->
           let s' = mk_bvsize s in
           mk_bop (BO_BVslt s') [a1;a2]
        | _ -> assert false

      and mk_bop_bvshl = function
        | [s;a1;a2] ->
           let s' = mk_bvsize s in
           mk_bop (BO_BVshl s') [a1;a2]
        | _ -> assert false

      and mk_bop_bvshr = function
        | [s;a1;a2] ->
           let s' = mk_bvsize s in
           mk_bop (BO_BVshr s') [a1;a2]
        | _ -> assert false

      and mk_bop_bvconcat = function
        | [s1;s2;a1;a2] ->
           mk_bop (BO_BVconcat (mk_bvsize s1, mk_bvsize s2)) [a1;a2]
        | _ -> assert false

      and mk_bop_bveq = function
        | [s;a1;a2] when SL.mem LBitvectors known_logic ->
          let s' = mk_bvsize s in
          mk_teq (SmtBtype.TBV s') [a1;a2]
        (* We still want to interpret bv equality as uninterpreted
           smtlib2 equality if the solver doesn't support bitvectors *)
        | [s;a1;a2] ->
          let ty = SmtBtype.of_coq rt known_logic (mklApp cbitvector [|s|]) in
          mk_teq ty [a1;a2]
        | _ -> assert false

      and mk_bop_select = function
        | [ti;te;_;_;_;a;i] ->
          let ti' = SmtBtype.of_coq rt known_logic ti in
          let te' = SmtBtype.of_coq rt known_logic te in
          mk_bop (BO_select (ti', te')) [a; i]
        | _ -> assert false

      and mk_bop_diff = function
        | [ti;te;_;_;_;_;_;_;_;_;a;b] ->
          let ti' = SmtBtype.of_coq rt known_logic ti in
          let te' = SmtBtype.of_coq rt known_logic te in
          mk_bop (BO_diffarray (ti', te')) [a; b]
        | _ -> assert false

      and mk_top_store = function
        | [ti;te;_;_;_;_;_;_;a;i;e] ->
          let ti' = SmtBtype.of_coq rt known_logic ti in
          let te' = SmtBtype.of_coq rt known_logic te in
          mk_top (TO_store (ti', te')) [a; i; e]
        | _ -> assert false

      and mk_bop_farray_equal = function
        | [ti;te;_;_;_;_;_;a;b] when SL.mem LArrays known_logic ->
          let ti' = SmtBtype.of_coq rt known_logic ti in
          let te' = SmtBtype.of_coq rt known_logic te in
          mk_teq (SmtBtype.TFArray (ti', te')) [a; b]
        (* We still want to interpret array equality as uninterpreted
           smtlib2 equality if the solver doesn't support arrays *)
        | [ti;te;ord_ti;_;_;_;inh_te;a;b] ->
          let ty = SmtBtype.of_coq rt known_logic
              (mklApp cfarray [|ti; te; ord_ti; inh_te|]) in
          mk_teq ty [a;b]
        | _ -> assert false

      and mk_unknown c args ty =
        (* Collecting types and CompDec allows to reify applied
           polymorphic functions *)
        let rec collect_types = function
          | [] -> ([],[])
          | x::xs as l ->
             let (l1, l2) = collect_types xs in
             match l1 with
               | [] -> 
                 let ty = CoqInterface.retyping_get_type_of env sigma x in
                 if Constr.iskind ty ||
                      let c, _ = CoqInterface.decompose_app ty in
                      CoqInterface.eq_constr c (Lazy.force cCompDec)
                 then
                   ([x], xs)
                 else
                   ([], l)
               | _ -> (x::l1, l2)
        in
        let (args1, args2) = collect_types args in
        let c, args =
          match args1 with
            | [] -> c, args
            | _ -> Constr.mkApp (c, Array.of_list args1), args2
        in
        let hargs = Array.of_list (List.map mk_hatom args) in
        let op =
          try Op.of_coq ro c
          with | Not_found ->
            let targs = Array.map type_of hargs in
            let tres = SmtBtype.of_coq rt known_logic ty in
            let os = if CoqInterface.isRel c then
                       let i = CoqInterface.destRel c in
                       let n, _ = CoqInterface.destruct_rel_decl (Environ.lookup_rel i env) in
                       Some (CoqInterface.string_of_name n)
                     else if Vars.closed0 c then
                       None
                     else
                       (* Uninterpreted expression depending on a quantified variable.
                          We do not handle it for the moment.
                          We leave for future work to have "dependent" constants.
                        *)
                       raise UnknownUnderForall
            in
            Op.declare ro c targs tres os
        in
        (try
           let (i, _) = destruct "" op in
           Hashtbl.add op_coq_terms i c (* Chantal: I think we should move it to "Not_found" (otherwise it is already in the table) *)
         with | Failure _ -> ());
        get reify (Aapp (op,hargs))

      (* create an uninterpreted symbol for an unsupported symbol but fisrt do
         partial application to its dependent arguments whose number is given by
         [gobble] *)
      and mk_unknown_deps c args ty gobble =
        let deps, args = split_list_at gobble args in
        let c = CoqInterface.mkApp (c, Array.of_list deps) in
        mk_unknown c args ty

      in

      mk_hatom c


    let to_coq h = mkInt h.index

    let a_to_coq a =
      match a with
      | Acop op -> mklApp cAcop [|Op.c_to_coq op|]
      | Auop (op,h) -> mklApp cAuop [|Op.u_to_coq op; to_coq h|]
      | Abop (op,h1,h2) ->
	  mklApp cAbop [|Op.b_to_coq op;to_coq h1; to_coq h2|]
      | Atop (op,h1,h2,h3) ->
	  mklApp cAtop [|Op.t_to_coq op;to_coq h1; to_coq h2; to_coq h3|]
      | Anop (op,ha) ->
        let cop = Op.n_to_coq op in
        let cargs = Array.fold_right
            (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|])
            ha (mklApp cnil [|Lazy.force cint|]) in
        mklApp cAnop [|cop; cargs|]
      | Aapp (op,args) ->
        let cop = Op.i_to_coq op in
        let cargs = Array.fold_right
            (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|])
            args (mklApp cnil [|Lazy.force cint|]) in
        mklApp cAapp [|cop; cargs|]

    let dft_atom = lazy (mklApp cAcop [| Lazy.force cCO_xH |])

    let to_array reify dft f =
      let t = Array.make (reify.count + 1) dft in
      let set _ h = t.(h.index) <- f h.hval in
      HashAtom.iter set reify.tbl;
      t

    let interp_tbl reify =
      let t = to_array reify (Lazy.force dft_atom) a_to_coq in
      CoqTerms.mkArray (Lazy.force catom, t)


    (** Producing a Coq term corresponding to the interpretation of an atom *)
    let interp_to_coq t_i atom_tbl a =
      let rec interp_atom a =
	let l = index a in
	try Hashtbl.find atom_tbl l
	with Not_found ->
	  let pc =
	    match atom a with
              | Acop c -> Op.interp_cop c
              | Auop (op,h) -> CoqInterface.mkApp (Op.interp_uop op, [|interp_atom h|])
              | Abop (op,h1,h2) ->
                CoqInterface.mkApp (Op.interp_bop t_i op,
                            [|interp_atom h1; interp_atom h2|])
              | Atop (op,h1,h2,h3) ->
                CoqInterface.mkApp (Op.interp_top t_i op,
                            [|interp_atom h1; interp_atom h2; interp_atom h3|])
              | Anop (NO_distinct ty as op,ha) ->
                let cop = Op.interp_nop t_i op in
                let typ = SmtBtype.interp t_i ty in
                let cargs = Array.fold_right (fun h l ->
                    mklApp ccons [|typ; interp_atom h; l|])
                    ha (mklApp cnil [|typ|]) in
                CoqInterface.mkApp (cop,[|cargs|])
              | Aapp (op,t) ->
                CoqInterface.mkApp ((snd op).op_val, Array.map interp_atom t) in
	  Hashtbl.add atom_tbl l pc;
	  pc in
      interp_atom a


    (* Generation of atoms *)

    let mk_nop ?declare:(decl=true) op reify a = get ~declare:decl reify (Anop (op,a))

    let mk_binop ?declare:(decl=true) op reify h1 h2 = get ~declare:decl reify (Abop (op, h1, h2))

    let mk_terop ?declare:(decl=true) op reify h1 h2 h3 = get ~declare:decl reify (Atop (op, h1, h2, h3))

    let mk_unop ?declare:(decl=true) op reify h = get ~declare:decl reify (Auop (op, h))

    let rec hatom_pos_of_int reify i =
      if i <= 1 then
        get reify (Acop CO_xH)
      else
        if i land 1 = 0
        then mk_unop UO_xO reify (hatom_pos_of_int reify (i lsr 1))
        else mk_unop UO_xI reify (hatom_pos_of_int reify (i lsr 1))

    let hatom_Z_of_int reify i =
      if i = 0 then
        get reify (Acop CO_Z0)
      else
        if i > 0
        then mk_unop UO_Zpos reify (hatom_pos_of_int reify i)
        else mk_unop UO_Zneg reify (hatom_pos_of_int reify (-i))

    let rec hatom_pos_of_bigint reify i =
      if Big_int.le_big_int i Big_int.unit_big_int then
        get reify (Acop CO_xH)
      else
        let (q,r) = Big_int.quomod_big_int i (Big_int.big_int_of_int 2) in
        if Big_int.eq_big_int r Big_int.zero_big_int then
          mk_unop UO_xO reify (hatom_pos_of_bigint reify q)
        else
          mk_unop UO_xI reify (hatom_pos_of_bigint reify q)

    let hatom_Z_of_bigint reify i =
      if Big_int.eq_big_int i Big_int.zero_big_int then
        get reify (Acop CO_Z0)
      else
        if Big_int.gt_big_int i Big_int.zero_big_int then
          mk_unop UO_Zpos reify (hatom_pos_of_bigint reify i)
        else
          mk_unop UO_Zneg reify
            (hatom_pos_of_bigint reify (Big_int.minus_big_int i))

    let mk_unop ?declare:(decl=true) op reify h = get ~declare:decl reify (Auop (op, h))

    let mk_lt ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zlt ra
    let mk_le ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zle ra
    let mk_gt ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zgt ra
    let mk_ge ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zge ra
    let mk_plus ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zplus ra
    let mk_minus ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zminus ra
    let mk_mult ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zmult ra
    let mk_bvand reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVand s) reify
    let mk_bvor reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVor s) reify
    let mk_bvxor reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVxor s) reify
    let mk_bvadd reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVadd s) reify
    let mk_bvmult reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVmult s) reify
    let mk_bvult reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVult s) reify
    let mk_bvslt reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVslt s) reify
    let mk_bvconcat reify ?declare:(decl=true) s1 s2 = mk_binop ~declare:decl (BO_BVconcat (s1, s2)) reify
    let mk_opp ra ?declare:(decl=true) = mk_unop ~declare:decl UO_Zopp ra
    let mk_distinct reify ?declare:(decl=true) ty = mk_nop ~declare:decl (NO_distinct ty) reify
    let mk_bitof reify ?declare:(decl=true) s i = mk_unop ~declare:decl (UO_BVbitOf (s, i)) reify
    let mk_bvnot reify ?declare:(decl=true) s = mk_unop ~declare:decl (UO_BVnot s) reify
    let mk_bvneg reify ?declare:(decl=true) s = mk_unop ~declare:decl (UO_BVneg s) reify
    let mk_bvconst reify bool_list = get reify (Acop (CO_BV bool_list))
    let mk_select reify ?declare:(decl=true) ti te = mk_binop ~declare:decl (BO_select (ti, te)) reify
    let mk_diffarray reify ?declare:(decl=true) ti te = mk_binop ~declare:decl (BO_diffarray (ti, te)) reify
    let mk_store reify ?declare:(decl=true) ti te = mk_terop ~declare:decl (TO_store (ti, te)) reify
    let mk_bvextr reify ?declare:(decl=true) ~i ~n ~s = mk_unop ~declare:decl (UO_BVextr (i, n, s)) reify
    let mk_bvzextn reify ?declare:(decl=true) ~s ~n = mk_unop ~declare:decl (UO_BVzextn (s, n)) reify
    let mk_bvsextn reify ?declare:(decl=true) ~s ~n = mk_unop ~declare:decl (UO_BVsextn (s, n)) reify
    let mk_bvshl reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVshl s) reify
    let mk_bvshr reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVshr s) reify


    let rec logic_atom = function
      | Acop c -> Op.logic_of_cop c
      | Auop (u, h) -> SL.union (Op.logic_of_uop u) (logic h)
      | Abop (b, h1, h2) ->
        SL.union (Op.logic_of_bop b) (SL.union (logic h1) (logic h2))
      | Atop (t, h1, h2, h3) ->
        SL.union (Op.logic_of_top t)
          (SL.union (logic h1) (SL.union (logic h2) (logic h3)))
      | Anop (n, ha) ->
        Array.fold_left (fun l h -> SL.union (logic h) l) (Op.logic_of_nop n) ha
      | Aapp (i, ha) ->
        Array.fold_left (fun l h -> SL.union (logic h) l)
          (Op.logic_of_indexed i) ha

    and logic h = logic_atom h.hval

  end


module Form = SmtForm.Make(Atom)
module Trace = SmtTrace.MakeOpt(Form)


(* 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; SmtBtype.to_coq bt; acc|])
      cod (mklApp cnil [|typeb|]) in
  let b = SmtBtype.to_coq dom in
  mklApp cpair [|typea;typeb;a;b|]

let make_t_i = SmtBtype.make_t_i
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