Functor Arith.Make (.ml)

module Make: functor (X : Sig.X) -> functor (P : Polynome.T  with type r = X.r) -> functor (C : Sig.C  with type t = P.t and type r = X.r) -> Sig.THEORY  
  with type r = X.r and type t = P.t

Parameters:

`X`	:	`Sig.X`
`P`	:	`Polynome.T with type r = X.r`
`C`	:	`Sig.C with type t = P.t and type r = X.r`

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