Module UfSymbol

module UfSymbol: sig .. end
Uninterpreted function symbols
Author(s): Christoph Sticksel


Types and hash-consing


type uf_symbol = string 
Uninterpreted symbol are just strings of their name
type t 
Hashconsed uninterpreted symbol

Hashtables, maps and sets


val compare_uf_symbols : t -> t -> int
Comparison function on uninterpreted function symbols
val equal_uf_symbols : t -> t -> bool
Equality function on uninterpreted function symbols
val hash_uf_symbol : t -> int
Hashing function on uninterpreted function symbols
module UfSymbolHashtbl: Hashtbl.S  with type key = t
Hash table over uninterpreted function symbols
module UfSymbolSet: Set.S  with type elt = t
Set over uninterpreted function symbols
module UfSymbolMap: Map.S  with type key = t
Map over uninterpreted function symbols

Constructor


val mk_uf_symbol : string -> Type.t list -> Type.t -> t
Declare an uninterpreted symbol

mk_uf_symbol s a r constructs and returns an uninterpreted symbol with its name, the type of its arguments and the type of its result.

Uninterpreted symbols can only be constructed with this function in order to ensure that they are properly declared.

Declaring an uninterpreted function again with the same signature is harmless and will simply return the previously declared symbol. However, re-declaring an uninterpreted function with a different signature will raise an Invalid_argument exception.

val mk_fresh_uf_symbol : Type.t list -> Type.t -> t
Return a fresh uninterpreted symbol
val import : t -> t
Import an uninterpreted symbol from a different instance into this hashcons table

We may have clashes if we import fresh uninterpreted symbols from one instance to another.


Accessor functions


val uf_symbol_of_string : string -> t
Return a previously declared uninterpreted function symbol

Raise exception Not_found if symbol has not been declared.

val name_of_uf_symbol : t -> string
Return the name of the uninterpreted function symbol
val arg_type_of_uf_symbol : t -> Type.t list
Return the type of the arguments of the uninterpreted symbol
val res_type_of_uf_symbol : t -> Type.t
Return the type of the result of the uninterpreted symbol

Iterators over defined uninterpreted symbols


val fold_uf_declarations : (string -> Type.t list -> Type.t -> 'a -> 'a) -> 'a -> 'a
fold_declarations f a computes (f sN aN rN ... (f s2 a2 r2 (f
    s1 a1 r1 a))...)
, where sI, aI and rI, respectively are the name of the uninterpreted symbol, the types of its arguments and the type of its value.
val iter_uf_declarations : (string -> Type.t list -> Type.t -> unit) -> unit
iter_declarations f t iterates f over all declarations, calling f s a r on each, where s, a and r, respectively are the name of the uninterpreted symbol, the types of its arguments and the type of its value.

Pretty-printing


val pp_print_uf_symbol : Format.formatter -> t -> unit
Pretty-print a symbol
val string_of_uf_symbol : t -> string
Return a string representation of a symbol