Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(BV): Interval domains for bit-vectors #1058

Merged
merged 8 commits into from
Jun 21, 2024
Merged

feat(BV): Interval domains for bit-vectors #1058

merged 8 commits into from
Jun 21, 2024

Commits on Jun 20, 2024

  1. feat(BV): Interval domains for bit-vectors 

    This patch adds interval domains to the Bitv_rel module, as well as
interreductions between the bitlist and interval domains following:

  Sharpening Constraint Programming approaches for Bit-Vector Theory.
  Zakaria Chihani, Bruno Marre, François Bobot, Sébastien Bardin.
  CPAIOR 2017. International Conference on AI and OR Techniques in
    Constraint Programming for Combinatorial Optimization Problems, Jun
    2017, Padova, Italy.

More precisely:

 - The `Intervals` module is extended to support the `extract`
   operation, which is used to propagate between bit-vector compositions
   and their components;

 - The interreductions are implemented using the new
   `Bitlist.increase_lower_bound`, `Bitlist.decrease_upper_bound`, and
   the new `shared_msb` helper in `Bitv_rel`;

 - Propagations are performed by alternating propagations until fixpoint
   in each domain, followed by interreductions and propagations until
   fixpoint in the other domain, until reaching a fixpoint for the whole
   procedure. It is not clear that this is the best strategy; the goal
   is to try and limit interreductions since they are relatively
   expensive but we should revisit this once more operations are
   supported.

For now, only the `bvule`, `bvult`, `bvugt` and `bvuge` primitives are
supported as built-in bit-vector operations; other operations such as
`bvadd` are still encoded using `bv2nat`. These operations will be
migrated to bit-vector primitives in a follow-up PR.

Finally, there are some tests for the tricky bits (`Intervals.extract`
and the interreduction primitives) using QCheck.
    @bclement-ocp
    bclement-ocp committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    a396b5e View commit details
    Browse the repository at this point in the history

  2. Review comments

    @bclement-ocp
    bclement-ocp committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    b9fab02 View commit details
    Browse the repository at this point in the history

  3. Add _bitlist prefix

    @bclement-ocp
    bclement-ocp committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    96e99bd View commit details
    Browse the repository at this point in the history

  4. Fix typo

    @bclement-ocp
    bclement-ocp committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    a8772c2 View commit details
    Browse the repository at this point in the history

  5. Add documentation

    @bclement-ocp
    bclement-ocp committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    5000254 View commit details
    Browse the repository at this point in the history

  6. Mention exception

    @bclement-ocp
    bclement-ocp committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    7ef7477 View commit details
    Browse the repository at this point in the history

  7. Remove obsolete argument from doc

    @bclement-ocp
    bclement-ocp committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    13a695c View commit details
    Browse the repository at this point in the history

  8. Bitlist_domains

    @bclement-ocp
    bclement-ocp committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    143b640 View commit details
    Browse the repository at this point in the history