Module Mc2_core.Proof
Resolution proofs
This modules defines functions to create and manipulate resolution proofs.
Type declarations
type t
Lazy type for proof trees. Proofs are persistent objects, and can be extended to proof nodes using functions defined later.
and node
=
{
conclusion : Mc2_core__.Solver_types.clause;
The conclusion of the proof
step : step;
The reasoning step used to prove the conclusion
}
A proof can be expanded into a proof node, which show the first step of the proof.
and step
=
|
Hypothesis
The conclusion is a user-provided hypothesis
|
Assumption
The conclusion has been locally assumed by the user
|
Lemma of Mc2_core__.Solver_types.lemma
The conclusion is a tautology provided by the theory, with associated proof
|
Simplify of
{
init : t;
duplicates : Mc2_core__.Solver_types.atom list;
absurd : Mc2_core__.Solver_types.atom list;
}
The conclusion is obtained by eliminating multiple occurrences of atoms in the conclusion of the provided proof, and removing some absurd atoms.
|
Hyper_res of
{
init : t;
steps : Mc2_core__.Solver_types.premise_step list;
}
The conclusion can be deduced by performing a series of resolution steps between
init
and, successively, each clause in the list on the corresponding pivot atom.A proof can be expanded into a proof node, which show the first step of the proof.
The type of reasoning steps allowed in a proof.
val conclusion : node -> Mc2_core__.Solver_types.clause
val step : node -> step
Proof building functions
val prove : Mc2_core__.Solver_types.clause -> t
Given a clause, return a proof of that clause.
- raises Util.Error
if it does not succeed.
val prove_unsat : Mc2_core__.Solver_types.clause -> t
Given a conflict clause
c
, returns a proof of the empty clause.- raises Util.Error
if it does not succeed
val prove_atom : Mc2_core__.Solver_types.atom -> t option
Given an atom
a
, returns a proof of the clause[a]
ifa
is true at level 0
Proof Nodes
val is_leaf : step -> bool
Returns whether the proof node is a leaf, i.e. an hypothesis, an assumption, or a lemma.
true
if and only ifparents
returns the empty list.
val expl : step -> string
Returns a short string description for the proof step; for instance
"hypothesis"
for aHypothesis
(it currently returns the variant name in lowercase).
Proof Manipulation
val fold : ('a -> node -> 'a) -> 'a -> t -> 'a
fold f acc p
, foldf
over the proofp
and all its node. It is guaranteed thatf
is executed exactly once on each proof node in the tree, and that the execution off
on a proof node happens after the execution on the parents of the nodes.
val iter : (node -> unit) -> t -> unit
val unsat_core : t -> Mc2_core__.Solver_types.clause list
Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof. More efficient than using the
fold
function since it has access to the internal representation of proofs
val debug_step : step CCFormat.printer
Misc
val check_step : t -> unit
Check only this proof step
val check : t -> unit
Check the contents of a proof. Mainly for internal use
Unsafe
module H : CCHashtbl.S with type H.key = Mc2_core__.Solver_types.clause
Hashtable over clauses. Uses the details of the internal representation to achieve the best performances, however hashtables from this module become invalid when solving is restarted, so they should only be live during inspection of a single proof.