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

Dune Dependency

alt-ergo.ocamlpro.com Readme Changelog LicenseRef-OCamlpro-Non-Commercial; Apache-2.0 License Edit opam file Versions (15)

Authors

A

Alt-Ergo developers

Maintainers

A

Alt-Ergo developers

Sources

alt-ergo-2.5.4.tbz

sha256=02c1e89398badafa89e612bc5d1883f2133a250685bf774cc5901c5581229bac

sha512=9f565c3f0d17328465832b8b107f048d67225bee23b83c7b02e820796201ca96cdb99574ff50c619badaadd5274b5c128d8f30e7532d44a1ee061a7e2d5d318d

doc/alt-ergo-lib/AltErgoLib/Sig/module-type-X/index.html

Module type `Sig.X`

type r

val save_cache : unit -> unit

saves the module's current cache

val reinit_cache : unit -> unit

restores the module's cache

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

val type_info : r -> Ty.t

val str_cmp : r -> r -> int

val hash_cmp : r -> r -> int

val equal : r -> r -> bool

val hash : r -> int

val leaves : r -> r list

val subst : r -> r -> r -> r

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

val term_embed : Expr.t -> r

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

val ac_embed : r ac -> r

val ac_extract : r -> r ac option

val color : r ac -> r

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

val is_a_leaf : r -> bool

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

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

val top : unit -> r

val bot : unit -> r

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

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

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