struct

  type t = term

  let rec compare t1 t2 = 
    match t1, t2 with
    | Const c1, Const c2 -> compare_constants c1 c2
    | Const _, _ -> -1 | _, Const _ -> 1
    | Elem (_, (Constr | Var)), Elem (_, Glob) -> -1
    | Elem (_, Glob), Elem (_, (Constr | Var)) -> 1
    | Elem (s1, _), Elem (s2, _) -> Hstring.compare s1 s2
    | Elem _, _ -> -1 | _, Elem _ -> 1
    | Access (a1, l1), Access (a2, l2) ->
       let c = Hstring.compare a1 a2 in
       if c<>0 then c else Hstring.compare_list l1 l2
    | Access _, _ -> -1 | _, Access _ -> 1 
    | Arith (t1, cs1), Arith (t2, cs2) ->
       let c = compare t1 t2 in
       if c<>0 then c else compare_constants cs1 cs2

  let hash = Hashtbl.hash_param 50 50

  let equal t1 t2 = compare t1 t2 = 0

  let htrue = Hstring.make "True"
  let hfalse = Hstring.make "False"

  module STerm = Set.Make (struct
                            type t = term
                            let compare = compare
                          end)

  module Set = STerm

  let rec subst sigma t =
    match t with
    | Elem (x, s) ->
       let nx = Variable.subst sigma x in
       if x == nx then t
       else Elem (nx, s)
    | Access (a, lz) -> 
       Access (a, List.map
                    (fun z ->
                     try Variable.subst sigma z with Not_found -> z) lz)
    | Arith (x, c) -> Arith (subst sigma x, c)
    | _ -> t


  let rec variables = function
    | Elem (x, Var) -> Variable.Set.singleton x
    | Access (_, lx) ->
       List.fold_left (fun acc x -> Variable.Set.add x acc)
                      Variable.Set.empty lx
    | Arith (t, _) -> variables t
    | _ -> Variable.Set.empty


  let variables_proc t = Variable.Set.filter Variable.is_proc (variables t)

  let rec type_of = function
    | Const cs ->
       if is_int_const (fst (MConst.choose cs)) then
         Smt.Type.type_int
       else Smt.Type.type_real
    | Elem (x, Var) -> Smt.Type.type_proc
    | Elem (x, _) | Access (x, _) -> snd (Smt.Symbol.type_of x)
    | Arith(t, _) -> type_of t


  let rec print_strings fmt = function
    | [] -> ()
    | [s] -> fprintf fmt "%s" s
    | s :: l -> fprintf fmt "%s %a" s print_strings l

  let print_const fmt = function
    | ConstInt n | ConstReal n -> fprintf fmt "%s" (Num.string_of_num n)
    | ConstName n -> fprintf fmt "%a" Hstring.print n

  let print_cs alone fmt cs =
    let first = ref true in
    MConst.iter 
      (fun c i ->
         if !first && alone && i >= 0 then
           if i = 1 then print_const fmt c
           else fprintf fmt "%s %a" (string_of_int (abs i)) print_const c
         else
           fprintf fmt " %s %a" 
             (if i = 1 then "+" else if i = -1 then "-" 
              else if i < 0 then "- "^(string_of_int (abs i)) 
              else "+ "^(string_of_int (abs i)))
             print_const c;
         first := false;
      ) cs

  let rec print fmt = function
    | Const cs -> print_cs true fmt cs
    | Elem (s, _) -> fprintf fmt "%a" Hstring.print s
    | Access (a, li) ->
       fprintf fmt "%a[%a]" Hstring.print a (Hstring.print_list ", ") li
    | Arith (x, cs) -> 
       fprintf fmt "@[%a%a@]" print x (print_cs false) cs

end