module Symbol:sig
..end
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)
. A pairwise symbol is to be read as the conjunction of
each pair of arguments, for example
(<= 2 3))(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
typeinterpreted_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 ]
typesymbol =
[ `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 ]
type
t
val compare_symbols : t -> t -> int
val equal_symbols : t -> t -> bool
val hash_symbol : t -> int
module SymbolHashtbl:Hashtbl.S
with type key = t
module SymbolSet:Set.S
with type elt = t
module SymbolMap:Map.S
with type key = t
val mk_symbol : symbol -> t
val import : t -> t
val s_true : t
val s_false : t
val s_not : t
val s_and : t
val s_or : t
val s_implies : t
val s_ite : t
val s_eq : t
val s_geq : t
val s_leq : t
val s_gt : t
val s_lt : t
val s_mod : t
val s_plus : t
val s_minus : t
val s_times : t
val s_div : t
val s_select : Type.t -> t
val s_store : t
val node_of_symbol : t -> symbol
val is_numeral : t -> bool
val is_decimal : t -> bool
val is_select : t -> bool
val is_bool : t -> bool
`TRUE
or `FALSE
val numeral_of_symbol : t -> Numeral.t
`NUMERAL _
symbolval decimal_of_symbol : t -> Decimal.t
`DECIMAL _
symbolval bool_of_symbol : t -> bool
true
for the `TRUE
symbol and false
for the `FALSE
symbolval is_uf : t -> bool
val uf_of_symbol : t -> UfSymbol.t
val pp_print_symbol : Format.formatter -> t -> unit
val string_of_symbol : t -> string
val string_of_symbol_node : symbol -> string
val stats : unit -> int * int * int * int * int * int