# package mc2

Legend:
Library
Module
Module type
Parameter
Class
Class type

Formulas

`type combinator = `
1. `| And`
2. `| Or`
3. `| Not`
`type id`
`type t = private {`
1. `id : id;`
2. `view : view;`
`}`
`and view = `
1. `| True`
2. `| Lit of Mc2_core.atom`
3. `| Comb of combinator * t list`
(*

The type of arbitrary boolean formulas. Arbitrary boolean formulas can be built using functions in this module, and then converted to a CNF, which is a list of clauses that only use atomic formulas.

*)
`val view : t -> view`
`val true_ : t`

The `true` formula, i.e a formula that is always satisfied.

`val false_ : t`

The `false` formula, i.e a formula that cannot be satisfied.

`val atom : Mc2_core.atom -> t`

`atom p` builds the boolean formula equivalent to the atomic formula `p`.

`val not_ : t -> t`

Creates the negation of a boolean formula.

`val and_ : t list -> t`

Creates the conjunction of a list of formulas. An empty conjunction is always satisfied.

`val or_ : t list -> t`

Creates the disjunction of a list of formulas. An empty disjunction is never satisfied.

`val xor : t -> t -> t`

`xor p q` creates the boolean formula "`p` xor `q`".

`val imply : t -> t -> t`

`imply p q` creates the boolean formula "`p` implies `q`".

`val imply_l : t list -> t -> t`
`val equiv : t -> t -> t`

`equiv p q` creates the boolena formula "`p` is equivalent to `q`".

```val cnf : ?simplify:bool -> fresh:(unit -> Mc2_core.atom) -> t -> Mc2_core.atom list list```

`cnf f` returns a conjunctive normal form of `f` under the form: a list (which is a conjunction) of lists (which are disjunctions) of atomic formulas.

• parameter fresh

used to generate fresh atoms to name formulas

• parameter simplify

if true (default) simplifiy formula

`val pp : t CCFormat.printer`

`pp fmt f` prints the formula on the formatter `fmt`.

Innovation. Community. Security.

##### Ecosystem
Packages Community Events OCaml Planet Jobs
##### Policies
Carbon Footprint Governance Privacy Code of Conduct