package alt-ergo-lib

  1. Overview
  2. Docs
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

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

Maintainers

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

Sources

alt-ergo-2.6.1.tbz
sha256=df56045a3af79fbcfbd1deeaf09012d5bc390b4c2223e1d9c25c11c301d9eeba
sha512=ff83e5ce7598bc30509be8ca2c14d791856b0269f852903f81216ae1cbc27737d90b6313176fa24768944433b875811ee19b51fc821948634ea678dbcca4befb

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

Module AltErgoLib.Uf

Uf module

type t
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