Skip to content

Commit

Permalink
Refactoring Enum_rel using domains on class representatives only (#…
Browse files Browse the repository at this point in the history
…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
Halbaroth authored Apr 4, 2024
1 parent bc0e045 commit ef4119e
Show file tree
Hide file tree
Showing 2 changed files with 328 additions and 239 deletions.
Loading

0 comments on commit ef4119e

Please sign in to comment.