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

sha256=52e9e9cdbedf7afd1b32154dfb71ca7bead44fa2efcab7eb6d9ccc1989129388

md5=3b060044767d16d1de3416944abd2dd5

Sourcemodule SA : Set.S with type elt = Expr.t * Explanation.t

Sourcetype t

Sourcetype r = Shostak.Combine.r

Sourceval empty : t

Sourceval find : r -> t -> Expr.Set.t * SA.t

Sourceval add : r -> (Expr.Set.t * SA.t) -> t -> t

Sourceval mem : r -> t -> bool

Sourceval print : t -> unit

Sourceval up_add : t -> Expr.t -> r -> r list -> t

Sourceval congr_add : t -> r list -> Expr.Set.t

Sourceval up_close_up : t -> r -> r -> t

Sourceval congr_close_up : t -> r -> r list -> Expr.Set.t * SA.t