From 8f4e35488c07140619513b91c38ad364abc182bc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 12 Mar 2021 09:55:31 +0100
Subject: [PATCH] Add a generic part of the model computation
---
.gitignore | 3 -
colibri2.opam | 2 +-
colibrics.opam | 2 +-
dune-project | 2 +-
src_colibri2/core/.ocamlformat | 0
src_colibri2/core/.ocamlformat-ignore | 24 +++
src_colibri2/core/datastructure.ml | 2 +
src_colibri2/core/datastructure.mli | 2 +
src_colibri2/core/demon.ml | 48 ++++-
src_colibri2/core/demon.mli | 14 +-
src_colibri2/core/egraph.ml | 189 ++++++++---------
src_colibri2/core/egraph.mli | 9 +-
src_colibri2/core/events.ml | 15 +-
src_colibri2/core/events.mli | 7 +-
src_colibri2/core/ground.mli | 2 +-
src_colibri2/core/interp.ml | 202 ++++++++++++++----
src_colibri2/core/interp.mli | 54 ++++-
src_colibri2/core/structures/nodes.ml | 16 +-
src_colibri2/core/structures/nodes.mli | 18 +-
src_colibri2/solver/scheduler.ml | 4 +
src_colibri2/stdlib/context.ml | 2 +
src_colibri2/stdlib/context.mli | 2 +
src_colibri2/stdlib/wto.ml | 236 ++++++++++++++++++++++
src_colibri2/stdlib/wto.mli | 64 ++++++
src_colibri2/theories/ADT/adt.ml | 11 +-
src_colibri2/theories/LRA/LRA.ml | 70 ++++---
src_colibri2/theories/LRA/dom_interval.ml | 4 +-
src_colibri2/theories/LRA/realValue.ml | 5 +-
src_colibri2/theories/bool/boolean.ml | 115 ++++++-----
src_colibri2/theories/bool/equality.ml | 121 +++++------
src_colibri2/theories/bool/equality.mli | 3 +-
31 files changed, 909 insertions(+), 339 deletions(-)
create mode 100644 src_colibri2/core/.ocamlformat
create mode 100644 src_colibri2/core/.ocamlformat-ignore
create mode 100644 src_colibri2/stdlib/wto.ml
create mode 100644 src_colibri2/stdlib/wto.mli
diff --git a/.gitignore b/.gitignore
index e3cddf25f..cf0682e64 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,9 +4,6 @@ _build/
# executable
*.exe
-# jbuild generated files
-*.merlin
-
# test result files
*.res
diff --git a/colibri2.opam b/colibri2.opam
index a58a31c1a..fb3eb7e18 100644
--- a/colibri2.opam
+++ b/colibri2.opam
@@ -20,7 +20,7 @@ depends: [
"dolmen_loop" {>= "0.5~dev"}
"cmdliner"
"gen"
- "dune" {>= "2.7"}
+ "dune" {>= "2.8"}
"zarith"
"ppx_deriving" {> "4.1.5"}
"ppx_optcomp"
diff --git a/colibrics.opam b/colibrics.opam
index 7cf296b71..09cd7ff21 100644
--- a/colibrics.opam
+++ b/colibrics.opam
@@ -7,7 +7,7 @@ depends: [
"dolmen" {>= "0.5~dev"}
"dolmen_type" {>= "0.5~dev"}
"dolmen_loop" {>= "0.5~dev"}
- "dune" {>= "2.7"}
+ "dune" {>= "2.8"}
"zarith"
"cmdliner"
"ocaml" {>= "4.08"}
diff --git a/dune-project b/dune-project
index b758b5f52..65842d36c 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.7)
+(lang dune 2.8)
(cram enable)
(generate_opam_files true)
diff --git a/src_colibri2/core/.ocamlformat b/src_colibri2/core/.ocamlformat
new file mode 100644
index 000000000..e69de29bb
diff --git a/src_colibri2/core/.ocamlformat-ignore b/src_colibri2/core/.ocamlformat-ignore
new file mode 100644
index 000000000..19b3d4c70
--- /dev/null
+++ b/src_colibri2/core/.ocamlformat-ignore
@@ -0,0 +1,24 @@
+env.ml
+events.ml
+theory.ml
+structures
+structures/nodes.mli
+structures/term.ml
+structures/domKind.ml
+structures/dune
+structures/domKind.mli
+structures/expr.ml
+structures/nodes.ml
+structures/.merlin
+datastructure.mli
+colibri2_core.ml
+demon.mli
+env.mli
+ground.mli
+dune
+datastructure.ml
+egraph.ml
+egraph.mli
+events.mli
+demon.ml
+ground.ml
diff --git a/src_colibri2/core/datastructure.ml b/src_colibri2/core/datastructure.ml
index 123535639..9731f2494 100644
--- a/src_colibri2/core/datastructure.ml
+++ b/src_colibri2/core/datastructure.ml
@@ -242,6 +242,8 @@ module Queue = struct
let fold ~f ~init t d =
Context.Queue.fold f init (Egraph.get_unsaved_env d t)
+ let length t d = Context.Queue.length (Egraph.get_unsaved_env d t)
+ let get t d i = Context.Queue.get (Egraph.get_unsaved_env d t) i
end
diff --git a/src_colibri2/core/datastructure.mli b/src_colibri2/core/datastructure.mli
index 89dd3b015..be6adf803 100644
--- a/src_colibri2/core/datastructure.mli
+++ b/src_colibri2/core/datastructure.mli
@@ -75,6 +75,8 @@ module Queue: sig
val push: 'a t -> Egraph.t -> 'a -> unit
val iter: f:('a -> unit) -> 'a t -> Egraph.t -> unit
val fold: f:('acc -> 'a -> 'acc) -> init:'acc -> 'a t -> Egraph.t -> 'acc
+ val length: 'a t -> Egraph.t -> int
+ val get: 'a t -> Egraph.t -> int -> 'a
end
diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml
index 587ce8593..b2358dda6 100644
--- a/src_colibri2/core/demon.ml
+++ b/src_colibri2/core/demon.ml
@@ -32,6 +32,7 @@ module Create = struct
| EventAnyDom : 'a DomKind.t * 'b -> 'b event
| EventValue : Node.t * 'a ValueKind.t * 'b -> 'b event
| EventAnyValue : Node.t * 'b -> 'b event
+ | EventRegAny : 'b -> 'b event
| EventRegCl : Node.t * 'b -> 'b event
| EventChange : Node.t * 'b -> 'b event
| EventChangeAny: 'b -> 'b event
@@ -50,6 +51,8 @@ module Create = struct
Format.fprintf fmt "any value of %a" Node.pp node
| EventRegCl (node, _) ->
Format.fprintf fmt "registration of %a" Node.pp node
+ | EventRegAny (_) ->
+ Format.fprintf fmt "any registration"
| EventChange (node, _) ->
Format.fprintf fmt "changeNode of %a" Node.pp node
| EventChangeAny (_) ->
@@ -230,7 +233,7 @@ module Key = struct
let open Events.Fired in
match event with
| EventDom (a, b , (k,d)) -> k, EventDom(a, b, d)
- | EventValue (a, b , c, (k,d)) -> k, EventValue(a, b, c, d)
+ | EventValue (a, c, (k,d)) -> k, EventValue(a, c, d)
| EventSem (a, b, c, (k,d)) -> k, EventSem(a, b, c, d)
| EventReg (a, (k,d)) -> k, EventReg(a, d)
| EventRegNode (a, (k,d)) -> k, EventRegNode(a, d)
@@ -298,6 +301,8 @@ module Key = struct
Egraph.attach_any_node t dem.dk_id (k,data)
| Create.EventRegCl (node,data) ->
Egraph.attach_reg_node t node dem.dk_id (k,data)
+ | Create.EventRegAny (data) ->
+ Egraph.attach_reg_any t dem.dk_id (k,data)
| Create.EventRegSem (sem,data) ->
Egraph.attach_reg_sem t sem dem.dk_id (k,data)
| Create.EventRegValue (value,data) ->
@@ -428,7 +433,7 @@ module Fast = struct
Debug.dprintf0 debug "[Demon] @[Done@]";
(match D.delay with
| Immediate -> ()
- | Delayed_by _ | LastEffort _ -> Egraph.flush_internal d);
+ | Delayed_by _ | LastEffort _ | FixingModel -> Egraph.flush_internal d);
run_one () in
try
run_one ();
@@ -500,6 +505,8 @@ module Fast = struct
Egraph.attach_any_value d node dem.dk_id data
| EventRegCl (node,data) ->
Egraph.attach_reg_node d node dem.dk_id data
+ | EventRegAny (data) ->
+ Egraph.attach_reg_any d dem.dk_id data
| EventChange (node,data) ->
Egraph.attach_node d node dem.dk_id data
| EventChangeAny (data) ->
@@ -582,6 +589,27 @@ module Fast = struct
RDaemonInit.init init_d;
attach init_d DaemonInit.key [Create.EventChangeAny(())]
+ let register_any_new_node_daemon
+ ~name
+ ?(delay=Events.Delayed_by 1)
+ ?(throttle=100)
+ (f:Egraph.t -> Node.t -> unit)
+ (init_d:Egraph.t)
+ =
+ let module DaemonInit = struct
+ let key = create name
+ module Data = Popop_stdlib.DUnit
+ let delay = delay
+ let throttle = throttle
+ let wakeup d = function
+ | Events.Fired.EventReg(node,()) ->
+ f d node
+ | _ -> raise UnwaitedEvent
+ end in
+ let module RDaemonInit = Register(DaemonInit) in
+ RDaemonInit.init init_d;
+ attach init_d DaemonInit.key [Create.EventRegAny(())]
+
let register_change_domain_daemon
(type a) (type b)
~name
@@ -657,16 +685,20 @@ module Fast = struct
let delay = delay
let throttle = throttle
let wakeup d = function
- | Events.Fired.EventValue(node,value,v,data) ->
- let v = ValueKind.Eq.coerce value Val.key v in
+ | Events.Fired.EventValue(node,value,data) ->
+ let v = Opt.get_exn Impossible (Value.value Val.key value) in
f d node v data
| _ -> raise UnwaitedEvent
end in
let module RDaemonInit = Register(DaemonInit) in
let attach d n data =
- match Egraph.get_value d Val.key n with
+ match Egraph.get_value d n with
| None -> attach d DaemonInit.key [Create.EventValue(n,Val.key,data)]
- | Some v -> f d n v data
+ | Some v ->
+ match Value.value Val.key v with
+ | None -> attach d DaemonInit.key [Create.EventValue(n,Val.key,data)]
+ | Some v ->
+ f d n v data
in
RDaemonInit.init, attach
@@ -691,7 +723,7 @@ module Fast = struct
let wakeup d = function
| Events.Fired.EventDom(node,_,f) ->
f d node
- | Events.Fired.EventValue(node,_,_,f) ->
+ | Events.Fired.EventValue(node,_,f) ->
f d node
| _ -> raise UnwaitedEvent
end in
@@ -704,7 +736,7 @@ module Fast = struct
in
let for_value d value n f =
attach d DaemonInit.key [Create.EventValue(n,value,f)];
- match Egraph.get_value d value n with
+ match Egraph.get_value d n with
| None -> ()
| Some _ -> f d n
in
diff --git a/src_colibri2/core/demon.mli b/src_colibri2/core/demon.mli
index 901e3b296..7c4dbde8b 100644
--- a/src_colibri2/core/demon.mli
+++ b/src_colibri2/core/demon.mli
@@ -31,7 +31,9 @@ module Create : sig
| EventValue : Node.t * 'a ValueKind.t * 'b -> 'b event
(** the values of the class is watched *)
| EventAnyValue : Node.t * 'b -> 'b event
- (** we want to register this class *)
+ (** Warn when any class registered *)
+ | EventRegAny : 'b -> 'b event
+ (** Warn when this class is registered *)
| EventRegCl : Node.t * 'b -> 'b event
(** Warn when the class is not the representant of its eq-class anymore *)
| EventChange : Node.t * 'b -> 'b event
@@ -161,6 +163,16 @@ module Fast: sig
unit
(** *)
+ (** helper *)
+ val register_any_new_node_daemon:
+ name:string ->
+ ?delay:Events.delay ->
+ ?throttle:int ->
+ (Egraph.t -> Node.t -> unit) ->
+ Egraph.t ->
+ unit
+ (** *)
+
(** helper *)
val register_change_domain_daemon:
name:string ->
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index ae0ac0652..505ac7314 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -50,12 +50,11 @@ module VDomTable = DomKind.MkVector (struct type ('a,'unused) t = 'a domtable en
module VSemTable = ThTermKind.Vector
-type 'a valuetable = {
- table : 'a Node.M.t;
- events : Events.Wait.t Bag.t Node.M.t;
- reg_events : Events.Wait.t list;
+type valuetable = {
+ values : Value.t Node.M.t;
+ events : Events.Wait.t Bag.t Node.M.t ValueKind.M.t;
+ reg_events : Events.Wait.t list ValueKind.M.t;
}
-module VValueTable = ValueKind.MkVector (struct type ('a,'unit) t = 'a valuetable end)
(** Environnement *)
@@ -73,7 +72,7 @@ module Def = struct
saved_event_any_reg : Events.Wait.t list;
saved_dom : delayed_t VDomTable.t;
saved_sem : semtable VSemTable.t;
- saved_value : unit VValueTable.t;
+ saved_value : valuetable;
saved_envs : Env.Saved.VectorH.t;
}
@@ -89,7 +88,7 @@ module Def = struct
(** extensible "number of fields" *)
dom : delayed_t VDomTable.t;
sem : semtable VSemTable.t;
- value : unit VValueTable.t;
+ mutable value : valuetable;
envs : Env.Saved.VectorH.t;
mutable current_delayed : delayed_t; (** For assert-check *)
unsaved_envs: Env.Unsaved.VectorH.t;
@@ -189,7 +188,7 @@ module Hidden = Context.Make(struct
saved_event_any_reg = t.event_any_reg;
saved_dom = VDomTable.copy t.dom;
saved_sem = VSemTable.copy t.sem;
- saved_value = VValueTable.copy t.value;
+ saved_value = t.value;
saved_envs = Env.Saved.VectorH.copy t.envs;
}
@@ -200,9 +199,9 @@ module Hidden = Context.Make(struct
t.event_value <- s.saved_event_value ;
t.event_reg <- s.saved_event_reg ;
t.event_any_reg <- s.saved_event_any_reg;
+ t.value <- s.saved_value;
VDomTable.move ~from:s.saved_dom ~to_:t.dom;
VSemTable.move ~from:s.saved_sem ~to_:t.sem;
- VValueTable.move ~from:s.saved_value ~to_:t.value;
Env.Saved.VectorH.move ~from:s.saved_envs ~to_:t.envs;
t.current_delayed <- dumb_delayed
@@ -222,13 +221,6 @@ let get_table_sem t k =
Nodes.check_thterm_registered k;
ThTermKind.Vector.get_def t.sem k []
-let get_table_value t k =
- Nodes.check_value_registered k;
- VValueTable.get_def t.value k
- { table = Node.M.empty;
- events = Node.M.empty;
- reg_events = [] }
-
exception UninitializedEnv of string
exception NotRegistered
@@ -265,12 +257,12 @@ module T = struct
let node = find_def t node in
get_direct_dom t dom node
- let get_direct_value t value node =
- Node.M.find_opt node (get_table_value t value).table
+ let get_direct_value t node =
+ Node.M.find_opt node t.value.values
- let get_value t value node =
+ let get_value t node =
let node = find_def t node in
- get_direct_value t value node
+ get_direct_value t node
let get_env : type a. t -> a Env.Saved.t -> a
= fun t k ->
@@ -339,11 +331,13 @@ let output_graph filename t =
DomKind.pp dom (escape_for_dot (VDom.print_dom dom) s);
with Not_found -> ()
in
- let iter_value value fmt (valuetable: _ valuetable) =
+ let print_value fmt valuetable =
try
- let s = Node.M.find node valuetable.table in
+ let s = Node.M.find node valuetable.values in
+ (match Value.kind s with
+ | Value.Value (kind, value) ->
Format.fprintf fmt "| {%a | %s}"
- ValueKind.pp value (escape_for_dot (print_value value) s);
+ ValueKind.pp kind (escape_for_dot (print_value kind) value))
with Not_found -> ()
in
let print_sem fmt node =
@@ -366,9 +360,7 @@ let output_graph filename t =
else Format.silent)
t.dom
(if is_repr t node
- then VValueTable.pp Format.silent Format.silent
- {VValueTable.printk=Format.silent}
- {VValueTable.printd=iter_value}
+ then print_value
else Format.silent)
t.value
@@ -435,9 +427,9 @@ module Delayed = struct
assert (is_current_env t);
get_dom t.env dom node
- let get_value t value node =
+ let get_value t node =
assert (is_current_env t);
- get_value t.env value node
+ get_value t.env node
let get_env t env =
assert (is_current_env t);
@@ -455,19 +447,26 @@ module Delayed = struct
assert (is_current_env t);
is_registered t.env node
- let set_value_direct (type a) t (value : a ValueKind.t) node0 new_v =
+ let set_value_direct t node0 new_v =
Debug.incr stats_set_value;
let node = find t node0 in
- let valuetable = get_table_value t.env value in
+ let valuetable = t.env.value in
let valuetable = {
valuetable with
- table = Node.M.add node new_v valuetable.table;
+ values = Node.M.add node new_v valuetable.values;
} in
- VValueTable.set t.env.value value valuetable;
- let events = Node.M.find_opt node valuetable.events in
- Wait.wakeup_events_bag Events.Wait.translate_value t events (node,value,new_v);
+ t.env.value <- valuetable;
+ (match Value.kind new_v with
+ | Value.Value(valuekind,_) ->
+ let events =
+ let open Option in
+ let* events = ValueKind.M.find_opt valuekind valuetable.events in
+ Node.M.find_opt node events
+ in
+ Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v)
+ );
let events = Node.M.find_opt node t.env.event_value in
- Wait.wakeup_events_bag Events.Wait.translate_value t events (node,value,new_v)
+ Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v)
let add_pending_merge (t : t) node node' =
Debug.dprintf4 debug "[Egraph] @[add_pending_merge for %a and %a@]"
@@ -515,13 +514,13 @@ module Delayed = struct
t (Some reg_events) (thterm)
end
| Only_for_solver.Value nodevalue ->
- begin match Only_for_solver.value_of_node nodevalue with
- | Only_for_solver.Value(value,v) ->
- let valuetable = get_table_value t.env value in
- let reg_events = valuetable.reg_events in
+ begin match Value.kind nodevalue with
+ | Value(value,_) ->
+ let valuetable = t.env.value in
+ let reg_events = ValueKind.M.find_opt value valuetable.reg_events in
Wait.wakeup_events_list Events.Wait.translate_regvalue
- t (Some reg_events) (nodevalue);
- set_value_direct t value node v
+ t reg_events (nodevalue);
+ set_value_direct t node nodevalue
end
end
@@ -545,9 +544,7 @@ module Delayed = struct
match Nodes.Only_for_solver.nodevalue node0' with
| None -> ()
| Some value ->
- match Nodes.Only_for_solver.value_of_node value with
- | Nodes.Only_for_solver.Value(value,v) ->
- set_value_direct t value node0 v
+ set_value_direct t node0 value
end
(** node' is already registered *)
else if Node.equal node (find t node0') then
@@ -662,32 +659,28 @@ module Delayed = struct
let merge_values t node0 node0' =
let node = find t node0 in
let node' = find t node0' in
- let iteri (type a) (value:a ValueKind.t) (valuetable:a valuetable) =
- let old_s = Node.M.find_opt node valuetable.table in
- let old_s' = Node.M.find_opt node' valuetable.table in
- let (module V) = Nodes.get_value value in
- Debug.dprintf14 debug
- "[Egraph] @[merge value %a (%a(%a),%a)@ and (%a(%a),%a)@]"
- ValueKind.pp value
- Node.pp node Node.pp node0
- (Format.opt (print_value value)) old_s
- Node.pp node' Node.pp node0'
- (Format.opt (print_value value)) old_s';
- match old_s, old_s' with
- | None, None -> ()
- | Some v, None ->
- set_value_direct t value node0' v
- | None, Some v' ->
- set_value_direct t value node0 v'
- | Some v, Some v' ->
- if V.equal v v'
- then
- (* already same value. Does that really happen? *)
- ()
- else
- raise Contradiction
- in
- VValueTable.iter_initializedi {VValueTable.iteri} t.env.value
+ let valuetable = t.env.value in
+ let old_s = Node.M.find_opt node valuetable.values in
+ let old_s' = Node.M.find_opt node' valuetable.values in
+ Debug.dprintf12 debug
+ "[Egraph] @[merge value (%a(%a),%a)@ and (%a(%a),%a)@]"
+ Node.pp node Node.pp node0
+ (Format.opt Value.pp) old_s
+ Node.pp node' Node.pp node0'
+ (Format.opt Value.pp) old_s';
+ match old_s, old_s' with
+ | None, None -> ()
+ | Some v, None ->
+ set_value_direct t node0' v
+ | None, Some v' ->
+ set_value_direct t node0 v'
+ | Some v, Some v' ->
+ if Value.equal v v'
+ then
+ (* already same value. Does that really happen? *)
+ ()
+ else
+ raise Contradiction
let finalize_merge t node1_0 node2_0 inv =
let node1 = find t node1_0 in
@@ -726,17 +719,16 @@ module Delayed = struct
VDomTable.iter_initializedi {VDomTable.iteri} t.env.dom;
(** move value events *)
- let iteri (type a) (value : a ValueKind.t) (valuetable: a valuetable) =
- match Node.M.find_opt other_node valuetable.events with
- | None -> ()
+ let mapi _ events =
+ match Node.M.find_opt other_node events with
+ | None -> events
| Some other_events ->
- let new_events =
- Node.M.add_change (fun x -> x) Bag.concat repr_node other_events
- valuetable.events in
- let valuetable = { valuetable with events = new_events } in
- VValueTable.set t.env.value value valuetable
+ Node.M.add_change (fun x -> x) Bag.concat repr_node other_events
+ events
in
- VValueTable.iter_initializedi {VValueTable.iteri} t.env.value;
+ t.env.value <- { t.env.value with events =
+ ValueKind.M.mapi {mapi} t.env.value.events
+ };
(** wakeup the daemons *)
Wait.wakeup_events_bag
@@ -931,12 +923,16 @@ module Delayed = struct
let attach_value (type a) t node (value : a ValueKind.t) dem event =
let node = find_def t node in
let event = Events.Wait.Event (dem,event) in
- let valuetable = (get_table_value t.env value) in
+ let valuetable = t.env.value in
let valuetable = {
valuetable with
- events = Node.M.add_change Bag.elt Bag.add node event valuetable.events
+ events =
+ ValueKind.M.add_change
+ (fun event -> Node.M.singleton node (Bag.elt event))
+ (Node.M.add_change Bag.elt Bag.add node)
+ value event valuetable.events
} in
- VValueTable.set t.env.value value valuetable
+ t.env.value <- valuetable
let attach_node t node dem event =
let node = find_def t node in
@@ -961,6 +957,15 @@ module Delayed = struct
t.env.event_reg <-
Node.M.add_change Lists.singleton Lists.add node event t.env.event_reg
+ let attach_reg_any t dem event =
+ let event = Events.Wait.Event (dem,event) in
+ (* todo already registered ? *)
+ (* match find t node with
+ * | node -> (\** already registered *\)
+ * Wait.wakeup_events_list Events.Wait.translate_regnode t (Some [event]) node
+ * | exception NotRegistered -> *)
+ t.env.event_any_reg <- event::t.env.event_any_reg
+
let attach_reg_sem (type a) t (sem : a ThTermKind.t) dem event =
let event = Events.Wait.Event (dem,event) in
let reg_events = get_table_sem t.env sem in
@@ -969,9 +974,11 @@ module Delayed = struct
let attach_reg_value (type a) t (value : a ValueKind.t) dem event =
let event = Events.Wait.Event (dem,event) in
- let value_table = get_table_value t.env value in
- let reg_events = event::value_table.reg_events in
- VValueTable.set t.env.value value {value_table with reg_events}
+ let value_table = t.env.value in
+ let reg_events = event::(ValueKind.M.find_def [] value value_table.reg_events) in
+ t.env.value <-
+ {value_table with reg_events =
+ ValueKind.M.add value reg_events value_table.reg_events}
let attach_any_dom (type a) t (dom : a DomKind.t) dem event =
let event = Events.Wait.Event (dem,event) in
@@ -1024,7 +1031,10 @@ module Backtrackable = struct
event_any_reg = [];
dom = VDomTable.create 5;
sem = VSemTable.create 5;
- value = VValueTable.create 5;
+ value = { reg_events = ValueKind.M.empty;
+ values = Node.M.empty;
+ events = ValueKind.M.empty;
+ };
envs = Env.Saved.VectorH.create 5;
unsaved_envs = Env.Unsaved.VectorH.create 5;
current_delayed = dumb_delayed;
@@ -1101,10 +1111,10 @@ module Backtrackable = struct
let t = Hidden.rw t in
T.get_dom t dom node
- let get_value t value node =
+ let get_value t node =
let t = Hidden.rw t in
assert (check_disabled_delayed t);
- T.get_value t value node
+ T.get_value t node
let get_env t env =
let t = Hidden.rw t in
@@ -1150,8 +1160,7 @@ module type Getter = sig
val find_def : t -> Node.t -> Node.t
val get_dom : t -> 'a DomKind.t -> Node.t -> 'a option
(** dom of the nodeass *)
- val get_value : t -> 'a ValueKind.t -> Node.t -> 'a option
- (** value of the nodeass *)
+ val get_value : t -> Node.t -> Value.t option
(** {4 The nodeasses must have been marked has registered} *)
diff --git a/src_colibri2/core/egraph.mli b/src_colibri2/core/egraph.mli
index 71f6418a0..a964f1b73 100644
--- a/src_colibri2/core/egraph.mli
+++ b/src_colibri2/core/egraph.mli
@@ -38,9 +38,9 @@ module type Getter = sig
val is_equal : t -> Node.t -> Node.t -> bool
val find_def : t -> Node.t -> Node.t
val get_dom : t -> 'a DomKind.t -> Node.t -> 'a option
- (** dom of the class *)
- val get_value : t -> 'a ValueKind.t -> Node.t -> 'a option
- (** value of the class *)
+ (** dom of the class *)
+ val get_value : t -> Node.t -> Value.t option
+ (** one of the value of the class *)
(** {4 The classes must have been registered} *)
@@ -50,6 +50,7 @@ module type Getter = sig
val is_registered : t -> Node.t -> bool
val get_env : t -> 'a Env.Saved.t -> 'a
+ (** Can raise UninitializedEnv *)
val set_env : t -> 'a Env.Saved.t -> 'a -> unit
val get_unsaved_env : t -> 'a Env.Unsaved.t -> 'a
@@ -103,6 +104,8 @@ val attach_value: t -> Node.t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> '
(** wakeup when a value is attached to this equivalence class *)
val attach_any_value: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
(** wakeup when any kind of value is attached to this equivalence class *)
+val attach_reg_any: t -> ('event,'r) Events.Dem.t -> 'event -> unit
+(** wakeup when any node is registered *)
val attach_reg_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
(** wakeup when this node is registered *)
val attach_reg_sem: t -> 'a ThTermKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml
index 6c67f5657..d6182f65a 100644
--- a/src_colibri2/core/events.ml
+++ b/src_colibri2/core/events.ml
@@ -52,7 +52,7 @@ module Fired = struct
(** the domain dom of the class change *)
| EventDom : Node.t * 'a DomKind.t * 'b -> 'b event
(** the value of the class has been set *)
- | EventValue : Node.t * 'a ValueKind.t * 'a * 'b -> 'b event
+ | EventValue : Node.t * Value.t * 'b -> 'b event
(** a new theory term 'a point to this class (not complete) *)
| EventSem : Node.t * 'a ThTermKind.t * 'a * 'b -> 'b event
(** we want to register a class *)
@@ -69,8 +69,8 @@ module Fired = struct
let pp fmt = function
| EventDom (node, dom, _) ->
Format.fprintf fmt "dom:%a of %a" DomKind.pp dom Node.pp node
- | EventValue (node, value, _, _) ->
- Format.fprintf fmt "value:%a of %a" ValueKind.pp value Node.pp node
+ | EventValue (node, value, _) ->
+ Format.fprintf fmt "value:%a of %a" Value.pp value Node.pp node
| EventSem (node, sem, v, _) ->
Format.fprintf fmt "sem:%a of %a with %a"
ThTermKind.pp sem Node.pp node (print_thterm sem) v
@@ -89,15 +89,15 @@ module Fired = struct
end
| EventRegValue (nodevalue, _) ->
let node = Only_for_solver.node_of_nodevalue nodevalue in
- begin match Only_for_solver.value_of_node nodevalue with
- | Only_for_solver.Value(value,v) ->
+ begin match Value.kind nodevalue with
+ | Value(value,v) ->
Format.fprintf fmt "registration of value:%a of %a with %a"
ValueKind.pp value Node.pp node (print_value value) v
end
let get_data = function
| EventDom (_, _ , d) -> d
- | EventValue (_, _ , _, d) -> d
+ | EventValue (_, _ , d) -> d
| EventSem (_, _, _, d) -> d
| EventReg (_, d) -> d
| EventRegNode (_, d) -> d
@@ -112,6 +112,7 @@ type delay =
| Immediate
| Delayed_by of int
| LastEffort of int
+ | FixingModel
module Wait = struct
type t =
@@ -140,7 +141,7 @@ module Wait = struct
let translate_dom =
{translate = fun (node,dom) data -> EventDom(node,dom,data)}
let translate_value =
- {translate = fun (node,value,v) data -> EventValue(node,value,v,data)}
+ {translate = fun (node,value) data -> EventValue(node,value,data)}
let translate_sem =
{translate = fun (node,sem,s) data -> EventSem(node,sem,s,data)}
let translate_reg =
diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli
index dc5415241..5bd66017a 100644
--- a/src_colibri2/core/events.mli
+++ b/src_colibri2/core/events.mli
@@ -26,7 +26,7 @@ module Fired : sig
(** the domain dom of the class change *)
| EventDom : Node.t * 'a DomKind.t * 'b -> 'b event
(** the value of the node has been set *)
- | EventValue : Node.t * 'a ValueKind.t * 'a * 'b -> 'b event
+ | EventValue : Node.t * Value.t * 'b -> 'b event
(** a new semantical term 'a point to this class (not complete) *)
| EventSem : Node.t * 'a ThTermKind.t * 'a * 'b -> 'b event
(** we want to register a class *)
@@ -54,7 +54,8 @@ type delay =
| Delayed_by of int
(** Must be strictly positive *)
| LastEffort of int
- (** When no decisions remains, must be strictly positive *)
+ (** Should try to ensure that a model exists, must be strictly positive *)
+ | FixingModel
module Wait : sig
type t =
@@ -75,7 +76,7 @@ module Wait : sig
type 'a translate = { translate : 'd. 'a -> 'd -> 'd Fired.event}
val translate_dom : (Node.t * 'a DomKind.t) translate
- val translate_value : (Node.t * 'a ValueKind.t * 'a) translate
+ val translate_value : (Node.t * Value.t) translate
val translate_reg : Node.t translate
val translate_regnode : Node.t translate
val translate_change : Node.t translate
diff --git a/src_colibri2/core/ground.mli b/src_colibri2/core/ground.mli
index 8badd2227..4f9d94f0d 100644
--- a/src_colibri2/core/ground.mli
+++ b/src_colibri2/core/ground.mli
@@ -92,7 +92,7 @@ val init: Egraph.t -> unit
val register_converter:
Egraph.t -> (Egraph.t -> t -> unit) -> unit
-(** register converters between syntactic terms *)
+(** register callback called for each new ground term registered *)
module Defs : sig
val add:
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index 7c8ee2713..7b0fd0764 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -18,55 +18,171 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
+open Base
open Colibri2_popop_lib
+type env =
+ | Before (** fixing model *)
+ | During of { limitreached : bool ref; limit : int; nextnode : int }
+[@@deriving show]
+
+module Data = struct
+ let ground = Datastructure.Queue.create Fmt.nop "Interp.ground"
+
+ let check = Datastructure.Queue.create Fmt.nop "Interp.check"
+
+ let node = Datastructure.Queue.create Fmt.nop "Interp.node"
+
+ let ty = Datastructure.Queue.create Fmt.nop "Interp.ty"
+
+ let reg_ground = Datastructure.Queue.create Fmt.nop "Interp.reg_ground"
+
+ let reg_node = Datastructure.Queue.create Fmt.nop "Interp.reg_node"
+
+ let env =
+ Env.Saved.create_key
+ (module struct
+ type t = env
+
+ let name = "Interp.name"
+ end)
+
+ let () = Env.Saved.register pp_env env
+end
+
+module SeqLim = struct
+ type 'a t = 'a Sequence.t
+
+ let of_seq d s =
+ match Egraph.get_env d Data.env with
+ | Before -> s
+ | During d ->
+ Sequence.unfold_with s ~init:0 ~f:(fun i x ->
+ if i <= d.limit then Sequence.Step.Yield (x, i + 1)
+ else (
+ d.limitreached := true;
+ Sequence.Step.Done))
+
+ let ( let+ ) = Sequence.( >>| )
+
+ let ( let* ) t f = Sequence.bind t ~f
+
+ let ( and* ) = Sequence.cartesian_product
+end
+
module Register = struct
- type interp_term = Expr.Term.t -> Nodes.Value.t
- let ids : (interp_term -> Expr.Term.t -> Nodes.Value.t option) list ref = ref []
- let id f = ids := f::!ids
+ open Data
+
+ let check d f = Datastructure.Queue.push check d f
+
+ let node d f = Datastructure.Queue.push node d f
+
+ let ty d f = Datastructure.Queue.push ty d f
+end
+
+let get_registered (type a) exn db d x =
+ let exception Found of a in
+ match
+ Datastructure.Queue.iter
+ ~f:(fun f -> Option.iter (f d x) ~f:(fun s -> raise (Found s)))
+ db d
+ with
+ | exception Found s -> s
+ | () -> exn x
+ [@@inline always]
+
+exception CantInterpretTy of Ground.Ty.t
+
+let ty d ty = get_registered (fun ty -> raise (CantInterpretTy ty)) Data.ty d ty
+
+exception CantInterpretNode of Nodes.Node.t
+
+let node d n =
+ get_registered (fun n -> raise (CantInterpretNode n)) Data.node d n
+
+exception CantCheckGround of Ground.t
+
+let ground d n =
+ get_registered (fun n -> raise (CantCheckGround n)) Data.ground d n
+
+let check_ground_terms d =
+ Datastructure.Queue.iter Data.reg_ground d ~f:(fun g ->
+ if not (ground d g) then Egraph.contradiction d)
+
+(* module WTO = Colibri2_stdlib.Wto.Make (Ground) *)
- module ThInterp = Nodes.ThTermKind.MkVector(struct
- type ('a,_) t = (interp:(Nodes.Node.t -> Nodes.Value.t) -> 'a -> Nodes.Value.t)
- end)
+(* let compute_wto d =
+ * let g = Nodes.Node.H.create 100 in *)
- let thterms = ThInterp.create 10
- let thterm sem f =
- if not (ThInterp.is_uninitialized thterms sem)
- then invalid_arg (Format.asprintf "Interpretation for semantic value %a already done" Nodes.ThTermKind.pp sem);
- ThInterp.set thterms sem f
+let init d =
+ Egraph.set_env d Data.env Before;
+ Demon.Fast.register_any_new_node_daemon ~name:"Interp.new_node"
+ (fun d g -> Datastructure.Queue.push Data.reg_node d g)
+ d;
+ Ground.register_converter d (fun d g ->
+ Datastructure.Queue.push Data.reg_ground d g)
- let models = Expr.Ty.H.create 16
- let model ty (f:Egraph.t -> Nodes.Node.t -> Nodes.Value.t) =
- Expr.Ty.H.add models ty f
+module Fix_model = struct
+ let init d =
+ let env =
+ During
+ {
+ limitreached =
+ (* true because we want to continue (i.e start) *)
+ ref true;
+ nextnode = Datastructure.Queue.length Data.reg_node d - 1;
+ limit = 1;
+ }
+ in
+ Egraph.set_env d Data.env env
+ let next_dec d =
+ match Egraph.get_env d Data.env with
+ | Before ->
+ (* The first branching is about the limit *)
+ init d;
+ Sequence.unfold ~init:(1, d) ~f:(fun (i, d) ->
+ match Egraph.get_env d Data.env with
+ | Before -> assert false
+ | During r ->
+ if !(r.limitreached) then
+ let limit = i * 2 in
+ let dec d =
+ match Egraph.get_env d Data.env with
+ | Before -> assert false
+ | During r ->
+ Egraph.set_env d Data.env (During { r with limit })
+ in
+ Some (dec, (limit, d))
+ else None)
+ | During r ->
+ let rec aux nextnode =
+ if nextnode < 0 then (
+ check_ground_terms d;
+ Egraph.set_env d Data.env Before;
+ Sequence.empty)
+ else
+ (* The others are about the values *)
+ let n = Datastructure.Queue.get Data.reg_node d r.nextnode in
+ match Egraph.get_value d n with
+ | Some _ -> aux (nextnode - 1)
+ | None ->
+ let seq = node d n in
+ Sequence.map seq ~f:(fun v d ->
+ Egraph.set_env d Data.env
+ (During { r with nextnode = nextnode - 1 });
+ Egraph.set_value d n v)
+ in
+ aux r.nextnode
end
-exception CantInterpretTerm of Expr.Term.t
-
-type leaf = Expr.Term.t -> Nodes.Value.t option
-
-let term ?(leaf=(fun _ -> None)) t =
- let rec interp regl t =
- let rec aux t = function
- | [] -> raise (CantInterpretTerm t)
- | a::l ->
- match a (interp regl) t with
- | Some v -> v
- | None -> aux t l
- in
- aux t regl
- in
- interp ((fun _ -> leaf)::!Register.ids) t
-
-(* let model d n =
- * match Ty.H.find_opt Register.models (Nodes.Node.ty n) with
- * | None -> invalid_arg "Uninterpreted type"
- * | Some f -> f d n *)
-
-let () = Exn_printer.register (fun fmt exn ->
- match exn with
- | CantInterpretTerm t ->
- Format.fprintf fmt "Can't interpret the term %a."
- Expr.Term.pp t
- | exn -> raise exn
- )
+let () =
+ Exn_printer.register (fun fmt exn ->
+ match exn with
+ | CantInterpretNode t ->
+ Fmt.pf fmt "Can't interpret the node %a." Nodes.Node.pp t
+ | CantCheckGround t ->
+ Fmt.pf fmt "Can't check ground term %a." Ground.pp t
+ | CantInterpretTy t ->
+ Fmt.pf fmt "Can't interpret the type %a." Ground.Ty.pp t
+ | exn -> raise exn)
diff --git a/src_colibri2/core/interp.mli b/src_colibri2/core/interp.mli
index da52e484b..e2df2c8e1 100644
--- a/src_colibri2/core/interp.mli
+++ b/src_colibri2/core/interp.mli
@@ -18,18 +18,58 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
+open Base
-module Register: sig
- val id: ((Expr.Term.t -> Nodes.Value.t) -> (Expr.Term.t -> Nodes.Value.t option)) -> unit
+module SeqLim : sig
+ type 'a t
+ (** Sequence, finite during module fixing *)
- val thterm: 'a Nodes.ThTermKind.t -> (interp:(Nodes.Node.t -> Nodes.Value.t) -> 'a -> Nodes.Value.t) -> unit
+ val of_seq : Egraph.t -> 'a Sequence.t -> 'a t
+ (** Limit the sequence to the given bound of the iterative deepening.
+ Sequence used for enumerating the values should be limited for ensuring
+ fairness. If the sequence contained more elements than limited the top
+ decision will restart with a bigger limit
+ *)
- (* val model: Ty.t -> (Egraph.t -> Nodes.Node.t -> Nodes.Value.t) -> unit *)
+ val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+ val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
+ (** cartesian product {!Base.Sequence.cartesian_product} *)
+
+ val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
end
-type leaf = Expr.Term.t -> Nodes.Value.t option
+module Register : sig
+ val check : Egraph.t -> (Egraph.t -> Ground.t -> bool option) -> unit
+ (** Check the value of the arguments corresponds to the the one of the of the term *)
+
+ val node :
+ Egraph.t ->
+ (Egraph.t -> Nodes.Node.t -> Nodes.Value.t SeqLim.t option) ->
+ unit
+ (** Register the computation of possible values for a node using the
+ information on the domains *)
+
+ val ty :
+ Egraph.t ->
+ (Egraph.t -> Ground.Ty.t -> Nodes.Value.t SeqLim.t option) ->
+ unit
+ (** Register iterators on all the possible value of some types, all the values
+ must be reached eventually *)
+end
-val term : ?leaf:leaf -> Expr.Term.t -> Nodes.Value.t
+val ty : Egraph.t -> Ground.Ty.t -> Nodes.Value.t SeqLim.t
+(** Iterate on all the possible value of the given type, usually all the values
+ will be reached eventually *)
-(* val model : Egraph.t -> Nodes.Node.t -> Nodes.Value.t *)
+val init : Egraph.t -> unit
+(** Initialize the module for later use *)
+
+module Fix_model : sig
+ (** The model is search using iterative deepening depth-first search for
+ ensuring optimality even in presence of infinite choice *)
+
+ val next_dec : Egraph.t -> (Egraph.t -> unit) Sequence.t
+ (** Add a level of decision for fixing the model, another level could be
+ needed. Could raise unsatisfiable if all the model have been tried *)
+end
diff --git a/src_colibri2/core/structures/nodes.ml b/src_colibri2/core/structures/nodes.ml
index ad82ca99c..7c455376f 100644
--- a/src_colibri2/core/structures/nodes.ml
+++ b/src_colibri2/core/structures/nodes.ml
@@ -261,11 +261,11 @@ module Value = struct
| Poly.Neq -> None
| Poly.Eq -> Some v
- let semantic_equal (x:t) (y:t) : [ `Uncomparable | `Equal | `Disequal ] =
- match x, y with
- | Node.Value(_,xk,_), Node.Value(_,yk,_) when not (ValueKind.equal xk yk) ->
- `Uncomparable
- | _ -> if equal x y then `Equal else `Disequal
+ type kind =
+ | Value: 'a ValueKind.t * 'a -> kind
+
+ let kind: t -> kind = function
+ | Node.Value (_,value,v) -> Value(value,v)
end
@@ -403,16 +403,10 @@ module Only_for_solver = struct
let sem_of_node: ThTerm.t -> sem_of_node = function
| Node.ThTerm (_,sem,v) -> ThTerm(sem,v)
- type value_of_node =
- | Value: 'a ValueKind.t * 'a -> value_of_node
-
let nodevalue: Node.t -> Value.t option = function
| Node.All Node.ThTerm _ -> None
| Node.All (Node.Value _ as x) -> Some x
- let value_of_node: Value.t -> value_of_node = function
- | Node.Value (_,value,v) -> Value(value,v)
-
let node_of_thterm : ThTerm.t -> Node.t = ThTerm.node
let node_of_nodevalue : Value.t -> Node.t = Value.node
diff --git a/src_colibri2/core/structures/nodes.mli b/src_colibri2/core/structures/nodes.mli
index 45ca30607..6ab60caa3 100644
--- a/src_colibri2/core/structures/nodes.mli
+++ b/src_colibri2/core/structures/nodes.mli
@@ -140,8 +140,13 @@ module Value: sig
val value: 'a ValueKind.t -> t -> 'a option
- val semantic_equal: t -> t -> [ `Uncomparable | `Equal | `Disequal ]
- (** Test semantic equality of comparable value (same value kind) *)
+ type kind =
+ | Value: 'a ValueKind.t * 'a -> kind
+
+ val kind: t -> kind
+ (** give the value associated with a node, make sense only for not merged
+ class. So only the module solver can use it *)
+
end
(** {3 For building a particular value} *)
@@ -179,6 +184,7 @@ val get_registered_value: 'a ValueKind.t -> (module RegisteredValue with type s
val check_initialization: unit -> bool
(** Check if the initialization of all the sem and value have been done *)
+
(** {2 Only for the solver } *)
module Only_for_solver: sig
type sem_of_node =
@@ -194,19 +200,11 @@ module Only_for_solver: sig
(** give the sem associated with a node, make sense only for not merged
class. So only the module solver can use it *)
- type value_of_node =
- | Value: 'a ValueKind.t * 'a -> value_of_node
-
val nodevalue:
Node.t -> Value.t option
(** give the value associated with a node, make sense only for not merged
class. So only the module solver can use it *)
- val value_of_node:
- Value.t -> value_of_node
- (** give the value associated with a node, make sense only for not merged
- class. So only the module solver can use it *)
-
val node_of_thterm: ThTerm.t -> Node.t
val node_of_nodevalue: Value.t -> Node.t
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 756617357..572aadd85 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -80,6 +80,7 @@ type t =
{ mutable choices : Prio.t;
daemons : Events.Wait.daemon_key Context.TimeWheel.t;
lasteffort : Events.Wait.daemon_key Context.TimeWheel.t;
+ mutable fixing_model : Events.Wait.daemon_key list;
mutable prev_scheduler_state : bp option;
solver_state : Egraph.Backtrackable.t;
mutable delayed : Egraph.t option;
@@ -115,6 +116,7 @@ let new_solver () =
{ choices = Prio.empty;
daemons = Context.TimeWheel.create (Context.creator context);
lasteffort = Context.TimeWheel.create (Context.creator context);
+ fixing_model = [];
prev_scheduler_state = None;
solver_state = Egraph.Backtrackable.new_t (Context.creator context);
context;
@@ -169,6 +171,8 @@ let new_delayed =
| Delayed_by offset -> Context.TimeWheel.add t.daemons att offset
| LastEffort offset ->
Context.TimeWheel.add t.lasteffort att offset
+ | FixingModel ->
+ t.fixing_model <- att :: t.fixing_model
in
let sched_decision dec =
incr dec_count;
diff --git a/src_colibri2/stdlib/context.ml b/src_colibri2/stdlib/context.ml
index c93ee2f71..8e2bfdf0c 100644
--- a/src_colibri2/stdlib/context.ml
+++ b/src_colibri2/stdlib/context.ml
@@ -324,6 +324,8 @@ module Queue = struct
let push t v = save t; Vector.push t.v v
let iter f t = refresh t; Vector.iter f t.v
let fold f acc t = refresh t; Vector.fold f acc t.v
+ let length t = refresh t; Vector.length t.v
+ let get t i = refresh t; Vector.get t.v i
let pp ?sep pp fmt v = Vector.pp ?pp_sep:sep pp fmt v.v
end
diff --git a/src_colibri2/stdlib/context.mli b/src_colibri2/stdlib/context.mli
index 40bf9a974..17b6ca326 100644
--- a/src_colibri2/stdlib/context.mli
+++ b/src_colibri2/stdlib/context.mli
@@ -176,6 +176,8 @@ module Queue: sig
val push: 'a t -> 'a -> unit
val iter: ('a -> unit) -> 'a t -> unit
val fold: ('acc -> 'a -> 'acc) -> 'acc -> 'a t -> 'acc
+ val length: 'a t -> int
+ val get: 'a t -> int -> 'a
val pp: ?sep:unit Fmt.t -> 'a Fmt.t -> 'a t Fmt.t
end
diff --git a/src_colibri2/stdlib/wto.ml b/src_colibri2/stdlib/wto.ml
new file mode 100644
index 000000000..defb3ba99
--- /dev/null
+++ b/src_colibri2/stdlib/wto.ml
@@ -0,0 +1,236 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Each component of the graph is either an individual node of the graph
+ (without) self loop, or a strongly connected component where a node is
+ designed as the head of the component and the remaining nodes are given
+ by a list of components topologically ordered. *)
+type 'n component =
+ | Component of 'n * 'n partition
+ (** A strongly connected component, described by its head node and the
+ remaining sub-components topologically ordered *)
+ | Node of 'n
+ (** A single node without self loop *)
+
+(** A list of strongly connected components, sorted topologically *)
+and 'n partition = 'n component list
+
+
+let rec pp_partition pp_node fmt part =
+ List.iter (fun x -> Format.fprintf fmt "@ %a" (pp_component pp_node) x) part
+and pp_component pp_node fmt : 'a component -> unit = function
+ | Node n -> pp_node fmt n
+ | Component(head,part) ->
+ Format.fprintf fmt "@[<hov 1>(%a%a)@]"
+ pp_node head (pp_partition pp_node) part
+
+let fold_heads f acc l =
+ let rec partition acc l =
+ List.fold_left component acc l
+ and component acc = function
+ | Node _ -> acc
+ | Component (h,l) ->
+ partition (f acc h) l
+ in
+ partition acc l
+
+
+let flatten wto =
+ let rec f acc = function
+ | [] -> acc
+ | Node v :: l -> f (v :: acc) l
+ | Component (v,w) :: l -> f (f (v :: acc) w) l
+ in
+ List.rev (f [] wto)
+
+(* Bourdoncle's WTO algorithm builds on Tarjan's SCC algorithm. In Tarjan:
+
+ - We visit every node once, starting from root, by following the
+ successors; this creates a spanning tree of the graph. SCCs are
+ subtrees of this spanning tree, whose root is the head of the SCC
+ (although in non-natural SCCs, it is possible to enter into a SCC
+ without going through the head).
+
+ - This spanning tree is obtained using DFS. What DFS guarantees is
+ that there is no path from a child c of a node n to other
+ children of n, provided that there is no path from c to an
+ ancestor of n. Thus when we visit other children of n, we know
+ that they are no path to them from the descendants of c.
+
+ - We assign consecutive numbers to each node in the order in which
+ they have been visited. As the iteration is depth-first search,
+ this gives a depth-first numbering (DFN).
+
+ - Each time we visit a node n, we push it on a stack. After the
+ visit, n is popped, unless a path exists from n to an element
+ earlier on the stack. So the stack contains elements currently
+ visited or that belongs to a non-trivial scc. Moreover, they
+ are in topological order.
+
+ About the proof of Tarjan:
+ http://ls2-www.cs.uni-dortmund.de/~wegener/papers/connected.pdf
+*)
+
+module Make(N:sig
+ type t (* = int *)
+ val equal: t -> t -> bool
+ val hash: t -> int
+ val pp: Format.formatter -> t -> unit
+ (* val succ: t -> t list *)
+ end) = struct
+
+ let rec equal_component (x:N.t component) (y:N.t component) =
+ match x,y with
+ | Node x, Node y -> N.equal x y
+ | Component (x,cx), Component (y,cy) -> N.equal x y && equal_partition cx cy
+ | _ -> false
+
+ and equal_partition x y =
+ (try List.for_all2 equal_component x y with Invalid_argument _ -> false)
+
+ module DFN = Hashtbl.Make(N);;
+
+ type level = int
+
+ (** Status of a visited vertex during the algorithm. *)
+ type status =
+ | Invisible (** The vertex have already been added into the partition and
+ is hidden until the end of the search. *)
+ | Parent of level (** The vertex have been visited and given a [level]. For
+ the algorithm, this implies that there is a path
+ between this vertex and the current vertex. *)
+
+ (** Result of one [visit] *)
+ type loop =
+ | NoLoop (** The vertex is not in a loop *)
+ | Loop of N.t * level (** The vertex is inside at least one loop, and
+ level is the smallest level of all these loops *)
+
+ let min_loop x y =
+ match x, y with
+ | NoLoop, z | z, NoLoop -> z
+ | Loop(_,xi), Loop(_,yi) ->
+ if xi <= yi then x else y
+
+ let is_no_loop = function
+ | NoLoop -> true | Loop _ -> false
+
+ type state =
+ { dfn: status DFN.t; (* Mapping from nodes to its dfn, depth-first
+ numbering. Note that we replaced the DFN=0
+ test by presence in the Hashtable. *)
+ mutable num: level; (* Number of visited nodes. *)
+ succs: N.t -> (N.t list); (* Successors transition. *)
+ stack: N.t Stack.t
+ }
+
+ (** Visit [vertex], and all the vertices reachable from [vertex]
+ which have not been explored yet (this is a depth-first search).
+ Also gives [partition], which is the partition built so far
+
+ Returns a pair (loop,partition) where
+ - [loop] tells whether we are in a loop or not and gives the vertex of
+ this loop with the lowest level. This vertex is also the deepest in the
+ stack and the neareast vertex from the root that is below [vertex] in
+ the spanning tree built by the DFS);
+ - [partition] is returned completed. *)
+ let rec visit ~pref state vertex partition =
+ match DFN.find state.dfn vertex with
+ (* The vertex is already in the partition *)
+ | Invisible -> NoLoop, partition (* skip it *)
+ (* The vertex have been visited but is not yet in the partition *)
+ | Parent i -> Loop (vertex,i), partition (* we are in a loop *)
+ (* The vertex have not been visited yet *)
+ | exception Not_found ->
+ (* Put the current vertex into the stack *)
+ Stack.push vertex state.stack;
+ (* Number it and mark it as visited *)
+ let n = state.num + 1 in
+ state.num <- n;
+ DFN.replace state.dfn vertex (Parent n);
+ (* Visit all its successors *)
+ let succs = state.succs vertex in
+ let (loop,partition) = List.fold_left (fun (loop,partition) succ ->
+ let (loop',partition) = visit ~pref state succ partition in
+ let loop = min_loop loop loop' in
+ (loop,partition)
+ ) (NoLoop,partition) succs
+ in
+ match loop with
+ (* We are not in a loop. Add the vertex to the partition *)
+ | NoLoop ->
+ let _ = Stack.pop state.stack in
+ DFN.replace state.dfn vertex Invisible;
+ (NoLoop,Node(vertex)::partition)
+ (* We are in a loop and the current vertex is the head of this loop *)
+ | Loop(head,_) when N.equal head vertex ->
+ (* Unmark all vertices in the loop, and, if pref is given, try to
+ return a better head *)
+ let rec reset_SCC best_head =
+ (** pop until vertex *)
+ let element = Stack.pop state.stack in
+ DFN.remove state.dfn element;
+ if not (N.equal element vertex) then begin
+ let best_head = match pref with
+ (** the strict is important because we are conservative *)
+ | Some cmp when cmp best_head element < 0 -> element
+ | _ -> best_head
+ in
+ reset_SCC best_head
+ end
+ else
+ best_head
+ in
+ let best_head = reset_SCC vertex in
+ let vertex, succs =
+ if N.equal best_head vertex
+ then vertex,succs
+ else best_head, state.succs best_head
+ in
+ (* Makes [vertex] invisible in the subsequents visits. *)
+ DFN.replace state.dfn vertex Invisible;
+ (* Restart the component analysis *)
+ let component = List.fold_left
+ (fun component succ ->
+ let (loop,component) = visit ~pref state succ component in
+ (* Since we reset the component we should have no loop *)
+ assert (is_no_loop loop);
+ component
+ ) [] succs
+ in
+ (NoLoop,Component(vertex,component)::partition)
+ | _ ->
+ (* [vertex] is part of a strongly connected component but is not the
+ head. Do not update partition; the vertex will
+ be added during the second visit of the SCC. *)
+ (loop,partition)
+
+ type pref = N.t -> N.t -> int
+
+ let partition ?pref ~init ~succs =
+ let state = {dfn = DFN.create 17; num = 0; succs;
+ stack = Stack.create () } in
+ let loop,component = visit ~pref state init [] in
+ assert (is_no_loop loop);
+ component
+
+end
diff --git a/src_colibri2/stdlib/wto.mli b/src_colibri2/stdlib/wto.mli
new file mode 100644
index 000000000..82d6f5b19
--- /dev/null
+++ b/src_colibri2/stdlib/wto.mli
@@ -0,0 +1,64 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Weak topological orderings (WTOs) are a hierarchical decomposition of the
+ a graph where each layer is topologically ordered and strongly connected
+ components are aggregated and ordered recursively. This is a very
+ convenient representation to describe an evaluation order to reach a
+ fixpoint. *)
+
+(** Each component of the graph is either an individual node of the graph
+ (without) self loop, or a strongly connected component where a node is
+ designed as the head of the component and the remaining nodes are given
+ by a list of components topologically ordered. *)
+type 'n component =
+ | Component of 'n * 'n partition
+ (** A strongly connected component, described by its head node and the
+ remaining sub-components topologically ordered *)
+ | Node of 'n
+ (** A single node without self loop *)
+
+(** A list of strongly connected components, sorted topologically *)
+and 'n partition = 'n component list
+
+val flatten: 'n partition -> 'n list
+
+val fold_heads: ('a -> 'n -> 'a) -> 'a -> 'n partition -> 'a
+
+(** This functor provides the partitioning algorithm constructing a WTO. *)
+module Make(Node:sig
+ type t
+ val equal: t -> t -> bool
+ val hash: t -> int
+ val pp: Format.formatter -> t -> unit
+ end):sig
+
+ type pref = Node.t -> Node.t -> int
+ (** partial order of preference for the choice of the head of a loop *)
+
+ (** Implements Bourdoncle "Efficient chaotic iteration strategies with
+ widenings" algorithm to compute a WTO. *)
+ val partition: ?pref:pref -> init:Node.t -> succs:(Node.t -> Node.t list) -> Node.t partition
+
+ val equal_component: Node.t component -> Node.t component -> bool
+ val equal_partition: Node.t partition -> Node.t partition -> bool
+end
diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index 44f5c3fc8..f77b2dcfb 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -10,11 +10,11 @@ module D = struct
let key =
DomKind.create_key
- ( module struct
+ (module struct
type nonrec t = t
let name = "adt"
- end )
+ end)
let merged d1 d2 = Option.equal equal d1 d2
@@ -36,8 +36,8 @@ module D = struct
f1 f2;
}
else Egraph.contradiction d
- | (One { case = c1; _ } as d1), Unk c2 | Unk c2, (One { case = c1; _ } as d1)
- ->
+ | (One { case = c1; _ } as d1), Unk c2
+ | Unk c2, (One { case = c1; _ } as d1) ->
if Case.S.mem c1 c2 then d1 else Egraph.contradiction d
let merge d (d1, n1) (d2, n2) _ =
@@ -121,7 +121,8 @@ end = struct
let[@ocaml.always inline] get a = get_dom D.key a
- let[@ocaml.always inline] get_value key n' d _ = Egraph.get_value d key n'
+ let[@ocaml.always inline] get_value key n' d _ =
+ Option.bind (Egraph.get_value d n') (Value.value key)
let[@ocaml.always inline] set_value (type b)
(value : (module ValueKind.Registered with type s = b)) n'
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index df5b98b0a..4c2480f44 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -19,39 +19,50 @@
(*************************************************************************)
open Colibri2_core
+open Colibri2_popop_lib
open Colibri2_stdlib.Std
let default_value = Q.zero
-let () =
- Interp.Register.id (fun interp t ->
- let (!>) t = RealValue.value (RealValue.coerce_nodevalue (interp t)) in
- let (!<) v = Some (RealValue.nodevalue (RealValue.index v)) in
- let (!<<) b = Some (if b then Boolean.values_true else Boolean.values_false) in
- match t with
- | { descr = Expr.App({builtin = Expr.Integer s},[],[]); _ } ->
- !< (Q.of_string s)
- | { descr = Expr.App({builtin = Expr.Decimal s},[],[]); _ } ->
- !< (Q.of_string_decimal s)
- | { descr = Expr.App({builtin = Expr.Rational s},[],[]); _ } ->
- !< (Q.of_string_decimal s)
- | { descr = Expr.App({builtin = Expr.Add},[],[a;b]); _ } ->
- !< (Q.add !>a !>b)
- | { descr = Expr.App({builtin = Expr.Sub},[],[a;b]); _ } ->
- !< (Q.sub !>a !>b)
- | { descr = Expr.App({builtin = Expr.Minus},[],[a]); _ } ->
- !< (Q.neg !>a)
- | { descr = Expr.App({builtin = Expr.Mul},[],[a;b]); _ } ->
- !< (Q.mul !>a !>b)
- | { descr = Expr.App({builtin = Expr.Lt},[],[arg1;arg2]); _ } ->
- !<< (Q.lt !>arg1 !>arg2)
- | { descr = Expr.App({builtin = Expr.Leq},[],[arg1;arg2]); _ } ->
- !<< (Q.leq !>arg1 !>arg2)
- | { descr = Expr.App({builtin = Expr.Gt},[],[arg1;arg2]); _ } ->
- !<< (Q.gt !>arg1 !>arg2)
- | { descr = Expr.App({builtin = Expr.Geq},[],[arg1;arg2]); _ } ->
- !<< (Q.geq !>arg1 !>arg2)
- | _ -> None
+let init_check d =
+ Interp.Register.check d (fun d t ->
+ let exception False in
+ try
+ let interp n = Opt.get_exn False (Egraph.get_value d n) in
+ let (!>) t = RealValue.value (RealValue.coerce_nodevalue (interp t)) in
+ let check r =
+ Some (Value.equal r (interp (Ground.node t)))
+ in
+ let (!<) v = check (RealValue.nodevalue (RealValue.index v)) in
+ let (!<<) b =
+ let r = if b then Boolean.values_true else Boolean.values_false in
+ check r
+ in
+ match Ground.sem t with
+ | { app = {builtin = Expr.Integer s}; tyargs = []; args = []; ty = _ } ->
+ !< (Q.of_string s)
+ | { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; ty = _ } ->
+ !< (Q.of_string_decimal s)
+ | { app = {builtin = Expr.Rational s}; tyargs = []; args = []; ty = _ } ->
+ !< (Q.of_string_decimal s)
+ | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; ty = _ } ->
+ !< (Q.add !>a !>b)
+ | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; ty = _ } ->
+ !< (Q.sub !>a !>b)
+ | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; ty = _ } ->
+ !< (Q.neg !>a)
+ | { app = {builtin = Expr.Mul}; tyargs = []; args = [a;b]; ty = _ } ->
+ !< (Q.mul !>a !>b)
+ | { app = {builtin = Expr.Lt}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
+ !<< (Q.lt !>arg1 !>arg2)
+ | { app = {builtin = Expr.Leq}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
+ !<< (Q.leq !>arg1 !>arg2)
+ | { app = {builtin = Expr.Gt}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
+ !<< (Q.gt !>arg1 !>arg2)
+ | { app = {builtin = Expr.Geq}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
+ !<< (Q.geq !>arg1 !>arg2)
+ | _ -> None
+ with False -> Some false
)
module RealValue = RealValue
@@ -63,6 +74,7 @@ let th_register env =
Fourier.init env;
Mul.init env;
Dom_product.init env;
+ init_check env;
()
let () = Egraph.add_default_theory th_register
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index 994f70fa1..cbb5f1848 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -160,7 +160,9 @@ end = struct
(v' d n)
let [@ocaml.always inline] get a = get_dom dom a
let [@ocaml.always inline] get_value key n' = fun d _ ->
- Egraph.get_value d key n'
+ let open Option in
+ let* v = Egraph.get_value d n' in
+ Value.value key v
let [@ocaml.always inline] set_value (type b)
(value:(module ValueKind.Registered with type s = b))
n' (v':b option option monad) : unit monad =
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 18b57f2bc..c6a2e8f33 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -61,7 +61,10 @@ module Monad : sig
end = struct
type ('a,'b) monad = Egraph.t -> Node.t -> 'a -> 'b
let [@ocaml.always inline] get' key n' = fun d n v ->
- if Node.equal n n' then Some v else Egraph.get_value d key n'
+ if Node.equal n n' then Some v else
+ let open Option in
+ let* v = Egraph.get_value d n' in
+ Value.value key v
let [@ocaml.always inline] set' : type b.
(module ValueKind.Registered with type s = b) ->
Node.t -> ('a,b option) monad -> ('a, unit) monad =
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index 1ed567891..4492b29a5 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -50,7 +50,11 @@ let node_false = BoolValue.node value_false
let index sem v = Node.index_sem sem v
-let is env node = Egraph.get_value env dom node
+let is env node =
+ let open Option in
+ let+ v = Egraph.get_value env node in
+ Opt.get_exn Impossible (Value.value dom v)
+
let is_true env node = Node.equal node node_true
|| Equal.option Equal.bool (is env node) (Some true)
let is_false env node = Node.equal node node_false
@@ -124,7 +128,7 @@ module Th = struct
exception Found of Node.t * bool
let find_not_known d l =
IArray.iter (fun (node,b) ->
- match Egraph.get_value d dom node with
+ match Egraph.get_value d node with
| Some _ -> ()
| None -> raise (Found (node,b))
) l
@@ -132,8 +136,8 @@ module Th = struct
let _bcp d l absorbent =
try
let res = IArray.fold (fun acc node ->
- match Egraph.get_value d dom node, acc with
- | Some b, _ when Equal.bool b absorbent -> raise (TopKnown absorbent)
+ match is d node, acc with
+ | Some b, _ when Bool.equal b absorbent -> raise (TopKnown absorbent)
| Some _, _ -> acc
| None, Some _ -> raise Exit
| None, None -> Some node)
@@ -160,9 +164,8 @@ module DaemonPropaNot = struct
let throttle = 100
let wakeup d =
function
- | Events.Fired.EventValue(_,dom',_,((_,node,ncl))) ->
- assert (ValueKind.equal dom dom');
- begin match Egraph.get_value d dom node with
+ | Events.Fired.EventValue(_,_,((_,node,ncl))) ->
+ begin match is d node with
| None -> raise Impossible
| Some b ->
set_bool d ncl (not b)
@@ -215,17 +218,17 @@ module DaemonPropa = struct
let own = ThE.node thterm in
let set_dom_up_true d own _ _ =
let b = (not v.topnot) in
- match Egraph.get_value d dom own with
+ match is d own with
| Some b' when Equal.bool b' b -> ()
| _ -> set_bool d own b in
let merge_bcp node sign =
Debug.dprintf2 debug "[Bool] @[merge_bcp %a@]" Node.pp node;
- match Egraph.get_value d dom own with
+ match is d own with
| Some b' ->
let b = mulbool sign (mulbool b' v.topnot) in
set_bool d node b
| None -> (** merge *)
- match Egraph.get_value d dom node with
+ match is d node with
| Some b' ->
let b = mulbool sign (mulbool b' v.topnot) in
set_bool d own b
@@ -241,7 +244,7 @@ module DaemonPropa = struct
(merge_bcp node sign; raise Exit)
else
let node,sign = IArray.get v.lits pos in
- match Egraph.get_value d dom node with
+ match is d node with
| None -> node,pos
| Some b when mulbool b sign (** true absorbent of or *) ->
set_dom_up_true d own node b; raise Exit
@@ -271,7 +274,7 @@ module DaemonPropa = struct
let wakeup_own d thterm =
let v = ThE.sem thterm in
let own = ThE.node thterm in
- begin match Egraph.get_value d dom own with
+ begin match is d own with
| None -> (* only during init *)
Demon.Fast.attach d key
[Demon.Create.EventValue(own, dom, All thterm)];
@@ -295,11 +298,9 @@ module DaemonPropa = struct
wakeup_lit d thterm last watcher
let wakeup d = function
- | Events.Fired.EventValue(_,dom',_,Lit(thterm,watched,next)) ->
- assert( ValueKind.equal dom dom' );
+ | Events.Fired.EventValue(_,_,Lit(thterm,watched,next)) ->
ignore (wakeup_lit d thterm watched next)
- | Events.Fired.EventValue(_ownr,dom',_,All thterm) ->
- assert( ValueKind.equal dom dom' );
+ | Events.Fired.EventValue(_ownr,_,All thterm) ->
(** use this own because the other is the representant *)
ignore (wakeup_own d thterm)
| _ -> raise UnwaitedEvent
@@ -401,7 +402,7 @@ module ChoBool = struct
set_bool env node b
let choose_decision node env =
- match Egraph.get_value env dom node with
+ match is env node with
| Some _ ->
Debug.dprintf2 Egraph.print_decision "[Bool] No decision for %a" Node.pp node;
Egraph.DecNo
@@ -442,6 +443,37 @@ let converter d (f:Ground.t) =
reg _false
| _ -> ()
+
+let init_check d =
+ Interp.Register.check d (fun d t ->
+ let exception False in
+ try
+ let interp n = Opt.get_exn False (Egraph.get_value d n) in
+ let (!>) t = BoolValue.value (BoolValue.coerce_nodevalue (interp t)) in
+ let check r =
+ Some (Value.equal r (interp (Ground.node t)))
+ in
+ let (!<) b =
+ let r = if b then values_true else values_false in
+ check r
+ in
+ match Ground.sem t with
+ | { app = {builtin = Expr.Or}; tyargs = []; args = args; ty = _ } ->
+ !< (List.fold_left (||) false (List.map (!>) args))
+ | { app = {builtin = Expr.And}; tyargs = []; args = args; ty = _ } ->
+ !< (List.fold_left (&&) true (List.map (!>) args))
+ | { app = {builtin = Expr.Imply}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
+ !< ( not (!> arg1) || !> arg2 )
+ | { app = {builtin = Expr.Neg}; tyargs = []; args = [arg]; ty = _ } ->
+ !< (not (!> arg))
+ | { app = {builtin = Expr.True}; tyargs = []; args = []; ty = _ } ->
+ check values_true
+ | { app = {builtin = Expr.False}; tyargs = []; args = []; ty = _ } ->
+ check values_false
+ | _ -> None
+ with False -> Some false
+ )
+
let th_register env =
RDaemonPropaNot.init env;
RDaemonPropa.init env;
@@ -451,30 +483,31 @@ let th_register env =
Egraph.register env node_true;
Egraph.register env node_false;
Ground.register_converter env converter;
+ init_check 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 () =
+ * 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 = Egraph.get_value d dom n in
+ * 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) *)
@@ -482,24 +515,4 @@ let default_value = true
-let () =
- Interp.Register.id (fun interp t ->
- let (!>) t = BoolValue.value (BoolValue.coerce_nodevalue (interp t)) in
- let (!<) b = Some (if b then values_true else values_false) in
- match t with
- | { descr = Expr.App({builtin = Expr.Or},[],args); _ } ->
- !< (List.fold_left (||) false (List.map (!>) args))
- | { descr = Expr.App({builtin = Expr.And},[],args); _ } ->
- !< (List.fold_left (&&) true (List.map (!>) args))
- | { descr = Expr.App({builtin = Expr.Imply},[],[arg1;arg2]); _ } ->
- !< ( not (!> arg1) || !> arg2 )
- | { descr = Expr.App({builtin = Expr.Neg},[],[arg]); _ } ->
- !< (not (!> arg))
- | { descr = Expr.App({builtin = Expr.True},[],[]); _ } ->
- Some values_true
- | { descr = Expr.App({builtin = Expr.False},[],[]); _ } ->
- Some values_false
- | _ -> None
- )
-
type t = T.t
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index 553bf87e5..3a26d4635 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -191,22 +191,13 @@ let find_not_disequal d s =
(match dis1, dis2 with
| Some dis1, Some dis2 when not (Dis.disjoint dis1 dis2) -> true
| _ -> false) ||
- (try
- let fold2_inter (type a) (k:a ValueKind.t) v1 v2 () =
- let (module V) = ValueKind.get k in
- if not (V.equal v1 v2) then raise Exit
- in
- MValues.fold2_inter {fold2_inter} values1 values2 ();
- false
- with Exit -> true)
+ (match values1, values2 with
+ | Some v1, Some v2 -> not (Value.equal v1 v2)
+ | _ -> false)
in
let get_dis_and_values cl =
Egraph.get_dom d dom cl,
- ValueKind.fold {fold=(fun k acc ->
- match Egraph.get_value d k cl with
- | None -> acc
- | Some v -> MValues.add k v acc)}
- MValues.empty
+ Egraph.get_value d cl
in
assert (Th.inv s);
let rec inner_loop cl1 s1 enum2 =
@@ -428,8 +419,7 @@ module DaemonPropaITE = struct
let delay = Events.Delayed_by 1
let throttle = 100
let wakeup d = function
- | Events.Fired.EventValue(cond,dom,_,clsem) ->
- assert (ValueKind.equal dom Boolean.dom);
+ | Events.Fired.EventValue(cond,_,clsem) ->
let v = EITE.sem clsem in
assert (Egraph.is_equal d cond v.cond);
begin match Boolean.is d v.cond with
@@ -480,9 +470,6 @@ module RDaemonInitITE = Demon.Fast.Register(DaemonInitITE)
(** Give for a node the values that are different *)
let iter_on_value_different
- (type a)
- (type b)
- ((module Val): (module Colibri2_core.ValueKind.Registered with type s = a and type t = b))
~they_are_different
(d:Egraph.t)
(own:Node.t) =
@@ -490,10 +477,10 @@ let iter_on_value_different
let iter elt =
let iter n =
if not (Egraph.is_equal d own n) then
- match Egraph.get_value d Val.key n with
+ match Egraph.get_value d n with
| None -> ()
| Some v ->
- they_are_different n v
+ they_are_different n v
in
Node.S.iter iter (ThE.sem (Dis.to_node elt))
in
@@ -558,46 +545,59 @@ let bool_init_diff_to_value d =
~already_registered:[Boolean.value_true;Boolean.value_false]
(** {2 Interpretations} *)
-let () =
- let interp ~interp t =
- try
- let fold acc e = Value.S.add_new Exit (interp e) acc in
- let _ = Node.S.fold_left fold Value.S.empty t in
- Boolean.values_false
- with Exit ->
- Boolean.values_true
- in
- Interp.Register.thterm sem interp
-
-let () =
- let interp ~interp (t:ITE.t) =
- let c = Boolean.BoolValue.value (Boolean.BoolValue.coerce_nodevalue (interp t.cond)) in
- if c then interp t.then_ else interp t.else_
- in
- Interp.Register.thterm ITE.key interp
-
-let () =
- Interp.Register.id (fun interp t ->
- let (!>) n = Boolean.BoolValue.value (Boolean.BoolValue.coerce_nodevalue (interp n)) in
- let (!<) b = Some (if b then Boolean.values_true else Boolean.values_false) in
- match t with
- | { descr = Expr.App({builtin = Expr.Equal},[_],a::l); _ } ->
- let a = interp a in
- !< (List.for_all (fun t -> Value.equal a (interp t)) l)
- | { descr = Expr.App({builtin = Expr.Equiv},[_],[a;b]); _ } ->
- !< (Value.equal (interp a) (interp b))
- | { descr = Expr.App({builtin = Expr.Distinct},[_],args); _ } ->
- begin
- try
- let fold acc v = Value.S.add_new Exit (interp v) acc in
- let _ = List.fold_left fold Value.S.empty args in
- Some Boolean.values_false
- with Exit ->
- Some Boolean.values_true
- end
- | { descr = Expr.App({builtin = Expr.Ite},[_],[c;a;b]); _ } ->
- Some (if (!> c) then interp a else interp b)
- | _ -> None
+(* let () =
+ * let interp ~interp t =
+ * try
+ * let fold acc e = Value.S.add_new Exit (interp e) acc in
+ * let _ = Node.S.fold_left fold Value.S.empty t in
+ * Boolean.values_false
+ * with Exit ->
+ * Boolean.values_true
+ * in
+ * Interp.Register.thterm sem interp
+ *
+ * let () =
+ * let interp ~interp (t:ITE.t) =
+ * let c = Boolean.BoolValue.value (Boolean.BoolValue.coerce_nodevalue (interp t.cond)) in
+ * if c then interp t.then_ else interp t.else_
+ * in
+ * Interp.Register.thterm ITE.key interp *)
+
+let init_check d =
+ Interp.Register.check d (fun d t ->
+ let exception False in
+ try
+ let interp n = Opt.get_exn False (Egraph.get_value d n) in
+ let (!>) n =
+ Boolean.BoolValue.value
+ (Boolean.BoolValue.coerce_nodevalue (interp n))
+ in
+ let check r =
+ Some (Value.equal r (interp (Ground.node t)))
+ in
+ let (!<) b =
+ let r = if b then Boolean.values_true else Boolean.values_false in
+ check r
+ in
+ match Ground.sem t with
+ | { app = {builtin = Expr.Equal}; tyargs = [_]; args = a::l; ty = _ } ->
+ let a = interp a in
+ !< (List.for_all (fun t -> Value.equal a (interp t)) l)
+ | { app = {builtin = Expr.Equiv}; tyargs = [_]; args = [a;b]; ty = _ } ->
+ !< (Value.equal (interp a) (interp b))
+ | { app = {builtin = Expr.Distinct}; tyargs = [_]; args = args; ty = _ } ->
+ begin
+ try
+ let fold acc v = Value.S.add_new Exit (interp v) acc in
+ let _ = List.fold_left fold Value.S.empty args in
+ check Boolean.values_false
+ with Exit ->
+ check Boolean.values_true
+ end
+ | { app = {builtin = Expr.Ite}; tyargs = [_]; args = [c;a;b]; ty = _ } ->
+ check (if (!> c) then interp a else interp b)
+ | _ -> None
+ with False -> Some false
)
@@ -635,6 +635,7 @@ let th_register env =
DaemonInitITE.key [Demon.Create.EventRegSem(ITE.key,())];
Ground.register_converter env converter;
bool_init_diff_to_value env;
+ init_check env;
()
let () = Egraph.add_default_theory th_register
diff --git a/src_colibri2/theories/bool/equality.mli b/src_colibri2/theories/bool/equality.mli
index 1352f9a6d..9cabfdec5 100644
--- a/src_colibri2/theories/bool/equality.mli
+++ b/src_colibri2/theories/bool/equality.mli
@@ -27,8 +27,7 @@ val is_disequal : Egraph.t -> Node.t -> Node.t -> bool
val ite : Node.t -> Node.t -> Node.t -> Node.t
val iter_on_value_different:
- (module ValueKind.Registered with type s = 'a and type t = 'b) ->
- they_are_different:(Node.t -> 'a -> unit) ->
+ they_are_different:(Node.t -> Value.t -> unit) ->
Egraph.t -> Node.t -> unit
--
GitLab