Module Qed

module Qed: sig .. end
not exposed class inheriting smt_inplace_visitor

type qed_checker 
val create_qed_checker : Formula_type.formula -> qed_checker
Returns a Qed.qed_checker form a formula.

Note:The formula given is not meant to be modified

val qed_check_entry : qed_checker -> Formula_type.formula_entry -> unit
check the given entry
val qed_get_status : qed_checker -> Smtlib2.smt_result option
return the final status after all the entries have been provided to the checker. The two possible return values are: