package hardcaml_verify

You can search for identifiers within the package.

in-package search v0.2.0

hardcaml_verify
- Hardcaml_verify
  - Nusmv
    
    Counter_example_trace
hardcaml_verify.kernel
- Hardcaml_verify_kernel
  - Basic_gates
    
    Uid
  - Cnf
    
    Conjunction
    
    Disjunction
    
    Literal
    
    Model
    
    Model_with_bits
    
    Model_with_vectors
  - Comb_gates
    
    Signed
    
    Sop
    
    TypedMath
    
    Unsigned
    
    Uop
  - Dimacs
  - Is_one_hot
    
    Make
    
    Comb
    
    Signed
    
    Sop
    
    TypedMath
    
    Unsigned
    
    Uop
  - Label
    
    Uid
  - Nusmv
    
    Circuit_properties
    
    Counter_example_trace
    
    Output_parser
    
    Proof_result
    
    With_interface
    
    I
    
    All
    
    M
    
    Let_syntax
    
    Let_syntax
    
    Open_on_rhs
    
    Monad_infix
    
    Comb
    
    Make_comb
    
    Comb
    
    Signed
    
    Sop
    
    TypedMath
    
    Unsigned
    
    Uop
    
    Names_and_widths
    
    Of_always
    
    Of_bits
    
    Of_signal
    
    Unsafe_assoc_by_port_name
    
    O
    
    All
    
    M
    
    Let_syntax
    
    Let_syntax
    
    Open_on_rhs
    
    Monad_infix
    
    Comb
    
    Make_comb
    
    Comb
    
    Signed
    
    Sop
    
    TypedMath
    
    Unsigned
    
    Uop
    
    Names_and_widths
    
    Of_always
    
    Of_bits
    
    Of_signal
    
    Unsafe_assoc_by_port_name
  - Sat
  - Sec
    
    Equivalence_result
    
    Instantiation_ports_match
    
    Proposition
  - Solver
  - Tseitin
    
    Make
    
    B
    
    S

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