Module type Sig.THEORY

module type THEORY = sig .. end

type t 

Type of terms of the theory

type r 

Type of representants of terms of the theory

val name : string

Name of the theory

val is_mine_symb : Symbols.t -> bool

return true if the symbol is owned by the theory

val unsolvable : t -> bool

return true when the argument is an unsolvable function of the theory

val make : Term.t -> r * Literal.LT.t list

Give a representant of a term of the theory

val term_extract : r -> Term.t option
val type_info : t -> Ty.t
val embed : r -> t
val leaves : t -> r list

Give the leaves of a term of the theory

val subst : r -> r -> t -> r
val compare : t -> t -> int
val hash : t -> int

solve r1 r2, solve the equality r1=r2 and return the substitution

val solve : r -> r -> (r * r) list
val print : Format.formatter -> t -> unit
val fully_interpreted : Symbols.t -> bool
module Rel: Sig.RELATION  with type r = r