package mc2

You can search for identifiers within the package.

in-package search v0.2.0

mc2
- Library mc2.backend
  - Mc2_backend
    
    Backend_intf
    
    S
    
    Dot
    
    S
    
    Arg
    
    Default
    
    Make
- Library mc2.core
  - Mc2_core
    
    Atom
    
    Tbl
    
    Set
    
    Term
    
    Bool
    
    Watch1
    
    Watch2
    
    TC
    
    TERM_ALLOC_OPS
    
    TERM_ALLOC
    
    Term_allocator
    
    Tbl
    
    Map
    
    Set
    
    Type
    
    TC
    
    TY_ALLOC_OPS
    
    Alloc
    
    Value
    
    Tbl
    
    TC
    
    Actions
    
    Builtins
    
    Clause
    
    Tbl
    
    Set
    
    Proof
    
    H
    
    Solver
    
    Sat_state
    
    Unsat_state
    
    Service
    
    Key
    
    Registry
    
    Plugin
    
    S
    
    Factory
    
    Tseitin
    
    Arg
    
    S
    
    Make
    
    ID
    
    Map
    
    Set
    
    Tbl
    
    Smtlib
    
    Lemma
    
    TC
    
    Statement
    
    Bound_var
    
    Error
    
    Fmt
    
    Int_map
- Library mc2.dimacs
  - Mc2_dimacs
    
    Plugin_sat
- Library mc2.lra
  - Mc2_lra
    
    LE
    
    Infix
- Library mc2.propositional
  - Mc2_propositional
    
    F
- Library mc2.smtlib
  - Mc2_smtlib
    
    PA
    
    Typecheck
    
    Loc
    
    PA
    
    T
    
    Stmt
    
    Make
    
    Make
- Library mc2.uf
  - Mc2_uf
- Library mc2.unin_sort
  - Mc2_unin_sort
- Sources
  - mc2.backend
    
    Dot.ml
    
    backend_intf.ml
    
    mc2_backend.ml
  - mc2.core
    
    Actions.ml
    
    Atom.ml
    
    BitField.ml
    
    Bound_var.ml
    
    Builtins.ml
    
    Clause.ml
    
    Error.ml
    
    Heap.ml
    
    Heap_intf.ml
    
    Het_map.ml
    
    ID.ml
    
    Internal.ml
    
    Lemma.ml
    
    Log.ml
    
    Mc2_core.ml
    
    Plugin.ml
    
    Premise.ml
    
    Proof.ml
    
    Reason.ml
    
    Service.ml
    
    Solver.ml
    
    Solver_types.ml
    
    Statement.ml
    
    Term.ml
    
    Tseitin.ml
    
    Tseitin_intf.ml
    
    Type.ml
    
    Util.ml
    
    Value.ml
    
    Vec.ml
    
    formula_intf.ml
    
    mc2_core__.ml
  - mc2.dimacs
    
    Lexer.ml
    
    Mc2_dimacs.ml
    
    Parser.ml
    
    Plugin_sat.ml
    
    mc2_dimacs__.ml
  - mc2.lra
    
    Linexp.ml
    
    Mc2_lra.ml
    
    mc2_lra__.ml
  - mc2.propositional
    
    Mc2_propositional.ml
  - mc2.smtlib
    
    Mc2_smtlib.ml
    
    Typecheck.ml
    
    mc2_smtlib__.ml
  - mc2.uf
    
    Mc2_uf.ml
  - mc2.unin_sort
    
    Mc2_unin_sort.ml

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

Module `Mc2_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 : 
  Arg
    with type atom := Mc2_core.Atom.t
     and type hyp := Mc2_core.Clause.t
     and type lemma := Mc2_core.Clause.t
     and type assumption := Mc2_core.Clause.t

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

Source

module Make
  (A : 
    Arg
      with type atom := Mc2_core.Atom.t
       and type hyp := Mc2_core.Clause.t
       and type lemma := Mc2_core.Clause.t
       and type assumption := Mc2_core.Clause.t) : 
  S with type t := Mc2_core.Proof.t

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

package mc2

Module Mc2_backend.DotSource

Module `Mc2_backend.Dot`Source