package alt-ergo-lib

  1. Overview
  2. Docs
The Alt-Ergo SMT prover library

Install 

dune-project
 Dependency

alt-ergo.ocamlpro.com Edit opam file Versions (15)

Authors

  1. A
    Alt-Ergo developers

Maintainers

  1. O
    OCamlPro <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.3.2.tar.gz
sha256=69418b8b959f695de06a85347d554efd5f2dd28a58a976e3f354abf9a58e108c
md5=efdf062a6bfdc1505637591b37334a28

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

Module AltErgoLib.ExplanationSource

Sourcetype t
Sourcetype exp =
  1. | Literal of Satml_types.Atom.atom
  2. | Fresh of int
  3. | Bj of Expr.t
  4. | Dep of Expr.t
  5. | 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