package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 literals_ids_of : t -> int MI.t
val make_deps : Expr.Set.t -> t
val has_no_bj : t -> bool
val compare : t -> t -> int
val 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