mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-24 18:36:43 -05:00
45 lines
No EOL
34 KiB
HTML
45 lines
No EOL
34 KiB
HTML
<!DOCTYPE html>
|
||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_cc (sidekick.Sidekick_cc)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.1.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick</a> » Sidekick_cc</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc</span></code></h1><p>Congruence Closure Implementation</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module-type" id="module-type-DYN_MONOID_PLUGIN" class="anchored"><a href="#module-type-DYN_MONOID_PLUGIN" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-DYN_MONOID_PLUGIN/index.html">DYN_MONOID_PLUGIN</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module-type" id="module-type-MONOID_PLUGIN_ARG" class="anchored"><a href="#module-type-MONOID_PLUGIN_ARG" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-MONOID_PLUGIN_ARG/index.html">MONOID_PLUGIN_ARG</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module-type" id="module-type-MONOID_PLUGIN_BUILDER" class="anchored"><a href="#module-type-MONOID_PLUGIN_BUILDER" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-MONOID_PLUGIN_BUILDER/index.html">MONOID_PLUGIN_BUILDER</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module" id="module-View" class="anchored"><a href="#module-View" class="anchor"></a><code><span><span class="keyword">module</span> View</span><span> = <a href="../Sidekick_core/CC_view/index.html">Sidekick_core.CC_view</a></span></code></div></div><div class="odoc-spec"><div class="spec module" id="module-E_node" class="anchored"><a href="#module-E_node" class="anchor"></a><code><span><span class="keyword">module</span> <a href="E_node/index.html">E_node</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>E-node.</p></div></div><div class="odoc-spec"><div class="spec module" id="module-Expl" class="anchored"><a href="#module-Expl" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Expl/index.html">Expl</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Explanations</p></div></div><div class="odoc-spec"><div class="spec module" id="module-Signature" class="anchored"><a href="#module-Signature" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Signature/index.html">Signature</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>A signature is a shallow term shape where immediate subterms are representative</p></div></div><div class="odoc-spec"><div class="spec module" id="module-Resolved_expl" class="anchored"><a href="#module-Resolved_expl" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Resolved_expl/index.html">Resolved_expl</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Resolved explanations.</p></div></div><div class="odoc-spec"><div class="spec module" id="module-Plugin" class="anchored"><a href="#module-Plugin" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Plugin/index.html">Plugin</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Congruence Closure Plugin</p></div></div><div class="odoc-spec"><div class="spec module" id="module-CC" class="anchored"><a href="#module-CC" class="anchor"></a><code><span><span class="keyword">module</span> <a href="CC/index.html">CC</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Main congruence closure signature.</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <span class="keyword">module</span> <span class="keyword">type</span> <span class="keyword">of</span> <span class="keyword">struct</span> <span class="keyword">include</span> <a href="CC/index.html">CC</a> <span class="keyword">end</span></span></code></summary><div class="odoc-spec"><div class="spec type" id="type-e_node" class="anchored"><a href="#type-e_node" class="anchor"></a><code><span><span class="keyword">type</span> e_node</span><span> = <a href="E_node/index.html#type-t">E_node.t</a></span></code></div><div class="spec-doc"><p>A node of the congruence closure</p></div></div><div class="odoc-spec"><div class="spec type" id="type-repr" class="anchored"><a href="#type-repr" class="anchor"></a><code><span><span class="keyword">type</span> repr</span><span> = <a href="E_node/index.html#type-t">E_node.t</a></span></code></div><div class="spec-doc"><p>Node that is currently a representative.</p></div></div><div class="odoc-spec"><div class="spec type" id="type-explanation" class="anchored"><a href="#type-explanation" class="anchor"></a><code><span><span class="keyword">type</span> explanation</span><span> = <a href="Expl/index.html#type-t">Expl.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-bitfield" class="anchored"><a href="#type-bitfield" class="anchor"></a><code><span><span class="keyword">type</span> bitfield</span></code></div><div class="spec-doc"><p>A field in the bitfield of this node. This should only be allocated when a theory is initialized.</p><p>Bitfields are accessed using preallocated keys. See <a href="#val-allocate_bitfield"><code>allocate_bitfield</code></a>.</p><p>All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.</p></div></div><div class="odoc-spec"><div class="spec type" id="type-t" class="anchored"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>The congruence closure object. It contains a fair amount of state and is mutable and backtrackable.</p></div></div><h4 id="accessors_2"><a href="#accessors_2" class="anchor"></a>Accessors</h4><div class="odoc-spec"><div class="spec value" id="val-term_store" class="anchored"><a href="#val-term_store" class="anchor"></a><code><span><span class="keyword">val</span> term_store : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="../Sidekick_core/Term/index.html#type-store">Sidekick_core.Term.store</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-proof_tracer" class="anchored"><a href="#val-proof_tracer" class="anchor"></a><code><span><span class="keyword">val</span> proof_tracer : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="../Sidekick_proof/Tracer/class-type-t/index.html">Sidekick_proof.Tracer.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-stat" class="anchored"><a href="#val-stat" class="anchor"></a><code><span><span class="keyword">val</span> stat : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="../Sidekick_util/Stat/index.html#type-t">Sidekick_util.Stat.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-find" class="anchored"><a href="#val-find" class="anchor"></a><code><span><span class="keyword">val</span> find : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-e_node">e_node</a> <span class="arrow">-></span></span> <a href="#type-repr">repr</a></span></code></div><div class="spec-doc"><p>Current representative</p></div></div><div class="odoc-spec"><div class="spec value" id="val-add_term" class="anchored"><a href="#val-add_term" class="anchor"></a><code><span><span class="keyword">val</span> add_term : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> <a href="#type-e_node">e_node</a></span></code></div><div class="spec-doc"><p>Add the Term.t to the congruence closure, if not present already. Will be backtracked.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-mem_term" class="anchored"><a href="#val-mem_term" class="anchor"></a><code><span><span class="keyword">val</span> mem_term : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Returns <code>true</code> if the Term.t is explicitly present in the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value" id="val-allocate_bitfield" class="anchored"><a href="#val-allocate_bitfield" class="anchor"></a><code><span><span class="keyword">val</span> allocate_bitfield : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span>descr:string <span class="arrow">-></span></span> <a href="#type-bitfield">bitfield</a></span></code></div><div class="spec-doc"><p>Allocate a new e_node field (see <code>E_node</code>.bitfield).</p><p>This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using <a href="#val-set_bitfield"><code>set_bitfield</code></a> for each class_ individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor Term.t in the class").</p><p>There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most <code>Sys</code>.int_size fields).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-get_bitfield" class="anchored"><a href="#val-get_bitfield" class="anchor"></a><code><span><span class="keyword">val</span> get_bitfield : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-bitfield">bitfield</a> <span class="arrow">-></span></span> <span><a href="E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Access the bit field of the given e_node</p></div></div><div class="odoc-spec"><div class="spec value" id="val-set_bitfield" class="anchored"><a href="#val-set_bitfield" class="anchor"></a><code><span><span class="keyword">val</span> set_bitfield : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-bitfield">bitfield</a> <span class="arrow">-></span></span> <span>bool <span class="arrow">-></span></span> <span><a href="E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Set the bitfield for the e_node. This will be backtracked. See <code>E_node</code>.bitfield.</p></div></div><div class="odoc-spec"><div class="spec type" id="type-propagation_reason" class="anchored"><a href="#type-propagation_reason" class="anchor"></a><code><span><span class="keyword">type</span> propagation_reason</span><span> =
|
||
<span>unit <span class="arrow">-></span></span>
|
||
<span><a href="../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> list</span> * <a href="../Sidekick_proof/Pterm/index.html#type-delayed">Sidekick_proof.Pterm.delayed</a></span></code></div></div><div class="odoc-spec"><div class="spec module" id="module-Handler_action" class="anchored"><a href="#module-Handler_action" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Handler_action/index.html">Handler_action</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Handler Actions</p></div></div><div class="odoc-spec"><div class="spec module" id="module-Result_action" class="anchored"><a href="#module-Result_action" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Result_action/index.html">Result_action</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Result Actions.</p></div></div><h4 id="events_2"><a href="#events_2" class="anchor"></a>Events</h4><p>Events triggered by the congruence closure, to which other plugins can subscribe.</p><div class="odoc-spec"><div class="spec value" id="val-on_pre_merge" class="anchored"><a href="#val-on_pre_merge" class="anchor"></a><code><span><span class="keyword">val</span> on_pre_merge :
|
||
<span><a href="#type-t">t</a> <span class="arrow">-></span></span>
|
||
<span><span>( <a href="#type-t">t</a> * <a href="E_node/index.html#type-t">E_node.t</a> * <a href="E_node/index.html#type-t">E_node.t</a> * <a href="Expl/index.html#type-t">Expl.t</a>, <a href="Handler_action/index.html#type-or_conflict">Handler_action.or_conflict</a> )</span>
|
||
<a href="../Sidekick_util/Event/index.html#type-t">Sidekick_util.Event.t</a></span></span></code></div><div class="spec-doc"><p>Events emitted by the congruence closure when something changes.</p><p><code>Ev_on_pre_merge acts n1 n2 expl</code> is emitted right before <code>n1</code> and <code>n2</code> are merged with explanation <code>expl</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_pre_merge2" class="anchored"><a href="#val-on_pre_merge2" class="anchor"></a><code><span><span class="keyword">val</span> on_pre_merge2 :
|
||
<span><a href="#type-t">t</a> <span class="arrow">-></span></span>
|
||
<span><span>( <a href="#type-t">t</a> * <a href="E_node/index.html#type-t">E_node.t</a> * <a href="E_node/index.html#type-t">E_node.t</a> * <a href="Expl/index.html#type-t">Expl.t</a>, <a href="Handler_action/index.html#type-or_conflict">Handler_action.or_conflict</a> )</span>
|
||
<a href="../Sidekick_util/Event/index.html#type-t">Sidekick_util.Event.t</a></span></span></code></div><div class="spec-doc"><p>Second phase of "on pre merge". This runs after <a href="#val-on_pre_merge"><code>on_pre_merge</code></a> and is used by Plugins. <b>NOTE</b>: Plugin state might be observed as already changed in these handlers.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_post_merge" class="anchored"><a href="#val-on_post_merge" class="anchor"></a><code><span><span class="keyword">val</span> on_post_merge :
|
||
<span><a href="#type-t">t</a> <span class="arrow">-></span></span>
|
||
<span><span>( <a href="#type-t">t</a> * <a href="E_node/index.html#type-t">E_node.t</a> * <a href="E_node/index.html#type-t">E_node.t</a>, <span><a href="Handler_action/index.html#type-t">Handler_action.t</a> list</span> )</span> <a href="../Sidekick_util/Event/index.html#type-t">Sidekick_util.Event.t</a></span></span></code></div><div class="spec-doc"><p><code>ev_on_post_merge acts n1 n2</code> is emitted right after <code>n1</code> and <code>n2</code> were merged. <code>find cc n1</code> and <code>find cc n2</code> will return the same E_node.t.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_new_term" class="anchored"><a href="#val-on_new_term" class="anchor"></a><code><span><span class="keyword">val</span> on_new_term :
|
||
<span><a href="#type-t">t</a> <span class="arrow">-></span></span>
|
||
<span><span>( <a href="#type-t">t</a> * <a href="E_node/index.html#type-t">E_node.t</a> * <a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a>, <span><a href="Handler_action/index.html#type-t">Handler_action.t</a> list</span> )</span>
|
||
<a href="../Sidekick_util/Event/index.html#type-t">Sidekick_util.Event.t</a></span></span></code></div><div class="spec-doc"><p><code>ev_on_new_term n t</code> is emitted whenever a new Term.t <code>t</code> is added to the congruence closure. Its E_node.t is <code>n</code>.</p></div></div><div class="odoc-spec"><div class="spec type" id="type-ev_on_conflict" class="anchored"><a href="#type-ev_on_conflict" class="anchor"></a><code><span><span class="keyword">type</span> ev_on_conflict</span><span> = </span><span>{</span></code><table><tr id="type-ev_on_conflict.cc" class="anchored"><td class="def record field"><a href="#type-ev_on_conflict.cc" class="anchor"></a><code><span>cc : <a href="#type-t">t</a>;</span></code></td></tr><tr id="type-ev_on_conflict.th" class="anchored"><td class="def record field"><a href="#type-ev_on_conflict.th" class="anchor"></a><code><span>th : bool;</span></code></td></tr><tr id="type-ev_on_conflict.c" class="anchored"><td class="def record field"><a href="#type-ev_on_conflict.c" class="anchor"></a><code><span>c : <span><a href="../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> list</span>;</span></code></td></tr></table><code><span>}</span></code></div><div class="spec-doc"><p>Event emitted when a conflict occurs in the CC.</p><p><code>th</code> is true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_conflict" class="anchored"><a href="#val-on_conflict" class="anchor"></a><code><span><span class="keyword">val</span> on_conflict : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>( <a href="#type-ev_on_conflict">ev_on_conflict</a>, unit )</span> <a href="../Sidekick_util/Event/index.html#type-t">Sidekick_util.Event.t</a></span></span></code></div><div class="spec-doc"><p><code>ev_on_conflict {th; c}</code> is emitted when the congruence closure triggers a conflict by asserting the tautology <code>c</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_propagate" class="anchored"><a href="#val-on_propagate" class="anchor"></a><code><span><span class="keyword">val</span> on_propagate :
|
||
<span><a href="#type-t">t</a> <span class="arrow">-></span></span>
|
||
<span><span>( <a href="#type-t">t</a> * <a href="../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> * <a href="#type-propagation_reason">propagation_reason</a>, <span><a href="Handler_action/index.html#type-t">Handler_action.t</a> list</span> )</span>
|
||
<a href="../Sidekick_util/Event/index.html#type-t">Sidekick_util.Event.t</a></span></span></code></div><div class="spec-doc"><p><code>ev_on_propagate Lit.t reason</code> is emitted whenever <code>reason() => Lit.t</code> is a propagated lemma. See <code>CC_ACTIONS</code>.propagate.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_is_subterm" class="anchored"><a href="#val-on_is_subterm" class="anchor"></a><code><span><span class="keyword">val</span> on_is_subterm :
|
||
<span><a href="#type-t">t</a> <span class="arrow">-></span></span>
|
||
<span><span>( <a href="#type-t">t</a> * <a href="E_node/index.html#type-t">E_node.t</a> * <a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a>, <span><a href="Handler_action/index.html#type-t">Handler_action.t</a> list</span> )</span>
|
||
<a href="../Sidekick_util/Event/index.html#type-t">Sidekick_util.Event.t</a></span></span></code></div><div class="spec-doc"><p><code>ev_on_is_subterm n t</code> is emitted when <code>n</code> is a subterm of another E_node.t for the first time. <code>t</code> is the Term.t corresponding to the E_node.t <code>n</code>. This can be useful for theory combination.</p></div></div><h4 id="misc_2"><a href="#misc_2" class="anchor"></a>Misc</h4><div class="odoc-spec"><div class="spec value" id="val-n_true" class="anchored"><a href="#val-n_true" class="anchor"></a><code><span><span class="keyword">val</span> n_true : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="E_node/index.html#type-t">E_node.t</a></span></code></div><div class="spec-doc"><p>Node for <code>true</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-n_false" class="anchored"><a href="#val-n_false" class="anchor"></a><code><span><span class="keyword">val</span> n_false : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="E_node/index.html#type-t">E_node.t</a></span></code></div><div class="spec-doc"><p>Node for <code>false</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-n_bool" class="anchored"><a href="#val-n_bool" class="anchor"></a><code><span><span class="keyword">val</span> n_bool : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span>bool <span class="arrow">-></span></span> <a href="E_node/index.html#type-t">E_node.t</a></span></code></div><div class="spec-doc"><p>Node for either true or false</p></div></div><div class="odoc-spec"><div class="spec value" id="val-set_as_lit" class="anchored"><a href="#val-set_as_lit" class="anchor"></a><code><span><span class="keyword">val</span> set_as_lit : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>map the given e_node to a literal.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-find_t" class="anchored"><a href="#val-find_t" class="anchor"></a><code><span><span class="keyword">val</span> find_t : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> <a href="#type-repr">repr</a></span></code></div><div class="spec-doc"><p>Current representative of the Term.t.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <span class="value">E_node.t_found</span> <p>if the Term.t is not already <code>add</code>-ed.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value" id="val-add_iter" class="anchored"><a href="#val-add_iter" class="anchor"></a><code><span><span class="keyword">val</span> add_iter : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span><a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="xref-unresolved">Iter</span>.t</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Add a sequence of terms to the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value" id="val-all_classes" class="anchored"><a href="#val-all_classes" class="anchor"></a><code><span><span class="keyword">val</span> all_classes : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-repr">repr</a> <span class="xref-unresolved">Iter</span>.t</span></span></code></div><div class="spec-doc"><p>All current classes. This is costly, only use if there is no other solution</p></div></div><div class="odoc-spec"><div class="spec value" id="val-explain_eq" class="anchored"><a href="#val-explain_eq" class="anchor"></a><code><span><span class="keyword">val</span> explain_eq : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <a href="Resolved_expl/index.html#type-t">Resolved_expl.t</a></span></code></div><div class="spec-doc"><p>Explain why the two nodes are equal. Fails if they are not, in an unspecified way.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-explain_expl" class="anchored"><a href="#val-explain_expl" class="anchor"></a><code><span><span class="keyword">val</span> explain_expl : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="Expl/index.html#type-t">Expl.t</a> <span class="arrow">-></span></span> <a href="Resolved_expl/index.html#type-t">Resolved_expl.t</a></span></code></div><div class="spec-doc"><p>Transform explanation into an actionable conflict clause</p></div></div><div class="odoc-spec"><div class="spec value" id="val-merge" class="anchored"><a href="#val-merge" class="anchor"></a><code><span><span class="keyword">val</span> merge : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="Expl/index.html#type-t">Expl.t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Merge these two nodes given this explanation. It must be a theory tautology that <code>expl ==> n1 = n2</code>. To be used in theories.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-merge_t" class="anchored"><a href="#val-merge_t" class="anchor"></a><code><span><span class="keyword">val</span> merge_t :
|
||
<span><a href="#type-t">t</a> <span class="arrow">-></span></span>
|
||
<span><a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><a href="Expl/index.html#type-t">Expl.t</a> <span class="arrow">-></span></span>
|
||
unit</span></code></div><div class="spec-doc"><p>Shortcut for adding + merging</p></div></div><h4 id="main-api_2"><a href="#main-api_2" class="anchor"></a>Main API</h4><div class="odoc-spec"><div class="spec value" id="val-assert_eq" class="anchored"><a href="#val-assert_eq" class="anchor"></a><code><span><span class="keyword">val</span> assert_eq :
|
||
<span><a href="#type-t">t</a> <span class="arrow">-></span></span>
|
||
<span><a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><a href="Expl/index.html#type-t">Expl.t</a> <span class="arrow">-></span></span>
|
||
unit</span></code></div><div class="spec-doc"><p>Assert that two terms are equal, using the given explanation.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-assert_lit" class="anchored"><a href="#val-assert_lit" class="anchor"></a><code><span><span class="keyword">val</span> assert_lit : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Given a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.</p><p>Useful for the theory combination or the SAT solver's functor</p></div></div><div class="odoc-spec"><div class="spec value" id="val-assert_lits" class="anchored"><a href="#val-assert_lits" class="anchor"></a><code><span><span class="keyword">val</span> assert_lits : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span><a href="../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> <span class="xref-unresolved">Iter</span>.t</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Addition of many literals</p></div></div><div class="odoc-spec"><div class="spec value" id="val-check" class="anchored"><a href="#val-check" class="anchor"></a><code><span><span class="keyword">val</span> check : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Result_action/index.html#type-or_conflict">Result_action.or_conflict</a></span></code></div><div class="spec-doc"><p>Perform all pending operations done via <a href="#val-assert_eq"><code>assert_eq</code></a>, <a href="#val-assert_lit"><code>assert_lit</code></a>, etc. Will use the <code>actions</code> to propagate literals, declare conflicts, etc.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-push_level" class="anchored"><a href="#val-push_level" class="anchor"></a><code><span><span class="keyword">val</span> push_level : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Push backtracking level</p></div></div><div class="odoc-spec"><div class="spec value" id="val-pop_levels" class="anchored"><a href="#val-pop_levels" class="anchor"></a><code><span><span class="keyword">val</span> pop_levels : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Restore to state <code>n</code> calls to <code>push_level</code> earlier. Used during backtracking.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-get_model" class="anchored"><a href="#val-get_model" class="anchor"></a><code><span><span class="keyword">val</span> get_model : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span><a href="E_node/index.html#type-t">E_node.t</a> <span class="xref-unresolved">Iter</span>.t</span> <span class="xref-unresolved">Iter</span>.t</span></span></code></div><div class="spec-doc"><p>get all the equivalence classes so they can be merged in the model</p></div></div><div class="odoc-spec"><div class="spec type" id="type-view_as_cc" class="anchored"><a href="#type-view_as_cc" class="anchor"></a><code><span><span class="keyword">type</span> view_as_cc</span><span> =
|
||
<span><a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><span>( <a href="../Sidekick_core_logic/Const/index.html#type-t">Sidekick_core.Const.t</a>, <a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a>, <span><a href="../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> list</span> )</span>
|
||
<a href="../Sidekick_core/CC_view/index.html#type-t">Sidekick_core.CC_view.t</a></span></span></code></div></div><div class="odoc-spec"><div class="spec module-type" id="module-type-ARG" class="anchored"><a href="#module-type-ARG" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-ARG/index.html">ARG</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Arguments to a congruence closure's implementation</p></div></div><div class="odoc-spec"><div class="spec module-type" id="module-type-BUILD" class="anchored"><a href="#module-type-BUILD" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-BUILD/index.html">BUILD</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module" id="module-Make" class="anchored"><a href="#module-Make" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Make/index.html">Make</a></span><span> (<a href="Make/argument-1-_/index.html">_</a> : <a href="module-type-ARG/index.html">ARG</a>) : <a href="module-type-BUILD/index.html">BUILD</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-create" class="anchored"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create :
|
||
<span><span>(<span class="keyword">module</span> <a href="module-type-ARG/index.html">ARG</a>)</span> <span class="arrow">-></span></span>
|
||
<span>?stat:<a href="../Sidekick_util/Stat/index.html#type-t">Sidekick_util.Stat.t</a> <span class="arrow">-></span></span>
|
||
<span>?size:<span>[ `Small <span>| `Big</span> ]</span> <span class="arrow">-></span></span>
|
||
<span><a href="../Sidekick_core/Term/index.html#type-store">Sidekick_core.Term.store</a> <span class="arrow">-></span></span>
|
||
<span><a href="../Sidekick_proof/Tracer/class-type-t/index.html">Sidekick_proof.Tracer.t</a> <span class="arrow">-></span></span>
|
||
<a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Create a new congruence closure.</p><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">term_store</span> <p>used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value" id="val-create_default" class="anchored"><a href="#val-create_default" class="anchor"></a><code><span><span class="keyword">val</span> create_default :
|
||
<span>?stat:<a href="../Sidekick_util/Stat/index.html#type-t">Sidekick_util.Stat.t</a> <span class="arrow">-></span></span>
|
||
<span>?size:<span>[ `Small <span>| `Big</span> ]</span> <span class="arrow">-></span></span>
|
||
<span><a href="../Sidekick_core/Term/index.html#type-store">Sidekick_core.Term.store</a> <span class="arrow">-></span></span>
|
||
<span><a href="../Sidekick_proof/Tracer/class-type-t/index.html">Sidekick_proof.Tracer.t</a> <span class="arrow">-></span></span>
|
||
<a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Same as <a href="#val-create"><code>create</code></a> but with the default CC view</p></div></div></details></div></div></body></html> |