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"             {>= "4.14.0"}
  "base"              {= "v0.17~preview.129.11+135"}
  "hardcaml"          {= "v0.17~preview.129.11+135"}
  "hardcaml_waveterm" {= "v0.17~preview.129.11+135"}
  "ppx_hardcaml"      {= "v0.17~preview.129.11+135"}
  "ppx_jane"          {= "v0.17~preview.129.11+135"}
  "stdio"             {= "v0.17~preview.129.11+135"}
  "dune"              {>= "2.0.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/0f6093a48f15164cacd2deb7443f1bb89bc56cca.tar.gz"
checksum: "sha256=07c3e9cbe53b4ff617a22f85db3e92d0b512711ed298469e01e93c60be82aff7"
}

flags: deprecated
post-messages: [
  "IMPORTANT: The bleeding edge repository mirror on ocaml.janestreet.com is being deprecated in favor of our official GitHub repository."
  "To ensure you receive the latest packages and updates, please update your repository URL by running:"
  "  opam repo set-url janestreet-bleeding https://github.com/janestreet/opam-repository.git"
]