Module `Logtk.Literals`

Array of literals

include Interfaces.HASH with type t := t

include Interfaces.EQ

val variant : ?⁠subst:Subst.t -> t Scoped.t -> t Scoped.t -> (Subst.t * Builtin.Tag.t list) Iter.t: Variant checking (alpha-equivalence). It can reorder literals to do its check, so that might be computationnally expensive (a bit like subsumption).

val are_variant : t -> t -> bool: Simple interface on top of variant with distinc scopes

val matching : ?⁠subst:Subst.t -> pattern:t Scoped.t -> t Scoped.t -> (Subst.t * Builtin.Tag.t list) Iter.t
val matches : t -> t -> bool
val weight : t -> int
val ho_weight : t -> int
val depth : t -> int
val vars : t -> Type.t HVar.t list
val is_ground : t -> bool: all the literals are ground?

val to_form : t -> term SLiteral.t list: Make a 'or' formula from literals

val apply_subst : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t
val of_unif_subst : Subst.Renaming.t -> Unif_subst.t -> t
val map : (term -> term) -> t -> t
val pos : t -> CCBV.t
val neg : t -> CCBV.t
val maxlits : ord:Ordering.t -> t -> CCBV.t: Bitvector of positions of maximal literals

val maxlits_l : ord:Ordering.t -> t -> (Literal.t * int) list: List of maximal literals, with their index, among the array

val is_max : ord:Ordering.t -> t -> int -> bool: Is the i-th literal maximal in the ordering?

val is_absurd : t -> bool: All literals are false, or there are no literals

module Seq : sig ... end

module Pos : sig ... end

module Conv : sig ... end

module View : sig ... end

val fold_lits : eligible:(int -> Literal.t -> bool) -> t -> (Literal.t * int) Iter.t: Fold over literals who satisfy eligible. The folded function is given the literal and its index.

val fold_eqn : ?⁠both:bool -> ?⁠sign:bool -> ord:Ordering.t -> eligible:(int -> Literal.t -> bool) -> t -> (term * term * bool * Position.t) Iter.t: fold f over all literals sides, with their positions. f is given (left side, right side, sign, position of left side) if ord is present, then only the max side of an oriented equation will be visited, otherwise they will both be explored. if both = true, then both sides of a non-oriented equation will be visited, otherwise only one side. if sign = true, then only positive equations are visited; if it's false, only negative ones; if it's not defined, both.

val fold_eqn_simple : ?⁠sign:bool -> t -> (term * term * bool * Position.t) Iter.t: Like previous version but simpler: it visits all equations only in the orientation l = r

val fold_terms : ?⁠vars:bool -> ?⁠var_args:bool -> ?⁠fun_bodies:bool -> ?⁠ty_args:bool -> which:[< `Max | `All ] -> ord:Ordering.t -> subterms:bool -> eligible:(int -> Literal.t -> bool) -> t -> term Position.With.t Iter.t: See Literal.fold_terms, which is the same but for the eligible argument

val symbols : ?⁠init:Logtk.ID.Set.t -> ?⁠include_types:bool -> t -> Logtk.ID.Set.t

val is_RR_horn_clause : t -> bool: Recognized whether the clause is a Range-Restricted Horn clause

val is_horn : t -> bool: Recognizes Horn clauses (at most one positive literal)

val is_unique_max_horn_clause : ord:Ordering.t -> t -> bool: Recognized whether the clause is a Range-Restricted Horn clause

val is_pos_eq : t -> (term * term) option: Recognize whether the clause is a positive unit equality.

val is_shielded : Term.var -> t -> bool: Is this variable shielded in this clause?

val unshielded_vars : ?⁠filter:(Term.var -> bool) -> t -> Term.var list: Set of variables occurring unshielded