From 926a0c241e0d863addd2ba39642871986e087c6c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 7 Jun 2021 13:44:32 +0200
Subject: [PATCH] [Boolean] Some cleanup
---
src_colibri2/theories/bool/boolean.ml | 36 +++------------------------
1 file changed, 3 insertions(+), 33 deletions(-)
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index fdcb9c426..ea064fe48 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -260,9 +260,6 @@ module TwoWatchLiteral = struct
let create = Daemon.create
end
-let wait_for_this_node_get_a_value d n =
- Daemon.attach_value d n BoolValue.key
-
let converter d (f:Ground.t) =
let res = Ground.node f in
let reg_args args = IArray.iter ~f:(Egraph.register d) args in
@@ -294,12 +291,12 @@ let converter d (f:Ground.t) =
if v then set_bool d res true
else if is_true d res then set_bool d a false
in
- List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;res]
+ List.iter (fun n -> Daemon.attach_value d n BoolValue.key wait) [a;b;res]
| { app = {builtin = Expr.Neg}; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
reg_args args;
- wait_for_this_node_get_a_value d a (fun d _ v -> set_bool d res (not (BoolValue.value v)));
- wait_for_this_node_get_a_value d res (fun d _ v -> set_bool d a (not (BoolValue.value v)))
+ Daemon.attach_value d a BoolValue.key (fun d _ v -> set_bool d res (not (BoolValue.value v)));
+ Daemon.attach_value d res BoolValue.key (fun d _ v -> set_bool d a (not (BoolValue.value v)))
| { app = {builtin = Expr.True}; tyargs = []; args; _ } ->
assert ( IArray.is_empty args);
reg _true
@@ -351,30 +348,3 @@ let th_register env =
()
let () = Egraph.add_default_theory th_register
-
-(** {2 Interpretations} *)
-(* let () =
- * let interp ~interp t =
- * let v =
- * IArray.fold (fun acc (n,b) ->
- * acc ||
- * let v = BoolValue.value (BoolValue.coerce_nodevalue (interp n)) in
- * if b then not v else v
- * ) false t.T.lits
- * in
- * let v = if t.T.topnot then not v else v in
- * BoolValue.nodevalue (if v then value_true else value_false)
- * in
- * Interp.Register.thterm sem interp *)
-
-let default_value = true
-
-(* let () =
- * Interp.Register.model ty (fun d n ->
- * let v = is d n in
- * let v = Colibri2_popop_lib.Opt.get_def default_value v in
- * let v = if v then values_true else values_false in
- * v) *)
-
-
-
--
GitLab