[Choice] Fix successive add_to_group and simplify

colibri2/core/choice_group.ml

@@ -31,7 +31,10 @@ type t = {
 and choosable =
   | Choosable
   | Init
-  | Wait of { choices : Egraph.choice list; groups : t list }
+  | Wait of {
+      choices : Egraph.choice list;
+      terms_added_to_group : Nodes.ThTerm.t list;
+    }
 
 let pp_choosable fmt = function
   | Choosable -> Fmt.pf fmt "!"
@@ -45,24 +48,30 @@ let register_decision d thterm choice =
   match HThTerm.find state d thterm with
   | Choosable -> Egraph.register_decision d choice
   | Init ->
-      (* HThTerm.set state d thterm (Wait { choices = [ choice ]; groups = [] }) *)
-      HThTerm.set state d thterm Choosable;
-      Egraph.register_decision d choice
+      (* Some terms are not correctly attached, so currently with consider this case as choosable *)
+      if false then
+        HThTerm.set state d thterm
+          (Wait { choices = [ choice ]; terms_added_to_group = [] })
+      else (
+        HThTerm.set state d thterm Choosable;
+        Egraph.register_decision d choice)
   | Wait l ->
       HThTerm.set state d thterm
-        (Wait { choices = choice :: l.choices; groups = l.groups })
+        (Wait
+           {
+             choices = choice :: l.choices;
+             terms_added_to_group = l.terms_added_to_group;
+           })
+
+let empty_wait = Wait { choices = []; terms_added_to_group = [] }
 
 let add_to_group d thterm group =
-  let add_group () = Context.Queue.enqueue group.terms thterm in
   match HThTerm.find state d thterm with
   | Choosable -> ()
   | Init ->
-      HThTerm.set state d thterm (Wait { choices = []; groups = [ group ] });
-      add_group ()
-  | Wait l ->
-      add_group ();
-      HThTerm.set state d thterm
-        (Wait { choices = l.choices; groups = group :: l.groups })
+      Context.Queue.enqueue group.terms thterm;
+      HThTerm.set state d thterm empty_wait
+  | Wait _ -> Context.Queue.enqueue group.terms thterm
 
 let create d =
   (* Fmt.epr "Create_to_group@."; *)
@@ -71,7 +80,7 @@ let create d =
     terms = Context.Queue.create (Egraph.context d);
   }
 
-let make_choosable d thterm =
+let rec make_choosable d thterm =
   match HThTerm.find state d thterm with
   | Choosable -> ()
   | Init -> HThTerm.set state d thterm Choosable
@@ -79,7 +88,8 @@ let make_choosable d thterm =
       if not (List.is_empty l.choices) then
         Debug.dprintf2 debug "activate choice for %a" Nodes.ThTerm.pp thterm;
       HThTerm.set state d thterm Choosable;
-      List.iter l.choices ~f:(Egraph.register_decision d)
+      List.iter l.choices ~f:(Egraph.register_decision d);
+      List.iter l.terms_added_to_group ~f:(make_choosable d)
 
 let activate d t =
   (* Fmt.epr "Activate group@."; *)
@@ -88,17 +98,22 @@ let activate d t =
     Context.Queue.iter (make_choosable d) t.terms)
 
 let add_to_group_of d thterm thterm' =
-  let add_group groups choices =
+  let add_group () =
     match HThTerm.find state d thterm' with
     | Choosable -> make_choosable d thterm
-    | Init -> ()
-    | Wait { groups = groups'; _ } ->
-        List.iter groups' ~f:(fun group ->
-            Context.Queue.enqueue group.terms thterm);
-        HThTerm.set state d thterm (Wait { choices; groups = groups' @ groups })
+    | Init ->
+        HThTerm.set state d thterm'
+          (Wait { terms_added_to_group = [ thterm ]; choices = [] })
+    | Wait l ->
+        HThTerm.set state d thterm'
+          (Wait
+             {
+               terms_added_to_group = thterm :: l.terms_added_to_group;
+               choices = l.choices;
+             })
   in
 
   match HThTerm.find state d thterm with
   | Choosable -> ()
-  | Init -> add_group [] []
-  | Wait l -> add_group l.groups l.choices
+  | Init -> add_group ()
+  | Wait _ -> add_group ()

colibri2/tests/solve/all/unsat/dune.inc

@@ -62,6 +62,9 @@
 --dont-print-result %{dep:wp_initialize.psmt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_initialize.psmt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:wp_sharing_f_ensures.psmt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_sharing_f_ensures.psmt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:wp_simpl_is_type_f_ensures.psmt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_simpl_is_type_f_ensures.psmt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat