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 Edit opam file Versions (15)

Authors

A

Alt-Ergo developers

Maintainers

O

OCamlPro <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.3.2.tar.gz

sha256=69418b8b959f695de06a85347d554efd5f2dd28a58a976e3f354abf9a58e108c

md5=efdf062a6bfdc1505637591b37334a28

doc/alt-ergo-lib/AltErgoLib/Shostak/Bitv/index.html

Module `Shostak.Bitv`Source

Sourcetype t = Combine.r Bitv.abstract

Type of terms of the theory

Sourcetype r = Combine.r

Type of representants of terms of the theory

Sourceval name : string

Name of the theory

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

return true if the symbol and the type are owned by the theory

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

Give a representant of a term of the theory

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

Sourceval color : r Sig.ac -> r

Sourceval type_info : t -> Ty.t

Sourceval embed : r -> t

Sourceval is_mine : t -> r

Sourceval leaves : t -> r list

Give the leaves of a term of the theory

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

Sourceval compare : r -> r -> int

Sourceval equal : t -> t -> bool

Sourceval hash : t -> int

solve r1 r2, solve the equality r1=r2 and return the substitution

Sourceval solve : r -> r -> r Sig.solve_pb -> r Sig.solve_pb

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

Sourceval fully_interpreted : Symbols.t -> bool

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

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