package msat

You can search for identifiers within the package.

in-package search v0.2.0

doc
- Library msat
  - Msat
    
    Solver_intf
    
    FORMULA
    
    EXPR
    
    Term
    
    Value
    
    Formula
    
    PLUGIN_CDCL_T
    
    Formula
    
    PLUGIN_MCSAT
    
    Term
    
    Value
    
    Formula
    
    PLUGIN_SAT
    
    Formula
    
    PROOF
    
    Tbl
    
    S
    
    Term
    
    Value
    
    Formula
    
    Atom
    
    Clause
    
    Tbl
    
    Proof
    
    Tbl
    
    S
    
    FORMULA
    
    EXPR
    
    PLUGIN_CDCL_T
    
    PLUGIN_MCSAT
    
    PROOF
    
    Make_mcsat
    
    Term
    
    Value
    
    Formula
    
    Atom
    
    Clause
    
    Tbl
    
    Proof
    
    Tbl
    
    Make_cdcl_t
    
    Term
    
    Value
    
    Formula
    
    Atom
    
    Clause
    
    Tbl
    
    Proof
    
    Tbl
    
    Make_pure_sat
    
    Term
    
    Value
    
    Formula
    
    Atom
    
    Clause
    
    Tbl
    
    Proof
    
    Tbl
- Library msat.backend
  - Msat_backend
    
    Backend_intf
    
    S
    
    Coq
    
    S
    
    Arg
    
    Make
    
    Simple
    
    Dedukti
    
    S
    
    Arg
    
    Make
    
    Dot
    
    S
    
    Arg
    
    Default
    
    Make
    
    Simple
- Library msat.backtrack
  - Msat_backtrack
    
    Ref
- Library msat.sat
  - Msat_sat
    
    Int_lit
    
    Term
    
    Value
    
    Formula
    
    Atom
    
    Clause
    
    Tbl
    
    Proof
    
    Tbl
- Library msat.tseitin
  - Msat_tseitin
    
    Arg
    
    S
    
    Make
- Sources
  - msat
    
    Heap.ml
    
    Heap_intf.ml
    
    Internal.ml
    
    Log.ml
    
    Msat.ml
    
    Solver.ml
    
    Solver_intf.ml
    
    Vec.ml
    
    msat__.ml
  - msat.backend
    
    Backend_intf.ml
    
    Coq.ml
    
    Dedukti.ml
    
    Dot.ml
    
    msat_backend.ml
  - msat.backtrack
    
    Backtrackable_ref.ml
    
    Msat_backtrack.ml
    
    msat_backtrack__.ml
  - msat.sat
    
    Int_lit.ml
    
    Msat_sat.ml
    
    msat_sat__.ml
  - msat.tseitin
    
    Msat_tseitin.ml
    
    Tseitin_intf.ml
    
    msat_tseitin__.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Msat_backend.Dot`Source

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.

Sourcemodule type S = Backend_intf.S

Interface for exporting proofs.

Sourcemodule type Arg = sig ... end

Term printing for DOT

Source

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.

Source

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.

Source

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.

package msat

Module Msat_backend.DotSource

Module `Msat_backend.Dot`Source