Add CoBRA simplifier backend and simplify chain composition - #7
Open
mrexodia wants to merge 5 commits into
Open
Conversation
Add a CobraBackend built on the cobra-mba crate (binsnake/cobra), using the same maximal-island extraction as the Rumba backend: the structural skeleton of the target expression is copied verbatim while each maximal same-width MBA island is handed to CoBRA's worklist pipeline, with non-MBA subtrees abstracted as opaque boundary variables. Logical right-shifts by a constant amount convert into islands as well. By default the backend only adopts rewrites CoBRA backs with a replayable Lean certificate, declining everything weaker (including the probe-verified side paths), so unsupported islands fall back to a structural copy. A spot-checked constructor trades that guarantee for a higher simplification rate on non-adversarial inputs. A new SimplifyChainBackend composes simplifiers by feeding each stage the previous stage's output and skipping stages that decline; the shipped server now routes SIMPLIFY through Rumba then CoBRA. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015FYCZ18U7J69pBs3QxKoGG
CI runs clippy from the latest stable toolchain (1.98), whose new chunks_exact_to_as_chunks lint rejects the constant-size chunks_exact call in parse_annotation and fails the workspace-wide -D warnings gate on every run. Use as_chunks::<2>() as the lint suggests. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015FYCZ18U7J69pBs3QxKoGG
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: be9d03ed20
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
A cancelled request previously broke out of the stage loop and returned the last good block as a conclusive SIMPLIFIED result. Follow the backend cancellation convention instead: any observed cancellation yields an inconclusive UNKNOWN, so a racing layer never adopts a vacuous identity simplification from a cancelled chain. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015FYCZ18U7J69pBs3QxKoGG
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3673f7b4b1
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
The pre-stage cancellation check has no next iteration to run after the last stage, so cancellation arriving mid-flight in that stage was swallowed and the chain still answered with the last good block as a conclusive SIMPLIFIED result. Re-check the context after the stage loop and return the inconclusive cancellation result there too. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015FYCZ18U7J69pBs3QxKoGG
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 9141605097
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
A declined maximal island was retried on every nested subtree, and the tree conversion re-expands shared wire DAG nodes on each visit, so an adversarial unsimplifiable expression could turn one bounded request into quadratic (or, through sharing, exponential) conversion work with unbounded repeat runs of CoBRA's search pipeline. Give each request a node-visit budget shared across all island attempts, sized from the input's node count; once spent, remaining islands are copied structurally. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015FYCZ18U7J69pBs3QxKoGG
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.
Summary
This PR adds a new CoBRA-based simplifier backend to the SMT server and introduces a simplify chain mechanism for composing multiple simplifier backends in sequence.
Key Changes
New CoBRA Backend (
cobra_backend.rs): Implements a simplifier backend built on CoBRA, a worklist-driven mixed Boolean-arithmetic (MBA) simplifier. The backend:Simplify Chain Backend (
simplify_chain.rs): Enables sequential composition of simplifier backends where:Integration: Updated library exports and main server configuration to include the new backends
Tests (
cobra_simplify.rs): Comprehensive test suite covering:Implementation Details
__cobra_boundaryprefix with underscore disambiguation to avoid collisions with real variableshttps://claude.ai/code/session_015FYCZ18U7J69pBs3QxKoGG