From ac414990321917aada7a93fc95879c88906feb02 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 11 May 2021 15:39:17 +0200
Subject: [PATCH] Add a debugging message for each contradiction
and a debugging flag --debug-flag contradiction
---
src_colibri2/core/egraph.ml | 28 +++++++++------
src_colibri2/core/egraph.mli | 1 +
src_colibri2/core/interp.ml | 4 +--
src_colibri2/theories/ADT/adt.ml | 38 ++++++++++++++++----
src_colibri2/theories/LRA/dom_interval.ml | 11 ++++--
src_colibri2/theories/LRA/dom_polynome.ml | 12 +++++--
src_colibri2/theories/LRA/fourier.ml | 6 +++-
src_colibri2/theories/bool/equality.ml | 8 ++++-
src_colibri2/theories/quantifier/uninterp.ml | 7 +++-
9 files changed, 89 insertions(+), 26 deletions(-)
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index 8cf416a78..ef1ac0677 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -31,6 +31,9 @@ let debug_few = Debug.register_info_flag
~desc:"for the core solver"
"Egraph.few"
+let print_decision = Colibri2_popop_lib.Debug.register_flag ~desc:"Print@ information@ about@ the@ decisions@ made" "decision"
+let print_contradiction = Colibri2_popop_lib.Debug.register_flag ~desc:"Print@ information@ about@ the@ contradiction@ found" "contradiction"
+
let stats_set_dom =
Debug.register_stats_int ~name:"Egraph.set_dom/merge" ~init:0
let stats_set_value =
@@ -707,23 +710,31 @@ module Delayed = struct
then
(* already same value. Does that really happen? *)
()
- else
+ else begin
+ Debug.dprintf8 print_contradiction
+ "[Egraph] %a and %a are merged with conflicting values %a and %a"
+ Node.pp node0 Node.pp node0' Value.pp v Value.pp v';
raise Contradiction
+ end
- let test_mergeable_values t node node' =
+ let check_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
+ | None, Some _ -> ()
| Some v, Some v' ->
if Value.equal v v'
then
(* already same value. Does that really happen? *)
- true
- else
- false
+ ()
+ else begin
+ Debug.dprintf8 print_contradiction
+ "[Egraph] %a and %a are merged with conflicting values %a and %a"
+ Node.pp node Node.pp node' Value.pp v Value.pp v';
+ raise Contradiction
+ end
let finalize_merge t node1_0 node2_0 inv =
let node1 = find t node1_0 in
@@ -812,8 +823,7 @@ module Delayed = struct
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;
+ check_mergeable_values t node1 node2;
let ((other_node0,_),(_,_)) =
choose_repr t.env (node1_0,node1) (node2_0,node2) in
let inv = not (Node.equal node1_0 other_node0) in
@@ -1207,8 +1217,6 @@ let () = Exn_printer.register (fun fmt exn ->
| exn -> raise exn
)
-let print_decision = Colibri2_popop_lib.Debug.register_flag ~desc:"Print@ information@ about@ the@ decisions@ made" "decision"
-
type theory = t -> unit
let theories = ref []
diff --git a/src_colibri2/core/egraph.mli b/src_colibri2/core/egraph.mli
index 8c1b52fa8..9473dbe20 100644
--- a/src_colibri2/core/egraph.mli
+++ b/src_colibri2/core/egraph.mli
@@ -191,6 +191,7 @@ module Backtrackable: sig
end
val print_decision: Colibri2_popop_lib.Debug.flag
+val print_contradiction: Colibri2_popop_lib.Debug.flag
type theory = t -> unit
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index df46fe06f..7dc91cedb 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -205,8 +205,8 @@ let check_ground_terms d =
if Option.is_none (Egraph.get_value d n) then
raise (ArgOfGroundTermWithoutValueAfterModelFixing (g, n)));
if not (check d g) then (
- Debug.dprintf2 debug "Interp: checking of %a failed" Ground.Term.pp
- (Ground.sem g);
+ Debug.dprintf2 Egraph.print_contradiction
+ "Interp: checking of %a failed" Ground.Term.pp (Ground.sem g);
Egraph.contradiction d))
module WTO = Colibri2_stdlib.Wto.Make (Node)
diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index e60358194..cc054cd26 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -45,11 +45,16 @@ module D = struct
let merged d1 d2 = Option.equal equal d1 d2
- let merge' d d1 d2 =
+ let merge' info d d1 d2 =
match (d1, d2) with
| Unk s1, Unk s2 ->
let s = Case.S.inter s1 s2 in
- if Case.S.is_empty s then Egraph.contradiction d else Unk s
+ if Case.S.is_empty s then (
+ Debug.dprintf5 Egraph.print_contradiction
+ "[ADT] The intersection of %a and %a is empty %t" Field.S.pp s1
+ Case.S.pp s2 info;
+ Egraph.contradiction d)
+ else Unk s
| One { case = c1; fields = f1 }, One { case = c2; fields = f2 } ->
if Case.equal c1 c2 then
One
@@ -62,15 +67,27 @@ module D = struct
Some n1)
f1 f2;
}
- else Egraph.contradiction d
+ else (
+ Debug.dprintf5 Egraph.print_contradiction
+ "[ADT] case conflict between %a and %a %t" Case.pp c1 Case.pp c2
+ info;
+ Egraph.contradiction d)
| (One { case = c1; _ } as d1), Unk c2
| Unk c2, (One { case = c1; _ } as d1) ->
- if Case.S.mem c1 c2 then d1 else Egraph.contradiction d
+ if Case.S.mem c1 c2 then d1
+ else (
+ Debug.dprintf5 Egraph.print_contradiction
+ "[ADT] case %a is not in %a %t" Case.pp c1 Case.S.pp c2 info;
+ Egraph.contradiction d)
let merge d (d1, n1) (d2, n2) _ =
let s =
match (d1, d2) with
- | Some d1, Some d2 -> merge' d d1 d2
+ | Some d1, Some d2 ->
+ merge'
+ (fun fmt ->
+ Fmt.pf fmt "when merging %a and %a" Node.pp n1 Node.pp n2)
+ d d1 d2
| None, Some d1 | Some d1, None -> d1
| None, None -> assert false
(* absurd: already merged *)
@@ -85,7 +102,9 @@ let upd_dom d n d2 =
match Egraph.get_dom d D.key n with
| None -> Egraph.set_dom d D.key n d2
| Some d1 ->
- let d' = D.merge' d d1 d2 in
+ let d' =
+ D.merge' (fun fmt -> Fmt.pf fmt "when updating %a" Node.pp n) d d1 d2
+ in
if not (D.equal d' d1) then Egraph.set_dom d D.key n d'
let case_of_adt ty =
@@ -189,7 +208,12 @@ let converter d (f : Ground.t) =
if vr then D.Unk (Case.S.singleton case)
else
let s = Case.S.remove case (case_of_adt adt) in
- if Case.S.is_empty s then Egraph.contradiction d else D.Unk s));
+ if Case.S.is_empty s then (
+ Debug.dprintf4 Egraph.print_contradiction
+ "[ADT] tester %a removed the only case %a of the type" Node.pp
+ r Case.pp case;
+ Egraph.contradiction d)
+ else D.Unk s));
wait.for_dom d D.key e
(setb r
(let+ ve = get e in
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index 9d36f7e3d..a905003d4 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -45,6 +45,11 @@ let () = DomKind.register(module struct
| Some i1,_, Some i2,_ ->
begin match D.inter i1 i2 with
| None ->
+ Debug.dprintf8 Egraph.print_contradiction
+ "[LRA/Dom] The intersection of %a and %a is empty when merging %a and %a"
+ D.pp i1 D.pp i2
+ Node.pp cl1
+ Node.pp cl2;
Egraph.contradiction d
| Some i ->
if not (D.equal i i1) then
@@ -128,8 +133,10 @@ let upd_dom d n' v' =
| Some old ->
match D.inter old v' with
| None ->
- Debug.dprintf6 debug "[LRA] upd node = %a d = %a d' = %a"
- Node.pp n' D.pp old D.pp v';
+ Debug.dprintf6 Egraph.print_contradiction
+ "[LRA/Dom] The intersection of %a with %a is empty when updating %a"
+ D.pp old D.pp v'
+ Node.pp n';
Egraph.contradiction d
| Some d' ->
if not (D.equal old d')
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index a1ad365b6..d5058f51b 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -125,8 +125,12 @@ module Th = struct
(** p = other *)
add_itself d other p
end
- | Cst _ ->
+ | Cst c ->
(* 0 = cst <> 0 *)
+ Debug.dprintf6 Egraph.print_contradiction
+ "[LRA/Poly] Found 0 = %a when merging %a and %a"
+ Q.pp c
+ Node.pp cl1 Node.pp cl2;
Egraph.contradiction d
| Var(q,x,p') ->
(** diff = qx + p' *)
@@ -156,8 +160,12 @@ module Th = struct
Node.pp cl Polynome.pp p1 Polynome.pp p2 Polynome.pp diff;
begin match Polynome.extract diff with
| Zero -> ()
- | Cst _ ->
+ | Cst c ->
(* 0 = cst <> 0 *)
+ Debug.dprintf4 Egraph.print_contradiction
+ "[LRA/Poly] Found 0 = %a when updating %a"
+ Q.pp c
+ Node.pp cl;
Egraph.contradiction d
| Var(q,x,p') ->
(** diff = qx + p' *)
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 046503fd8..4258775bb 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -137,7 +137,11 @@ let add_eq d eqs p bound origins =
| Some p, _ when Q.sign p < 0 ->
Debug.dprintf2 debug "[Fourier] discard %a" Ground.S.pp origins;
eqs
- | _ -> Egraph.contradiction d
+ | Some p, bound ->
+ Debug.dprintf4 Egraph.print_contradiction
+ "[LRA/Fourier] Found %a%a0"
+ Q.pp p Bound.pp bound;
+ Egraph.contradiction d
let mk_eq d bound a b =
let (!) n =
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index f77cf9d57..8afe5938c 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -79,6 +79,7 @@ module Dis : sig
type t
type elt
val pp: t Format.printer
+ val pp_elt: elt Format.printer
val empty: t
val of_node: ThE.t -> elt
val to_node: elt -> ThE.t
@@ -93,6 +94,7 @@ end = struct
type t = ThE.S.t
type elt = ThE.t
let empty = ThE.S.empty
+ let pp_elt = ThE.pp
let pp fmt s =
let aux fmt m =
ThE.M.bindings m
@@ -135,7 +137,11 @@ module D = struct
| None, Some s ->
Egraph.set_dom d dom cl1 s
| Some s1, Some s2 ->
- let s = Dis.test_disjoint (fun _ -> Egraph.contradiction d) s1 s2 in
+ let s = Dis.test_disjoint (fun c ->
+ Debug.dprintf6 Egraph.print_contradiction
+ "[Equality] The currently merged %a and %a are different since %a"
+ Node.pp cl1 Node.pp cl2 Dis.pp_elt c;
+ Egraph.contradiction d) s1 s2 in
Egraph.set_dom d dom cl1 s;
Egraph.set_dom d dom cl2 s
diff --git a/src_colibri2/theories/quantifier/uninterp.ml b/src_colibri2/theories/quantifier/uninterp.ml
index bd9e08df7..efa8d6704 100644
--- a/src_colibri2/theories/quantifier/uninterp.ml
+++ b/src_colibri2/theories/quantifier/uninterp.ml
@@ -311,7 +311,12 @@ module UFModel = struct
let lv = IArray.map ~f:interp s.args in
let v = interp (Ground.node g) in
match find d s lv with
- | Some v' -> if not (Value.equal v v') then Egraph.contradiction d
+ | Some v' ->
+ if not (Value.equal v v') then (
+ Debug.dprintf8 Egraph.print_contradiction
+ "[Uninterp] The model of %a (%a) is %a and not %a" Ground.pp g
+ Ground.Term.pp s Value.pp v' Value.pp v;
+ Egraph.contradiction d)
| None -> set d s lv v
in
let f d g = waiter.for_any_value d (Ground.node g) (check_or_update g) in
--
GitLab