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:

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

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.

Types and hash-consing

type interpreted_symbol = [
  1. | `TRUE
    (*

    Boolean true value (nullary)

    *)
  2. | `FALSE
    (*

    Boolean false value (nullary)

    *)
  3. | `NOT
    (*

    Boolean negation (unary)

    *)
  4. | `IMPLIES
    (*

    Boolean implication (right-associative)

    *)
  5. | `AND
    (*

    Boolean conjunction (left-associative)

    *)
  6. | `OR
    (*

    Boolean disjunction (left-associative)

    *)
  7. | `XOR
    (*

    Boolean exclusive disjunction (left-associative)

    *)
  8. | `EQ
    (*

    Equality between terms (chainable)

    *)
  9. | `DISTINCT
    (*

    Pairwise distinct predicate (chainable)

    *)
  10. | `ITE
    (*

    If-then-else (ternary)

    *)
  11. | `NUMERAL of Numeral.t
    (*

    Infinite precision integer numeral (nullary)

    *)
  12. | `DECIMAL of Decimal.t
    (*

    infinite precision floating-point decimal (nullary)

    *)
  13. | `UBV of Bitvector.t
    (*

    Constant unsigned bitvector

    *)
  14. | `BV of Bitvector.t
    (*

    Constant bitvector

    *)
  15. | `MINUS
    (*

    Difference or unary negation (left-associative)

    *)
  16. | `PLUS
    (*

    Sum (left-associative)

    *)
  17. | `TIMES
    (*

    Product (left-associative)

    *)
  18. | `DIV
    (*

    Real quotient (left-associative)

    *)
  19. | `INTDIV
    (*

    Integer quotient (left-associative)

    *)
  20. | `MOD
    (*

    Modulus (binary)

    *)
  21. | `ABS
    (*

    Absolute value (unary)

    *)
  22. | `LEQ
    (*

    Less than or equal relation (chainable)

    *)
  23. | `LT
    (*

    Less than relation (chainable)

    *)
  24. | `GEQ
    (*

    Greater than or equal relation (chainable)

    *)
  25. | `GT
    (*

    Greater than relation (chainable)

    *)
  26. | `TO_REAL
    (*

    Conversion to a floating-point decimal (unary)

    *)
  27. | `TO_INT
    (*

    Conversion to an unsigned integer numeral (unary)

    *)
  28. | `TO_UBV of int
    (*

    Conversion to an unsigned bv numeral (unary)

    *)
  29. | `TO_BV of int
    (*

    Conversion to a signed bv numeral (unary)

    *)
  30. | `BV2NAT
    (*

    Conversion from bitvector to a natural number (now deprecated in SMT-LIB)

    *)
  31. | `UBV_TO_INT
    (*

    Conversion from bitvector to a natural number

    *)
  32. | `SBV_TO_INT
    (*

    Conversion from signed bitvector to integer number

    *)
  33. | `IS_INT
    (*

    Real is an integer (unary)

    *)
  34. | `DIVISIBLE of Numeral.t
    (*

    Divisible by n (unary)

    *)
  35. | `BVNOT
    (*

    Bit-wise negation (unary)

    *)
  36. | `BVNEG
    (*

    Arithmetic negation (unary)

    *)
  37. | `BVAND
    (*

    Bit-wise conjunction (binary)

    *)
  38. | `BVOR
    (*

    Bit-wise disjunction (binary)

    *)
  39. | `BVXOR
    (*

    Bit-wise exclusive disjunction (binary)

    *)
  40. | `BVADD
    (*

    Signed bitvector sum (binary)

    *)
  41. | `BVSUB
    (*

    Signed bitvector difference (binary)

    *)
  42. | `BVMUL
    (*

    Arithmetic multiplication (binary)

    *)
  43. | `BVUDIV
    (*

    Arithmetic integer division (binary)

    *)
  44. | `BVSDIV
    (*

    Arithmetic integer signed division (binary)

    *)
  45. | `BVUREM
    (*

    Arithmetic remainder (binary)

    *)
  46. | `BVSREM
    (*

    Arithmetic signed remainder (binary)

    *)
  47. | `BVSHL
    (*

    Logical shift left (binary)

    *)
  48. | `BVLSHR
    (*

    Logical shift right (binary)

    *)
  49. | `BVASHR
    (*

    Arithmetic shift right (binary)

    *)
  50. | `BVULT
  51. | `BVULE
  52. | `BVUGT
  53. | `BVUGE
  54. | `BVSLT
  55. | `BVSLE
  56. | `BVSGT
  57. | `BVSGE
  58. | `BVEXTRACT of Numeral.t * Numeral.t
    (*

    Extract subsequence from bitvector (unary)

    *)
  59. | `BVCONCAT
    (*

    Concatenation of bitvectors (binary)

    *)
  60. | `BVSIGNEXT of Numeral.t
    (*

    Sign extension of bitvector (unary)

    *)
  61. | `BVZEROEXT of Numeral.t
    (*

    Extend bitvector with zeros (unary)

    *)
  62. | `SELECT of Type.t
    (*

    Selection from array (binary)

    *)
  63. | `STORE
    (*

    Update of an array (ternary)

    *)
  64. | `CONST_ARRAY of Type.t
    (*

    Constant array (unary)

    *)
  65. | `IsConstructor of string
    (*

    ADT tester: (_ is CtorName), unary

    *)
  66. | `Selector of string * Type.t
    (*

    ADT field selector: name and result type, unary

    *)
]

The interpreted symbols

type symbol = [
  1. | interpreted_symbol
  2. | `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 key = t

Hash table over symbols

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

Set over symbols

module SymbolMap : Stdlib.Map.S with type key = t

Map over symbols

Constructor

val mk_symbol : symbol -> t

Create a symbol

val import : t -> t

Import a symbol built by another domain into the tables of this one

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

Constant cast to int symbol

val s_ubv_to_int : t

Constant cast ubv to int symbol

val s_sbv_to_int : t

Constant cast sbv to int symbol

val s_bv2nat : t

Constant cast bv to int (nat) symbol

val s_to_real : t

Constant cast to real symbol

val s_select : Type.t -> t

Array read operator

val s_store : t

array store symbol

val s_const_array : Type.t -> t
val s_extract : Numeral.t -> Numeral.t -> t

Bit-vector extract operator

val s_signext : Numeral.t -> t
val s_zeroext : Numeral.t -> t
val s_to_ubv : int -> t
val s_to_bv : int -> t
val s_bvneg : t

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_to_ubv : t -> bool

Return true if the symbol is a toubv

val is_to_bv : t -> bool

Return true if the symbol is a tobv

val is_select : t -> bool

Return true if the symbol is select from array

val is_const_array : t -> bool

Return true if the symbol is a constant 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