val empty : unit -> tval assume :
?ordered:bool ->
(Shostak.Literal.t * Th_util.lit_origin * Explanation.t * int * int) list ->
t ->
t * Expr.Set.t * intval add_objective : t -> Objective.Function.t -> Objective.Value.t -> tadd_objective env fn value indicates that the objective fn has been optimized to value.
val query : Expr.t -> t -> Th_util.answerval cl_extract : t -> Expr.Set.t listval extract_ground_terms : t -> Expr.Set.tval get_real_env : t -> Ccx.Main.tval get_case_split_env : t -> Ccx.Main.tval do_optimize : acts:Shostak.Literal.t Th_util.acts -> t -> unitval do_case_split :
?acts:Shostak.Literal.t Th_util.acts ->
t ->
Util.case_split_policy ->
t * Expr.Set.tval compute_concrete_model : acts:Shostak.Literal.t Th_util.acts -> t -> unitval extract_concrete_model :
declared_ids:Id.typed list ->
t ->
Models.t Lazy.t * Objective.Model.tval 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) ->
int ->
int ->
t * Sig_rel.instancesval get_assumed : t -> Expr.Set.tval get_objectives : t -> Objective.Model.t