package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
include S with type term = LogtkFOTerm.t and type term_set = LogtkFOTerm.Set.t
type term = LogtkFOTerm.t
type term_set = LogtkFOTerm.Set.t
type t = private LogtkScopedTerm.t
type form = t
type view = private
  1. | True
  2. | False
  3. | Atom of term
  4. | And of t list
  5. | Or of t list
  6. | Not of t
  7. | Imply of t * t
  8. | Equiv of t * t
  9. | Xor of t * t
  10. | Eq of term * term
  11. | Neq of term * term
  12. | Forall of type_ * t
    (*

    Quantified formula, with De Bruijn index

    *)
  13. | Exists of type_ * t
  14. | ForallTy of t
    (*

    quantification on type variable

    *)
val view : t -> view

View of the formula

val of_term : LogtkScopedTerm.t -> t option
val of_term_exn : LogtkScopedTerm.t -> t
  • raises Invalid_argument

    if the term isn't a formula

val is_form : LogtkScopedTerm.t -> bool
  • raises Invalid_argument

    if the term isn't a formula

include LogtkInterfaces.HASH with type t := t
include LogtkInterfaces.EQ with type t := t
val eq : t -> t -> bool
val hash_fun : t CCHash.hash_fun
val hash : t -> int
include LogtkInterfaces.ORD with type t := t
val cmp : t -> t -> int

Containers

module Tbl : Hashtbl.S with type key = t
module Set : Sequence.Set.S with type elt = t
module Map : Sequence.Map.S with type key = t

Caution: constructors can raise LogtkType.Error if the types are not as expected. In particular, Base.eq and Base.neq expect two terms of the exact same type.

module Base : sig ... end

Sequence

module Seq : sig ... end

Combinators

val map_leaf : (t -> t) -> t -> t

Call the function on leaves (atom,equal,true,false) and replace the leaves by their image. The image formulas should not contain free De Bruijn indexes (ie, should verify db_closed).

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

Map on terms

val fold : ('a -> term -> 'a) -> 'a -> t -> 'a

Map on terms

Fold on terms

val iter : (term -> unit) -> t -> unit

Fold on terms

val map_shallow : (t -> t) -> t -> t

Apply the function to the immediate subformulas

val map_depth : ?depth:int -> (int -> term -> term) -> t -> t

Map each term to another term. The number of binders from the root of the formula to the term is given to the function.

val map_leaf_depth : ?depth:int -> (int -> t -> t) -> t -> t
val fold_depth : ?depth:int -> ('a -> int -> term -> 'a) -> 'a -> t -> 'a

Fold on terms, but with an additional argument, the number of De Bruijn indexes bound on through the path to the term

val weight : t -> int

Number of 'nodes' of the formula, including the terms

val subterm : term -> t -> bool

subterm t f true iff t occurs in some term of f

val is_atomic : t -> bool

No connectives?

val is_ground : t -> bool

No connectives?

No variables?

val is_closed : t -> bool

No variables?

All variables bound?

val contains_symbol : LogtkSymbol.t -> t -> bool
val symbols : ?init:LogtkSymbol.Set.t -> t -> LogtkSymbol.Set.t

Set of symbols occurring in the formula

High level operations

val free_vars_set : t -> term_set

Set of free variables

val free_vars : t -> term list

Set of free variables

Set of free vars

val de_bruijn_set : t -> LogtkType.Set.t * term_set

Set of free vars

Set of De Bruijn indices that are not bound for types and terms

val close_forall : t -> t

Bind all free variables with forall

val close_exists : t -> t

Bind all free variables with forall

Bind all free variables with exists

val open_forall : ?offset:int -> t -> t

Remove outer forall binders, using fresh vars instead of DB symbols

val open_and : t -> t list

If the formula is an outer conjunction, return the list of elements of the conjunction

val open_or : t -> t list

Simplifications

val flatten : t -> t

Flatten AC connectives (or/and)

val simplify : t -> t

Flatten AC connectives (or/and)

Simplify the formula

val is_trivial : t -> bool

Trivially true formula?

val ac_normal_form : t -> t

Normal form modulo AC of "or" and "and"

val ac_eq : t -> t -> bool

Normal form modulo AC of "or" and "and"

Equal modulo AC?

Conversions

val to_prolog : ?depth:int -> t -> LogtkPrologTerm.t

IO

include LogtkInterfaces.PRINT with type t := t
val pp : Buffer.t -> t -> unit
val to_string : t -> string
val fmt : Format.formatter -> t -> unit
include LogtkInterfaces.PRINT_DE_BRUIJN with type t := t and type term := term
type print_hook = int -> (Buffer.t -> term -> unit) -> Buffer.t -> term -> bool

User-provided hook that can be used to print terms (for composite cases) before the default printing occurs. The int argument is the De Bruijn depth in the term. A hook takes as arguments the depth and the recursive printing function that it can use to print subterms. A hook should return true if it fired, false to fall back on the default printing.

val pp_depth : ?hooks:print_hook list -> int -> Buffer.t -> t -> unit
module TPTP : sig ... end

Conversion to higher-order term

val to_hoterm : t -> LogtkHOTerm.t
val of_hoterm : LogtkHOTerm.t -> t option
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