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=0fd6594f30d4e2bea97350a7906ecc2528c37e8fdd32588818a162aacc409688

md5=a0e9dda8f17c1f4f03119badd24d1bf5

module Th : Theory.S

Sourcetype t

Sourceexception Sat of t

Sourceexception Unsat of Explanation.t

Sourceexception I_dont_know of t

Sourceval empty : unit -> t

Sourceval empty_with_inst : (Expr.t -> bool) -> t

Sourceval assume : t -> Expr.gformula -> Explanation.t -> t

Sourceval assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t

Sourceval pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t

Sourceval unsat : t -> Expr.gformula -> Explanation.t

Sourceval print_model : header:bool -> Format.formatter -> t -> unit

Sourceval reset_refs : unit -> unit

Sourceval get_steps : unit -> int64

On This Page