package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module AltErgoLib.ExplanationSource

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

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

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 get_unsat_core : t -> rootdep list
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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct