Module Make_mcsat.Proof

exception Resolution_error of string
type atom = Atom.t
type clause = Clause.t
type formula = Formula.t
type lemma = Plugin.proof
val error_res_f : ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
val clear_var_of_ : atom -> unit
val resolve : clause -> clause -> atom list * atom list
val find_dups : clause -> atom list * atom list
val same_lits : atom Iter.t -> atom Iter.t -> bool
val prove : clause -> clause
val set_atom_proof : atom -> clause
val prove_unsat : clause -> clause
val prove_atom : atom -> clause option
type t = clause
and proof_node = {
conclusion : clause;
step : step;
}
and step =
| Hypothesis of lemma
| Assumption
| Lemma of lemma
| Duplicate of t * atom list
| Hyper_res of hyper_res_step
and hyper_res_step = {
hr_init : t;
hr_steps : (atom * t) list;
}
val conclusion : t -> clause
type res_step = {
rs_res : atom list;
rs_c1 : clause;
rs_c2 : clause;
rs_pivot : atom;
}
val find_pivots : clause -> clause list -> atom list * (atom * t) list
val expand : clause -> proof_node
val res_of_hyper_res : hyper_res_step -> t * t * atom
val is_leaf : step -> bool
val parents : step -> t list
val expl : step -> string
val unsat_core : clause -> clause list
module Tbl = Clause.Tbl
type task =
| Enter of t
| Leaving of t
val spop : 'a Stack.t -> 'a option
val fold_aux : task Stack.t -> bool Tbl.t -> ('a -> proof_node -> 'a) -> 'a -> 'a
val fold : ('a -> proof_node -> 'a) -> 'a -> t -> 'a
val check_empty_conclusion : t -> unit
val check : t -> unit