package hardcaml_verify

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

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.

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

module Disjunction : sig ... end

A collection of literals which are OR'd together.

module Conjunction : sig ... end

A collection of disjunctions which are AND'd together.

type t
val sexp_of_t : t -> Sexplib0.Sexp.t
val (~:) : Literal.t -> Literal.t

Not of a literal.

val create : Conjunction.t -> t

Create CNF from a Conjunction.t.

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

Fold over each disjunction in CNF

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

Iter over each disjunction in CNF

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

val number_of_variables : t -> Base.int

Total number of variables in the CNF

val number_of_clauses : t -> Base.int

Total number of clauses in the CNF.

module type Model = sig ... end
module Model_with_bits : sig ... end
module Model_with_vectors : sig ... end