sig
type t
type r
val name : string
val is_mine_symb : Symbols.t -> bool
val unsolvable : Sig.THEORY.t -> bool
val make : Term.t -> Sig.THEORY.r * Literal.LT.t list
val term_extract : Sig.THEORY.r -> Term.t option
val type_info : Sig.THEORY.t -> Ty.t
val embed : Sig.THEORY.r -> Sig.THEORY.t
val leaves : Sig.THEORY.t -> Sig.THEORY.r list
val subst : Sig.THEORY.r -> Sig.THEORY.r -> Sig.THEORY.t -> Sig.THEORY.r
val compare : Sig.THEORY.t -> Sig.THEORY.t -> int
val hash : Sig.THEORY.t -> int
val solve :
Sig.THEORY.r -> Sig.THEORY.r -> (Sig.THEORY.r * Sig.THEORY.r) list
val print : Format.formatter -> Sig.THEORY.t -> unit
val fully_interpreted : Symbols.t -> bool
module Rel :
sig
type t
type r = r
val empty : unit -> t
val assume : t -> r input list -> t * r result
val query : t -> r input -> answer
val case_split : t -> (r Literal.view * Explanation.t * Num.num) list
val add : t -> r -> t
end
end