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

Dot backend for proofs

This module provides functions to export proofs into the dot graph format. Graphs in dot format can be used to generates images using the graphviz tool.

module type S = Backend_intf.S

Interface for exporting proofs.

module type Arg = sig ... end

Term printing for DOT

module Default
  (S : Msat.S) : 
  Arg
    with type atom := S.atom
     and type hyp := S.clause
     and type lemma := S.clause
     and type assumption := S.clause

Provides a reasonnable default to instantiate the Make functor, assuming the original printing functions are compatible with DOT html labels.

module Make
  (S : Msat.S)
  (A : 
    Arg
      with type atom := S.atom
       and type hyp := S.clause
       and type lemma := S.clause
       and type assumption := S.clause) : 
  S with type t := S.proof

Functor for making a module to export proofs to the DOT format.

module Simple
  (S : Msat.S)
  (A : 
    Arg
      with type atom := S.formula
       and type hyp = S.formula list
       and type lemma := S.lemma
       and type assumption = S.formula) : 
  S with type t := S.proof

Functor for making a module to export proofs to the DOT format. The substitution of the hyp type is non-destructive due to a restriction of destructive substitutions on earlier versions of ocaml.