package hardcaml_verify

  1. Overview
  2. Docs
package hardcaml_verify
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Hardcaml_verify_kernel.CnfSource

Data structure for creating CNF formulae.

Literals are mapped to integer indexes internally so they can be easily converted to DIMACs format for input to a SAT solver, and a model constructed from the output.

Sourcemodule Literal : sig ... end

A literal is an input bit to the CNF. They are constructed with the vector and bit functions, negated with (~:) and managed as a group within a Disjunction.t.

Sourcemodule Disjunction : sig ... end

A collection of literals which are OR'd together.

Sourcemodule Conjunction : sig ... end

A collection of disjunctions which are AND'd together.

Sourcetype t
Sourceval sexp_of_t : t -> Sexplib0.Sexp.t

Not of a literal.

Sourceval create : Conjunction.t -> t

Create CNF from a Conjunction.t.

Sourceval fold : t -> init:'a -> f:('a -> Disjunction.t -> 'a) -> 'a

Fold over each disjunction in CNF

Sourceval iter : t -> f:(Disjunction.t -> Base.unit) -> Base.unit

Iter over each disjunction in CNF

Sourceval to_int_literal : t -> Literal.t -> Base.int Base.option

Get an integer representing the literal. It is negative if the literal is negated. Returns None if the literal is not in the CNF.

Sourceval number_of_variables : t -> Base.int

Total number of variables in the CNF

Sourceval number_of_clauses : t -> Base.int

Total number of clauses in the CNF.

Sourcemodule type Model = sig ... end
Sourcemodule Model_with_bits : sig ... end
Sourcemodule Model_with_vectors : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct