AltErgoLib.Explanation
type exp =
| Literal of Satml_types.Atom.atom |
| Fresh of int |
| Bj of Expr.t |
| Dep of Expr.t |
| RootDep of string |
exception Inconsistent of t * AltErgoLib.Expr.Set.t list
val empty : t
val is_empty : t -> bool
val fresh_exp : unit -> exp
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
val literals_ids_of : t -> int MI.t
val make_deps : AltErgoLib.Expr.Set.t -> t
val has_no_bj : t -> bool