package hardcaml_verify

You can search for identifiers within the package.

in-package search v0.2.0

Hardcaml Verification Tools

Install

Dune Dependency

github.com Readme Changelog MIT License Edit opam file Versions (3)

Authors

J

Jane Street Group, LLC

Maintainers

J

Jane Street developers

Sources

v0.17.0.tar.gz

sha256=a09a904776ad848f685afb4ebe85e0d449acb81f6f2425fccc52a3c5b76be629

doc/hardcaml_verify.kernel/Hardcaml_verify_kernel/Solver/index.html

Module `Hardcaml_verify_kernel.Solver`Source

Source

type run_solver =
  dimacs_in:Base.string ->
  result_out:Base.string ->
  Base.unit ->
  Base.unit Base.Or_error.t

Sourceval minisat : run_solver

Minisat solver

Sourceval picosat : run_solver

Picosat solver

Sourceval z3 : ?seed:Base.int -> parallel:Base.bool -> Base.unit -> run_solver

Z3 solver in DIMACs mode. parallel:true enableds parallel solving, however, as of V4.8.5 Z3 does not return a proper model.

Sourcetype 'a result = 'a Base.list Sat.t Base.Or_error.t

Sourceval sexp_of_result : ('a -> Sexplib0.Sexp.t) -> 'a result -> Sexplib0.Sexp.t

Source

val solve_with_model : 
  ?solver:run_solver ->
  ?print_model:Base.bool ->
  (module Cnf.Model with type input = 'input) ->
  Cnf.t ->
  'input result

Create intermediate files, run the given solver and return a model if satisfiable.

Source

val solve : 
  ?solver:run_solver ->
  ?print_model:Base.bool ->
  Cnf.t ->
  Cnf.Model_with_vectors.input result

package hardcaml_verify

Install

Dune Dependency

Authors

Maintainers

Sources

doc/hardcaml_verify.kernel/Hardcaml_verify_kernel/Solver/index.html

Module Hardcaml_verify_kernel.SolverSource

Module `Hardcaml_verify_kernel.Solver`Source