Support forall in annotation#141
Conversation
There was a problem hiding this comment.
Pull request overview
This PR adds support for forall in Thrust annotations (mirroring existing exists support), including end-to-end translation into CHC formulas and SMT-LIB2 output, plus UI tests to validate both satisfiable and unsatisfiable cases.
Changes:
- Introduces
thrust_models::foralland resolves it via a newforall_path+DefIdCache::forall()lookup. - Extends CHC AST/printing to represent and emit
forall(Formula::Forall) and generalizes quantified variables (Term::FormulaQuantifiedVar). - Adds UI pass/fail tests exercising
forallinside#[thrust_macros::ensures(...)].
Reviewed changes
Copilot reviewed 12 out of 12 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| tests/ui/pass/annot_forall.rs | Adds a passing UI test using forall in an ensures annotation. |
| tests/ui/fail/annot_forall.rs | Adds a failing UI test expecting an Unsat outcome for a forall annotation. |
| std.rs | Adds thrust_models::forall annotated with #[thrust::def::forall]. |
| src/rty.rs | Ensures type-parameter substitution traverses Formula::Forall and uses the renamed quantified-var term. |
| src/chc/unbox.rs | Adds unboxing support for Formula::Forall and renames the quantified-var term. |
| src/chc/smtlib2.rs | Emits SMT-LIB2 for forall and renames the quantified-var term printing. |
| src/chc/format_context.rs | Updates sort-collection logic for the renamed quantified-var term. |
| src/chc.rs | Adds Formula::Forall, pretty-printing, and renames the quantified-var term (but currently has pattern-matching compile issues). |
| src/annot.rs | Uses FormulaQuantifiedVar for sorted identifiers in annotations. |
| src/analyze/did_cache.rs | Caches and exposes the forall DefId lookup. |
| src/analyze/annot.rs | Adds forall_path() attribute path helper. |
| src/analyze/annot_fn.rs | Translates `forall( |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
![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: 78631c839e
ℹ️ 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".
supported in PCSat in the same way as existentials