Module Literals

module Literals: sig .. end

Array of literals

type term = Libzipperposition.FOTerm.t

type t = Literal.t array

Array of literals

val equal : t -> t -> bool

val equal_com : t -> t -> bool

val compare : t -> t -> int

include Interfaces.HASH

val variant : ?subst:Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t ->
       t Libzipperposition.Scoped.t ->
       Libzipperposition.Substs.t Sequence.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 Literals.variant with distinc scopes

val weight : t -> int

val depth : t -> int

val vars : t -> Libzipperposition.Type.t Libzipperposition.HVar.t list

val is_ground : t -> bool

all the literals are ground?

val to_form : t -> term Libzipperposition.SLiteral.t list

Make a 'or' formula from literals

val apply_subst : renaming:Libzipperposition.Substs.Renaming.t ->
       Libzipperposition.Substs.t ->
       t Libzipperposition.Scoped.t -> t

val map : (term -> term) -> t -> t

val pos : t -> CCBV.t

val neg : t -> CCBV.t

val maxlits : ord:Libzipperposition.Ordering.t -> t -> CCBV.t

Bitvector of positions of maximal literals

val maxlits_l : ord:Libzipperposition.Ordering.t -> t -> (Literal.t * int) list

List of maximal literals, with their index, among the array

val is_max : ord:Libzipperposition.Ordering.t -> t -> int -> bool

Is the i-th literal maximal in the ordering?

val is_trivial : t -> bool

Tautology? (simple syntactic criterion only)

val is_absurd : t -> bool

All literals are false, or there are no literals

module Seq: sig .. end

High order combinators

module Pos: sig .. end

module Conv: sig .. end

module View: sig .. end

val fold_lits : eligible:(int -> Literal.t -> bool) ->
       t -> (Literal.t * int) Sequence.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:Libzipperposition.Ordering.t ->
       eligible:(int -> Literal.t -> bool) ->
       t ->
       (term * term * bool * Libzipperposition.Position.t)
       Sequence.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_arith : eligible:(int -> Literal.t -> bool) ->
       t -> (ArithLit.t * Libzipperposition.Position.t) Sequence.t

Fold over eligible arithmetic literals

val fold_arith_terms : eligible:(int -> Literal.t -> bool) ->
       which:[< `All | `Max ] ->
       ord:Libzipperposition.Ordering.t ->
       t ->
       (term * ArithLit.Focus.t * Libzipperposition.Position.t) Sequence.t

Fold on terms under arithmetic literals, with the focus on the current term

val fold_terms : ?vars:bool ->
       ?ty_args:bool ->
       which:[< `All | `Max ] ->
       ord:Libzipperposition.Ordering.t ->
       subterms:bool ->
       eligible:(int -> Literal.t -> bool) ->
       t -> (term * Libzipperposition.Position.t) Sequence.t

See Literal.fold_terms, which is the same but for the eligible argument

val symbols : ?init:Libzipperposition.ID.Set.t -> t -> Libzipperposition.ID.Set.t

IO

val pp : t CCFormat.printer

val pp_tstp : t CCFormat.printer

val to_string : t -> string

Special kinds of literal arrays

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_pos_eq : t -> (term * term) option

Recognize whether the clause is a positive unit equality.