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.
Old option randomization code is (mostly) obsolete and replaced by the
--sample_strategy
, let's remove.I am not 100% sure about this. Maybe @selig wants to step in?
The new mechanism uses an external file in a domain-specific language. The language has more power for sampling (e.g., samplers for continuous domains). Also pulling the metadata out of the executable has its advantages (and some disadvantages). In any case, an external file means we can have as many samplers as we want (FOF, HOL, SMT, INDUCTION, SAT, ...) whereas the old mechanisms effort to cater for both SAT and UNS was already getting a bit messy.
The new mechanism doesn't (yet) have problem-property-dependent sampling (which the old one did), but that could be added as an extension.