package libzipperposition

You can search for identifiers within the package.

in-package search v0.2.0

Library for Zipperposition

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

Maintainers

S

simon.cruanes.2.17@m4x.org

Sources

2.1.tar.gz

md5=e72de75e9f0f87da9e6e8c0a4d4c89f9

sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287

doc/libzipperposition.induction/Libzipperposition_induction/Make/argument-1-E/Stm/index.html

Module `E.Stm`

module Ctx : Libzipperposition.Ctx.S

module C = C

type t = private {

id : int;
(*
unique ID of the stream
*)
parents : C.t list;
(*
parent clauses for inference generating this stream
*)
mutable penalty : int;
(*
heuristic penalty
*)
mutable hits : int;
(*
how many attemts to retrieve unifier were there
*)
mutable stm : C.t option OSeq.t;
(*
the stream itself
*)

}

exception Empty_Stream

exception Drip_n_Unfinished of C.t option list * int * int

Basics

val make : ?penalty:int -> parents:C.t list -> C.t option OSeq.t -> t

val equal : t -> t -> bool

val compare : t -> t -> int

val hash : t -> int

val id : t -> int

val is_empty : t -> bool

val penalty : t -> int

val drip : t -> C.t option

Remove the first element in the stream and return it.

raises Empty_Stream
if the stream is empty

val 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

val pp : t CCFormat.printer

On This Page

Basics
IO