package hardcaml

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type path =
  1. | True
  2. | P of atomic_proposition
  3. | Pn of atomic_proposition
  4. | And of path * path
  5. | Or of path * path
  6. | Not of path
  7. | X of path
  8. | U of path * path
  9. | R of path * path
  10. | F of path
  11. | G of path
val sexp_of_path : path -> Sexplib0.Sexp.t
val vdd : path

True

val gnd : path

False

Proposition

val (&:) : path -> path -> path

And

val (|:) : path -> path -> path

Or

val (~:) : path -> path

Not

val (^:) : path -> path -> path

Xor

val (==>:) : path -> path -> path

Implication

val (<>:) : path -> path -> path

Does not equal

val (==:) : path -> path -> path

Equals

val x : ?n:int -> path -> path

In the next step

val u : path -> path -> path

In u a b a holds at least until b holds

val r : path -> path -> path

Release

val f : path -> path

Finally(/eventually)

val g : path -> path

Globally/(always)

val w : path -> path -> path

Weak until

val to_string : ?name:(atomic_proposition -> string) -> path -> string

Convert property to a string

val atomic_propositions : path -> atomic_proposition list

Find all atomic propositions in the formula

val map_atomic_propositions : path -> f:(atomic_proposition -> atomic_proposition) -> path

Apply f to all atomic propositions in the formula

val depth : path -> int

Maximum nested depth of formula

val nnf : path -> path

Convert to negative normal form.

val limit_depth : int -> path -> path

Rewrite the formula only look a limited distance into the future.