package alt-ergo-lib

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

Install 

dune-project
 Dependency

alt-ergo.ocamlpro.com Readme Changelog LicenseRef-OCamlpro-Non-Commercial; Apache-2.0 License Edit opam file Versions (16)

Authors

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

Maintainers

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

Sources

alt-ergo-2.6.3.tbz
sha256=4ac2b5d8ae6c54a11a0cc349ec76a153aa95727bf57ef9cb3309a706a7fb1bfa
sha512=68b952ec7940c9f5d8ec9750420a6fd9ccaf6ca149ce96f5c32bbd8ff3b07481940b8c2938815b8540df1369e06da02f1edcbaeda809e8386be186011b7dd962

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

Module AltErgoLib.Explanation

type t
type rootdep = {
  1. name : string;
  2. f : Expr.t;
  3. loc : Loc.t;
}
type 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 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