Fixed bug in SMT option matching#5
Merged
strub merged 7 commits intoEasyCrypt:1.0from Feb 28, 2018
alleystoughton:1.0
Merged
Conversation
The elements of prover [...] have one of the following forms, where s is a string: s (add s to the use-only list) +s (add include s to the include/exclude list) -s (add exclude s to the include/exclude list) The include/exclude list is ordered, so that later instructions can supersede earlier ones. The use-only list was not ordered, but now is. The relative order of the use-only and include/exclude lists is irrelevant, so that, e.g., prover ["Z3" +"Alt-Ergo"] and prover [+"Alt-Ergo" "Z3"] are equivalent. The semantics is that the use-only list is first interpreted (if it's empty, one starts with the current provers as the base), and only then are the instructions of the include/exclude list applied to it, in order. There was already the special use-only instruction "ALL". Now, there is also the use-only instruction "CLEAR", which clears the use-only list, but may be superseded by the use-only instructions that follow. Examples (assuming "Z3" and "Alt-Ergo" are only known provers): prover []. (* a no-op *) prover [+"Z3"] (* adds just "Z3" to whatever current provers are *) prover [-"Z3"] (* removes just "Z3" from whatever current provers are *) prover ["ALL"] (* results in "Z3", "Alt-Ergo" *) prover ["CLEAR"] (* results in nothing *) prover ["CLEAR" +"Z3"] (* results in just "Z3" *) prover [+"Z3" "CLEAR"] (* results in just "Z3" *) prover ["CLEAR" "Z3"] (* result in just "Z3" *) prover ["Z3" "CLEAR"] (* results in nothing *) prover [-"Z3" "ALL"] (* results in "Alt-Ergo" *) prover [+"Z3" "ALL" -"Z3"] (* results in "Alt-Ergo" *) prover [-"Z3" "ALL" +"Z3"] (* results in "Z3", "Alt-Ergo" *)
All use-only instructions must come first. There are two "universal" use-only instructions: "" (all known provers), and "!" (no provers). It is illegal to mix ""/"!" with prover names (no point in doing so). As before, if the use-only part is empty, it means the currently known provers. The include/exclude instructions are processed in order, acting on the result of the use-only part. Examples (assuming "Z3" and "Alt-Ergo" are only known provers): prover []. (* no-op *) prover [-"Z3"]. (* removes "Z3" from current provers *) prover [+"Z3"]. (* adds "Z3" to current provers *) prover [""]. (* results in "Z3", "Alt-Ergo" *) prover ["!"]. (* results in no provers *) prover ["Z3"]. (* results in "Z3" *) prover ["Z3" "Alt-Ergo"]. (* results in "Z3", "Alt-Ergo" *) prover ["!" +"Z3"]. (* results in "Z3" *) prover ["" -"Z3"]. (* results in "Alt-Ergo" *)
The third stage of filtering in the definition of option_matching had a bug, meaning that attempts to rely on it resulted in assertion failures. But that last stage - disambiguating from right to left - was arguably hard for users to predict, anyway. So, fixed the third stage, but left it out of algorithm. (If it's really desired, easy to put it back in, as now it'll work. But do we really think users will understand why, e.g., [prover x=1] means [prover maxlemmas=1] - because the x in maxlemmas comes earlier when working backward as opposed to the x in maxprovers?) This is how option disambiguation works: First filter-in those option names having the letters of the abbreviation abv in the correct order. Then work through the letters of abv in order, keeping only those option names in which each successive letter appears as early as possible
strub
added a commit
that referenced
this pull request
Apr 30, 2026
…hange) Splits the existing TcCtt resolution logic into three named local helpers — strat_tvar_via_tvtc, strat_abs_via_decl, strat_infer_by_carrier — corresponding to catalog modes #5, #6, and #1/#2 in doc/typeclasses-inference.md. Behavior is identical: same dispatch order, same failures, same pickup of [Tvar a]/[Tconstr p] cases, same parking of univar carriers. The refactor exists so Phase 3 can drop a By-args strategy in without disturbing the existing logic.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
The third stage of filtering in the definition of option_matching had
a bug, meaning that attempts to rely on it resulted in assertion failures.
But that last stage - disambiguating from right to left - was arguably
hard for users to predict, anyway. So, fixed the third stage, but
left it out of algorithm.
(If it's really desired, easy to put it back in, as now it'll
work. But do we really think users will understand why, e.g., [prover
x=1] means [prover maxlemmas=1] - because the x in maxlemmas comes
earlier when working backward as opposed to the x in maxprovers?)
This is how option disambiguation works: First filter-in those option
names having the letters of the abbreviation abv in the correct
order. Then work through the letters of abv in order, keeping
only those option names in which each successive letter appears
as early as possible