mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 03:35:38 -05:00
3 lines
No EOL
34 KiB
HTML
3 lines
No EOL
34 KiB
HTML
<!DOCTYPE html>
|
||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Solver_internal (sidekick-bin.Sidekick_smtlib.Process.Solver.Solver_internal)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.0.2"/><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-bin</a> » <a href="../../../index.html">Sidekick_smtlib</a> » <a href="../../index.html">Process</a> » <a href="../index.html">Solver</a> » Solver_internal</nav><header class="odoc-preamble"><h1>Module <code><span>Solver.Solver_internal</span></code></h1><p>Internal solver, available to theories.</p></header><nav class="odoc-toc"><ul><li><a href="#actions-for-the-theories">Actions for the theories</a></li><li><a href="#congruence-closure">Congruence Closure</a></li><li><a href="#simplifiers">Simplifiers</a></li><li><a href="#preprocessors">Preprocessors</a></li><li><a href="#hooks-for-the-theory">hooks for the theory</a></li><li><a href="#model-production">Model production</a></li></ul></nav><div class="odoc-content"><div class="odoc-spec"><div class="spec module" id="module-T" class="anchored"><a href="#module-T" class="anchor"></a><code><span><span class="keyword">module</span> </span><span>T</span><span> = <a href="../T/index.html">T</a></span></code></div></div><div class="odoc-spec"><div class="spec module" id="module-Lit" class="anchored"><a href="#module-Lit" class="anchor"></a><code><span><span class="keyword">module</span> </span><span>Lit</span><span> = <a href="../Lit/index.html">Lit</a></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-ty" class="anchored"><a href="#type-ty" class="anchor"></a><code><span><span class="keyword">type</span> ty</span><span> = <a href="../T/Ty/index.html#type-t">T.Ty.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-term" class="anchored"><a href="#type-term" class="anchor"></a><code><span><span class="keyword">type</span> term</span><span> = <a href="../T/Term/index.html#type-t">T.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-term_store" class="anchored"><a href="#type-term_store" class="anchor"></a><code><span><span class="keyword">type</span> term_store</span><span> = <a href="../T/Term/index.html#type-store">T.Term.store</a></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-ty_store" class="anchored"><a href="#type-ty_store" class="anchor"></a><code><span><span class="keyword">type</span> ty_store</span><span> = <a href="../T/Ty/index.html#type-store">T.Ty.store</a></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-clause_pool" class="anchored"><a href="#type-clause_pool" class="anchor"></a><code><span><span class="keyword">type</span> clause_pool</span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-proof" class="anchored"><a href="#type-proof" class="anchor"></a><code><span><span class="keyword">type</span> proof</span><span> = <a href="../index.html#type-proof">proof</a></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-proof_step" class="anchored"><a href="#type-proof_step" class="anchor"></a><code><span><span class="keyword">type</span> proof_step</span><span> = <a href="../index.html#type-proof_step">proof_step</a></span></code></div></div><div class="odoc-spec"><div class="spec module" id="module-P" class="anchored"><a href="#module-P" class="anchor"></a><code><span><span class="keyword">module</span> </span><span>P</span><span> = <a href="../P/index.html">P</a></span></code></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>Main type for a solver</p></div></div><div class="odoc-spec"><div class="spec type" id="type-solver" class="anchored"><a href="#type-solver" class="anchor"></a><code><span><span class="keyword">type</span> solver</span><span> = <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-tst" class="anchored"><a href="#val-tst" class="anchor"></a><code><span><span class="keyword">val</span> tst : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-term_store">term_store</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-ty_st" class="anchored"><a href="#val-ty_st" class="anchor"></a><code><span><span class="keyword">val</span> ty_st : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-ty_store">ty_store</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-stats" class="anchored"><a href="#val-stats" class="anchor"></a><code><span><span class="keyword">val</span> stats : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="../../../../../sidekick/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-proof" class="anchored"><a href="#val-proof" class="anchor"></a><code><span><span class="keyword">val</span> proof : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-proof">proof</a></span></code></div><div class="spec-doc"><p>Access the proof object</p></div></div><h4 id="actions-for-the-theories"><a href="#actions-for-the-theories" class="anchor"></a>Actions for the theories</h4><div class="odoc-spec"><div class="spec type" id="type-theory_actions" class="anchored"><a href="#type-theory_actions" class="anchor"></a><code><span><span class="keyword">type</span> theory_actions</span></code></div><div class="spec-doc"><p>Handle that the theories can use to perform actions.</p></div></div><div class="odoc-spec"><div class="spec type" id="type-lit" class="anchored"><a href="#type-lit" class="anchor"></a><code><span><span class="keyword">type</span> lit</span><span> = <a href="../Lit/index.html#type-t">Lit.t</a></span></code></div></div><h4 id="congruence-closure"><a href="#congruence-closure" class="anchor"></a>Congruence Closure</h4><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> </span><span><a href="CC/index.html">CC</a></span><span> : <a href="../../../../../sidekick/Sidekick_core/module-type-CC_S/index.html">Sidekick_core.CC_S</a> <span class="keyword">with</span> <span><span class="keyword">module</span> <a href="../../../../../sidekick/Sidekick_core/module-type-CC_S/T/index.html">T</a> = <a href="../T/index.html">T</a></span> <span class="keyword">and</span> <span><span class="keyword">module</span> <a href="../../../../../sidekick/Sidekick_core/module-type-CC_S/Lit/index.html">Lit</a> = <a href="../Lit/index.html">Lit</a></span> <span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../../../../sidekick/Sidekick_core/module-type-CC_S/index.html#type-proof">proof</a> = <a href="#type-proof">proof</a></span> <span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../../../../sidekick/Sidekick_core/module-type-CC_S/index.html#type-proof_step">proof_step</a> = <a href="#type-proof_step">proof_step</a></span> <span class="keyword">and</span> <span><span class="keyword">type</span>
|
||
<a href="../../../../../sidekick/Sidekick_core/module-type-CC_S/P/index.html#type-t">P.t</a> = <a href="#type-proof">proof</a></span> <span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../../../../sidekick/Sidekick_core/module-type-CC_S/P/index.html#type-lit">P.lit</a> = <a href="#type-lit">lit</a></span> <span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../../../../sidekick/Sidekick_core/module-type-CC_S/Actions/index.html#type-t">Actions.t</a> = <a href="#type-theory_actions">theory_actions</a></span></span></code></div><div class="spec-doc"><p>Congruence closure instance</p></div></div><div class="odoc-spec"><div class="spec value" id="val-cc" class="anchored"><a href="#val-cc" class="anchor"></a><code><span><span class="keyword">val</span> cc : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="CC/index.html#type-t">CC.t</a></span></code></div><div class="spec-doc"><p>Congruence closure for this solver</p></div></div><h4 id="simplifiers"><a href="#simplifiers" class="anchor"></a>Simplifiers</h4><div class="odoc-spec"><div class="spec module" id="module-Simplify" class="anchored"><a href="#module-Simplify" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Simplify/index.html">Simplify</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Simplify terms</p></div></div><div class="odoc-spec"><div class="spec type" id="type-simplify_hook" class="anchored"><a href="#type-simplify_hook" class="anchor"></a><code><span><span class="keyword">type</span> simplify_hook</span><span> = <a href="Simplify/index.html#type-hook">Simplify.hook</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-add_simplifier" class="anchored"><a href="#val-add_simplifier" class="anchor"></a><code><span><span class="keyword">val</span> add_simplifier : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="Simplify/index.html#type-hook">Simplify.hook</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Add a simplifier hook for preprocessing.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-simplify_t" class="anchored"><a href="#val-simplify_t" class="anchor"></a><code><span><span class="keyword">val</span> simplify_t : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> <span><span>(<a href="#type-term">term</a> * <a href="#type-proof_step">proof_step</a>)</span> option</span></span></code></div><div class="spec-doc"><p>Simplify input term, returns <code>Some u</code> if some simplification occurred.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-simp_t" class="anchored"><a href="#val-simp_t" class="anchor"></a><code><span><span class="keyword">val</span> simp_t : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> <a href="#type-term">term</a> * <span><a href="#type-proof_step">proof_step</a> option</span></span></code></div><div class="spec-doc"><p><code>simp_t si t</code> returns <code>u</code> even if no simplification occurred (in which case <code>t == u</code> syntactically). It emits <code>|- t=u</code>. (see <code>simplifier</code>)</p></div></div><h4 id="preprocessors"><a href="#preprocessors" class="anchor"></a>Preprocessors</h4><p>These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.</p><div class="odoc-spec"><div class="spec module-type" id="module-type-PREPROCESS_ACTS" class="anchored"><a href="#module-type-PREPROCESS_ACTS" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> </span><span><a href="module-type-PREPROCESS_ACTS/index.html">PREPROCESS_ACTS</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-preprocess_actions" class="anchored"><a href="#type-preprocess_actions" class="anchor"></a><code><span><span class="keyword">type</span> preprocess_actions</span><span> = <span>(<span class="keyword">module</span> <a href="module-type-PREPROCESS_ACTS/index.html">PREPROCESS_ACTS</a>)</span></span></code></div><div class="spec-doc"><p>Actions available to the preprocessor</p></div></div><div class="odoc-spec"><div class="spec type" id="type-preprocess_hook" class="anchored"><a href="#type-preprocess_hook" class="anchor"></a><code><span><span class="keyword">type</span> preprocess_hook</span><span> = <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-preprocess_actions">preprocess_actions</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> <span><span>(<a href="#type-term">term</a> * <span><a href="#type-proof_step">proof_step</a> <span class="xref-unresolved">Iter</span>.t</span>)</span> option</span></span></code></div><div class="spec-doc"><p>Given a term, try to preprocess it. Return <code>None</code> if it didn't change, or <code>Some (u)</code> if <code>t=u</code>. Can also add clauses to define new terms.</p><p>Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.</p><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">preprocess_actions</span> <p>actions available during preprocessing.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value" id="val-on_preprocess" class="anchored"><a href="#val-on_preprocess" class="anchor"></a><code><span><span class="keyword">val</span> on_preprocess : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-preprocess_hook">preprocess_hook</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Add a hook that will be called when terms are preprocessed</p></div></div><div class="odoc-spec"><div class="spec value" id="val-preprocess_acts_of_acts" class="anchored"><a href="#val-preprocess_acts_of_acts" class="anchor"></a><code><span><span class="keyword">val</span> preprocess_acts_of_acts : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <a href="#type-preprocess_actions">preprocess_actions</a></span></code></div><div class="spec-doc"><p>Obtain preprocessor actions, from theory actions</p></div></div><h4 id="hooks-for-the-theory"><a href="#hooks-for-the-theory" class="anchor"></a>hooks for the theory</h4><div class="odoc-spec"><div class="spec value" id="val-raise_conflict" class="anchored"><a href="#val-raise_conflict" class="anchor"></a><code><span><span class="keyword">val</span> raise_conflict : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><span><a href="#type-lit">lit</a> list</span> <span class="arrow">-></span></span> <span><a href="#type-proof_step">proof_step</a> <span class="arrow">-></span></span> <span class="type-var">'a</span></span></code></div><div class="spec-doc"><p>Give a conflict clause to the solver</p></div></div><div class="odoc-spec"><div class="spec value" id="val-push_decision" class="anchored"><a href="#val-push_decision" class="anchor"></a><code><span><span class="keyword">val</span> push_decision : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><a href="#type-lit">lit</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-propagate" class="anchored"><a href="#val-propagate" class="anchor"></a><code><span><span class="keyword">val</span> propagate : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><a href="#type-lit">lit</a> <span class="arrow">-></span></span> <span>reason:<span>(<span>unit <span class="arrow">-></span></span> <span><a href="#type-lit">lit</a> list</span> * <a href="#type-proof_step">proof_step</a>)</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Propagate a boolean using a unit clause. <code>expl => lit</code> must be a theory lemma, that is, a T-tautology</p></div></div><div class="odoc-spec"><div class="spec value" id="val-propagate_l" class="anchored"><a href="#val-propagate_l" class="anchor"></a><code><span><span class="keyword">val</span> propagate_l : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><a href="#type-lit">lit</a> <span class="arrow">-></span></span> <span><span><a href="#type-lit">lit</a> list</span> <span class="arrow">-></span></span> <span><a href="#type-proof_step">proof_step</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Propagate a boolean using a unit clause. <code>expl => lit</code> must be a theory lemma, that is, a T-tautology</p></div></div><div class="odoc-spec"><div class="spec value" id="val-add_clause_temp" class="anchored"><a href="#val-add_clause_temp" class="anchor"></a><code><span><span class="keyword">val</span> add_clause_temp : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><span><a href="#type-lit">lit</a> list</span> <span class="arrow">-></span></span> <span><a href="#type-proof_step">proof_step</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Add local clause to the SAT solver. This clause will be removed when the solver backtracks.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-add_clause_permanent" class="anchored"><a href="#val-add_clause_permanent" class="anchor"></a><code><span><span class="keyword">val</span> add_clause_permanent : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><span><a href="#type-lit">lit</a> list</span> <span class="arrow">-></span></span> <span><a href="#type-proof_step">proof_step</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Add toplevel clause to the SAT solver. This clause will not be backtracked.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-mk_lit" class="anchored"><a href="#val-mk_lit" class="anchor"></a><code><span><span class="keyword">val</span> mk_lit : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span>?sign:bool <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> <a href="#type-lit">lit</a></span></code></div><div class="spec-doc"><p>Create a literal. This automatically preprocesses the term.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-preprocess_term" class="anchored"><a href="#val-preprocess_term" class="anchor"></a><code><span><span class="keyword">val</span> preprocess_term : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-preprocess_actions">preprocess_actions</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> <a href="#type-term">term</a> * <span><a href="#type-proof_step">proof_step</a> option</span></span></code></div><div class="spec-doc"><p>Preprocess a term.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-add_lit" class="anchored"><a href="#val-add_lit" class="anchor"></a><code><span><span class="keyword">val</span> add_lit : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span>?default_pol:bool <span class="arrow">-></span></span> <span><a href="#type-lit">lit</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Add the given literal to the SAT solver, so it gets assigned a boolean value.</p><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">default_pol</span> <p>default polarity for the corresponding atom</p></li></ul></div></div><div class="odoc-spec"><div class="spec value" id="val-add_lit_t" class="anchored"><a href="#val-add_lit_t" class="anchor"></a><code><span><span class="keyword">val</span> add_lit_t : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span>?sign:bool <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Add the given (signed) bool term to the SAT solver, so it gets assigned a boolean value</p></div></div><div class="odoc-spec"><div class="spec value" id="val-cc_raise_conflict_expl" class="anchored"><a href="#val-cc_raise_conflict_expl" class="anchor"></a><code><span><span class="keyword">val</span> cc_raise_conflict_expl : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><a href="CC/Expl/index.html#type-t">CC.Expl.t</a> <span class="arrow">-></span></span> <span class="type-var">'a</span></span></code></div><div class="spec-doc"><p>Raise a conflict with the given congruence closure explanation. it must be a theory tautology that <code>expl ==> absurd</code>. To be used in theories.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-cc_find" class="anchored"><a href="#val-cc_find" class="anchor"></a><code><span><span class="keyword">val</span> cc_find : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="CC/N/index.html#type-t">CC.N.t</a> <span class="arrow">-></span></span> <a href="CC/N/index.html#type-t">CC.N.t</a></span></code></div><div class="spec-doc"><p>Find representative of the node</p></div></div><div class="odoc-spec"><div class="spec value" id="val-cc_are_equal" class="anchored"><a href="#val-cc_are_equal" class="anchor"></a><code><span><span class="keyword">val</span> cc_are_equal : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Are these two terms equal in the congruence closure?</p></div></div><div class="odoc-spec"><div class="spec value" id="val-cc_merge" class="anchored"><a href="#val-cc_merge" class="anchor"></a><code><span><span class="keyword">val</span> cc_merge : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><a href="CC/N/index.html#type-t">CC.N.t</a> <span class="arrow">-></span></span> <span><a href="CC/N/index.html#type-t">CC.N.t</a> <span class="arrow">-></span></span> <span><a href="CC/Expl/index.html#type-t">CC.Expl.t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Merge these two nodes in the congruence closure, 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-cc_merge_t" class="anchored"><a href="#val-cc_merge_t" class="anchor"></a><code><span><span class="keyword">val</span> cc_merge_t : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> <span><a href="CC/Expl/index.html#type-t">CC.Expl.t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Merge these two terms in the congruence closure, given this explanation. See <a href="#val-cc_merge"><code>cc_merge</code></a></p></div></div><div class="odoc-spec"><div class="spec value" id="val-cc_add_term" class="anchored"><a href="#val-cc_add_term" class="anchor"></a><code><span><span class="keyword">val</span> cc_add_term : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> <a href="CC/N/index.html#type-t">CC.N.t</a></span></code></div><div class="spec-doc"><p>Add/retrieve congruence closure node for this term. To be used in theories</p></div></div><div class="odoc-spec"><div class="spec value" id="val-cc_mem_term" class="anchored"><a href="#val-cc_mem_term" class="anchor"></a><code><span><span class="keyword">val</span> cc_mem_term : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Return <code>true</code> if the term is explicitly in the congruence closure. To be used in theories</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_cc_pre_merge" class="anchored"><a href="#val-on_cc_pre_merge" class="anchor"></a><code><span><span class="keyword">val</span> on_cc_pre_merge : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>(<span><a href="CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><a href="CC/N/index.html#type-t">CC.N.t</a> <span class="arrow">-></span></span> <span><a href="CC/N/index.html#type-t">CC.N.t</a> <span class="arrow">-></span></span> <span><a href="CC/Expl/index.html#type-t">CC.Expl.t</a> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Callback for when two classes containing data for this key are merged (called before)</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_cc_post_merge" class="anchored"><a href="#val-on_cc_post_merge" class="anchor"></a><code><span><span class="keyword">val</span> on_cc_post_merge : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>(<span><a href="CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><a href="CC/N/index.html#type-t">CC.N.t</a> <span class="arrow">-></span></span> <span><a href="CC/N/index.html#type-t">CC.N.t</a> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Callback for when two classes containing data for this key are merged (called after)</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_cc_new_term" class="anchored"><a href="#val-on_cc_new_term" class="anchor"></a><code><span><span class="keyword">val</span> on_cc_new_term : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>(<span><a href="CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <span><a href="CC/N/index.html#type-t">CC.N.t</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Callback to add data on terms when they are added to the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_cc_is_subterm" class="anchored"><a href="#val-on_cc_is_subterm" class="anchor"></a><code><span><span class="keyword">val</span> on_cc_is_subterm : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>(<span><a href="CC/N/index.html#type-t">CC.N.t</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Callback for when a term is a subterm of another term in the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_cc_conflict" class="anchored"><a href="#val-on_cc_conflict" class="anchor"></a><code><span><span class="keyword">val</span> on_cc_conflict : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>(<span><a href="CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <span>th:bool <span class="arrow">-></span></span> <span><span><a href="#type-lit">lit</a> list</span> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Callback called on every CC conflict</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_cc_propagate" class="anchored"><a href="#val-on_cc_propagate" class="anchor"></a><code><span><span class="keyword">val</span> on_cc_propagate : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>(<span><a href="CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <span><a href="#type-lit">lit</a> <span class="arrow">-></span></span> <span><span>(<span>unit <span class="arrow">-></span></span> <span><a href="#type-lit">lit</a> list</span> * <a href="#type-proof_step">proof_step</a>)</span> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Callback called on every CC propagation</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_partial_check" class="anchored"><a href="#val-on_partial_check" class="anchor"></a><code><span><span class="keyword">val</span> on_partial_check : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>(<span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><span><a href="#type-lit">lit</a> <span class="xref-unresolved">Iter</span>.t</span> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Register callbacked to be called with the slice of literals newly added on the trail.</p><p>This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_final_check" class="anchored"><a href="#val-on_final_check" class="anchor"></a><code><span><span class="keyword">val</span> on_final_check : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>(<span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-theory_actions">theory_actions</a> <span class="arrow">-></span></span> <span><span><a href="#type-lit">lit</a> <span class="xref-unresolved">Iter</span>.t</span> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Register callback to be called during the final check.</p><p>Must be complete (i.e. must raise a conflict if the set of literals is not satisfiable) and can be expensive. The function is given the whole trail.</p></div></div><h4 id="model-production"><a href="#model-production" class="anchor"></a>Model production</h4><div class="odoc-spec"><div class="spec type" id="type-model_hook" class="anchored"><a href="#type-model_hook" class="anchor"></a><code><span><span class="keyword">type</span> model_hook</span><span> = <span>recurse:<span>(<span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="CC/N/index.html#type-t">CC.N.t</a> <span class="arrow">-></span></span> <a href="#type-term">term</a>)</span> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="CC/N/index.html#type-t">CC.N.t</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> option</span></span></code></div><div class="spec-doc"><p>A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.</p><p>If no hook assigns a value to a class, a fake value is created for it.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-on_model_gen" class="anchored"><a href="#val-on_model_gen" class="anchor"></a><code><span><span class="keyword">val</span> on_model_gen : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-model_hook">model_hook</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Add a hook that will be called when a model is being produced</p></div></div></div></body></html> |