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.3.tar.gz

sha256=52e9e9cdbedf7afd1b32154dfb71ca7bead44fa2efcab7eb6d9ccc1989129388

md5=3b060044767d16d1de3416944abd2dd5

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

Module `AltErgoLib.Explanation`Source

Sourcetype t

Sourcetype exp =

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

Sourceexception Inconsistent of t * Expr.Set.t list

Sourceval empty : t

Sourceval is_empty : t -> bool

Sourceval mem : exp -> t -> bool

Sourceval singleton : exp -> t

Sourceval union : t -> t -> t

Sourceval merge : t -> t -> t

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

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

Sourceval fresh_exp : unit -> exp

Sourceval remove_fresh : exp -> t -> t option

Sourceval remove : exp -> t -> t

Sourceval add_fresh : exp -> t -> t

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

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

Sourceval formulas_of : t -> Expr.Set.t

Sourceval bj_formulas_of : t -> Expr.Set.t

Sourcemodule MI : Map.S with type key = int

Sourceval literals_ids_of : t -> int MI.t

Sourceval make_deps : Expr.Set.t -> t

Sourceval has_no_bj : t -> bool

Sourceval compare : t -> t -> int

Sourceval subset : t -> t -> bool