Module UfSymbol

Uninterpreted function symbols

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 : Stdlib.Hashtbl.S with type key = t

Hash table over uninterpreted function symbols

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

Set over uninterpreted function symbols

module UfSymbolMap : Stdlib.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 : Stdlib.Format.formatter -> t -> unit

Pretty-print a symbol

val string_of_uf_symbol : t -> string

Return a string representation of a symbol