package mc2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Typeclass

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 `Term.TC`Source

Typeclass

Sourcetype t = tc

Source

val make : 
  ?init:
    (Mc2_core__.Solver_types.actions -> Mc2_core__.Solver_types.term -> unit) ->
  ?update_watches:
    (Mc2_core__.Solver_types.actions ->
      Mc2_core__.Solver_types.term ->
      watch:Mc2_core__.Solver_types.term ->
      Mc2_core__.Solver_types.watch_res) ->
  ?delete:(Mc2_core__.Solver_types.term -> unit) ->
  ?subterms:
    (Mc2_core__.Solver_types.term_view ->
      (Mc2_core__.Solver_types.term -> unit) ->
      unit) ->
  ?eval:(Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.eval_res) ->
  pp:Mc2_core__.Solver_types.term_view CCFormat.printer ->
  unit ->
  t

Make a new typeclass, directly

Lazy builder

Sourcetype lazy_tc

Sourceval lazy_from_val : t -> lazy_tc

Sourceval lazy_make : unit -> lazy_tc

Make a new typeclass, without providing the actual functions

Sourceval lazy_get : lazy_tc -> tc

Obtain the underlying typeclass; call only after lazy_complete

Source

val lazy_complete : 
  ?init:
    (Mc2_core__.Solver_types.actions -> Mc2_core__.Solver_types.term -> unit) ->
  ?update_watches:
    (Mc2_core__.Solver_types.actions ->
      Mc2_core__.Solver_types.term ->
      watch:Mc2_core__.Solver_types.term ->
      Mc2_core__.Solver_types.watch_res) ->
  ?delete:(Mc2_core__.Solver_types.term -> unit) ->
  ?subterms:
    (Mc2_core__.Solver_types.term_view ->
      (Mc2_core__.Solver_types.term -> unit) ->
      unit) ->
  ?eval:(Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.eval_res) ->
  pp:Mc2_core__.Solver_types.term_view CCFormat.printer ->
  lazy_tc ->
  unit

Now provide functions for this TC.

raises Failure
if the TC is already defined

package mc2

Module Term.TCSource

Typeclass

Module `Term.TC`Source