Module LogtkSymbol

module LogtkSymbol: sig .. end

LogtkSymbols

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


type connective = 
| Not
| And
| Or
| Imply
| Equiv
| Xor
| Eq
| Neq
| HasLogtkType
| True
| False
| Exists
| Forall
| ForallTy
| Lambda
| Arrow
| Wildcard
| Multiset
| FreshVar of int
| TType
type const_symbol = private {
   mutable cs_id : int;
   cs_name : string;
}
type t = 
| Conn of connective
| Cst of const_symbol
| Int of Z.t
| Rat of Q.t
include LogtkInterfaces.HASH
include LogtkInterfaces.ORD
include LogtkInterfaces.PRINT
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 | `Other | `Rat ]

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 LogtkSymbol.ArithOp deals only with numeric constants, i.e., all symbols must verify LogtkSymbol.is_numeric (and most of the time, have the same type). The semantics of operations follows TPTP.
module ArithOp: sig .. end