Functor Sum.Make (.ml)

module Make: functor (X : ALIEN) -> Sig.THEORY  with type r = X.r and type t = X.r abstract

Parameters:

X : ALIEN

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