Support quantifiers in cvc5 and bitwuzla (#662) - #669
Conversation
|
Warning Review limit reached
Next review available in: 34 minutes You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. How can I continue?After more reviews become available, a review can be triggered using the To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews. How do review limits work?CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window. Please refer docs for additional details. Review details⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (23)
📝 WalkthroughSummary by CodeRabbit
WalkthroughThe change adds explicit constant and variable constructors, namespace-aware encoding, and quantified expression support. CVC5 and Bitwuzla now construct ChangesQuantified term support
Estimated code review effort: 3 (Moderate) | ~30 minutes Suggested reviewers: 🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches 💡 1⚔️ Resolve merge conflicts 💡
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. 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
let x = Smtml.Typed.Bitv32.symbol (Smtml.Symbol.make (Smtml.Ty.Ty_bitv 32) "x")
let exprx = Smtml.Typed.Unsafe.unwrap (Smtml.Typed.Bitv32.lt Smtml.Typed.Bitv32.one x)
let expr = Smtml.Expr.forall [ Smtml.Typed.Unsafe.unwrap x ] exprx
module CVC5 = Smtml.Solver.Batch (Smtml.Cvc5_mappings)
let solver = CVC5.create ()
let () =
match CVC5.check solver [ expr ] with
| `Sat -> Format.printf "SAT@\n"
| `Unsat -> Format.printf "UNSAT@\n"
| `Unknown -> Format.printf "UNKNOWN@\n"
module Bitwulza = Smtml.Solver.Batch (Smtml.Bitwuzla_mappings)
let solver = Bitwulza.create ()
let () =
match Bitwulza.check solver [ expr ] with
| `Sat -> Format.printf "SAT@\n"
| `Unsat -> Format.printf "UNSAT@\n"
| `Unknown -> Format.printf "UNKNOWN@\n"
module Z3 = Smtml.Solver.Batch (Smtml.Z3_mappings)
let solver = Z3.create ()
let () =
match Z3.check solver [ expr ] with
| `Sat -> Format.printf "SAT@\n"
| `Unsat -> Format.printf "UNSAT@\n"
| `Unknown -> Format.printf "UNKNOWN@\n"
for the following code CVC5 and Bitwulza return SAT and Z3 returns UNSAT |
|
nice catch, I think this is happening because I'm only enconding the |
9d895fd to
7f327ab
Compare
| (* Ex. x != 0 is sat *) | ||
| let () = | ||
| let open Smtml in | ||
| let x = Typed.var Typed.Types.bitv32 "x" in |
There was a problem hiding this comment.
Actionable comments posted: 6
🤖 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 `@src/smtml/dolmenexpr_to_expr.ml`:
- Around line 105-107: Update the var function in the Dolmen expression mapping
to construct a Dolmen Var term instead of delegating to const, ensuring forall
and exists receive variable descriptors. Add quantifier coverage through the
Dolmen-backed mapping for both universal and existential expressions.
In `@src/smtml/mappings.ml`:
- Around line 700-704: Restrict the earlier regex-literal matches for re.all,
re.none, and re.allchar to symbols whose namespace is Term and type is
Ty_regexp. Ensure Var symbols, including variables with these names, bypass
literal handling and reach make_var through the existing namespace dispatch.
In `@src/smtml/symbol.ml`:
- Line 90: Update Symbol.Smtlib.pp to render Var symbols using their names in
binder context instead of asserting, while preserving the existing handling for
other symbol kinds. Ensure Ast.Declare_const does not pass quantified variables
through this printer as top-level declarations, and remove assert false from any
reachable Var path, retaining assertions only where the type system proves
branches unreachable.
In `@src/smtml/symbol.mli`:
- Around line 60-74: Complete the odoc documentation for the public constructors
create, make_const, make, and make_var in the symbol interface by adding `@param`
tags for every argument and an `@return` tag describing the resulting symbol.
Preserve the existing descriptions and deprecation annotation, ensuring make
receives the same complete parameter and return documentation as the other
constructors.
In `@src/smtml/typed.mli`:
- Around line 43-54: Complete the odoc documentation for the public declarations
const, var, symbol, Bool.forall, and Bool.exists by adding `@param` tags for every
argument and an `@return` tag describing the result. Preserve the existing
descriptions and deprecation annotation while documenting each function’s
parameters and returned expression.
In `@test/regression/test_issue_662.ml`:
- Around line 37-42: Update the comment above the regression test to describe
the actual formula constructed by exprx and expr: forall x. 1 < x. Leave the
test implementation unchanged.
🪄 Autofix
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: 0e450085-f960-4f77-846f-d03072cc83d8
📒 Files selected for processing (20)
docs/examples/product_mix.mlsrc/smtml/altergo_mappings.default.mlsrc/smtml/ast.mlsrc/smtml/dolmenexpr_to_expr.mlsrc/smtml/mappings.mlsrc/smtml/model.mlsrc/smtml/parser.mlysrc/smtml/symbol.mlsrc/smtml/symbol.mlisrc/smtml/typed.mlsrc/smtml/typed.mlisrc/smtml/z3_mappings.default.mltest/integration/test_solver.mltest/regression/dunetest/regression/test_issue_655.mltest/regression/test_issue_662.mltest/test_harness.mltest/unit/test_expr.mltest/unit/test_model.mltest/unit/test_smtlib_pp.ml
🚧 Files skipped from review as they are similar to previous changes (1)
- test/regression/dune
|
I think I cracked it! You can now declared quantified variables using the API: https://github.com/formalsec/smtml/pull/669/changes#r3737779666 I was unaware, but we already had a way to support this with the current API. But since it was a bit awkward to use and unknown to most, I decided to take deeper look at things and try to improve it. In particular, I'm proposing we adopt the |
7f327ab to
983ce27
Compare
Adds quantifier support in cvc5 and bitwuzla. As well as, unifies the API for creating symbols. In particular, we adopt the `const` API more commonly used in SMT solvers to replace the ambiguous `symbol` API which, with the introduction of `Symbol.make_var` and `Typed.var`, no longer made sense. In summary, API changes are summarised below: symbol.ml: - create: Ty.t -> name -> namespace -> t (was make3) - make_const: Ty.t -> string -> t (was make) - make_var: Ty.t -> string -> t (new) - make: deprecated alias for make_const typed.ml: - const: 'a ty -> string -> 'a expr (was symbol) - var: 'a ty -> string -> 'a expr (new) - symbol: deprecated alias for const BREAKING CHANGE: Creation of symbols now uses const/var convention
983ce27 to
4d1896a
Compare
2 participants
Closes #662