#### msat

Library

Module

Module type

Parameter

Class

Class type

#### Type declarations

`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.

#### Proof building functions

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.

#### Proof Nodes

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

#### Proof Manipulation

`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.

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

`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.