From da06bb7e3f6db3f3b83c52f6294995c8c63b05c2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 1 Feb 2016 15:00:23 +0100
Subject: [PATCH] Use the simpler interface for the tests
except for arith which is not yet converted
---
src/scheduler.ml | 16 --
src/variable.ml | 2 +-
src/variable.mli | 2 +-
tests/tests_arith.ml | 81 ++++----
tests/tests_arith_uninterp.ml | 42 +++--
tests/tests_bool.ml | 64 +++----
tests/tests_lib.ml | 11 ++
tests/tests_uf.ml | 346 +++++++++++++++-------------------
8 files changed, 262 insertions(+), 302 deletions(-)
diff --git a/src/scheduler.ml b/src/scheduler.ml
index 9ebd4dfe4..af719da6b 100644
--- a/src/scheduler.ml
+++ b/src/scheduler.ml
@@ -29,22 +29,6 @@ let new_env propagatel () =
Scheduler.flush_delayed sched;
sched
-let propagate sched cl =
- let d = Scheduler.get_delayed sched in
- ignore (Solver.Delayed.register d cl);
- Scheduler.flush_delayed sched
-
-let merge sched cl1 cl2 =
- let d = Scheduler.get_delayed sched in
- Solver.Delayed.merge d Explanation.pexpfact cl1 cl2;
- Scheduler.flush_delayed sched
-
-let is_equal sched cl1 cl2 =
- Scheduler.stop_delayed sched;
- Scheduler.run_inf_step sched;
- let env = Scheduler.get_t sched in
- Solver.is_equal env cl1 cl2
-
let get_t = Scheduler.get_delayed
let run_exn = Scheduler.run_exn
diff --git a/src/variable.ml b/src/variable.ml
index 8b1c3fff9..e21f49d6a 100644
--- a/src/variable.ml
+++ b/src/variable.ml
@@ -45,7 +45,7 @@ module EDem = Demon.Fast.Register(Dem)
let cst =
let h = DStr.H.create 10 in
- fun _ ty s ->
+ fun ty s ->
try
let cl = DStr.H.find h s in
assert (Ty.equal (Cl.ty cl) ty);
diff --git a/src/variable.mli b/src/variable.mli
index 850b68941..e8764dee8 100644
--- a/src/variable.mli
+++ b/src/variable.mli
@@ -23,7 +23,7 @@ open Types
type make_dec = Cl.t -> Explanation.chogen
-val cst: Solver.d -> Ty.t -> string -> Cl.t
+val cst: Ty.t -> string -> Cl.t
(** same string, same class *)
val fresh: Ty.t -> string -> Cl.t
diff --git a/tests/tests_arith.ml b/tests/tests_arith.ml
index 216d82a02..63763d25f 100644
--- a/tests/tests_arith.ml
+++ b/tests/tests_arith.ml
@@ -6,46 +6,63 @@ open Scheduler
let new_env =
new_env [Variable.th_register; Uninterp.th_register; Arith.th_register]
+let register sched cl =
+ let d = Scheduler.get_delayed sched in
+ Solver.Delayed.register d cl;
+ Scheduler.flush_delayed sched
+
+let merge sched cl1 cl2 =
+ let d = Scheduler.get_delayed sched in
+ Solver.Delayed.merge d Explanation.pexpfact cl1 cl2;
+ Scheduler.flush_delayed sched
+
+let is_equal sched cl1 cl2 =
+ Scheduler.stop_delayed sched;
+ Scheduler.run_inf_step sched;
+ let env = Scheduler.get_t sched in
+ Solver.is_equal env cl1 cl2
+
+
let solve0 () =
let env = new_env () in
- let a = Variable.cst (get_t env) Arith.real "ar" in
- let b = Variable.cst (get_t env) Arith.real "br" in
+ let a = Variable.cst Arith.real "ar" in
+ let b = Variable.cst Arith.real "br" in
let _1 = Arith.cst (get_t env) Q.one in
let a1 = Arith.add (get_t env) a _1 in
let b1 = Arith.add (get_t env) b _1 in
- propagate env a1; propagate env b1;
+ register env a1; register env b1;
merge env a1 b1;
assert_bool "a+1 = b+1 => a = b" (is_equal env a b)
let solve1 () =
let env = new_env () in
- let a,b = Shuffle.seq2 (Variable.cst (get_t env) Arith.real) ("ar","br") in
+ let a,b = Shuffle.seq2 (Variable.cst Arith.real) ("ar","br") in
let _1 = Arith.cst (get_t env) Q.one in
let a1 = Arith.add (get_t env) a _1 in
let b1 = Arith.add (get_t env) b _1 in
let _2 = Arith.cst (get_t env) (Q.of_int 2) in
let a2 = Arith.add (get_t env) a _2 in
let b2 = Arith.add (get_t env) b _2 in
- Shuffle.seql' (propagate env) [a1; b1; a2; b2];
+ Shuffle.seql' (register env) [a1; b1; a2; b2];
merge env a1 b1;
assert_bool "a+1 = b+1 => a+2 = b+2" (is_equal env a2 b2)
let solve2 () =
let env = new_env () in
- let a,b = Shuffle.seq2 (Variable.cst (get_t env) Arith.real) ("ar","br") in
+ let a,b = Shuffle.seq2 (Variable.cst Arith.real) ("ar","br") in
let _1 = Arith.cst (get_t env) Q.one in
let a1 = Arith.add (get_t env) a _1 in
let b1 = Arith.add (get_t env) b _1 in
let _2 = Arith.cst (get_t env) (Q.of_int 2) in
let a2 = Arith.add (get_t env) a _2 in
let b2 = Arith.add (get_t env) b _2 in
- Shuffle.seql' (propagate env) [a1; b1; a2; b2];
+ Shuffle.seql' (register env) [a1; b1; a2; b2];
merge env a2 b1;
assert_bool "a+2 = b+1 => a+1 = b" (is_equal env a1 b)
let solve3 () =
let env = new_env () in
- let a,b = Shuffle.seq2 (Variable.cst (get_t env) Arith.real) ("ar","br") in
+ let a,b = Shuffle.seq2 (Variable.cst Arith.real) ("ar","br") in
let _1 = Arith.cst (get_t env) Q.one in
let b1 = Arith.add (get_t env) b _1 in
let _2 = Arith.cst (get_t env) (Q.of_int 2) in
@@ -53,15 +70,15 @@ let solve3 () =
let _3 = Arith.cst (get_t env) (Q.of_int 3) in
Shuffle.seql [
(fun () ->
- Shuffle.seql' (propagate env) [b1;a2];
+ Shuffle.seql' (register env) [b1;a2];
merge env a2 b1;
);
(fun () ->
- Shuffle.seql' (propagate env) [a;_2];
+ Shuffle.seql' (register env) [a;_2];
merge env a _2;
);
(fun () ->
- propagate env _3;
+ register env _3;
);
];
assert_bool "" (not (is_equal env b _2));
@@ -71,7 +88,7 @@ let solve3 () =
let solve4 () =
let env = new_env () in
let a,b,c =
- Shuffle.seq3 (Variable.cst (get_t env) Arith.real) ("ar","br","cr") in
+ Shuffle.seq3 (Variable.cst Arith.real) ("ar","br","cr") in
let t1 = Arith.cst (get_t env) (Q.of_int 2) in
let t1 = Arith.add (get_t env) t1 c in
let t1 = Arith.add (get_t env) a t1 in
@@ -83,21 +100,21 @@ let solve4 () =
let t3' = Arith.cst (get_t env) (Q.of_int (-3)) in
Shuffle.seql [
(fun () ->
- Shuffle.seql' (propagate env) [t1;t1'];
+ Shuffle.seql' (register env) [t1;t1'];
merge env t1 t1');
(fun () ->
- Shuffle.seql' (propagate env) [t2;t2'];
+ Shuffle.seql' (register env) [t2;t2'];
merge env t2 t2');
- (fun () -> propagate env t3');
+ (fun () -> register env t3');
];
assert_bool "a+(2+c) = b+1 => a = 2 + b => c = -3" (is_equal env c t3')
let solve5 () =
let env = new_env () in
- let a = Variable.cst (get_t env) Arith.real "ar" in
- let b = Variable.cst (get_t env) Arith.real "br" in
- let c = Variable.cst (get_t env) Arith.real "cr" in
+ let a = Variable.cst Arith.real "ar" in
+ let b = Variable.cst Arith.real "br" in
+ let c = Variable.cst Arith.real "cr" in
let t1 = Arith.sub (get_t env) b c in
let t1 = Arith.add (get_t env) a t1 in
let t1' = (Arith.cst (get_t env) (Q.of_int 2)) in
@@ -107,13 +124,13 @@ let solve5 () =
let t3' = Arith.add (get_t env) b b in
Shuffle.seql [
(fun () ->
- Shuffle.seql' (propagate env) [t1;t1'];
+ Shuffle.seql' (register env) [t1;t1'];
merge env t1 t1');
(fun () ->
- Shuffle.seql' (propagate env) [t2;t2'];
+ Shuffle.seql' (register env) [t2;t2'];
merge env t2 t2');
(fun () ->
- Shuffle.seql' (propagate env) [t3;t3'];)
+ Shuffle.seql' (register env) [t3;t3'];)
];
assert_bool "a+(b-c) = 2 => a = 2 => b + c = 2b" (is_equal env t3 t3')
@@ -122,8 +139,8 @@ let basic = "Arith.Basic" &: [solve0; solve1; solve2; solve3; solve4; solve5]
let mult0 () =
let env = new_env () in
- let a = Variable.cst (get_t env) Arith.real "ar" in
- let b = Variable.cst (get_t env) Arith.real "br" in
+ let a = Variable.cst Arith.real "ar" in
+ let b = Variable.cst Arith.real "br" in
let t1 = Arith.sub (get_t env) a b in
let t1' = Arith.mult (get_t env) a b in
let t2 = a in
@@ -132,22 +149,22 @@ let mult0 () =
let t3' = Arith.cst (get_t env) (Q.of_int 1) in
Shuffle.seql [
(fun () ->
- Shuffle.seql' (propagate env) [t1;t1'];
+ Shuffle.seql' (register env) [t1;t1'];
merge env t1 t1');
(fun () ->
- Shuffle.seql' (propagate env) [t2;t2'];
+ Shuffle.seql' (register env) [t2;t2'];
merge env t2 t2');
(fun () ->
- Shuffle.seql' (propagate env) [t3;t3'];)
+ Shuffle.seql' (register env) [t3;t3'];)
];
assert_bool "a - b = a * b -> a = 1 -> 1 = 2b" (is_equal env t3 t3')
(** test that mult normalization trigger the needed solve *)
let mult1 () =
let env = new_env () in
- let a = Variable.cst (get_t env) Arith.real "ar" in
- let b = Variable.cst (get_t env) Arith.real "br" in
- let c = Variable.cst (get_t env) Arith.real "cr" in
+ let a = Variable.cst Arith.real "ar" in
+ let b = Variable.cst Arith.real "br" in
+ let c = Variable.cst Arith.real "cr" in
let t1 = Arith.mult (get_t env) a b in
let t1 = Arith.add (get_t env) a t1 in
let t1' = Arith.add (get_t env) b c in
@@ -158,13 +175,13 @@ let mult1 () =
let t3' = Arith.cst (get_t env) (Q.of_int 1) in
Shuffle.seql [
(fun () ->
- Shuffle.seql' (propagate env) [t1;t1'];
+ Shuffle.seql' (register env) [t1;t1'];
merge env t1 t1');
(fun () ->
- Shuffle.seql' (propagate env) [t2;t2'];
+ Shuffle.seql' (register env) [t2;t2'];
merge env t2 t2');
(fun () ->
- Shuffle.seql' (propagate env) [t3;t3'];)
+ Shuffle.seql' (register env) [t3;t3'];)
];
assert_bool "a + (a * b) = (b + c) * a -> a = 2 -> c = 1"
(is_equal env t3 t3')
diff --git a/tests/tests_arith_uninterp.ml b/tests/tests_arith_uninterp.ml
index efe7823c4..335614e19 100644
--- a/tests/tests_arith_uninterp.ml
+++ b/tests/tests_arith_uninterp.ml
@@ -3,30 +3,34 @@ open OUnit
open Tests_lib
open Scheduler
-let new_env = new_env [Variable.th_register; Uninterp.th_register; Arith.th_register]
+let theories = [Variable.th_register; Uninterp.th_register; Arith.th_register]
+let run = Scheduler.run_exn ~nodec:() ~theories
+let ($$) f x = f x
let solve6 () =
- let env = new_env () in
- let a = Variable.cst (get_t env) Arith.real "ar" in
- let b = Variable.cst (get_t env) Arith.real "br" in
- let c = Variable.cst (get_t env) Arith.real "cr" in
+ let a = Variable.fresh Arith.real "ar" in
+ let b = Variable.fresh Arith.real "br" in
+ let c = Variable.fresh Arith.real "cr" in
let f = Uninterp.fun1 Arith.real "fr" in
- let t1 = Arith.sub (get_t env) b c in
- let t1 = Arith.add (get_t env) a t1 in
- let t1' = (Arith.cst (get_t env) (Q.of_int 2)) in
- let t2 = a in
- let t2' = Arith.cst (get_t env) (Q.of_int 2) in
let t3 = f c in
let t3' = f b in
- propagate env t3';
- propagate env t3;
- propagate env t1;
- propagate env t1';
- propagate env t2;
- propagate env t2';
- merge env t1 t1';
- merge env t2 t2';
- assert_bool "a+(b-c) = 2 => a = 2 => f b = f c" (is_equal env t3 t3')
+ let env = run $$ fun env ->
+ let t1 = Arith.sub env b c in
+ let t1 = Arith.add env a t1 in
+ let t1' = Arith.cst env (Q.of_int 2) in
+ let t2 = a in
+ let t2' = Arith.cst env (Q.of_int 2) in
+ register env t3';
+ register env t3;
+ register env t1;
+ register env t1';
+ register env t2;
+ register env t2';
+ merge env t1 t1';
+ merge env t2 t2'
+ in
+ assert_bool "a+(b-c) = 2 => a = 2 => f b = f c"
+ (Solver.Delayed.is_equal env t3 t3')
diff --git a/tests/tests_bool.ml b/tests/tests_bool.ml
index f277010fe..9f0fcac29 100644
--- a/tests/tests_bool.ml
+++ b/tests/tests_bool.ml
@@ -1,30 +1,12 @@
open OUnit
+open Tests_lib
open Scheduler
let theories = [Variable.th_register; Uninterp.th_register; Bool.th_register]
-let new_env = new_env theories
-
-
-let is_true ?nodec sched cl1 =
- Scheduler.stop_delayed sched;
- Scheduler.run_inf_step ?nodec sched;
- let env = Scheduler.get_delayed sched in
- Bool.is_true env cl1
-
-let is_false ?nodec sched cl1 =
- Scheduler.stop_delayed sched;
- Scheduler.run_inf_step ?nodec sched;
- let env = Scheduler.get_delayed sched in
- Bool.is_false env cl1
-
-let set_true sched cl =
- let d = Scheduler.get_delayed sched in
- let pexp = Solver.Delayed.mk_pexp d Explanation.expfact () in
- Bool.set_true d pexp cl;
- Scheduler.flush_delayed sched
-
+let run = Scheduler.run_exn ~nodec:() ~theories
+let ($$) f x = f x
let true_is_true () =
let env = Scheduler.run_exn ~nodec:() ~theories (fun _ -> ()) in
@@ -33,45 +15,41 @@ let true_is_true () =
let not_true_is_false () =
let not_true = Bool._not Bool._true in
- let env = Scheduler.run_exn ~nodec:() ~theories begin fun env ->
- Solver.Delayed.register env not_true
- end
- in
+ let env = run $$ fun env -> Solver.Delayed.register env not_true in
assert_bool "" (Bool.is_false env not_true);
assert_bool "" (not (Bool.is_true env not_true))
let and_true_is_true () =
- let env = new_env () in
let _t = Bool._true in
let _and = Bool._and [_t;_t;_t] in
- propagate env _and;
- assert_bool "" (is_true ~nodec:true env _and);
- assert_bool "" (not (is_false ~nodec:true env _and))
+ let env = run $$ fun env -> Solver.Delayed.register env _and in
+ assert_bool "" (Bool.is_true env _and);
+ assert_bool "" (not (Bool.is_false env _and))
let or_not_true_is_false () =
- let env = new_env () in
let _f = (Bool._not Bool._true) in
let _or = Bool._and [_f;_f;_f] in
- propagate env _or;
- assert_bool "" (is_false ~nodec:true env _or);
- assert_bool "" (not (is_true ~nodec:true env _or))
+ let env = run $$ fun env -> Solver.Delayed.register env _or in
+ assert_bool "" (Bool.is_false env _or);
+ assert_bool "" (not (Bool.is_true env _or))
let merge_true () =
- let env = new_env () in
let a = Variable.fresh Bool.ty "a" in
let b = Variable.fresh Bool.ty "b" in
let c = Variable.fresh Bool.ty "c" in
let d = Variable.fresh Bool.ty "d" in
let _and = Bool._and [a;b;c] in
- propagate env _and;
- List.iter (propagate env) [a;b;c;d];
- Shuffle.seql
- [(fun () -> merge env a b);
- (fun () -> merge env a c);
-];
- merge env a d;
- set_true env d;
- assert_bool "" (is_true ~nodec:true env _and)
+ let env = run $$ fun env ->
+ Solver.Delayed.register env _and;
+ List.iter (Solver.Delayed.register env) [a;b;c;d];
+ Shuffle.seql
+ [(fun () -> merge env a b);
+ (fun () -> merge env a c);
+ ];
+ merge env a d;
+ Bool.set_true env Explanation.pexpfact d;
+ in
+ assert_bool "" (Bool.is_true env _and)
diff --git a/tests/tests_lib.ml b/tests/tests_lib.ml
index 198b223ca..c2edb1c18 100644
--- a/tests/tests_lib.ml
+++ b/tests/tests_lib.ml
@@ -46,3 +46,14 @@ let (&:) s l = s >::: (List.map (fun f -> TestCase f) l)
let ty_ctr = Types.Ty.Constr.create "a"
let ty = Types.Ty.ctr ty_ctr
+
+
+let register d cl =
+ Solver.Delayed.register d cl;
+ Solver.Delayed.flush d
+
+let merge d cl1 cl2 =
+ Solver.Delayed.merge d Explanation.pexpfact cl1 cl2;
+ Solver.Delayed.flush d
+
+let is_equal = Solver.Delayed.is_equal
diff --git a/tests/tests_uf.ml b/tests/tests_uf.ml
index f4df81cdf..7e1c675de 100644
--- a/tests/tests_uf.ml
+++ b/tests/tests_uf.ml
@@ -3,127 +3,117 @@ open OUnit
open Tests_lib
open Scheduler
-let new_env = new_env [Variable.th_register; Uninterp.th_register]
+let theories = [Variable.th_register; Uninterp.th_register]
+let run = Scheduler.run_exn ~nodec:() ~theories
+let ($$) f x = f x
+
+let a = Variable.fresh ty "a"
+let b = Variable.fresh ty "b"
+let c = Variable.fresh ty "c"
+
let empty () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- propagate env a; propagate env b;
+ let env = run $$ fun env ->
+ register env a; register env b;
+ in
assert_bool "a != b" (not (is_equal env a b))
let tauto () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- propagate env a; propagate env b;
- merge env a b;
+ let env = run $$ fun env ->
+ register env a; register env b;
+ merge env a b;
+ in
assert_bool "a = b => a = b"
(is_equal env a b)
let trans () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- let c = Variable.cst (get_t env) ty "c" in
- propagate env a; propagate env b; propagate env c;
- merge env a b; merge env b c;
+ let env = run $$ fun env ->
+ register env a; register env b; register env c;
+ merge env a b; merge env b c;
+ in
assert_bool "a = b => b = c => a = c" (is_equal env a c);
assert_bool "a = b => b = c => a = b" (is_equal env a b);
assert_bool "a = b => b = c => b = c" (is_equal env b c)
let noteq () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- let c = Variable.cst (get_t env) ty "c" in
- propagate env a; propagate env b; propagate env c;
- merge env b c;
+ let env = run $$ fun env ->
+ register env a; register env b; register env c;
+ merge env b c;
+ in
assert_bool "b = c => a != c" (not (is_equal env a c))
let basic = "Uf.Basic" >::: ["empty" >:: empty; "tauto" >:: tauto;
"trans" >:: trans; "noteq" >:: noteq]
+let f = Uninterp.fun1 ty "f"
+let fa = f a
+let fb = f b
+let ffa = f (f a)
+let ffb = f (f b)
+
let refl () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let f = Uninterp.fun1 ty "f" in
- let fa = f a in
- propagate env fa;
+ let env = run $$ fun env ->
+ register env fa;
+ in
assert_bool "f(a) = f(a)" (is_equal env fa fa)
+
let empty () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- let f = Uninterp.fun1 ty "f" in
- let fa = f a in
- let fb = f b in
- propagate env fa; propagate env fb;
+ let env = run $$ fun env ->
+ register env fa; register env fb;
+ in
assert_bool "f(a) != f(b)" (not (is_equal env fa fb))
+
let congru () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- let f = Uninterp.fun1 ty "f" in
- let fa = f a in
- let fb = f b in
- Shuffle.seql [
- (fun () -> propagate env fa);
- (fun () -> propagate env fb);
- (fun () -> propagate env a);
- (fun () -> propagate env b);
- ];
- merge env a b;
+ let env = run $$ fun env ->
+ Shuffle.seql [
+ (fun () -> register env fa);
+ (fun () -> register env fb);
+ (fun () -> register env a);
+ (fun () -> register env b);
+ ];
+ merge env a b;
+ in
assert_bool "a = b => f(a) = f(b)"
(is_equal env fa fb)
let _2level () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- let f = Uninterp.fun1 ty "f" in
- let ffa = f (f a) in
- let ffb = f (f b) in
- Shuffle.seql [
- (fun () -> propagate env ffa);
- (fun () -> propagate env ffb);
- (fun () -> propagate env a);
- (fun () -> propagate env b);
- ];
- merge env a b;
+ let env = run $$ fun env ->
+ Shuffle.seql [
+ (fun () -> register env ffa);
+ (fun () -> register env ffb);
+ (fun () -> register env a);
+ (fun () -> register env b);
+ ];
+ merge env a b;
+ in
assert_bool "a = b => f(f(a)) = f(f(b))"
(is_equal env ffa ffb)
let _2level' () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- let f = Uninterp.fun1 ty "f" in
- let ffa = f (f a) in
- let ffb = f (f b) in
- propagate env a; propagate env b;
- merge env a b;
- propagate env ffa; propagate env ffb;
+ let env = run $$ fun env ->
+ register env a; register env b;
+ merge env a b;
+ register env ffa; register env ffb;
+ in
assert_bool "a = b => f(f(a)) = f(f(b))" (is_equal env ffa ffb)
let bigger () =
- let env = new_env () in
- let f = Uninterp.fun1 ty "f" in
- let a = Variable.cst (get_t env) ty "a" in
let rec bf n = if n < 1 then a else (f (bf(n-1))) in
let fa = bf 1 in
let fffa = bf 3 in
let fffffa = bf 5 in
- Shuffle.seql
- [(fun () -> propagate env a);
- (fun () -> propagate env fa);
- (fun () -> propagate env fffa);
- (fun () -> propagate env fffffa);
- ];
- Shuffle.seql
- [(fun () -> merge env a fffa);
- (fun () -> merge env fffffa a)];
+ let env = run $$ fun env ->
+ Shuffle.seql
+ [(fun () -> register env a);
+ (fun () -> register env fa);
+ (fun () -> register env fffa);
+ (fun () -> register env fffffa);
+ ];
+ Shuffle.seql
+ [(fun () -> merge env a fffa);
+ (fun () -> merge env fffffa a)];
+ in
assert_bool "a = f(f(f(a))) => f(f(f(f(f(a))))) = a => f(a) = a"
(is_equal env fa a)
@@ -135,59 +125,47 @@ let congru1 = "Uf.Congru 1 arg" >::: ["refl" >:: refl; "congru" >:: congru;
"bigger" >:: bigger]
+let g = Uninterp.fun2 ty "g"
+let gab = g a b
+let gaa = g a a
+let ggabb = g gab b
+
let refl () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- let g = Uninterp.fun2 ty "g" in
- let gab = g a b in
- propagate env gab;
+ let env = run $$ fun env -> register env gab in
assert_bool "g(a,b) = g(a,b)" (is_equal env gab gab)
let congru () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- let g = Uninterp.fun2 ty "g" in
- let gab = g a b in
- let gaa = g a a in
- Shuffle.seql [
- (fun () -> propagate env gab);
- (fun () -> propagate env gaa);
- (fun () -> propagate env a);
- (fun () -> propagate env b);
- ];
- merge env a b;
+ let env = run $$ fun env ->
+ Shuffle.seql [
+ (fun () -> register env gab);
+ (fun () -> register env gaa);
+ (fun () -> register env a);
+ (fun () -> register env b);
+ ];
+ merge env a b;
+ in
assert_bool "a = b => g(a,b) = g(a,a)"
(is_equal env gab gaa)
let notcongru () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- let g = Uninterp.fun2 ty "g" in
- let gab = g a b in
- let gaa = g a a in
- propagate env a; propagate env gab; propagate env gaa;
- merge env a gab;
+ let env = run $$ fun env ->
+ register env a; register env gab; register env gaa;
+ merge env a gab;
+ in
assert_bool "a = g(a,b) => g(a,b) != g(a,a)"
(not (is_equal env gab gaa))
let _2level () =
- let env = new_env () in
- let a = Variable.cst (get_t env) ty "a" in
- let b = Variable.cst (get_t env) ty "b" in
- let g = Uninterp.fun2 ty "g" in
- let gab = g a b in
- let ggabb = g gab b in
- Shuffle.seql [
- (fun () -> propagate env a);
- (fun () -> propagate env gab);
- ];
- Shuffle.seql [
- (fun () -> merge env gab a;);
- (fun () -> propagate env ggabb);
- ];
+ let env = run $$ fun env ->
+ Shuffle.seql [
+ (fun () -> register env a);
+ (fun () -> register env gab);
+ ];
+ Shuffle.seql [
+ (fun () -> merge env gab a;);
+ (fun () -> register env ggabb);
+ ];
+ in
assert_bool "g(a,b) = a => g(g(a,b),b) = a"
(is_equal env ggabb a)
@@ -195,81 +173,69 @@ let congru2 = "Uf.congru 2 args" >::: ["refl" >:: refl; "congru" >:: congru;
"2level" >:: _2level;]
let merge env x y =
- propagate env x;
- propagate env y;
+ register env x;
+ register env y;
merge env x y
-
-let is_equal env x y =
- propagate env x;
- propagate env y;
- is_equal env x y
-
-
-let altergo0 =
- fun () ->
- let env = new_env () in
- let h = Uninterp.fun1 ty "h" in
- let g = Uninterp.fun2 ty "g" in
- let x = Variable.cst (get_t env) ty "x" in
- let a = Variable.cst (get_t env) ty "a" in
- let hx = h x in
- let gax = g a x in
+let x = Variable.fresh ty "x"
+let y = Variable.fresh ty "y"
+
+let altergo0 () =
+ let h = Uninterp.fun1 ty "h" in
+ let g = Uninterp.fun2 ty "g" in
+ let gax = g a x in
+ let hx = h x in
+ let gahx = g a hx in
+ let ggahxx = g gahx x in
+ let env = run $$ fun env ->
Shuffle.seql
[(fun () -> merge env hx x);
(fun () -> merge env gax a)];
- let hx = h x in
- let gahx = g a hx in
- let ggahxx = g gahx x in
- assert_bool "h(x)=x and g(a,x)=a -> g(g(a,h(x)),x)=a"
- (is_equal env ggahxx a)
-
-let altergo1 =
- fun () ->
- let env = new_env () in
- let f = Uninterp.fun1 ty "f" in
- let h = Uninterp.fun2 ty "h" in
- let g = Uninterp.fun2 ty "g" in
- let x = Variable.cst (get_t env) ty "x" in
- let y = Variable.cst (get_t env) ty "y" in
- let a = Variable.cst (get_t env) ty "a" in
- let rec bf n = if n < 1 then a else f (bf (n-1)) in
- let fffa = bf 3 in
- let fffffa = bf 5 in
- let gxy = g x y in
+ register env ggahxx
+ in
+ assert_bool "h(x)=x and g(a,x)=a -> g(g(a,h(x)),x)=a"
+ (is_equal env ggahxx a)
+
+let altergo1 () =
+ let h = Uninterp.fun2 ty "h" in
+ let rec bf n = if n < 1 then a else f (bf (n-1)) in
+ let fffa = bf 3 in
+ let fffffa = bf 5 in
+ let gxy = g x y in
+ let ggxyy = g gxy y in
+ let hggxyya = h ggxyy a in
+ let fa = f a in
+ let hxfa = h x fa in
+ let env = run $$ fun env ->
Shuffle.seql
- [(fun () -> merge env fffa a);
- (fun () -> merge env fffffa a);
- (fun () -> merge env gxy x)];
- let ggxyy = g gxy y in
- let hggxyya = h ggxyy a in
- let fa = f a in
- let hxfa = h x fa in
- assert_bool
- "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))"
- (is_equal env hggxyya hxfa)
-
-let altergo2 =
- fun () ->
- let env = new_env () in
- let f = Uninterp.fun1 ty "f" in
- let h = Uninterp.fun2 ty "h" in
- let g = Uninterp.fun2 ty "g" in
- let x = Variable.cst (get_t env) ty "x" in
- let y = Variable.cst (get_t env) ty "y" in
- let a = Variable.cst (get_t env) ty "a" in
- let gxy = g x y in
- let fa = f a in
+ [(fun () -> merge env fffa a);
+ (fun () -> merge env fffffa a);
+ (fun () -> merge env gxy x)];
+ register env hggxyya;
+ register env hxfa;
+ in
+ assert_bool
+ "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))"
+ (is_equal env hggxyya hxfa)
+
+let altergo2 () =
+ let h = Uninterp.fun2 ty "h" in
+ let gxy = g x y in
+ let fa = f a in
+ let ggxyy = g gxy y in
+ let hggxyya = h ggxyy a in
+ let hxfa = h x fa in
+ let env = run $$ fun env ->
Shuffle.seql
- [(fun () -> merge env fa a);
- (fun () -> merge env gxy x)];
- let ggxyy = g gxy y in
- let hggxyya = h ggxyy a in
- let hxfa = h x fa in
- assert_bool
- "f(a) = a -> g(x,y)=x -> h(g(g(x,y),y),a)=h(x,f(a))"
- (is_equal env hggxyya hxfa)
+ [(fun () -> merge env fa a);
+ (fun () -> merge env gxy x)];
+ register env hggxyya;
+ register env hxfa;
+ in
+ assert_bool
+ "f(a) = a -> g(x,y)=x -> h(g(g(x,y),y),a)=h(x,f(a))"
+ (is_equal env hggxyya hxfa)
--
GitLab