package hardcaml

  1. Overview
  2. Docs
package hardcaml
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.

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