Add comprehensive example for Optimize set_on_model callback functionality #208
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds a new comprehensive example demonstrating how to use the
set_on_modelcallback feature with Z3'sOptimizeclass. The example was requested in issue #207 to help users understand how to monitor optimization progress and implement custom termination conditions.What's Added
A new example file
06 - Optimize with Model Callbacks.mdunder the Python Example Programs section that includes:Basic Usage: Simple callback setup for monitoring optimization progress
Multiple Objectives: Resource allocation example showing how to track model evolution with competing optimization goals
Early Termination: Custom monitoring class demonstrating how to implement termination logic based on model count or quality thresholds
MaxSAT Integration: Practical weighted MaxSAT example with solution collection and analysis, particularly useful with local search engines
External Files: Implementation based on the original issue's bare bones example, showing integration with SMT-LIB files and various optimization engine configurations
Key Benefits
The examples show how
set_on_modelcallbacks are particularly valuable when using iterative optimization engines that find many intermediate solutions during the search process.Fixes #207.
💬 Share your feedback on Copilot coding agent for the chance to win a $200 gift card! Click here to start the survey.