type r = Shostak.Combine.rval empty : unit -> tval empty_facts : unit -> r Sig_rel.factsval add_fact : r Sig_rel.facts -> r Sig_rel.fact -> unitval add_term :
t ->
r Sig_rel.facts ->
Expr.t ->
Explanation.t ->
t * r Sig_rel.factsval add :
t ->
r Sig_rel.facts ->
Expr.t ->
Explanation.t ->
t * r Sig_rel.factsval assume_literals :
t ->
(r Sig_rel.literal * Explanation.t * Th_util.lit_origin) list ->
r Sig_rel.facts ->
t * (r Sig_rel.literal * Explanation.t * Th_util.lit_origin) listval case_split :
t ->
for_model:bool ->
(r Xliteral.view * bool * Th_util.lit_origin) list * tval query : t -> Expr.t -> Th_util.answerval new_terms : t -> Expr.Set.tval are_equal : t -> Expr.t -> Expr.t -> init_terms:bool -> Th_util.answerval are_distinct : t -> Expr.t -> Expr.t -> Th_util.answerval cl_extract : t -> Expr.Set.t listval print_model : Format.formatter -> t -> unitval assume_th_elt : t -> Expr.th_elt -> Explanation.t -> tval theories_instances :
do_syntactic_matching:bool ->
(Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t) ->
t ->
(Expr.t -> Expr.t -> bool) ->
t * Sig_rel.instances