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

Sourcetype r

Sourceval make : Expr.t -> r * Expr.t list

Sourceval type_info : r -> Ty.t

Sourceval str_cmp : r -> r -> int

Sourceval hash_cmp : r -> r -> int

Sourceval equal : r -> r -> bool

Sourceval hash : r -> int

Sourceval leaves : r -> r list

Sourceval subst : r -> r -> r -> r

Sourceval solve : r -> r -> (r * r) list

Sourceval term_embed : Expr.t -> r

Sourceval term_extract : r -> Expr.t option * bool

Sourceval ac_embed : r Sig.ac -> r

Sourceval ac_extract : r -> r Sig.ac option

Sourceval color : r Sig.ac -> r

Sourceval fully_interpreted : Symbols.t -> Ty.t -> bool

Sourceval is_a_leaf : r -> bool

Sourceval print : Format.formatter -> r -> unit

Sourceval abstract_selectors : r -> (r * r) list -> r * (r * r) list

Sourceval top : unit -> r

Sourceval bot : unit -> r

Sourceval is_solvable_theory_symbol : Symbols.t -> Ty.t -> bool

Sourceval assign_value : r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option

Sourceval choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string