package mc2

  1. Overview
  2. Docs
package mc2
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Tseitin.MakeSource

Tseitin's CNF conversion.

Parameters

module F : Arg

Signature

Sourcetype atom = F.t

The type of atomic 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 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 : 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 -> atom) -> t -> 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.

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