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 LicenseRef-OCamlPro-Non-Commercial-Purpose-License-Version-1 License Edit opam file Versions (15)

Authors

A

Alt-Ergo developers

Maintainers

O

OCamlPro <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.3.0.tar.gz

sha256=7f1906900272125315833b9f0a6abc3c5af7b836d604fdb10a98a9079c1b99f9

md5=d99bfaf748f7c640222e59677e6afd7c

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

Module `Ite.Shostak`Source

Parameters

module X : ALIEN

Signature

Sourcetype t = X.r abstract

Type of terms of the theory

Sourcetype r = X.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

On This Page

Parameters
Signature