diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..e9a773aee49ae7430dff88d0976a321363e6d4b9
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,15 @@
+
+*.tmp
+*~
+*.bak
+_build
+*.vo
+*.vd
+*.glob
+\#*\#
+*.native
+
+# /src/util/
+/src/util/config.ml
+/src/util/rc.ml
+
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..e48aaad258e52627806cf0c09f126acf9b221412
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,13 @@
+
+
+.PHONY: tests tests.native
+
+all: tests
+
+tests.native:
+ ocamlbuild tests/tests.native -I src -I src/util -package oUnit
+
+SEEDTEST=1 2 3 4 5 6 7
+
+tests: tests.native
+ ./tests.native
diff --git a/src/egraph_simple.ml b/src/egraph_simple.ml
index 1fcc2998f0e8312f37660d8bb3339e1427154d29..c482deefda75fc2580422af7be3307469d0f3e3f 100644
--- a/src/egraph_simple.ml
+++ b/src/egraph_simple.ml
@@ -20,6 +20,8 @@ let set_shuffle = function
| None -> opt_shuffle := None
| Some i -> opt_shuffle := Some (Random.State.make i)
+let is_shuffle () = !opt_shuffle <> None
+
let shuffle ((t1,t2) as p) =
match !opt_shuffle with
| None -> p
@@ -55,9 +57,6 @@ let is_added env t = Term.S.mem t env.added
(** Return the successors of a node *)
let use env t =
- assert (is_added env t);
- (** It's just impossible that the result is not empty if the node
- has never be added, so something is going on *)
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
@@ -133,7 +132,7 @@ let rec equal_aux queue env t1 t2 =
let parent = repr env parent in
let parent',env = normalize env parent' in
(** choose which one becomes representants p1 -> p2 *)
- if not (is_added env parent') then
+ 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
@@ -143,14 +142,16 @@ let rec equal_aux queue env t1 t2 =
Debug.dprintf debug
"[EGraph] @[@[%a@] !->@ @[%a@]@]@."
Term.print parent' Term.print parent;
- {env with repr = Term.M.add parent' parent env.repr}
+ parent', parent
end
else
begin
- let p1, p2 = shuffle (parent, parent') in
- if p1 != p2 then Queue.push (p1,p2) queue;
- env
- end in
+ shuffle (parent, parent')
+ end
+ in
+ if p1 != p2 then Queue.push (p1,p2) queue;
+ env
+ in
let env = Term.S.fold fold use1 env in
if Queue.is_empty queue then env
else
diff --git a/src/egraph_simple.mli b/src/egraph_simple.mli
index 51c57bad9d80abf076f9db5349dff0a9ccbaadce..a955ecae67ca7b68a8c1f93e89ef8d47d546d07b 100644
--- a/src/egraph_simple.mli
+++ b/src/egraph_simple.mli
@@ -1,6 +1,7 @@
val debug: Debug.flag
val set_shuffle: int array option -> unit
+val is_shuffle: unit -> bool
type env
diff --git a/tests/tests.ml b/tests/tests.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e05bc3da38659a16b2abb4253543c92c86252025
--- /dev/null
+++ b/tests/tests.ml
@@ -0,0 +1,28 @@
+open OUnit
+
+let opt_seed = ref 0
+
+let print_seed fmt = function
+ | None -> Format.fprintf fmt "No"
+ | Some [|i|] -> Format.fprintf fmt "%i" i
+ | _ -> assert false
+
+let rec make_tests acc seed =
+ let module Uf = Tests_uf.Tests(Egraph_simple) in
+ let test = ((Pp.sprintf "seed %a" print_seed seed) >::: [Uf.tests]) in
+ let test = test_decorate
+ (fun f -> (fun () -> Egraph_simple.set_shuffle seed; f ())) test in
+ test::acc
+
+let tests =
+ let l = Util.foldi (fun acc i -> make_tests acc (Some [|i|])) []
+ (!opt_seed + 1) (!opt_seed + 10)in
+ make_tests l None
+
+let _ =
+ run_test_tt_main
+ ~set_verbose:(fun _ -> Debug.Args.set_flags_selected () )
+ ~arg_specs:["--seed",Arg.Set_int opt_seed,
+ " Base seed used for shuffling the arbitrary decision";
+ Debug.Args.desc_debug]
+ (TestList tests)
diff --git a/src/test.ml b/tests/tests_uf.ml
similarity index 85%
rename from src/test.ml
rename to tests/tests_uf.ml
index 937bfbfe0374e20afe4fdd2f02732f9ea8ab9a37..4328a45a774a045dbebadf3d56a85a494abae62e 100644
--- a/src/test.ml
+++ b/tests/tests_uf.ml
@@ -7,8 +7,8 @@ let a = Term.cst "a"
let b = Term.cst "b"
let c = Term.cst "c"
-open Egraph_simple
-
+module Tests(E: module type of Egraph_simple) = struct
+open E
let env = empty_env
let a,env = add env a
@@ -50,11 +50,8 @@ let bigger () =
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
- exportdot "bigger_1.dot" env;
let env = equal env a fffa in
- exportdot "bigger_2.dot" env;
let env = equal env fffffa a in
- exportdot "bigger_3.dot" env;
assert_bool "a = f(f(f(a))) => f(f(f(f(f(a))))) = a => f(a) = a"
(is_equal env fa a)
@@ -80,13 +77,7 @@ let _2level () =
let congru2 = "congru 2 args" >::: ["refl" >:: refl; "congru" >:: congru;
"2level" >:: _2level;]
-let test = TestList [basic;congru1;congru2]
+let tests = TestList [basic;congru1;congru2]
-let _ =
- run_test_tt_main
- ~set_verbose:(fun _ -> Debug.Args.set_flags_selected () )
- ~arg_specs:["--seed",Arg.Int (fun i -> set_shuffle (Some [|i|])),
- " Seed used for shuffling the arbitrary decision";
- Debug.Args.desc_debug]
- test
+end