package mc2
Install
Dune Dependency
Authors
Maintainers
Sources
md5=92de696251ec76fbf3eba6ee917fd80f
sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0
doc/mc2.core/Mc2_core/Proof/index.html
Module Mc2_core.ProofSource
Resolution proofs
This modules defines functions to create and manipulate resolution proofs.
Type declarations
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
*)initand, 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.
Proof building functions
Given a conflict clause c, returns a proof of the empty clause.
Given an atom a, returns a proof of the clause [a] if a is true at level 0
Proof Nodes
Returns whether the proof node is a leaf, i.e. an hypothesis, an assumption, or a lemma. true if and only if parents returns the empty list.
Returns a short string description for the proof step; for instance "hypothesis" for a Hypothesis (it currently returns the variant name in lowercase).
Proof Manipulation
fold f acc p, fold f over the proof p and all its node. It is guaranteed that f is executed exactly once on each proof node in the tree, and that the execution of f on a proof node happens after the execution on the parents of the nodes.
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
Misc
Unsafe
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.