type r = Shostak.Combine.rval empty : 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 -> Th_util.case_split list * tval optimizing_objective :
t ->
Objective.Function.t ->
Th_util.optimized_split optionval query : t -> Expr.t -> Th_util.answerval new_terms : t -> Expr.Set.tval class_of : t -> Expr.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 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.instancesval extract_concrete_model :
prop_model:Expr.Set.t ->
declared_ids:Id.typed list ->
t ->
Models.t