[Egraph] separate uninterp from egraph

src/egraph_simple.ml

@@ -30,6 +30,7 @@
 
 let dont_clean_use = false
 
+
 open Stdlib
 open Shuffle
 
@@ -72,23 +73,25 @@ let rec normalize env cl =
     Debug.dprintf debug
       "[EGraph] normalize @[%a@]@."
       Cl.print cl;
-    let cl',env = match UnionFind.base cl with
-      | Term.Cst _ as v ->
+    let cl',env =
+      let v = UnionFind.base cl in
+      let leaves = Term.leaves v in
+      if Cl.S.is_empty leaves
+      then
         let env = UnionFind.set_repr env cl v in
         cl,env
-      | Term.App (f,g) ->
-        let clf,env = normalize env (UnionFind.find env f) in
-        let clg,env = normalize env (UnionFind.find env g) in
-        let v = Term.App(clf,clg) in
+      else
+        let env,leaves = Cl.M.mapi_fold (fun arg () env ->
+          let cl, env = normalize env (UnionFind.find env arg) in env,cl)
+          leaves env in
+        let v = Term.subst leaves v in
         let cl,env = UnionFind.basecl env v in
         if has_repr env cl then cl,env
         else
-            let env = UnionFind.add_use env cl v clf in
-            let env = if not (Cl.equal clf clg)
-              then UnionFind.add_use env cl v clg
-              else env in
-            let env = UnionFind.set_repr env cl v in
-            cl,env
+          let env = Cl.M.fold (fun _ norm env ->
+            UnionFind.add_use env cl v norm) leaves env in
+          let env = UnionFind.set_repr env cl v in
+          cl,env
     in
     let env = UnionFind.union_force env cl cl' in
     Debug.dprintf debug
@@ -103,33 +106,31 @@ let add env cl =
   Debug.dprintf debug
     "[EGraph] Add @[@[%a@]@ as@ @[%a@]@]@."
     (print_repr env) cl (print_repr env) cl';
-  let rec tag env cl =
+  let rec tag cl env =
     if UnionFind.is_added env cl then env
     else
       let env = UnionFind.added env cl in
-      match repr env cl with
-      | Term.Cst _ -> env
-      | Term.App (f,g) -> tag (tag env f) g
+      let leaves = Term.leaves (repr env cl) in
+      let env = Cl.S.fold tag leaves env in
+      env
   in
-  cl',tag env cl'
+  cl',tag cl' env
 
 let unuse env cl v =
   Debug.dprintf debug
     "[EGraph] @[Unuse @[%a@]@ @[%a@]@]@."
     (print_repr env) cl (UnionFind.print_value env) v;
-  match v with
-  | Term.Cst _ -> assert false
+  let leaves = Term.leaves v in
+  if Cl.S.is_empty leaves then
+    assert false
   (* no leaves so can't have been used in the first place *)
-  | Term.App (clf,clg) ->
-    let remove env cl v arg =
+  else
+    let remove arg env =
       Debug.dprintf debug "  Remove in @[%a@]@\n"
         (print_repr env) arg;
       UnionFind.remove_use env cl v arg
-      in
-    let env = remove env cl v clf in
-    let env = if not (Cl.equal clf clg)
-      then remove env cl v clg
-      else env in
+    in
+    let env = Cl.S.fold remove leaves env in
     env
 
 let rec is_equal env cl1 cl2 =
@@ -145,12 +146,8 @@ let rec is_equal env cl1 cl2 =
 
 (** t1 -> t2, t1 must be a direct subterm of t3 *)
 let subst t1 t2 t3 =
-  match t3 with
-  | Term.Cst _ -> assert false; (** can't substitute somthing without leaves *)
-  | Term.App(f,g) ->
-    assert ( Cl.equal t1 f || Cl.equal t1 g);
-    let subst t1 t2 arg = if Cl.equal t1 arg then t2 else arg in
-    Term.App (subst t1 t2 f, subst t1 t2 g)
+  let s = Cl.M.singleton t1 t2 in
+  Term.subst s t3
 
 exception ExitEnv of UnionFind.t
 

src/egraph_simple.mli

@@ -23,8 +23,62 @@
 
 val debug: Debug.flag
 
+(** For using the theories *)
+
 type env = Term.UnionFind.t
 
 val add: env -> Term.cl -> Term.cl * env
 val is_equal: env -> Term.cl -> Term.cl -> bool
 val equal: env -> Term.cl -> Term.cl -> env
+
+(*
+(** Used by the theories *)
+
+type cl (** class *)
+type value (** semantical value *)
+type delayed (** Environnement given to theories
+                 Modifications are delayed
+             *)
+val delayed_of_env : env -> delayed
+val find_cl : delayed -> value -> cl
+
+
+(** Register a theory *)
+
+module type S = sig
+  type repr
+  val print: delayed -> Format.formatter -> repr -> unit
+  val make: repr -> value
+  val extract: value -> repr option
+end
+
+module type Th = sig
+  val kind: thkind
+
+  type repr
+  val hash: repr -> int
+  val equal: repr -> repr -> bool
+
+  val leaves: repr -> Cl.S.t
+  val subst: delayed -> cl Cl.M.t -> repr -> cl
+  (** todo cl? et UnionFind.delayed? *)
+  (** Normally substitute only existing leaves *)
+
+  val solve: delayed -> repr -> value -> cl Cl.M.t * cl
+end
+
+module type ThMake = sig
+  type repr
+
+  module Make(X:S with type repr := repr) : sig
+    val print: (Format.formatter -> cl -> unit) ->
+      Format.formatter -> repr -> unit
+    include Th with type repr := repr
+  end
+end
+
+module Make(X:ThMake): sig
+  include S  with type repr = X.repr
+  include Th with type repr := X.repr
+end
+*)

src/term.ml

@@ -29,47 +29,141 @@ let debug = Debug.register_info_flag
 
 type tag = int
 
-type cl = {
-  tag  : int;
-  base : (** not the representative *) value;
-}
+type thkind =
+ | Polite
+ | Other
 
-and value =
- | Cst of Strings.Hashcons.t
- | App of cl * cl
+
+module rec Cl : Datatype with type t = Def.cl = struct
+  type t = Def.cl
+  module Cl = MakeMSH(struct type t = Def.cl let tag t = t.Def.tag end)
+  include Cl.T
+  let rec print fmt cl = Format.fprintf fmt "@[@@%i@]" cl.Def.tag
+  include Cl
+end
+
+and ModType : sig
+  module type Th = sig
+    type repr
+
+    val kind: thkind
+
+    val hash: repr -> int
+    val equal: repr -> repr -> bool
+    val print: (Format.formatter -> Cl.t -> unit) ->
+      Format.formatter -> repr -> unit
+
+    val leaves: repr -> Cl.S.t
+    val subst: Cl.t Cl.M.t -> repr -> Def.value
+    val solve: repr -> Def.value -> Cl.t Cl.M.t * Def.value
+    val id: int
+  end
+end = struct
+
+  module type Th = sig
+    type repr
+
+    val kind: thkind
+
+    val hash: repr -> int
+    val equal: repr -> repr -> bool
+    val print: (Format.formatter -> Cl.t -> unit) ->
+      Format.formatter -> repr -> unit
+
+    val leaves: repr -> Cl.S.t
+    val subst: Cl.t Cl.M.t -> repr -> Def.value
+    val solve: repr -> Def.value -> Cl.t Cl.M.t * Def.value
+    val id: int
+  end
+end
+
+and Def : sig
+
+  type 'a th = (module ModType.Th with type repr = 'a)
+
+  type cl = {
+    tag  : int;
+    base : (** not the representative *) value;
+  }
+
+  and value =
+  | Value: 'a th * 'a -> value
+end = struct
+  type 'a th = (module ModType.Th with type repr = 'a)
+
+  type cl = {
+    tag  : int;
+    base : (** not the representative *) value;
+  }
+
+  and value =
+  | Value: 'a th * 'a -> value
+
+end
+
+include Def
+
+module EqTh = Eqtype.Make(struct type 'a t = 'a th end)
+
+let eqth :
+   type a b. a th -> b th -> (a,b) Eqtype.eq option =
+     fun a b ->
+       let module A = (val a) in
+       let module B = (val b) in
+       if A.id <> B.id then None else
+         match EqTh.eq_type a b with
+         | None -> assert false (** id must be unique *)
+         | x -> x
 
 
 let equal n m =
-    match n, m with
-    | Cst i, Cst j -> i = j
-    | App (g1,f1), App(g2,f2) -> g1.tag = g2.tag && f1.tag = f2.tag
-    | _ -> false
+  match n, m with
+  | Value(nth,nv) , Value(mth,mv) ->
+    match eqth nth mth with
+    | None -> false
+    | Some Eqtype.Eq ->
+      let module Th = (val nth) in
+      Th.equal nv mv
+
+let leaves n =
+  match n with
+  | Value(th,v) ->
+    let module Th = (val th) in
+    Th.leaves v
+
+let subst s n =
+  match n with
+  | Value(th,v) ->
+    let module Th = (val th) in
+    Th.subst s v
+
+let solve n m =
+  match n with
+  | Value(nth,nv) ->
+    let module NTh = (val nth) in
+    match NTh.kind with
+    | Other -> NTh.solve nv m
+    | Polite ->
+      match m with
+      | Value(mth,mv) ->
+        let module MTh = (val mth) in
+        MTh.solve mv n
 
 module ClHashcons = struct
   type t = cl
 
   let hash n =
     match n.base with
-    | Cst i -> 2 * (i :> int)
-    | App(g,f) -> 3 * g.tag + 5 * f.tag
+    | Value(nth, n) ->
+      let module Nth = (val nth) in
+      3 * Nth.id + 17 * Nth.hash n
 
-  let equal n m =
-    match n.base, m.base with
-    | Cst i, Cst j -> i = j
-    | App (g1,f1), App(g2,f2) -> g1.tag = g2.tag && f1.tag = f2.tag
-    | _ -> false
+  let equal n m = equal n.base m.base
 
   let tag tag node = {node with tag}
 end
 
-module Cl = struct
-  type t = cl
-  module Cl = MakeMSH(struct type t = cl let tag t = t.tag end)
-  include Cl.T
-  let rec print fmt cl = Format.fprintf fmt "@[@@%i@]" cl.tag
-  include Cl
-end
-
+let print_depth = ref 7
 
 module UnionFind =
 struct
@@ -87,14 +181,12 @@ struct
   let repr exn t cl = Cl.M.find_exn exn cl t.repr
 
   let rec print_value nb env fmt v =
-      match v with
-      | Cst i -> Format.fprintf fmt "%a"
-        Strings.Hashcons.print i
-      | App (f,g) -> Format.fprintf fmt "(@[%a@],@,@[%a@])"
-        (print_repr nb env)  f (print_repr nb env) g
-
+    match v with
+    | Value (th,v) ->
+      let module Th = (val th) in
+      Th.print (print_repr' nb env) fmt v
 
-  and print_repr nb env fmt k =
+  and print_repr' nb env fmt k =
     if nb = 0 then Cl.print fmt k else
     try
       Format.fprintf fmt "%a"
@@ -102,10 +194,10 @@ struct
     with Exit ->
       Format.pp_print_string fmt "<NoRepr>"
 
-  let print_value env fmt v = print_value 7 env fmt v
+  let print_value env fmt v = print_value (!print_depth) env fmt v
   let print_repr env fmt k =
     Format.fprintf fmt "%a[%a]"
-      Cl.print k (print_repr 7 env) k
+      Cl.print k (print_repr' (!print_depth) env) k
 
   let empty =
     { eq    = Cl.M.empty;
@@ -117,7 +209,7 @@ struct
   (** union but t2 becomes the representatives *)
   let rec find t cl =
     let r = Cl.M.find cl t.eq in
-    if Cl.T.equal cl r then r else find t r
+    if Cl.equal cl r then r else find t r
 
   let rec is_findable t cl = Cl.equal (find t cl) cl
 
@@ -143,40 +235,6 @@ struct
       basecl, {t with eq   = Cl.M.add basecl basecl t.eq}
   let base cl = cl.base
 
-
-  let cst t s = basecl t (Cst (Strings.Hashcons.make s))
-  let app t f g = basecl t (App(f,g))
-
-
-  let appl t f l =
-    let rec aux t = function
-      | [] -> assert false
-      | [a] -> a,t
-      | a::l -> let l,t = aux t l in app t a l in
-    let l,t = aux t l in
-    app t f l
-
-  let fun1 t s =
-    let f,t = cst t s in
-    (fun t x -> app t f x), t
-
-  let fun2 t s =
-    let f,t = cst t s in
-    (fun t x1 x2 -> appl t f [x1;x2]), t
-
-  let fun3 t s =
-    let f,t = cst t s in
-    (fun t x1 x2 x3 -> appl t f [x1;x2;x3]), t
-
-  let fun4 t s =
-    let f,t = cst t s in
-    (fun t x1 x2 x3 x4 -> appl t f [x1;x2;x3;x4]), t
-
-  let fun5 t s =
-    let f,t = cst t s in
-    (fun t x1 x2 x3 x4 x5 -> appl t f [x1;x2;x3;x4;x5]), t
-
-
     (** For others *)
 
 
@@ -195,7 +253,7 @@ struct
     {t with use =
         Cl.M.change (function
         | None -> invalid_arg "can't remove what is not here"
-        | Some m -> assert( Cl.M.find cl m = v );
+        | Some m -> assert( equal (Cl.M.find cl m) v );
           let m = Cl.M.remove cl m in
           if Cl.M.is_empty m then None else Some m) arg t.use}
 
@@ -235,5 +293,69 @@ struct
     Format.pp_print_flush fmt ();
     close_out cout
 
+  module Delayed = struct
+    type env = t
+    type t = env ref
+    let basecl env v =
+      let cl,e = basecl !env v in
+      env := e; cl
+  end
 
 end
+
+
+
+module type S = sig
+  type repr
+  val print: UnionFind.t -> Format.formatter -> repr -> unit
+  val make: repr -> value
+  val extract: value -> repr option
+end
+
+module type Th = sig
+  type repr
+
+  val kind: thkind
+
+  val hash: repr -> int
+  val equal: repr -> repr -> bool
+
+  val leaves: repr -> Cl.S.t
+  val subst: Cl.t Cl.M.t -> repr -> value
+  val solve: repr -> Def.value -> Cl.t Cl.M.t * value
+end
+
+module type ThMake = sig
+  type repr
+
+  module Make(X:S with type repr := repr) : sig
+    val print: (Format.formatter -> cl -> unit) ->
+      Format.formatter -> repr -> unit
+    include Th with type repr := repr
+  end
+end
+
+let thid = ref (-1)
+
+module Make(X:ThMake) = struct
+  module rec Th : ModType.Th with type repr = X.repr = struct
+    module T = X.Make(S)
+    type repr = X.repr
+    include T
+    let id = incr thid; !thid
+  end and S : S with type repr := X.repr = struct
+    let th = (module Th : ModType.Th with type repr = X.repr)
+
+    let print env fmt v =
+      Th.print (UnionFind.print_repr' (!print_depth) env) fmt v
+    let make r = Value(th,r)
+    let extract : value -> X.repr option = fun v ->
+      match v with
+      | Value(vth,r) ->
+        match eqth (th: X.repr th) vth with
+        | None -> None
+        | Some Eqtype.Eq -> Some r
+  end
+  include S
+  include (Th : Th with type repr = X.repr)
+end

src/term.mli

@@ -22,16 +22,17 @@
 
 open Stdlib
 
-type tag = private int
 
 type cl
+module Cl : Datatype with type t = cl
 
-type value =
- | Cst of Strings.Hashcons.t
- | App of cl * cl
-
+type value
 val equal: value -> value -> bool
 
+val leaves: value -> Cl.S.t
+val subst:  cl Cl.M.t -> value -> value
+val solve:  value -> value -> cl Cl.M.t * value
+
 module UnionFind (* simple *) :
 sig
   type t
@@ -44,15 +45,6 @@ sig
   val union_force: t -> cl -> cl -> t
   val iter: (cl -> cl -> unit) -> t -> unit
 
-  val cst: t -> string -> cl * t
-  val app: t -> cl -> cl -> cl * t
-
-  val fun1 : t -> string -> (t -> cl -> cl * t) * t
-  val fun2 : t -> string -> (t -> cl -> cl -> cl * t) * t
-  val fun3 : t -> string -> (t -> cl -> cl -> cl -> cl * t)  * t
-  val fun4 : t -> string -> (t -> cl -> cl -> cl -> cl -> cl * t) * t
-  val fun5 : t -> string -> (t -> cl -> cl -> cl -> cl -> cl -> cl * t) * t
-
   val repr: exn -> t -> cl -> value
   val set_repr: t -> cl -> value -> t
   val print_repr: t -> Format.formatter -> cl -> unit
@@ -69,5 +61,46 @@ sig
 
 end
 
+type thkind =
+ | Polite (** really? don't work with the representant *)
+ | Other  (** very precise... *)
+
+
+
+module type S = sig
+  type repr
+  val print: UnionFind.t -> Format.formatter -> repr -> unit
+  val make: repr -> value
+  val extract: value -> repr option
+end
+
+module type Th = sig
+  val kind: thkind
+
+  type repr
+  val hash: repr -> int
+  val equal: repr -> repr -> bool
+
+  val leaves: repr -> Cl.S.t
+  val subst:  cl Cl.M.t -> repr -> value
+  (** todo cl? et UnionFind.delayed? *)
+  (** Normally substitute only existing leaves *)
+
+  val solve: repr -> value -> cl Cl.M.t * value
+end
+
+module type ThMake = sig
+  type repr
+
+  module Make(X:S with type repr := repr) : sig
+    val print: (Format.formatter -> cl -> unit) ->
+      Format.formatter -> repr -> unit
+    include Th with type repr := repr
+  end
+end
+
+module Make(X:ThMake): sig
+  include S  with type repr = X.repr
+  include Th with type repr := X.repr
+end
 
-module Cl : Datatype with type t = cl

src/uninterp.ml

+open Term
+
+
+type t =
+| Cst of Strings.Hashcons.t
+| App of cl * cl
+
+module Th = struct
+  type repr = t
+
+  module Make(X:S with type repr := repr)= struct
+    let kind = Polite
+
+    let equal n m =
+      match n, m with
+      | Cst i, Cst j -> (i :> int) = (j :> int)
+      | App (g1,f1), App(g2,f2) -> Cl.equal g1 g2 && Cl.equal f1 f2
+      | _ -> false
+
+    let hash n =
+      match n with
+      | Cst i -> 2 * (i :> int)
+      | App(g,f) -> 3 * (Cl.hash g) + 5 * (Cl.hash f)
+
+    let print print_cl fmt v =
+      match v with
+      | Cst i -> Format.fprintf fmt "%a"
+        Strings.Hashcons.print i
+      | App (f,g) -> Format.fprintf fmt "(@[%a@],@,@[%a@])"
+        print_cl  f print_cl g
+
+    let leaves t =
+      match t with
+      | Cst _ -> Cl.S.empty
+      | App(f,g) ->
+        Cl.S.add g (Cl.S.singleton f)
+
+    (* No more classes to merge than the two given class themselves *)
+    let solve  _ v = Cl.M.empty,v
+
+    let subst s t3 =
+      match t3 with
+      | Cst _ -> assert false (** Can't substitute something without leaves *)
+      | App(f,g) ->
+        assert ( Cl.M.mem f s || Cl.M.mem g s);
+        let subst s arg = Cl.M.find_def arg arg s in
+        X.make(App (subst s f,subst s g))
+  end
+
+end
+
+
+module M = Term.Make(Th)
+type env = UnionFind.t
+
+let basecl t r = Term.UnionFind.basecl t (M.make r)
+
+  let cst t s = basecl t (Cst (Strings.Hashcons.make s))
+  let app t f g = basecl t (App(f,g))
+
+
+  let appl t f l =
+    let rec aux t = function
+      | [] -> assert false
+      | [a] -> a,t
+      | a::l -> let l,t = aux t l in app t a l in
+    let l,t = aux t l in
+    app t f l
+
+  let fun1 t s =
+    let f,t = cst t s in
+    (fun t x -> app t f x), t
+
+  let fun2 t s =
+    let f,t = cst t s in
+    (fun t x1 x2 -> appl t f [x1;x2]), t
+
+  let fun3 t s =
+    let f,t = cst t s in
+    (fun t x1 x2 x3 -> appl t f [x1;x2;x3]), t
+
+  let fun4 t s =
+    let f,t = cst t s in
+    (fun t x1 x2 x3 x4 -> appl t f [x1;x2;x3;x4]), t
+
+  let fun5 t s =
+    let f,t = cst t s in
+    (fun t x1 x2 x3 x4 x5 -> appl t f [x1;x2;x3;x4;x5]), t

src/uninterp.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2013                                                    *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Term
+
+
+type t =
+ | Cst of Strings.Hashcons.t
+ | App of cl * cl
+
+type env = UnionFind.t
+
+val cst: env -> string -> cl * env
+val app: env -> cl -> cl -> cl * env
+
+val fun1 : env -> string -> (env -> cl -> cl * env) * env
+val fun2 : env -> string -> (env -> cl -> cl -> cl * env) * env
+val fun3 : env -> string -> (env -> cl -> cl -> cl -> cl * env)  * env
+val fun4 : env -> string -> (env -> cl -> cl -> cl -> cl -> cl * env) * env
+val fun5 : env -> string -> (env -> cl -> cl -> cl -> cl -> cl -> cl * env) * env

src/util/eqtype.ml

+type (_,_) eq = Eq : ('a,'a) eq
+
+module Make(X : sig type 'a t end) =
+struct
+
+  let eq_type :
+  type a b. a X.t -> b X.t -> (a,b) eq option =
+    fun a b ->
+      if Obj.repr a == Obj.repr b
+      then Some (Obj.magic (Eq : (a,a) eq) : (a,b) eq)
+      else None
+
+end

src/util/eqtype.mli

+type (_,_) eq = Eq : ('a,'a) eq
+
+module Make(X : sig type 'a t end) : sig
+
+  val eq_type : 'a X.t -> 'b X.t -> ('a,'b) eq option
+    (** If the two arguments are physically identical then an equality witness
+        between the types is returned *)
+
+end

tests/tests_uf.ml

@@ -7,12 +7,12 @@ module Uf = Term.UnionFind
 
 let env = Uf.empty
 
-let f,env = Uf.fun1 env "f"
-let g,env = Uf.fun2 env "g"
+let f,env = Uninterp.fun1 env "f"
+let g,env = Uninterp.fun2 env "g"
 
-let a,env = Uf.cst env "a"
-let b,env = Uf.cst env "b"
-let c,env = Uf.cst env "c"
+let a,env = Uninterp.cst env "a"
+let b,env = Uninterp.cst env "b"
+let c,env = Uninterp.cst env "c"
 
 let a,env = add env a
 let b,env = add env b
@@ -55,8 +55,8 @@ let _2level' () = assert_bool "a = c => f(f(a)) = f(f(c))"
 
 let bigger () =
   let env = Uf.empty in
-  let f,env = Uf.fun1 env "f" in
-  let a,env = Uf.cst env "a" in
+  let f,env = Uninterp.fun1 env "f" in
+  let a,env = Uninterp.cst env "a" in
   let fe (c,env) = f env c in
   let rec bf env n = if n < 1 then a,env else (fe (bf env (n-1))) in
   let fffa, env = adde (bf env 3) in
@@ -108,10 +108,10 @@ let altergo1 =
   "h(x)=x and g(a,x)=a ->  g(g(a,h(x)),x)=a" >::
     fun () ->
       let env = Uf.empty in
-      let h,env = Uf.fun1 env "h" in
-      let g,env = Uf.fun2 env "g" in
-      let x,env = Uf.cst env "x" in
-      let a,env = Uf.cst env "a" in
+      let h,env = Uninterp.fun1 env "h" in
+      let g,env = Uninterp.fun2 env "g" in
+      let x,env = Uninterp.cst env "x" in
+      let a,env = Uninterp.cst env "a" in
       let hx,env = h env x in
       let env = equal env hx x in
       let gax, env = g env a x in
@@ -126,12 +126,12 @@ let altergo2 =
    h(g(g(x,y),y),a)=h(x,f(a))" >::
     fun () ->
       let env = Uf.empty in
-      let f,env = Uf.fun1 env "f" in
-      let h,env = Uf.fun2 env "h" in
-      let g,env = Uf.fun2 env "g" in
-      let x,env = Uf.cst env "x" in
-      let y,env = Uf.cst env "y" in
-      let a,env = Uf.cst env "a" in
+      let f,env = Uninterp.fun1 env "f" in
+      let h,env = Uninterp.fun2 env "h" in
+      let g,env = Uninterp.fun2 env "g" in
+      let x,env = Uninterp.cst env "x" in
+      let y,env = Uninterp.cst env "y" in
+      let a,env = Uninterp.cst env "a" in
       let rec bf env n = if n < 1 then a,env else (fe (bf env (n-1))) in
       let fffa, env = bf env 3 in
       let env = equal env fffa a in