Module Function.Dnf

A representation of the disjunctive normal form (DNF) and related operations for this component.

include Custom.T
type t
val dump : Stdlib.Format.formatter -> t -> unit
val check : t -> unit
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
type atom = Node.t * Node.t

The type of atoms in the Boolean combinations

type mono

The type of Boolean combinations of atoms.

type line = Times.Dnf.line

An explicit representation of conjunctions of atoms.

type dnf = Times.Dnf.dnf

An explicit representation of the DNF of atoms.

val atom : atom -> t
val mono : mono -> t
val mono_dnf : mono -> dnf
val any : t
val empty : t
val cup : t -> t -> t
val cap : t -> t -> t
val diff : t -> t -> t
val neg : t -> t
val get : t -> dnf
val get_mono : t -> mono
val iter : (atom -> unit) -> t -> unit
val compute : empty:'b -> any:'b -> cup:('b -> 'b -> 'b) -> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) -> atom:(atom -> 'b) -> t -> 'b
val var : Cduce_types.Var.t -> t

Polymorphic interface.

val get_partial : t -> ((Cduce_types.Var.t list * Cduce_types.Var.t list) * mono) list
val get_full : t -> ((Cduce_types.Var.t list * Cduce_types.Var.t list) * line) list
val iter_partial : (Cduce_types.Var.t -> unit) -> (mono -> unit) -> t -> unit
val iter_full : (Cduce_types.Var.t -> unit) -> (atom -> unit) -> t -> unit
val compute_partial : empty:'b -> any:'b -> cup:('b -> 'b -> 'b) -> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) -> mono:(mono -> 'b) -> var:(Cduce_types.Var.t -> 'b) -> t -> 'b
val compute_full : empty:'b -> any:'b -> cup:('b -> 'b -> 'b) -> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) -> atom:(atom -> 'b) -> var:(Cduce_types.Var.t -> 'b) -> t -> 'b
module Infix : sig ... end