diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index 1adc21c4a7..153380e9ad 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -108,6 +108,12 @@ module Domain = struct
domain ~constrs ex
end
+let is_adt_ty = function
+ | Ty.Tadt _ -> true
+ | _ -> false
+
+let is_adt r = is_adt_ty (X.type_info r)
+
module Domains = struct
(** The type of simple domain maps. A domain map maps each representative
(semantic value, of type [X.r]) to its associated domain. *)
@@ -122,6 +128,8 @@ module Domains = struct
in [propagation]. *)
}
+ type _ Uf.id += Id : t Uf.id
+
let pp ppf t =
Fmt.(iter_bindings ~sep:semi MX.iter
(box @@ pair ~sep:(any " ->@ ") X.print Domain.pp)
@@ -131,6 +139,8 @@ module Domains = struct
let empty = { domains = MX.empty; changed = SX.empty }
+ let filter_ty = is_adt_ty
+
let internal_update r nd t =
let domains = MX.add r nd t.domains in
let changed = SX.add r t.changed in
@@ -148,16 +158,14 @@ module Domains = struct
Domain.unknown (X.type_info r)
let add r t =
- if MX.mem r t.domains then t
- else
- match Th.embed r with
- | Constr _ | Select _ -> t
- | Alien _ ->
- (* We have to add a default domain if the key `r` isn't in map in order
- to be sure that the case-split mechanism will attempt to choose a
- value for it. *)
- let nd = Domain.unknown (X.type_info r) in
- internal_update r nd t
+ match Th.embed r with
+ | Alien _ when not (MX.mem r t.domains) ->
+ (* We have to add a default domain if the key `r` isn't in map in order
+ to be sure that the case-split mechanism will attempt to choose a
+ value for it. *)
+ let nd = Domain.unknown (X.type_info r) in
+ internal_update r nd t
+ | Alien _ | Constr _ | Select _ -> t
(** [tighten r d t] replaces the domain of [r] in [t] by a domain [d] contains
in the current domain of [r]. The representative [r] is marked [changed]
@@ -177,6 +185,8 @@ module Domains = struct
let changed = SX.remove r t.changed in
{ domains ; changed }
+ exception Inconsistent = Domain.Inconsistent
+
(** [subst ~ex p v d] replaces all the instances of [p] with [v] in all
domains, merging the corresponding domains as appropriate.
@@ -191,7 +201,7 @@ module Domains = struct
let t = remove r t in
tighten nr nd t
- | exception Not_found -> t
+ | exception Not_found -> add nr 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
@@ -238,14 +248,6 @@ let dispatch = function
| _ -> None
type t = {
- classes : E.Set.t list;
- (* State of the union-find represented by all its equivalence classes.
- This state is kept for debugging purposes only. It is updated after
- assuming literals of the theory and returned by queries in case of
- inconsistency. *)
-
- domains : Domains.t;
-
delayed : Rel_utils.Delayed.t;
(* Set of delayed destructor applications. The computation of a destructor
application [d r] is forced if we see the tester `(_ is d) r` of the
@@ -262,13 +264,11 @@ type t = {
See the function [deduce_is_constr]. *)
}
-let empty classes = {
- classes;
- domains = Domains.empty;
+let empty uf = {
delayed = Rel_utils.Delayed.create ~is_ready dispatch;
size_splits = Numbers.Q.one;
new_terms = SE.empty;
-}
+}, Uf.Domains.add (module Domains) Domains.empty (Uf.domains uf)
(* ################################################################ *)
(*BISECT-IGNORE-BEGIN*)
@@ -282,12 +282,12 @@ module Debug = struct
~function_name:"assume"
"assume %a" LR.print (LR.make a)
- let pp_env loc env =
+ let pp_domains loc domains =
if Options.get_debug_adt () then begin
print_dbg ~flushed:false ~module_name:"Adt_rel"
"@[<v 2>--ADT env %s ---------------------------------@ " loc;
print_dbg ~flushed:false ~header:false "domains:@ %a"
- Domains.pp env.domains;
+ Domains.pp domains;
print_dbg ~header:false "---------------------"
end
@@ -327,18 +327,6 @@ let assume_th_elt t th_elt _ =
failwith "This Theory does not support theories extension"
| _ -> t
-let tighten_domain r nd env =
- { env with domains = Domains.tighten r 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 =
- let domains = Domains.subst ~ex r1 r2 env.domains in
- { env with domains }
-
(* Update the domains of the semantic values [r1] and [r2] according to the
disequality [r1 <> r2].
@@ -355,37 +343,37 @@ let assume_subst ~ex r1 r2 env =
@raise Domain.Inconsistent if the disequality is inconsistent with
the current environment [env]. *)
let assume_distinct =
- let aux ~ex r1 r2 env =
+ let aux ~ex r1 r2 domains =
match Th.embed r1 with
| Constr { c_args; _ } when List.length c_args = 0 ->
begin
- let d1 = Domains.get r1 env.domains in
- let d2 = Domains.get r2 env.domains in
+ let d1 = Domains.get r1 domains in
+ let d2 = Domains.get r2 domains in
match Domain.as_singleton d1 with
| Some (c, ex') ->
let ex = Ex.union ex ex' in
let nd = Domain.remove ~ex c d2 in
- tighten_domain r2 nd env
- | None -> env
+ Domains.tighten r2 nd domains
+ | None -> domains
end
| _ ->
(* If `d1` is a singleton domain but its constructor has a payload,
we cannot tighten the domain of `r2` because they could have
distinct payloads. *)
- env
- in fun ~ex r1 r2 env ->
- aux ~ex r1 r2 env |> aux ~ex r2 r1
+ domains
+ in fun ~ex r1 r2 domains ->
+ aux ~ex r1 r2 domains |> aux ~ex r2 r1
(* Assumes the tester `((_ is c) r)` where [r] can be a constructor
application or a uninterpreted semantic value.
@raise Domain.Inconsistent if we already know that the value of [r]
cannot be an application of the constructor [c]. *)
-let assume_is_constr ~ex r c env =
- let d1 = Domains.get r env.domains in
+let assume_is_constr ~ex r c domains =
+ let d1 = Domains.get r domains in
let d2 = Domain.singleton ~ex:Explanation.empty c in
let nd = Domain.intersect ~ex d1 d2 in
- tighten_domain r nd env
+ Domains.tighten r nd domains
(* Assume `(not ((_ is c) r))` where [r] can be a constructor application
or a uninterpreted semantic value.
@@ -394,49 +382,35 @@ let assume_is_constr ~ex r c env =
@raise Domain.Inconsistent if we already know that the value of [r] has to
be an application of the constructor [c]. *)
-let assume_not_is_constr ~ex r c env =
- let d = Domains.get r env.domains in
+let assume_not_is_constr ~ex r c domains =
+ let d = Domains.get r domains in
let nd = Domain.remove ~ex c d in
- tighten_domain r nd env
+ Domains.tighten r nd domains
-let add r uf env =
+let add r uf domains =
match X.type_info r with
| Ty.Tadt _ ->
Debug.add r;
let rr, _ = Uf.find_r uf r in
- { env with domains = Domains.add rr env.domains }
+ Domains.add rr domains
| _ ->
- env
-
-let is_adt r =
- match X.type_info r with
- | Ty.Tadt _ -> true
- | _ -> false
+ domains
-let add_rec r uf env =
- List.fold_left (fun env lf -> add lf uf env) env (X.leaves r)
+let add_rec r uf domains =
+ List.fold_left (fun env lf -> add lf uf env) domains (X.leaves r)
let add env uf r t =
if Options.get_disable_adts () then
- env, []
+ env, Uf.domains uf, []
else
- let env = add r uf env in
let delayed, eqs = Rel_utils.Delayed.add env.delayed uf r t in
- { env with delayed }, eqs
+ { env with delayed }, Uf.domains uf, eqs
-let assume_literals la uf env =
+let assume_literals la uf domains =
List.fold_left
- (fun env lit ->
+ (fun domains lit ->
let open Xliteral in
match lit with
- | Eq (r1, r2) as l, _, ex, Th_util.Subst when is_adt r1 ->
- Debug.assume l;
- (* Needed for models generation because fresh terms are not added with
- the function add. *)
- 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_adt r2 ->
Debug.assume l;
let rr1, ex1 = Uf.find_r uf r1 in
@@ -447,7 +421,7 @@ let assume_literals la uf env =
let ex = Ex.union ex1 @@ Ex.union ex2 ex in
(* Needed for models generation because fresh terms are not added with
the function add. *)
- let env = add_rec rr1 uf env in
+ let env = add_rec rr1 uf domains in
let env = add_rec rr2 uf env in
assume_distinct ~ex rr1 rr2 env
@@ -455,23 +429,16 @@ let assume_literals la uf env =
Debug.assume l;
let r, ex1 = Uf.find_r uf r in
let ex = Ex.union ex1 ex in
- assume_is_constr ~ex r c env
+ assume_is_constr ~ex r c domains
| Builtin (false, Sy.IsConstr c, [r]) as l, _, ex, _ ->
Debug.assume l;
let r, ex1 = Uf.find_r uf r in
let ex = Ex.union ex1 ex in
- assume_not_is_constr ~ex r c 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
+ assume_not_is_constr ~ex r c domains
+
+ | _ -> domains
+ ) domains la
(* For a uninterpreted semantic value [r] and [c] a constructor of the form:
(cons (d1 ty1) ... (dn tyn))
@@ -513,7 +480,7 @@ let build_constr_eq r c =
| Select _ ->
assert false
-let propagate_domains env =
+let propagate_domains new_terms domains =
Domains.propagate
(fun (eqs, new_terms) rr d ->
match Domain.as_singleton d with
@@ -527,7 +494,7 @@ let propagate_domains env =
end
| None ->
eqs, new_terms
- ) ([], env.new_terms) env.domains
+ ) ([], new_terms) domains
(* Remove duplicate literals in the list [la]. *)
let remove_redundancies la =
@@ -552,27 +519,30 @@ let count_splits env la =
) env.size_splits la
let assume env uf la =
- Debug.pp_env "before assume" env;
+ let ds = Uf.domains uf in
+ let domains = Uf.Domains.find (module Domains) ds in
+ Debug.pp_domains "before assume" domains;
(* should be done globally in CCX *)
let la = remove_redundancies la in
let delayed, result = Rel_utils.Delayed.assume env.delayed uf la in
- let env =
+ let domains =
try
- assume_literals la uf env
+ assume_literals la uf domains
with Domain.Inconsistent ex ->
- raise_notrace (Ex.Inconsistent (ex, env.classes))
+ raise_notrace (Ex.Inconsistent (ex, Uf.cl_extract uf))
in
- let (assume, new_terms), domains = propagate_domains env in
+ let (assume, new_terms), domains = propagate_domains env.new_terms domains in
let assume = List.rev_append assume result.assume in
let env = {
- delayed; domains;
- classes = Uf.cl_extract uf;
+ delayed;
size_splits = count_splits env la;
new_terms;
}
in
- Debug.pp_env "after assume" env;
- env, Sig_rel.{ assume; remove = [] }
+ Debug.pp_domains "after assume" domains;
+ env,
+ Uf.Domains.add (module Domains) domains ds,
+ Sig_rel.{ assume; remove = [] }
(* ################################################################ *)
@@ -620,13 +590,15 @@ let pick_delayed_destructor env =
(* Do a case-split by choosing a semantic value [r] and constructor [c]
for which there are delayed destructor applications and propagate the
literal [(not (_ is c) r)]. *)
-let case_split env _uf ~for_model =
+let case_split env uf ~for_model =
if Options.get_disable_adts () || not (Options.get_enable_adts_cs())
then
[]
else begin
assert (not for_model);
- if Options.get_debug_adt () then Debug.pp_env "before cs" env;
+ if Options.get_debug_adt () then
+ Debug.pp_domains "before cs"
+ (Uf.Domains.find (module Domains) (Uf.domains uf));
match pick_delayed_destructor env with
| Some (r, d) ->
if Options.get_debug_adt () then
@@ -644,24 +616,25 @@ let case_split env _uf ~for_model =
let optimizing_objective _env _uf _o = None
-let query env uf (ra, _, ex, _) =
+let query _env uf (ra, _, ex, _) =
if Options.get_disable_adts () then None
else
+ let domains = Uf.Domains.find (module Domains) (Uf.domains uf) in
try
match ra with
| Xliteral.Builtin(true, Sy.IsConstr c, [r]) ->
let rr, _ = Uf.find_r uf r in
- ignore (assume_is_constr ~ex rr c env);
+ ignore (assume_is_constr ~ex rr c domains);
None
| Xliteral.Builtin(false, Sy.IsConstr c, [r]) ->
let rr, _ = Uf.find_r uf r in
- ignore (assume_not_is_constr ~ex rr c env);
+ ignore (assume_not_is_constr ~ex rr c domains);
None
| _ ->
None
with
- | Domain.Inconsistent ex -> Some (ex, env.classes)
+ | Domain.Inconsistent ex -> Some (ex, Uf.cl_extract uf)
(* ################################################################ *)
diff --git a/src/lib/reasoners/arrays_rel.ml b/src/lib/reasoners/arrays_rel.ml
index 4866f51e45..ef418fa050 100644
--- a/src/lib/reasoners/arrays_rel.ml
+++ b/src/lib/reasoners/arrays_rel.ml
@@ -94,7 +94,7 @@ type t =
}
-let empty _ =
+let empty uf =
{gets = G.empty;
tbset = TBS.empty;
split = LRset.empty;
@@ -102,7 +102,7 @@ let empty _ =
seen = Tmap.empty;
new_terms = E.Set.empty;
size_splits = Numbers.Q.one;
- }
+ }, Uf.domains uf
(*BISECT-IGNORE-BEGIN*)
module Debug = struct
@@ -428,10 +428,10 @@ let assume env uf la =
Conseq.fold (fun (a,ex) l ->
((Literal.LTerm a, ex, Th_util.Other)::l)) atoms []
in
- env, { Sig_rel.assume = l; remove = [] }
+ env, Uf.domains uf, { Sig_rel.assume = l; remove = [] }
let query _ _ _ = None
-let add env _ _ _ = env, []
+let add env uf _ _ = env, Uf.domains uf, []
let new_terms env = env.new_terms
let instantiate ~do_syntactic_matching:_ _ env _ _ = env, []
diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
index 267d0fcec4..52dcf7131b 100644
--- a/src/lib/reasoners/bitv_rel.ml
+++ b/src/lib/reasoners/bitv_rel.ml
@@ -33,6 +33,7 @@ module Ex = Explanation
module Sy = Symbols
module X = Shostak.Combine
module SX = Shostak.SXH
+module MX = Shostak.MXH
module HX = Shostak.HX
module L = Xliteral
@@ -83,6 +84,8 @@ module Domain : Rel_utils.Domain with type t = Bitlist.t = struct
include Bitlist
+ let filter_ty = is_bv_ty
+
let fold_signed f { Bitv.value; negated } bl acc =
let bl = if negated then lognot bl else bl in
f value bl acc
@@ -476,22 +479,23 @@ let propagate eqs bcs dom =
type t =
{ delayed : Rel_utils.Delayed.t
- ; domain : Domains.t
; constraints : Constraints.t
; size_splits : Q.t }
-let empty _ =
+let empty uf =
{ delayed = Rel_utils.Delayed.create ~is_ready:X.is_constant dispatch
- ; domain = Domains.empty
; constraints = Constraints.empty
- ; size_splits = Q.one }
+ ; size_splits = Q.one },
+ Uf.Domains.add (module Domains) Domains.empty (Uf.domains uf)
let assume env uf la =
+ let ds = Uf.domains uf in
+ let domain = Uf.Domains.find (module Domains) ds in
let delayed, result = Rel_utils.Delayed.assume env.delayed uf la in
let (domain, constraints, eqs, size_splits) =
try
- let ((constraints, domain), eqs, size_splits) =
- List.fold_left (fun ((bcs, dom), eqs, ss) (a, _root, ex, orig) ->
+ let (constraints, eqs, size_splits) =
+ List.fold_left (fun (bcs, eqs, ss) (a, _root, ex, orig) ->
let ss =
match orig with
| Th_util.CS (Th_bitv, n) -> Q.(ss * n)
@@ -504,9 +508,8 @@ let assume env uf la =
in
match a, orig with
| L.Eq (rr, nrr), Subst when is_bv_r rr ->
- let dom = Domains.subst ~ex rr nrr dom in
let bcs = Constraints.subst ~ex rr nrr bcs in
- ((bcs, dom), eqs, ss)
+ (bcs, eqs, ss)
| L.Distinct (false, [rr; nrr]), _ when is_1bit rr ->
(* We don't (yet) support [distinct] in general, but we must
support it for case splits to avoid looping.
@@ -516,10 +519,10 @@ let assume env uf la =
let not_nrr =
Shostak.Bitv.is_mine (Bitv.lognot (Shostak.Bitv.embed nrr))
in
- ((bcs, dom), (Uf.LX.mkv_eq rr not_nrr, ex) :: eqs, ss)
- | _ -> ((bcs, dom), eqs, ss)
+ (bcs, (Uf.LX.mkv_eq rr not_nrr, ex) :: eqs, ss)
+ | _ -> (bcs, eqs, ss)
)
- ((env.constraints, env.domain), [], env.size_splits)
+ (env.constraints, [], env.size_splits)
la
in
let eqs, constraints, domain = propagate eqs constraints domain in
@@ -541,14 +544,17 @@ let assume env uf la =
let result =
{ result with assume = List.rev_append assume result.assume }
in
- { delayed ; constraints ; domain ; size_splits }, result
+ { delayed ; constraints ; size_splits },
+ Uf.Domains.add (module Domains) domain ds,
+ result
let query _ _ _ = None
-let case_split env _uf ~for_model =
+let case_split env uf ~for_model =
if not for_model && Stdlib.(env.size_splits >= Options.get_max_split ()) then
[]
else
+ let domain = Uf.Domains.find (module Domains) (Uf.domains uf) in
(* Look for representatives with minimal, non-fully known, domain size.
We first look among the constrained variables, then if there are no
@@ -566,28 +572,28 @@ let case_split env _uf ~for_model =
Some (nunk', SX.add r xs)
| _ -> Some (nunk, SX.singleton r)
in
+ let f_acc' r acc =
+ let r, _ = Uf.find_r uf r in
+ List.fold_left (fun acc { Bitv.bv; _ } ->
+ match bv with
+ | Bitv.Cte _ -> acc
+ | Other r | Ext (r, _, _, _) ->
+ let bl = Domains.get r.value domain in
+ f_acc r.value bl acc
+ ) acc (Shostak.Bitv.embed r)
+ in
let _, candidates =
- match
- Constraints.fold_args (fun r acc ->
- List.fold_left (fun acc { Bitv.bv; _ } ->
- match bv with
- | Bitv.Cte _ -> acc
- | Other r | Ext (r, _, _, _) ->
- let bl = Domains.get r.value env.domain in
- f_acc r.value bl acc
- ) acc (Shostak.Bitv.embed r)
- ) env.constraints None
- with
+ match Constraints.fold_args f_acc' env.constraints None with
| Some (nunk, xs) -> nunk, xs
- | None ->
- match Domains.fold_leaves f_acc env.domain None with
+ | _ ->
+ match Domains.fold_leaves f_acc domain None with
| Some (nunk, xs) -> nunk, xs
| None -> 0, SX.empty
in
(* For now, just pick a value for the most significant bit. *)
match SX.choose candidates with
| r ->
- let bl = Domains.get r env.domain in
+ let bl = Domains.get r domain in
let w = Bitlist.width bl in
let unknown = Z.extract (Z.lognot @@ Bitlist.bits_known bl) 0 w in
let bitidx = Z.numbits unknown - 1 in
@@ -607,19 +613,16 @@ let case_split env _uf ~for_model =
let add env uf r t =
let delayed, eqs = Rel_utils.Delayed.add env.delayed uf r t in
let env, eqs =
- match X.type_info r with
- | Tbitv _ -> (
- try
- let dom = Domains.add r env.domain in
- let bcs = extract_constraints env.constraints uf r t in
- let eqs, bcs, dom = propagate eqs bcs dom in
- { env with constraints = bcs ; domain = dom }, eqs
- with Domains.Inconsistent ex ->
- raise @@ Ex.Inconsistent (ex, Uf.cl_extract uf)
- )
- | _ -> env, eqs
+ if is_bv_r r then
+ try
+ let constraints = extract_constraints env.constraints uf r t in
+ { env with constraints }, eqs
+ with Domains.Inconsistent ex ->
+ raise @@ Ex.Inconsistent (ex, Uf.cl_extract uf)
+ else
+ env, eqs
in
- { env with delayed }, eqs
+ { env with delayed }, Uf.domains uf, eqs
let optimizing_objective _env _uf _o = None
diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml
index 53193809d4..51606c2e6b 100644
--- a/src/lib/reasoners/ccx.ml
+++ b/src/lib/reasoners/ccx.ml
@@ -108,11 +108,15 @@ module Main : S = struct
type r = Shostak.Combine.r
- let empty = {
- use = Use.empty ;
- uf = Uf.empty;
- relation = Rel.empty [];
- }
+ let empty =
+ let uf = Uf.empty in
+ let relation, domains = Rel.empty uf in
+ let uf = Uf.set_domains uf domains in
+ {
+ use = Use.empty;
+ uf;
+ relation;
+ }
let empty_facts () =
Sig_rel.{ equas = Queue.create ();
@@ -465,7 +469,8 @@ module Main : S = struct
let replay_atom env sa =
Options.exec_thread_yield ();
let sa = make_unique sa in
- let relation, result = Rel.assume env.relation env.uf sa in
+ let relation, domains, result = Rel.assume env.relation env.uf sa in
+ let env = { env with uf = Uf.set_domains env.uf domains } in
let env = { env with relation = relation } in
let env = clean_use env result.remove in
env, result.assume
@@ -492,7 +497,8 @@ module Main : S = struct
let nuse = Use.up_add env.use t rt lvs in
(* If finitetest is used we add the term to the relation *)
- let rel, eqs = Rel.add env.relation nuf rt t in
+ let rel, doms, eqs = Rel.add env.relation nuf rt t in
+ let nuf = Uf.set_domains nuf doms in
Debug.rel_add_cst t eqs;
(* We add terms made from relations as fact *)
List.iter (fun (a,ex) -> add_fact facts (LSem a, ex, Th_util.Other)) eqs;
diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index db5a75faa4..67c5441311 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -98,6 +98,12 @@ module Domain = struct
domain ~constrs ex
end
+let is_enum_ty = function
+ | Ty.Tsum _ -> true
+ | _ -> false
+
+let is_enum r = is_enum_ty (X.type_info r)
+
module Domains = struct
(** The type of simple domain maps. A domain map maps each representative
(semantic value, of type [X.r]) to its associated domain. *)
@@ -112,6 +118,8 @@ module Domains = struct
in [propagation]. *)
}
+ type _ Uf.id += Id : t Uf.id
+
let pp ppf t =
Fmt.(iter_bindings ~sep:semi MX.iter
(box @@ pair ~sep:(any " ->@ ") X.print Domain.pp)
@@ -121,6 +129,8 @@ module Domains = struct
let empty = { domains = MX.empty; changed = SX.empty }
+ let filter_ty = is_enum_ty
+
let internal_update r nd t =
let domains = MX.add r nd t.domains in
let changed = SX.add r t.changed in
@@ -138,16 +148,14 @@ module Domains = struct
Domain.unknown (X.type_info r)
let add r t =
- if MX.mem r t.domains then t
- else
- match Th.embed r with
- | Cons _ -> t
- | _ ->
- (* We have to add a default domain if the key `r` isn't in map in order
- to be sure that the case-split mechanism will attempt to choose a
- value for it. *)
- let nd = Domain.unknown (X.type_info r) in
- internal_update r nd t
+ match Th.embed r with
+ | Alien _ when not (MX.mem r t.domains) ->
+ (* We have to add a default domain if the key `r` isn't in map in order
+ to be sure that the case-split mechanism will attempt to choose a
+ value for it. *)
+ let nd = Domain.unknown (X.type_info r) in
+ internal_update r nd t
+ | Cons _ | Alien _ -> t
(** [tighten r d t] replaces the domain of [r] in [t] by a domain [d] contains
in the current domain of [r]. The representative [r] is marked [changed]
@@ -167,6 +175,8 @@ module Domains = struct
let changed = SX.remove r t.changed in
{ domains ; changed }
+ exception Inconsistent = Domain.Inconsistent
+
(** [subst ~ex p v d] replaces all the instances of [p] with [v] in all
domains, merging the corresponding domains as appropriate.
@@ -181,7 +191,7 @@ module Domains = struct
let t = remove r t in
tighten nr nd t
- | exception Not_found -> t
+ | exception Not_found -> add nr t
let fold f t acc = MX.fold f t.domains acc
@@ -200,16 +210,6 @@ module Domains = struct
end
type t = {
- 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.
- This state is kept for debugging purposes only. It is updated with
- [Uf.cl_extract] after assuming literals of the theory and returned by
- queries in case of inconsistency. *)
-
size_splits : Numbers.Q.t
(* Estimate the number of case-splits performed by the theory. The
estimation is updated while assuming new literals of the theory.
@@ -240,18 +240,16 @@ module Debug = struct
Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"add"
"%a" X.print r
- let pp_env env =
+ let pp_domains domains =
if Options.get_debug_sum () then
Printer.print_dbg ~module_name:"Enum_rel"
- "The environment before assuming:@ @[%a@]" Domains.pp env.domains
+ "The environment before assuming:@ @[%a@]" Domains.pp domains
end
(*BISECT-IGNORE-END*)
-let empty classes = {
- domains = Domains.empty;
- classes = classes;
+let empty uf = {
size_splits = Numbers.Q.one
-}
+}, Uf.Domains.add (module Domains) Domains.empty (Uf.domains uf)
(* Update the counter of case-split size in [env]. *)
let count_splits env la =
@@ -263,18 +261,10 @@ let count_splits env la =
| _ -> nb
) env.size_splits la
in
- {env with size_splits = nb}
-
-let tighten_domain rr nd env =
- { env with domains = Domains.tighten rr nd env.domains }
+ {size_splits = nb}
-(* 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 }
+let tighten_domain rr nd domains =
+ Domains.tighten rr nd domains
(* Update the domains of the semantic values [r1] and [r2] according to the
disequality [r1 <> r2].
@@ -292,17 +282,17 @@ let assume_subst ~ex r1 r2 env =
@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 assume_distinct ~ex r1 r2 domains =
+ let d1 = Domains.get r1 domains in
+ let d2 = Domains.get r2 domains in
let env =
match Domain.as_singleton d1 with
| Some (c, ex1) ->
let ex = Ex.union ex1 ex in
let nd = Domain.remove ~ex c d2 in
- tighten_domain r2 nd env
+ tighten_domain r2 nd domains
| None ->
- env
+ domains
in
match Domain.as_singleton d2 with
| Some (c, ex2) ->
@@ -312,57 +302,38 @@ let assume_distinct ~ex r1 r2 env =
| None ->
env
-let is_enum r =
- match X.type_info r with
- | Ty.Tsum _ -> true
- | _ -> false
-
-let add r uf env =
+let add r uf domains =
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 }
+ Domains.add rr domains
| _ ->
- env
+ domains
-let add_rec r uf env =
- List.fold_left (fun env leaf -> add leaf uf env) env (X.leaves r)
+let add_rec r uf domains =
+ List.fold_left (fun env leaf -> add leaf uf env) domains (X.leaves r)
-let add env uf r _t = add r uf env, []
+let add env uf _r _t =
+ env, Uf.domains uf, []
-let assume_literals la uf env =
+let assume_literals la uf domains =
List.fold_left
- (fun env lit ->
+ (fun domains lit ->
let open Xliteral in
match lit with
- | Eq (r1, r2) as l, _, ex, Th_util.Subst when is_enum r1 ->
- Debug.assume l;
- (* Needed for models generation because fresh terms are not added with
- the function add. *)
- 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;
(* Needed for models generation because fresh terms are not added with
the function add. *)
- 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 =
+ let domains = add_rec r1 uf domains in
+ let domains = add_rec r2 uf domains in
+ assume_distinct ~ex r1 r2 domains
+
+ | _ -> domains
+ ) domains la
+
+let propagate_domains domains =
Domains.propagate
(fun eqs rr d ->
match Domain.as_singleton d with
@@ -372,21 +343,23 @@ let propagate_domains env =
eq :: eqs
| None ->
eqs
- ) [] env.domains
+ ) [] domains
let assume env uf la =
- Debug.pp_env env;
+ let ds = Uf.domains uf in
+ let domains = Uf.Domains.find (module Domains) ds in
+ Debug.pp_domains domains;
let env = count_splits env la in
- let classes = Uf.cl_extract uf in
- let env = { env with classes = classes } in
- let env =
+ let domains =
try
- assume_literals la uf env
+ assume_literals la uf domains
with Domain.Inconsistent ex ->
- raise_notrace (Ex.Inconsistent (ex, env.classes))
+ raise_notrace (Ex.Inconsistent (ex, Uf.cl_extract uf))
in
- let assume, domains = propagate_domains env in
- { env with domains }, Sig_rel.{ assume; remove = [] }
+ let assume, domains = propagate_domains domains in
+ env,
+ Uf.Domains.add (module Domains) domains ds,
+ Sig_rel.{ assume; remove = [] }
let can_split env n =
let m = Options.get_max_split () in
@@ -409,7 +382,7 @@ let case_split env uf ~for_model =
match best with
| Some (n, _, _) when n <= cd -> best
| _ -> Some (cd, r, Domain.choose d)
- ) env.domains None
+ ) (Uf.Domains.find (module Domains) (Uf.domains uf)) None
in
match best with
| Some (n, r, c) ->
diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml
index ac25097a0f..47576ba684 100644
--- a/src/lib/reasoners/intervalCalculus.ml
+++ b/src/lib/reasoners/intervalCalculus.ml
@@ -683,7 +683,7 @@ let dispatch = function
| Symbols.Pow -> Some delayed_pow
| _ -> None
-let empty classes = {
+let empty uf = {
inequations = MPL.empty;
monomes = MX.empty ;
polynomes = MP.empty ;
@@ -691,7 +691,7 @@ let empty classes = {
known_eqs = SX.empty ;
improved_p = SP.empty ;
improved_x = SX.empty ;
- classes = classes;
+ classes = Uf.cl_extract uf;
size_splits = Q.one;
new_uf = Uf.empty;
@@ -705,7 +705,7 @@ let empty classes = {
th_axioms = ME.empty;
linear_dep = ME.empty;
syntactic_matching = [];
-}
+}, Uf.domains uf
(*let up_improved env p oldi newi =
if I.is_strict_smaller newi oldi then
@@ -1700,7 +1700,7 @@ let assume ~query env uf la =
if Uf.is_normalized uf (alien_of p) then mp else MP.remove p mp)
env.polynomes env.polynomes
in
- {env with polynomes = polys}, res
+ {env with polynomes = polys}, Uf.domains uf, res
let query env uf a_ex =
try
@@ -1801,8 +1801,8 @@ let add =
let delayed, eqs =
Rel_utils.Delayed.add env.delayed env.new_uf r t
in
- { env with delayed }, eqs
- else env, []
+ { env with delayed }, Uf.domains new_uf, eqs
+ else env, Uf.domains new_uf, []
with I.NotConsistent expl ->
Debug.inconsistent_interval expl;
raise (Ex.Inconsistent (expl, env.classes))
diff --git a/src/lib/reasoners/ite_rel.ml b/src/lib/reasoners/ite_rel.ml
index d3e2dba9f0..258143f64f 100644
--- a/src/lib/reasoners/ite_rel.ml
+++ b/src/lib/reasoners/ite_rel.ml
@@ -89,13 +89,13 @@ type t = {
state of the solver to their explanation. *)
}
-let empty _ = {
+let empty uf = {
pending_deds = ME2.empty;
guarded_pos_deds = ME.empty;
guarded_neg_deds = ME.empty;
assumed_pos_preds = ME.empty;
assumed_neg_preds = ME.empty;
-}
+}, Uf.domains uf
let is_ite =
let ite = Symbols.Op Symbols.Tite in
@@ -135,8 +135,8 @@ let add_aux env t =
let guarded_neg_deds = add_to_guarded p t t2 env.guarded_neg_deds in
{env with guarded_pos_deds; guarded_neg_deds}
-let add env _ _ t =
- add_aux env t, []
+let add env uf _ t =
+ add_aux env t, Uf.domains uf, []
(* Extract all the assumed predicates with their explanation from the input of
the function assume below. *)
@@ -180,8 +180,9 @@ let extract_pending_deductions env =
(* Save in the environment env all the assumed predicates of la. Produce new
deductions implied by these new assumed predicates.
Eventually, return all the pending deductions. *)
-let assume env _ la =
- if Options.get_disable_ites () then env, { Sig_rel.assume = []; remove = [] }
+let assume env uf la =
+ if Options.get_disable_ites () then
+ env, Uf.domains uf, { Sig_rel.assume = []; remove = [] }
else
let env =
TB.fold
@@ -209,7 +210,7 @@ let assume env _ la =
)(extract_preds env la) env
in
let env, deds = extract_pending_deductions env in
- env, { Sig_rel.assume = deds; remove = [] }
+ env, Uf.domains uf, { Sig_rel.assume = deds; remove = [] }
let case_split _env _uf ~for_model:_ = []
diff --git a/src/lib/reasoners/records_rel.ml b/src/lib/reasoners/records_rel.ml
index f50a993331..54c06f77dd 100644
--- a/src/lib/reasoners/records_rel.ml
+++ b/src/lib/reasoners/records_rel.ml
@@ -32,13 +32,13 @@ type t = unit
let timer = Timers.M_Records
-let empty _ = ()
-let assume _ _ _ =
- (), { Sig_rel.assume = []; remove = []}
+let empty uf = (), Uf.domains uf
+let assume _ uf _ =
+ (), Uf.domains uf, { Sig_rel.assume = []; remove = [] }
let query _ _ _ = None
let case_split _env _uf ~for_model:_ = []
let optimizing_objective _env _uf _o = None
-let add env _ _ _ = env, []
+let add env uf _ _ = env, Uf.domains uf, []
let new_terms _ = Expr.Set.empty
let instantiate ~do_syntactic_matching:_ _ env _ _ = env, []
diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml
index fac5c20041..4762485486 100644
--- a/src/lib/reasoners/rel_utils.ml
+++ b/src/lib/reasoners/rel_utils.ml
@@ -225,8 +225,13 @@ module type Domain = sig
exception Inconsistent of Explanation.t
(** Exception raised by [intersect] when an inconsistency is detected. *)
+ val filter_ty : Ty.t -> bool
+ (** Filter for the types of values this domain can be attached to. *)
+
val unknown : Ty.t -> t
- (** [unknown ty] returns a full domain for values of type [t]. *)
+ (** [unknown ty] returns a full domain for values of type [t].
+
+ @raises Invalid_argument if [filter_ty ty] does not hold. *)
val add_explanation : ex:Explanation.t -> t -> t
(** [add_explanation ~ex d] adds the justification [ex] to the domain d. The
@@ -258,29 +263,14 @@ module type Domain = sig
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. *)
+ (** Extended signature for global domains. *)
- val pp : t Fmt.t
- (** Pretty-printer for domain maps. *)
-
- val empty : t
- (** The empty domain map. *)
+ include Uf.Domains
type elt
(** 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], [subst] and [structural_propagation] 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]. *)
@@ -288,14 +278,6 @@ module type Domains = sig
(** [fold f t acc] folds [f] over all the domains in [t] that are associated
with leaves. *)
- 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 Inconsistent if this causes any domain in [d] to become empty. *)
-
val has_changed : t -> bool
(** Returns [true] if any element is marked as changed. This can be used to
avoid unnecessary calls to [edit].
@@ -388,16 +370,19 @@ struct
(** Map from leaves to the *tracked* representatives that contains them *)
}
+ type _ Uf.id += Id : t Uf.id
+
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 ; leaves_map = MX.empty }
+ let filter_ty = Domain.filter_ty
+
let r_add r leaves_map =
List.fold_left (fun leaves_map leaf ->
MX.update leaf (function
@@ -412,9 +397,7 @@ struct
) r ()
let add r t =
- match MX.find r t.domains with
- | _ -> t
- | exception Not_found ->
+ if MX.mem r t.domains then t else
(* Note: we do not need to mark [r] as needing propagation, because no
constraints applied to it yet. Any constraint that apply to [r] will
already be marked as pending due to being newly added. *)
@@ -473,65 +456,51 @@ struct
) t.leaves_map acc
let subst ~ex rr nrr t =
- match MX.find rr t.leaves_map with
- | parents ->
- SX.fold (fun r t ->
- let d =
- (* Need to add [ex] to be a valid domain for nrr *)
- try Domain.add_explanation ~ex (MX.find r t.domains)
- with Not_found ->
- (* [r] was in the [leaves_map] to it must have a domain *)
- assert false
- in
- let changed = SX.mem r t.changed in
- let t = remove r t in
- let nr = X.subst rr nrr r in
- match MX.find nr t.domains with
- | nd ->
- (* If there is an existing domain for [nr], there might be
- constraints applying to [nr] prior to the substitution, and the
- constraints that used to apply to [r] will also apply to [nr]
- after the substitution.
-
- We need to notify changed to either of these constraints, so we
- must notify if the domain is different from *either* the old
- domain of [r] or the old domain of [nr]. *)
- let nnd = Domain.intersect d nd in
- let nr_changed = not (Domain.equal nnd nd) in
- let r_changed = not (Domain.equal nnd d) in
- let domains =
- if nr_changed then MX.add nr nnd t.domains else t.domains
- in
- let changed = changed || r_changed || nr_changed in
- let changed =
- if changed then SX.add nr t.changed else t.changed
- in
- { t with domains; changed }
- | exception Not_found ->
- (* If there is no existing domain for [nr], there were no
- constraints applying to [nr] prior to the substitution.
-
- The only constraints that need to be notified are those that
- were applying to [r], and they only need to be notified if the
- new domain is different from the old domain of [r]. *)
- let default = create_domain nr in
- let nd = Domain.intersect d default in
- let r_changed = not (Domain.equal nd d) in
- (* Make sure to not add more constraints than necessary for the
- representative domain. *)
- let nd = if Domain.equal nd default then default else nd in
- let domains = MX.add nr nd t.domains in
- let leaves_map = r_add nr t.leaves_map in
- let changed = changed || r_changed in
- let changed =
- if changed then SX.add nr t.changed else t.changed
- in
- { domains; changed; leaves_map }
- ) parents t
+ (* Need to add [ex] to be a valid domain for [nrr] *)
+ let d = Domain.add_explanation ~ex (get rr t) in
+ let changed = SX.mem rr t.changed in
+ let t = remove rr t in
+ match MX.find nrr t.domains with
+ | nd ->
+ (* If there is an existing domain for [nrr], there might be
+ constraints applying to [nrr] prior to the substitution, and the
+ constraints that used to apply to [rr] will also apply to [nrr]
+ after the substitution.
+
+ We need to notify changed to either of these constraints, so we
+ must notify if the domain is different from *either* the old
+ domain of [rr] or the old domain of [nrr]. *)
+ let nnd = Domain.intersect d nd in
+ let nrr_changed = not (Domain.equal nnd nd) in
+ let rr_changed = not (Domain.equal nnd d) in
+ let domains =
+ if nrr_changed then MX.add nrr nnd t.domains else t.domains
+ in
+ let changed = changed || rr_changed || nrr_changed in
+ let changed =
+ if changed then SX.add nrr t.changed else t.changed
+ in
+ { t with domains; changed }
| exception Not_found ->
- (* We are not tracking any semantic value that have [r] as a leaf, so we
- have nothing to do. *)
- t
+ (* If there is no existing domain for [nr], there were no
+ constraints applying to [nr] prior to the substitution.
+
+ The only constraints that need to be notified are those that
+ were applying to [r], and they only need to be notified if the
+ new domain is different from the old domain of [r]. *)
+ let default = create_domain nrr in
+ let nd = Domain.intersect d default in
+ let rr_changed = not (Domain.equal nd d) in
+ (* Make sure to not add more constraints than necessary for the
+ representative domain. *)
+ let nd = if Domain.equal nd default then default else nd in
+ let domains = MX.add nrr nd t.domains in
+ let leaves_map = r_add nrr t.leaves_map in
+ let changed = changed || rr_changed in
+ let changed =
+ if changed then SX.add nrr t.changed else t.changed
+ in
+ { domains; changed; leaves_map }
let has_changed t =
not @@ SX.is_empty t.changed
diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml
index 21c9c57f49..ce0a0d9a7e 100644
--- a/src/lib/reasoners/relation.ml
+++ b/src/lib/reasoners/relation.ml
@@ -59,15 +59,15 @@ type t = {
r7: Rel7.t;
}
-let empty classes = {
- r1=Rel1.empty classes;
- r2=Rel2.empty classes;
- r3=Rel3.empty classes;
- r4=Rel4.empty classes;
- r5=Rel5.empty classes;
- r6=Rel6.empty classes;
- r7=Rel7.empty classes;
-}
+let empty uf =
+ let r1, doms1 = Rel1.empty uf in
+ let r2, doms2 = Rel2.empty (Uf.set_domains uf doms1) in
+ let r3, doms3 = Rel3.empty (Uf.set_domains uf doms2) in
+ let r4, doms4 = Rel4.empty (Uf.set_domains uf doms3) in
+ let r5, doms5 = Rel5.empty (Uf.set_domains uf doms4) in
+ let r6, doms6 = Rel6.empty (Uf.set_domains uf doms5) in
+ let r7, doms7 = Rel7.empty (Uf.set_domains uf doms6) in
+ {r1; r2; r3; r4; r5; r6; r7}, doms7
let (|@|) l1 l2 =
if l1 == [] then l2
@@ -76,35 +76,36 @@ let (|@|) l1 l2 =
let assume env uf sa =
Options.exec_thread_yield ();
- let env1, ({ assume = a1; remove = rm1}:_ Sig_rel.result) =
+ let env1, doms1, ({ assume = a1; remove = rm1}:_ Sig_rel.result) =
Timers.with_timer Rel1.timer Timers.F_assume @@ fun () ->
Rel1.assume env.r1 uf sa
in
- let env2, ({ assume = a2; remove = rm2}:_ Sig_rel.result) =
+ let env2, doms2, ({ assume = a2; remove = rm2}:_ Sig_rel.result) =
Timers.with_timer Rel2.timer Timers.F_assume @@ fun () ->
- Rel2.assume env.r2 uf sa
+ Rel2.assume env.r2 (Uf.set_domains uf doms1) sa
in
- let env3, ({ assume = a3; remove = rm3}:_ Sig_rel.result) =
+ let env3, doms3, ({ assume = a3; remove = rm3}:_ Sig_rel.result) =
Timers.with_timer Rel3.timer Timers.F_assume @@ fun () ->
- Rel3.assume env.r3 uf sa
+ Rel3.assume env.r3 (Uf.set_domains uf doms2) sa
in
- let env4, ({ assume = a4; remove = rm4}:_ Sig_rel.result) =
+ let env4, doms4, ({ assume = a4; remove = rm4}:_ Sig_rel.result) =
Timers.with_timer Rel4.timer Timers.F_assume @@ fun () ->
- Rel4.assume env.r4 uf sa
+ Rel4.assume env.r4 (Uf.set_domains uf doms3) sa
in
- let env5, ({ assume = a5; remove = rm5}:_ Sig_rel.result) =
+ let env5, doms5, ({ assume = a5; remove = rm5}:_ Sig_rel.result) =
Timers.with_timer Rel5.timer Timers.F_assume @@ fun () ->
- Rel5.assume env.r5 uf sa
+ Rel5.assume env.r5 (Uf.set_domains uf doms4) sa
in
- let env6, ({ assume = a6; remove = rm6}:_ Sig_rel.result) =
+ let env6, doms6, ({ assume = a6; remove = rm6}:_ Sig_rel.result) =
Timers.with_timer Rel6.timer Timers.F_assume @@ fun () ->
- Rel6.assume env.r6 uf sa
+ Rel6.assume env.r6 (Uf.set_domains uf doms5) sa
in
- let env7, ({ assume = a7; remove = rm7}:_ Sig_rel.result) =
+ let env7, doms7, ({ assume = a7; remove = rm7}:_ Sig_rel.result) =
Timers.with_timer Rel7.timer Timers.F_assume @@ fun () ->
- Rel7.assume env.r7 uf sa
+ Rel7.assume env.r7 (Uf.set_domains uf doms6) sa
in
{r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6; r7=env7},
+ doms7,
({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6 |@| a7;
remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 |@| rm7}
: _ Sig_rel.result)
@@ -177,14 +178,14 @@ let optimizing_objective env uf o =
let add env uf r t =
Options.exec_thread_yield ();
- let r1, eqs1 =Rel1.add env.r1 uf r t in
- let r2, eqs2 =Rel2.add env.r2 uf r t in
- let r3, eqs3 =Rel3.add env.r3 uf r t in
- let r4, eqs4 =Rel4.add env.r4 uf r t in
- let r5, eqs5 =Rel5.add env.r5 uf r t in
- let r6, eqs6 =Rel6.add env.r6 uf r t in
- let r7, eqs7 =Rel7.add env.r7 uf r t in
- {r1;r2;r3;r4;r5;r6;r7;},eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6|@|eqs7
+ let r1, doms1, eqs1 =Rel1.add env.r1 uf r t in
+ let r2, doms2, eqs2 =Rel2.add env.r2 (Uf.set_domains uf doms1) r t in
+ let r3, doms3, eqs3 =Rel3.add env.r3 (Uf.set_domains uf doms2) r t in
+ let r4, doms4, eqs4 =Rel4.add env.r4 (Uf.set_domains uf doms3) r t in
+ let r5, doms5, eqs5 =Rel5.add env.r5 (Uf.set_domains uf doms4) r t in
+ let r6, doms6, eqs6 =Rel6.add env.r6 (Uf.set_domains uf doms5) r t in
+ let r7, doms7, eqs7 =Rel7.add env.r7 (Uf.set_domains uf doms6) r t in
+ {r1;r2;r3;r4;r5;r6;r7;},doms7,eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6|@|eqs7
let instantiate ~do_syntactic_matching t_match env uf selector =
diff --git a/src/lib/reasoners/sig_rel.mli b/src/lib/reasoners/sig_rel.mli
index 8406392e49..03064cd6b9 100644
--- a/src/lib/reasoners/sig_rel.mli
+++ b/src/lib/reasoners/sig_rel.mli
@@ -45,7 +45,7 @@ type 'a facts = {
}
type 'a result = {
- assume : 'a fact list;
+ assume: 'a fact list;
remove: Expr.t list;
}
@@ -54,10 +54,11 @@ module type RELATION = sig
val timer : Timers.ty_module
- val empty : Expr.Set.t list -> t
+ val empty : Uf.t -> t * Uf.Domains.t
val assume : t ->
- Uf.t -> (Shostak.Combine.r input) list -> t * Shostak.Combine.r result
+ Uf.t -> (Shostak.Combine.r input) list ->
+ t * Uf.Domains.t * Shostak.Combine.r result
val query : t -> Uf.t -> Shostak.Combine.r input -> Th_util.answer
val case_split :
@@ -80,7 +81,7 @@ module type RELATION = sig
Returns [None] if the theory cannot optimize the objective. *)
val add : t -> Uf.t -> Shostak.Combine.r -> Expr.t ->
- t * (Shostak.Combine.r Xliteral.view * Explanation.t) list
+ t * Uf.Domains.t * (Shostak.Combine.r Xliteral.view * Explanation.t) list
(** add a representant to take into account *)
val instantiate :
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index 53ccef25ed..66182b4ee3 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -47,8 +47,8 @@ end
module SetX = Shostak.SXH
module SetXX = Set.Make(struct
- type t = X.r * X.r
- let compare (r1, r1') (r2, r2') =
+ type t = X.r * X.r * Explanation.t
+ let compare (r1, r1', _) (r2, r2', _) =
let c = X.hash_cmp r1 r2 in
if c <> 0 then c
else X.hash_cmp r1' r2'
@@ -78,6 +78,87 @@ end
type r = X.r
+type _ id = ..
+
+module type Domains = sig
+ type t
+
+ val pp : t Fmt.t
+
+ type _ id += Id : t id
+
+ val empty : t
+
+ val filter_ty : Ty.t -> bool
+
+ val add : X.r -> t -> t
+
+ exception Inconsistent of Explanation.t
+
+ val subst : ex:Explanation.t -> r -> r -> t -> t
+end
+
+type 'a domains = (module Domains with type t = 'a)
+
+module Domains = struct
+ type (_, _) eq = Equal : ('a, 'a) eq
+
+ let[@inline] uid (type a) ((module Doms) : a domains) =
+ Obj.Extension_constructor.id (Obj.Extension_constructor.of_val Doms.Id)
+
+ module MapI = Map.Make(Int)
+
+ type binding = B : 'a domains * 'a -> binding
+
+ type t = binding MapI.t
+
+ let pp : t Fmt.t =
+ let open Fmt in
+ vbox (
+ any "@,=================== UF: Domains ======================@," ++
+ iter
+ ~sep:(any "@,------------------------------------------------------@,")
+ (fun f ->
+ MapI.iter (fun _ (B ((module D), d)) ->
+ f (hvbox (const D.pp d))
+ ))
+ (fun ppf pp -> pp ppf ())
+ ) ++ cut
+
+ let empty = MapI.empty
+
+ let find (type a) ((module D) as k : a domains) t : a =
+ match MapI.find (uid k) t with
+ | exception Not_found -> D.empty
+ | B ((module D'), d) ->
+ match D'.Id with
+ | D.Id -> d
+ | _ ->
+ (* Distinct extension constructors cannot have the same uid. *)
+ assert false
+
+ let init r t =
+ let ty = X.type_info r in
+ MapI.map (function B ((module D) as dom, d) as b ->
+ if D.filter_ty ty then B (dom, D.add r d) else b
+ ) t
+
+ let add (type a) ((module D) as dom : a domains) v t =
+ MapI.add (uid dom) (B (dom, v)) t
+
+ exception Inconsistent of Ex.t
+
+ let subst ~ex rr nrr t =
+ let ty = X.type_info rr in
+ MapI.map (function B (((module D) as dom), d) as b ->
+ if D.filter_ty ty then
+ try
+ B (dom, D.subst ~ex rr nrr d)
+ with D.Inconsistent ex -> raise (Inconsistent ex)
+ else b
+ ) t
+end
+
type t = {
(* term -> [t] *)
@@ -86,6 +167,9 @@ type t = {
(* representative table *)
repr : (r * Ex.t) MapX.t;
+ (* domains associated with class representatives (values in repr) only *)
+ domains : Domains.t;
+
(* r -> class (of terms) *)
classes : SE.t MapX.t;
@@ -100,7 +184,6 @@ type t = {
ac_rs : SetRL.t RS.t;
}
-
exception Found_term of E.t
(* hack: would need an inverse map from semantic values to terms *)
@@ -200,13 +283,14 @@ module Debug = struct
print_dbg
~module_name:"Uf" ~function_name:"all"
"@[<v 0>-------------------------------------------------@ \
- %a%a%a%a%a\
+ %a%a%a%a%a%a\
-------------------------------------------------@]"
pmake env.make
prepr env.repr
prules env.ac_rs
pclasses env.classes
pneqs env.neqs
+ (if Options.get_verbose () then Domains.pp else Fmt.any "") env.domains
let lookup_not_found t env =
print_err
@@ -502,6 +586,10 @@ module Env = struct
function again with x == repr_x *)
MapX.add repr_x mapl (MapX.remove x env.neqs)
+ let update_domains ~ex rr nrr env =
+ try Domains.subst ~ex rr nrr env.domains
+ with Domains.Inconsistent ex -> raise (Ex.Inconsistent (ex, cl_extract env))
+
let init_leaf env p =
Debug.init_leaf p;
let in_repr = MapX.mem p env.repr in
@@ -521,6 +609,9 @@ module Env = struct
repr =
if in_repr then env.repr
else MapX.add p (rp, ex_rp) env.repr;
+ domains =
+ if in_repr then env.domains
+ else Domains.init rp env.domains;
classes =
if MapX.mem p env.classes then env.classes
else update_classes p rp env.classes;
@@ -555,6 +646,7 @@ module Env = struct
{env with
make = ME.add t mkr env.make;
repr = MapX.add mkr (rp,ex) env.repr;
+ domains = Domains.init rp env.domains;
classes = add_to_classes t rp env.classes;
gamma = add_to_gamma mkr rp env.gamma;
neqs =
@@ -628,12 +720,13 @@ module Env = struct
head_cp eqs env p r v dep;
env
- let update_aux dep set env=
+ let update_aux dep set env =
SetXX.fold
- (fun (rr, nrr) env ->
+ (fun (rr, nrr, ex) env ->
{ env with
neqs = update_neqs rr nrr dep env ;
- classes = update_classes rr nrr env.classes})
+ classes = update_classes rr nrr env.classes ;
+ domains = update_domains ~ex rr nrr env })
set env
(* Patch modudo AC for CC: if p is a leaf different from r and r is AC
@@ -668,7 +761,7 @@ module Env = struct
env,
(r, nrr, ex)::touched_p,
update_global_tch global_tch p r nrr ex,
- SetXX.add (rr, nrr) neqs_to_up
+ SetXX.add (rr, nrr, dep) neqs_to_up
) use_p (env, [], global_tch, SetXX.empty)
in
(* Correction : Do not update neqs twice for the same r *)
@@ -695,7 +788,7 @@ module Env = struct
if X.is_a_leaf r then (r,[r, nrr, ex],nrr) :: tch
else tch
in
- env, tch, SetXX.add (rr, nrr) neqs_to_up
+ env, tch, SetXX.add (rr, nrr, ex_nrr) neqs_to_up
) env.repr (env, tch, SetXX.empty)
in
(* Correction : Do not update neqs twice for the same r *)
@@ -868,6 +961,10 @@ let find_r =
Options.tool_req 3 "TR-UFX-Find";
Env.find_or_normal_form
+let domains env = env.domains
+
+let set_domains env domains = { env with domains }
+
let print = Debug.all
let mem = Env.mem
@@ -891,6 +988,7 @@ let empty =
let env = {
make = ME.empty;
repr = MapX.empty;
+ domains = Domains.empty;
classes = MapX.empty;
gamma = MapX.empty;
neqs = MapX.empty;
diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli
index 95396a30b5..390bc544d6 100644
--- a/src/lib/reasoners/uf.mli
+++ b/src/lib/reasoners/uf.mli
@@ -34,6 +34,77 @@ type t
type r = Shostak.Combine.r
+type _ id = ..
+(** Extensible type for global domains identifiers, see {!Domains}. *)
+
+module type Domains = sig
+ (** Module signature for global domains used by the union-find module.
+
+ The union-find module updates global domains when equivalence classes are
+ merged. *)
+
+ type t
+ (** The type of global domains. *)
+
+ val pp : t Fmt.t
+ (** Pretty-printer for global domains. *)
+
+ type _ id += Id : t id
+ (** Id used by the union-find module to dispatch to this module. Must be
+ unique (i.e. do not re-export the [Id] from another module). *)
+
+ val empty : t
+ (** The empty domain. *)
+
+ val filter_ty : Ty.t -> bool
+ (** Limit the type of terms that this module cares about. Only substitutions
+ of representatives for which [filter_ty (type_info r)] holds will be
+ propagated to this module. *)
+
+ val add : r -> t -> t
+ (** [add r t] is called when the representative [r] is added to the
+ union-find, if it has a type that matches [filter_ty].
+
+ {b Note}: unlike [Relation.add], this function is called even for
+ "dynamic" representatives added by [X.make] or AC normalization. *)
+
+ exception Inconsistent of Explanation.t
+ (** Raised by [subst] below when an inconsistency is found while merging the
+ domains.*)
+
+ val subst : ex:Explanation.t -> r -> r -> t -> t
+ (** [subst ~ex rr nrr t] is called when the representatives [rr] and [nrr] are
+ merged with explanation [ex]. [nrr] is the new representative; [rr] should
+ no longer be tracked and the intersection of domains should be associated
+ with [nrr].
+
+ The explanation [ex] justifies the equality [rr = nrr].
+
+ @raise Inconsistent if the domains for [rr] and [nrr] are incompatible. *)
+end
+
+type 'a domains = (module Domains with type t = 'a)
+(** The type for global domain modules with storage type ['a]. *)
+
+module Domains : sig
+ (** Maps from domain module to an instance of the corresponding type. *)
+
+ type t
+ (** The [Domains.t] type maps domain modules (of type ['a domains]) to an
+ associated domain of the corresponding type ['a]. *)
+
+ val empty : t
+ (** [empty] maps all domain modules [D] to its default domain [D.empty]. *)
+
+ val find : 'a domains -> t -> 'a
+ (** [find (module D) t] returns the global domain associated with the domain
+ module [D]. Defaults to [D.empty]. *)
+
+ val add : 'a domains -> 'a -> t -> t
+ (** [add (module D) d t] registers the global domain [d] for the domain module
+ [D]. Overwrite any pre-existing global domain associated with [D]. *)
+end
+
module LX = Shostak.L
val empty : t
@@ -45,6 +116,10 @@ val find : t -> Expr.t -> r * Explanation.t
val find_r : t -> r -> r * Explanation.t
+val domains : t -> Domains.t
+
+val set_domains : t -> Domains.t -> t
+
val union :
t -> r -> r -> Explanation.t ->
t * (r * (r * r * Explanation.t) list * r) list