sig
  type t
  type r
  val empty : unit -> Sig.RELATION.t
  val assume :
    Sig.RELATION.t ->
    Sig.RELATION.r Sig.input list ->
    Sig.RELATION.t * Sig.RELATION.r Sig.result
  val query : Sig.RELATION.t -> Sig.RELATION.r Sig.input -> Sig.answer
  val case_split :
    Sig.RELATION.t ->
    (Sig.RELATION.r Literal.view * Explanation.t * Num.num) list
  val add : Sig.RELATION.t -> Sig.RELATION.r -> Sig.RELATION.t
end