package mc2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Typeclass

package mc2

mc2.backend
- Mc2_backend
  - Backend_intf
    
    S
  - Dot
    
    Arg
    
    Default
    
    Make
    
    A
mc2.core
- Mc2_core
  - Actions
  - Atom
    
    Set
    
    Tbl
  - Bound_var
  - Builtins
  - Clause
    
    Set
    
    Tbl
  - Error
  - ID
    
    Map
    
    Set
    
    Smtlib
    
    Tbl
  - Int_map
  - Lemma
    
    TC
  - Plugin
    
    Factory
    
    S
  - Proof
    
    H
  - Service
    
    Key
    
    Registry
  - Solver
    
    Sat_state
    
    Unsat_state
  - Statement
  - Term
    
    Bool
    
    Map
    
    Set
    
    TC
    
    TERM_ALLOC
    
    TERM_ALLOC_OPS
    
    Tbl
    
    Term_allocator
    
    T
    
    Watch1
    
    Watch2
  - Tseitin
    
    Arg
    
    Make
    
    F
    
    S
  - Type
    
    Alloc
    
    T
    
    TC
    
    TY_ALLOC_OPS
  - Value
    
    TC
    
    Tbl
mc2.dimacs
- Mc2_dimacs
  - Plugin_sat
mc2.lra
- Mc2_lra
  - LE
    
    Infix
mc2.propositional
- Mc2_propositional
  - F
mc2.smtlib
- Mc2_smtlib
  - Make
    
    ARG
  - Typecheck
    
    Make
    
    ARG
mc2.uf
- Mc2_uf
mc2.unin_sort
- Mc2_unin_sort

Legend:
Library
Module
Module type
Parameter
Class
Class type

Typeclass

type t = tc

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

type lazy_tc

val lazy_from_val : t -> lazy_tc

val lazy_make : unit -> lazy_tc

Make a new typeclass, without providing the actual functions

val lazy_get : lazy_tc -> tc

Obtain the underlying typeclass; call only after lazy_complete

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