opam-version: "2.0"
maintainer: "Jane Street developers"
authors: ["Jane Street Group, LLC"]
homepage: "https://github.com/janestreet/hardcaml_verify"
bug-reports: "https://github.com/janestreet/hardcaml_verify/issues"
dev-repo: "git+https://github.com/janestreet/hardcaml_verify.git"
doc: "https://ocaml.janestreet.com/ocaml-core/latest/doc/hardcaml_verify/index.html"
license: "MIT"
build: [
  ["dune" "build" "-p" name "-j" jobs]
]
depends: [
  "ocaml"             {>= "5.1.0"}
  "base"              {>= "v0.17" & < "v0.18"}
  "hardcaml"          {>= "v0.17" & < "v0.18"}
  "hardcaml_waveterm" {>= "v0.17" & < "v0.18"}
  "ppx_hardcaml"      {>= "v0.17" & < "v0.18"}
  "ppx_jane"          {>= "v0.17" & < "v0.18"}
  "stdio"             {>= "v0.17" & < "v0.18"}
  "dune"              {>= "3.11.0"}
  "re"                {>= "1.8.0"}
]
available: arch != "arm32" & arch != "x86_32"
synopsis: "Hardcaml Verification Tools"
description: "
Tools for verifying properties of Hardcaml circuits.

Combinational circuits can be converted to 'conjunctive normal form' for input into SAT
solvers via DIMAC files. Support for a few opensource solvers is integrated - minisat,
picosat, Z3 - just ensure they are in your PATH.

Circuits can also be converted to NuSMV format for advanced bounded and unbounded model
checking tasks.
"
url {
src: "https://github.com/janestreet/hardcaml_verify/archive/refs/tags/v0.17.0.tar.gz"
checksum: "sha256=a09a904776ad848f685afb4ebe85e0d449acb81f6f2425fccc52a3c5b76be629"
}