Skip to content

Feat int minimization - #303

Merged
tnelson merged 24 commits into
devfrom
feat_int_minimization
Apr 25, 2025
Merged

tnelson merged 24 commits into
devfrom
feat_int_minimization

Conversation

@tnelson

@tnelson tnelson commented Apr 24, 2025

Copy link
Copy Markdown
Owner

This PR implements the optimization features described here. The set-based optimization is still somewhat brittle, but the feature should be made available in preview form.

Known issues:

  • Combining a partial-instance bound and a partial-instance target is restricted and needs better documentation (e.g., the lower bound of the target must be contained in the upper bound of the run).
  • The hidden internal relations that convert an integer-optimization problem to a set-optimization problem persist between runs, even into runs that don't use integer optimization. (This is an architectural problem that will require a small amount of refactoring. Forge wasn't originally built to allow removing relations from the model.)

This PR also fixes the verbosity level that triggers collector spam for debugging; 5 ("HIGH") will no longer be enough.

Finally, this PR also expands the run-tests.sh script to no longer attempt to run the SMT backend tests if cvc5 is not on the path. (Aside: I don't have a lot of shell-script experience beyond the basics, so this is a place I would like to request extra review effort.)

@tnelson
tnelson merged commit 8a0e270 into dev Apr 25, 2025
@tnelson
tnelson deleted the feat_int_minimization branch April 25, 2025 12:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants