From 6f1fd15b0ecbe5d6e81f8cd757cf4f9bfe829a08 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 11 May 2021 14:58:24 +0200
Subject: [PATCH] [Bool] it is LRA that should decide on its literals if
fourier needs it
---
src_colibri2/theories/LRA/fourier.ml | 3 ++-
src_colibri2/theories/bool/boolean.ml | 3 ---
2 files changed, 2 insertions(+), 4 deletions(-)
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 06f226218..046503fd8 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -259,7 +259,8 @@ let converter d (f:Ground.t) =
IArray.iter ~f:attach args;
Egraph.attach_value d (Ground.node f) Boolean.dom Daemon.key ();
Datastructure.Push.push comparisons d f;
- Egraph.register_delayed_event d Daemon.key ()
+ Egraph.register_delayed_event d Daemon.key ();
+ Egraph.register_decision d (Boolean.chobool (Ground.node f))
| _ -> ()
let init env =
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index ad5c4d0bb..aff3d50e4 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -323,9 +323,6 @@ let converter d (f:Ground.t) =
| { app = {builtin = Expr.False}; tyargs = []; args; _ } ->
assert ( IArray.is_empty args);
reg _false
- | { ty; _ }
- when Ground.Ty.equal ty Ground.Ty.bool ->
- Egraph.register_decision d (chobool res)
| _ -> ()
--
GitLab