Support quantifiers in cvc5 and bitwuzla (#662) - #669
Open
filipeom wants to merge 1 commit into
Open
Conversation
📝 WalkthroughSummary by CodeRabbit
WalkthroughChangesQuantified term support
Estimated code review effort: 3 (Moderate) | ~25 minutes 🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🧹 Nitpick comments (1)
src/smtml/dolmenexpr_to_expr.mli (1)
63-63: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winComplete odoc documentation for the new quantifier APIs.
Both interface additions expose public functions without the required parameter and return documentation.
src/smtml/dolmenexpr_to_expr.mli#L63-L63: documentvarwith@paramand@returntags.src/smtml/typed.mli#L142-L147: documentvars,e, and the return value forforallandexists.As per path instructions, interface files must fully document public functions.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@src/smtml/dolmenexpr_to_expr.mli` at line 63, The public quantifier APIs lack complete odoc parameter and return documentation. In src/smtml/dolmenexpr_to_expr.mli lines 63-63, document var’s string and ty parameters and returned term; in src/smtml/typed.mli lines 142-147, document vars and e plus the return values of forall and exists, without changing their signatures or behavior.Source: Path instructions
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@test/regression/test_issue_662.ml`:
- Line 1: Add the repository-standard SPDX, copyright, and author header to
test_issue_662.ml, followed by a top-level (** ... *) module documentation
comment before the existing Smtml.Typed.Bitv32.symbol declaration.
- Around line 12-16: Update both backend result matches in test_issue_662.ml to
succeed only for Sat and fail the regression for Unsat or Unknown. Extend the
regression with a universally quantified unsatisfiable case that ensures the
tested variable is actually bound, and assert that both backends return Sat for
the intended cases while preserving explicit failure for unexpected results.
---
Nitpick comments:
In `@src/smtml/dolmenexpr_to_expr.mli`:
- Line 63: The public quantifier APIs lack complete odoc parameter and return
documentation. In src/smtml/dolmenexpr_to_expr.mli lines 63-63, document var’s
string and ty parameters and returned term; in src/smtml/typed.mli lines
142-147, document vars and e plus the return values of forall and exists,
without changing their signatures or behavior.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro Plus
Run ID: 80f1a65b-5543-466e-b6ef-93b8fe9daa62
📒 Files selected for processing (12)
src/smtml/bitwuzla_mappings.default.mlsrc/smtml/cvc5_mappings.default.mlsrc/smtml/dolmenexpr_to_expr.mlsrc/smtml/dolmenexpr_to_expr.mlisrc/smtml/mappings.mlsrc/smtml/mappings.nop.mlsrc/smtml/mappings_intf.mlsrc/smtml/typed.mlsrc/smtml/typed.mlisrc/smtml/z3_mappings.default.mltest/regression/dunetest/regression/test_issue_662.ml
| @@ -0,0 +1,26 @@ | |||
| let x = Smtml.Typed.Bitv32.symbol (Smtml.Symbol.make (Smtml.Ty.Ty_bitv 32) "x") | |||
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Add the required OCaml file header and module documentation.
This new .ml file is missing the SPDX, copyright, author header, and top-level (** ... *) module comment.
As per path instructions, every new .ml/.mli file must include these headers. Based on learnings, new OCaml modules in this repository also require a top-level module documentation comment.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@test/regression/test_issue_662.ml` at line 1, Add the repository-standard
SPDX, copyright, and author header to test_issue_662.ml, followed by a top-level
(** ... *) module documentation comment before the existing
Smtml.Typed.Bitv32.symbol declaration.
Sources: Path instructions, Learnings
Comment on lines
+12
to
+16
| let () = | ||
| match CVC5.check solver [ Smtml.Typed.Unsafe.unwrap expr ] with | ||
| | `Sat -> Format.printf "SAT@\n" | ||
| | `Unsat -> Format.printf "UNSAT@\n" | ||
| | `Unknown -> Format.printf "UNKNOWN@\n" |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
Assert that both backends return Sat.
Both matches only print Unsat or Unknown and then exit successfully, so Dune treats the regression as passing even when quantifier encoding is wrong. Fail on any result other than Sat; add a universal unsatisfiable case to ensure the variable is actually bound.
As per path instructions, regression tests should cover expected results and error paths.
Also applies to: 22-26
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@test/regression/test_issue_662.ml` around lines 12 - 16, Update both backend
result matches in test_issue_662.ml to succeed only for Sat and fail the
regression for Unsat or Unknown. Extend the regression with a universally
quantified unsatisfiable case that ensures the tested variable is actually
bound, and assert that both backends return Sat for the intended cases while
preserving explicit failure for unexpected results.
Source: Path instructions
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.
Closes #662