Skip to content

Conversation

@filipeom
Copy link
Contributor

smtml.0.13.0

An SMT solver frontend for OCaml
Smt.ml is an SMT solver frontend for OCaml that simplifies integration with various solvers through a consistent interface. Its parametric encoding facilitates the easy addition of new solver backends, while optimisations like formula simplification, result caching, and detailed error feedback enhance performance and usability.



Git shortlog

Filipe Marques (4):
      Unpin opam-publish in publish CI
      Expose a solver's `M_with_make` as part of the solver mappings
      Expose solver mappings to declare non-parametric datatypes
      Bump ocamlformat 0.27.0 -> 0.28.1

github-actions[bot] (1):
      Release 0.13.0

hra687261 (10):
      Fix the order of formulas printed by the z3 mapping printer
      Replace Format with Fmt
      Rename Expr.pp_smt to Expr.pp_smtml
      Add the to-smtml command
      Parse "signed" operations the way they are printed (with the `_s` at the end)
      No commas between asserts in smtml format
      upd examples.mld
      Prettier formatting for printing in the smtml format
      Properly print bvs and floats and ensure that they can be parsed
      Use the the hex format to print and parse floats

🐫 Pull-request generated by opam-publish v2.7.0

Copy link
Member

@jmid jmid left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, LGTM!

@dinosaure
Copy link
Contributor

Thanks!

@dinosaure dinosaure merged commit 47abc0a into ocaml:master Oct 27, 2025
3 of 4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants