package msat

You can search for identifiers within the package.

in-package search v0.2.0

msat
- Msat
  - Make_cdcl_t
    
    Atom
    
    Clause
    
    Tbl
    
    Proof
    
    Tbl
    
    Th
    
    Formula
    
    Value
  - Make_mcsat
    
    Atom
    
    Clause
    
    Tbl
    
    Proof
    
    Tbl
    
    Th
    
    Formula
    
    Term
    
    Value
    
    Value
  - Make_pure_sat
    
    Atom
    
    Clause
    
    Tbl
    
    Proof
    
    Tbl
    
    Th
    
    Formula
    
    Value
  - Solver_intf
    
    EXPR
    
    Formula
    
    Term
    
    Value
    
    FORMULA
    
    PLUGIN_CDCL_T
    
    Formula
    
    PLUGIN_MCSAT
    
    Formula
    
    Term
    
    Value
    
    PLUGIN_SAT
    
    Formula
    
    PROOF
    
    Tbl
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
msat.backend
- Msat_backend
  - Backend_intf
    
    S
  - Coq
    
    Arg
    
    Make
    
    A
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
    
    Simple
    
    A
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
  - Dedukti
    
    Arg
    
    Make
    
    A
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
  - Dot
    
    Arg
    
    Default
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
    
    Make
    
    A
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
    
    Simple
    
    A
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
msat.backtrack
- Msat_backtrack
  - Ref
msat.sat
- Msat_sat
  - Atom
  - Clause
    
    Tbl
  - Formula
  - Int_lit
  - Proof
    
    Tbl
  - Term
  - Value
msat.tseitin
- Msat_tseitin
  - Arg
  - Make
    
    F
  - S

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.