From 4ecc6dd5043fc82ca99f005940896b4ecce4865c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois@bobot.eu>
Date: Sun, 20 Jan 2013 14:16:19 +0100
Subject: [PATCH] [Egraph] Use classes instead of term representant
---
Makefile | 8 +-
src/egraph_simple.ml | 275 +++++++++++++++++-----------------------
src/egraph_simple.mli | 11 +-
src/term.ml | 238 ++++++++++++++++++++++++++--------
src/term.mli | 52 ++++++--
src/util/exn_printer.ml | 13 +-
tests/tests_uf.ml | 107 ++++++++++------
7 files changed, 419 insertions(+), 285 deletions(-)
diff --git a/Makefile b/Makefile
index e48aaad25..3bd2ea635 100644
--- a/Makefile
+++ b/Makefile
@@ -1,13 +1,17 @@
-.PHONY: tests tests.native
+.PHONY: tests tests.native tests_debug
all: tests
tests.native:
- ocamlbuild tests/tests.native -I src -I src/util -package oUnit
+ ocamlbuild tests/tests.native -I src -I src/util -package oUnit \
+ -tag annot -tag debug
SEEDTEST=1 2 3 4 5 6 7
tests: tests.native
./tests.native
+
+tests_debug: tests.native
+ OCAMLRUNPARAM=b ./tests.native -verbose --debug egraph_simple --debug unionfind
\ No newline at end of file
diff --git a/src/egraph_simple.ml b/src/egraph_simple.ml
index fa943e329..4a01229f0 100644
--- a/src/egraph_simple.ml
+++ b/src/egraph_simple.ml
@@ -35,192 +35,155 @@ let debug = Debug.register_info_flag
~desc:"for the simple version of the egraph"
"egraph_simple"
-module UnionFind (* simple *) :
-sig type t
- val empty: t
- val find: exn -> t -> Term.t -> Term.t
- val union: t -> Term.t -> Term.t -> t
- val iter: (Term.t -> Term.t -> unit) -> t -> unit
-end =
-struct
- type t = Term.t Term.M.t
-
- let empty = Term.M.empty
-
- let rec find exn uf t =
- let r = Term.M.find_exn exn t uf in
- if Term.equal t r then r else find exn uf r
-
- (** union but t2 becomes the representatives *)
- let union uf t1 t2 = Term.M.add t1 t2 uf
-
- let iter = Term.M.iter
-end
-
-type env =
- {
- repr : UnionFind.t;
- (** representants represent themselves. The signatures (as in DST)
- are also in this structure *)
- use : Term.S.t Term.M.t;
- (** keep the successors (in the egraph) of the terms *)
- added : Term.S.t;
- (** invariant the values in repr are always in added *)
- }
-
-let empty_env = { repr = UnionFind.empty;
- use = Term.M.empty;
- added = Term.S.empty }
+module UnionFind = Term.UnionFind
+module Cl = Term.Cl
+
+type env = UnionFind.t
(** Get the representative or raise NoRepr if the node have never be
added *)
exception NoRepr
-let repr env t = UnionFind.find NoRepr env.repr t
-
-(** Test if a node is not just a signature *)
-let is_added env t = Term.S.mem t env.added
-
-(** Return the successors of a node *)
-let use env t =
- assert (Term.equal (repr env t) t);
- (** Strange if it's used not with a representative *)
- Term.M.find_def Term.S.empty t env.use
+let repr env t = UnionFind.repr NoRepr env t
+let has_repr env t =
+ try ignore (repr env t:Term.value); true
+ with NoRepr -> false
+let print_repr = UnionFind.print_repr
-(** Normalize the term and update the use *)
-let rec normalize env t =
- try
- repr env t,env
- with NoRepr ->
- let t',env = match t.Term.value with
- | Term.Cst _ -> t,env
+(** Normalize the term and update the use
+ precondition cl is_findable
+*)
+let rec normalize env cl =
+ if has_repr env cl then cl,env
+ else begin
+ Debug.dprintf debug
+ "[EGraph] normalize @[%a@]@."
+ Cl.print cl;
+ let cl',env = match UnionFind.base cl with
+ | Term.Cst _ as v ->
+ let env = UnionFind.set_repr env cl v in
+ cl,env
| Term.App (f,g) ->
- let f,env = normalize env f in
- let g,env = normalize env g in
- let t' = Term.app f g in
- try repr env t',env
- with NoRepr ->
- match t.Term.value with
- | Term.Cst _ -> t',env
- | Term.App (f,g) ->
- let add_use use t arg =
- Term.M.change (function
- | None -> Some (Term.S.singleton t)
- | Some s -> Some (Term.S.add t s)) arg use in
- t',{env with
- use = add_use (add_use env.use t f) t g;
- repr = UnionFind.union env.repr t' t'}
+ 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
+ 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 = UnionFind.add_use env cl v clg in
+ let env = UnionFind.set_repr env cl v in
+ cl,env
in
- t',{env with repr = UnionFind.union env.repr t t'}
+ let env = UnionFind.union env cl cl' in
+ Debug.dprintf debug
+ "[EGraph] normalized @[%a@] as @[%a@]@."
+ Cl.print cl (print_repr env) cl;
+ cl',env
+ end
(** really add the term, can be used as representative *)
-let add env t =
- let rec tag env t =
- if is_added env t then env
+let add env cl =
+ let cl',env = normalize env cl in
+ Debug.dprintf debug
+ "[EGraph] Add @[@[%a@]@ as@ @[%a@]@]@."
+ (print_repr env) cl (print_repr env) cl';
+ let rec tag env cl =
+ if UnionFind.is_added env cl then env
else
- let env = {env with added = Term.S.add t env.added} in
- match t.Term.value with
+ let env = UnionFind.added env cl in
+ match repr env cl with
| Term.Cst _ -> env
| Term.App (f,g) -> tag (tag env f) g
in
- let t',env = normalize env t in
- Debug.dprintf debug
- "[EGraph] Add @[@[%a@]@ as@ @[%a@]@]@."
- Term.print t Term.print t';
- t',tag env t'
+ cl',tag env cl'
-let rec is_equal env t1 t2 =
- let t1' = repr env t1 in
- let t2' = repr env t2 in
+let rec is_equal env cl1 cl2 =
+ assert (UnionFind.is_added env cl1);
+ assert (UnionFind.is_added env cl2);
+ let cl1' = UnionFind.find env cl1 in
+ let cl2' = UnionFind.find env cl2 in
Debug.dprintf debug
"[EGraph] @[@[%a@]@,{@[%a@]} =?@ @[%a@]@,{@[%a@]}@]@."
- Term.print t1 Term.print t1' Term.print t2 Term.print t2';
- Term.equal t1' t2'
+ (print_repr env) cl1 (print_repr env) cl1' (print_repr env) cl2
+ (print_repr env) cl2';
+ Cl.equal cl1' cl2'
(** t1 -> t2, t1 must be a direct subterm of t3 *)
let subst t1 t2 t3 =
- match t3.Term.value with
- | Term.Cst _ -> assert (Term.equal t1 t3); t2
+ match t3 with
+ | Term.Cst _ -> assert false; (** can't substitute somthing without leaves *)
| Term.App(f,g) ->
- assert ( Term.equal t1 f || Term.equal t1 g);
- let subst t1 t2 arg = if Term.equal t1 arg then t2 else arg in
- Term.app (subst t1 t2 f) (subst t1 t2 g)
-
-let rec equal_aux queue env t1 t2 =
- let t1 = repr env t1 in
- let t2 = repr env t2 in
- if Term.equal t1 t2 then env else begin
+ 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)
+
+exception ExitEnv of UnionFind.t
+
+let rec equal_aux nb queue env cl1 cl2 =
+ let cl1 = UnionFind.find env cl1 in
+ let cl2 = UnionFind.find env cl2 in
+ if Cl.equal cl1 cl2 then env else begin
Debug.dprintf debug
- "[EGraph] @[@[%a@] =@ @[%a@]@]@." Term.print t1 Term.print t2;
- (* t1 -> t2 *)
- let use1 = use env t1 in
- let env = {env with repr = UnionFind.union env.repr t1 t2} in
- let fold parent env =
- (** We use the version in use because it must have t1 as leaves *)
- let parent' = subst t1 t2 parent in
- Debug.dprintf debug
- "[EGraph] @[%a[@[%a@]->@[%a@]]@]@."
- Term.print parent Term.print t1 Term.print t2;
- (** can be an old parent or even not added ( but once normalized ) *)
- let parent = repr env parent in
- let parent',env = normalize env parent' in
- (** choose which one becomes representants p1 -> p2 *)
- let p1,p2 = if not (is_added env parent') then
- begin
- (** we choose parent' -> parent since parent' is a node not added
- we need to use only representant that have been added
- (for termination)
- *)
- assert (is_added env parent);
- Debug.dprintf debug
- "[EGraph] @[@[%a@] !->@ @[%a@]@]@."
- Term.print parent' Term.print parent;
- parent', parent
- end
- else
- begin
- shufflep (parent, parent')
- end
- in
- if p1 != p2 then Queue.push (p1,p2) queue;
- env
+ "[EGraph] Equal_Aux @[@[%a@] =>@ @[%a@]@]@."
+ (print_repr env) cl1 (print_repr env) cl2;
+ (* cl1 -> cl2 *)
+ let fold clparent vparent env =
+ try
+ (** First we take the representative class
+ and then we verify that the represnentative doesn't change *)
+ let clparent = UnionFind.find env clparent in
+ (* if not (Term.equal vparent (repr env clparent)) then raise (ExitEnv env); *)
+ (** We use the version in use because it must have cl1 as leaves *)
+ let clparent',env = UnionFind.basecl env (subst cl1 cl2 vparent) in
+ Debug.dprintf debug
+ "[EGraph] @[%a[@[%a@]->@[%a@]]@]@."
+ (print_repr env) clparent (print_repr env) cl1 (print_repr env) cl2;
+ let clparent',env = normalize env clparent' in
+ if clparent != clparent' then Queue.push (clparent,clparent') queue;
+ env
+ with ExitEnv env ->
+ Debug.dprintf debug
+ "[EGraph] Use skipped %a %a@."
+ (print_repr env) clparent (UnionFind.print_value env) vparent;
+ env
+ in
+ let use1 = UnionFind.fold_use fold env cl1 in
+ (** choose which one becomes representants p1 -> p2 *)
+ let env = if not (UnionFind.is_added env cl2) then
+ begin
+ (** we choose parent' -> parent since parent' is a node not added
+ we need to use only representant that have been added
+ (for termination)
+ *)
+ assert (UnionFind.is_added env cl1);
+ Debug.dprintf debug
+ "[EGraph] @[@[%a@] !->@ @[%a@]@]@."
+ (print_repr env) cl2 (print_repr env) cl1;
+ let env = UnionFind.set_repr env cl1 (repr env cl2) in
+ let env = UnionFind.union env cl2 cl1 in
+ env
+ end
+ else
+ begin
+ let env = UnionFind.union env cl1 cl2 in
+ env
+ end
in
- let env = Term.S.fold fold use1 env in
+ let env = use1 env in
if Queue.is_empty queue then env
else
- let (t1,t2) = Queue.pop queue in
- equal_aux queue env t1 t2
+ let (cl1,cl2) = Queue.pop queue in
+ if !nb = 0 then invalid_arg ("Two many step? Cycle?");
+ decr nb;
+ equal_aux nb queue env cl1 cl2
end
let equal env t1 t2 =
let t1,t2 = shufflep (t1,t2) in
+ let nb = ref 100 in
let queue = Queue.create () in
- equal_aux queue env t1 t2
-
-let exportdot filename env =
- let cout = open_out filename in
- let fmt = Format.formatter_of_out_channel cout in
- Format.fprintf fmt "@[<2>digraph G {@\n";
- UnionFind.iter
- (fun k r -> Format.fprintf fmt "\"@[<h>%a@]\" -> \"@[<h>%a@]\";@\n"
- Term.print k Term.print r)
- env.repr;
- Term.M.iter
- (fun k s ->
- Term.S.iter (fun r ->
- Format.fprintf fmt "\"@[<h>%a@]\"@ -> \"@[<h>%a@]\"@ \
- [@[style=\"dashed\",@ constraint=false@],@ \
- color=\"gray\"];@\n"
- Term.print k Term.print r) s)
- env.use;
- Term.S.iter
- (fun s ->
- Format.fprintf fmt "\"@[<h>%a@]\"@ [@[style=\"bold\"@]];@\n"
- Term.print s)
- env.added;
- Format.fprintf fmt "}@]@.";
- Format.pp_print_flush fmt ();
- close_out cout
+ equal_aux nb queue env t1 t2
let () = Exn_printer.register (fun fmt exn ->
match exn with
diff --git a/src/egraph_simple.mli b/src/egraph_simple.mli
index f51b9d950..86344acd6 100644
--- a/src/egraph_simple.mli
+++ b/src/egraph_simple.mli
@@ -23,11 +23,8 @@
val debug: Debug.flag
-type env
+type env = Term.UnionFind.t
-val empty_env: env
-val add: env -> Term.t -> Term.t * env
-val is_equal: env -> Term.t -> Term.t -> bool
-val equal: env -> Term.t -> Term.t -> env
-
-val exportdot: string -> env -> unit
+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
diff --git a/src/term.ml b/src/term.ml
index 29f330be3..405224794 100644
--- a/src/term.ml
+++ b/src/term.ml
@@ -22,77 +22,203 @@
open Stdlib
+
+let debug = Debug.register_info_flag
+ ~desc:"for the simple version of uf"
+ "unionfind"
+
type tag = int
-type t = {
- tag : int;
- value : value;
+type cl = {
+ tag : int;
+ base : (** not the representative *) value;
}
and value =
| Cst of Strings.Hashcons.t
- | App of t * t
-
-type node = t
-
-module Node = Hashcons.Make(
- struct
- type t = node
-
- let hash n =
- match n.value with
- | Cst i -> 2 * (i :> int)
- | App(g,f) -> 3 * g.tag + 5 * f.tag
-
- let equal n m =
- match n.value, m.value with
- | Cst i, Cst j -> i = j
- | App (g1,f1), App(g2,f2) -> g1.tag = g2.tag && f1.tag = f2.tag
- | _ -> false
+ | App of cl * cl
+
+
+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
+
+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
+
+ 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 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 tag tag node = {node with tag}
- end
-)
-let dumb_tag = -1
-let cst s = Node.hashcons({tag = dumb_tag;
- value = Cst (Strings.Hashcons.make s)})
-let app f g = Node.hashcons({tag = dumb_tag; value = App(f,g)})
+module UnionFind =
+struct
-let rec print fmt k =
- match k.value with
- | Cst i -> Strings.Hashcons.print fmt i
- | App (f,g) -> Format.fprintf fmt "(@[%a@],@,@[%a@])" print f print g
+ module H = Hashcons.Make(ClHashcons)
+ type t = {
+ eq : cl Cl.M.t;
+ (** stocking value for others *)
+ repr : value Cl.M.t;
+ use : value Cl.M.t Cl.M.t;
+ added : Cl.S.t;
+ }
-let appl f l =
- let rec aux = function
- | [] -> assert false
- | [a] -> a
- | a::l -> app a (aux l) in
- app f (aux l)
+ let repr exn t cl = Cl.M.find_exn exn cl t.repr
-let fun1 s =
- let f = cst s in
- (fun x -> app f x)
+ 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
-let fun2 s =
- let f = cst s in
- (fun x1 x2 -> appl f [x1;x2])
-let fun3 s =
- let f = cst s in
- (fun x1 x2 x3 -> appl f [x1;x2;x3])
+ and print_repr nb env fmt k =
+ if nb = 0 then Cl.print fmt k else
+ try
+ Format.fprintf fmt "%a"
+ (print_value (nb-1) env) (repr Exit env k)
+ with Exit ->
+ Format.pp_print_string fmt "<NoRepr>"
-let fun4 s =
- let f = cst s in
- (fun x1 x2 x3 x4 -> appl f [x1;x2;x3;x4])
+ let print_value env fmt v = print_value 10 env fmt v
+ let print_repr env fmt k =
+ Format.fprintf fmt "%a[%a]"
+ Cl.print k (print_repr 10 env) k
-let fun5 s =
- let f = cst s in
- (fun x1 x2 x3 x4 x5 -> appl f [x1;x2;x3;x4;x5])
+ let empty =
+ { eq = Cl.M.empty;
+ repr = Cl.M.empty;
+ use = Cl.M.empty;
+ added = Cl.M.empty;
+ }
+
+ (** 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
+
+ let rec is_findable t cl = Cl.equal (find t cl) cl
+
+ let union t cl1 cl2 =
+ Debug.dprintf debug "[Uf]@[ Union@ @[%a@]@ @[%a@]@]@\n"
+ (print_repr t) cl1 (print_repr t) cl2;
+ { t with eq = Cl.M.add cl1 cl2 t.eq }
+
+ let iter f t = Cl.M.iter f t.eq
+
+ let basecl t v =
+ let basecl = H.hashcons({tag = -1 (** dumb *); base = v}) in
+ try
+ find t basecl, t
+ with Not_found ->
+ 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 *)
+
+
+ let set_repr t cl v = {t with repr = Cl.M.add cl v t.repr}
+
+ let fold_use f t cl acc = Cl.M.fold f (Cl.M.find_def Cl.M.empty cl t.use) acc
+
+ let add_use t cl v arg =
+ {t with use =
+ Cl.M.change (function
+ | None -> Some (Cl.M.singleton cl v)
+ | Some m -> (* assert( not (Cl.M.mem cl m) );*)
+ Some (Cl.M.add cl v m)) arg t.use}
+
+ let is_added t cl = Cl.S.mem cl t.added
+
+ let added t cl = {t with added = Cl.S.add cl t.added}
+
+
+
+ let exportdot filename env =
+ let cout = open_out filename in
+ let fmt = Format.formatter_of_out_channel cout in
+ Format.fprintf fmt "@[<2>digraph G {@\n";
+ Cl.M.iter
+ (fun k r -> Format.fprintf fmt "@[<h>\"%a\"@] -> @[<h>\"%a\"@];@\n"
+ Cl.print k Cl.print r)
+ env.eq;
+ Cl.M.iter
+ (fun k s ->
+ Cl.M.iter (fun r _ ->
+ Format.fprintf fmt "@[<h>\"%a\"@]@ -> @[<h>\"%a\"@]@ \
+ [@[style=\"dashed\",@ constraint=false@],@ \
+ color=\"gray\"];@\n"
+ Cl.print k Cl.print r) s)
+ env.use;
+ Cl.M.iter
+ (fun k _ ->
+ Format.fprintf fmt "@[<h>\"%a\"@]@ [@[label=@[<h>\"%a\"@]@]];@\n"
+ Cl.print k (print_repr env) k)
+ env.repr;
+ Cl.S.iter
+ (fun s ->
+ Format.fprintf fmt "@[<h>\"%a\"@]@ [@[style=\"bold\"@]];@\n"
+ Cl.print s)
+ env.added;
+ Format.fprintf fmt "}@]@.";
+ Format.pp_print_flush fmt ();
+ close_out cout
-module MSH = MakeMSH(struct type t = node let tag t = t.tag end)
-include MSH
-include MSH.T
+end
diff --git a/src/term.mli b/src/term.mli
index d6987b4bb..6b84598f8 100644
--- a/src/term.mli
+++ b/src/term.mli
@@ -24,24 +24,48 @@ open Stdlib
type tag = private int
-type t = private {
- tag : tag;
- value : value;
-}
+type cl
-and value = private
+type value =
| Cst of Strings.Hashcons.t
- | App of t * t
+ | App of cl * cl
-include Datatype with type t := t
+val equal: value -> value -> bool
+module UnionFind (* simple *) :
+sig
+ type t
+ val basecl: t -> value -> cl * t
+ val base: cl -> value
+ val empty: t
+ val find: t -> cl -> cl
+ val is_findable: t -> cl -> bool (* find cl = cl *)
+ val union: t -> cl -> cl -> t
+ val iter: (cl -> cl -> unit) -> t -> unit
-val cst: string -> t
-val app: t -> t -> t
+ 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 fun1 : string -> (t -> t)
-val fun2 : string -> (t -> t -> t)
-val fun3 : string -> (t -> t -> t -> t)
-val fun4 : string -> (t -> t -> t -> t -> t)
-val fun5 : string -> (t -> t -> t -> t -> t -> t)
+ val repr: exn -> t -> cl -> value
+ val set_repr: t -> cl -> value -> t
+ val print_repr: t -> Format.formatter -> cl -> unit
+ val print_value: t -> Format.formatter -> value -> unit
+
+ val add_use : t -> cl -> value -> cl -> t
+ val fold_use : (cl -> value -> 'a -> 'a) -> t -> cl -> 'a -> 'a
+ val is_added : t -> cl -> bool
+ val added : t -> cl -> t
+
+
+ val exportdot: string -> t -> unit
+
+end
+
+
+module Cl : Datatype with type t = cl
diff --git a/src/util/exn_printer.ml b/src/util/exn_printer.ml
index d570c9e20..3c452c4f1 100644
--- a/src/util/exn_printer.ml
+++ b/src/util/exn_printer.ml
@@ -15,12 +15,6 @@ let exn_printers =
(Stack.create () : (Format.formatter -> exn -> unit) Stack.t)
let register exn_printer = Stack.push exn_printer exn_printers;
- Printexc.register_printer (fun exn -> Some (Pp.string_of exn_printer exn))
-
-let () =
- let all_exn_printer fmt exn =
- Format.fprintf fmt "anomaly: %s" (Printexc.to_string exn) in
- register all_exn_printer
exception Exit_loop
@@ -30,9 +24,10 @@ let exn_printer fmt exn =
Format.fprintf fmt "@[%a@]" f exn;
raise Exit_loop
with
- | Exit_loop -> raise Exit_loop
+ | Exit_loop -> raise exn
| _ -> ()
in
- try Stack.iter test exn_printers
- with Exit_loop -> ()
+ Stack.iter test exn_printers
+let () =
+ Printexc.register_printer (fun exn -> Some (Pp.string_of exn_printer exn))
diff --git a/tests/tests_uf.ml b/tests/tests_uf.ml
index 812370f0d..d19e09b00 100644
--- a/tests/tests_uf.ml
+++ b/tests/tests_uf.ml
@@ -1,15 +1,18 @@
open OUnit
-let f = Term.cst "f"
-let g = Term.cst "g"
-
-let a = Term.cst "a"
-let b = Term.cst "b"
-let c = Term.cst "c"
-
module Tests(E: module type of Egraph_simple) = struct
open E
-let env = empty_env
+
+module Uf = Term.UnionFind
+
+let env = Uf.empty
+
+let f,env = Uf.fun1 env "f"
+let g,env = Uf.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 = add env a
let b,env = add env b
@@ -28,30 +31,40 @@ let trans () = let env = (equal (equal env a b) b c) in
let basic = "Basic" >::: ["empty" >:: empty; "tauto" >:: tauto;
"trans" >:: trans]
-let fa,env = add env (Term.app f a)
-let fb,env = add env (Term.app f b)
+let adde (c,env) = add env c
+
+let fa,env = adde (f env a)
+let fb,env = adde (f env b)
let refl () = assert_bool "f(a) = f(a)" (is_equal env fa fa)
let empty () = assert_bool "f(a) != f(b)" (not (is_equal env fa fb))
let congru () = assert_bool "a = b => f(a) = f(b)"
(is_equal (equal env a b) fa fb)
-let ffa,env = add env (Term.app f fa)
-let ffb,env = add env (Term.app f fb)
+let ffa,env = adde (f env fa)
+let ffb,env = adde (f env fb)
let _2level () = assert_bool "a = b => f(f(a)) = f(f(b))"
(is_equal (equal env a b) ffa ffb)
-let ffc,env = add env (Term.app f (Term.app f c))
+let fe (c,env) = f env c
+
+let ffc,env = adde (fe (f env c))
let _2level' () = assert_bool "a = c => f(f(a)) = f(f(c))"
(is_equal (equal env a c) ffa ffc)
let bigger () =
- let env = empty_env in
- let rec bf n = if n < 1 then a else (Term.app f (bf (n-1))) in
- let fffa, env = add env (bf 3) in
- let fffffa, env = add env (bf 5) in
+ let env = Uf.empty in
+ let f,env = Uf.fun1 env "f" in
+ let a,env = Uf.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
+ let fffffa, env = adde (bf env 5) in
+ Uf.exportdot "bigger0.dot" env;
let env = equal env a fffa in
+ Uf.exportdot "bigger1.dot" env;
let env = equal env fffffa a in
+ Uf.exportdot "bigger2.dot" env;
assert_bool "a = f(f(f(a))) => f(f(f(f(f(a))))) = a => f(a) = a"
(is_equal env fa a)
@@ -61,15 +74,15 @@ let congru1 = "Congru 1 arg" >::: ["refl" >:: refl; "congru" >:: congru;
"bigger" >:: bigger]
-let gab,env = add env (Term.app g (Term.app a b))
-let gaa,env = add env (Term.app g (Term.app a a))
-let gbb,env = add env (Term.app g (Term.app b b))
+let gab,env = adde (g env a b)
+let gaa,env = adde (g env a a)
+let gbb,env = adde (g env b b)
let refl () = assert_bool "g(a,b) = g(a,b)" (is_equal env gab gab)
let congru () = assert_bool "a = b => g(a,b) = g(a,a)"
(is_equal (equal env a b) gab gaa)
let _2level () =
- let ggabb,env = add env (Term.app g (Term.app gab b)) in
+ let ggabb,env = adde (g env gab b) in
(* f(a,b) = a, show f(f(a,b),b) = a *)
assert_bool "g(a,b) = a => g(g(a,b),b) = a"
(is_equal (equal env gab a) ggabb a)
@@ -92,31 +105,43 @@ let is_equal env x y =
let altergo1 =
"h(x)=x and g(a,x)=a -> g(g(a,h(x)),x)=a" >::
fun () ->
- let env = empty_env in
- let h = Term.fun1 "h" in
- let g = Term.fun2 "g" in
- let x = Term.cst "x" in
- let a = Term.cst "a" in
- let env = equal env (h x) x in
- let env = equal env (g a x) a in
- assert_bool ""
- (is_equal env (g (g a (h x)) x) a)
+ 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 hx,env = h env x in
+ let env = equal env hx x in
+ let gax, env = g env a x in
+ let env = equal env gax a in
+ let hx, env = h env x in
+ let gahx, env = g env a hx in
+ let ggahxx, env = g env gahx x in
+ assert_bool "" (is_equal env ggahxx a)
let altergo2 =
"f(f(f(a)))=a and f(f(f(f(f(a)))))=a and g(x,y)=x -> \
h(g(g(x,y),y),a)=h(x,f(a))" >::
fun () ->
- let env = empty_env in
- let f = Term.fun1 "f" in
- let h = Term.fun2 "h" in
- let g = Term.fun2 "g" in
- let x = Term.cst "x" in
- let y = Term.cst "y" in
- let a = Term.cst "a" in
- let env = equal env (f (f (f a))) a in
- let env = equal env (f (f (f (f (f a))))) a in
- let env = equal env (g x y) x in
- assert_bool "" (is_equal env (h (g (g x y) y) a) (h x (f a)))
+ 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 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
+ let fffffa, env = bf env 5 in
+ let env = equal env fffffa a in
+ let gxy, env = g env x y in
+ let env = equal env gxy x in
+ let ggxyy, env = g env gxy y in
+ let hggxyya, env = h env ggxyy a in
+ let fa, env = f env a in
+ let hxfa, env = h env x fa in
+ assert_bool "" (is_equal env hggxyya hxfa)
--
GitLab