You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
|
|
|
|
|
<!DOCTYPE html>
|
|
|
|
|
|
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Prop (infer.InferModules.Prop)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc %%VERSION%%"/><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">infer</a> » <a href="../index.html">InferModules</a> » Prop</nav><h1>Module <code>InferModules.Prop</code></h1><nav class="toc"><ul><li><a href="#basic-functions-for-propositions">Basic Functions for propositions</a></li><li><a href="#normalization">Normalization</a></li><li><a href="#compaction">Compaction</a></li><li><a href="#queries-about-propositions">Queries about propositions</a></li><li><a href="#functions-for-changing-and-generating-propositions">Functions for changing and generating propositions</a></li><li><a href="#functions-for-existentially-quantifying-and-unquantifying-variables">Functions for existentially quantifying and unquantifying variables</a></li><li><a href="#prop-iterators">Prop iterators</a></li><li><a href="#internal-modules">Internal modules</a></li></ul></nav></header><aside><p>Functions for Propositions (i.e., Symbolic Heaps)</p></aside><dl><dt class="spec type" id="type-normal"><a href="#type-normal" class="anchor"></a><code><span class="keyword">type</span> normal</code></dt><dd><p>kind for normal props, i.e. normalized</p></dd></dl><dl><dt class="spec type" id="type-exposed"><a href="#type-exposed" class="anchor"></a><code><span class="keyword">type</span> exposed</code></dt><dd><p>kind for exposed props</p></dd></dl><dl><dt class="spec type" id="type-sorted"><a href="#type-sorted" class="anchor"></a><code><span class="keyword">type</span> sorted</code></dt><dd><p>kind for sorted props</p></dd></dl><aside><p>Proposition.</p></aside><dl><dt class="spec type" id="type-pi"><a href="#type-pi" class="anchor"></a><code><span class="keyword">type</span> pi</code><code> = <span><a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> list</span></code></dt><dt class="spec type" id="type-sigma"><a href="#type-sigma" class="anchor"></a><code><span class="keyword">type</span> sigma</code><code> = <span><a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list</span></code></dt><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> <span>'a t</span></code><code> = <span class="keyword">private</span> </code><code>{</code><table class="record"><tr id="type-t.sigma" class="anchored"><td class="def field"><a href="#type-t.sigma" class="anchor"></a><code>sigma : <a href="index.html#type-sigma">sigma</a>;</code></td><td class="doc"><p>spatial part</p></td></tr><tr id="type-t.sub" class="anchored"><td class="def field"><a href="#type-t.sub" class="anchor"></a><code>sub : <a href="../../../InferIR/InferIR/Sil/index.html#type-subst">InferIR.Sil.subst</a>;</code></td><td class="doc"><p>substitution</p></td></tr><tr id="type-t.pi" class="anchored"><td class="def field"><a href="#type-t.pi" class="anchor"></a><code>pi : <a href="index.html#type-pi">pi</a>;</code></td><td class="doc"><p>pure part</p></td></tr><tr id="type-t.sigma_fp" class="anchored"><td class="def field"><a href="#type-t.sigma_fp" class="anchor"></a><code>sigma_fp : <a href="index.html#type-sigma">sigma</a>;</code></td><td class="doc"><p>abduced spatial part</p></td></tr><tr id="type-t.pi_fp" class="anchored"><td class="def field"><a href="#type-t.pi_fp" class="anchor"></a><code>pi_fp : <a href="index.html#type-pi">pi</a>;</code></td><td class="doc"><p>abduced pure part</p></td></tr></table><code>}</code></dt><dd><p>the kind 'a should range over <code>normal</code> and <code>exposed</code></p></dd></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><cod
|
