update dev docs

This commit is contained in:
Simon Cruanes 2019-06-07 18:05:28 -05:00
parent 5b989c33ba
commit 6176085965
599 changed files with 5 additions and 2654 deletions

View file

@ -1,18 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>index</title>
<link rel="stylesheet" href="./odoc.css"/>
<meta charset="utf-8"/>
<meta name="viewport" content="width=device-width,initial-scale=1.0"/>
</head>
<body>
<div class="by-name">
<h2>OCaml package documentation</h2>
<ol>
<li><a href="msat_test/index.html">msat_test</a> <span class="version">dev</span></li>
<li><a href="sidekick/index.html">sidekick</a> <span class="version">dev</span></li>
</ol>
</div>
</body>
</html>

5
index.md Normal file
View file

@ -0,0 +1,5 @@
# Sidekick
## Documentation
- [dev](dev)

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>index (msat_test.index)</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> &mdash; <span class="package">package <a href="index.html">msat_test</a></span></nav><header></header></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Form (sidekick.CDCL_tseitin.Make.1-A.Form)</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>Module <code>CDCL_tseitin.Make.1-A.Form</code></h1></header><dl><dt id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type </span>t</code><code></code><code></code></dt><dd><p>Type of atomic formulas.</p></dd></dl><dl><dt id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Negation of atomic formulas.</p></dd></dl><dl><dt id="val-print"><a href="#val-print" class="anchor"></a><code><span class="keyword">val </span>print : Format.formatter <span>&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> unit</code></dt><dd><p>Print the given formula.</p></dd></dl></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-A (sidekick.CDCL_tseitin.Make.1-A)</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>CDCL_tseitin.Make.1-A</code></h1></header><aside><p>Formulas</p><p>This defines what is needed of formulas in order to implement Tseitin's CNF conversion.</p></aside><article id="module-Form"><a href="#module-Form" class="anchor"></a><code><span class="keyword">module </span><a href="Form/index.html">Form</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></article><dl><dt id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type </span>t</code><code></code><code></code></dt><dd><p>State</p></dd></dl><dl><dt id="val-fresh"><a href="#val-fresh" class="anchor"></a><code><span class="keyword">val </span>fresh : <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> <a href="Form/index.html#type-t">Form.t</a></code></dt><dd><p>Generate fresh formulas (that are different from any other).</p></dd></dl></body></html>

File diff suppressed because one or more lines are too long

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>CDCL_tseitin (sidekick.CDCL_tseitin)</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>Module <code>CDCL_tseitin</code></h1><p>Tseitin CNF conversion</p><p>This modules implements Tseitin's Conjunctive Normal Form conversion, i.e. the ability to transform an arbitrary boolean formula into an equi-satisfiable CNF, that can then be fed to a SAT/SMT/McSat solver.</p></header><article id="module-type-Arg"><a href="#module-type-Arg" class="anchor"></a><code><span class="keyword">module type </span><a href="module-type-Arg/index.html">Arg</a> = <a href="../CDCL_tseitin__/Tseitin_intf/index.html#module-type-Arg">CDCL_tseitin__.Tseitin_intf.Arg</a></code></article><article id="module-type-S"><a href="#module-type-S" class="anchor"></a><code><span class="keyword">module type </span><a href="module-type-S/index.html">S</a> = <a href="../CDCL_tseitin__/Tseitin_intf/index.html#module-type-S">CDCL_tseitin__.Tseitin_intf.S</a></code></article><article id="module-Make"><a href="#module-Make" class="anchor"></a><code><span class="keyword">module </span><a href="Make/index.html">Make</a> : <span class="keyword">functor</span> (<a href="Make/argument-1-A/index.html">A</a> : <a href="index.html#module-type-Arg">Arg</a>) -&gt; <a href="index.html#module-type-S">S</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-atom">atom</a><span class="keyword"> = </span><a href="Make/argument-1-A/Form/index.html#type-t">A.Form.t</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-fresh_state">fresh_state</a><span class="keyword"> = </span><a href="Make/argument-1-A/index.html#type-t">A.t</a></code></article></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Form (sidekick.CDCL_tseitin.Arg.Form)</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>Module <code>CDCL_tseitin.Arg.Form</code></h1></header><dl><dt id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type </span>t</code><code></code><code></code></dt><dd><p>Type of atomic formulas.</p></dd></dl><dl><dt id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Negation of atomic formulas.</p></dd></dl><dl><dt id="val-print"><a href="#val-print" class="anchor"></a><code><span class="keyword">val </span>print : Format.formatter <span>&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> unit</code></dt><dd><p>Print the given formula.</p></dd></dl></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Arg (sidekick.CDCL_tseitin.Arg)</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>Module type <code>CDCL_tseitin.Arg</code></h1></header><div class="doc"><p>The implementation of formulas required to implement Tseitin's CNF conversion.</p></div><aside><p>Formulas</p><p>This defines what is needed of formulas in order to implement Tseitin's CNF conversion.</p></aside><article id="module-Form"><a href="#module-Form" class="anchor"></a><code><span class="keyword">module </span><a href="Form/index.html">Form</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></article><dl><dt id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type </span>t</code><code></code><code></code></dt><dd><p>State</p></dd></dl><dl><dt id="val-fresh"><a href="#val-fresh" class="anchor"></a><code><span class="keyword">val </span>fresh : <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> <a href="Form/index.html#type-t">Form.t</a></code></dt><dd><p>Generate fresh formulas (that are different from any other).</p></dd></dl></body></html>

File diff suppressed because one or more lines are too long

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Tseitin_intf (sidekick.CDCL_tseitin__.Tseitin_intf)</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>Module <code>CDCL_tseitin__.Tseitin_intf</code></h1></header><aside><p>Interfaces for Tseitin's CNF conversion</p></aside><article id="module-type-Arg"><a href="#module-type-Arg" class="anchor"></a><code><span class="keyword">module type </span><a href="module-type-Arg/index.html">Arg</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></article><article id="module-type-S"><a href="#module-type-S" class="anchor"></a><code><span class="keyword">module type </span><a href="module-type-S/index.html">S</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></article></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Form (sidekick.CDCL_tseitin__.Tseitin_intf.Arg.Form)</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>Module <code>CDCL_tseitin__.Tseitin_intf.Arg.Form</code></h1></header><dl><dt id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type </span>t</code><code></code><code></code></dt><dd><p>Type of atomic formulas.</p></dd></dl><dl><dt id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Negation of atomic formulas.</p></dd></dl><dl><dt id="val-print"><a href="#val-print" class="anchor"></a><code><span class="keyword">val </span>print : Format.formatter <span>&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> unit</code></dt><dd><p>Print the given formula.</p></dd></dl></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Arg (sidekick.CDCL_tseitin__.Tseitin_intf.Arg)</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>Module type <code>CDCL_tseitin__.Tseitin_intf.Arg</code></h1></header><aside><p>Formulas</p><p>This defines what is needed of formulas in order to implement Tseitin's CNF conversion.</p></aside><article id="module-Form"><a href="#module-Form" class="anchor"></a><code><span class="keyword">module </span><a href="Form/index.html">Form</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></article><dl><dt id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type </span>t</code><code></code><code></code></dt><dd><p>State</p></dd></dl><dl><dt id="val-fresh"><a href="#val-fresh" class="anchor"></a><code><span class="keyword">val </span>fresh : <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> <a href="Form/index.html#type-t">Form.t</a></code></dt><dd><p>Generate fresh formulas (that are different from any other).</p></dd></dl></body></html>

File diff suppressed because one or more lines are too long

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>CDCL_tseitin__ (sidekick.CDCL_tseitin__)</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>Module <code>CDCL_tseitin__</code></h1></header><article id="module-CDCL_tseitin"><a href="#module-CDCL_tseitin" class="anchor"></a><code><span class="keyword">module </span>CDCL_tseitin = <a href="../CDCL_tseitin/index.html">CDCL_tseitin</a></code></article><article id="module-Tseitin_intf"><a href="#module-Tseitin_intf" class="anchor"></a><code><span class="keyword">module </span><a href="Tseitin_intf/index.html">Tseitin_intf</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></article></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>CDCL_tseitin__Tseitin_intf (sidekick.CDCL_tseitin__Tseitin_intf)</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>Module <code>CDCL_tseitin__Tseitin_intf</code></h1><p>Interfaces for Tseitin's CNF conversion</p></header><article id="module-type-Arg"><a href="#module-type-Arg" class="anchor"></a><code><span class="keyword">module type </span><a href="module-type-Arg/index.html">Arg</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></article><article id="module-type-S"><a href="#module-type-S" class="anchor"></a><code><span class="keyword">module type </span><a href="module-type-S/index.html">S</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></article></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Form (sidekick.CDCL_tseitin__Tseitin_intf.Arg.Form)</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>Module <code>CDCL_tseitin__Tseitin_intf.Arg.Form</code></h1></header><dl><dt id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type </span>t</code><code></code><code></code></dt><dd><p>Type of atomic formulas.</p></dd></dl><dl><dt id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Negation of atomic formulas.</p></dd></dl><dl><dt id="val-print"><a href="#val-print" class="anchor"></a><code><span class="keyword">val </span>print : Format.formatter <span>&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> unit</code></dt><dd><p>Print the given formula.</p></dd></dl></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Arg (sidekick.CDCL_tseitin__Tseitin_intf.Arg)</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>Module type <code>CDCL_tseitin__Tseitin_intf.Arg</code></h1></header><aside><p>Formulas</p><p>This defines what is needed of formulas in order to implement Tseitin's CNF conversion.</p></aside><article id="module-Form"><a href="#module-Form" class="anchor"></a><code><span class="keyword">module </span><a href="Form/index.html">Form</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></article><dl><dt id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type </span>t</code><code></code><code></code></dt><dd><p>State</p></dd></dl><dl><dt id="val-fresh"><a href="#val-fresh" class="anchor"></a><code><span class="keyword">val </span>fresh : <a href="index.html#type-t">t</a> <span>&#8209;&gt;</span> <a href="Form/index.html#type-t">Form.t</a></code></dt><dd><p>Generate fresh formulas (that are different from any other).</p></dd></dl></body></html>

File diff suppressed because one or more lines are too long

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Backend_intf (sidekick.Sidekick_backend.Backend_intf)</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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Backend_intf</span></h1></header><p>Backend interface</p><p>This modules defines the interface of the modules providing
export of proofs.</p><div class="spec module-type" id="module-type-S"><a href="#module-type-S" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-S/index.html">S</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>S (sidekick.Sidekick_backend.Backend_intf.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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend.Backend_intf.S</span></h1></header><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick.Sidekick_backend.Coq.Make.1-S.Atom)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Coq.Make.1-S.Atom</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-atom">atom</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-is_pos"><a href="#val-is_pos" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>is_pos : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-neg"><a href="#val-neg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-abs"><a href="#val-abs" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>abs : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-compare"><a href="#val-compare" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>compare : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-equal"><a href="#val-equal" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>equal : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-lit"><a href="#val-lit" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lit : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-formula">formula</a></code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Clause (sidekick.Sidekick_backend.Coq.Make.1-S.Clause)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Coq.Make.1-S.Clause</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-clause">clause</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-name"><a href="#val-name" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>name : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> string</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms"><a href="#val-atoms" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> array</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms_l"><a href="#val-atoms_l" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms_l : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> list</code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"><p>A nice looking printer for clauses, which sort the atoms before printing.</p></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-t">t</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,14 +0,0 @@
<!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> &mdash; <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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> string</code></div><div class="doc"><p>Returns a short string description for the proof step; for instance
<code class="code">&quot;hypothesis&quot;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> <a href="index.html#type-proof_node">proof_node</a> <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span>) <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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>

View file

@ -1,8 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>2-A (sidekick.Sidekick_backend.Coq.Make.2-A)</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> &mdash; <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.2-A</span></h1></header><p>Term printing for Coq</p><div class="spec type" id="type-hyp"><a href="#type-hyp" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>hyp</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-assumption"><a href="#type-assumption" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>assumption</code><code></code><code></code></div><div class="doc"><p>The types of hypotheses, lemmas, and assumptions</p></div></div><div class="spec val" id="val-prove_hyp"><a href="#val-prove_hyp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_hyp : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-hyp">hyp</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_lemma"><a href="#val-prove_lemma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_lemma : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_assumption"><a href="#val-prove_assumption" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_assumption : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-assumption">assumption</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Proving function for hypotheses, lemmas and assumptions.
<code class="code">prove_x fmt name x</code> should prove <code class="code">x</code>, and be such that after
executing it, <code class="code">x</code> is among the coq hypotheses under the name <code class="code">name</code>.
The hypothesis should be the encoding of the given clause, i.e
for a clause <code class="code">a \/ not b \/ c</code>, the proved hypothesis should be:
<code class="code"> ~ a -&gt; ~ ~ b -&gt; ~ c -&gt; False </code>, keeping the same order as the
one in the atoms array of the clause.</p></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (sidekick.Sidekick_backend.Coq.Make)</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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Coq.Make</span></h1></header><div class="doc"><p>Base functor to output Coq proofs</p></div><h3 class="heading">Parameters</h3><div><div class="spec argument" id="argument-2-A"><a href="#argument-2-A" class="anchor"></a><div class="def argument"><code><a href="argument-2-A/index.html">A</a> : <a href="../index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-hyp">hyp</a> := <a href="argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-lemma">lemma</a> := <a href="argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-assumption">assumption</a> := <a href="argument-1-S/index.html#type-clause">S.clause</a></code></div><div class="doc"></div></div><div class="spec argument" id="argument-1-S"><a href="#argument-1-S" class="anchor"></a><div class="def argument"><code><a href="argument-1-S/index.html">S</a> : <a href="../../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a></code></div><div class="doc"></div></div></div><h3 class="heading">Signature</h3><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick.Sidekick_backend.Coq.Simple.1-S.Atom)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Coq.Simple.1-S.Atom</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-atom">atom</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-is_pos"><a href="#val-is_pos" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>is_pos : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-neg"><a href="#val-neg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-abs"><a href="#val-abs" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>abs : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-compare"><a href="#val-compare" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>compare : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-equal"><a href="#val-equal" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>equal : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-lit"><a href="#val-lit" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lit : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-formula">formula</a></code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Clause (sidekick.Sidekick_backend.Coq.Simple.1-S.Clause)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Coq.Simple.1-S.Clause</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-clause">clause</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-name"><a href="#val-name" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>name : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> string</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms"><a href="#val-atoms" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> array</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms_l"><a href="#val-atoms_l" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms_l : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> list</code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"><p>A nice looking printer for clauses, which sort the atoms before printing.</p></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-t">t</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,14 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-S (sidekick.Sidekick_backend.Coq.Simple.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> &mdash; <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.Simple.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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> string</code></div><div class="doc"><p>Returns a short string description for the proof step; for instance
<code class="code">&quot;hypothesis&quot;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> <a href="index.html#type-proof_node">proof_node</a> <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span>) <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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>

View file

@ -1,8 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>2-A (sidekick.Sidekick_backend.Coq.Simple.2-A)</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> &mdash; <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.Simple.2-A</span></h1></header><p>Term printing for Coq</p><div class="spec type" id="type-hyp"><a href="#type-hyp" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>hyp</code><code><span class="keyword"> = </span><a href="../argument-1-S/index.html#type-formula">S.formula</a> list</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-assumption"><a href="#type-assumption" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>assumption</code><code></code><code></code></div><div class="doc"><p>The types of hypotheses, lemmas, and assumptions</p></div></div><div class="spec val" id="val-prove_hyp"><a href="#val-prove_hyp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_hyp : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-hyp">hyp</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_lemma"><a href="#val-prove_lemma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_lemma : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_assumption"><a href="#val-prove_assumption" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_assumption : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-assumption">assumption</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Proving function for hypotheses, lemmas and assumptions.
<code class="code">prove_x fmt name x</code> should prove <code class="code">x</code>, and be such that after
executing it, <code class="code">x</code> is among the coq hypotheses under the name <code class="code">name</code>.
The hypothesis should be the encoding of the given clause, i.e
for a clause <code class="code">a \/ not b \/ c</code>, the proved hypothesis should be:
<code class="code"> ~ a -&gt; ~ ~ b -&gt; ~ c -&gt; False </code>, keeping the same order as the
one in the atoms array of the clause.</p></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Simple (sidekick.Sidekick_backend.Coq.Simple)</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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Coq.Simple</span></h1></header><div class="doc"><p>Simple functo to output Coq proofs</p></div><h3 class="heading">Parameters</h3><div><div class="spec argument" id="argument-2-A"><a href="#argument-2-A" class="anchor"></a><div class="def argument"><code><a href="argument-2-A/index.html">A</a> : <a href="../index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-hyp">hyp</a><span class="keyword"> = </span><a href="argument-1-S/index.html#type-formula">S.formula</a> list<span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-lemma">lemma</a> := <a href="argument-1-S/index.html#type-lemma">S.lemma</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-assumption">assumption</a> := <a href="argument-1-S/index.html#type-formula">S.formula</a></code></div><div class="doc"></div></div><div class="spec argument" id="argument-1-S"><a href="#argument-1-S" class="anchor"></a><div class="def argument"><code><a href="argument-1-S/index.html">S</a> : <a href="../../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a></code></div><div class="doc"></div></div></div><h3 class="heading">Signature</h3><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,4 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Coq (sidekick.Sidekick_backend.Coq)</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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Coq</span></h1></header><p>Coq Backend</p><p>This module provides an easy way to produce coq scripts
corresponding to the resolution proofs output by the
sat solver.</p><div class="spec module-type" id="module-type-S"><a href="#module-type-S" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-S/index.html">S</a> = <a href="../Backend_intf/index.html#module-type-S">Backend_intf.S</a></code></div><div class="doc"><p>Interface for exporting proofs.</p></div></div><div class="spec module-type" id="module-type-Arg"><a href="#module-type-Arg" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-Arg/index.html">Arg</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Make"><a href="#module-Make" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Make/index.html">Make</a> : <span class="keyword">functor</span> (<a href="Make/argument-1-S/index.html">S</a> : <a href="../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a>) -&gt; <span class="keyword">functor</span> (<a href="Make/argument-2-A/index.html">A</a> : <a href="index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-hyp">hyp</a> := <a href="Make/argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-lemma">lemma</a> := <a href="Make/argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-assumption">assumption</a> := <a href="Make/argument-1-S/index.html#type-clause">S.clause</a>) -&gt; <a href="index.html#module-type-S">S</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-t">t</a> := <a href="Make/argument-1-S/index.html#type-proof">S.proof</a></code></div><div class="doc"><p>Base functor to output Coq proofs</p></div></div><div class="spec module" id="module-Simple"><a href="#module-Simple" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Simple/index.html">Simple</a> : <span class="keyword">functor</span> (<a href="Simple/argument-1-S/index.html">S</a> : <a href="../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a>) -&gt; <span class="keyword">functor</span> (<a href="Simple/argument-2-A/index.html">A</a> : <a href="index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Simple/index.html#type-hyp">hyp</a><span class="keyword"> = </span><a href="Simple/argument-1-S/index.html#type-formula">S.formula</a> list<span class="keyword"> and </span><span class="keyword">type </span><a href="Simple/index.html#type-lemma">lemma</a> := <a href="Simple/argument-1-S/index.html#type-lemma">S.lemma</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Simple/index.html#type-assumption">assumption</a> := <a href="Simple/argument-1-S/index.html#type-formula">S.formula</a>) -&gt; <a href="index.html#module-type-S">S</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Simple/index.html#type-t">t</a> := <a href="Simple/argument-1-S/index.html#type-proof">S.proof</a></code></div><div class="doc"><p>Simple functo to output Coq proofs</p></div></div></body></html>

View file

@ -1,8 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Arg (sidekick.Sidekick_backend.Coq.Arg)</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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend.Coq.Arg</span></h1></header><p>Term printing for Coq</p><div class="spec type" id="type-hyp"><a href="#type-hyp" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>hyp</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-assumption"><a href="#type-assumption" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>assumption</code><code></code><code></code></div><div class="doc"><p>The types of hypotheses, lemmas, and assumptions</p></div></div><div class="spec val" id="val-prove_hyp"><a href="#val-prove_hyp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_hyp : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-hyp">hyp</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_lemma"><a href="#val-prove_lemma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_lemma : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_assumption"><a href="#val-prove_assumption" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_assumption : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-assumption">assumption</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Proving function for hypotheses, lemmas and assumptions.
<code class="code">prove_x fmt name x</code> should prove <code class="code">x</code>, and be such that after
executing it, <code class="code">x</code> is among the coq hypotheses under the name <code class="code">name</code>.
The hypothesis should be the encoding of the given clause, i.e
for a clause <code class="code">a \/ not b \/ c</code>, the proved hypothesis should be:
<code class="code"> ~ a -&gt; ~ ~ b -&gt; ~ c -&gt; False </code>, keeping the same order as the
one in the atoms array of the clause.</p></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>S (sidekick.Sidekick_backend.Coq.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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend.Coq.S</span></h1></header><div class="doc"><p>Interface for exporting proofs.</p></div><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick.Sidekick_backend.Dedukti.Make.1-S.Atom)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dedukti.Make.1-S.Atom</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-atom">atom</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-is_pos"><a href="#val-is_pos" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>is_pos : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-neg"><a href="#val-neg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-abs"><a href="#val-abs" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>abs : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-compare"><a href="#val-compare" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>compare : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-equal"><a href="#val-equal" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>equal : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-lit"><a href="#val-lit" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lit : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-formula">formula</a></code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Clause (sidekick.Sidekick_backend.Dedukti.Make.1-S.Clause)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dedukti.Make.1-S.Clause</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-clause">clause</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-name"><a href="#val-name" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>name : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> string</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms"><a href="#val-atoms" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> array</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms_l"><a href="#val-atoms_l" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms_l : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> list</code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"><p>A nice looking printer for clauses, which sort the atoms before printing.</p></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-t">t</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,14 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-S (sidekick.Sidekick_backend.Dedukti.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> &mdash; <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.Dedukti.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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> string</code></div><div class="doc"><p>Returns a short string description for the proof step; for instance
<code class="code">&quot;hypothesis&quot;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> <a href="index.html#type-proof_node">proof_node</a> <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span>) <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>2-A (sidekick.Sidekick_backend.Dedukti.Make.2-A)</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> &mdash; <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.Dedukti.Make.2-A</span></h1></header><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-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"></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 val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-formula">formula</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><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 : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-context"><a href="#val-context" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>context : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (sidekick.Sidekick_backend.Dedukti.Make)</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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dedukti.Make</span></h1></header><div class="doc"><p>Functor to generate a backend to output proofs for the dedukti type checker.</p></div><h3 class="heading">Parameters</h3><div><div class="spec argument" id="argument-2-A"><a href="#argument-2-A" class="anchor"></a><div class="def argument"><code><a href="argument-2-A/index.html">A</a> : <a href="../index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-formula">formula</a> := <a href="argument-1-S/index.html#type-formula">S.formula</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-lemma">lemma</a> := <a href="argument-1-S/index.html#type-lemma">S.lemma</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-proof">proof</a> := <a href="argument-1-S/index.html#type-proof">S.proof</a></code></div><div class="doc"></div></div><div class="spec argument" id="argument-1-S"><a href="#argument-1-S" class="anchor"></a><div class="def argument"><code><a href="argument-1-S/index.html">S</a> : <a href="../../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a></code></div><div class="doc"></div></div></div><h3 class="heading">Signature</h3><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Dedukti (sidekick.Sidekick_backend.Dedukti)</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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dedukti</span></h1></header><p>Deduki backend for proofs</p><p>Work in progress...</p><div class="spec module-type" id="module-type-S"><a href="#module-type-S" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-S/index.html">S</a> = <a href="../Backend_intf/index.html#module-type-S">Backend_intf.S</a></code></div><div class="doc"></div></div><div class="spec module-type" id="module-type-Arg"><a href="#module-type-Arg" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-Arg/index.html">Arg</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Make"><a href="#module-Make" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Make/index.html">Make</a> : <span class="keyword">functor</span> (<a href="Make/argument-1-S/index.html">S</a> : <a href="../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a>) -&gt; <span class="keyword">functor</span> (<a href="Make/argument-2-A/index.html">A</a> : <a href="index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-formula">formula</a> := <a href="Make/argument-1-S/index.html#type-formula">S.formula</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-lemma">lemma</a> := <a href="Make/argument-1-S/index.html#type-lemma">S.lemma</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-proof">proof</a> := <a href="Make/argument-1-S/index.html#type-proof">S.proof</a>) -&gt; <a href="index.html#module-type-S">S</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-t">t</a> := <a href="Make/argument-1-S/index.html#type-proof">S.proof</a></code></div><div class="doc"><p>Functor to generate a backend to output proofs for the dedukti type checker.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Arg (sidekick.Sidekick_backend.Dedukti.Arg)</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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend.Dedukti.Arg</span></h1></header><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-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"></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 val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-formula">formula</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><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 : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-context"><a href="#val-context" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>context : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>S (sidekick.Sidekick_backend.Dedukti.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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend.Dedukti.S</span></h1></header><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Formula (sidekick.Sidekick_backend.Dimacs.Make.1-St.Formula)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dimacs.Make.1-St.Formula</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-formula">formula</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-equal"><a href="#val-equal" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>equal : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-hash"><a href="#val-hash" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>hash : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat/Solver_types_intf/index.html#type-printer">Sidekick_sat.Solver_types_intf.printer</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,4 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Var (sidekick.Sidekick_backend.Dimacs.Make.1-St.Var)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dimacs.Make.1-St.Var</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-var">var</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-dummy"><a href="#val-dummy" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>dummy : <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-pos"><a href="#val-pos" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pos : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a></code></div><div class="doc"></div></div><div class="spec val" id="val-neg"><a href="#val-neg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a></code></div><div class="doc"></div></div><div class="spec val" id="val-level"><a href="#val-level" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>level : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-idx"><a href="#val-idx" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>idx : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-reason"><a href="#val-reason" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>reason : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-reason">reason</a> option</code></div><div class="doc"></div></div><div class="spec val" id="val-weight"><a href="#val-weight" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>weight : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> float</code></div><div class="doc"></div></div><div class="spec val" id="val-set_level"><a href="#val-set_level" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>set_level : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-set_idx"><a href="#val-set_idx" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>set_idx : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-set_weight"><a href="#val-set_weight" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>set_weight : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> float <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-in_heap"><a href="#val-in_heap" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>in_heap : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-make"><a href="#val-make" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>make : <a href="../index.html#type-state">state</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-formula">formula</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a><span class="keyword"> * </span><a href="../../../../../Sidekick_sat/Theory_intf/index.html#type-negated">Sidekick_sat.Theory_intf.negated</a></code></div><div class="doc"><p>Returns the variable linked with the given formula,
and whether the atom associated with the formula
is <code class="code">var.pa</code> or <code class="code">var.na</code></p></div></div><div class="spec val" id="val-seen_both"><a href="#val-seen_both" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>seen_both : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"><p>both atoms have been seen?</p></div></div><div class="spec val" id="val-clear"><a href="#val-clear" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>clear : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Clear the 'seen' field of the variable.</p></div></div></body></html>

File diff suppressed because one or more lines are too long

View file

@ -1,8 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (sidekick.Sidekick_backend.Dimacs.Make)</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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dimacs.Make</span></h1></header><div class="doc"><p>Functor to create a module for exporting probems to the dimacs (&amp; iCNF) formats.</p></div><h3 class="heading">Parameters</h3><div><div class="spec argument" id="argument-1-St"><a href="#argument-1-St" class="anchor"></a><div class="def argument"><code><a href="argument-1-St/index.html">St</a> : <a href="../../../Sidekick_sat/Solver_types_intf/index.html#module-type-S">Sidekick_sat.Solver_types_intf.S</a></code></div><div class="doc"></div></div></div><h3 class="heading">Signature</h3><div class="spec type" id="type-st"><a href="#type-st" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>st</code><code><span class="keyword"> = </span><a href="argument-1-St/index.html#type-t">St.t</a></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>The type of clauses</p></div></div><div class="spec val" id="val-export"><a href="#val-export" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>export : <a href="index.html#type-st">st</a> <span class="keyword">&#8209;&gt;</span> Format.formatter <span class="keyword">&#8209;&gt;</span> hyps:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> history:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> local:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Export the given clause vectors to the dimacs format.
The arguments should be transmitted directly from the corresponding
function of the module.</p></div></div><div class="spec val" id="val-export_icnf"><a href="#val-export_icnf" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>export_icnf : Format.formatter <span class="keyword">&#8209;&gt;</span> hyps:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> history:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> local:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Export the given clause vectors to the dimacs format.
The arguments should be transmitted directly from the corresponding
function of the module.
This function may be called multiple times in order to add
new clauses (and new local hyps) to the problem.</p></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Dimacs (sidekick.Sidekick_backend.Dimacs)</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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dimacs</span></h1></header><p>Dimacs backend for problems</p><p>This module provides functiosn to export problems to the dimacs and
iCNF formats.</p><div class="spec module-type" id="module-type-S"><a href="#module-type-S" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-S/index.html">S</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Make"><a href="#module-Make" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Make/index.html">Make</a> : <span class="keyword">functor</span> (<a href="Make/argument-1-St/index.html">St</a> : <a href="../../Sidekick_sat/Solver_types_intf/index.html#module-type-S">Sidekick_sat.Solver_types_intf.S</a>) -&gt; <a href="index.html#module-type-S">S</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-clause">clause</a> := <a href="Make/argument-1-St/index.html#type-clause">St.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-st">st</a><span class="keyword"> = </span><a href="Make/argument-1-St/index.html#type-t">St.t</a></code></div><div class="doc"><p>Functor to create a module for exporting probems to the dimacs (&amp; iCNF) formats.</p></div></div></body></html>

View file

@ -1,8 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>S (sidekick.Sidekick_backend.Dimacs.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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend.Dimacs.S</span></h1></header><div class="spec type" id="type-st"><a href="#type-st" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>st</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>The type of clauses</p></div></div><div class="spec val" id="val-export"><a href="#val-export" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>export : <a href="index.html#type-st">st</a> <span class="keyword">&#8209;&gt;</span> Format.formatter <span class="keyword">&#8209;&gt;</span> hyps:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> history:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> local:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Export the given clause vectors to the dimacs format.
The arguments should be transmitted directly from the corresponding
function of the module.</p></div></div><div class="spec val" id="val-export_icnf"><a href="#val-export_icnf" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>export_icnf : Format.formatter <span class="keyword">&#8209;&gt;</span> hyps:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> history:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> local:<a href="index.html#type-clause">clause</a> <a href="../../../Sidekick_util/Vec/index.html#type-t">Sidekick_sat.Vec.t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Export the given clause vectors to the dimacs format.
The arguments should be transmitted directly from the corresponding
function of the module.
This function may be called multiple times in order to add
new clauses (and new local hyps) to the problem.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick.Sidekick_backend.Dot.Default.1-S.Atom)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dot.Default.1-S.Atom</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-atom">atom</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-is_pos"><a href="#val-is_pos" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>is_pos : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-neg"><a href="#val-neg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-abs"><a href="#val-abs" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>abs : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-compare"><a href="#val-compare" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>compare : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-equal"><a href="#val-equal" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>equal : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-lit"><a href="#val-lit" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lit : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-formula">formula</a></code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Clause (sidekick.Sidekick_backend.Dot.Default.1-S.Clause)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dot.Default.1-S.Clause</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-clause">clause</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-name"><a href="#val-name" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>name : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> string</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms"><a href="#val-atoms" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> array</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms_l"><a href="#val-atoms_l" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms_l : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> list</code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"><p>A nice looking printer for clauses, which sort the atoms before printing.</p></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-t">t</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,14 +0,0 @@
<!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"/><meta name="generator" content="doc-ock-html v1.0.0-1-g1fc9bf0"/></head><body><nav id="top"><a href="../index.html">Up</a> &mdash; <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.Dot.Default.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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> string</code></div><div class="doc"><p>Returns a short string description for the proof step; for instance
<code class="code">&quot;hypothesis&quot;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> <a href="index.html#type-proof_node">proof_node</a> <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span>) <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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>

View file

@ -1,10 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Default (sidekick.Sidekick_backend.Dot.Default)</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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dot.Default</span></h1></header><div class="doc"><p>Provides a reasonnable default to instantiate the <code class="code">Make</code> functor, assuming
the original printing functions are compatible with DOT html labels.</p></div><h3 class="heading">Parameters</h3><div><div class="spec argument" id="argument-1-S"><a href="#argument-1-S" class="anchor"></a><div class="def argument"><code><a href="argument-1-S/index.html">S</a> : <a href="../../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a></code></div><div class="doc"></div></div></div><h3 class="heading">Signature</h3><p>Term printing for DOT</p><p>This module defines what functions are required in order to export
a proof to the DOT format.</p><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"><p>The type of atomic formuals</p></div></div><div class="spec type" id="type-hyp"><a href="#type-hyp" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>hyp</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-assumption"><a href="#type-assumption" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>assumption</code><code></code><code></code></div><div class="doc"><p>The type of theory-specifi proofs (also called lemmas).</p></div></div><div class="spec val" id="val-print_atom"><a href="#val-print_atom" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print_atom : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-atom">atom</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Print the contents of the given atomic formulas.
WARNING: this function should take care to escape and/or not output special
reserved characters for the dot format (such as quotes and so on).</p></div></div><div class="spec val" id="val-hyp_info"><a href="#val-hyp_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>hyp_info : <a href="index.html#type-hyp">hyp</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"></div></div><div class="spec val" id="val-lemma_info"><a href="#val-lemma_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lemma_info : <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"></div></div><div class="spec val" id="val-assumption_info"><a href="#val-assumption_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>assumption_info : <a href="index.html#type-assumption">assumption</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"><p>Generate some information about the leafs of the proof tree. Currently this backend
print each lemma/assumption/hypothesis as a single leaf of the proof tree.
These function should return a triplet <code class="code">(rule, color, l)</code>, such that:
</p><ul><li><code class="code">rule</code> is a name for the proof (arbitrary, does not need to be unique, but
should rather be descriptive)</li><li><code class="code">color</code> is a color name (optional) understood by DOT</li><li><code class="code">l</code> is a list of printers that will be called to print some additional information</li></ul></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick.Sidekick_backend.Dot.Make.1-S.Atom)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dot.Make.1-S.Atom</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-atom">atom</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-is_pos"><a href="#val-is_pos" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>is_pos : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-neg"><a href="#val-neg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-abs"><a href="#val-abs" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>abs : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-compare"><a href="#val-compare" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>compare : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-equal"><a href="#val-equal" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>equal : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-lit"><a href="#val-lit" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lit : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-formula">formula</a></code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Clause (sidekick.Sidekick_backend.Dot.Make.1-S.Clause)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dot.Make.1-S.Clause</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-clause">clause</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-name"><a href="#val-name" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>name : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> string</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms"><a href="#val-atoms" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> array</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms_l"><a href="#val-atoms_l" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms_l : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> list</code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"><p>A nice looking printer for clauses, which sort the atoms before printing.</p></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-t">t</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,14 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-S (sidekick.Sidekick_backend.Dot.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> &mdash; <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.Dot.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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> string</code></div><div class="doc"><p>Returns a short string description for the proof step; for instance
<code class="code">&quot;hypothesis&quot;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> <a href="index.html#type-proof_node">proof_node</a> <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span>) <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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>

View file

@ -1,9 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>2-A (sidekick.Sidekick_backend.Dot.Make.2-A)</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> &mdash; <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.Dot.Make.2-A</span></h1></header><p>Term printing for DOT</p><p>This module defines what functions are required in order to export
a proof to the DOT format.</p><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"><p>The type of atomic formuals</p></div></div><div class="spec type" id="type-hyp"><a href="#type-hyp" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>hyp</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-assumption"><a href="#type-assumption" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>assumption</code><code></code><code></code></div><div class="doc"><p>The type of theory-specifi proofs (also called lemmas).</p></div></div><div class="spec val" id="val-print_atom"><a href="#val-print_atom" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print_atom : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-atom">atom</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Print the contents of the given atomic formulas.
WARNING: this function should take care to escape and/or not output special
reserved characters for the dot format (such as quotes and so on).</p></div></div><div class="spec val" id="val-hyp_info"><a href="#val-hyp_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>hyp_info : <a href="index.html#type-hyp">hyp</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"></div></div><div class="spec val" id="val-lemma_info"><a href="#val-lemma_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lemma_info : <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"></div></div><div class="spec val" id="val-assumption_info"><a href="#val-assumption_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>assumption_info : <a href="index.html#type-assumption">assumption</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"><p>Generate some information about the leafs of the proof tree. Currently this backend
print each lemma/assumption/hypothesis as a single leaf of the proof tree.
These function should return a triplet <code class="code">(rule, color, l)</code>, such that:
</p><ul><li><code class="code">rule</code> is a name for the proof (arbitrary, does not need to be unique, but
should rather be descriptive)</li><li><code class="code">color</code> is a color name (optional) understood by DOT</li><li><code class="code">l</code> is a list of printers that will be called to print some additional information</li></ul></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (sidekick.Sidekick_backend.Dot.Make)</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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dot.Make</span></h1></header><div class="doc"><p>Functor for making a module to export proofs to the DOT format.</p></div><h3 class="heading">Parameters</h3><div><div class="spec argument" id="argument-2-A"><a href="#argument-2-A" class="anchor"></a><div class="def argument"><code><a href="argument-2-A/index.html">A</a> : <a href="../index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-atom">atom</a> := <a href="argument-1-S/index.html#type-atom">S.atom</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-hyp">hyp</a> := <a href="argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-lemma">lemma</a> := <a href="argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-assumption">assumption</a> := <a href="argument-1-S/index.html#type-clause">S.clause</a></code></div><div class="doc"></div></div><div class="spec argument" id="argument-1-S"><a href="#argument-1-S" class="anchor"></a><div class="def argument"><code><a href="argument-1-S/index.html">S</a> : <a href="../../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a></code></div><div class="doc"></div></div></div><h3 class="heading">Signature</h3><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick.Sidekick_backend.Dot.Simple.1-S.Atom)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dot.Simple.1-S.Atom</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-atom">atom</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-is_pos"><a href="#val-is_pos" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>is_pos : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-neg"><a href="#val-neg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-abs"><a href="#val-abs" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>abs : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-compare"><a href="#val-compare" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>compare : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-equal"><a href="#val-equal" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>equal : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-lit"><a href="#val-lit" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lit : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-formula">formula</a></code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Clause (sidekick.Sidekick_backend.Dot.Simple.1-S.Clause)</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> &mdash; <span class="package">package <a href="../../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dot.Simple.1-S.Clause</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-clause">clause</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-name"><a href="#val-name" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>name : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> string</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms"><a href="#val-atoms" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> array</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms_l"><a href="#val-atoms_l" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms_l : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> list</code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"><p>A nice looking printer for clauses, which sort the atoms before printing.</p></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-t">t</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,14 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-S (sidekick.Sidekick_backend.Dot.Simple.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> &mdash; <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.Dot.Simple.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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> string</code></div><div class="doc"><p>Returns a short string description for the proof step; for instance
<code class="code">&quot;hypothesis&quot;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> <a href="index.html#type-proof_node">proof_node</a> <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span>) <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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>

View file

@ -1,9 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>2-A (sidekick.Sidekick_backend.Dot.Simple.2-A)</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> &mdash; <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.Dot.Simple.2-A</span></h1></header><p>Term printing for DOT</p><p>This module defines what functions are required in order to export
a proof to the DOT format.</p><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"><p>The type of atomic formuals</p></div></div><div class="spec type" id="type-hyp"><a href="#type-hyp" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>hyp</code><code><span class="keyword"> = </span><a href="../argument-1-S/index.html#type-formula">S.formula</a> list</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-assumption"><a href="#type-assumption" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>assumption</code><code><span class="keyword"> = </span><a href="../argument-1-S/index.html#type-formula">S.formula</a></code><code></code></div><div class="doc"><p>The type of theory-specifi proofs (also called lemmas).</p></div></div><div class="spec val" id="val-print_atom"><a href="#val-print_atom" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print_atom : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-atom">atom</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Print the contents of the given atomic formulas.
WARNING: this function should take care to escape and/or not output special
reserved characters for the dot format (such as quotes and so on).</p></div></div><div class="spec val" id="val-hyp_info"><a href="#val-hyp_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>hyp_info : <a href="index.html#type-hyp">hyp</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"></div></div><div class="spec val" id="val-lemma_info"><a href="#val-lemma_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lemma_info : <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"></div></div><div class="spec val" id="val-assumption_info"><a href="#val-assumption_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>assumption_info : <a href="index.html#type-assumption">assumption</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"><p>Generate some information about the leafs of the proof tree. Currently this backend
print each lemma/assumption/hypothesis as a single leaf of the proof tree.
These function should return a triplet <code class="code">(rule, color, l)</code>, such that:
</p><ul><li><code class="code">rule</code> is a name for the proof (arbitrary, does not need to be unique, but
should rather be descriptive)</li><li><code class="code">color</code> is a color name (optional) understood by DOT</li><li><code class="code">l</code> is a list of printers that will be called to print some additional information</li></ul></div></div></body></html>

View file

@ -1,5 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Simple (sidekick.Sidekick_backend.Dot.Simple)</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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dot.Simple</span></h1></header><div class="doc"><p>Functor for making a module to export proofs to the DOT format.
The substitution of the hyp type is non-destructive due to a restriction
of destructive substitutions on earlier versions of ocaml.</p></div><h3 class="heading">Parameters</h3><div><div class="spec argument" id="argument-2-A"><a href="#argument-2-A" class="anchor"></a><div class="def argument"><code><a href="argument-2-A/index.html">A</a> : <a href="../index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-atom">atom</a> := <a href="argument-1-S/index.html#type-formula">S.formula</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-hyp">hyp</a><span class="keyword"> = </span><a href="argument-1-S/index.html#type-formula">S.formula</a> list<span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-lemma">lemma</a> := <a href="argument-1-S/index.html#type-lemma">S.lemma</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-assumption">assumption</a><span class="keyword"> = </span><a href="argument-1-S/index.html#type-formula">S.formula</a></code></div><div class="doc"></div></div><div class="spec argument" id="argument-1-S"><a href="#argument-1-S" class="anchor"></a><div class="def argument"><code><a href="argument-1-S/index.html">S</a> : <a href="../../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a></code></div><div class="doc"></div></div></div><h3 class="heading">Signature</h3><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,6 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Dot (sidekick.Sidekick_backend.Dot)</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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend.Dot</span></h1></header><p>Dot backend for proofs</p><p>This module provides functions to export proofs into the dot graph format.
Graphs in dot format can be used to generates images using the graphviz tool.</p><div class="spec module-type" id="module-type-S"><a href="#module-type-S" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-S/index.html">S</a> = <a href="../Backend_intf/index.html#module-type-S">Backend_intf.S</a></code></div><div class="doc"><p>Interface for exporting proofs.</p></div></div><div class="spec module-type" id="module-type-Arg"><a href="#module-type-Arg" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-Arg/index.html">Arg</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Default"><a href="#module-Default" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Default/index.html">Default</a> : <span class="keyword">functor</span> (<a href="Default/argument-1-S/index.html">S</a> : <a href="../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a>) -&gt; <a href="index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Default/index.html#type-atom">atom</a> := <a href="Default/argument-1-S/index.html#type-atom">S.atom</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Default/index.html#type-hyp">hyp</a> := <a href="Default/argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Default/index.html#type-lemma">lemma</a> := <a href="Default/argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Default/index.html#type-assumption">assumption</a> := <a href="Default/argument-1-S/index.html#type-clause">S.clause</a></code></div><div class="doc"><p>Provides a reasonnable default to instantiate the <code class="code">Make</code> functor, assuming
the original printing functions are compatible with DOT html labels.</p></div></div><div class="spec module" id="module-Make"><a href="#module-Make" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Make/index.html">Make</a> : <span class="keyword">functor</span> (<a href="Make/argument-1-S/index.html">S</a> : <a href="../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a>) -&gt; <span class="keyword">functor</span> (<a href="Make/argument-2-A/index.html">A</a> : <a href="index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-atom">atom</a> := <a href="Make/argument-1-S/index.html#type-atom">S.atom</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-hyp">hyp</a> := <a href="Make/argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-lemma">lemma</a> := <a href="Make/argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-assumption">assumption</a> := <a href="Make/argument-1-S/index.html#type-clause">S.clause</a>) -&gt; <a href="index.html#module-type-S">S</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-t">t</a> := <a href="Make/argument-1-S/index.html#type-proof">S.proof</a></code></div><div class="doc"><p>Functor for making a module to export proofs to the DOT format.</p></div></div><div class="spec module" id="module-Simple"><a href="#module-Simple" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Simple/index.html">Simple</a> : <span class="keyword">functor</span> (<a href="Simple/argument-1-S/index.html">S</a> : <a href="../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a>) -&gt; <span class="keyword">functor</span> (<a href="Simple/argument-2-A/index.html">A</a> : <a href="index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Simple/index.html#type-atom">atom</a> := <a href="Simple/argument-1-S/index.html#type-formula">S.formula</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Simple/index.html#type-hyp">hyp</a><span class="keyword"> = </span><a href="Simple/argument-1-S/index.html#type-formula">S.formula</a> list<span class="keyword"> and </span><span class="keyword">type </span><a href="Simple/index.html#type-lemma">lemma</a> := <a href="Simple/argument-1-S/index.html#type-lemma">S.lemma</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Simple/index.html#type-assumption">assumption</a><span class="keyword"> = </span><a href="Simple/argument-1-S/index.html#type-formula">S.formula</a>) -&gt; <a href="index.html#module-type-S">S</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Simple/index.html#type-t">t</a> := <a href="Simple/argument-1-S/index.html#type-proof">S.proof</a></code></div><div class="doc"><p>Functor for making a module to export proofs to the DOT format.
The substitution of the hyp type is non-destructive due to a restriction
of destructive substitutions on earlier versions of ocaml.</p></div></div></body></html>

View file

@ -1,9 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Arg (sidekick.Sidekick_backend.Dot.Arg)</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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend.Dot.Arg</span></h1></header><p>Term printing for DOT</p><p>This module defines what functions are required in order to export
a proof to the DOT format.</p><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"><p>The type of atomic formuals</p></div></div><div class="spec type" id="type-hyp"><a href="#type-hyp" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>hyp</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-assumption"><a href="#type-assumption" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>assumption</code><code></code><code></code></div><div class="doc"><p>The type of theory-specifi proofs (also called lemmas).</p></div></div><div class="spec val" id="val-print_atom"><a href="#val-print_atom" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print_atom : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-atom">atom</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Print the contents of the given atomic formulas.
WARNING: this function should take care to escape and/or not output special
reserved characters for the dot format (such as quotes and so on).</p></div></div><div class="spec val" id="val-hyp_info"><a href="#val-hyp_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>hyp_info : <a href="index.html#type-hyp">hyp</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"></div></div><div class="spec val" id="val-lemma_info"><a href="#val-lemma_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lemma_info : <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"></div></div><div class="spec val" id="val-assumption_info"><a href="#val-assumption_info" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>assumption_info : <a href="index.html#type-assumption">assumption</a> <span class="keyword">&#8209;&gt;</span> string<span class="keyword"> * </span>string option<span class="keyword"> * </span>(Format.formatter <span class="keyword">&#8209;&gt;</span> unit <span class="keyword">&#8209;&gt;</span> unit) list</code></div><div class="doc"><p>Generate some information about the leafs of the proof tree. Currently this backend
print each lemma/assumption/hypothesis as a single leaf of the proof tree.
These function should return a triplet <code class="code">(rule, color, l)</code>, such that:
</p><ul><li><code class="code">rule</code> is a name for the proof (arbitrary, does not need to be unique, but
should rather be descriptive)</li><li><code class="code">color</code> is a color name (optional) understood by DOT</li><li><code class="code">l</code> is a list of printers that will be called to print some additional information</li></ul></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>S (sidekick.Sidekick_backend.Dot.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> &mdash; <span class="package">package <a href="../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend.Dot.S</span></h1></header><div class="doc"><p>Interface for exporting proofs.</p></div><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_backend (sidekick.Sidekick_backend)</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> &mdash; <span class="package">package <a href="../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend</span></h1></header><div class="spec module" id="module-Backend_intf"><a href="#module-Backend_intf" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Backend_intf/index.html">Backend_intf</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Coq"><a href="#module-Coq" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Coq/index.html">Coq</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Dedukti"><a href="#module-Dedukti" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Dedukti/index.html">Dedukti</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Dimacs"><a href="#module-Dimacs" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Dimacs/index.html">Dimacs</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Dot"><a href="#module-Dot" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Dot/index.html">Dot</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_backend__Backend_intf (sidekick.Sidekick_backend__Backend_intf)</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> &mdash; <span class="package">package <a href="../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Backend_intf</span></h1></header><p>Backend interface</p><p>This modules defines the interface of the modules providing
export of proofs.</p><div class="spec module-type" id="module-type-S"><a href="#module-type-S" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-S/index.html">S</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>S (sidekick.Sidekick_backend__Backend_intf.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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend__Backend_intf.S</span></h1></header><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick.Sidekick_backend__Coq.Make.1-S.Atom)</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> &mdash; <span class="package">package <a href="../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Coq.Make.1-S.Atom</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-atom">atom</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-is_pos"><a href="#val-is_pos" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>is_pos : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-neg"><a href="#val-neg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-abs"><a href="#val-abs" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>abs : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-compare"><a href="#val-compare" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>compare : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-equal"><a href="#val-equal" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>equal : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-lit"><a href="#val-lit" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lit : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-formula">formula</a></code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Clause (sidekick.Sidekick_backend__Coq.Make.1-S.Clause)</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> &mdash; <span class="package">package <a href="../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Coq.Make.1-S.Clause</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-clause">clause</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-name"><a href="#val-name" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>name : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> string</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms"><a href="#val-atoms" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> array</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms_l"><a href="#val-atoms_l" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms_l : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> list</code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"><p>A nice looking printer for clauses, which sort the atoms before printing.</p></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-t">t</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,14 +0,0 @@
<!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> &mdash; <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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> string</code></div><div class="doc"><p>Returns a short string description for the proof step; for instance
<code class="code">&quot;hypothesis&quot;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> <a href="index.html#type-proof_node">proof_node</a> <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span>) <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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>

View file

@ -1,8 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>2-A (sidekick.Sidekick_backend__Coq.Make.2-A)</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> &mdash; <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.2-A</span></h1></header><p>Term printing for Coq</p><div class="spec type" id="type-hyp"><a href="#type-hyp" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>hyp</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-assumption"><a href="#type-assumption" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>assumption</code><code></code><code></code></div><div class="doc"><p>The types of hypotheses, lemmas, and assumptions</p></div></div><div class="spec val" id="val-prove_hyp"><a href="#val-prove_hyp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_hyp : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-hyp">hyp</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_lemma"><a href="#val-prove_lemma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_lemma : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_assumption"><a href="#val-prove_assumption" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_assumption : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-assumption">assumption</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Proving function for hypotheses, lemmas and assumptions.
<code class="code">prove_x fmt name x</code> should prove <code class="code">x</code>, and be such that after
executing it, <code class="code">x</code> is among the coq hypotheses under the name <code class="code">name</code>.
The hypothesis should be the encoding of the given clause, i.e
for a clause <code class="code">a \/ not b \/ c</code>, the proved hypothesis should be:
<code class="code"> ~ a -&gt; ~ ~ b -&gt; ~ c -&gt; False </code>, keeping the same order as the
one in the atoms array of the clause.</p></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (sidekick.Sidekick_backend__Coq.Make)</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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Coq.Make</span></h1></header><div class="doc"><p>Base functor to output Coq proofs</p></div><h3 class="heading">Parameters</h3><div><div class="spec argument" id="argument-2-A"><a href="#argument-2-A" class="anchor"></a><div class="def argument"><code><a href="argument-2-A/index.html">A</a> : <a href="../index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-hyp">hyp</a> := <a href="argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-lemma">lemma</a> := <a href="argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-assumption">assumption</a> := <a href="argument-1-S/index.html#type-clause">S.clause</a></code></div><div class="doc"></div></div><div class="spec argument" id="argument-1-S"><a href="#argument-1-S" class="anchor"></a><div class="def argument"><code><a href="argument-1-S/index.html">S</a> : <a href="../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a></code></div><div class="doc"></div></div></div><h3 class="heading">Signature</h3><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick.Sidekick_backend__Coq.Simple.1-S.Atom)</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> &mdash; <span class="package">package <a href="../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Coq.Simple.1-S.Atom</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-atom">atom</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-is_pos"><a href="#val-is_pos" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>is_pos : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-neg"><a href="#val-neg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-abs"><a href="#val-abs" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>abs : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-compare"><a href="#val-compare" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>compare : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-equal"><a href="#val-equal" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>equal : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-lit"><a href="#val-lit" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lit : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-formula">formula</a></code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Clause (sidekick.Sidekick_backend__Coq.Simple.1-S.Clause)</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> &mdash; <span class="package">package <a href="../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Coq.Simple.1-S.Clause</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-clause">clause</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-name"><a href="#val-name" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>name : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> string</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms"><a href="#val-atoms" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> array</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms_l"><a href="#val-atoms_l" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms_l : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> list</code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"><p>A nice looking printer for clauses, which sort the atoms before printing.</p></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-t">t</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,14 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-S (sidekick.Sidekick_backend__Coq.Simple.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> &mdash; <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.Simple.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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> string</code></div><div class="doc"><p>Returns a short string description for the proof step; for instance
<code class="code">&quot;hypothesis&quot;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> <a href="index.html#type-proof_node">proof_node</a> <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span>) <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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>

View file

@ -1,8 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>2-A (sidekick.Sidekick_backend__Coq.Simple.2-A)</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> &mdash; <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.Simple.2-A</span></h1></header><p>Term printing for Coq</p><div class="spec type" id="type-hyp"><a href="#type-hyp" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>hyp</code><code><span class="keyword"> = </span><a href="../argument-1-S/index.html#type-formula">S.formula</a> list</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-assumption"><a href="#type-assumption" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>assumption</code><code></code><code></code></div><div class="doc"><p>The types of hypotheses, lemmas, and assumptions</p></div></div><div class="spec val" id="val-prove_hyp"><a href="#val-prove_hyp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_hyp : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-hyp">hyp</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_lemma"><a href="#val-prove_lemma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_lemma : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_assumption"><a href="#val-prove_assumption" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_assumption : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-assumption">assumption</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Proving function for hypotheses, lemmas and assumptions.
<code class="code">prove_x fmt name x</code> should prove <code class="code">x</code>, and be such that after
executing it, <code class="code">x</code> is among the coq hypotheses under the name <code class="code">name</code>.
The hypothesis should be the encoding of the given clause, i.e
for a clause <code class="code">a \/ not b \/ c</code>, the proved hypothesis should be:
<code class="code"> ~ a -&gt; ~ ~ b -&gt; ~ c -&gt; False </code>, keeping the same order as the
one in the atoms array of the clause.</p></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Simple (sidekick.Sidekick_backend__Coq.Simple)</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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Coq.Simple</span></h1></header><div class="doc"><p>Simple functo to output Coq proofs</p></div><h3 class="heading">Parameters</h3><div><div class="spec argument" id="argument-2-A"><a href="#argument-2-A" class="anchor"></a><div class="def argument"><code><a href="argument-2-A/index.html">A</a> : <a href="../index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-hyp">hyp</a><span class="keyword"> = </span><a href="argument-1-S/index.html#type-formula">S.formula</a> list<span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-lemma">lemma</a> := <a href="argument-1-S/index.html#type-lemma">S.lemma</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-assumption">assumption</a> := <a href="argument-1-S/index.html#type-formula">S.formula</a></code></div><div class="doc"></div></div><div class="spec argument" id="argument-1-S"><a href="#argument-1-S" class="anchor"></a><div class="def argument"><code><a href="argument-1-S/index.html">S</a> : <a href="../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a></code></div><div class="doc"></div></div></div><h3 class="heading">Signature</h3><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,4 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_backend__Coq (sidekick.Sidekick_backend__Coq)</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> &mdash; <span class="package">package <a href="../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Coq</span></h1></header><p>Coq Backend</p><p>This module provides an easy way to produce coq scripts
corresponding to the resolution proofs output by the
sat solver.</p><div class="spec module-type" id="module-type-S"><a href="#module-type-S" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-S/index.html">S</a> = <a href="../Sidekick_backend/Backend_intf/index.html#module-type-S">Sidekick_backend.Backend_intf.S</a></code></div><div class="doc"><p>Interface for exporting proofs.</p></div></div><div class="spec module-type" id="module-type-Arg"><a href="#module-type-Arg" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-Arg/index.html">Arg</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Make"><a href="#module-Make" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Make/index.html">Make</a> : <span class="keyword">functor</span> (<a href="Make/argument-1-S/index.html">S</a> : <a href="../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a>) -&gt; <span class="keyword">functor</span> (<a href="Make/argument-2-A/index.html">A</a> : <a href="index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-hyp">hyp</a> := <a href="Make/argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-lemma">lemma</a> := <a href="Make/argument-1-S/index.html#type-clause">S.clause</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-assumption">assumption</a> := <a href="Make/argument-1-S/index.html#type-clause">S.clause</a>) -&gt; <a href="index.html#module-type-S">S</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-t">t</a> := <a href="Make/argument-1-S/index.html#type-proof">S.proof</a></code></div><div class="doc"><p>Base functor to output Coq proofs</p></div></div><div class="spec module" id="module-Simple"><a href="#module-Simple" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Simple/index.html">Simple</a> : <span class="keyword">functor</span> (<a href="Simple/argument-1-S/index.html">S</a> : <a href="../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a>) -&gt; <span class="keyword">functor</span> (<a href="Simple/argument-2-A/index.html">A</a> : <a href="index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Simple/index.html#type-hyp">hyp</a><span class="keyword"> = </span><a href="Simple/argument-1-S/index.html#type-formula">S.formula</a> list<span class="keyword"> and </span><span class="keyword">type </span><a href="Simple/index.html#type-lemma">lemma</a> := <a href="Simple/argument-1-S/index.html#type-lemma">S.lemma</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Simple/index.html#type-assumption">assumption</a> := <a href="Simple/argument-1-S/index.html#type-formula">S.formula</a>) -&gt; <a href="index.html#module-type-S">S</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Simple/index.html#type-t">t</a> := <a href="Simple/argument-1-S/index.html#type-proof">S.proof</a></code></div><div class="doc"><p>Simple functo to output Coq proofs</p></div></div></body></html>

View file

@ -1,8 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Arg (sidekick.Sidekick_backend__Coq.Arg)</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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend__Coq.Arg</span></h1></header><p>Term printing for Coq</p><div class="spec type" id="type-hyp"><a href="#type-hyp" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>hyp</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-assumption"><a href="#type-assumption" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>assumption</code><code></code><code></code></div><div class="doc"><p>The types of hypotheses, lemmas, and assumptions</p></div></div><div class="spec val" id="val-prove_hyp"><a href="#val-prove_hyp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_hyp : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-hyp">hyp</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_lemma"><a href="#val-prove_lemma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_lemma : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-prove_assumption"><a href="#val-prove_assumption" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prove_assumption : Format.formatter <span class="keyword">&#8209;&gt;</span> string <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-assumption">assumption</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>Proving function for hypotheses, lemmas and assumptions.
<code class="code">prove_x fmt name x</code> should prove <code class="code">x</code>, and be such that after
executing it, <code class="code">x</code> is among the coq hypotheses under the name <code class="code">name</code>.
The hypothesis should be the encoding of the given clause, i.e
for a clause <code class="code">a \/ not b \/ c</code>, the proved hypothesis should be:
<code class="code"> ~ a -&gt; ~ ~ b -&gt; ~ c -&gt; False </code>, keeping the same order as the
one in the atoms array of the clause.</p></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>S (sidekick.Sidekick_backend__Coq.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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend__Coq.S</span></h1></header><div class="doc"><p>Interface for exporting proofs.</p></div><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick.Sidekick_backend__Dedukti.Make.1-S.Atom)</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> &mdash; <span class="package">package <a href="../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Dedukti.Make.1-S.Atom</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-atom">atom</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-is_pos"><a href="#val-is_pos" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>is_pos : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-neg"><a href="#val-neg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>neg : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-abs"><a href="#val-abs" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>abs : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-compare"><a href="#val-compare" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>compare : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> int</code></div><div class="doc"></div></div><div class="spec val" id="val-equal"><a href="#val-equal" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>equal : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> bool</code></div><div class="doc"></div></div><div class="spec val" id="val-lit"><a href="#val-lit" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lit : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-formula">formula</a></code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Clause (sidekick.Sidekick_backend__Dedukti.Make.1-S.Clause)</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> &mdash; <span class="package">package <a href="../../../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Dedukti.Make.1-S.Clause</span></h1></header><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code><span class="keyword"> = </span><a href="../index.html#type-clause">clause</a></code><code></code></div><div class="doc"></div></div><div class="spec val" id="val-name"><a href="#val-name" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>name : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> string</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms"><a href="#val-atoms" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> array</code></div><div class="doc"></div></div><div class="spec val" id="val-atoms_l"><a href="#val-atoms_l" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atoms_l : <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> <a href="../index.html#type-atom">atom</a> list</code></div><div class="doc"></div></div><div class="spec val" id="val-pp"><a href="#val-pp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp : <a href="index.html#type-t">t</a> <a href="../../../../Sidekick_sat__/Res_intf/index.html#type-printer">Sidekick_sat__.Res_intf.printer</a></code></div><div class="doc"><p>A nice looking printer for clauses, which sort the atoms before printing.</p></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-t">t</a></code></div><div class="doc"></div></div></body></html>

View file

@ -1,14 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-S (sidekick.Sidekick_backend__Dedukti.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> &mdash; <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__Dedukti.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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> string</code></div><div class="doc"><p>Returns a short string description for the proof step; for instance
<code class="code">&quot;hypothesis&quot;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</span> <a href="index.html#type-proof_node">proof_node</a> <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span>) <span class="keyword">&#8209;&gt;</span> <span class="type-var">'a</span> <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</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">&#8209;&gt;</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">&#8209;&gt;</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>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>2-A (sidekick.Sidekick_backend__Dedukti.Make.2-A)</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> &mdash; <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__Dedukti.Make.2-A</span></h1></header><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-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"></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 val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-formula">formula</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><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 : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-context"><a href="#val-context" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>context : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (sidekick.Sidekick_backend__Dedukti.Make)</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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Dedukti.Make</span></h1></header><div class="doc"><p>Functor to generate a backend to output proofs for the dedukti type checker.</p></div><h3 class="heading">Parameters</h3><div><div class="spec argument" id="argument-2-A"><a href="#argument-2-A" class="anchor"></a><div class="def argument"><code><a href="argument-2-A/index.html">A</a> : <a href="../index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-formula">formula</a> := <a href="argument-1-S/index.html#type-formula">S.formula</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-lemma">lemma</a> := <a href="argument-1-S/index.html#type-lemma">S.lemma</a><span class="keyword"> and </span><span class="keyword">type </span><a href="argument-2-A/index.html#type-proof">proof</a> := <a href="argument-1-S/index.html#type-proof">S.proof</a></code></div><div class="doc"></div></div><div class="spec argument" id="argument-1-S"><a href="#argument-1-S" class="anchor"></a><div class="def argument"><code><a href="argument-1-S/index.html">S</a> : <a href="../../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a></code></div><div class="doc"></div></div></div><h3 class="heading">Signature</h3><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_backend__Dedukti (sidekick.Sidekick_backend__Dedukti)</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> &mdash; <span class="package">package <a href="../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">Sidekick_backend__Dedukti</span></h1></header><p>Deduki backend for proofs</p><p>Work in progress...</p><div class="spec module-type" id="module-type-S"><a href="#module-type-S" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-S/index.html">S</a> = <a href="../Sidekick_backend/Backend_intf/index.html#module-type-S">Sidekick_backend.Backend_intf.S</a></code></div><div class="doc"></div></div><div class="spec module-type" id="module-type-Arg"><a href="#module-type-Arg" class="anchor"></a><div class="def module-type"><code><span class="keyword">module type </span><a href="module-type-Arg/index.html">Arg</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-Make"><a href="#module-Make" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Make/index.html">Make</a> : <span class="keyword">functor</span> (<a href="Make/argument-1-S/index.html">S</a> : <a href="../Sidekick_sat/Res/index.html#module-type-S">Sidekick_sat.Res.S</a>) -&gt; <span class="keyword">functor</span> (<a href="Make/argument-2-A/index.html">A</a> : <a href="index.html#module-type-Arg">Arg</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-formula">formula</a> := <a href="Make/argument-1-S/index.html#type-formula">S.formula</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-lemma">lemma</a> := <a href="Make/argument-1-S/index.html#type-lemma">S.lemma</a><span class="keyword"> and </span><span class="keyword">type </span><a href="Make/index.html#type-proof">proof</a> := <a href="Make/argument-1-S/index.html#type-proof">S.proof</a>) -&gt; <a href="index.html#module-type-S">S</a><span class="keyword"> with </span><span class="keyword">type </span><a href="Make/index.html#type-t">t</a> := <a href="Make/argument-1-S/index.html#type-proof">S.proof</a></code></div><div class="doc"><p>Functor to generate a backend to output proofs for the dedukti type checker.</p></div></div></body></html>

View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Arg (sidekick.Sidekick_backend__Dedukti.Arg)</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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend__Dedukti.Arg</span></h1></header><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-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"></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 val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-formula">formula</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><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 : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-lemma">lemma</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-context"><a href="#val-context" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>context : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-proof">proof</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"></div></div></body></html>

View file

@ -1,3 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>S (sidekick.Sidekick_backend__Dedukti.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> &mdash; <span class="package">package <a href="../../index.html">sidekick</a></span></nav><header><h1><span class="keyword">Module type</span> <span class="module-path">Sidekick_backend__Dedukti.S</span></h1></header><p>Proof exporting</p><p>Currently, exporting a proof means printing it into a file
according to the conventions of a given format.</p><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>t</code><code></code><code></code></div><div class="doc"><p>The type of proofs.</p></div></div><div class="spec val" id="val-print"><a href="#val-print" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>print : Format.formatter <span class="keyword">&#8209;&gt;</span> <a href="index.html#type-t">t</a> <span class="keyword">&#8209;&gt;</span> unit</code></div><div class="doc"><p>A function for printing proofs in the desired format.</p></div></div></body></html>

File diff suppressed because one or more lines are too long

Some files were not shown because too many files have changed in this diff Show more