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

A

Alt-Ergo developers

Sources

2.4.2.tar.gz

md5=c47327ae132c860890c820bfd5d49d51

sha512=61ae181ccd60a49f833ea79bbd5184a46f8eef24e7fe1169b15e905ed86584bdbe993ef86c203d5bfc3d79961024f96af0e4e623dc15479aa9538648291c9a75

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

Module `Shostak.Records`

type t = Combine.r Records.abstract

Type of terms of the theory

type r = Combine.r

Type of representants of terms of the theory

val name : string

Name of the theory

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

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

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

Give a representant of a term of the theory

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

val color : r Sig.ac -> r

val type_info : t -> Ty.t

val embed : r -> t

val is_mine : t -> r

val leaves : t -> r list

Give the leaves of a term of the theory

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

val compare : r -> r -> int

val equal : t -> t -> bool

val hash : t -> int

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

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

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

val fully_interpreted : Symbols.t -> bool

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

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