mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 11:45:41 -05:00
2 lines
No EOL
13 KiB
HTML
2 lines
No EOL
13 KiB
HTML
<!DOCTYPE html>
|
||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>P (sidekick-bin.Sidekick_smtlib.Process.Solver.P)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.3"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-bin</a> » <a href="../../../index.html">Sidekick_smtlib</a> » <a href="../../index.html">Process</a> » <a href="../index.html">Solver</a> » P</nav><h1>Module <code>Solver.P</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>The abstract representation of a proof. A proof always proves a clause to be <b>valid</b> (true in every possible interpretation of the problem's assertions, and the theories)</p></dd></dl><dl><dt class="spec type" id="type-term"><a href="#type-term" class="anchor"></a><code><span class="keyword">type</span> term</code><code> = <a href="../T/Term/index.html#type-t">T.Term.t</a></code></dt><dt class="spec type" id="type-ty"><a href="#type-ty" class="anchor"></a><code><span class="keyword">type</span> ty</code></dt><dt class="spec type" id="type-hres_step"><a href="#type-hres_step" class="anchor"></a><code><span class="keyword">type</span> hres_step</code></dt><dd><p>hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation</p></dd></dl><dl><dt class="spec value" id="val-r"><a href="#val-r" class="anchor"></a><code><span class="keyword">val</span> r : <a href="index.html#type-t">t</a> <span>-></span> <span>pivot:<a href="index.html#type-term">term</a></span> <span>-></span> <a href="index.html#type-hres_step">hres_step</a></code></dt><dd><p>Resolution step on given pivot term</p></dd></dl><dl><dt class="spec value" id="val-r1"><a href="#val-r1" class="anchor"></a><code><span class="keyword">val</span> r1 : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-hres_step">hres_step</a></code></dt><dd><p>Unit resolution; pivot is obvious</p></dd></dl><dl><dt class="spec value" id="val-p"><a href="#val-p" class="anchor"></a><code><span class="keyword">val</span> p : <a href="index.html#type-t">t</a> <span>-></span> <span>lhs:<a href="index.html#type-term">term</a></span> <span>-></span> <span>rhs:<a href="index.html#type-term">term</a></span> <span>-></span> <a href="index.html#type-hres_step">hres_step</a></code></dt><dd><p>Paramodulation using proof whose conclusion has a literal <code>lhs=rhs</code></p></dd></dl><dl><dt class="spec value" id="val-p1"><a href="#val-p1" class="anchor"></a><code><span class="keyword">val</span> p1 : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-hres_step">hres_step</a></code></dt><dd><p>Unit paramodulation</p></dd></dl><dl><dt class="spec type" id="type-lit"><a href="#type-lit" class="anchor"></a><code><span class="keyword">type</span> lit</code></dt><dd><p>Proof representation of literals</p></dd></dl><dl><dt class="spec value" id="val-pp_lit"><a href="#val-pp_lit" class="anchor"></a><code><span class="keyword">val</span> pp_lit : <span><a href="index.html#type-lit">lit</a> <a href="../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-lit_a"><a href="#val-lit_a" class="anchor"></a><code><span class="keyword">val</span> lit_a : <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-lit">lit</a></code></dt><dt class="spec value" id="val-lit_na"><a href="#val-lit_na" class="anchor"></a><code><span class="keyword">val</span> lit_na : <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-lit">lit</a></code></dt><dt class="spec value" id="val-lit_mk"><a href="#val-lit_mk" class="anchor"></a><code><span class="keyword">val</span> lit_mk : bool <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-lit">lit</a></code></dt><dt class="spec value" id="val-lit_eq"><a href="#val-lit_eq" class="anchor"></a><code><span class="keyword">val</span> lit_eq : <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-lit">lit</a></code></dt><dt class="spec value" id="val-lit_neq"><a href="#val-lit_neq" class="anchor"></a><code><span class="keyword">val</span> lit_neq : <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-lit">lit</a></code></dt><dt class="spec value" id="val-lit_not"><a href="#val-lit_not" class="anchor"></a><code><span class="keyword">val</span> lit_not : <a href="index.html#type-lit">lit</a> <span>-></span> <a href="index.html#type-lit">lit</a></code></dt><dt class="spec value" id="val-lit_sign"><a href="#val-lit_sign" class="anchor"></a><code><span class="keyword">val</span> lit_sign : <a href="index.html#type-lit">lit</a> <span>-></span> bool</code></dt></dl><dl><dt class="spec type" id="type-composite_step"><a href="#type-composite_step" class="anchor"></a><code><span class="keyword">type</span> composite_step</code></dt></dl><dl><dt class="spec value" id="val-stepc"><a href="#val-stepc" class="anchor"></a><code><span class="keyword">val</span> stepc : <span>name:string</span> <span>-></span> <span><a href="index.html#type-lit">lit</a> list</span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-composite_step">composite_step</a></code></dt><dt class="spec value" id="val-deft"><a href="#val-deft" class="anchor"></a><code><span class="keyword">val</span> deft : <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-composite_step">composite_step</a></code></dt><dd><p>define a (new) atomic term</p></dd></dl><dl><dt class="spec value" id="val-is_trivial_refl"><a href="#val-is_trivial_refl" class="anchor"></a><code><span class="keyword">val</span> is_trivial_refl : <a href="index.html#type-t">t</a> <span>-></span> bool</code></dt><dd><p>is this a proof of <code>|- t=t</code>? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using <code>refl t</code> is useless).</p></dd></dl><dl><dt class="spec value" id="val-assertion"><a href="#val-assertion" class="anchor"></a><code><span class="keyword">val</span> assertion : <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-assertion_c"><a href="#val-assertion_c" class="anchor"></a><code><span class="keyword">val</span> assertion_c : <span><a href="index.html#type-lit">lit</a> Iter.t</span> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-ref_by_name"><a href="#val-ref_by_name" class="anchor"></a><code><span class="keyword">val</span> ref_by_name : string <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-assertion_c_l"><a href="#val-assertion_c_l" class="anchor"></a><code><span class="keyword">val</span> assertion_c_l : <span><a href="index.html#type-lit">lit</a> list</span> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-hres_iter"><a href="#val-hres_iter" class="anchor"></a><code><span class="keyword">val</span> hres_iter : <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-hres_step">hres_step</a> Iter.t</span> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-hres_l"><a href="#val-hres_l" class="anchor"></a><code><span class="keyword">val</span> hres_l : <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-hres_step">hres_step</a> list</span> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-res"><a href="#val-res" class="anchor"></a><code><span class="keyword">val</span> res : <span>pivot:<a href="index.html#type-term">term</a></span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-res1"><a href="#val-res1" class="anchor"></a><code><span class="keyword">val</span> res1 : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-refl"><a href="#val-refl" class="anchor"></a><code><span class="keyword">val</span> refl : <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-true_is_true"><a href="#val-true_is_true" class="anchor"></a><code><span class="keyword">val</span> true_is_true : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-true_neq_false"><a href="#val-true_neq_false" class="anchor"></a><code><span class="keyword">val</span> true_neq_false : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-nn"><a href="#val-nn" class="anchor"></a><code><span class="keyword">val</span> nn : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-cc_lemma"><a href="#val-cc_lemma" class="anchor"></a><code><span class="keyword">val</span> cc_lemma : <span><a href="index.html#type-lit">lit</a> list</span> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-cc_imply2"><a href="#val-cc_imply2" class="anchor"></a><code><span class="keyword">val</span> cc_imply2 : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-cc_imply_l"><a href="#val-cc_imply_l" class="anchor"></a><code><span class="keyword">val</span> cc_imply_l : <span><a href="index.html#type-t">t</a> list</span> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-composite_iter"><a href="#val-composite_iter" class="anchor"></a><code><span class="keyword">val</span> composite_iter : <span>?⁠assms:<span><span>(string * <a href="index.html#type-lit">lit</a>)</span> list</span></span> <span>-></span> <span><a href="index.html#type-composite_step">composite_step</a> Iter.t</span> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-composite_l"><a href="#val-composite_l" class="anchor"></a><code><span class="keyword">val</span> composite_l : <span>?⁠assms:<span><span>(string * <a href="index.html#type-lit">lit</a>)</span> list</span></span> <span>-></span> <span><a href="index.html#type-composite_step">composite_step</a> list</span> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-sorry"><a href="#val-sorry" class="anchor"></a><code><span class="keyword">val</span> sorry : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-sorry_c"><a href="#val-sorry_c" class="anchor"></a><code><span class="keyword">val</span> sorry_c : <span><a href="index.html#type-lit">lit</a> Iter.t</span> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-sorry_c_l"><a href="#val-sorry_c_l" class="anchor"></a><code><span class="keyword">val</span> sorry_c_l : <span><a href="index.html#type-lit">lit</a> list</span> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-default"><a href="#val-default" class="anchor"></a><code><span class="keyword">val</span> default : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-pp_debug"><a href="#val-pp_debug" class="anchor"></a><code><span class="keyword">val</span> pp_debug : <span>sharing:bool</span> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt><dd><p>Pretty print a proof.</p><dl><dt>parameter sharing</dt><dd><p>if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.</p></dd></dl></dd></dl><div class="spec module" id="module-Quip"><a href="#module-Quip" class="anchor"></a><code><span class="keyword">module</span> <a href="Quip/index.html">Quip</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div></div></body></html> |