From c5d3d6b7f33c63777d5ea260c28a7f4d46878ed7 Mon Sep 17 00:00:00 2001
From: Quentin Petitjean <petitjean.quentin.54@gmail.com>
Date: Tue, 15 Jun 2021 03:56:04 +0200
Subject: [PATCH] Modifying some blob functions
---
src_colibri2/solver/scheduler.ml | 2 +-
src_colibri2/theories/bool/boolean.ml | 5 ++++-
src_colibri2/theories/bool/equality.ml | 8 ++++----
3 files changed, 9 insertions(+), 6 deletions(-)
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 529da7728..160a046e0 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -239,7 +239,7 @@ let run_one_step_propagation_l t =
let module Dem = (val Egraph.Wait.get_dem key) in
if Ground.Learn.is_uninitialized key then begin
let blob = Ground.Learn.get key in
- if (LearnSet.mem (blob key Dem.t) (t.learn_set)) then
+ if (LearnSet.mem (blob key runable) (t.learn_set)) then
true
else begin
let d = Egraph.Backtrackable.get_delayed t.solver_state in
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index c7d2fcadb..b9a15de66 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -152,6 +152,8 @@ module TwoWatchLiteral = struct
let delay = Events.Delayed_by 1
+ let blob _ e = e.ground
+
type res_scan =
| LimitReached
| Absorbent
@@ -269,7 +271,8 @@ module TwoWatchLiteral = struct
attach (d :> Egraph.Ro.t) r from_end
end
- let () = Egraph.Wait.register_dem (module Daemon)
+ let () = Egraph.Wait.register_dem (module Daemon);
+ Ground.Learn.set Daemon.key Daemon.blob
let create = Daemon.create
end
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index ed1d8397a..1cf221de6 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -336,7 +336,7 @@ module DaemonPropa = struct
let delay = Events.Delayed_by 1
let wakeup d v _ev () =
norm_dom d (ThE.index v)
- let blob _ _ _ = None
+ let blob _ _ _ = Some "Equality.DaemonPropa : "
end
module RDaemonPropa = Demon.Key.Register(DaemonPropa)
@@ -379,7 +379,7 @@ module DaemonInit = struct
| _ -> raise UnwaitedEvent
) ev;
Demon.AliveReattached
- let blob _ _ _ = None
+ let blob _ _ _ = Some "Equality.DaemonInit : "
end
module RDaemonInit = Demon.Key.Register(DaemonInit)
@@ -434,7 +434,7 @@ module DaemonPropaITE = struct
| Some b -> simplify d clsem b
end
| _ -> raise UnwaitedEvent
- let blob _ _ = None
+ let blob _ _ = Some "ITE.propa : "
end
@@ -468,7 +468,7 @@ module DaemonInitITE = struct
Demon.Fast.attach d DaemonPropaITE.key events
end
| _ -> raise UnwaitedEvent
- let blob _ _ = None
+ let blob _ _ = Some "ITE.init : "
end
module RDaemonInitITE = Demon.Fast.Register(DaemonInitITE)
--
GitLab