package msat

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

Module Msat_tseitin.MakeSource

This functor provides an implementation of Tseitin's CNF conversion.

CNF conversion

This modules converts arbitrary boolean formulas into CNF.

Parameters

module F : Arg

Signature

Sourcetype atom = F.t

The type of atomic formulas.

Sourcetype t

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 f_true : t

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

Sourceval f_false : t

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

Sourceval make_atom : atom -> t

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

Sourceval make_not : t -> t

Creates the negation of a boolean formula.

Sourceval make_and : t list -> t

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

Sourceval make_or : t list -> t

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

Sourceval make_xor : t -> t -> t

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

Sourceval make_imply : t -> t -> t

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

Sourceval make_equiv : t -> t -> t

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

Sourceval make_cnf : t -> atom list list

make_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.

Sourceval pp : Format.formatter -> t -> unit

print 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