Use latest PCSat - #275
Merged
Merged
Use latest PCSat#275
Conversation
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
coeff-aij
added a commit
to coeff-aij/thrust
that referenced
this pull request
Sep 24, 2026
…casts) into forall-sort Brings in coord-e#114 (Rust expressions as thrust::predicate bodies, instantiated per generic arguments), coord-e#275 (newer PCSat in CI), coord-e#276, coord-e#277 and coord-e#278 on top of forall-sort. Resolution: - A predicate call whose instance resolves goes through Analyzer::predicate_with_args, so a Rust-body predicate is defined once per instantiation and a raw SMT-LIB2 predicate keeps its single definition. A call that does not resolve (it still depends on the owner's type parameters) keeps the forall predicate. - predicate_with_args takes the calling function as owner, since forall-sort translates type parameters relative to it; an instance whose arguments mention type parameters is keyed by that owner too. - UserDefinedPredDef keeps both the new body enum and the ForallPred dependency set. A formula body contributes its ForallPred atoms directly and its calls to other user-defined predicates as edges of the dependency graph; a raw body is still scanned by name. - The refinement clause builder records the value-variable origin only when the value term is a variable, as the singleton case substitutes a default term. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
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.
continued from #270