From 1944788f912fc628caa328df045d096180cb52f3 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 26 Mar 2024 19:02:18 +0100 Subject: [PATCH] Refactoring `Enum_rel` using domains on class representatives only This PR refactors the `Enum` relations in order to use a proper type for the domains of enum semantic values. Now, we only store domains for class representatives and I believe that the new implementation is simpler to understand and to maintain. I don't use the functor `Domains_make` of `Rel_utils` as domain's propagations performed in `Enum_rel` are much simpler than the propagations in the BV theory. --- src/lib/reasoners/bitv_rel.ml | 5 +- src/lib/reasoners/enum_rel.ml | 461 ++++++++++++++++----------------- src/lib/reasoners/rel_utils.ml | 150 ++++++++++- 3 files changed, 367 insertions(+), 249 deletions(-) diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index 6b41b21462..778491e804 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/src/lib/reasoners/bitv_rel.ml @@ -77,7 +77,7 @@ let is_bv_ty = function let is_bv_r r = is_bv_ty @@ X.type_info r -module Domain : Rel_utils.Domain with type t = Bitlist.t = struct +module Domain = struct (* Note: these functions are not in [Bitlist] proper in order to avoid a (direct) dependency from [Bitlist] to the [Shostak] module. *) @@ -124,7 +124,8 @@ module Domain : Rel_utils.Domain with type t = Bitlist.t = struct | Ext (r, _r_size, i, j) -> extract (map_signed f r acc) i j ) empty (Shostak.Bitv.embed r) - let unknown = function + let unknown r = + match X.type_info r with | Ty.Tbitv n -> unknown n Ex.empty | _ -> (* Only bit-vector values can have bitlist domains. *) diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml index 391aa95ea2..f376e3ce77 100644 --- a/src/lib/reasoners/enum_rel.ml +++ b/src/lib/reasoners/enum_rel.ml @@ -28,32 +28,81 @@ (* *) (**************************************************************************) -module A = Xliteral module L = List -module Hs = Hstring +module X = Shostak.Combine +module Ex = Explanation +module MX = Shostak.MXH +module SX = Shostak.SXH +module HSS = Set.Make (Hstring) +module LR = Uf.LX +module Th = Shostak.Enum let timer = Timers.M_Sum -type 'a abstract = 'a Enum.abstract = - | Cons of Hs.t * Ty.t - | Alien of 'a +module Domain = struct + type t = { + constrs : HSS.t; + ex : Ex.t; + } -module X = Shostak.Combine -module Sh = Shostak.Enum + exception Inconsistent of Ex.t -module Ex = Explanation + let[@inline always] cardinal { constrs; _ } = HSS.cardinal constrs -module MX = Shostak.MXH -module HSS = Set.Make (struct type t=Hs.t let compare = Hs.compare end) + let[@inline always] choose { constrs; _ } = HSS.choose constrs -module LR = Uf.LX + let domain ~constrs ex = + if HSS.is_empty constrs then + raise_notrace @@ Inconsistent ex + else + { constrs; ex } + + let unknown r = + match Th.embed r with + | Cons (c, _) -> + domain ~constrs:(HSS.singleton c) Ex.empty + | _ -> + match X.type_info r with + | Ty.Tsum (_, constrs) -> + (* Return the list of all the constructors of the type of [r]. *) + let constrs = HSS.of_list constrs in + assert (not @@ HSS.is_empty constrs); + { constrs; ex = Ex.empty } + | _ -> + (* Only Enum values can have a domain. This case can happen since we + don't dispatch the literals processed in [assume] by their types in + the Relation module. *) + invalid_arg "unknown" + + let equal d1 d2 = HSS.equal d1.constrs d2.constrs + + let pp ppf d = + Fmt.pf ppf "%a" + Fmt.(iter ~sep:comma HSS.iter Hstring.print) d.constrs; + if Options.(get_verbose () || get_unsat_core ()) then + Fmt.pf ppf " %a" (Fmt.box Ex.print) d.ex + + let intersect ~ex d1 d2 = + let constrs = HSS.inter d1.constrs d2.constrs in + let ex = ex |> Ex.union d1.ex |> Ex.union d2.ex in + domain ~constrs ex + + let remove ~ex c d = + let constrs = HSS.remove c d.constrs in + let ex = Ex.union ex d.ex in + domain ~constrs ex + + let fold_leaves _f _rr _d _ = assert false + + let map_leaves _f _rr _ = assert false +end + +module Domains = Rel_utils.SimpleDomains_make (Domain) type t = { - (* TODO: rename the field domains to be consistent with the ADT theory. *) - mx : (HSS.t * Ex.t) MX.t; - (* Map of uninterpreted enum semantic values to domains of their possible - values. The explanation justifies that any value assigned to the semantic - value has to lie in the domain. *) + domains : Domains.t; + (* Map of class representatives of enum semantic values to their + domains. *) classes : Expr.Set.t list; (* State of the union-find represented by all its equivalence classes. @@ -68,265 +117,203 @@ type t = { [Options.get_max_split ()]. *) } -let empty classes = { - mx = MX.empty; - classes = classes; - size_splits = Numbers.Q.one -} - (*BISECT-IGNORE-BEGIN*) module Debug = struct - open Printer - - let assume bol r1 r2 = + let assume l = if Options.get_debug_sum () then - print_dbg - ~module_name:"Enum_rel" ~function_name:"assume" - "we assume %a %s %a" - X.print r1 (if bol then "=" else "<>") X.print r2 - - let print_env env = - if Options.get_debug_sum () then begin - Printer.print_dbg ~flushed:false - ~module_name:"Enum_rel" ~function_name:"print_env" - "@[--SUM env ---------------------------------@ "; - MX.iter - (fun r (hss, ex) -> - Printer.print_dbg ~flushed:false ~header:false - "%a ::= " X.print r; - begin - match HSS.elements hss with - [] -> () - | hs :: l -> - Printer.print_dbg ~flushed:false ~header:false - " %s" (Hs.view hs); - L.iter (fun hs -> - Printer.print_dbg ~flushed:false ~header:false - " | %s" (Hs.view hs)) l - end; - Printer.print_dbg ~flushed:false ~header:false - " : %a@ " Ex.print ex; - ) env.mx; - Printer.print_dbg ~header:false - "@ -------------------------------------------"; - end - - let case_split r r' = + Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"assume" + "assume %a" + (Xliteral.print_view X.print) l + + let case_split r1 r2 = if Options.get_debug_sum () then - Printer.print_dbg - ~module_name:"Enum_rel" ~function_name:"case_split" - "%a = %a" X.print r X.print r' + Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"case_split" + "%a = %a" X.print r1 X.print r2 let no_case_split () = if Options.get_debug_sum () then - Printer.print_dbg - ~module_name:"Enum_rel" ~function_name:"no_case_split" - "sum: nothing" + Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"case_split" + "nothing" let add r = if Options.get_debug_sum () then - Printer.print_dbg - ~module_name:"Enum_rel" ~function_name:"add" + Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"add" "%a" X.print r + let pp_env env = + if Options.get_debug_sum () then + Printer.print_dbg ~module_name:"Enum_rel" + "The environment before assuming:@ @[%a@]" Domains.pp env.domains end (*BISECT-IGNORE-END*) -(* Return the list of all the constructors of the type of [r]. *) -let values_of r = - match X.type_info r with - | Ty.Tsum (_,l) -> - Some (List.fold_left (fun st hs -> HSS.add hs st) HSS.empty l) - | _ -> - (* This case can happen since we don't dispatch the literals - processed in [assume] by their types in the Relation module. *) - None - -(* Update the domains of the semantic values [sm1] and [sm2] according to - the disequality [sm1 <> sm2]. More precisely, if one of these semantic - values is a constructor, we remove it from the domain of the other one. - - In any case, we produce an equality if the domain of one of these semantic - values becomes a singleton. - - @raise Ex.Inconsistent if the disequality is inconsistent with the - current environment [env]. *) -let add_diseq hss sm1 sm2 dep env eqs = - match sm1, sm2 with - | Alien r , Cons(h,ty) - | Cons (h,ty), Alien r -> - let enum, ex = try MX.find r env.mx with Not_found -> hss, Ex.empty in - let enum = HSS.remove h enum in - let ex = Ex.union ex dep in - if HSS.is_empty enum then raise (Ex.Inconsistent (ex, env.classes)) - else - let env = { env with mx = MX.add r (enum, ex) env.mx } in - if HSS.cardinal enum = 1 then - let h' = HSS.choose enum in - env, - (Literal.LSem (LR.mkv_eq r (Sh.is_mine (Cons(h',ty)))), - ex, Th_util.Other)::eqs - else env, eqs - - | Alien r1, Alien r2 -> - let enum1,ex1= try MX.find r1 env.mx with Not_found -> hss,Ex.empty in - let enum2,ex2= try MX.find r2 env.mx with Not_found -> hss,Ex.empty in - - let eqs = - if HSS.cardinal enum1 = 1 then - let ex = Ex.union dep ex1 in - let h' = HSS.choose enum1 in - let ty = X.type_info r1 in - (Literal.LSem (LR.mkv_eq r1 (Sh.is_mine (Cons(h',ty)))), - ex, Th_util.Other)::eqs - else eqs - in - let eqs = - if HSS.cardinal enum2 = 1 then - let ex = Ex.union dep ex2 in - let h' = HSS.choose enum2 in - let ty = X.type_info r2 in - (Literal.LSem (LR.mkv_eq r2 (Sh.is_mine (Cons(h',ty)))), - ex, Th_util.Other)::eqs - else eqs - in - env, eqs - - | _ -> env, eqs - -(* Update the domains of the semantic values [sm1] and [sm2] according to - the equation [sm1 = sm2]. More precisely, we replace their domains by - the intersection of these domains. - - @raise Ex.Inconsistent if the domains of [sm1] and [sm2] are disjoint. *) -let add_eq hss sm1 sm2 dep env eqs = - match sm1, sm2 with - | Alien r, Cons(h,_) - | Cons (h,_), Alien r -> - let enum, ex = try MX.find r env.mx with Not_found -> hss, Ex.empty in - let ex = Ex.union ex dep in - if not (HSS.mem h enum) then raise (Ex.Inconsistent (ex, env.classes)); - (* We don't need to produce a new equality as we are already processing - it. *) - {env with mx = MX.add r (HSS.singleton h, ex) env.mx} , eqs - - | Alien r1, Alien r2 -> - let enum1,ex1 = - try MX.find r1 env.mx with Not_found -> hss, Ex.empty in - let enum2,ex2 = - try MX.find r2 env.mx with Not_found -> hss, Ex.empty in - let ex = Ex.union dep (Ex.union ex1 ex2) in - let diff = HSS.inter enum1 enum2 in - if HSS.is_empty diff then raise (Ex.Inconsistent (ex, env.classes)); - let mx = MX.add r1 (diff, ex) env.mx in - let env = {env with mx = MX.add r2 (diff, ex) mx } in - - (* We produce an equality if the domain of these semantic values becomes - a singleton. *) - if HSS.cardinal diff = 1 then - let h' = HSS.choose diff in - let ty = X.type_info r1 in - env, (Literal.LSem (LR.mkv_eq r1 (Sh.is_mine (Cons(h',ty)))), - ex, Th_util.Other)::eqs - else env, eqs - - | _ -> env, eqs +let empty classes = { + domains = Domains.empty; + classes = classes; + size_splits = Numbers.Q.one +} (* Update the counter of case-split size in [env]. *) let count_splits env la = let nb = List.fold_left - (fun nb (_,_,_,i) -> + (fun nb (_, _, _, i) -> match i with | Th_util.CS (Th_util.Th_sum, n) -> Numbers.Q.mult nb n | _ -> nb - )env.size_splits la + ) env.size_splits la in {env with size_splits = nb} -(* Add the uninterpreted semantic value [r] to the environment [env] with - all the constructors of its type as domain. *) -let add_aux env r = - Debug.add r; - match Sh.embed r, values_of r with - | Alien r, Some hss -> - if MX.mem r env.mx then env else - { env with mx = MX.add r (hss, Ex.empty) env.mx } - | _ -> env +let update_domain rr nd env = + { env with domains = Domains.update rr nd env.domains } + +(* Update the domains of the semantic values [r1] and [r2] according to + the substitution `r1 |-> r2`. + + @raise Domain.Inconsistent if this substitution is inconsistent with + the current environment [env]. *) +let assume_subst ~ex r1 r2 env = + { env with domains = Domains.subst ~ex r1 r2 env.domains } + +(* Update the domains of the semantic values [r1] and [r2] according to the + disequality [r1 <> r2]. + + This function alone isn't sufficient to produce a complete decision + procedure for the Enum theory. For instance, let's assume we have three + semantic values [r1], [r2] and [r3] whose the domain is `{C1, C2}`. It's + clear that `(distinct r1 r2 r3)` is unsatisfiable but we haven't enough + information to discover this contradiction. + + Now, if we produce a case-split for one of these semantic values, + we reach a contradiction for each choice and so our implementation got + a complete decision procedure (assuming we have fuel to produce enough + case-splits). + + @raise Domain.Inconsistent if the disequality is inconsistent with + the current environment [env]. *) +let assume_distinct ~ex r1 r2 env = + let d1 = Domains.get r1 env.domains in + let d2 = Domains.get r2 env.domains in + let env = + if Domain.cardinal d1 = 1 then + let c = Domain.choose d1 in + let nd = Domain.remove ~ex c d2 in + update_domain r2 nd env + else + env + in + if Domain.cardinal d2 = 1 then + let c = Domain.choose d2 in + let nd = Domain.remove ~ex c d1 in + update_domain r1 nd env + else + env + +let is_enum r = + match X.type_info r with + | Ty.Tsum _ -> true + | _ -> false -(* Needed for models generation because fresh terms are not added with function - add. *) -let add_rec env r = List.fold_left add_aux env (X.leaves r) +(* Needed for models generation because fresh terms are not added with the + function add. *) +let add r uf env = + match X.type_info r with + | Ty.Tsum _ -> + Debug.add r; + let rr, _ = Uf.find_r uf r in + { env with domains = Domains.add rr env.domains } + | _ -> + env + +let add_rec r uf env = + List.fold_left (fun env leaf -> add leaf uf env) env (X.leaves r) + +let add env uf r _t = add r uf env, [] + +let assume_literals la uf env = + List.fold_left + (fun env lit -> + let open Xliteral in + match lit with + | Eq (r1, r2) as l, _, ex, Th_util.Subst when is_enum r1 -> + Debug.assume l; + let env = add_rec r1 uf env in + let env = add_rec r2 uf env in + assume_subst ~ex r1 r2 env + + | Distinct (false, [r1; r2]) as l, _, ex, _ when is_enum r2 -> + Debug.assume l; + let env = add_rec r1 uf env in + let env = add_rec r2 uf env in + assume_distinct ~ex r1 r2 env + + | _ -> + (* We ignore [Eq] literals that aren't substitutions as the propagation + of such equalities will produce substitutions later. + More precisely, the equation [Eq (r1, r2)] will produce two + substitutions: + [Eq (r1, rr)] and [Eq (r2, rr)] + where [rr] is the new class representative. *) + env + ) env la + +let propagate_domains env = + Domains.propagate + (fun eqs rr d -> + if Domain.cardinal d = 1 then + let c = Domain.choose d in + let nr = Th.is_mine (Cons (c, X.type_info rr)) in + let eq = Literal.LSem (LR.mkv_eq rr nr), d.ex, Th_util.Other in + eq :: eqs + else + eqs + ) [] env.domains let assume env uf la = + Debug.pp_env env; let env = count_splits env la in let classes = Uf.cl_extract uf in let env = { env with classes = classes } in - let aux bol r1 r2 dep env eqs = function - | None -> env, eqs - | Some hss -> - Debug.assume bol r1 r2; - if bol then - add_eq hss (Sh.embed r1) (Sh.embed r2) dep env eqs - else - add_diseq hss (Sh.embed r1) (Sh.embed r2) dep env eqs - in - Debug.print_env env; - let env, eqs = - List.fold_left - (fun (env,eqs) -> function - | A.Eq(r1,r2), _, ex, _ -> - (* needed for models generation because fresh terms are not - added with function add *) - let env = add_rec (add_rec env r1) r2 in - aux true r1 r2 ex env eqs (values_of r1) - - | A.Distinct(false, [r1;r2]), _, ex, _ -> - (* needed for models generation because fresh terms are not - added with function add *) - let env = add_rec (add_rec env r1) r2 in - aux false r1 r2 ex env eqs (values_of r1) - - | _ -> env, eqs - - ) (env,[]) la + let env = + try + assume_literals la uf env + with Domain.Inconsistent ex -> + raise_notrace (Ex.Inconsistent (ex, env.classes)) in - env, { Sig_rel.assume = eqs; remove = [] } + let assume, domains = propagate_domains env in + { env with domains }, Sig_rel.{ assume; remove = [] } -let add env _ r _ = add_aux env r, [] +let case_split_limit env n = + let m = Options.get_max_split () in + Numbers.Q.(compare (mult n env.size_splits) m) <= 0 || Numbers.Q.sign m < 0 -(* Do a case-split by choosing a value for an uninterpreted semantic value - whose domain in [env] is of minimal size. *) +(* Do a case-split by choosing a value for class representatives having of + minimal size. *) let case_split env uf ~for_model = - let acc = MX.fold - (fun r (hss, _) acc -> - let x, _ = Uf.find_r uf r in - match Sh.embed x with - | Cons _ -> - (* The equivalence class of [r] already contains a value so - we don't need to make another case-split for this semantic - value. *) - acc - | _ -> - (* We have to perform a case-split, even if the domain of [r] is - of cardinal 1 as we have to let the union-find know this - equality. *) - let sz = HSS.cardinal hss in - match acc with - | Some (n,_,_) when n <= sz -> acc - | _ -> Some (sz, r, HSS.choose hss) - ) env.mx None + let best = + Domains.fold (fun r d best -> + let rr, _ = Uf.find_r uf r in + match Th.embed rr with + | Cons _ -> + (* The equivalence class of [r] already contains a model term so + we don't need to make another case-split for this semantic + value. *) + best + | _ -> + let cd = Domain.cardinal d in + match best with + | Some (n, _, _) when n <= cd -> best + | _ -> Some (cd, r, Domain.choose d) + ) env.domains None in - match acc with - | Some (n,r,hs) -> + match best with + | Some (n, r, c) -> let n = Numbers.Q.from_int n in - if for_model || - Numbers.Q.compare - (Numbers.Q.mult n env.size_splits) (Options.get_max_split ()) <= 0 || - Numbers.Q.sign (Options.get_max_split ()) < 0 then - let r' = Sh.is_mine (Cons(hs,X.type_info r)) in - Debug.case_split r r'; - [LR.mkv_eq r r', true, Th_util.CS (Th_util.Th_sum, n)] + if for_model || case_split_limit env n then + let nr = Th.is_mine (Cons (c, X.type_info r)) in + Debug.case_split r nr; + [LR.mkv_eq r nr, true, Th_util.CS (Th_util.Th_sum, n)] else [] | None -> diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml index fb17f1528d..a40bfff3c4 100644 --- a/src/lib/reasoners/rel_utils.ml +++ b/src/lib/reasoners/rel_utils.ml @@ -214,13 +214,8 @@ module type Domain = sig exception Inconsistent of Explanation.t (** Exception raised by [intersect] when an inconsistency is detected. *) - val unknown : Ty.t -> t - (** [unknown ty] returns a full domain for values of type [t]. *) - - val add_explanation : ex:Explanation.t -> t -> t - (** [add_explanation ~ex d] adds the justification [ex] to the domain d. The - returned domain is identical to the domain of [d], only the - justifications are changed. *) + val unknown : X.r -> t + (** [unknown r] returns a full domain for values of the semantic value [r]. *) val intersect : ex:Explanation.t -> t -> t -> t (** [intersect ~ex d1 d2] returns a new domain [d] that subsumes both [d1] @@ -250,7 +245,7 @@ end module type Domains = sig type t (** The type of domain maps. A domain map maps each representative (semantic - value, of type [X.r]) to its associated domain.*) + value, of type [X.r]) to its associated domain. *) val pp : t Fmt.t (** Pretty-printer for domain maps. *) @@ -269,7 +264,7 @@ module type Domains = sig val add : X.r -> t -> t (** [add r t] adds a domain for [r] in the domain map. If [r] does not already have an associated domain, a fresh domain will be created for - [r]. *) + [r] using [Domain.unknown]. *) val get : X.r -> t -> elt (** [get r t] returns the domain currently associated with [r] in [t]. *) @@ -398,7 +393,7 @@ struct let create_domain r = Domain.map_leaves (fun r () -> - Domain.unknown (X.type_info r) + Domain.unknown r ) r () let add r t = @@ -623,6 +618,141 @@ struct ) t.Ephemeral.dirty_cache t.persistent end +(** Simplified version of [Domains_make] used by theories that perform + only one step of propagation. + + The input [Domain] doesn't need to implement [fold_leaves] or + [map_leaves]. *) +module SimpleDomains_make (Domain : Domain) : sig + type t + (** The type of simple domain maps. A domain map maps each representative + (semantic value, of type [X.r]) to its associated domain. *) + + val pp : t Fmt.t + (** Pretty-printer for domain maps. *) + + val empty : t + (** The empty domain map. *) + + type elt = Domain.t + (** The type of domains contained in the map. Each domain of type [elt] + applies to a single semantic value. *) + + exception Inconsistent of Explanation.t + (** Exception raised by [update] or [subst] when an inconsistency is + detected. *) + + val add : X.r -> t -> t + (** [add r t] adds a domain for [r] in the domain map. If [r] does not + already have an associated domain, a fresh domain will be created for + [r] using [Domain.unknown]. *) + + val get : X.r -> t -> elt + (** [get r t] returns the domain currently associated with [r] in [t]. *) + + val subst : ex:Explanation.t -> X.r -> X.r -> t -> t + (** [subst ~ex p v d] replaces all the instances of [p] with [v] in all + domains, merging the corresponding domains as appropriate. + + The explanation [ex] justifies the equality [p = v]. + + @raise Domain.Inconsistent if this causes any domain in [d] to become + empty. *) + + val update : X.r -> elt -> t -> t + (** [update r d t] replaces the domain of [r] in [t] by [d]. The + representative [r] is marked [changed] after this call. *) + + val propagate : ('a -> X.r -> elt -> 'a) -> 'a -> t -> 'a * t + (* [propagate f a t] iterates on all the changed domains of [t] since the + last call of [propagate]. The list of changed domains is flushed after + this call. *) + + val fold : (X.r -> elt -> 'a -> 'a) -> t -> 'a -> 'a + (* [fold f t a] iterates on all the domains of [t]. *) +end = struct + type elt = Domain.t + + exception Inconsistent = Domain.Inconsistent + + type t = { + domains : Domain.t MX.t; + (** Map from tracked representatives to their domain. *) + + changed : SX.t; + (** Representatives whose domain has changed since the last flush + in [propagation]. *) + } + + let pp ppf t = + Fmt.(iter_bindings ~sep:semi MX.iter + (box @@ pair ~sep:(any " ->@ ") X.print Domain.pp) + |> braces + ) + ppf t.domains + + let empty = { domains = MX.empty; changed = SX.empty } + + let internal_update r nd t = + let domains = MX.add r nd t.domains in + let changed = SX.add r t.changed in + { domains; changed } + + let add r t = + match MX.find r t.domains with + | _ -> t + | exception Not_found -> + let nd = Domain.unknown r in + internal_update r nd t + + let update r d t = + match MX.find r t.domains with + | od -> + let nd = Domain.intersect ~ex:Explanation.empty od d in + if Domain.equal od nd then + t + else + internal_update r nd t + + | exception Not_found -> + let nd = Domain.intersect ~ex:Explanation.empty (Domain.unknown r) d in + internal_update r nd t + + let get r t = + try MX.find r t.domains + with Not_found -> Domain.unknown r + + let remove r t = + let domains = MX.remove r t.domains in + let changed = SX.remove r t.changed in + { domains ; changed } + + let subst ~ex r nr t = + match MX.find r t.domains with + | d -> + let nnd = + match MX.find nr t.domains with + | nd -> Domain.intersect ~ex d nd + | exception Not_found -> d + in + let t = remove r t in + internal_update nr nnd t + + | exception Not_found -> t + + let fold f t acc = MX.fold f t.domains acc + + let propagate f acc t = + let acc = + SX.fold + (fun r acc -> + let d = get r t in + f acc r d + ) t.changed acc + in + acc, { t with changed = SX.empty } +end + (** The ['c acts] type is used to register new facts and constraints in [Constraint.simplify]. *) type 'c acts =