Module `Msat_sat.Proof`

A module to manipulate proofs.

type formula = formula
type atom = atom
type lemma = lemma
type clause = clause: Abstract types for atoms, clauses and theory-specific lemmas

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

and proof_node = { conclusion : 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 of lemma The conclusion is a user-provided hypothesis | Assumption The conclusion has been locally assumed by the user | Lemma of lemma The conclusion is a tautology provided by the theory, with associated proof | Duplicate of t * atom list The conclusion is obtained by eliminating multiple occurences of the atom in the conclusion of the provided proof. | Hyper_res of hyper_res_step: The type of reasoning steps allowed in a proof.

and hyper_res_step = { hr_init : t; hr_steps : (atom * t) list; }

val prove : clause -> t

Given a clause, return a proof of that clause.

val prove_unsat : clause -> t

Given a conflict clause c, returns a proof of the empty clause.

val prove_atom : atom -> t option: Given an atom a, returns a proof of the clause [a] if a is true at level 0

val res_of_hyper_res : hyper_res_step -> t * t * atom: Turn an hyper resolution step into a resolution step. The conclusion can be deduced by performing a resolution between the conclusions of the two given proofs. The atom on which to perform the resolution is also given.

val is_leaf : step -> bool: Returns wether the 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.

val 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).

val expand : t -> proof_node: Return the proof step at the root of a given proof.

val fold : ('a -> proof_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.

val unsat_core : t -> 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 check_empty_conclusion : t -> unit

Check that the proof's conclusion is the empty clause,

val check : t -> unit: Check the contents of a proof. Mainly for internal use.

module Tbl : Hashtbl.S with type Tbl.key = t

`conclusion : clause;`	The conclusion of the proof
`step : step;`	The reasoning step used to prove the conclusion

`\|` `Hypothesis of lemma`	The conclusion is a user-provided hypothesis
`\|` `Assumption`	The conclusion has been locally assumed by the user
`\|` `Lemma of lemma`	The conclusion is a tautology provided by the theory, with associated proof
`\|` `Duplicate of t * atom list`	The conclusion is obtained by eliminating multiple occurences of the atom in the conclusion of the provided proof.
`\|` `Hyper_res of hyper_res_step`