package mc2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Propositional Literal

package mc2

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_propositional`Source

Propositional Literal

Sourcemodule F : Mc2_core.Tseitin.S with type atom := Mc2_core.atom

Formulas

Source

val k_cnf : 
  (?simplify:bool -> F.t -> Mc2_core.atom list list) Mc2_core.Service.Key.t

Service for computing CNF

Sourceval k_fresh : (unit -> Mc2_core.atom) Mc2_core.Service.Key.t

Service for making fresh terms

Sourceval plugin : Mc2_core.Plugin.Factory.t

Plugin providing boolean terms and the cnf service

package mc2

Module Mc2_propositionalSource

Propositional Literal

Module `Mc2_propositional`Source