package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 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

type rhs = E.rhs

Right hand side of equation

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

Index the given (in)equation

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

Number of indexed (in)equations

val 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.

val to_dot : t CCFormat.printer

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