# Module Symbol

`module Symbol: `sig` .. `end``
Kind's symbols

The term representation is modeled after the SMTLIB 2.0 standard and the symbols are a subset of the symbols defined in the SMTLIB theories Core and Reals_Ints with the addition of uninterpreted symbols.

Most symbols are variadic and associativity is to be understood as defined in the SMTLIB standard:

• ``TRUE` nullary: Boolean true value
• ``FALSE` nullary: Boolean false value
• ``NOT` unary: Boolean negation
• ``IMPLIES` variadic, right-associative: Boolean implication
• ``AND` variadic, left-associative: Boolean conjunction
• ``OR` variadic, left-associative: Boolean disjunction
• ``XOR` variadic, left-associative: Boolean exclusice disjunction
• ``EQ` variadic, chainable: equality between terms
• ``DISTINCT` variadic, pairwise: distict predicate on terms
• ``ITE` ternary: if-then-else
• ``NUMERAL i` nullary: integer numeral
• ``DECIMAL f` nullary: floating-point decimal
• ``BV b` nullary: onstant bitvector
• ``MINUS` variadic, left-associative: difference or a unary negation
• ``PLUS` variadic, left-associative: sum
• ``TIMES` variadic, left-associative: product
• ``DIV` variadic, left-associative: real quotient
• ``INTDIV` variadic, left-associative: integer quotient
• ``MOD` binary: modulus
• ``ABS` unary: absolute value
• ``LEQ` chainable: less than or equal relation
• ``LT` chainable: less than relation
• ``GEQ` chainable: greater than or equal relation
• ``GT` chainable: greater than relation
• ``TO_REAL` unary: conversion to a real number
• ``TO_INT` unary: conversion to an integer number
• ``IS_INT` unary: real is an integer
• ``DIVISIBLE n` unary: divisibilibty by n
• ``CONCAT` binary: concatenation of bitvectors
• ``EXTRACT (i, j)` unary: extract subsequence from bitvector
• ``BVNOT` unary: bit-wise negation
• ``BVNEG` unary: arithmetic negation (unary)
• ``BVAND` binary: bit-wise conjunction
• ``BVOR` binary: bit-wise disjunction
• ``BVADD` binary: arithmetic sum
• ``BVMUL` binary: arithmetic multiplication
• ``BVDIV` binary: arithmetic integer division
• ``BVUREM` binary: arithmetic remainder
• ``BVSHL` unary: logical shift left
• ``BVLSHR` unary: logical shift right
• ``BVULT` binary: arithmetic comparision
• ``SELECT` binary: selection from array
• ``STORE` ternary: update of an array

A chainable symbol is to be read as the conjunction of successive pairs, for example `(<= 1 2 3)` is equivalent to ```(and (<= 1 2)     (<= 2 3))```. A pairwise symbol is to be read as the conjunction of each pair of arguments, for example `(distinct a b c)` is ```(and     (distinct a b) (distinct a c) (distinct b c))```.

In addition to these interpreted symbols we use the following symbols

• ``UF u` variadic: uninterpreted symbol

Symbols are hashconsed so that we can rely on physical equality for comparison, however, as of now there are no useful properties to be stored alongside symbols. In particular the ``NUMERAL i`, ``DECIMAL f` and ``SYM (s, t)` symbols need to be hashconsed for physical equality.
Author(s): Christoph Sticksel

# Types and hash-consing

`type interpreted_symbol = `[ `ABS       | `AND       | `DECIMAL of Decimal.t       | `DISTINCT       | `DIV       | `DIVISIBLE of Numeral.t       | `EQ       | `FALSE       | `GEQ       | `GT       | `IMPLIES       | `INTDIV       | `IS_INT       | `ITE       | `LEQ       | `LT       | `MINUS       | `MOD       | `NOT       | `NUMERAL of Numeral.t       | `OR       | `PLUS       | `SELECT of Type.t       | `STORE       | `TIMES       | `TO_INT       | `TO_REAL       | `TRUE       | `XOR ]` `
The interpreted symbols
`type symbol = `[ `ABS       | `AND       | `DECIMAL of Decimal.t       | `DISTINCT       | `DIV       | `DIVISIBLE of Numeral.t       | `EQ       | `FALSE       | `GEQ       | `GT       | `IMPLIES       | `INTDIV       | `IS_INT       | `ITE       | `LEQ       | `LT       | `MINUS       | `MOD       | `NOT       | `NUMERAL of Numeral.t       | `OR       | `PLUS       | `SELECT of Type.t       | `STORE       | `TIMES       | `TO_INT       | `TO_REAL       | `TRUE       | `UF of UfSymbol.t       | `XOR ]` `
Adding uninterpreted function symbols separately for conversions from expressions in the SMT solver interface
`type t `
Hashconsed symbol

# Hashtables, maps and sets

`val compare_symbols : `t -> t -> int``
Comparison function on symbols
`val equal_symbols : `t -> t -> bool``
Equality function on symbols
`val hash_symbol : `t -> int``
Hashing function on symbols
`module SymbolHashtbl: `Hashtbl.S``  with type key = t``
Hash table over symbols
`module SymbolSet: `Set.S``  with type elt = t``
Set over symbols
`module SymbolMap: `Map.S``  with type key = t``
Map over symbols

# Constructor

`val mk_symbol : `symbol -> t``
Create a symbol
`val import : `t -> t``
Import symbol from a different instance into this hashcons table

# Static symbols

`val s_true : `t``
Constant Boolean value symbol
`val s_false : `t``
Constant Boolean value symbol
`val s_not : `t``
Constant negation symbol
`val s_and : `t``
Constant conjunction symbol
`val s_or : `t``
Constant disjunction symbol
`val s_implies : `t``
Constant implication symbol
`val s_ite : `t``
Constant ite symbol
`val s_eq : `t``
Constant equality symbol
`val s_geq : `t``
Constant greater than or equal symbol
`val s_leq : `t``
Constant less than or equal symbol
`val s_gt : `t``
Constant greater than symbol
`val s_lt : `t``
Constant less than symbol
`val s_mod : `t``
Constant modulus operator symbol
`val s_plus : `t``
Constant plus operator symbol
`val s_minus : `t``
Constant minus operator symbol
`val s_times : `t``
Constant times operator symbol
`val s_div : `t``
Constant division operator symbol
`val s_select : `Type.t -> t``
`val s_store : `t``
array store symbol

# Accessors functions

`val node_of_symbol : `t -> symbol``
Return the node of the hashconsed symbol
`val is_numeral : `t -> bool``
Return true if the symbol is a numeral
`val is_decimal : `t -> bool``
Return true if the symbol is a decimal
`val is_select : `t -> bool``
Return true if the symbol is select from array
`val is_bool : `t -> bool``
Return true if the symbol is ``TRUE` or ``FALSE`
`val numeral_of_symbol : `t -> Numeral.t``
Return the numeral in a ``NUMERAL _` symbol
`val decimal_of_symbol : `t -> Decimal.t``
Return the decimal in a ``DECIMAL _` symbol
`val bool_of_symbol : `t -> bool``
Return `true` for the ``TRUE` symbol and `false` for the ``FALSE` symbol
`val is_uf : `t -> bool``
Return true if the symbol is uninterpreted
`val uf_of_symbol : `t -> UfSymbol.t``
Return the uninterpreted symbol of a symbol

# Pretty-printing

`val pp_print_symbol : `Format.formatter -> t -> unit``
Pretty-print a symbol
`val string_of_symbol : `t -> string``
Return a string representation of a symbol
`val string_of_symbol_node : `symbol -> string``
Return a string representation of a symbol
`val stats : `unit -> int * int * int * int * int * int``