mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-28 12:24:50 -05:00
2 lines
No EOL
11 KiB
HTML
2 lines
No EOL
11 KiB
HTML
<!DOCTYPE html>
|
||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-S (sidekick.Sidekick_backend.Dot.Default.1-S)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><header><nav><a href="../index.html">Up</a> – package <a href="../../../../index.html">sidekick</a></nav><h1>Parameter <code>Sidekick_backend.Dot.Default.1-S</code></h1></header><aside><p>Signature for a module handling proof by resolution from sat solving traces</p></aside><section><header><h3 id="type-declarations"><a href="#type-declarations" class="anchor"></a>Type declarations</h3></header><dl><dt id="exception-Insufficient_hyps"><a href="#exception-Insufficient_hyps" class="anchor"></a><code><span class="keyword">exception </span></code><code><span class="exception">Insufficient_hyps</span></code></dt><dd><p>Raised when a complete resolution derivation cannot be found using the current hypotheses.</p></dd></dl><dl><dt id="type-formula"><a href="#type-formula" class="anchor"></a><code><span class="keyword">type </span>formula</code><code></code><code></code></dt><dt id="type-atom"><a href="#type-atom" class="anchor"></a><code><span class="keyword">type </span>atom</code><code></code><code></code></dt><dt id="type-lemma"><a href="#type-lemma" class="anchor"></a><code><span class="keyword">type </span>lemma</code><code></code><code></code></dt><dt id="type-clause"><a href="#type-clause" class="anchor"></a><code><span class="keyword">type </span>clause</code><code></code><code></code></dt><dd><p>Abstract types for atoms, clauses and theory-specific lemmas</p></dd></dl><dl><dt id="type-proof"><a href="#type-proof" class="anchor"></a><code><span class="keyword">type </span>proof</code><code></code><code></code></dt><dd><p>Lazy type for proof trees. Proofs are persistent objects, and can be extended to proof nodes using functions defined later.</p></dd></dl><dl><dt id="type-proof_node"><a href="#type-proof_node" class="anchor"></a><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></dt><dd><p>A proof can be expanded into a proof node, which show the first step of the proof.</p></dd></dl><dl><dt id="type-step"><a href="#type-step" class="anchor"></a><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></dt><dd><p>The type of reasoning steps allowed in a proof.</p></dd></dl></section><section><header><h3 id="proof-building-functions"><a href="#proof-building-functions" class="anchor"></a>Proof building functions</h3></header><dl><dt id="val-prove"><a href="#val-prove" class="anchor"></a><code><span class="keyword">val </span>prove : <a href="index.html#type-clause">clause</a> <span>‑></span> <a href="index.html#type-proof">proof</a></code></dt><dd><p>Given a clause, return a proof of that clause.</p><dl><dt>raises Insuficient_hyps</dt><dd><p>if it does not succeed.</p></dd></dl></dd></dl><dl><dt id="val-prove_unsat"><a href="#val-prove_unsat" class="anchor"></a><code><span class="keyword">val </span>prove_unsat : <a href="index.html#type-clause">clause</a> <span>‑></span> <a href="index.html#type-proof">proof</a></code></dt><dd><p>Given a conflict clause <code>c</code>, returns a proof of the empty clause.</p><dl><dt>raises Insuficient_hyps</dt><dd><p>if it does not succeed.</p></dd></dl></dd></dl><dl><dt id="val-prove_atom"><a href="#val-prove_atom" class="anchor"></a><code><span class="keyword">val </span>prove_atom : <a href="index.html#type-atom">atom</a> <span>‑></span> <a href="index.html#type-proof">proof</a> option</code></dt><dd><p>Given an atom <code>a</code>, returns a proof of the clause <code>[a]</code> if <code>a</code> is true at level 0</p></dd></dl></section><section><header><h3 id="proof-nodes"><a href="#proof-nodes" class="anchor"></a>Proof Nodes</h3></header><dl><dt id="val-is_leaf"><a href="#val-is_leaf" class="anchor"></a><code><span class="keyword">val </span>is_leaf : <a href="index.html#type-step">step</a> <span>‑></span> bool</code></dt><dt id="val-expl"><a href="#val-expl" class="anchor"></a><code><span class="keyword">val </span>expl : <a href="index.html#type-step">step</a> <span>‑></span> string</code></dt><dd><p>Returns a short string description for the proof step; for instance <code>"hypothesis"</code> for a <code>Hypothesis</code> (it currently returns the variant name in lowercase).</p></dd></dl><dl><dt id="val-parents"><a href="#val-parents" class="anchor"></a><code><span class="keyword">val </span>parents : <a href="index.html#type-step">step</a> <span>‑></span> <a href="index.html#type-proof">proof</a> list</code></dt><dd><p>Returns the parents of a proof node.</p></dd></dl></section><section><header><h3 id="proof-manipulation"><a href="#proof-manipulation" class="anchor"></a>Proof Manipulation</h3></header><dl><dt id="val-expand"><a href="#val-expand" class="anchor"></a><code><span class="keyword">val </span>expand : <a href="index.html#type-proof">proof</a> <span>‑></span> <a href="index.html#type-proof_node">proof_node</a></code></dt><dd><p>Return the proof step at the root of a given proof.</p></dd></dl><dl><dt id="val-conclusion"><a href="#val-conclusion" class="anchor"></a><code><span class="keyword">val </span>conclusion : <a href="index.html#type-proof">proof</a> <span>‑></span> <a href="index.html#type-clause">clause</a></code></dt><dd><p>What is proved at the root of the clause</p></dd></dl><dl><dt id="val-fold"><a href="#val-fold" class="anchor"></a><code><span class="keyword">val </span>fold : (<span class="type-var">'a</span> <span>‑></span> <a href="index.html#type-proof_node">proof_node</a> <span>‑></span> <span class="type-var">'a</span>) <span>‑></span> <span class="type-var">'a</span> <span>‑></span> <a href="index.html#type-proof">proof</a> <span>‑></span> <span class="type-var">'a</span></code></dt><dd><p><code>fold f acc p</code>, fold <code>f</code> over the proof <code>p</code> and all its node. It is guaranteed that <code>f</code> is executed exactly once on each proof node in the tree, and that the execution of <code>f</code> on a proof node happens after the execution on the parents of the nodes.</p></dd></dl><dl><dt id="val-unsat_core"><a href="#val-unsat_core" class="anchor"></a><code><span class="keyword">val </span>unsat_core : <a href="index.html#type-proof">proof</a> <span>‑></span> <a href="index.html#type-clause">clause</a> list</code></dt><dd><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>fold</code> function since it has access to the internal representation of proofs</p></dd></dl></section><section><header><h3 id="misc"><a href="#misc" class="anchor"></a>Misc</h3></header><dl><dt id="val-check"><a href="#val-check" class="anchor"></a><code><span class="keyword">val </span>check : <a href="index.html#type-proof">proof</a> <span>‑></span> unit</code></dt><dd><p>Check the contents of a proof. Mainly for internal use</p></dd></dl><article id="module-Clause"><a href="#module-Clause" class="anchor"></a><code><span class="keyword">module </span><a href="Clause/index.html">Clause</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></article><article id="module-Atom"><a href="#module-Atom" class="anchor"></a><code><span class="keyword">module </span><a href="Atom/index.html">Atom</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></article><article id="module-Tbl"><a href="#module-Tbl" class="anchor"></a><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></article></section></body></html> |