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 <alt-ergo@ocamlpro.com>

Maintainers

A

Alt-Ergo developers <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.6.1.tbz

sha256=df56045a3af79fbcfbd1deeaf09012d5bc390b4c2223e1d9c25c11c301d9eeba

sha512=ff83e5ce7598bc30509be8ca2c14d791856b0269f852903f81216ae1cbc27737d90b6313176fa24768944433b875811ee19b51fc821948634ea678dbcca4befb

doc/alt-ergo-lib/AltErgoLib/Explanation/index.html

Module `AltErgoLib.Explanation`

type t

type rootdep = {

name : string;
f : Expr.t;
loc : Loc.t;

}

type exp =

| Literal of Satml_types.Atom.atom
| Fresh of int
| Bj of Expr.t
| Dep of Expr.t
| RootDep of rootdep

exception Inconsistent of t * Expr.Set.t list

val empty : t

val is_empty : t -> bool

val mem : exp -> t -> bool

val singleton : exp -> t

val union : t -> t -> t

val merge : t -> t -> t

val iter_atoms : (exp -> unit) -> t -> unit

val fold_atoms : (exp -> 'a -> 'a) -> t -> 'a -> 'a

val fresh_exp : unit -> exp

val exists_fresh : t -> bool

Does there exists a Fresh _ exp in an explanation set.

val remove_fresh : exp -> t -> t option

val remove : exp -> t -> t

val add_fresh : exp -> t -> t

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

val get_unsat_core : t -> rootdep list

val print_unsat_core : ?tab:bool -> Format.formatter -> t -> unit

val formulas_of : t -> Expr.Set.t

val bj_formulas_of : t -> Expr.Set.t

module MI : Map.S with type key = int

val make_deps : Expr.Set.t -> t

val has_no_bj : t -> bool

val compare : t -> t -> int

val subset : t -> t -> bool