Module Mc2_propositional.FSource

Formulas

Sourcetype combinator =
  1. | And
  2. | Or
  3. | Not
Sourcetype id
Sourcetype t = private {
  1. id : id;
  2. view : view;
}
Sourceand 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.

    *)
Sourceval view : t -> view
Sourceval true_ : t

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

Sourceval false_ : t

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

Sourceval atom : Mc2_core.atom -> t

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

Sourceval not_ : t -> t

Creates the negation of a boolean formula.

Sourceval and_ : t list -> t

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

Sourceval or_ : t list -> t

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

Sourceval xor : t -> t -> t

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

Sourceval imply : t -> t -> t

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

Sourceval imply_l : t list -> t -> t
Sourceval equiv : t -> t -> t

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

Sourceval 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

pp fmt f prints the formula on the formatter fmt.