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

[Bitv] Add support for the SMT-LIB2's BV primitives #669

Closed
wants to merge 37 commits into from
Closed

[Bitv] Add support for the SMT-LIB2's BV primitives #669

wants to merge 37 commits into from

Commits on Jun 19, 2023

  1. Full support of BV primitives, 1st version

    @hra687261
    hra687261 committed Jun 19, 2023
    Configuration menu
    Copy the full SHA
    3a92a55 View commit details
    Browse the repository at this point in the history

  2. Move bv smart constructors to expr.ml

    @hra687261
    hra687261 committed Jun 19, 2023
    Configuration menu
    Copy the full SHA
    05f6349 View commit details
    Browse the repository at this point in the history

Commits on Jun 20, 2023

  1. Fix mk_add in D_cnf

    @hra687261
    hra687261 committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    ebb6f1c View commit details
    Browse the repository at this point in the history

  2. Merge branch 'next' into bv-primitives

    @hra687261
    hra687261 committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    c247259 View commit details
    Browse the repository at this point in the history

  3. Move dolmen-fe only tests to tests/dolmen/...

    @hra687261
    hra687261 committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    ed5b711 View commit details
    Browse the repository at this point in the history

  4. Move the expansion of most BV ops to the theory

    @hra687261
    hra687261 committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    376fd4b View commit details
    Browse the repository at this point in the history

Commits on Jun 25, 2023

  1. Merge branch 'next' into bv-primitives-wip

    @hra687261
    hra687261 committed Jun 25, 2023
    Configuration menu
    Copy the full SHA
    94165c3 View commit details
    Browse the repository at this point in the history

Commits on Jun 26, 2023

  1. Merge branch 'OCamlPro:next' into bv-primitives

    @hra687261
    hra687261 authored Jun 26, 2023
    Configuration menu
    Copy the full SHA
    4f40a6c View commit details
    Browse the repository at this point in the history

  2. Add op comparison for bv_rotate & bv_repeat

    @hra687261
    hra687261 committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    d6a1991 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'next' into bv-primitives

    @hra687261
    hra687261 committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    2524a69 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'OCamlPro:next' into bv-primitives

    @hra687261
    hra687261 authored Jun 26, 2023
    Configuration menu
    Copy the full SHA
    5e48a02 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'OCamlPro:next' into bv-primitives

    @hra687261
    hra687261 authored Jun 26, 2023
    Configuration menu
    Copy the full SHA
    533cefd View commit details
    Browse the repository at this point in the history

  6. Update src/lib/structures/symbols.ml 

    Co-authored-by: Basile Clément <[email protected]>
    @hra687261 @bclement-ocp
    hra687261 and bclement-ocp authored Jun 26, 2023
    Configuration menu
    Copy the full SHA
    bfd9916 View commit details
    Browse the repository at this point in the history

  7. Update src/lib/structures/expr.ml 

    Co-authored-by: Basile Clément <[email protected]>
    @hra687261 @bclement-ocp
    hra687261 and bclement-ocp authored Jun 26, 2023
    Configuration menu
    Copy the full SHA
    03660ac View commit details
    Browse the repository at this point in the history

  8. Update src/lib/structures/expr.ml 

    Co-authored-by: Basile Clément <[email protected]>
    @hra687261 @bclement-ocp
    hra687261 and bclement-ocp authored Jun 26, 2023
    Configuration menu
    Copy the full SHA
    2d5877b View commit details
    Browse the repository at this point in the history

  9. Update src/lib/reasoners/bitv.ml 

    Co-authored-by: Basile Clément <[email protected]>
    @hra687261 @bclement-ocp
    hra687261 and bclement-ocp authored Jun 26, 2023
    Configuration menu
    Copy the full SHA
    818829e View commit details
    Browse the repository at this point in the history

  10. Update src/lib/reasoners/bitv.ml 

    Co-authored-by: Basile Clément <[email protected]>
    @hra687261 @bclement-ocp
    hra687261 and bclement-ocp authored Jun 26, 2023
    Configuration menu
    Copy the full SHA
    3bc686c View commit details
    Browse the repository at this point in the history

  11. Merge branch 'OCamlPro:next' into bv-primitives

    @hra687261
    hra687261 authored Jun 26, 2023
    Configuration menu
    Copy the full SHA
    0ff6b42 View commit details
    Browse the repository at this point in the history

  12. Applied some requested changes, fixed build

    @hra687261
    hra687261 committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    61cb00d View commit details
    Browse the repository at this point in the history

Commits on Jun 27, 2023

  1. More requested changes

    @hra687261
    hra687261 committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    3e2bdf9 View commit details
    Browse the repository at this point in the history

  2. Util.failwith instead of failwith, asprintf

    @hra687261
    hra687261 committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    0cb9ef9 View commit details
    Browse the repository at this point in the history

  3. Remove unused nctx

    @hra687261
    hra687261 committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    52eb884 View commit details
    Browse the repository at this point in the history

  4. revert changes to mk_add in d_cnf

    @hra687261
    hra687261 committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    1ffcf50 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'next' into bv-primitives

    @hra687261
    hra687261 committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    6d5c2a8 View commit details
    Browse the repository at this point in the history

Commits on Jun 28, 2023

  1. Fix defintions of udiv and urem

    @hra687261
    hra687261 committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    cc005ee View commit details
    Browse the repository at this point in the history

  2. Make Dolmen ignore the "shawoding" warning

    @hra687261
    hra687261 committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    ed084e6 View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2023

  1. Merge branch 'OCamlPro:next' into bv-primitives

    @hra687261
    hra687261 authored Jun 29, 2023
    Configuration menu
    Copy the full SHA
    032e315 View commit details
    Browse the repository at this point in the history

Commits on Jul 2, 2023

  1. [bitv] simply & rename mk_bvor -> mk_bvbinop

    @hra687261
    hra687261 committed Jul 2, 2023
    Configuration menu
    Copy the full SHA
    e634b55 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'OCamlPro:next' into bv-primitives

    @hra687261
    hra687261 authored Jul 2, 2023
    Configuration menu
    Copy the full SHA
    e315e82 View commit details
    Browse the repository at this point in the history

Commits on Jul 4, 2023

  1. Added failing tests

    @hra687261
    hra687261 committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    c6e9d83 View commit details
    Browse the repository at this point in the history

  2. Add failing tests

    @hra687261
    hra687261 committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    f330337 View commit details
    Browse the repository at this point in the history

  3. Fix type of mk_bvsign

    @bclement-ocp
    bclement-ocp committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    46568f3 View commit details
    Browse the repository at this point in the history

Commits on Jul 6, 2023

  1. Merge branch 'OCamlPro:next' into bv-primitives

    @hra687261
    hra687261 authored Jul 6, 2023
    Configuration menu
    Copy the full SHA
    778e332 View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2023

  1. Fail if mk_bvule or mk_bvult receive n < 0 (with n being the size… 

    … of the bit-vectors they are called on)
    @hra687261
    hra687261 committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    0405db3 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'OCamlPro:next' into bv-primitives

    @hra687261
    hra687261 authored Jul 10, 2023
    Configuration menu
    Copy the full SHA
    be74d71 View commit details
    Browse the repository at this point in the history

  3. Type fix

    @bclement-ocp
    bclement-ocp committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    a0b2910 View commit details
    Browse the repository at this point in the history

  4. [bitv] Proper bvnot support

    @bclement-ocp
    bclement-ocp committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    9c2758e View commit details
    Browse the repository at this point in the history