package logtk

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

Module Logtk.LiteralsSource

Array of literals

An array of literals is one of the major components of a clause.

It defines (implicitly) a scope for its variables; applying a substitution should always be done with the same Subst.Renaming.t for all literals in the array.

This also provides printers, comparison, matching, positions, simplifications, etc. for such arrays of literals.

Sourcetype term = Term.t
Sourcetype t = Literal.t array

Array of literals

Sourceval equal_com : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval compare_multiset : ord:Ordering.t -> t -> t -> Comparison.t
include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourceval 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).

Sourceval are_variant : t -> t -> bool

Simple interface on top of variant with distinc scopes

Sourceval matching : ?subst:Subst.t -> pattern:t Scoped.t -> t Scoped.t -> (Subst.t * Builtin.Tag.t list) Iter.t
Sourceval matches : t -> t -> bool
Sourceval weight : t -> int
Sourceval ho_weight : t -> int
Sourceval depth : t -> int
Sourceval vars : t -> Type.t HVar.t list
Sourceval is_ground : t -> bool

all the literals are ground?

Sourceval to_form : t -> term SLiteral.t list

Make a 'or' formula from literals

Sourceval of_unif_subst : Subst.Renaming.t -> Unif_subst.t -> t
Sourceval map : (term -> term) -> t -> t
Sourceval pos : t -> CCBV.t
Sourceval neg : t -> CCBV.t
Sourceval maxlits : ord:Ordering.t -> t -> CCBV.t

Bitvector of positions of maximal literals

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

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

Sourceval is_max : ord:Ordering.t -> t -> int -> bool

Is the i-th literal maximal in the ordering?

Sourceval is_trivial : t -> bool

Tautology? (simple syntactic criterion only)

Sourceval is_absurd : t -> bool

All literals are false, or there are no literals

Sourceval apply_subst : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t
Sourcemodule Seq : sig ... end

High order combinators

Sourcemodule Pos : sig ... end
Sourcemodule Conv : sig ... end
Sourcemodule View : sig ... end
Sourceval 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.

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

Sourceval fold_arith : eligible:(int -> Literal.t -> bool) -> t -> Int_lit.t Position.With.t Iter.t

Fold over eligible arithmetic literals

Sourceval fold_arith_terms : eligible:(int -> Literal.t -> bool) -> which:[< `Max | `All ] -> ord:Ordering.t -> t -> (term * Int_lit.Focus.t * Position.t) Iter.t

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

Sourceval fold_rat : eligible:(int -> Literal.t -> bool) -> t -> Rat_lit.t Position.With.t Iter.t

Fold over eligible arithmetic literals

Sourceval fold_rat_terms : eligible:(int -> Literal.t -> bool) -> which:[< `Max | `All ] -> ord:Ordering.t -> t -> (term * Rat_lit.Focus.t * Position.t) Iter.t

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

Sourceval 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

Sourceval symbols : ?init:ID.Set.t -> ?include_types:bool -> t -> ID.Set.t

IO

Sourceval pp_tstp_closed : t CCFormat.printer
Sourceval pp_zf_closed : t CCFormat.printer
Sourceval to_string : t -> string

Special kinds of literal arrays

Sourceval is_RR_horn_clause : t -> bool

Recognized whether the clause is a Range-Restricted Horn clause

Sourceval is_horn : t -> bool

Recognizes Horn clauses (at most one positive literal)

Sourceval is_pos_eq : t -> (term * term) option

Recognize whether the clause is a positive unit equality.

Shielded Variables

Sourceval is_shielded : Term.var -> t -> bool

Is this variable shielded in this clause?

Sourceval unshielded_vars : ?filter:(Term.var -> bool) -> t -> Term.var list

Set of variables occurring unshielded

Sourceval vars_distinct : t -> bool
Sourceval ground_lits : t -> t
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