From 4584d5ed48b9436ccedfeda4ca29769a30f13a2a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois@bobot.eu>
Date: Tue, 5 Feb 2013 22:41:30 +0100
Subject: [PATCH] [Solve] normalize in set_sem
---
src/solver.ml | 21 ++++--
src/uninterp.ml | 2 -
tests/tests_uf.ml | 178 ++++++++++++++++++++++++----------------------
3 files changed, 105 insertions(+), 96 deletions(-)
diff --git a/src/solver.ml b/src/solver.ml
index 6c50291e8..51c4cc95f 100644
--- a/src/solver.ml
+++ b/src/solver.ml
@@ -294,10 +294,15 @@ module Delayed = struct
let is_repr t cl = Cl.equal (Cl.M.find cl t.env.repr) cl
+ let is_normalized t cl = Cl.M.mem cl t.env.repr
+
let add_pending_merge (t : t) cl cl' =
+ assert (is_normalized t cl);
+ assert (is_normalized t cl');
Queue.add (Merge (cl,cl')) t.todo
let add_pending_set_sem (type a) (t : t) (sem : 'a sem) cl (v:'a) =
+ assert (is_normalized t cl);
Queue.add (SetSem (sem,cl,v)) t.todo
let get_dom t dom cl = get_dom t.env dom cl
@@ -344,7 +349,10 @@ module Delayed = struct
Simple_vector.set t.env.sem sem (module SemTable');
match cl' with
| None -> ()
- | Some cl' -> add_pending_merge t cl cl'
+ | Some cl' ->
+ (** come from invtable, can be just indexed *)
+ let cl' = normalize t cl' in
+ add_pending_merge t cl cl'
(*
merge:
@@ -356,8 +364,7 @@ module Delayed = struct
*)
let choose_repr cl1 cl2 =
- (* (Shuffle.shufflep (cl1,cl2)) *)
- (min cl1 cl2, max cl1 cl2)
+ (Shuffle.shufflep (cl1,cl2))
let merge_sem t cl1 cl2 repr_cl =
assert (Cl.equal repr_cl cl1 || Cl.equal repr_cl cl2);
@@ -451,7 +458,9 @@ module Delayed = struct
let set_dom t = assert false
let rec do_pending t =
- try
+ if Queue.is_empty t.todo
+ then Debug.dprintf debug "[Solver] @[do_pending Nothing@]@."
+ else begin
begin match Queue.pop t.todo with
| Merge (cl1,cl2) ->
Debug.dprintf debug "[Solver] @[do_pending Merge %a %a@]@."
@@ -463,9 +472,7 @@ module Delayed = struct
set_sem_pending t sem cl v
end;
do_pending t
- with Queue.Empty ->
- Debug.dprintf debug "[Solver] @[do_pending Nothing@]@."
-
+ end
let if_cl_change t cl f =
let events = {clcallback = f}::(Cl.M.find_def [] cl t.env.event) in
diff --git a/src/uninterp.ml b/src/uninterp.ml
index 505ea90ce..23486db86 100644
--- a/src/uninterp.ml
+++ b/src/uninterp.ml
@@ -133,7 +133,6 @@ module Registered = RegisterSem(Th)
Cl.print arg (Th.print Cl.print) s;
Delayed.if_cl_change d arg (subst s)
-
and subst t3 d ~old:t1 t2 =
Debug.dprintf debug "[Uninterp] @[subst %a[%a -> %a]@]@."
(Th.print Cl.print) t3 Cl.print t1 Cl.print t2;
@@ -152,7 +151,6 @@ module Registered = RegisterSem(Th)
add_daemon d g s;
Delayed.set_sem d sem cl3 s
-
let propagate env =
Solver.if_propagate_sem env sem
( fun d cl s ->
diff --git a/tests/tests_uf.ml b/tests/tests_uf.ml
index b11410f46..ad37332d3 100644
--- a/tests/tests_uf.ml
+++ b/tests/tests_uf.ml
@@ -1,7 +1,5 @@
open OUnit
-let r = ref 0
-
module Tests(E: sig end) = struct
open Solver
@@ -77,7 +75,6 @@ let _2level' () =
let bigger () =
- incr r;
let env = new_t () in
Uninterp.propagate env;
let f = Uninterp.fun1 env "f" in
@@ -86,13 +83,10 @@ let bigger () =
let fa = !$ env (bf 1) in
let fffa = !$ env (bf 3) in
let fffffa = !$ env (bf 5) in
- output_graph (Format.sprintf "bigger%i_1.dot" !r) env;
equal env a fffa;
- output_graph (Format.sprintf "bigger%i_2.dot" !r) env;
assert_bool "a = f(f(f(a))) => f(a) != a"
(not (is_equal env fa a));
equal env fffffa a;
- output_graph (Format.sprintf "bigger%i_3.dot" !r) env;
assert_bool "a = f(f(f(a))) => f(f(f(f(f(a))))) = a => f(a) = a"
(is_equal env fa a)
@@ -104,87 +98,97 @@ let congru1 = "Congru 1 arg" >::: ["refl" >:: refl; "congru" >:: congru;
"bigger" >:: bigger]
-(* let gab = adde (g env a b) *)
-(* let gaa = adde (g env a a) *)
-(* let gbb = 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 notcongru () = assert_bool "a = g(a,b) => g(a,b) != g(a,a)" *)
-(* (not (is_equal (equal env a gab) gab gaa)) *)
-(* let _2level () = *)
-(* let ggabb = 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) *)
-
-(* let congru2 = "congru 2 args" >::: ["refl" >:: refl; "congru" >:: congru; *)
-(* "2level" >:: _2level;] *)
-
-(* let equal env x y = *)
-(* let x = add env x in *)
-(* let y = add env y in *)
-(* equal env x y *)
-
-
-(* let is_equal env x y = *)
-(* let x = add env x in *)
-(* let y = add env y in *)
-(* 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 = Uf.empty in *)
-(* let h = Uninterp.fun1 env "h" in *)
-(* let g = Uninterp.fun2 env "g" in *)
-(* let x = Uninterp.cst env "x" in *)
-(* let a = Uninterp.cst env "a" in *)
-(* let hx = 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 = Uf.empty in *)
-(* let f = Uninterp.fun1 env "f" in *)
-(* let h = Uninterp.fun2 env "h" in *)
-(* let g = Uninterp.fun2 env "g" in *)
-(* let x = Uninterp.cst env "x" in *)
-(* let y = Uninterp.cst env "y" in *)
-(* let a = Uninterp.cst env "a" in *)
-(* let rec bf env n = if n < 1 then a 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) *)
-
-
-
-(* let altergo = "altergo tests" >::: [altergo1; altergo2] *)
-
-(* let files = ["tests/tests_altergo_qualif.split"] *)
-
-(* let altergo = TestList (List.map Tests_lib.test_split files) *)
-
-
-let tests = TestList [basic;congru1;(*congru2;altergo *)]
+let gab = !$ env (g env a b)
+let gaa = !$ env (g env a a)
+let gbb = !$ env (g env b b)
+
+let refl () = assert_bool "g(a,b) = g(a,b)" (is_equal env gab gab)
+let congru () =
+ let env = new_handler env in
+ equal env a b;
+ assert_bool "a = b => g(a,b) = g(a,a)"
+ (is_equal env gab gaa)
+let notcongru () =
+ let env = new_handler env in
+ equal env a gab;
+ assert_bool "a = g(a,b) => g(a,b) != g(a,a)"
+ (not (is_equal env gab gaa))
+let _2level () =
+ let env = new_handler env in
+ let ggabb = !$ env (g env gab b) in
+ equal env gab a;
+ (* 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 env ggabb a)
+
+let congru2 = "congru 2 args" >::: ["refl" >:: refl; "congru" >:: congru;
+ "2level" >:: _2level;]
+
+let equal env x y =
+ let x = propagate env x in
+ let y = propagate env y in
+ equal env x y
+
+
+let is_equal env x y =
+ let x = propagate env x in
+ let y = propagate env y in
+ 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 = new_t () in
+ Uninterp.propagate env;
+ let h = Uninterp.fun1 env "h" in
+ let g = Uninterp.fun2 env "g" in
+ let x = Uninterp.cst env "x" in
+ let a = Uninterp.cst env "a" in
+ let hx = h env x in
+ equal env hx x;
+ let gax = g env a x in
+ equal env gax a;
+ let hx = h env x in
+ let gahx = g env a hx in
+ let ggahxx = 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 = new_t () in
+ Uninterp.propagate env;
+ let f = Uninterp.fun1 env "f" in
+ let h = Uninterp.fun2 env "h" in
+ let g = Uninterp.fun2 env "g" in
+ let x = Uninterp.cst env "x" in
+ let y = Uninterp.cst env "y" in
+ let a = Uninterp.cst env "a" in
+ let rec bf n = if n < 1 then !$ env a else !$ env (f env (bf (n-1))) in
+ let fffa = bf 3 in
+ equal env fffa a;
+ let fffffa = bf 5 in
+ equal env fffffa a;
+ let gxy = g env x y in
+ equal env gxy x;
+ let ggxyy = g env gxy y in
+ let hggxyya = h env ggxyy a in
+ let fa = f env a in
+ let hxfa = h env x fa in
+ assert_bool "" (is_equal env hggxyya hxfa)
+
+
+
+let altergo = "altergo tests" >::: [altergo1; altergo2]
+
+let files = ["tests/tests_altergo_qualif.split"]
+
+(* let altergo2 = TestList (List.map Tests_lib.test_split files) *)
+
+
+let tests = TestList [basic;congru1;congru2;altergo;(* altergo2 *)]
end
--
GitLab