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 `Proof.H`Source

Hashtable over clauses. Uses the details of the internal representation to achieve the best performances, however hashtables from this module become invalid when solving is restarted, so they should only be live during inspection of a single proof.

include Hashtbl.S with type key = Mc2_core__.Solver_types.clause

Sourcetype key

Sourcetype !'a t

Sourceval create : int -> 'a t

Sourceval clear : 'a t -> unit

Sourceval reset : 'a t -> unit

since 4.00

Sourceval copy : 'a t -> 'a t

Sourceval add : 'a t -> key -> 'a -> unit

Sourceval remove : 'a t -> key -> unit

Sourceval find : 'a t -> key -> 'a

Sourceval find_opt : 'a t -> key -> 'a option

since 4.05

Sourceval find_all : 'a t -> key -> 'a list

Sourceval replace : 'a t -> key -> 'a -> unit

Sourceval mem : 'a t -> key -> bool

Sourceval iter : (key -> 'a -> unit) -> 'a t -> unit

Sourceval filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit

since 4.03

Sourceval fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc

Sourceval length : 'a t -> int

Sourceval stats : 'a t -> Hashtbl.statistics

since 4.00

Sourceval to_seq : 'a t -> (key * 'a) Seq.t

since 4.07

Sourceval to_seq_keys : _ t -> key Seq.t

since 4.07

Sourceval to_seq_values : 'a t -> 'a Seq.t

since 4.07

Sourceval replace_seq : 'a t -> (key * 'a) Seq.t -> unit

since 4.07

Sourceval get : 'a t -> key -> 'a option

get tbl k finds a binding for the key k if present, or returns None if no value is found. Safe version of Hashtbl.find.

Sourceval get_or : 'a t -> key -> default:'a -> 'a

get_or tbl k ~default returns the value associated to k if present, and returns default otherwise (if k doesn't belong in tbl).

since 0.16

Sourceval add_list : 'a list t -> key -> 'a -> unit

add_list tbl x y adds y to the list x is bound to. If x is not bound, it becomes bound to y.

since 0.16

Sourceval incr : ?by:int -> int t -> key -> unit

incr ?by tbl x increments or initializes the counter associated with x. If get tbl x = None, then after update, get tbl x = Some 1; otherwise, if get tbl x = Some n, now get tbl x = Some (n+1).

parameter by
if specified, the int value is incremented by by rather than 1.

since 0.16

Sourceval decr : ?by:int -> int t -> key -> unit

decr ?by tbl x is like incr but subtract 1 (or the value of by). If the value reaches 0, the key is removed from the table. This does nothing if the key is not already present in the table.

since 0.16

Sourceval keys : 'a t -> key CCHashtbl.iter

keys tbl f iterates on keys (similar order as Hashtbl.iter).

Sourceval values : 'a t -> 'a CCHashtbl.iter

values tbl f iterates on values in the table.

Sourceval keys_list : _ t -> key list

keys_list tbl is the list of keys in tbl. If the key is in the Hashtable multiple times, all occurrences will be returned.

since 0.8

Sourceval values_list : 'a t -> 'a list

values_list t is the list of values in t.

since 0.8

Sourceval map_list : (key -> 'a -> 'b) -> 'a t -> 'b list

Map on a hashtable's items, collect into a list.

Sourceval to_iter : 'a t -> (key * 'a) CCHashtbl.iter

Iterate on bindings in the table.

since 2.8

Sourceval add_iter : 'a t -> (key * 'a) CCHashtbl.iter -> unit

Add the corresponding pairs to the table, using Hashtbl.add.

since 2.8

Source

val add_iter_with : 
  f:(key -> 'a -> 'a -> 'a) ->
  'a t ->
  (key * 'a) CCHashtbl.iter ->
  unit

Add the corresponding pairs to the table, using Hashtbl.add. If a key occurs multiple times in the input, the values are combined using f in an unspecified order.

since 3.3

Sourceval add_seq : 'a t -> (key * 'a) Seq.t -> unit

Add the corresponding pairs to the table, using Hashtbl.add. Renamed from add_std_seq since 3.0.

since 3.0

Source

val add_seq_with : 
  f:(key -> 'a -> 'a -> 'a) ->
  'a t ->
  (key * 'a) Seq.t ->
  unit

Add the corresponding pairs to the table, using Hashtbl.add. If a key occurs multiple times in the input, the values are combined using f in an unspecified order.

since 3.3

Sourceval of_iter : (key * 'a) CCHashtbl.iter -> 'a t

From the given bindings, added in order.

since 2.8

Source

val of_iter_with : 
  f:(key -> 'a -> 'a -> 'a) ->
  (key * 'a) CCHashtbl.iter ->
  'a t

From the given bindings, added in order. If a key occurs multiple times in the input, the values are combined using f in an unspecified order.

since 3.3

Sourceval of_seq : (key * 'a) Seq.t -> 'a t

From the given bindings, added in order. Renamed from of_std_seq since 3.0.

since 3.0

Sourceval of_seq_with : f:(key -> 'a -> 'a -> 'a) -> (key * 'a) Seq.t -> 'a t

From the given bindings, added in order. If a key occurs multiple times in the input, the values are combined using f in an unspecified order.

since 3.3

Sourceval add_iter_count : int t -> key CCHashtbl.iter -> unit

add_iter_count tbl i increments the count of each element of i by calling incr. This is useful for counting how many times each element of i occurs.

since 2.8

Sourceval add_seq_count : int t -> key Seq.t -> unit

add_seq_count tbl seq increments the count of each element of seq by calling incr. This is useful for counting how many times each element of seq occurs. Renamed from of_std_seq_count since 3.0.

since 3.0

Sourceval of_iter_count : key CCHashtbl.iter -> int t

Like add_seq_count, but allocates a new table and returns it.

since 2.8

Sourceval of_seq_count : key Seq.t -> int t

Like add_seq_count, but allocates a new table and returns it. Renamed from of_std_seq_count since 3.0.

since 3.0

Sourceval to_list : 'a t -> (key * 'a) list

to_list tbl returns the list of (key,value) bindings (order unspecified).

Sourceval of_list : (key * 'a) list -> 'a t

of_list l builds a table from the given list l of bindings k_i -> v_i, added in order using add. If a key occurs several times, it will be added several times, and the visible binding will be the last one.

Sourceval of_list_with : f:(key -> 'a -> 'a -> 'a) -> (key * 'a) list -> 'a t

of_list l builds a table from the given list l of bindings k_i -> v_i. If a key occurs multiple times in the input, the values are combined using f in an unspecified order.

since 3.3

Sourceval update : 'a t -> f:(key -> 'a option -> 'a option) -> k:key -> unit

update tbl ~f ~k updates key k by calling f k (Some v) if k was mapped to v, or f k None otherwise; if the call returns None then k is removed/stays removed, if the call returns Some v' then the binding k -> v' is inserted using Hashtbl.replace.

since 0.14

Sourceval get_or_add : 'a t -> f:(key -> 'a) -> k:key -> 'a

get_or_add tbl ~k ~f finds and returns the binding of k in tbl, if it exists. If it does not exist, then f k is called to obtain a new binding v; k -> v is added to tbl and v is returned.

since 1.0

Source

val pp : 
  ?pp_start:unit CCHashtbl.printer ->
  ?pp_stop:unit CCHashtbl.printer ->
  ?pp_sep:unit CCHashtbl.printer ->
  ?pp_arrow:unit CCHashtbl.printer ->
  key CCHashtbl.printer ->
  'a CCHashtbl.printer ->
  'a t CCHashtbl.printer

pp ~pp_start ~pp_stop ~pp_sep ~pp arrow pp_k pp_v returns a table printer given a pp_k printer for individual key and a pp_v printer for individual value. pp_start and pp_stop control the opening and closing delimiters, by default print nothing. pp_sep control the separator between binding. pp_arrow control the arrow between the key and value. Renamed from print since 2.0.

since 0.13

package mc2

Module Proof.HSource

Module `Proof.H`Source