Skip to content

Clean up warrowing box - #891

Merged
sim642 merged 7 commits into
masterfrom
rm-box
Jan 16, 2023
Merged

sim642 merged 7 commits into
masterfrom
rm-box

Conversation

@sim642

@sim642 sim642 commented Nov 8, 2022

Copy link
Copy Markdown
Member

Currently the constraint system has a box function, which is always defined to just be warrowing, and at one point that is passed on via the box argument of solve in solvers.
This is redundant because solvers then have access to box in two different ways. Also the fixed box doesn't need to be carried around everywhere.

Therefore, this removes box both from the constraint system and solver argument.
SLR is the only solver that in some variation overrides box to just widen or narrow, making the argument also irrelevant. Since the choice of box is such a solver-specific thing, it makes the most sense to just do it directly in the solver in a way that's supported by the solver.

@sim642 sim642 added the cleanup Refactoring, clean-up label Nov 8, 2022
@sim642 sim642 added this to the v2.1.0 milestone Nov 8, 2022
@sim642 sim642 modified the milestones: v2.1.0, v2.2.0 Nov 21, 2022
@michael-schwarz

Copy link
Copy Markdown
Member

@jerhard or @stilscher, could you have a look? You guys know more about the intricacies of the solver.

Comment thread src/solvers/sLR.ml
@sim642
sim642 merged commit b9f527f into master Jan 16, 2023
@sim642
sim642 deleted the rm-box branch January 16, 2023 14:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

cleanup Refactoring, clean-up

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants