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>Pulselib__PulsePathCondition (infer.Pulselib__PulsePathCondition)</title><linkrel="stylesheet"href="../../odoc.css"/><metacharset="utf-8"/><metaname="generator"content="odoc 1.5.1"/><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>» Pulselib__PulsePathCondition</nav><h1>Module <code>Pulselib__PulsePathCondition</code></h1><navclass="toc"><ul><li><ahref="#building-arithmetic-constraints">Building arithmetic constraints</a></li><li><ahref="#operations">Operations</a></li><li><ahref="#queries">Queries</a></li></ul></nav></header><divclass="spec module"id="module-F"><ahref="#module-F"class="anchor"></a><code><spanclass="keyword">module</span> F = Stdlib.Format</code></div><divclass="spec module"id="module-AbstractValue"><ahref="#module-AbstractValue"class="anchor"></a><code><spanclass="keyword">module</span> AbstractValue = <ahref="../Pulselib/index.html#module-PulseAbstractValue">Pulselib.PulseAbstractValue</a></code></div><divclass="spec module"id="module-SatUnsat"><ahref="#module-SatUnsat"class="anchor"></a><code><spanclass="keyword">module</span> SatUnsat = <ahref="../Pulselib/index.html#module-PulseSatUnsat">Pulselib.PulseSatUnsat</a></code></div><divclass="spec module"id="module-ValueHistory"><ahref="#module-ValueHistory"class="anchor"></a><code><spanclass="keyword">module</span> ValueHistory = <ahref="../Pulselib/index.html#module-PulseValueHistory">Pulselib.PulseValueHistory</a></code></div><dl><dtclass="spec type"id="type-t"><ahref="#type-t"class="anchor"></a><code><spanclass="keyword">type</span> t</code></dt></dl><div><divclass="spec include"><divclass="doc"><dl><dtclass="spec value"id="val-compare"><ahref="#val-compare"class="anchor"></a><code><spanclass="keyword">val</span> compare : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span> int</code></dt><dtclass="spec value"id="val-equal"><ahref="#val-equal"class="anchor"></a><code><spanclass="keyword">val</span> equal : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dtclass="spec value"id="val-yojson_of_t"><ahref="#val-yojson_of_t"class="anchor"></a><code><spanclass="keyword">val</span> yojson_of_t : <ahref="index.html#type-t">t</a><span>-></span> Ppx_yojson_conv_lib.Yojson.Safe.t</code></dt></dl></div></div></div><dl><dtclass="spec value"id="val-true_"><ahref="#val-true_"class="anchor"></a><code><spanclass="keyword">val</span> true_ : <ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-false_"><ahref="#val-false_"class="anchor"></a><code><spanclass="keyword">val</span> false_ : <ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-pp"><ahref="#val-pp"class="anchor"></a><code><spanclass="keyword">val</span> pp : <ahref="index.html#module-F">F</a>.formatter <span>-></span><ahref="index.html#type-t">t</a><span>-></span> unit</code></dt></dl><dl><dtclass="spec type"id="type-new_eqs"><ahref="#type-new_eqs"class="anchor"></a><code><spanclass="keyword">type</span> new_eqs</code><code> = <ahref="../Pulselib/PulseFormula/index.html#type-new_eqs">Pulselib.PulseFormula.new_eqs</a></code></dt></dl><section><header><h3id="building-arithmetic-constraints"><ahref="#building-arithmetic-constraints"class="anchor"></a>Building arithmetic constraints</h3></header><dl><dtclass="spec value"id="val-and_nonnegative"><ahref="#val-and_nonnegative"class="anchor"></a><code><spanclass="keyword">val</span> and_nonnegative : <ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dd><p><code>and_nonnegative v phi</code> is <code>phi ∧ v≥0</code></p></dd></dl><dl><dtclass="spec value"id="val-and_positive"><ahref="#val-and_positive"class="anchor"></a><code><spanclass="keyword">val</span> and_positive : <ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dd><p><code>and_positive v phi</code> is <code>phi ∧ v>0</code></p></dd></dl><dl><dtclass="spec value"id="val-and_eq_int"><ahref="#val-and_eq_int"class="anchor"></a><code><spanclass="keyword">val</span> and_eq_int : <ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../IR/IntLit/index.html#type-t">IR.IntLit.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dd><p><code>and_eq_int v i phi</code> is <code>phi ∧ v=i</code></p></dd></dl><dl><dtclass="spec value"id="val-and_eq_vars"><ahref="#val-and_eq_vars"class="anchor"></a><code><spanclass="keyword">val</span> and_eq_vars : <ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dtclass="spec value"id="val-simplify"><ahref="#val-simplify"class="anchor"></a><code><spanclass="keyword">val</span> simplify : <ahref="../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span>can_be_pruned:<ahref="../Pulselib__PulseAbstractValue/index.html#module-Set">AbstractValue.Set</a>.t</span><span>-></span><span>keep:<ahref="../Pulselib__PulseAbstractValue/index.html#module-Set">AbstractValue.Set</a>.t</span><span>-></span><span>get_dynamic_type:<span>(<ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><span><ahref="../IR/Typ/index.html#type-t">IR.Typ.t</a> option</span>)</span></span><span>-></span><ahref="index.html#type-t">t</a><span>-></span><span><span>(<ahref="index.html#type-t">t</a> * <ahref="../Pulselib__PulseAbstractValue/index.html#module-Set">AbstractValue.Set</a>.t * <ahref="index.html#type-new_eqs">new_eqs</a>)</span><ahref="../Pulselib/PulseSatUnsat/index.html#type-t">SatUnsat.t</a></span></code></dt><dd><p><code>simplify ~can_be_pruned ~keep phi</code> attempts to get rid of as many variables in <code>fv phi</code> but not in <code>keep</code> as possible, and tries to eliminate variables not in <code>can_be_pruned</code> from the "pruned" part of the formula</p></dd></dl><dl><dtclass="spec value"id="val-and_callee"><ahref="#val-and_callee"class="anchor"></a><code><spanclass="keyword">val</span> and_callee : <span><span>(<ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a> * <ahref="../Pulselib/PulseValueHistory/index.html#type-t">ValueHistory.t</a>)</span><ahref="../Pulselib__PulseAbstractValue/index.html#module-Map">AbstractValue.Map</a>.t</span><span>-></span><ahref="index.html#type-t">t</a><span>-></span><span>callee:<ahref="index.html#type-t">t</a></span><span>-></span><span><span>(<ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a> * <ahref="../Pulselib/PulseValueHistory/index.html#type-t">ValueHistory.t</a>)</span><ahref="../Pulselib__PulseAbstractValue/index.html#module-Map">AbstractValue.Map</a>.t</span> * <ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt></dl></section><section><header><h3id="operations"><ahref="#operations"class="anchor"></a>Operations</h3></header><dl><dtclass="spec type"id="type-operand"><ahref="#type-operand"class="anchor"></a><code><spanclass="keyword">type</span> operand</code><code> = </code><tableclass="variant"><trid="type-operand.LiteralOperand"class="anchored"><tdclass="def constructor"><ahref="#type-operand.LiteralOperand"class="anchor"></a><code>| </code><code><spanclass="constructor">LiteralOperand</span><spanclass="keyword">of</span><ahref="../IR/IntLit/index.html#type-t">IR.IntLit.t</a></code></td></tr><trid="type-operand.AbstractValueOperand"class="anchored"><tdclass="def constructor"><ahref="#type-operand.AbstractValueOperand"class="anchor"></a><code>| </code><code><spanclass="constructor">AbstractValueOperand</span><spanclass="keyword">of</span><ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a></code></td></tr></table></dt></dl><div><divclass="spec include"><divclass="doc"><dl><dtclass="spec value"id="val-compare_operand"><ahref="#val-compare_operand"class="anchor"></a><code><spanclass="keyword">val</span> compare_operand : <ahref="index.html#type-operand">operand</a><span>-></span><ahref="index.html#type-operand">operand</a><span>-></span> int</code></dt></dl></div></div></div><dl><dtclass="spec value"id="val-pp_operand"><ahref="#val-pp_operand"class="anchor"></a><code><spanclass="keyword">val</span> pp_operand : <ahref="../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.Formatter.t <span>-></span><ahref="index.html#type-operand">operand</a><span>-></span> unit</code></dt><dtclass="spec value"id="val-eval_binop"><ahref="#val-eval_binop"class="anchor"></a><code><spanclass="keyword">val</span> eval_binop : <ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../IR/Binop/index.html#type-t">IR.Binop.t</a><span>-></span><ahref="index.html#type-operand">operand</a><span>-></span><ahref="index.html#type-operand">operand</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dtclass="spec value"id="val-eval_unop"><ahref="#val-eval_unop"class="anchor"></a><code><spanclass="keyword">val</span> eval_unop : <ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../IR/Unop/index.html#type-t">IR.Unop.t</a><span>-></span><ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dtclass="spec value"id="val-prune_binop"><ahref="#val-prune_binop"class="anchor"></a><code><spanclass="keyword">val</span> prune_binop : <span>negated:bool</span><span>-></span><ahref="../IR/Binop/index.html#type-t">IR.Binop.t</a><span>-></span><ahref="index.html#type-operand">operand</a><span>-></span><ahref="index.html#type-operand">operand</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dtclass="spec value"id="val-and_eq_instanceof"><ahref="#val-and_eq_instanceof"class="anchor"></a><code><spanclass="keyword">val</span> and_eq_instanceof : <ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../IR/Typ/index.html#type-t">IR.Typ.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt></dl></section><section><header><h3id="queries"><ahref="#queries"class="anchor"></a>Queries</h3></header><dl><dtclass="spec value"id="val-is_known_zero"><ahref="#val-is_known_zero"class="anchor"></a><code><spanclass="keyword">val</span> is_known_zero : <ahref="index.html#type-t">t</a><span>-></span><ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span> bool</code></dt><dd><p><code>is_known_zero phi t</code> returns <code>true</code> if <code>phi |- t = 0</code>, <code>false</code> if we don't know for sure</p></dd></dl><dl><dtclass="spec value"id="val-is_known_not_equal_zero"><ahref="#val-is_known_not_equal_zero"class="anchor"></a><code><spanclass="keyword">val</span> is_known_not_equal_zero : <ahref="index.html#type-t">t</a><span>-></span><ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span> bool</code></dt><dd><p><code>is_known_not_equal_zero phi t</code> returns <code>true</code> if <code>phi |- t != 0</code>, <code>false</code> if we don't know for sure</p></dd></dl><dl><dtclass="spec value"id="val-is_unsat_cheap"><ahref="#val-is_unsat_cheap"class="anchor"></a><code><spanclass="keyword">val</span> is_unsat_cheap : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dd><p>whether the state contains a contradiction, call this as often as you want</p></dd></dl><dl><dtclass="spec value"id="val-is_unsat_expensive"><ahref="#val-is_unsat_expensive"class="anchor"></a><code><spanclass="keyword">val</span> is_unsat_expensive : <ahref="../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span>get_dynamic_type:<span>(<ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><span><ahref="../IR/Typ/index.html#type-t">IR.Typ.t</a> option</span>)</span></span><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * bool * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dd><p>whether the state contains a contradiction, only call this when you absolutely have to</p></dd></dl><dl><dtclass="spec value"id="val-has_no_assumptions"><ahref="#val-has_no_assumptions"class="anchor"></a><code><spanclass="keyword">val</span> has_no_assumptions : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dd><p>whether the current path is independent of any calling context</p></dd></dl><dl><dtclass="spec value"id="val-get_known_var_repr"><ahref="#val-get_known_var_repr"class="anchor"></a><code><spanclass="keyword">val</span> get_known_var_repr : <ahref="index.html#type-t">t</a><span>-></span><ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a></code></dt><dd><p>get the canonical representative for the variable according to the equality relation in the "known" part of the formula</p></dd></dl><dl><dtclass="spec value"id="val-get_both_var_repr"><ahref="#val-get_both_var_repr"class="anchor"></a><code><spanclass="keyword">val</span> get_both_var_repr : <ahref="index.html#type-t">t</a><span>-></span><ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../Pulselib/PulseAbstractValue/index.html#type-t">AbstractValue.t</a></code></dt><dd><p>get the canonical representative for the variable according to the equality relation in the "both" (known + pruned) part of the formula</p></dd></dl></section></div></body></html>
