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

`\|` `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)

`\|` `interpreted_symbol`
`\|` `UF of UfSymbol.t	Uninterpreted symbol (fixed arity)