Stabilize fs_dice Base-3: feed all enodes to e-matching under relevancy#1
Draft
CanCebeci wants to merge 2 commits into
Draft
Stabilize fs_dice Base-3: feed all enodes to e-matching under relevancy#1CanCebeci wants to merge 2 commits into
CanCebeci wants to merge 2 commits into
Conversation
When smt.case_split 3 (CS_RELEVANCY) is active, enodes in unexplored ControlFlow branches are never marked as relevant, preventing the MAM (Multi-pattern Abstract Machine) from matching them. This creates a circular dependency: the proof requires instantiating quantifiers that match these enodes, but the enodes are never processed because their containing branch is never explored. As a last resort before giving up with UNKNOWN, perform one full rematch pass including irrelevant enodes. This allows the solver to discover critical quantifier instances that would otherwise be missed, then restart search to propagate them. Fixes outcome instability in WFProperSplitBucketInList.smt2 where different random seeds caused some runs to return unsat (when relevancy happened to reach the critical branch) and others unknown (when it did not). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…se-3 Under relevancy the ho_matching plugin's propagate() only bulk-feeds newly created enodes to the pattern-matching machine (mam) when relevancy is disabled; otherwise the matcher receives enodes solely through relevancy-driven relevant_eh callbacks. Which trigger terms reach e-matching therefore depends on the relevancy-propagation / boolean-assignment order. Mutation (reseed/rename/shuffle) perturbs that order, so the enodes needed for the refuting quantifier instantiations reach the matcher in some mutants (unsat) but not others, where e-matching saturates and returns unknown -- i.e. outcome instability. fs_dice Base-3.smt2 (smt.relevancy 2, smt.mbqi false, smt.case_split 3) exhibits this: on the clean baseline the query and most reseed/rename/ shuffle mutants return unknown, while a few shuffles return unsat. The refutation is built over many instantiation "layers" (each instance produces terms that trigger the next), so the existing last-resort single irrelevant rematch in check_model is insufficient here. Feed newly created enodes to mam whenever e-matching is enabled, regardless of relevancy, so e-matching is no longer starved by the relevancy-propagation order and instantiations proceed layer by layer during normal search. With this change all 31 mariposa mutants reach unsat (0 unknown); the few that exceed the 60s wall-clock under 31-way parallel load still terminate with unsat given more time. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
CanCebeci
force-pushed
the
branch-isolation-debugging-clean
branch
from
fa027a6 to
fc8754a
Compare
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.
Query
query/fs_dice-queries/Base-3.smt2(options:smt.relevancy 2,smt.mbqi false,smt.case_split 3).Symptom: outcome instability
On the clean baseline, Mariposa (reseed/rename/shuffle, 31 mutants) returns a mix of unsat and unknown — the original query and all reseed/rename mutants are
unknown; only a few shuffles areunsat.branch-isolation-debugging-clean)The 6 timeouts are slow-but-solvable: they exceed Mariposa's 60s wall-clock only under 31-way parallel CPU contention; standalone they return
unsat(e.g. one such mutant solves in ~50s). No mutant returnsunknownorsat.Root cause
The
ho_matchingplugin'spropagate()only bulk-feeds newly created enodes to the pattern-matching machine (mam) when relevancy is disabled:Under relevancy,
mamreceives enodes solely through relevancy-drivenrelevant_ehcallbacks, so which trigger terms reach e-matching depends on the relevancy-propagation / boolean-assignment order. Mutation perturbs that order, so the enodes needed for the refuting quantifier instantiations reach the matcher in some mutants (→unsat) but not others, where e-matching saturates and gives up withunknown.Direct evidence
On the same isolated failing mutant (
unknown_mutant.smt2):unknownin 3.2s, saturates at 31,561 quant-instantiations (reaches final-check, out of relevant terms — not blocked by any cost/generation threshold).unsatin 8.8s, 65,319 quant-instantiations.Feeding the previously-withheld (irrelevant-but-present) enodes to
mamis exactly what lets e-matching find the refuting instantiations.Why not the existing last-resort rematch
fa027a633added a single irrelevantmam->rematch(true)incheck_modelbefore returningUNKNOWN. That fixes single-layer cases, but Base-3's refutation is built over many instantiation layers (each instance produces terms that trigger the next). Generalising that fix to repeat the rematch per layer requires one full restart per layer — a restart storm that does not converge here. Feeding enodes continuously inpropagate()instead lets instantiations proceed layer-by-layer during normal search.Fix
Feed newly created enodes to
mamwhenever e-matching is enabled, regardless of relevancy:Tradeoff / notes
This makes e-matching relevancy-independent, so under relevancy some terms that relevancy would have filtered are now matched (more instantiations, potentially slower on some queries). Draft for review: an alternative would be to gate this on
smt.case_split == CS_RELEVANCYto limit the behavior change. Soundness is unaffected (e-matching only adds valid instances); no mutant produced a wrongsat.