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/Uf/index.html

Module `AltErgoLib.Uf`

Uf module

type t

type r = Shostak.Combine.r

type _ id = ..

Extensible type for global domains identifiers, see GlobalDomains.

val src : Logs.src

module type GlobalDomain = sig ... end

Module signature for global domains used by the union-find module.

type 'a global_domain = (module GlobalDomain with type t = 'a)

The type of global domain modules with a given storage type (see GlobalDomain).

module GlobalDomains : sig ... end

This module provides a registry type to access and update a single "current" instance associated with multiple global domain types.

module LX = Shostak.L

val empty : t

val add : t -> Expr.t -> t * Expr.t list

val mem : t -> Expr.t -> bool

val find : t -> Expr.t -> r * Explanation.t

val find_r : t -> r -> r * Explanation.t

val domains : t -> GlobalDomains.t

val set_domains : t -> GlobalDomains.t -> t

val union : 
  t ->
  r ->
  r ->
  Explanation.t ->
  t * (r * (r * r * Explanation.t) list * r) list

val distinct : t -> r list -> Explanation.t -> t

val are_equal : t -> Expr.t -> Expr.t -> added_terms:bool -> Th_util.answer

val are_distinct : t -> Expr.t -> Expr.t -> Th_util.answer

val already_distinct : t -> r list -> bool

val class_of : t -> Expr.t -> Expr.Set.t

val rclass_of : t -> r -> Expr.Set.t

val cl_extract : t -> Expr.Set.t list

val print : t -> unit

val term_repr : t -> Expr.t -> Expr.t

val make : t -> Expr.t -> r

val is_normalized : t -> r -> bool

val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t

Counterexample function

val extract_concrete_model : 
  prop_model:Expr.Set.t ->
  declared_ids:Id.typed list ->
  t ->
  Models.t

Compute a counterexample using the Uf environment

val save_cache : unit -> unit

saves the module's cache

val reinit_cache : unit -> unit

reinitializes the module's cache with the saved one

On This Page

Uf module
1. Counterexample function