package mc2

You can search for identifiers within the package.

in-package search v0.2.0

mc2.backend
- Mc2_backend
  - Backend_intf
    
    S
  - Dot
    
    Arg
    
    Default
    
    Make
    
    A
mc2.core
- Mc2_core
  - Actions
  - Atom
  - Bound_var
  - Builtins
  - Clause
  - Error
  - ID
    
    Smtlib
  - Lemma
    
    TC
  - Plugin
    
    Factory
    
    S
  - Proof
  - Service
    
    Key
    
    Registry
  - Solver
    
    Sat_state
    
    Unsat_state
  - Statement
  - Term
    
    Bool
    
    TC
    
    TERM_ALLOC
    
    TERM_ALLOC_OPS
    
    Term_allocator
    
    T
    
    Watch1
    
    Watch2
  - Tseitin
    
    Arg
    
    Make
    
    F
    
    S
  - Type
    
    Alloc
    
    T
    
    TC
    
    TY_ALLOC_OPS
  - Value
    
    TC
mc2.dimacs
- Mc2_dimacs
  - Plugin_sat
mc2.lra
- Mc2_lra
  - LE
    
    Infix
mc2.propositional
- Mc2_propositional
  - F
mc2.smtlib
- Mc2_smtlib
  - Make
    
    ARG
  - Typecheck
    
    Make
    
    ARG
mc2.uf
- Mc2_uf
mc2.unin_sort
- Mc2_unin_sort

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

Tseitin's CNF conversion.