this repo has no description
anil.recoil.org
1opam-version: "2.0"
2maintainer: "Jane Street developers"
3authors: ["Jane Street Group, LLC"]
4homepage: "https://github.com/janestreet/hardcaml_verify"
5bug-reports: "https://github.com/janestreet/hardcaml_verify/issues"
6dev-repo: "git+https://github.com/janestreet/hardcaml_verify.git"
7doc: "https://ocaml.janestreet.com/ocaml-core/latest/doc/hardcaml_verify/index.html"
8license: "MIT"
9build: [
10 ["dune" "build" "-p" name "-j" jobs]
11]
12depends: [
13 "ocaml" {>= "5.1.0"}
14 "base" {>= "v0.17" & < "v0.18"}
15 "hardcaml" {>= "v0.17" & < "v0.18"}
16 "hardcaml_waveterm" {>= "v0.17" & < "v0.18"}
17 "ppx_hardcaml" {>= "v0.17" & < "v0.18"}
18 "ppx_jane" {>= "v0.17" & < "v0.18"}
19 "stdio" {>= "v0.17" & < "v0.18"}
20 "dune" {>= "3.11.0"}
21 "re" {>= "1.8.0"}
22]
23available: arch != "arm32" & arch != "x86_32"
24synopsis: "Hardcaml Verification Tools"
25description: "
26Tools for verifying properties of Hardcaml circuits.
27
28Combinational circuits can be converted to 'conjunctive normal form' for input into SAT
29solvers via DIMAC files. Support for a few opensource solvers is integrated - minisat,
30picosat, Z3 - just ensure they are in your PATH.
31
32Circuits can also be converted to NuSMV format for advanced bounded and unbounded model
33checking tasks.
34"
35url {
36src: "https://github.com/janestreet/hardcaml_verify/archive/refs/tags/v0.17.0.tar.gz"
37checksum: "sha256=a09a904776ad848f685afb4ebe85e0d449acb81f6f2425fccc52a3c5b76be629"
38}