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.1.tbz

sha256=9cf8d69a0e457a939b86aba2a18c6154faba51d387b42a361ece55d329dd601d

sha512=09694d18496ba1938daaa7b4e28e6b3d6811687dd3aaede17917f20511be9d8328394fac021af683d4c0217d4b030da9a60a5b9c14d968f1948735ea7ec52543

doc/alt-ergo-lib/AltErgoLib/Arith/Shostak/argument-1-X/index.html

Parameter `Shostak.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 Sig.ac -> r

val ac_extract : r -> r Sig.ac option

val color : r Sig.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