package alt-ergo-lib

  1. Overview
  2. Docs
The Alt-Ergo SMT prover library

Install 

dune-project
 Dependency

alt-ergo.ocamlpro.com Edit opam file Versions (15)

Authors

  1. A
    Alt-Ergo developers

Maintainers

  1. O
    OCamlPro <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.3.3.tar.gz
sha256=52e9e9cdbedf7afd1b32154dfb71ca7bead44fa2efcab7eb6d9ccc1989129388
md5=3b060044767d16d1de3416944abd2dd5

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

Module AltErgoLib.UfSource

Sourcetype t
Sourcemodule LX : Xliteral.S with type elt = r
Sourceval empty : unit -> t
Sourceval add : t -> Expr.t -> t * Expr.t list
Sourceval mem : t -> Expr.t -> bool
Sourceval find : t -> Expr.t -> r * Explanation.t
Sourceval find_r : t -> r -> r * Explanation.t
Sourceval union : t -> r -> r -> Explanation.t -> t * (r * (r * r * Explanation.t) list * r) list
Sourceval distinct : t -> r list -> Explanation.t -> t
Sourceval are_equal : t -> Expr.t -> Expr.t -> added_terms:bool -> Th_util.answer
Sourceval are_distinct : t -> Expr.t -> Expr.t -> Th_util.answer
Sourceval already_distinct : t -> r list -> bool
Sourceval class_of : t -> Expr.t -> Expr.t list
Sourceval rclass_of : t -> r -> Expr.Set.t
Sourceval cl_extract : t -> Expr.Set.t list
Sourceval model : t -> (r * Expr.t list * (Expr.t * r) list) list * Expr.t list list
Sourceval print : Format.formatter -> t -> unit
Sourceval term_repr : t -> Expr.t -> Expr.t
Sourceval make : t -> Expr.t -> r
Sourceval is_normalized : t -> r -> bool
Sourceval assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t
Sourceval output_concrete_model : t -> unit