Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Refactoring
Enum_rel
using domains on class representatives only (#…
…1078) * 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. * Use stubs for `fold_leaves` and `map_leaves` * Move the comment * Add `as_singleton` in `Domain` * Rename `case_split_limit` to `can_split` * Inline the function SimpleDomains in `Enum_rel` * Fix comment about the `unknown` function of `Domain` * Revert the modification of `unknown` in `Rel_utils` * Preserve default domain during updates The previous implementation of `Domain.update` could replace a default domain (with the empty explanation) by a default one with a non-empty explanation. There is no reason to add these extra explanations. This new implementation doesn't update the map `t.domains` if the intersection is a default domain. It means `update` doesn't add a domain if `d` is a default domain and `r` isn't in the map, which is ok as we ensure that all seen semantic values are added to `t.domains` in `assume`. * Rename `unknown` into `default` The `unknown` function in `Enum_rel` doesn't return the full domain for constructor semantic values but the tightest possible domain for it. The `default` name is more appropriate for this behaviour. * Improve efficency of `get` and `add` As we inlined the function `SimpleDomains_make` in `Enum_rel`, we can write more efficient code for this theory. We don't need to look in the map `t.domains` for constructor semantic values as we always produce the same default domain for them, that is a singleton without any explanation. * No intersection in `update` We don't need to perform an intersection in `Domain.update` as we always call it on domains that are subsets of the old ones. * Restore bitv_rel and rel_utils * Add comments * Review changes
- Loading branch information