package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

The Alt-Ergo SMT prover library

Install

dune-project

Dependency

alt-ergo.ocamlpro.com Readme Changelog LicenseRef-OCamlpro-Non-Commercial; Apache-2.0 License Edit opam file Versions (15)

Authors

A

Alt-Ergo developers <alt-ergo@ocamlpro.com>

Maintainers

A

Alt-Ergo developers <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.6.2.tbz

sha256=39e2c9128a7d1e89f332e31a2716f359f3b9e1a925fe81f11fa4a749b5d24d82

sha512=ca953fe5a4964287de7e328ec4e3724a9baaa908c22862b075da5870bbf3707c7f78bd9fe0af98ee6c6382b5de0a4ddfcc93e09dc8b5b8e7d6ab6b1196a0656d

doc/alt-ergo-lib/AltErgoLib/Relation/index.html

Module `AltErgoLib.Relation`

include Sig_rel.RELATION

type t

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