package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Make.SubsumptionIndexSource

Sourcetype t
Sourcemodule C : Logtk.Index_intf.CLAUSE with type t = C.t
Sourceval name : string
Sourceval empty : unit -> t

Empty index

Sourceval add : t -> C.t -> t

Index the clause

Sourceval add_seq : t -> C.t Iter.t -> t
Sourceval add_list : t -> C.t list -> t
Sourceval remove : t -> C.t -> t

Un-index the clause

Sourceval remove_seq : t -> C.t Iter.t -> t

Fold on a set of indexed candidate clauses, that may subsume the given clause.

Sourceval retrieve_subsuming_c : t -> C.t -> C.t Iter.t

Fold on a set of indexed candidate clauses, that may be subsumed by the given clause

Sourceval retrieve_subsumed_c : t -> C.t -> C.t Iter.t
Sourceval retrieve_alpha_equiv : t -> Logtk.Index_intf.lits -> Logtk.Index_intf.labels -> C.t Iter.t

Retrieve clauses that are potentially alpha-equivalent to the given clause

Sourceval retrieve_alpha_equiv_c : t -> C.t -> C.t Iter.t

Retrieve clauses that are potentially alpha-equivalent to the given clause

Sourceval iter : t -> C.t Iter.t
Sourceval fold : ('a -> C.t -> 'a) -> 'a -> t -> 'a
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct