Previous  Up  Next

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:

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.
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
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_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