Previous  Up  Next

Module Symbol (.ml)


module Symbol: sig .. end
constant and function symbols

A symbol consists of

All symbols are irrevocably registered in a global symbol table.

Types


type sort =
| Predicate (*a predicate symbol of the input signature*)
| Function (*a function symbol of the input signature*)
| Skolem (*a skolem constant*)
| Connection (*a predicate that connects clauses split in preprocessing*)
| FD_Relation (*finite model finding: relational representation of functions (predicate). for each arity exists a unique relation symbol.*)
| FD_Size_Marker (*finite model finding: a marker for the domain size (predicate)*)
| FD_Element (*finite model finding: domain element (constant)*)
| FD_Symbol (*finite model finding: symbol of original signature transformed into a constant*)
each symbol has a sort. the basic sorts are predicates and functions from the input signature. In addition there are various sorts generated in the system, in skolemization, preprocessing, ...
type symbol
a symbol
module SymbolTable: Hashtbl.S  with type key = symbol
a specialized Hashtbl with symbols as keys.

Functions


Special Symbols



these special symbols are automatically added to the symbol table.
val equality : symbol
the equality symbol
val diff : symbol
the negated equality symbol
val lemma_root : symbol
used to denote the pseudo-predicate standing for the closed clause, when computing a lemma.

Creation


val create_predicate : string -> int -> symbol
Symbol.create_predicate name arity registers a predicate symbol and returns it.
val create_function : string -> int -> symbol
Symbol.create_function name arity registers a function symbol and returns it.
val create_skolem : ?arity:int -> ?name:string option -> unit -> symbol
creates a unique fresh skolem symbol. arity is 0 by default, so a skolem constant will be created.
val create_connection : int -> symbol
creates a unique fresh connection symbol of the given arity.
val get_fd_relation : int -> symbol
returns the relation symbol of the given arity.

this symbol has the given arity, that is it represents function symbols of arity - 2.

val get_fd_size_marker : int -> symbol
returns the maker symbol of the given domain size.
val get_fd_element : int -> symbol
returns the i.th domain element. to_string ~pretty returns i.
val create_fd_symbol : symbol -> symbol
returns the constant symbol which is the transformation of the given constant/function symbol.
val get_symbol_from_fd_symbol : symbol -> symbol
reverse function to Symbol.create_fd_symbol. fails with an exception if Symbol.create_fd_symbol has not been called before.

Decomposition


val name : symbol -> string
the symbol's unique name.
val arity : symbol -> int
the symbol arity.
val id : symbol -> int
the symbol' uniqe id. Useful for hashing on symbols or terms.
val sort : symbol -> sort
the symbol's sort

Comparison


val equal : symbol -> symbol -> bool
the same symbol?
val compare : symbol -> symbol -> int
total order by id.
val compare_name : symbol -> symbol -> int
total order by name.
val is_predicate : symbol -> bool
a predicate symbol (sort = Predicate)?
val is_function : symbol -> bool
a function symbol (sort = Function)?
val is_input : symbol -> bool
a symbol from the input signature? Same as is_predicate || is_function.
val is_skolem : symbol -> bool
a skolem symbol?
val is_connection : symbol -> bool
a connection symbol?
val is_fd_relation : symbol -> bool
a finite domain relation symbol?
val is_fd_size_marker : symbol -> bool
a finite domain marker symbol?
val is_fd_element : symbol -> bool
a finite domain element symbol?
val is_fd_symbol : symbol -> bool
a finite domain function symbol?

String Representation


val to_string : ?pretty:bool -> symbol -> string
print a symbol. pretty (default: true) printing prints e.g. domain elements as '1 instead of __fd1
val sort_to_string : sort -> string
string representation of a sort.