mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-28 12:24:50 -05:00
14 lines
No EOL
12 KiB
HTML
14 lines
No EOL
12 KiB
HTML
<!DOCTYPE html>
|
|
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-S (sidekick.Sidekick_backend__Coq.Make.1-S)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><meta name="generator" content="doc-ock-html v1.0.0-1-g1fc9bf0"/></head><body><nav id="top"><a href="../index.html">Up</a> — <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Parameter</span> <span class="module-path">Sidekick_backend__Coq.Make.1-S</span></h1></header><p>Signature for a module handling proof by resolution from sat solving traces</p><h4>Type declarations</h4><div class="spec exception" id="exception-Insufficient_hyps"><a href="#exception-Insufficient_hyps" class="anchor"></a><div class="def exception"><code><span class="keyword">exception </span></code><code><span class="exception">Insufficient_hyps</span></code></div><div class="doc"><p>Raised when a complete resolution derivation cannot be found using the current hypotheses.</p></div></div><div class="spec type" id="type-formula"><a href="#type-formula" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>formula</code><code></code><code></code></div><div class="doc"></div></div><div class="spec type" id="type-atom"><a href="#type-atom" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>atom</code><code></code><code></code></div><div class="doc"></div></div><div class="spec type" id="type-lemma"><a href="#type-lemma" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>lemma</code><code></code><code></code></div><div class="doc"></div></div><div class="spec type" id="type-clause"><a href="#type-clause" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>clause</code><code></code><code></code></div><div class="doc"><p>Abstract types for atoms, clauses and theory-specific lemmas</p></div></div><div class="spec type" id="type-proof"><a href="#type-proof" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>proof</code><code></code><code></code></div><div class="doc"><p>Lazy type for proof trees. Proofs are persistent objects, and can be
|
|
extended to proof nodes using functions defined later.</p></div></div><div class="spec type" id="type-proof_node"><a href="#type-proof_node" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>proof_node</code><code></code><code><span class="keyword"> = </span></code><code>{</code><table class="record"><tr id="type-proof_node.conclusion" class="anchored"><td class="def field"><a href="#type-proof_node.conclusion" class="anchor"></a><code>conclusion : <a href="index.html#type-clause">clause</a>;</code></td><td class="doc"><p>(** The conclusion of the proof *)</p></td></tr><tr id="type-proof_node.step" class="anchored"><td class="def field"><a href="#type-proof_node.step" class="anchor"></a><code>step : <a href="index.html#type-step">step</a>;</code></td><td class="doc"><p>(** The reasoning step used to prove the conclusion *)</p></td></tr></table><code>}</code><code></code></div><div class="doc"><p>A proof can be expanded into a proof node, which show the first step of the proof.</p></div></div><div class="spec type" id="type-step"><a href="#type-step" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>step</code><code></code><code><span class="keyword"> = </span></code><table class="variant"><tr id="type-step.Hypothesis" class="anchored"><td class="def constructor"><a href="#type-step.Hypothesis" class="anchor"></a><code><span class="keyword">| </span></code><code><span class="constructor">Hypothesis</span></code></td><td class="doc"><p>(** The conclusion is a user-provided hypothesis *)</p></td></tr><tr id="type-step.Assumption" class="anchored"><td class="def constructor"><a href="#type-step.Assumption" class="anchor"></a><code><span class="keyword">| </span></code><code><span class="constructor">Assumption</span></code></td><td class="doc"><p>(** The conclusion has been locally assumed by the user *)</p></td></tr><tr id="type-step.Lemma" class="anchored"><td class="def constructor"><a href="#type-step.Lemma" class="anchor"></a><code><span class="keyword">| </span></code><code><span class="constructor">Lemma</span><span class="keyword"> of </span><a href="index.html#type-lemma">lemma</a></code></td><td class="doc"><p>(** The conclusion is a tautology provided by the theory, with associated proof *)</p></td></tr><tr id="type-step.Duplicate" class="anchored"><td class="def constructor"><a href="#type-step.Duplicate" class="anchor"></a><code><span class="keyword">| </span></code><code><span class="constructor">Duplicate</span><span class="keyword"> of </span><a href="index.html#type-proof">proof</a><span class="keyword"> * </span><a href="index.html#type-atom">atom</a> list</code></td><td class="doc"><p>(** The conclusion is obtained by eliminating multiple occurences of the atom in
|
|
the conclusion of the provided proof. *)</p></td></tr><tr id="type-step.Resolution" class="anchored"><td class="def constructor"><a href="#type-step.Resolution" class="anchor"></a><code><span class="keyword">| </span></code><code><span class="constructor">Resolution</span><span class="keyword"> of </span><a href="index.html#type-proof">proof</a><span class="keyword"> * </span><a href="index.html#type-proof">proof</a><span class="keyword"> * </span><a href="index.html#type-atom">atom</a></code></td><td class="doc"><p>(** 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. *)</p></td></tr></table><code></code></div><div class="doc"><p>The type of reasoning steps allowed in a proof.</p></div></div><h4>Proof building functions</h4><div class="spec val" id="val-prove"><a href="#val-prove" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove : <a href="index.html#type-clause">clause</a> <span class="keyword">‑></span> <a href="index.html#type-proof">proof</a></code></div><div class="doc"><p>Given a clause, return a proof of that clause.</p><ul class="at-tag"><li><span class="at-tag raise">Raises</span> <span class="module-path">Insuficient_hyps</span>: if it does not succeed.</li></ul></div></div><div class="spec val" id="val-prove_unsat"><a href="#val-prove_unsat" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_unsat : <a href="index.html#type-clause">clause</a> <span class="keyword">‑></span> <a href="index.html#type-proof">proof</a></code></div><div class="doc"><p>Given a conflict clause <code class="code">c</code>, returns a proof of the empty clause.</p><ul class="at-tag"><li><span class="at-tag raise">Raises</span> <span class="module-path">Insuficient_hyps</span>: if it does not succeed.</li></ul></div></div><div class="spec val" id="val-prove_atom"><a href="#val-prove_atom" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_atom : <a href="index.html#type-atom">atom</a> <span class="keyword">‑></span> <a href="index.html#type-proof">proof</a> option</code></div><div class="doc"><p>Given an atom <code class="code">a</code>, returns a proof of the clause <code class="code">[a]</code> if <code class="code">a</code> is true at level 0</p></div></div><h4>Proof Nodes</h4><div class="spec val" id="val-is_leaf"><a href="#val-is_leaf" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>is_leaf : <a href="index.html#type-step">step</a> <span class="keyword">‑></span> bool</code></div><div class="doc"><p>Returns wether the the proof node is a leaf, i.e. an hypothesis,
|
|
an assumption, or a lemma.
|
|
<code class="code">true</code> if and only if returns the empty list.</p></div></div><div class="spec val" id="val-expl"><a href="#val-expl" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>expl : <a href="index.html#type-step">step</a> <span class="keyword">‑></span> string</code></div><div class="doc"><p>Returns a short string description for the proof step; for instance
|
|
<code class="code">"hypothesis"</code> for a <code class="code">Hypothesis</code>
|
|
(it currently returns the variant name in lowercase).</p></div></div><div class="spec val" id="val-parents"><a href="#val-parents" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>parents : <a href="index.html#type-step">step</a> <span class="keyword">‑></span> <a href="index.html#type-proof">proof</a> list</code></div><div class="doc"><p>Returns the parents of a proof node.</p></div></div><h4>Proof Manipulation</h4><div class="spec val" id="val-expand"><a href="#val-expand" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>expand : <a href="index.html#type-proof">proof</a> <span class="keyword">‑></span> <a href="index.html#type-proof_node">proof_node</a></code></div><div class="doc"><p>Return the proof step at the root of a given proof.</p></div></div><div class="spec val" id="val-conclusion"><a href="#val-conclusion" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>conclusion : <a href="index.html#type-proof">proof</a> <span class="keyword">‑></span> <a href="index.html#type-clause">clause</a></code></div><div class="doc"><p>What is proved at the root of the clause</p></div></div><div class="spec val" id="val-fold"><a href="#val-fold" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>fold : (<span class="type-var">'a</span> <span class="keyword">‑></span> <a href="index.html#type-proof_node">proof_node</a> <span class="keyword">‑></span> <span class="type-var">'a</span>) <span class="keyword">‑></span> <span class="type-var">'a</span> <span class="keyword">‑></span> <a href="index.html#type-proof">proof</a> <span class="keyword">‑></span> <span class="type-var">'a</span></code></div><div class="doc"><p><code class="code">fold f acc p</code>, fold <code class="code">f</code> over the proof <code class="code">p</code> and all its node. It is guaranteed that
|
|
<code class="code">f</code> is executed exactly once on each proof node in the tree, and that the execution of
|
|
<code class="code">f</code> on a proof node happens after the execution on the parents of the nodes.</p></div></div><div class="spec val" id="val-unsat_core"><a href="#val-unsat_core" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>unsat_core : <a href="index.html#type-proof">proof</a> <span class="keyword">‑></span> <a href="index.html#type-clause">clause</a> list</code></div><div class="doc"><p>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 <code class="code">fold</code> function since it has
|
|
access to the internal representation of proofs</p></div></div><h4>Misc</h4><div class="spec val" id="val-check"><a href="#val-check" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>check : <a href="index.html#type-proof">proof</a> <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Check the contents of a proof. Mainly for internal use</p></div></div><div class="spec module" id="module-Clause"><a href="#module-Clause" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Clause/index.html">Clause</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Atom"><a href="#module-Atom" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Atom/index.html">Atom</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Tbl"><a href="#module-Tbl" class="anchor"></a><div class="def module"><code><span class="keyword">module </span>Tbl : Hashtbl.S<span class="keyword"> with </span><span class="keyword">type </span><a href="index.html#module-Tbl">Tbl</a>.key<span class="keyword"> = </span><a href="index.html#type-proof">proof</a></code></div><div class="doc"></div></div></body></html> |