package logtk

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