[Solve] normalize in set_sem

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

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 ->

tests/tests_uf.ml

 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