AltErgoLib.Relationinclude Sig_rel.RELATIONval timer : Timers.ty_moduleval empty : Uf.t -> t * Uf.GlobalDomains.tempty uf creates a new environment for this relation and allows for the registration of global domains in the union-find.
The second component of the pair should be Uf.domains uf with any domains that the relation requires added.
val assume :
t ->
Uf.t ->
Shostak.Combine.r Sig_rel.input list ->
t * Uf.GlobalDomains.t * Shostak.Combine.r Sig_rel.resultassume env uf la adds and processes the literals in la to the environment env.
The second value returned by this function can be used to update any relevant domain.
val query : t -> Uf.t -> Shostak.Combine.r Sig_rel.input -> Th_util.answerval case_split : t -> Uf.t -> for_model:bool -> Th_util.case_split listcase_split env returns a list of equalities
The returned case splits *must* have a CS origin; see the doc of Th_util.case_split.
The for_model flag is true when we are splitting for the purpose of generating a model; the case split may need to be more aggressive in this case to ensure completeness.
Note: not always equalities (e.g. the arrays theory returns disequalities)
val optimizing_objective :
t ->
Uf.t ->
Objective.Function.t ->
Th_util.optimized_split optionoptimizing_split env uf o tries to optimize objective o. Returns None if no theory knows how to optimize the objective.
If the function returns Some o then the value of the optimized split o is never Unknown because all the theories that support optimization will always produce an answer even if this answer is not the best value.
For instance, if the objective is a nonlinear arithmetical expressions of the form: 5 * x * x + 2 * y + 3, the arithmetic theory will translate this function into the linear objective function: 5 * U + 2 * y + 3 where U = x * x and send it to Ocplib-simplex.
val add :
t ->
Uf.t ->
Shostak.Combine.r ->
Expr.t ->
t
* Uf.GlobalDomains.t
* (Shostak.Combine.r Xliteral.view * Explanation.t) listadd a representant to take into account
val instantiate :
do_syntactic_matching:bool ->
(Matching_types.info AltErgoLib.Expr.Map.t
* Expr.t list AltErgoLib.Expr.Map.t AltErgoLib.Symbols.Map.t) ->
t ->
Uf.t ->
(Expr.t -> Expr.t -> bool) ->
t * Sig_rel.instancesval new_terms : t -> AltErgoLib.Expr.Set.tnew_terms env returns all the new terms created by the theory. These terms can be used to instantiate axiomes.
val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t