Module BoolFunction

module BoolFunction: sig .. end

Represent Boolean functions.

Basic Type Definition

type bool_function =

`\|`	`Fun of string * string list`
`\|`	`PosVar of string * string`
`\|`	`NegVar of string * string`
`\|`	`Not of bool_function`
`\|`	`And of bool_function list`
`\|`	`Or of bool_function list`
`\|`	`Ex of (string * string) list * bool_function`

This type describes Boolean functions

type bool_def = string * bool * (string * string) list * bool_function

Boolean definition of a function, knows whether it is a fixed-point.

val print : bool_function -> unit

Print.

Print to string.

val sprint : bool_function -> string

Another name for sprint.

val str : bool_function -> string

Print to formatter.

val fprint : Format.formatter -> bool_function -> unit

val print_def : ?print_bool:bool -> bool_def -> unit

Print definition.

Print definition to string.

val sprint_def : ?print_bool:bool -> bool_def -> string

Another name for sprint_def.

val str_def : ?print_bool:bool -> bool_def -> string

Print definition to formatter.

val fprint_def : ?print_bool:bool -> Format.formatter -> bool_def -> unit

val print_defs : ?print_bool:bool ->
       (string * string list) list * bool_def list -> unit

Print definitions.

Print definitions to string.

val sprint_defs : ?print_bool:bool ->
       (string * string list) list * bool_def list -> string

Another name for sprint_defs.

val str_defs : ?print_bool:bool ->
       (string * string list) list * bool_def list -> string

Print definitions to formatter.

val fprint_defs : ?print_bool:bool ->
       Format.formatter ->
       (string * string list) list * bool_def list -> unit

val size : ?acc:int -> bool_function -> int

Compute the size of a Boolean function.

val flatten : bool_function -> bool_function

Flatten conjunctions and disjunctions.

val triv_simp : bool_function -> bool_function

Flatten and perform trivial simplifications (e.g. absorb true, false)

val triv_simp_defs : bool_def list -> bool_def list

Trivial simplification of Boolean definitions.

val subst_mod_vars : (string * string) list ->
       bool_function -> bool_function

Substitute module variables. Simple, fails on quantifier conflicts.

val apply_defs : bool_def list ->
       bool_function -> bool_function

Insert non-fixed-point definitions into a function.

val inline_defs : bool_def list -> bool_def list

Inline all non-fixed-point definitions.

val dnf : ?tm:float ->
       (string * string list) list ->
       bool_function -> bool_function option

Convert a function to DNF with eliminated quantifiers.

val solve_lfp : ?nf:int ->
       (string * string list) list ->
       bool_def list -> bool_def list

Inline and solve fixed-points in the definitions.