Prune VC content disconnected from the goal before SMT solving#407
Closed
alcides wants to merge 1 commit into
Closed
Prune VC content disconnected from the goal before SMT solving#407alcides wants to merge 1 commit into
alcides wants to merge 1 commit into
Conversation
Verification conditions accumulate every binder and refinement in scope,
even when most of them cannot affect the obligation being checked. This
adds a cone-of-influence pass in `flatten`: when building each canonic
(flattened) constraint, only the quantified variables and premises
transitively connected to the conclusion's variables (through shared
bound variables) are handed to Z3.
Dropping is done safely. Because the disconnected premises share no
variable with the kept side or the conclusion, the negated VC factors
over disjoint variable sets, so they can only affect validity by being
unsatisfiable. Before dropping them we probe their satisfiability with a
dedicated auxiliary solver: if they are contradictory the whole
obligation is vacuously valid (we emit a trivially-true constraint); if
the solver returns unknown we conservatively keep everything. This
preserves refutation-style proofs (e.g. proving `{r:Int | false}` from
contradictory hypotheses) while shrinking the formulas in the common
case.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GdAFspBnYJndsiUTYLyPK7
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.
What
Optimizes verification by ensuring each VC (verification condition) handed to Z3 only contains the variables and refinements (premises) that actually mention variables used inside the obligation. Content disconnected from the goal is dropped, avoiding useless VC content and shrinking the formulas the SMT solver has to reason about.
How
A cone-of-influence pass is added to
flatteninaeon/verification/smt.py. When building each canonic (flattened) constraint,_split_by_conepartitions the accumulated premises around the variables actually mentioned in the conclusion:Only the kept variables and premises are declared in the
CanonicConstraintsent to Z3.Correctness
Dropping premises naively is unsound for completeness: a disconnected but contradictory hypothesis set can discharge a goal (e.g. proving
{r: Int | false}from contradictory premises — the conclusion mentions no variables, so every premise looks "disconnected"). This is exactly what thelearning_axiomsrefutation tests exercise.The split is therefore made safe. Because the dropped premises share no variable with the kept side or the conclusion, the negated VC factors over disjoint variable sets — the dropped premises can only affect validity by being unsatisfiable. Before dropping them, a dedicated auxiliary Z3 solver (
_premises_satisfiable) probes their satisfiability:kept ⇒ conclusion.Premises with no variables of their own (constants like a literal
false) are always kept. The common case (everything connected) returns the original objects unchanged, so no extra solver work and identity-based memoization downstream keeps hitting.Testing
tests/smt_test.pycovering: unrelated variable/premise pruning, keeping connected premises, keeping contradictory unrelated premises (refutation), and not flipping a genuinely-invalid VC to valid.mypyandruff/format clean via pre-commit.🤖 Generated with Claude Code
Generated by Claude Code