From 27af5a8d38c1055ed9b41ef676dc407a8ad092e4 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Wed, 2 Jun 2021 10:37:36 +0200
Subject: [PATCH] Dom_interval backward cmp ?
---
src_colibri2/theories/FP/dom_interval.ml | 14 ++++++--------
1 file changed, 6 insertions(+), 8 deletions(-)
diff --git a/src_colibri2/theories/FP/dom_interval.ml b/src_colibri2/theories/FP/dom_interval.ml
index d0bb75203..88a4c5131 100644
--- a/src_colibri2/theories/FP/dom_interval.ml
+++ b/src_colibri2/theories/FP/dom_interval.ml
@@ -214,17 +214,15 @@ let converter d (f:Ground.t) =
let r = Ground.node f in
let reg n = Egraph.register d n in
let open Monad in
- let cmp test _cmp a b =
+ let cmp test cmp a b =
reg a; reg b;
let wakeup =
setb r (let+ va = get a and+ vb = get b in
- test (D.is_comparable va vb))
- (*&&
- set b (let+ va = get a and+ vr = getb r in
- backward (if vr then (com_cmp cmp) else (com_cmp (neg_cmp cmp))) va) &&
- set a (let+ vb = get b and+ vr = getb r in
- backward (if vr then cmp else (neg_cmp cmp)) vb)
- *)
+ test (D.is_comparable va vb)) &&
+ set b (let+ va = get a and+ vr = getb r in
+ backward (if vr then (com_cmp cmp) else (com_cmp (neg_cmp cmp))) va) &&
+ set a (let+ vb = get b and+ vr = getb r in
+ backward (if vr then cmp else (neg_cmp cmp)) vb)
in
List.iter (fun n -> wait.for_dom d dom n wakeup) [a;b];
wait.for_value d Boolean.BoolValue.key r wakeup
--
GitLab