Fail early when merging node with different values

src_colibri2/core/egraph.ml

@@ -621,8 +621,9 @@ module Delayed = struct
     let old_other_s = Node.M.find_opt node1 domtable.table in
     let old_repr_s = Node.M.find_opt node2  domtable.table in
     let (module Dom) = VDom.get_dom dom in
-    Debug.dprintf13 debug_few
-      "[Egraph] @[merge dom (%a(%a),%a)@ %s@ (%a(%a),%a)@]"
+    Debug.dprintf15 debug_few
+      "[Egraph] @[merge dom %a (%a(%a),%a)@ %s@ (%a(%a),%a)@]"
+      DomKind.pp Dom.key
       Node.pp node1 Node.pp node1_0
       (Format.opt Dom.pp) old_other_s
       (if inv then "<-" else "->")
@@ -682,6 +683,21 @@ module Delayed = struct
       else
         raise Contradiction
 
+  let test_mergeable_values t node node' =
+    let old_s   = Node.M.find_opt node  t.env.value.values in
+    let old_s'  = Node.M.find_opt node' t.env.value.values in
+    match old_s, old_s' with
+    | None, None
+    | Some _, None
+    | None, Some _ -> true
+    | Some v, Some v' ->
+      if Value.equal v v'
+      then
+        (* already same value. Does that really happen? *)
+        true
+      else
+        false
+
   let finalize_merge t node1_0 node2_0 inv =
     let node1 = find t node1_0 in
     let node2  = find t node2_0  in
@@ -749,7 +765,7 @@ module Delayed = struct
     Wait.wakeup_events_list
       Events.Wait.translate_change t (Some t.env.event_any_repr) other_node
 
-  let do_delayed_merge t node1_0 node2_0 inv  =
+  let continue_merge t node1_0 node2_0 inv  =
     let dom_not_done = merge_dom t node1_0 node2_0 inv in
     if dom_not_done
     then begin
@@ -761,14 +777,16 @@ module Delayed = struct
       finalize_merge t node1_0 node2_0 inv
 
   (** merge two pending actions *)
-  let merge_pending t node1_0 node2_0 =
+  let start_merge t node1_0 node2_0 =
     let node1 = find t node1_0 in
     let node2 = find t node2_0 in
     if not (Node.equal node1 node2) then begin
+      if not (test_mergeable_values t node1 node2) then
+        raise Contradiction;
       let ((other_node0,_),(_,_)) =
         choose_repr t.env (node1_0,node1) (node2_0,node2) in
       let inv = not (Node.equal node1_0 other_node0) in
-      do_delayed_merge t node1_0 node2_0 inv
+      continue_merge t node1_0 node2_0 inv
     end
 
   (** {2 Internal scheduler} *)
@@ -816,7 +834,7 @@ module Delayed = struct
         assert (not (merge_dom ~dry_run:true t node1_0 node2_0 inv));
         (** understand why that happend.
             Is it really needed to do a fixpoint? *)
-        do_delayed_merge t node1_0 node2_0 inv;
+        continue_merge t node1_0 node2_0 inv;
         do_pending t
       | None ->
         if not (Queue.is_empty t.todo_merge) then
@@ -824,7 +842,7 @@ module Delayed = struct
           | Merge (node1,node2) ->
             Debug.dprintf4 debug "[Egraph] @[do_pending Merge %a %a@]"
               Node.pp node1 Node.pp node2;
-            merge_pending t node1 node2;
+            start_merge t node1 node2;
             do_pending t
         else if not (Queue.is_empty t.todo_ext_action) then
           (begin match Queue.pop t.todo_ext_action with

src_colibri2/popop_lib/debug.ml

@@ -158,6 +158,9 @@ let dprintf13 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 =
 let dprintf14 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 =
   if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14
 
+let dprintf15 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 =
+  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15
+
 let dprintfn ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 =
   if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15
   else

src_colibri2/popop_lib/debug.mli

@@ -137,6 +137,12 @@ val dprintf14 : ?nobox:unit -> flag ->
   'n -> 'm -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
+val dprintf15 : ?nobox:unit -> flag ->
+  ('o -> 'n -> 'm -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
+  Format.formatter, unit) format ->
+  'o -> 'n -> 'm -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
+(** Print only if the flag is set *)
+
 val dprintfn : ?nobox:unit -> flag ->
   ('o -> 'n -> 'm -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> 'z,
   Format.formatter, unit) format ->

src_colibri2/tests/solve/smt_adt/unsat/dune.inc

 (rule (action (with-stdout-to oracle (echo "unsat\n"))))
 (rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:enum.smt2}))))
 (rule (alias runtest) (action (diff oracle enum.smt2.res)))
+(rule (action (with-stdout-to enum2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:enum2.smt2}))))
+(rule (alias runtest) (action (diff oracle enum2.smt2.res)))
 (rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list0.smt2}))))
 (rule (alias runtest) (action (diff oracle list0.smt2.res)))
 (rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list1.smt2}))))

src_colibri2/tests/solve/smt_adt/unsat/enum2.smt2

+;; produced by colibri.drv ;;
+(set-logic ALL)
+
+(declare-datatype enum (
+  ( A )
+  ( B )
+  ( C )))
+
+(declare-fun f (enum) Bool)
+(declare-fun x () enum)
+
+(assert (f B))
+(assert (f C))
+(assert (not (f x)))
+(assert (not ((_ is A) x)))
+
+(check-sat)