Codex/decompose wrapper kill aiger - #15
Merged
Merged
Conversation
Dual of the boolean-fragment UNREAL pre-check: a one-step combinational controller win. When every guarantee is boolean-G and (exists outputs. G_bool) is valid over all inputs, the Skolem function o = f(i) is a memoryless Mealy controller that realizes the spec regardless of the environment. Verdict-trust class TRUST_UNDER: it refutes unrealizability of a *strengthening* (drops every assumption, bails on any temporal guarantee), so its REALIZABLE verdict is trustworthy and it never claims UNREALIZABLE. Mealy-only -- the Skolem controller reads the current input -- so it bails on Moore (and on finite). Exposed via a new --realizability flag: a fast verdict oracle printing REALIZABLE / UNREALIZABLE / UNKNOWN (exit 0/1/2), no plan or controller. Gated behind the flag because, unlike the terminal UNREAL verdict, REAL yields only a verdict; short-circuiting plan or --aiger mode would drop their deliverable. Corpus (2545 specs, --split): 61 REAL / 19 UNREAL / 2465 UNKNOWN; sound -- 0 REAL on a declared-unrealizable spec and 0 UNREAL on a declared-realizable one (ltlsynt confirms the unlabeled fires). 3 oracle tests; valgrind clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
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.
No description provided.