package msat

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

Tseitin CNF conversion

This modules implements Tseitin's Conjunctive Normal Form conversion, i.e. the ability to transform an arbitrary boolean formula into an equi-satisfiable CNF, that can then be fed to a SAT/SMT/McSat solver.

module type Arg = sig ... end

The implementation of formulas required to implement Tseitin's CNF conversion.

module type S = sig ... end

The exposed interface of Tseitin's CNF conversion.

module Make (F : Arg) : S with type atom = F.t

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