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

Support optimization for the BV theory #884

Closed
Halbaroth opened this issue Oct 13, 2023 · 2 comments · Fixed by #1165
Closed

Support optimization for the BV theory #884

Halbaroth opened this issue Oct 13, 2023 · 2 comments · Fixed by #1165
Labels
enhancement optimization This issue is related to optimization in models.
Milestone
2.6.0

Comments

@Halbaroth
Copy link
Collaborator

No description provided.

@bclement-ocp
Copy link
Collaborator

What do we need that was not in #841 ?

@Halbaroth
Copy link
Collaborator Author

I forgot to put optimization in the title ;)

@Halbaroth Halbaroth changed the title Support model generation for Bitvector Support optimized model generation for Bitvector Oct 13, 2023
@Halbaroth Halbaroth added enhancement models This issue is related to model generation. labels Oct 13, 2023
@Halbaroth Halbaroth mentioned this issue Oct 18, 2023
Closed
@Halbaroth Halbaroth changed the title Support optimized model generation for Bitvector Support optimization for the BV theory Oct 18, 2023
@Halbaroth Halbaroth added optimization This issue is related to optimization in models. and removed models This issue is related to model generation. labels Oct 18, 2023
@Halbaroth Halbaroth added this to the 2.7.0 milestone Oct 18, 2023
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Jul 16, 2024
@bclement-ocp
feat(BV, Opt): Support bit-vector optimization
91873b6 
Since we track intervals for bit-vector variables, adding support for
optimization in the bit-vector theory is fairly inconsequential.

Fixes OCamlPro#884
@bclement-ocp bclement-ocp mentioned this issue Jul 16, 2024
Merged
@Halbaroth Halbaroth modified the milestones: 2.7.0, 2.6.0 Jul 16, 2024
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Jul 17, 2024
@bclement-ocp
feat(BV, Opt): Support bit-vector optimization
c10d426 
Since we track intervals for bit-vector variables, adding support for
optimization in the bit-vector theory is fairly inconsequential.

Fixes OCamlPro#884
bclement-ocp added a commit that referenced this issue Jul 17, 2024
@bclement-ocp
feat(BV, Opt): Support bit-vector optimization (#1165)
a1f2e60 
Since we track intervals for bit-vector variables, adding support for
optimization in the bit-vector theory is fairly inconsequential.

Fixes #884
Halbaroth pushed a commit to Halbaroth/alt-ergo that referenced this issue Jul 24, 2024
@bclement-ocp @Halbaroth
feat(BV, Opt): Support bit-vector optimization (OCamlPro#1165)
98c920f 
Since we track intervals for bit-vector variables, adding support for
optimization in the bit-vector theory is fairly inconsequential.

Fixes OCamlPro#884
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement optimization This issue is related to optimization in models.
Projects
None yet
Milestone
2.6.0
Development

Successfully merging a pull request may close this issue.

feat(BV, Opt): Support bit-vector optimization bclement-ocp/alt-ergo
2 participants
@Halbaroth @bclement-ocp