This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.
<!DOCTYPE html>
<htmlxmlns="http://www.w3.org/1999/xhtml"><head><title>Prover (infer.Biabduction.Prover)</title><linkrel="stylesheet"href="../../../odoc.css"/><metacharset="utf-8"/><metaname="generator"content="odoc 1.5.0"/><metaname="viewport"content="width=device-width,initial-scale=1.0"/><scriptsrc="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><divclass="content"><header><nav><ahref="../index.html">Up</a>–<ahref="../../index.html">infer</a>»<ahref="../index.html">Biabduction</a>» Prover</nav><h1>Module <code>Biabduction.Prover</code></h1><navclass="toc"><ul><li><ahref="#ordinary-theorem-proving">Ordinary Theorem Proving</a></li><li><ahref="#abduction-prover">Abduction prover</a></li><li><ahref="#cover:-minimum-set-of-pi's-whose-disjunction-is-equivalent-to-true">Cover: minimum set of pi's whose disjunction is equivalent to true</a></li></ul></nav></header><aside><p>Functions for Theorem Proving</p></aside><dl><dtclass="spec value"id="val-atom_negate"><ahref="#val-atom_negate"class="anchor"></a><code><spanclass="keyword">val</span> atom_negate : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><ahref="../Predicates/index.html#type-atom">Predicates.atom</a><span>-></span><ahref="../Predicates/index.html#type-atom">Predicates.atom</a></code></dt><dd><p>Negate an atom</p></dd></dl><section><header><h3id="ordinary-theorem-proving"><ahref="#ordinary-theorem-proving"class="anchor"></a>Ordinary Theorem Proving</h3></header><dl><dtclass="spec value"id="val-check_zero"><ahref="#val-check_zero"class="anchor"></a><code><spanclass="keyword">val</span> check_zero : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span> bool</code></dt><dd><p>Check <code>|- e=0</code>. Result <code>false</code> means "don't know".</p></dd></dl><dl><dtclass="spec value"id="val-check_equal"><ahref="#val-check_equal"class="anchor"></a><code><spanclass="keyword">val</span> check_equal : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><ahref="../Prop/index.html#type-normal">Prop.normal</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span><ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span> bool</code></dt><dd><p>Check <code>prop |- exp1=exp2</code>. Result <code>false</code> means "don't know".</p></dd></dl><dl><dtclass="spec value"id="val-check_disequal"><ahref="#val-check_disequal"class="anchor"></a><code><spanclass="keyword">val</span> check_disequal : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><ahref="../Prop/index.html#type-normal">Prop.normal</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span><ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span> bool</code></dt><dd><p>Check whether <code>prop |- exp1!=exp2</code>. Result <code>false</code> means "don't know".</p></dd></dl><dl><dtclass="spec value"id="val-check_atom"><ahref="#val-check_atom"class="anchor"></a><code><spanclass="keyword">val</span> check_atom : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><ahref="../Prop/index.html#type-normal">Prop.normal</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span><ahref="../Predicates/index.html#type-atom">Predicates.atom</a><span>-></span> bool</code></dt><dd><p>Check whether <code>prop |- a</code>. Result <code>false</code> means "don't know".</p></dd></dl><dl><dtclass="spec value"id="val-check_inconsistency_base"><ahref="#val-check_inconsistency_base"class="anchor"></a><code><spanclass="keyword">val</span> check_inconsistency_base : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><ahref="../Prop/index.html#type-normal">Prop.normal</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span> bool</code></dt><dd><p>Inconsistency checking ignoring footprint.</p></dd></dl><dl><dtclass="spec value"id="val-check_inconsistency"><ahref="#val-check_inconsistency"class="anchor"></a><code><spanclass="keyword">val</span> check_inconsistency : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><ahref="../Prop/index.html#type-normal">Prop.normal</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span> bool</code></dt><dd><p>Inconsistency checking.</p></dd></dl><dl><dtclass="spec value"id="val-check_allocatedness"><ahref="#val-check_allocatedness"class="anchor"></a><code><spanclass="keyword">val</span> check_allocatedness : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><ahref="../Prop/index.html#type-normal">Prop.normal</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span><ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span> bool</code></dt><dd><p>Check whether <code>prop |- allocated(exp)</code>.</p></dd></dl><dl><dtclass="spec value"id="val-is_root"><ahref="#val-is_root"class="anchor"></a><code><spanclass="keyword">val</span> is_root : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><ahref="../Prop/index.html#type-normal">Prop.normal</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span><ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><span><span><ahref="../Predicates/index.html#type-offset">Predicates.offset</a> list</span> option</span></code></dt><dd><p><code>is_root prop base_exp exp</code> checks whether <code>base_exp = exp.offlist</code> for some list of offsets <code>offlist</code>. If so, it returns <code>Some(offlist)</code>. Otherwise, it returns <code>None</code>. Assumes that <code>base_exp</code> points to the beginning of a structure, not the middle.</p></dd></dl><dl><dtclass="spec value"id="val-expand_hpred_pointer"><ahref="#val-expand_hpred_pointer"class="anchor"></a><code><spanclass="keyword">val</span> expand_hpred_pointer : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span> bool <span>-></span><ahref="../Predicates/index.html#type-hpred">Predicates.hpred</a><span>-></span> bool * bool * <ahref="../Predicates/index.html#type-hpred">Predicates.hpred</a></code></dt><dd><p><code>expand_hpred_pointer calc_index_frame hpred</code> expands <code>hpred</code> if it is a |-> whose lhs is a Lfield or Lindex or ptr+off. Return <code>(changed, calc_index_frame', hpred')</code> where <code>changed</code> indicates whether the predicate has changed.</p></dd></dl><dl><dtclass="spec value"id="val-get_bounds"><ahref="#val-get_bounds"class="anchor"></a><code><spanclass="keyword">val</span> get_bounds : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><ahref="../Prop/index.html#type-normal">Prop.normal</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span><ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><span><ahref="../../IR/IntLit/index.html#type-t">IR.IntLit.t</a> option</span> * <span><ahref="../../IR/IntLit/index.html#type-t">IR.IntLit.t</a> option</span></code></dt><dd><p>Get upper and lower bounds of an expression, if any</p></dd></dl></section><section><header><h3id="abduction-prover"><ahref="#abduction-prover"class="anchor"></a>Abduction prover</h3></header><dl><dtclass="spec value"id="val-check_implication"><ahref="#val-check_implication"class="anchor"></a><code><spanclass="keyword">val</span> check_implication : <span><ahref="../BiabductionSummary/index.html#type-t">BiabductionSummary.t</a><ahref="../../Absint/InterproceduralAnalysis/index.html#type-t">Absint.InterproceduralAnalysis.t</a></span><span>-></span><span><ahref="../Prop/index.html#type-normal">Prop.normal</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span><span><ahref="../Prop/index.html#type-exposed">Prop.exposed</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span> bool</code></dt><dd><p><code>check_implication p1 p2</code> returns true if <code>p1|-p2</code></p></dd></dl><dl><dtclass="spec type"id="type-check"><ahref="#type-check"class="anchor"></a><code><spanclass="keyword">type</span> check</code><code> = </code><tableclass="variant"><trid="type-check.Bounds_check"class="anchored"><tdclass="def constructor"><ahref="#type-check.Bounds_check"class="anchor"></a><code>| </code><code><spanclass="constructor">Bounds_check</span></code></td></tr><trid="type-check.Class_cast_check"class="anchored"><tdclass="def constructor"><ahref="#type-check.Class_cast_check"class="anchor"></a><code>| </code><code><spanclass="constructor">Class_cast_check</span><spanclass="keyword">of</span><ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a></code></td></tr></table></dt></dl><dl><dtclass="spec value"id="val-d_typings"><ahref="#val-d_typings"class="anchor"></a><code><spanclass="keyword">val</span> d_typings : <span><span>(<ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a>)</span> list</span><span>-></span> unit</code></dt></dl><dl><dtclass="spec type"id="type-implication_result"><ahref="#type-implication_result"class="anchor"></a><code><spanclass="keyword">type</span> implication_result</code><code> = </code><tableclass="variant"><trid="type-implication_result.ImplOK"class="anchored"><tdclass="def constructor"><ahref="#type-implication_result.ImplOK"class="anchor"></a><code>| </code><code><spanclass="constructor">ImplOK</span><spanclass="keyword">of</span><span><ahref="index.html#type-check">check</a> list</span> * <ahref="../Predicates/index.html#type-subst">Predicates.subst</a> * <ahref="../Predicates/index.html#type-subst">Predicates.subst</a> * <span><ahref="../Predicates/index.html#type-hpred">Predicates.hpred</a> list</span> * <span><ahref="../Predicates/index.html#type-atom">Predicates.atom</a> list</span> * <span><ahref="../Predicates/index.html#type-hpred">Predicates.hpred</a> list</span> * <span><ahref="../Predicates/index.html#type-hpred">Predicates.hpred</a> list</span> * <span><ahref="../Predicates/index.html#type-hpred">Predicates.hpred</a> list</span> * <span><span>(<ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a>)</span> list</span> * <span><span>(<ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../../IR/Exp/index.html#type-t">IR.Exp.t</a>)</span> list</span></code></td></tr><trid="type-implication_result.ImplFail"class="anchored"><tdclass="def constructor"><ahref="#type-implication_result.ImplFail"class="anchor"></a><code>| </code><code><spanclass="constructor">ImplFail</span><spanclass="keyword">of</span><span><ahref="index.html#type-check">check</a> list</span></code></td></tr></table></dt></dl><dl><dtclass="spec value"id="val-check_implication_for_footprint"><ahref="#val-check_implication_for_footprint"class="anchor"></a><code><spanclass="keyword">val</span> check_implication_for_footprint : <span><ahref="../BiabductionSummary/index.html#type-t">BiabductionSummary.t</a><ahref="../../Absint/InterproceduralAnalysis/index.html#type-t">Absint.InterproceduralAnalysis.t</a></span><span>-></span><span><ahref="../Prop/index.html#type-normal">Prop.normal</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span><span><ahref="../Prop/index.html#type-exposed">Prop.exposed</a><ahref="../Prop/index.html#type-t">Prop.t</a></span><span>-></span><ahref="index.html#type-implication_result">implication_result</a></code></dt><dd><p><code>check_implication_for_footprint p1 p2</code> returns <code>Some(sub, frame, missing)</code> if <code>sub(p1 * missing) |- sub(p2 * frame)</code> where <code>sub</code> is a substitution which instantiates the primed vars of <code>p1</code> and <code>p2</code>, which are assumed to be disjoint.</p></dd></dl></section><section><header><h3id="cover:-minimum-set-of-pi's-whose-disjunction-is-equivalent-to-true"><ahref="#cover:-minimum-set-of-pi's-whose-disjunction-is-equivalent-to-true"class="anchor"></a>Cover: minimum set of pi's whose disjunction is equivalent to true</h3></header><dl><dtclass="spec value"id="val-find_minimum_pure_cover"><ahref="#val-find_minimum_pure_cover"class="anchor"></a><code><spanclass="keyword">val</span> find_minimum_pure_cover : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span><span>(<span><ahref="../Predicates/index.html#type-atom">Predicates.atom</a> list</span> * <spanclass="type-var">'a</span>)</span> list</span><span>-></span><span><span><span>(<span><ahref="../Predicates/index.html#type-atom">Predicates.atom</a> list</span> * <spanclass="type-var">'a</span>)</span> list</span> option</span></code></dt><dd><p>Find minimum set of pi's in <code>cases</code> whose disjunction covers true</p></dd></dl></section></div></body></html>
