package hardcaml_verify

  1. Overview
  2. Docs
Hardcaml Verification Tools

Install

Dune Dependency

Authors

Maintainers

Sources

v0.17.0.tar.gz
sha256=a09a904776ad848f685afb4ebe85e0d449acb81f6f2425fccc52a3c5b76be629

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

Module Hardcaml_verify_kernel.SolverSource

Sourcetype 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.

Sourceval sexp_of_result : ('a -> Sexplib0.Sexp.t) -> 'a result -> Sexplib0.Sexp.t
Sourceval 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.

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

Innovation. Community. Security.