package alt-ergo-lib
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=39e2c9128a7d1e89f332e31a2716f359f3b9e1a925fe81f11fa4a749b5d24d82
sha512=ca953fe5a4964287de7e328ec4e3724a9baaa908c22862b075da5870bbf3707c7f78bd9fe0af98ee6c6382b5de0a4ddfcc93e09dc8b5b8e7d6ab6b1196a0656d
doc/alt-ergo-lib/AltErgoLib/Relation/index.html
Module AltErgoLib.Relation
include Sig_rel.RELATION
val timer : Timers.ty_module
val empty : Uf.t -> t * Uf.GlobalDomains.t
empty 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.result
assume 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.answer
val case_split : t -> Uf.t -> for_model:bool -> Th_util.case_split list
case_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 option
optimizing_split env uf o
tries to optimize objective o
. Returns None
if the theory cannot optimize the objective.
val add :
t ->
Uf.t ->
Shostak.Combine.r ->
Expr.t ->
t
* Uf.GlobalDomains.t
* (Shostak.Combine.r Xliteral.view * Explanation.t) list
add a representant to take into account
val instantiate :
do_syntactic_matching:bool ->
(Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t) ->
t ->
Uf.t ->
(Expr.t -> Expr.t -> bool) ->
t * Sig_rel.instances
val new_terms : t -> Expr.Set.t
new_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