From 3ff240f52aa55f4ebfd948a3302e9b79a7e509ef Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois@bobot.eu>
Date: Thu, 17 Jan 2013 18:24:17 +0100
Subject: [PATCH] [Test] Generic infrastructure
---
.gitignore | 15 +++++++++++++++
Makefile | 13 +++++++++++++
src/egraph_simple.ml | 19 ++++++++++---------
src/egraph_simple.mli | 1 +
tests/tests.ml | 28 ++++++++++++++++++++++++++++
src/test.ml => tests/tests_uf.ml | 17 ++++-------------
6 files changed, 71 insertions(+), 22 deletions(-)
create mode 100644 .gitignore
create mode 100644 Makefile
create mode 100644 tests/tests.ml
rename src/test.ml => tests/tests_uf.ml (85%)
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 000000000..e9a773aee
--- /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 000000000..e48aaad25
--- /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 1fcc2998f..c482deefd 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 51c57bad9..a955ecae6 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 000000000..e05bc3da3
--- /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 937bfbfe0..4328a45a7 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
--
GitLab