package logtk

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

LogtkSymbols

LogtkSymbols are abstract, but must be constructible from strings, printable, comparable and hashable.

type connective =
  1. | Not
  2. | And
  3. | Or
  4. | Imply
  5. | Equiv
  6. | Xor
  7. | Eq
  8. | Neq
  9. | HasType
  10. | LiftType
    (*
    • since 0.8
    *)
  11. | True
  12. | False
  13. | Exists
  14. | Forall
  15. | ForallTy
  16. | Lambda
  17. | Arrow
  18. | Wildcard
  19. | Multiset
  20. | FreshVar of int
  21. | TType
type const_symbol = private {
  1. mutable cs_id : int;
  2. cs_name : string;
}
type t =
  1. | Conn of connective
  2. | Cst of const_symbol
  3. | Int of Z.t
  4. | Rat of Q.t
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
include LogtkInterfaces.PRINT with type t := t
val pp : Buffer.t -> t -> unit
val to_string : t -> string
val fmt : Format.formatter -> t -> unit
val is_prefix : t -> bool

is_infix s returns true if the way the symbol is printed should be used in a prefix way if applied to 1 argument

val is_infix : t -> bool

is_infix s returns true if the way the symbol is printed should be used in an infix way if applied to two arguments

module Map : Sequence.Map.S with type key = t
module Set : Sequence.Set.S with type elt = t
module Tbl : Hashtbl.S with type key = t
val ty : t -> [ `Int | `Rat | `Other ]

Base Constructors

val of_string : string -> t
val mk_int : Z.t -> t
val of_int : int -> t
val int_of_string : string -> t
val mk_rat : Q.t -> t
val of_rat : int -> int -> t
val rat_of_string : string -> t
val is_const : t -> bool
val is_int : t -> bool
val is_rat : t -> bool
val is_numeric : t -> bool
val is_distinct : t -> bool
module Seq : sig ... end
module Base : sig ... end

Generation of symbols

val gensym : ?prefix:string -> unit -> t

Fresh symbol (with unique name)

TPTP Interface

Creates symbol and give them properties.

module TPTP : sig ... end

The module ArithOp deals only with numeric constants, i.e., all symbols must verify is_numeric (and most of the time, have the same type). The semantics of operations follows TPTP.

module ArithOp : sig ... end