Fix parser, powerset domains, and compound var aliases#11
Merged
Conversation
…ccesses parse_postfix_expr() unconditionally matched LParen after any expression. When `require x < 10` preceded `(x = x + 1)` on the next line, the parser treated `10(x = x + 1)` as a function call, swallowing the entire effect into the guard. Restrict the postfix LParen branch to fire only when the base expression is an Ident or Field, which are the only callable forms. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
… and choose
Replace extract_range with resolve_domain_values at 4 call sites
(encode_choose, encode_len, encode_set_membership, encode_as_set) so
set-local domains from powerset quantifiers are handled alongside ranges.
Handle empty domain (empty subset in powerset) gracefully.
Fixes multipaxos-reconfig spec which uses len({a in Q if ...}) where Q
is a powerset-bound set variable.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add whole_var_locals tracking for locals that alias an entire compound variable (e.g., inlined function arg `AnyInSet(toCheck)` where toCheck is a Dict). The Let handler detects bare Var/PrimedVar with compound z3_var_count > 1, and encode_index resolves these aliases back to the original variable's z3 vars. Fixes parallel-commits spec which uses AnyInSet(toCheck) where toCheck is Dict[Int, Bool]. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
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
1 participant
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.
Summary
Three bugs fixed, bringing symbolic checker from 49/59 to 54/59 specs (52 OK + 2 expected violations).
parse_postfix_exprunconditionally matchedLParenafter any expression, causing10\n(x = x+1)to parse as a function call10(x=x+1). Now restricted toIdentandFieldexpressions only.extract_rangefailed on set-local domains from powerset quantifiers. Addedresolve_domain_valueshelper that handles bothRangeand set-local domains, used at 4 call sites (choose, len, membership, as_set).AnyInSet(toCheck)wheretoCheckis aDictproducedLet { value: Var(idx), body: ... }which failed because bare compoundVarcan't encode to a single Z3 value. Addedwhole_var_localstracking to alias these back to the original variable.Remaining 5 failures (not bugs)
Set[Seq[T]]not yet supportedlen()on non-range set expressionTest plan
cargo fmt --checkclean🤖 Generated with Claude Code