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

md5=35d6c6f3fa43bcd10fe7f524b1eb59ca

sha512=c3eee41d3c588ca89c2a1eebe9f10914ef647743b58fb562b682172cf6b6bdeb0920ebbba8a850820c0cb53bad0260f11b82fe71f00830ea9b33f5bb5d4fd048

module Th : Theory.S

Sourcetype t

Sourceexception Bottom of Explanation.t * Expr.Set.t list * t

Sourceval empty : unit -> t

Sourceval is_true : t -> Expr.t -> (Explanation.t Lazy.t * int) option

Sourceval assume : bool -> t -> (Expr.gformula * Explanation.t) list -> t

Sourceval decide : t -> Expr.t -> int -> t

Sourceval forget_decision : t -> Expr.t -> int -> t

Sourceval reset_decisions : t -> t

Sourceval get_decisions : t -> (int * Expr.t) list

On This Page