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

Jump to bottom

refactor(BV): Merge Congruence and Constraints #1010

Merged
merged 4 commits into from
Jan 10, 2024
Merged

refactor(BV): Merge Congruence and Constraints #1010

merged 4 commits into from
Jan 10, 2024

Commits on Jan 9, 2024

  1. refactor(BV): Hide constraint representation 

    This patch makes the representation of bit-vector constraints abstract.
This is preparatory work for further refactoring, as there is no reason
to expose it outside of the `Constraint` module.
    @bclement-ocp
    bclement-ocp committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    9e1008d View commit details
    Browse the repository at this point in the history

  2. refactor(BV): Extract signature of the Constraint module 

    This is in preparation of further refactoring work to make `Constraints`
a functor.
    @bclement-ocp
    bclement-ocp committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    9a43a23 View commit details
    Browse the repository at this point in the history

  3. refactor(BV): Fold Congruence into Constraints 

    In OCamlPro#944, the `Congruence` module was added to simplify handling
dependences for both domains and constraints, because we tracked domains
separately for all terms.

After OCamlPro#1004, we now track domains only for uninterpreted leaves, and the
`Congruence` module is only used for `Constraints`. This leads to a sort
of double indirection: the `Congruence` module keeps track of reverse
uninterpreted leaves -> class representative dependencies, and then the
`Constraints` module keeps track of reverse class representative ->
constraint dependencies.

This patch removes the `Congruence` module entirely; instead, the
`Constraints` module is now keeping track of reverse uninterpreted
leaves -> constraint dependencies directly.

Further refactoring work will move the `Congruence` module to
`Rel_utils` as it can be a generally useful module for other theories.
    @bclement-ocp
    bclement-ocp committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    ae1f6df View commit details
    Browse the repository at this point in the history

  4. refactor(CP): Generalize Constraints module 

    This patch moves the `Constraints` module from the BV theory to the
`Rel_utils` theory and make it a functor. This makes it independent from
the implementation of BV constraints and makes it useable in other
theories in the future.
    @bclement-ocp
    bclement-ocp committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    ea5bce6 View commit details
    Browse the repository at this point in the history