Skip to content
Snippets Groups Projects
Commit 926a0c24 authored by François Bobot's avatar François Bobot
Browse files

[Boolean] Some cleanup

parent 6a72a13c
No related branches found
No related tags found
1 merge request!13Improve doc, a simplify daemons
......@@ -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) *)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment