package libzipperposition

  1. Overview
  2. Docs
Library for Zipperposition

Install

Dune Dependency

Authors

Maintainers

Sources

1.6.tar.gz
md5=97cdb2f90468e9e27c7bbe3b4fb160bb
sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d

doc/libzipperposition.calculi/Libzipperposition_calculi/Superposition/Make/Stm/index.html

Module Make.StmSource

Sourcemodule C = Env.C
Sourcetype t = private {
  1. id : int;
    (*

    unique ID of the stream

    *)
  2. penalty : int;
    (*

    heuristic penalty

    *)
  3. mutable stm : C.t option OSeq.t;
    (*

    the stream itself

    *)
}
Sourceexception Empty_Stream
Sourceexception Drip_n_Unfinished of C.t option list * int

Basics

Sourceval make : ?penalty:int -> C.t option OSeq.t -> t
Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval hash : t -> int
Sourceval id : t -> int
Sourceval is_empty : t -> bool
Sourceval penalty : t -> int
Sourceval drip : t -> C.t option

Remove the first element in the stream and return it.

Sourceval drip_n : t -> int -> int -> C.t option list

Attempt to remove the n first elements in the stream and return them. Return less if the guard is reached.

  • raises Drip_n_Unfinished(cl,n)

    where cl is the list of elements already found and n the number of elements if the stream contains less than n elements

IO

OCaml

Innovation. Community. Security.

On This Page
  1. Basics
  2. IO