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