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

[Bool] it is LRA that should decide on its literals if fourier needs it

parent 28f1ab26
No related branches found
No related tags found
1 merge request!7One delayed by environment
...@@ -259,7 +259,8 @@ let converter d (f:Ground.t) = ...@@ -259,7 +259,8 @@ let converter d (f:Ground.t) =
IArray.iter ~f:attach args; IArray.iter ~f:attach args;
Egraph.attach_value d (Ground.node f) Boolean.dom Daemon.key (); Egraph.attach_value d (Ground.node f) Boolean.dom Daemon.key ();
Datastructure.Push.push comparisons d f; 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 = let init env =
......
...@@ -323,9 +323,6 @@ let converter d (f:Ground.t) = ...@@ -323,9 +323,6 @@ let converter d (f:Ground.t) =
| { app = {builtin = Expr.False}; tyargs = []; args; _ } -> | { app = {builtin = Expr.False}; tyargs = []; args; _ } ->
assert ( IArray.is_empty args); assert ( IArray.is_empty args);
reg _false reg _false
| { ty; _ }
when Ground.Ty.equal ty Ground.Ty.bool ->
Egraph.register_decision d (chobool res)
| _ -> () | _ -> ()
......
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