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