# Module `Symbol`

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
• ``UBV b` nullary: constant unsigned bitvector
• ``BV b` nullary: consant 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
• ``BVNOT` unary: bit-wise negation
• ``BVNEG` unary: arithmetic negation (unary)
• ``BVAND` binary: bit-wise conjunction
• ``BVOR` binary: bit-wise disjunction
• ``BVADD` binary: signed bitvector sum
• ``BVSUB` binary: signed bitvector difference
• ``BVMUL` binary: arithmetic multiplication
• ``BVUDIV` binary: arithmetic integer division
• ``BVSDIV` binary: arithmetic integer signed division
• ``BVUREM` binary: arithmetic remainder
• ``BVSREM` binary: arithmetic signed remainder
• ``BVSHL` binary: logical shift left
• ``BVLSHR` binary: logical shift right
• ``BVASHR` binary: arithmetic shift right
• ``BVULT` binary: arithmetic comparision less than
• ``BVULE` binary: arithmetic comparision less than or equal to
• ``BVUGT` binary: arithmetic comparision greater than
• ``BVUGE` binary: arithmetic comparision greater than or equal to
• ``BVSLT` signed binary: arithmetic comparision less than
• ``BVSLE` signed binary: arithmetic comparision less than or equal to
• ``BVSGT` signed binary: arithmetic comparision greater than
• ``BVSGE` signed binary: arithmetic comparision greater than or equal to
• ``BVEXTRACT (i, j)` unary: extract subsequence from bitvector
• ``BVCONCAT` binary: concatenation of bitvectors
• ``BVSIGNEXT i` unary: sign extension of bitvectors
• ``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
Christoph Sticksel, Arjun Viswanathan

## Types and hash-consing

`type interpreted_symbol` = `[ `
 `| ```TRUE` Boolean true value (nullary) `| ```FALSE` Boolean false value (nullary) `| ```NOT` Boolean negation (unary) `| ```IMPLIES` Boolean implication (right-associative) `| ```AND` Boolean conjunction (left-associative) `| ```OR` Boolean disjunction (left-associative) `| ```XOR` Boolean exclusive disjunction (left-associative) `| ```EQ` Equality between terms (chainable) `| ```DISTINCT` Pairwise distinct predicate (chainable) `| ```ITE` If-then-else (ternary) `| ```NUMERAL of Numeral.t` Infinite precision integer numeral (nullary) `| ```DECIMAL of Decimal.t` infinite precision floating-point decimal (nullary) `| ```UBV of Bitvector.t` Constant unsigned bitvector `| ```BV of Bitvector.t` Constant bitvector `| ```MINUS` Difference or unary negation (left-associative) `| ```PLUS` Sum (left-associative) `| ```TIMES` Product (left-associative) `| ```DIV` Real quotient (left-associative) `| ```INTDIV` Integer quotient (left-associative) `| ```MOD` Modulus (binary) `| ```ABS` Absolute value (unary) `| ```LEQ` Less than or equal relation (chainable) `| ```LT` Less than relation (chainable) `| ```GEQ` Greater than or equal relation (chainable) `| ```GT` Greater than relation (chainable) `| ```TO_REAL` Conversion to a floating-point decimal (unary) `| ```TO_INT` Conversion to an unsigned integer numeral (unary) `| ```TO_UINT8` Conversion to an unsigned integer8 numeral (unary) `| ```TO_UINT16` Conversion to an unsigned integer16 numeral (unary) `| ```TO_UINT32` Conversion to an unsigned integer32 numeral (unary) `| ```TO_UINT64` Conversion to an unsigned integer64 numeral (unary) `| ```TO_INT8` Conversion to an integer8 numeral (unary) `| ```TO_INT16` Conversion to an integer16 numeral (unary) `| ```TO_INT32` Conversion to an integer32 numeral (unary) `| ```TO_INT64` Conversion to an integer64 numeral (unary) `| ```BV2NAT` Conversion from bitvector to a natural number `| ```IS_INT` Real is an integer (unary) `| ```DIVISIBLE of Numeral.t` Divisible by `n` (unary) `| ```BVNOT` Bit-wise negation (unary) `| ```BVNEG` Arithmetic negation (unary) `| ```BVAND` Bit-wise conjunction (binary) `| ```BVOR` Bit-wise disjunction (binary) `| ```BVADD` Signed bitvector sum (binary) `| ```BVSUB` Signed bitvector difference (binary) `| ```BVMUL` Arithmetic multiplication (binary) `| ```BVUDIV` Arithmetic integer division (binary) `| ```BVSDIV` Arithmetic integer signed division (binary) `| ```BVUREM` Arithmetic remainder (binary) `| ```BVSREM` Arithmetic signed remainder (binary) `| ```BVSHL` Logical shift left (binary) `| ```BVLSHR` Logical shift right (binary) `| ```BVASHR` Arithmetic shift right (binary) `| ```BVULT` `| ```BVULE` `| ```BVUGT` `| ```BVUGE` `| ```BVSLT` `| ```BVSLE` `| ```BVSGT` `| ```BVSGE` `| ```BVEXTRACT of Numeral.t * Numeral.t` Extract subsequence from bitvector (unary) `| ```BVCONCAT` Concatenation of bitvectors (binary) `| ```BVSIGNEXT of Numeral.t` Sign extension of bitvector (unary) `| ```SELECT of Type.t` `| ```STORE` Update of an array (ternary)
` ]`

The interpreted symbols

`type symbol` = `[ `
 `| ``interpreted_symbol` `| ```UF of UfSymbol.t` Uninterpreted symbol (fixed arity)
` ]`

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 : Stdlib.Hashtbl.S with type SymbolHashtbl.key = t`

Hash table over symbols

`module SymbolSet : Stdlib.Set.S with type SymbolSet.elt = t`

Set over symbols

`module SymbolMap : Stdlib.Map.S with type SymbolMap.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_to_int : t`
`val s_to_real : t`
`val s_select : Type.t -> t`

Array read operator

`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_bitvector : t -> bool`

Return true if the symbol is a bitvector

`val is_ubitvector : t -> bool`

Return true if the symbol is an unsigned bitvector

`val is_ubv8 : t -> bool`

Return true if the symbol is an unsigned bitvector of size 8

`val is_ubv16 : t -> bool`

Return true if the symbol is an unsigned bitvector of size 16

`val is_ubv32 : t -> bool`

Return true if the symbol is an unsigned bitvector of size 32

`val is_ubv64 : t -> bool`

Return true if the symbol is an unsigned bitvector of size 64

`val is_bv8 : t -> bool`

Return true if the symbol is a bitvector of size 8

`val is_bv16 : t -> bool`

Return true if the symbol is a bitvector of size 16

`val is_bv32 : t -> bool`

Return true if the symbol is a bitvector of size 32

`val is_bv64 : t -> bool`

Return true if the symbol is a bitvector of size 64

`val is_to_uint8 : t -> bool`

Return true if the symbol is a touint8

`val is_to_uint16 : t -> bool`

Return true if the symbol is a touint16

`val is_to_uint32 : t -> bool`

Return true if the symbol is a touint32

`val is_to_uint64 : t -> bool`

Return true if the symbol is a touint64

`val is_to_int8 : t -> bool`

Return true if the symbol is a toint8

`val is_to_int16 : t -> bool`

Return true if the symbol is a toint16

`val is_to_int32 : t -> bool`

Return true if the symbol is a toint32

`val is_to_int64 : t -> bool`

Return true if the symbol is a toint64

`val is_select : t -> bool`

Return true if the symbol is select from array

`val is_divisible : t -> bool`

Return true if the symbol is the divisible function

`val is_bool : t -> bool`

Return true if the symbol is ``TRUE` or ``FALSE`

`val is_ite : t -> bool`

Return true if the symbol is ``ITE`

`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 bitvector_of_symbol : t -> Bitvector.t`

Return the bitvector in a ``BV _` symbol

`val ubitvector_of_symbol : t -> Bitvector.t`

Return the ubitvector in a ``UBV _` 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 : Stdlib.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`