diff --git a/src_colibri2/core/dune b/src_colibri2/core/dune
index c0ce1717e0e529a5a96948fff5aa5d125ca8d94d..12453f2f4e307ea03c62aff17b9dd91374c4aeab 100644
--- a/src_colibri2/core/dune
+++ b/src_colibri2/core/dune
@@ -6,7 +6,7 @@
colibri2_core_structures)
(preprocess
(pps ppx_deriving.std ppx_hash))
- (flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
+ (flags :standard -w +a-4-42-44-48-50-58-60-40-9@8 -color always -open
Containers -open Colibri2_stdlib -open Std -open Colibri2_core_structures)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index 243c9cb655bae5f308d8f4195b0d8cf88c9ca0c3..2461eedfced2d5717b2ea166dec905c6342ca6bd 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -40,14 +40,16 @@ let stats_register =
module DecTag = DInt
+(** For each kind of domain *)
type 'a domtable = {
+ (** For each representative node its associated domain if any *)
table : 'a Node.M.t;
+ (** Events: the domain of this node changed *)
events : Events.Wait.t Bag.t Node.M.t;
+ (** Events: the domain of any node changed *)
reg_events : Events.Wait.t list;
}
-type semtable = Events.Wait.t list
-
module VDomTable = DomKind.MkVector (struct type ('a,'unused) t = 'a domtable end)
module VSemTable = ThTermKind.Vector
@@ -73,28 +75,38 @@ module Def = struct
saved_event_reg : Events.Wait.t list Node.M.t;
saved_event_any_reg : Events.Wait.t list;
saved_dom : delayed_t VDomTable.t;
- saved_sem : semtable VSemTable.t;
+ saved_sem : Events.Wait.t list VSemTable.t;
saved_value : valuetable;
saved_envs : Env.Saved.VectorH.t;
}
- and t = {
+ and t = {
+ (** Union Find *)
mutable repr : Node.t Node.M.t;
mutable rang : int Node.M.t;
+ (** Events: the representative of this node changed *)
mutable event_repr : Events.Wait.t Bag.t Node.M.t;
+ (** Events: the representative of any node changed *)
mutable event_any_repr : Events.Wait.t list;
+ (** Events: the value of this node has been set *)
mutable event_value : Events.Wait.t Bag.t Node.M.t;
+ (** Events: this node have been registered *)
mutable event_reg : Events.Wait.t list Node.M.t;
+ (** Events: any node have been registered *)
mutable event_any_reg : Events.Wait.t list;
- (** extensible "number of fields" *)
+ (** Events: semantic term of this kind has been registered *)
+ sem : Events.Wait.t list VSemTable.t;
+ (** Information on the domains, data is {!'a domtable} *)
dom : delayed_t VDomTable.t;
- sem : semtable VSemTable.t;
+ (** Value *)
mutable value : valuetable;
+ (** Environment saved during backtrack point *)
envs : Env.Saved.VectorH.t;
- mutable current_delayed : delayed_t; (** For assert-check *)
+ (** Environment not saved during backtrack point, they should use !{Context} *)
unsaved_envs: Env.Unsaved.VectorH.t;
history : saved Context.history;
+ mutable current_delayed : delayed_t; (** For assert-check *)
}
(** delayed_t is used *)
@@ -504,13 +516,6 @@ module Delayed = struct
(* Add the actual merge for later *)
Queue.add (Merge (node,node')) t.todo_merge
- let check_no_dom t node =
- let foldi acc _dom (domtable: _ domtable) =
- acc &&
- not (Node.M.mem node domtable.table)
- in
- VDomTable.fold_initializedi {VDomTable.foldi} true t.env.dom
-
let register t node =
assert (is_current_env t);
if not (is_registered t node) then begin
@@ -1044,26 +1049,6 @@ module Delayed = struct
let reg_events = event::dom_table.reg_events in
VDomTable.set t.env.dom dom {dom_table with reg_events}
- let attached_reg_node
- (type k) (type d) d node (dem:(k,d) Events.Dem.t) : k Enum.t =
- Enum.from_list
- ~filter:(function
- | Events.Wait.Event(dem',_) ->
- Events.Dem.equal dem dem'
- )
- ~map:(fun (Events.Wait.Event(dem',event)) ->
- let Poly.Eq = Events.Dem.Eq.coerce_type dem dem' in (event:k)
- )
- (Node.M.find_def [] node d.env.event_reg)
-
- let attached_node
- (type k) (type d) d node (dem:(k,d) Events.Dem.t) : k Enum.t =
- Enum.from_bag
- ~filter:(fun (Events.Wait.Event(dem',_)) -> Events.Dem.equal dem dem')
- ~map:(fun (Events.Wait.Event(dem',event)) ->
- let Poly.Eq = Events.Dem.Eq.coerce_type dem dem' in (event:k) )
- (Node.M.find_def Bag.empty node d.env.event_repr)
-
end
@@ -1203,10 +1188,6 @@ module Backtrackable = struct
(* assert (check_disabled_delayed t); *)
t
- let get_direct_dom t dom node =
- assert (check_disabled_delayed t);
- get_direct_dom t dom node
-
let draw_graph ?force t = let t = Hidden.ro t in draw_graph ?force t
let output_graph s t = let t = Hidden.ro t in output_graph s t
end
diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml
index a6d69ec436f37134bba1be9e12d39dd3bec10006..bad08ebd9776cb66695537c8ebde5dacd3059d08 100644
--- a/src_colibri2/core/events.ml
+++ b/src_colibri2/core/events.ml
@@ -41,8 +41,6 @@ module Print = struct (** Cutting the knot for pp *)
let pdem_runable : pdem_runable =
{pdem_runable = fun _ _ _ -> assert false} (** called too early *)
- let dem_runable dem fmt s = pdem_runable.pdem_runable dem fmt s
-
end
@@ -143,8 +141,6 @@ module Wait = struct
{translate = fun (node,dom) data -> EventDom(node,dom,data)}
let translate_value =
{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 =
{translate = fun node data -> EventReg(node,data)}
let translate_regnode =
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index fb4ca294f7276b4bc460d3bd175c42518e81118f..cc708f14d5a08cc6768033bfd869ad38cc07ae78 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -172,7 +172,7 @@ module ClosedQuantifier = struct
module T = struct
open! Base
type binder = Forall | Exists
- [@@deriving eq, ord, show, hash]
+ [@@deriving eq, ord, hash]
type t = {
binder: binder;
subst: Subst.t;
diff --git a/src_colibri2/core/ground.mli b/src_colibri2/core/ground.mli
index d0a830f244e5d4021cdd2391a386c81f2a909439..a98fddf323ea4e209df1914965621b2dbb661c4b 100644
--- a/src_colibri2/core/ground.mli
+++ b/src_colibri2/core/ground.mli
@@ -44,7 +44,7 @@ module Subst: sig
type t = {
term: Node.t Expr.Term.Var.M.t;
ty: ty;
- } [@@deriving show, hash, ord, eq ]
+ }
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
@@ -57,7 +57,7 @@ module Ty: sig
type t = All.ty = {
app: Expr.Ty.Const.t;
args: t list
- } [@@deriving hash, ord, eq ]
+ }
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
@@ -99,7 +99,7 @@ module Term: sig
tyargs : Ty.t list;
args : Node.t IArray.t;
ty:Ty.t
- } [@@deriving hash, ord, eq ]
+ }
val key: t ThTermKind.t
diff --git a/src_colibri2/core/structures/domKind.ml b/src_colibri2/core/structures/domKind.ml
index df4d01380a6f4021e0ebc42599dbe63c2ad375f8..a5ac1051cde3ae7c438bec1663d28722fd9c9dd1 100644
--- a/src_colibri2/core/structures/domKind.ml
+++ b/src_colibri2/core/structures/domKind.ml
@@ -18,13 +18,8 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Colibri2_popop_lib
open Nodes
-let debug = Debug.register_info_flag
- ~desc:"for the domains"
- "Egraph.dom"
-
module Dom = Keys.Make_key(struct end)
include Dom
type 'a dom = 'a t
diff --git a/src_colibri2/core/structures/dune b/src_colibri2/core/structures/dune
index ea68cfe709676bb1153ab933d3dcac0a154853de..92ee0942528014e9a40dd3927df9dd5fc9eccc9f 100644
--- a/src_colibri2/core/structures/dune
+++ b/src_colibri2/core/structures/dune
@@ -7,7 +7,7 @@
dolmen.std)
(preprocess
(pps ppx_deriving.std))
- (flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
+ (flags :standard -w +a-4-42-44-48-50-58-60-40-9@8 -color always -open
Containers -open Colibri2_stdlib -open Std)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src_colibri2/popop_lib/TimeWheel.ml b/src_colibri2/popop_lib/TimeWheel.ml
index 66c9667d00dce3f4c5edea203e4b6dcf320a9acc..bfdfbda7ecf50aa26772ec524bc532bcf5d15dc5 100644
--- a/src_colibri2/popop_lib/TimeWheel.ml
+++ b/src_colibri2/popop_lib/TimeWheel.ml
@@ -69,16 +69,6 @@ module Make
size: int Ref.t;
}
- let new_bits o n = (lnot o) land n
-
- (* lowest first *)
- let rec iter_bits f i =
- if i <> 0 then
- let j = Int.ctz i in
- f j;
- iter_bits f (i land (lnot (1 lsl j)))
-
-
let create ctx = {
current = Ref.create ctx 0;
futur = Array.create ctx Int.num_bits Nil;
diff --git a/src_colibri2/popop_lib/dune b/src_colibri2/popop_lib/dune
index e668e715828128044b83a34aad71016b0eaf25b2..e3657e73e4bba13224c51ee8d9171e6be9cad8a4 100644
--- a/src_colibri2/popop_lib/dune
+++ b/src_colibri2/popop_lib/dune
@@ -8,6 +8,6 @@
(libraries str unix zarith base fmt)
(preprocess
(pps ppx_deriving.std ppx_hash))
- (flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always)
+ (flags :standard -w +a-4-42-44-48-50-58-60-40-9@8 -color always)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src_colibri2/popop_lib/intmap.ml b/src_colibri2/popop_lib/intmap.ml
index d5c688349b080767b028263d718a9737f84902fe..a1b331e0d0e92233189ff386d3110e17697f9844 100644
--- a/src_colibri2/popop_lib/intmap.ml
+++ b/src_colibri2/popop_lib/intmap.ml
@@ -135,11 +135,6 @@ module Make(K:Map_intf.TaggedEqualType) :
let empty = mk_Empty
let singleton = mk_Lf
- let br p t0 t1 = match view t0 , view t1 with
- | Empty,_ -> t1
- | _,Empty -> t0
- | _ -> mk_Br p t0 t1
-
let lf k = function None -> mk_Empty | Some x -> mk_Lf k x
(* good sharing *)
@@ -217,14 +212,14 @@ module Make(K:Map_intf.TaggedEqualType) :
match_prefix (K.tag k) p &&
mem k (if zero_bit (K.tag k) p then t0 else t1)
- let rec findq k t = match view t with
- | Empty -> raise Not_found
- | Lf(i,x) -> if K.equal k i then (x,t) else raise Not_found
- | Br(p,t0,t1) ->
- if match_prefix (K.tag k) p then
- findq k (if zero_bit (K.tag k) p then t0 else t1)
- else
- raise Not_found
+ (* let rec findq k t = match view t with
+ * | Empty -> raise Not_found
+ * | Lf(i,x) -> if K.equal k i then (x,t) else raise Not_found
+ * | Br(p,t0,t1) ->
+ * if match_prefix (K.tag k) p then
+ * findq k (if zero_bit (K.tag k) p then t0 else t1)
+ * else
+ * raise Not_found *)
let rec find_exn exn k t = match view t with
| Empty -> raise exn
@@ -442,25 +437,25 @@ module Make(K:Map_intf.TaggedEqualType) :
let t1 = mapf phi t1 in glue t0 t1
(* good sharing *)
- let mapq phi t =
- let rec mapq phi t = match view t with
- | Empty -> t
- | Lf(k,x) -> lf0 k x t (phi k x)
- | Br(_,t0,t1) ->
- let t0' = mapq phi t0 in
- let t1' = mapq phi t1 in
- glue01 t0' t1' t0 t1 t
- in match view t with (* to be sorted *)
- | Empty -> t
- | Lf(k,x) -> lf0 k x t (phi k x)
- | Br(p,t0,t1) when p = max_int ->
- let t1' = mapq phi t1 in
- let t0' = mapq phi t0 in
- glue01 t0' t1' t0 t1 t
- | Br(_,t0,t1) ->
- let t0' = mapq phi t0 in
- let t1' = mapq phi t1 in
- glue01 t0' t1' t0 t1 t
+ (* let mapq phi t =
+ * let rec mapq phi t = match view t with
+ * | Empty -> t
+ * | Lf(k,x) -> lf0 k x t (phi k x)
+ * | Br(_,t0,t1) ->
+ * let t0' = mapq phi t0 in
+ * let t1' = mapq phi t1 in
+ * glue01 t0' t1' t0 t1 t
+ * in match view t with (\* to be sorted *\)
+ * | Empty -> t
+ * | Lf(k,x) -> lf0 k x t (phi k x)
+ * | Br(p,t0,t1) when p = max_int ->
+ * let t1' = mapq phi t1 in
+ * let t0' = mapq phi t0 in
+ * glue01 t0' t1' t0 t1 t
+ * | Br(_,t0,t1) ->
+ * let t0' = mapq phi t0 in
+ * let t1' = mapq phi t1 in
+ * glue01 t0' t1' t0 t1 t *)
(** bad sharing but polymorph *)
let mapq' :
@@ -567,15 +562,15 @@ module Make(K:Map_intf.TaggedEqualType) :
| _ -> aux k t
(* good sharing *)
- let rec partition_split p t = match view t with
- | Empty -> (t,t)
- | Lf(k,x) -> let u,v = p k x in (lf0 k x t u), (lf0 k x t v)
- | Br(_,t0,t1) ->
- let t0',u0' = partition_split p t0 in
- let t1',u1' = partition_split p t1 in
- if t0'==t0 && t1'==t1 then (t, u0') (* u0' and u1' are empty *)
- else if u0'==t0 && u1'==t1 then (t0', t) (* t0' and t1' are empty *)
- else (glue t0' t1'),(glue u0' u1')
+ (* let rec partition_split p t = match view t with
+ * | Empty -> (t,t)
+ * | Lf(k,x) -> let u,v = p k x in (lf0 k x t u), (lf0 k x t v)
+ * | Br(_,t0,t1) ->
+ * let t0',u0' = partition_split p t0 in
+ * let t1',u1' = partition_split p t1 in
+ * if t0'==t0 && t1'==t1 then (t, u0') (\* u0' and u1' are empty *\)
+ * else if u0'==t0 && u1'==t1 then (t0', t) (\* t0' and t1' are empty *\)
+ * else (glue t0' t1'),(glue u0' u1') *)
(* ---------------------------------------------------------------------- *)
(* --- Iter --- *)
@@ -725,45 +720,45 @@ module Make(K:Map_intf.TaggedEqualType) :
let inter phi = interi (fun i x y -> lf i (phi i x y))
(* good sharing with s *)
- let lfq phi i x y s t =
- match phi i x y with
- | None -> mk_Empty
- | Some w -> if w == x then s else if w == y then t else mk_Lf i w
- let occur0 phi i x s t =
- try let (y,t) = findq i t in lfq phi i x y s t
- with Not_found -> mk_Empty
- let occur1 phi j y s t =
- try let (x,s) = findq j s in lfq phi j x y s t
- with Not_found -> mk_Empty
+ (* let lfq phi i x y s t =
+ * match phi i x y with
+ * | None -> mk_Empty
+ * | Some w -> if w == x then s else if w == y then t else mk_Lf i w *)
+ (* let occur0 phi i x s t =
+ * try let (y,t) = findq i t in lfq phi i x y s t
+ * with Not_found -> mk_Empty *)
+ (* let occur1 phi j y s t =
+ * try let (x,s) = findq j s in lfq phi j x y s t
+ * with Not_found -> mk_Empty *)
(* good sharing with s *)
- let rec interq phi s t =
- match view s , view t with
- | Empty , _ -> s
- | _ , Empty -> t
- | Lf(i,x) , Lf(j,y) ->
- if K.equal i j
- then lfq phi i x y s t
- else mk_Empty
- | Lf(i,x) , Br _ -> occur0 phi i x s t
- | Br _ , Lf(j,y) -> occur1 phi j y s t
- | Br(p,s0,s1) , Br(q,t0,t1) ->
- if p == q then
- (* prefixes agree *)
- glue2 (interq phi s0 t0) (interq phi s1 t1) s0 s1 s t0 t1 t
- else if included_prefix p q then
- (* q contains p. Intersect t with a subtree of s *)
- if zero_bit q p
- then interq phi s0 t (* t has bit m = 0 => t is inside s0 *)
- else interq phi s1 t (* t has bit m = 1 => t is inside s1 *)
- else if included_prefix q p then
- (* p contains q. Intersect s with a subtree of t *)
- if zero_bit p q
- then interq phi s t0 (* s has bit n = 0 => s is inside t0 *)
- else interq phi s t1 (* t has bit n = 1 => s is inside t1 *)
- else
- (* prefix disagree *)
- mk_Empty
+ (* let rec interq phi s t =
+ * match view s , view t with
+ * | Empty , _ -> s
+ * | _ , Empty -> t
+ * | Lf(i,x) , Lf(j,y) ->
+ * if K.equal i j
+ * then lfq phi i x y s t
+ * else mk_Empty
+ * | Lf(i,x) , Br _ -> occur0 phi i x s t
+ * | Br _ , Lf(j,y) -> occur1 phi j y s t
+ * | Br(p,s0,s1) , Br(q,t0,t1) ->
+ * if p == q then
+ * (\* prefixes agree *\)
+ * glue2 (interq phi s0 t0) (interq phi s1 t1) s0 s1 s t0 t1 t
+ * else if included_prefix p q then
+ * (\* q contains p. Intersect t with a subtree of s *\)
+ * if zero_bit q p
+ * then interq phi s0 t (\* t has bit m = 0 => t is inside s0 *\)
+ * else interq phi s1 t (\* t has bit m = 1 => t is inside s1 *\)
+ * else if included_prefix q p then
+ * (\* p contains q. Intersect s with a subtree of t *\)
+ * if zero_bit p q
+ * then interq phi s t0 (\* s has bit n = 0 => s is inside t0 *\)
+ * else interq phi s t1 (\* t has bit n = 1 => s is inside t1 *\)
+ * else
+ * (\* prefix disagree *\)
+ * mk_Empty *)
(* ---------------------------------------------------------------------- *)
(* --- Union --- *)
@@ -976,42 +971,42 @@ module Make(K:Map_intf.TaggedEqualType) :
(* good sharing with s *)
- let rec diffq phi s t =
- match view s , view t with
- | Empty , _ -> s
- | _ , Empty -> s
- | Lf(i,x) , Lf(j,y) ->
- if K.equal i j
- then lfq phi i x y s t
- else s
- | Lf(i,x) , Br _ ->
- (match occur i t with None -> s | Some y -> lfq phi i x y s t)
- | Br _ , Lf(j,y) -> change (fun j y x -> match x with
- | None -> None
- | Some x -> phi j x y) j y s
- | Br(p,s0,s1) , Br(q,t0,t1) ->
- if p == q then
- (* prefixes agree *)
- let t0' = (diffq phi s0 t0) in
- let t1' = (diffq phi s1 t1) in
- glue01 t0' t1' s0 s1 s
- else if included_prefix p q then
- (* q contains p. *)
- if zero_bit q p
- then (* t has bit m = 0 => t is inside s0 *)
- let s0' = (diffq phi s0 t) in
- glue0 s0' s0 s1 s
- else (* t has bit m = 1 => t is inside s1 *)
- let s1' = (diffq phi s1 t) in
- glue1 s1' s0 s1 s
- else if included_prefix q p then
- (* p contains q. *)
- if zero_bit p q
- then diffq phi s t0 (* s has bit n = 0 => s is inside t0 *)
- else diffq phi s t1 (* t has bit n = 1 => s is inside t1 *)
- else
- (* prefix disagree *)
- s
+ (* let rec diffq phi s t =
+ * match view s , view t with
+ * | Empty , _ -> s
+ * | _ , Empty -> s
+ * | Lf(i,x) , Lf(j,y) ->
+ * if K.equal i j
+ * then lfq phi i x y s t
+ * else s
+ * | Lf(i,x) , Br _ ->
+ * (match occur i t with None -> s | Some y -> lfq phi i x y s t)
+ * | Br _ , Lf(j,y) -> change (fun j y x -> match x with
+ * | None -> None
+ * | Some x -> phi j x y) j y s
+ * | Br(p,s0,s1) , Br(q,t0,t1) ->
+ * if p == q then
+ * (\* prefixes agree *\)
+ * let t0' = (diffq phi s0 t0) in
+ * let t1' = (diffq phi s1 t1) in
+ * glue01 t0' t1' s0 s1 s
+ * else if included_prefix p q then
+ * (\* q contains p. *\)
+ * if zero_bit q p
+ * then (\* t has bit m = 0 => t is inside s0 *\)
+ * let s0' = (diffq phi s0 t) in
+ * glue0 s0' s0 s1 s
+ * else (\* t has bit m = 1 => t is inside s1 *\)
+ * let s1' = (diffq phi s1 t) in
+ * glue1 s1' s0 s1 s
+ * else if included_prefix q p then
+ * (\* p contains q. *\)
+ * if zero_bit p q
+ * then diffq phi s t0 (\* s has bit n = 0 => s is inside t0 *\)
+ * else diffq phi s t1 (\* t has bit n = 1 => s is inside t1 *\)
+ * else
+ * (\* prefix disagree *\)
+ * s *)
(* good sharing with s *)
let rec diff :
@@ -1058,119 +1053,119 @@ module Make(K:Map_intf.TaggedEqualType) :
(* --- Iter Kernel --- *)
(* ---------------------------------------------------------------------- *)
- let rec iterk phi s t =
- match view s , view t with
- | Empty , _ | _ , Empty -> ()
- | Lf(i,x) , Lf(j,y) -> if K.equal i j then phi i x y
- | Lf(i,x) , Br _ ->
- (match occur i t with None -> () | Some y -> phi i x y)
- | Br _ , Lf(j,y) ->
- (match occur j s with None -> () | Some x -> phi j x y)
- | Br(p,s0,s1) , Br(q,t0,t1) ->
- if p == q then
- (* prefixes agree *)
- (iterk phi s0 t0 ; iterk phi s1 t1)
- else if included_prefix p q then
- (* q contains p. Intersect t with a subtree of s *)
- if zero_bit q p
- then iterk phi s0 t (* t has bit m = 0 => t is inside s0 *)
- else iterk phi s1 t (* t has bit m = 1 => t is inside s1 *)
- else if included_prefix q p then
- (* p contains q. Intersect s with a subtree of t *)
- if zero_bit p q
- then iterk phi s t0 (* s has bit n = 0 => s is inside t0 *)
- else iterk phi s t1 (* t has bit n = 1 => s is inside t1 *)
- else
- (* prefix disagree *)
- ()
+ (* let rec iterk phi s t =
+ * match view s , view t with
+ * | Empty , _ | _ , Empty -> ()
+ * | Lf(i,x) , Lf(j,y) -> if K.equal i j then phi i x y
+ * | Lf(i,x) , Br _ ->
+ * (match occur i t with None -> () | Some y -> phi i x y)
+ * | Br _ , Lf(j,y) ->
+ * (match occur j s with None -> () | Some x -> phi j x y)
+ * | Br(p,s0,s1) , Br(q,t0,t1) ->
+ * if p == q then
+ * (\* prefixes agree *\)
+ * (iterk phi s0 t0 ; iterk phi s1 t1)
+ * else if included_prefix p q then
+ * (\* q contains p. Intersect t with a subtree of s *\)
+ * if zero_bit q p
+ * then iterk phi s0 t (\* t has bit m = 0 => t is inside s0 *\)
+ * else iterk phi s1 t (\* t has bit m = 1 => t is inside s1 *\)
+ * else if included_prefix q p then
+ * (\* p contains q. Intersect s with a subtree of t *\)
+ * if zero_bit p q
+ * then iterk phi s t0 (\* s has bit n = 0 => s is inside t0 *\)
+ * else iterk phi s t1 (\* t has bit n = 1 => s is inside t1 *\)
+ * else
+ * (\* prefix disagree *\)
+ * () *)
(* ---------------------------------------------------------------------- *)
(* --- Iter2 --- *)
(* ---------------------------------------------------------------------- *)
- let iter21 phi s = iteri (fun i x -> phi i (Some x) None) s
- let iter22 phi t = iteri (fun j y -> phi j None (Some y)) t
-
- let rec iter2 phi s t =
- match view s , view t with
- | Empty , _ -> iter22 phi t
- | _ , Empty -> iter21 phi s
- | Lf(i,x) , Lf(j,y) ->
- if K.equal i j then phi i (Some x) (Some y)
- else ( phi i (Some x) None ; phi j None (Some y) )
-
- | Lf(i,x) , Br(q,t0,t1) ->
- if match_prefix (K.tag i) q then
- (* leaf i is in tree t *)
- if zero_bit (K.tag i) q
- then (iter2 phi s t0 ; iter22 phi t1) (* s=i is in t0 *)
- else (iter22 phi t0 ; iter2 phi s t1) (* s=i is in t1 *)
- else
- (* leaf i does not appear in t *)
- (phi i (Some x) None ; iter22 phi t)
-
- | Br(p,s0,s1) , Lf(j,y) ->
- if match_prefix (K.tag j) p then
- (* leaf j is in tree s *)
- if zero_bit (K.tag j) p
- then (iter2 phi s0 t ; iter21 phi s1) (* t=j is in s0 *)
- else (iter21 phi s0 ; iter2 phi s1 t) (* t=j is in s1 *)
- else
- (* leaf j does not appear in s *)
- (iter21 phi s ; phi j None (Some y))
-
- | Br(p,s0,s1) , Br(q,t0,t1) ->
- if p == q then
- (* prefixes agree *)
- (iter2 phi s0 t0 ; iter2 phi s1 t1)
- else if included_prefix p q then
- (* q contains p. Merge t with a subtree of s *)
- if zero_bit q p
- then (* t has bit m = 0 => t is inside s0 *)
- (iter2 phi s0 t ; iter21 phi s1)
- else (* t has bit m = 1 => t is inside s1 *)
- (iter21 phi s0 ; iter2 phi s1 t)
- else if included_prefix q p then
- (* p contains q. Merge s with a subtree of t *)
- if zero_bit p q
- then (* s has bit n = 0 => s is inside t0 *)
- (iter2 phi s t0 ; iter22 phi t1)
- else (* s has bit n = 1 => s is inside t1 *)
- (iter22 phi t0 ; iter2 phi s t1)
- else
- (iter21 phi s ; iter22 phi t)
+ (* let iter21 phi s = iteri (fun i x -> phi i (Some x) None) s *)
+ (* let iter22 phi t = iteri (fun j y -> phi j None (Some y)) t *)
+
+ (* let rec iter2 phi s t =
+ * match view s , view t with
+ * | Empty , _ -> iter22 phi t
+ * | _ , Empty -> iter21 phi s
+ * | Lf(i,x) , Lf(j,y) ->
+ * if K.equal i j then phi i (Some x) (Some y)
+ * else ( phi i (Some x) None ; phi j None (Some y) )
+ *
+ * | Lf(i,x) , Br(q,t0,t1) ->
+ * if match_prefix (K.tag i) q then
+ * (\* leaf i is in tree t *\)
+ * if zero_bit (K.tag i) q
+ * then (iter2 phi s t0 ; iter22 phi t1) (\* s=i is in t0 *\)
+ * else (iter22 phi t0 ; iter2 phi s t1) (\* s=i is in t1 *\)
+ * else
+ * (\* leaf i does not appear in t *\)
+ * (phi i (Some x) None ; iter22 phi t)
+ *
+ * | Br(p,s0,s1) , Lf(j,y) ->
+ * if match_prefix (K.tag j) p then
+ * (\* leaf j is in tree s *\)
+ * if zero_bit (K.tag j) p
+ * then (iter2 phi s0 t ; iter21 phi s1) (\* t=j is in s0 *\)
+ * else (iter21 phi s0 ; iter2 phi s1 t) (\* t=j is in s1 *\)
+ * else
+ * (\* leaf j does not appear in s *\)
+ * (iter21 phi s ; phi j None (Some y))
+ *
+ * | Br(p,s0,s1) , Br(q,t0,t1) ->
+ * if p == q then
+ * (\* prefixes agree *\)
+ * (iter2 phi s0 t0 ; iter2 phi s1 t1)
+ * else if included_prefix p q then
+ * (\* q contains p. Merge t with a subtree of s *\)
+ * if zero_bit q p
+ * then (\* t has bit m = 0 => t is inside s0 *\)
+ * (iter2 phi s0 t ; iter21 phi s1)
+ * else (\* t has bit m = 1 => t is inside s1 *\)
+ * (iter21 phi s0 ; iter2 phi s1 t)
+ * else if included_prefix q p then
+ * (\* p contains q. Merge s with a subtree of t *\)
+ * if zero_bit p q
+ * then (\* s has bit n = 0 => s is inside t0 *\)
+ * (iter2 phi s t0 ; iter22 phi t1)
+ * else (\* s has bit n = 1 => s is inside t1 *\)
+ * (iter22 phi t0 ; iter2 phi s t1)
+ * else
+ * (iter21 phi s ; iter22 phi t) *)
(* ---------------------------------------------------------------------- *)
(* --- Intersects --- *)
(* ---------------------------------------------------------------------- *)
(** TODO seems wrong *)
- let rec intersectf phi s t =
- match view s , view t with
- | Empty , _ -> false
- | _ , Empty -> false
- | Lf(i,x) , Lf(j,y) -> if K.equal i j then phi i x y else false
- | Lf(i,x) , Br _ -> (match occur i t with None -> false
- | Some y -> phi i x y)
- | Br _ , Lf(j,y) -> (match occur j s with None -> false
- | Some x -> phi j x y)
- | Br(p,s0,s1) , Br(q,t0,t1) ->
- if p == q then
- (* prefixes agree *)
- (intersectf phi s0 t0) || (intersectf phi s1 t1)
- else if included_prefix p q then
- (* q contains p. Intersect t with a subtree of s *)
- if zero_bit q p
- then intersectf phi s0 t (* t has bit m = 0 => t is inside s0 *)
- else intersectf phi s1 t (* t has bit m = 1 => t is inside s1 *)
- else if included_prefix q p then
- (* p contains q. Intersect s with a subtree of t *)
- if zero_bit p q
- then intersectf phi s t0 (* s has bit n = 0 => s is inside t0 *)
- else intersectf phi s t1 (* t has bit n = 1 => s is inside t1 *)
- else
- (* prefix disagree *)
- false
+ (* let rec intersectf phi s t =
+ * match view s , view t with
+ * | Empty , _ -> false
+ * | _ , Empty -> false
+ * | Lf(i,x) , Lf(j,y) -> if K.equal i j then phi i x y else false
+ * | Lf(i,x) , Br _ -> (match occur i t with None -> false
+ * | Some y -> phi i x y)
+ * | Br _ , Lf(j,y) -> (match occur j s with None -> false
+ * | Some x -> phi j x y)
+ * | Br(p,s0,s1) , Br(q,t0,t1) ->
+ * if p == q then
+ * (\* prefixes agree *\)
+ * (intersectf phi s0 t0) || (intersectf phi s1 t1)
+ * else if included_prefix p q then
+ * (\* q contains p. Intersect t with a subtree of s *\)
+ * if zero_bit q p
+ * then intersectf phi s0 t (\* t has bit m = 0 => t is inside s0 *\)
+ * else intersectf phi s1 t (\* t has bit m = 1 => t is inside s1 *\)
+ * else if included_prefix q p then
+ * (\* p contains q. Intersect s with a subtree of t *\)
+ * if zero_bit p q
+ * then intersectf phi s t0 (\* s has bit n = 0 => s is inside t0 *\)
+ * else intersectf phi s t1 (\* t has bit n = 1 => s is inside t1 *\)
+ * else
+ * (\* prefix disagree *\)
+ * false *)
let rec disjoint phi s t =
match view s , view t with
@@ -1337,8 +1332,8 @@ module Make(K:Map_intf.TaggedEqualType) :
(* prefix disagree *)
false
- let subset = subsetf
- let subsetk s t = subsetf (fun _i _x _y -> true) s t
+ (* let subset = subsetf
+ * let subsetk s t = subsetf (fun _i _x _y -> true) s t *)
let submap = subsetf
(* ---------------------------------------------------------------------- *)
@@ -1671,8 +1666,8 @@ module Make(K:Map_intf.TaggedEqualType) :
| Lf of K.t * 'a
| Br of int * 'a t * 'a t
- (** implemntation without obj bust with copy of the next function *)
- let view_ : 'a t -> 'a view = function
+ (** implementation without obj but with copy of the next function *)
+ let _view_ : 'a t -> 'a view = function
| Empty -> Empty
| Lf(k,v,_) -> Lf(k,v)
| Br(i,t1,t2,_) -> Br(i,t1,t2)
diff --git a/src_colibri2/popop_lib/popop_stdlib.ml b/src_colibri2/popop_lib/popop_stdlib.ml
index 74bfc53b814c86111713799587f50679d834e398..f7701f5154de40ddd74850e9eb0f6527d973e2d4 100644
--- a/src_colibri2/popop_lib/popop_stdlib.ml
+++ b/src_colibri2/popop_lib/popop_stdlib.ml
@@ -50,7 +50,6 @@ struct
include T
let hash_fold_t state t = Base.Hash.fold_int state (X.tag t)
let sexp_of_t = sexp_of_t_of_pp pp
- let tag = X.tag
module MGen = Intmap.Make(struct
include X
let equal ts1 ts2 = X.tag ts1 == X.tag ts2
@@ -103,7 +102,6 @@ end
module Int = struct
type t = int
- let compare (x : int) (y : int) = Stdlib.compare x y
let equal (x : int) y = x = y
let hash (x : int) = x
let tag x = x
diff --git a/src_colibri2/solver/dune b/src_colibri2/solver/dune
index 1f81076c7215f68f1ad55c0ed2021e63ddf150bb..f8ee1077ed96d252df3ee08be3085b32a63efaee 100644
--- a/src_colibri2/solver/dune
+++ b/src_colibri2/solver/dune
@@ -7,7 +7,7 @@
dolmen_type)
(preprocess
(pps ppx_deriving.std))
- (flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
+ (flags :standard -w +a-4-42-44-48-50-58-60-40-9@8 -color always -open
Colibri2_stdlib -open Colibri2_core)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index ae30079caf52c3ae6828cf6cb735aae7caa85613..35480c5aacb34ce28875d98435a7708c1c2fb4c8 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -52,9 +52,6 @@ module Att = struct
type prio = float
type db = float Node.H.t
- let get_prio db n =
- Node.H.find_def db 0. n
-
let le (x:t) (xp:float) (y:t) (yp:float) =
match x, y with
| Decision (x,_), Decision (y,_) ->
@@ -98,8 +95,6 @@ type t =
}
(** To treat in the reverse order *)
-let get_t t = t.solver_state
-
let print_level fmt t =
let nb_dec =
Prio.fold (fun acc x _ -> match x with Att.Decision _ -> acc + 1)
@@ -160,11 +155,6 @@ let pop_to t prev =
Debug.dprintf2 debug_pushpop "[Scheduler] pop to %a"
print_level t
-let update_prio t chogen =
- Node.H.change (function
- | None -> Some (!(t.var_inc))
- | Some i -> Some (i +. (!(t.var_inc)))) t.decprio chogen
-
let new_delayed =
let daemon_count = ref (-1) in
let dec_count = ref (-1) in
@@ -410,12 +400,6 @@ let get_delayed t =
t.delayed <- Some d;
d
-let flush_delayed t =
- match t.delayed with
- | None -> ()
- | Some d ->
- t.delayed <- Some (flush t d)
-
let stop t d =
let d = flush t d in
Egraph.Backtrackable.delayed_stop d;
diff --git a/src_colibri2/stdlib/comp_keys.ml b/src_colibri2/stdlib/comp_keys.ml
index 619d2c43d09760a0003f5ec6dfc29c116d18d138..22c2d756a0f92bac88eb82b040e5640f3febbe04 100644
--- a/src_colibri2/stdlib/comp_keys.ml
+++ b/src_colibri2/stdlib/comp_keys.ml
@@ -160,12 +160,10 @@ module Make_key(X:sig end): Key = struct
type 'a key = 'a VH.key
type t = unit VH.t
let create = VH.create
- let size = VH.size
let get = VH.get
let get_def = VH.get_def
let set = VH.set
let is_uninitialized = VH.is_uninitialized
- let inc_size = VH.inc_size
type iter_initialized = { iter : 'a. 'a -> unit; }
type iter_initializedi = { iteri : 'a. 'a key -> 'a -> unit; }
let iter_initializedi ({iteri}:iter_initializedi) =
@@ -234,9 +232,6 @@ module Make_key(X:sig end): Key = struct
end};
!well_initialized
- let is_registered dom =
- V.is_uninitialized registry dom
-
let get k =
check_is_registered k;
V.get registry k
@@ -311,7 +306,6 @@ module Make_key2(X:sig end) : Key2 = struct
let pp fmt x = K.pp fmt x
let equal = K.equal
let hash x = K.hash x
- let key x = x
type iter = {iter : 'k 'd. ('k,'d) t -> unit}
let iter f = K.iter f.iter
@@ -385,9 +379,6 @@ module Make_key2(X:sig end) : Key2 = struct
end};
!well_initialized
- let is_registered dom =
- V.is_uninitialized registry dom
-
let get k =
check_is_registered k;
V.get registry k
diff --git a/src_colibri2/stdlib/dune b/src_colibri2/stdlib/dune
index 59f1efce1f65cdaac1bed2d6b29999bd9b7c0d29..c5c2832adcc532e8a9576b1fa0b733a5e63e803f 100644
--- a/src_colibri2/stdlib/dune
+++ b/src_colibri2/stdlib/dune
@@ -5,7 +5,7 @@
(libraries zarith containers colibri2_popop_lib colibrics_lib fmt)
(preprocess
(pps ppx_optcomp ppx_deriving.std ppx_hash))
- (flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
+ (flags :standard -w +a-4-42-44-48-50-58-60-40-9@8 -color always -open
Containers)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src_colibri2/stdlib/keys.ml b/src_colibri2/stdlib/keys.ml
index dfc1c0624a6f4eb475412cc91f9d7e621908102a..b6f03cf5364bab65a36a13cc959cade8e5534771 100644
--- a/src_colibri2/stdlib/keys.ml
+++ b/src_colibri2/stdlib/keys.ml
@@ -140,9 +140,6 @@ module Make_key(X:sig end) = struct
end};
!well_initialized
- let is_registered dom =
- V.is_uninitialized registry dom
-
let get k =
check_is_registered k;
V.get registry k
@@ -168,7 +165,6 @@ module Make_key2(X:sig end) : Key2 = struct
let pp fmt x = String.pp fmt x.name
let equal a b = a.id = b.id
- let compare x y = compare x.id y.id
let hash x = x.id
let tag = hash
let name x = x.name
@@ -255,9 +251,6 @@ module Make_key2(X:sig end) : Key2 = struct
end};
!well_initialized
- let is_registered dom =
- V.is_uninitialized registry dom
-
let get k =
check_is_registered k;
V.get registry k
diff --git a/src_colibri2/stdlib/wto.ml b/src_colibri2/stdlib/wto.ml
index 09fa2038d92a67192ce4d693db9a34badfc859dd..22ca87a36d00f3f924ef42936977913595e816f1 100644
--- a/src_colibri2/stdlib/wto.ml
+++ b/src_colibri2/stdlib/wto.ml
@@ -92,7 +92,6 @@ 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
diff --git a/src_colibri2/stdlib/wto.mli b/src_colibri2/stdlib/wto.mli
index d3e6ad31ff95de6db0c8a4256612cf91cf14b7a2..c5f3939c7ea8c37bbed7eb629b120be749cabaf3 100644
--- a/src_colibri2/stdlib/wto.mli
+++ b/src_colibri2/stdlib/wto.mli
@@ -50,7 +50,6 @@ 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
diff --git a/src_colibri2/tests/dune b/src_colibri2/tests/dune
index e0e390190557c0680e6ddee74ce6037013f4a07c..2cb73042e8b678970b5b3fcfbe400e54af3efdec 100644
--- a/src_colibri2/tests/dune
+++ b/src_colibri2/tests/dune
@@ -3,7 +3,7 @@
(name tests)
(libraries containers colibri2.core colibri2.theories.bool
colibri2.theories.LRA colibri2.theories.quantifiers ounit2 colibri2.solver colibri2.stdlib)
- (flags :standard -w +a-4-42-44-48-50-58-32-60-9@8 -color always)
+ (flags :standard -w +a-4-42-44-48-50-58-60-9@8 -color always)
(ocamlopt_flags :standard -O3 -unbox-closures -unbox-closures-factor 20))
(rule
diff --git a/src_colibri2/tests/tests_LRA.ml b/src_colibri2/tests/tests_LRA.ml
index 16087451d9950dcb21c7806c277637e0552fd791..2db0f17032a4d6a52c94d7c1c982dd69464e01c3 100644
--- a/src_colibri2/tests/tests_LRA.ml
+++ b/src_colibri2/tests/tests_LRA.ml
@@ -30,8 +30,6 @@ open Colibri2_stdlib
let theories = [Boolean.th_register; Equality.th_register;
Colibri2_theories_quantifiers.Uninterp.th_register; LRA.th_register]
-let ($$) f x = f x
-
let run = Scheduler.run_exn ~nodec:() ~theories
let run_dec = Scheduler.run_exn ?nodec:None ~theories
let ($$) f x = f x