package alt-ergo-lib

  1. Overview
  2. Docs
type 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 string
exception Inconsistent of t * AltErgoLib.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 remove_fresh : exp -> t -> t option
val remove : exp -> t -> t
val add_fresh : exp -> t -> t
val print : Stdlib.Format.formatter -> t -> unit
val print_unsat_core : ?tab:bool -> Stdlib.Format.formatter -> t -> unit
val formulas_of : t -> AltErgoLib.Expr.Set.t
val bj_formulas_of : t -> AltErgoLib.Expr.Set.t
module MI : Stdlib.Map.S with type key = int
val literals_ids_of : t -> int MI.t
val make_deps : AltErgoLib.Expr.Set.t -> t
val has_no_bj : t -> bool
val compare : t -> t -> int
val subset : t -> t -> bool
OCaml

Innovation. Community. Security.