package hardcaml_verify
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
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.Solver
Source
Source
type run_solver =
dimacs_in:Base.string ->
result_out:Base.string ->
Base.unit ->
Base.unit Base.Or_error.t
Minisat solver
Picosat solver
Z3 solver in DIMACs mode. parallel:true
enableds parallel solving, however, as of V4.8.5 Z3 does not return a proper model.
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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>