Module Mc2_core.ProofSource

Resolution proofs

This modules defines functions to create and manipulate resolution proofs.

Type declarations

Sourcetype t

Lazy type for proof trees. Proofs are persistent objects, and can be extended to proof nodes using functions defined later.

Sourceand node = {
  1. conclusion : Mc2_core__.Solver_types.clause;
    (*

    The conclusion of the proof

    *)
  2. 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.

Sourceand step =
  1. | Hypothesis
    (*

    The conclusion is a user-provided hypothesis

    *)
  2. | Assumption
    (*

    The conclusion has been locally assumed by the user

    *)
  3. | Lemma of Mc2_core__.Solver_types.lemma
    (*

    The conclusion is a tautology provided by the theory, with associated proof

    *)
  4. | Simplify of {
    1. init : t;
    2. duplicates : Mc2_core__.Solver_types.atom list;
    3. 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.

    *)
  5. | Hyper_res of {
    1. init : t;
    2. 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.

Sourceval conclusion : node -> Mc2_core__.Solver_types.clause
Sourceval step : node -> step

Proof building functions

Sourceval prove : Mc2_core__.Solver_types.clause -> t

Given a clause, return a proof of that clause.

  • raises Util.Error

    if it does not succeed.

Sourceval 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

Sourceval prove_atom : Mc2_core__.Solver_types.atom -> t option

Given an atom a, returns a proof of the clause [a] if a is true at level 0

Proof Nodes

Sourceval 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 if parents returns the empty list.

Sourceval expl : step -> string

Returns a short string description for the proof step; for instance "hypothesis" for a Hypothesis (it currently returns the variant name in lowercase).

Sourceval parents : step -> t list

Returns the parents of a proof node.

Proof Manipulation

Sourceval expand : t -> node

Return the proof step at the root of a given proof.

Sourceval fold : ('a -> node -> 'a) -> 'a -> t -> 'a

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.

Sourceval iter : (node -> unit) -> t -> unit
Sourceval 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

Sourceval debug_step : step CCFormat.printer

Misc

Sourceval check_step : t -> unit

Check only this proof step

Sourceval check : t -> unit

Check the contents of a proof. Mainly for internal use

Unsafe

Sourcemodule H : CCHashtbl.S with type 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.