package libzipperposition

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

Module Make.UnitIndexSource

Sourcetype t
module E : Logtk.Index_intf.EQUATION with type t = Logtk.Term.t * Logtk.Term.t * bool * C.t with type rhs = Logtk.Term.t

Module that describes indexed equations

Sourcetype rhs = E.rhs

Right hand side of equation

Sourceval empty : unit -> t
Sourceval is_empty : t -> bool
Sourceval add : t -> E.t -> t

Index the given (in)equation

Sourceval add_seq : t -> E.t Iter.t -> t
Sourceval add_list : t -> E.t list -> t
Sourceval remove : t -> E.t -> t
Sourceval remove_seq : t -> E.t Iter.t -> t
Sourceval size : t -> int

Number of indexed (in)equations

Sourceval iter : t -> (Logtk.Index_intf.term -> E.t -> unit) -> unit

Iterate on indexed equations

retrieve ~sign (idx,si) (t,st) acc iterates on (in)equations l ?= r of given sign and substitutions subst, such that subst(l, si) = t. It therefore finds generalizations of the query term.

print the index in the DOT format

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