mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 11:45:41 -05:00
2 lines
No EOL
26 KiB
HTML
2 lines
No EOL
26 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 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">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><h1>Module <code>Solver.Solver_internal</code></h1><p>Internal solver, available to theories.</p><nav class="toc"><ul><li><a href="#actions-for-the-theories">Actions for the theories</a></li><li><a href="#proof-helpers">Proof helpers</a></li><li><a href="#congruence-closure">Congruence Closure</a></li><li><a href="#simplifiers">Simplifiers</a></li><li><a href="#hooks-for-the-theory">hooks for the theory</a></li><li><a href="#preprocessors">Preprocessors</a></li><li><a href="#model-production">Model production</a></li></ul></nav></header><div class="spec module" id="module-T"><a href="#module-T" class="anchor"></a><code><span class="keyword">module</span> T = <a href="../index.html#module-T">T</a></code></div><div class="spec module" id="module-P"><a href="#module-P" class="anchor"></a><code><span class="keyword">module</span> P = <a href="../index.html#module-P">P</a></code></div><dl><dt class="spec type" id="type-ty"><a href="#type-ty" class="anchor"></a><code><span class="keyword">type</span> ty</code><code> = <a href="T/Ty/index.html#type-t">T.Ty.t</a></code></dt><dt class="spec type" id="type-term"><a href="#type-term" class="anchor"></a><code><span class="keyword">type</span> term</code><code> = <a href="T/Term/index.html#type-t">T.Term.t</a></code></dt><dt class="spec type" id="type-term_store"><a href="#type-term_store" class="anchor"></a><code><span class="keyword">type</span> term_store</code><code> = <a href="T/Term/index.html#type-store">T.Term.store</a></code></dt><dt class="spec type" id="type-ty_store"><a href="#type-ty_store" class="anchor"></a><code><span class="keyword">type</span> ty_store</code><code> = <a href="T/Ty/index.html#type-store">T.Ty.store</a></code></dt><dt class="spec type" id="type-proof"><a href="#type-proof" class="anchor"></a><code><span class="keyword">type</span> proof</code><code> = <a href="P/index.html#type-t">P.t</a></code></dt><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><h4 id="main-type-for-a-solver"><a href="#main-type-for-a-solver" class="anchor"></a>Main type for a solver</h4></dd></dl><dl><dt class="spec type" id="type-solver"><a href="#type-solver" class="anchor"></a><code><span class="keyword">type</span> solver</code><code> = <a href="index.html#type-t">t</a></code></dt></dl><dl><dt class="spec value" id="val-tst"><a href="#val-tst" class="anchor"></a><code><span class="keyword">val</span> tst : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-term_store">term_store</a></code></dt><dt class="spec value" id="val-ty_st"><a href="#val-ty_st" class="anchor"></a><code><span class="keyword">val</span> ty_st : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-ty_store">ty_store</a></code></dt><dt class="spec value" id="val-stats"><a href="#val-stats" class="anchor"></a><code><span class="keyword">val</span> stats : <a href="index.html#type-t">t</a> <span>-></span> <a href="../../../../../sidekick/Sidekick_util/Stat/index.html#type-t">Sidekick_util.Stat.t</a></code></dt></dl><section><header><h4 id="actions-for-the-theories"><a href="#actions-for-the-theories" class="anchor"></a>Actions for the theories</h4></header><dl><dt class="spec type" id="type-actions"><a href="#type-actions" class="anchor"></a><code><span class="keyword">type</span> actions</code></dt><dd><p>Handle that the theories can use to perform actions.</p></dd></dl><dl><dt class="spec module" id="module-Lit"><a href="#module-Lit" class="anchor"></a><code><span class="keyword">module</span> Lit = <a href="../index.html#module-Lit">Lit</a></code></dt><dd></dd></dl><dl><dt class="spec type" id="type-lit"><a href="#type-lit" class="anchor"></a><code><span class="keyword">type</span> lit</code><code> = <a href="Lit/index.html#type-t">Lit.t</a></code></dt></dl></section><section><header><h4 id="proof-helpers"><a href="#proof-helpers" class="anchor"></a>Proof helpers</h4></header><dl><dt class="spec value" id="val-define_const"><a href="#val-define_const" class="anchor"></a><code><span class="keyword">val</span> define_const : <a href="index.html#type-t">t</a> <span>-></span> <span>const:<a href="index.html#type-term">term</a></span> <span>-></span> <span>rhs:<a href="index.html#type-term">term</a></span> <span>-></span> unit</code></dt><dd><p><code>define_const si ~const ~rhs</code> adds the definition <code>const := rhs</code> to the (future) proof. <code>const</code> should be a fresh constant that occurs nowhere else, and <code>rhs</code> a term defined without <code>const</code>.</p></dd></dl></section><section><header><h4 id="congruence-closure"><a href="#congruence-closure" class="anchor"></a>Congruence Closure</h4></header><dl><dt class="spec module" id="module-CC"><a href="#module-CC" class="anchor"></a><code><span class="keyword">module</span> <a href="CC/index.html">CC</a> : <a href="../../../../../sidekick/Sidekick_core/index.html#module-type-CC_S">Sidekick_core.CC_S</a> <span class="keyword">with</span> <span class="keyword">module</span> <a href="../../../../../sidekick/Sidekick_core/module-type-CC_S/T/index.html">T</a> = <a href="index.html#module-T">T</a> <span class="keyword">and</span> <span class="keyword">module</span> <a href="../../../../../sidekick/Sidekick_core/module-type-CC_S/P/index.html">P</a> = <a href="index.html#module-P">P</a> <span class="keyword">and</span> <span class="keyword">module</span> <a href="../../../../../sidekick/Sidekick_core/module-type-CC_S/Lit/index.html">Lit</a> = <a href="index.html#module-Lit">Lit</a> <span class="keyword">and</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="index.html#type-actions">actions</a></code></dt><dd><p>Congruence closure instance</p></dd></dl><dl><dt class="spec value" id="val-cc"><a href="#val-cc" class="anchor"></a><code><span class="keyword">val</span> cc : <a href="index.html#type-t">t</a> <span>-></span> <a href="CC/index.html#type-t">CC.t</a></code></dt><dd><p>Congruence closure for this solver</p></dd></dl></section><section><header><h4 id="simplifiers"><a href="#simplifiers" class="anchor"></a>Simplifiers</h4></header><dl><dt class="spec module" id="module-Simplify"><a href="#module-Simplify" class="anchor"></a><code><span class="keyword">module</span> <a href="Simplify/index.html">Simplify</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>Simplify terms</p></dd></dl><dl><dt class="spec type" id="type-simplify_hook"><a href="#type-simplify_hook" class="anchor"></a><code><span class="keyword">type</span> simplify_hook</code><code> = <a href="Simplify/index.html#type-hook">Simplify.hook</a></code></dt></dl><dl><dt class="spec value" id="val-add_simplifier"><a href="#val-add_simplifier" class="anchor"></a><code><span class="keyword">val</span> add_simplifier : <a href="index.html#type-t">t</a> <span>-></span> <a href="Simplify/index.html#type-hook">Simplify.hook</a> <span>-></span> unit</code></dt><dd><p>Add a simplifier hook for preprocessing.</p></dd></dl><dl><dt class="spec value" id="val-simplifier"><a href="#val-simplifier" class="anchor"></a><code><span class="keyword">val</span> simplifier : <a href="index.html#type-t">t</a> <span>-></span> <a href="Simplify/index.html#type-t">Simplify.t</a></code></dt><dt class="spec value" id="val-simplify_t"><a href="#val-simplify_t" class="anchor"></a><code><span class="keyword">val</span> simplify_t : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <span><span>(<a href="index.html#type-term">term</a> * <a href="index.html#type-proof">proof</a>)</span> option</span></code></dt><dd><p>Simplify input term, returns <code>Some (u, |- t=u)</code> if some simplification occurred.</p></dd></dl><dl><dt class="spec value" id="val-simp_t"><a href="#val-simp_t" class="anchor"></a><code><span class="keyword">val</span> simp_t : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-term">term</a> * <a href="index.html#type-proof">proof</a></code></dt><dd><p><code>simp_t si t</code> returns <code>u, |- t=u</code> even if no simplification occurred (in which case <code>t == u</code> syntactically). (see <a href="index.html#val-simplifier"><code>simplifier</code></a>)</p></dd></dl></section><section><header><h4 id="hooks-for-the-theory"><a href="#hooks-for-the-theory" class="anchor"></a>hooks for the theory</h4></header><dl><dt class="spec value" id="val-raise_conflict"><a href="#val-raise_conflict" class="anchor"></a><code><span class="keyword">val</span> raise_conflict : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <span><a href="index.html#type-lit">lit</a> list</span> <span>-></span> <a href="index.html#type-proof">proof</a> <span>-></span> <span class="type-var">'a</span></code></dt><dd><p>Give a conflict clause to the solver</p></dd></dl><dl><dt class="spec value" id="val-push_decision"><a href="#val-push_decision" class="anchor"></a><code><span class="keyword">val</span> push_decision : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <a href="index.html#type-lit">lit</a> <span>-></span> unit</code></dt><dd><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></dd></dl><dl><dt class="spec value" id="val-propagate"><a href="#val-propagate" class="anchor"></a><code><span class="keyword">val</span> propagate : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <a href="index.html#type-lit">lit</a> <span>-></span> <span>reason:<span>(unit <span>-></span> <span><a href="index.html#type-lit">lit</a> list</span> * <a href="index.html#type-proof">proof</a>)</span></span> <span>-></span> unit</code></dt><dd><p>Propagate a boolean using a unit clause. <code>expl => lit</code> must be a theory lemma, that is, a T-tautology</p></dd></dl><dl><dt class="spec value" id="val-propagate_l"><a href="#val-propagate_l" class="anchor"></a><code><span class="keyword">val</span> propagate_l : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <a href="index.html#type-lit">lit</a> <span>-></span> <span><a href="index.html#type-lit">lit</a> list</span> <span>-></span> <a href="index.html#type-proof">proof</a> <span>-></span> unit</code></dt><dd><p>Propagate a boolean using a unit clause. <code>expl => lit</code> must be a theory lemma, that is, a T-tautology</p></dd></dl><dl><dt class="spec value" id="val-add_clause_temp"><a href="#val-add_clause_temp" class="anchor"></a><code><span class="keyword">val</span> add_clause_temp : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <span><a href="index.html#type-lit">lit</a> list</span> <span>-></span> <a href="index.html#type-proof">proof</a> <span>-></span> unit</code></dt><dd><p>Add local clause to the SAT solver. This clause will be removed when the solver backtracks.</p></dd></dl><dl><dt class="spec value" id="val-add_clause_permanent"><a href="#val-add_clause_permanent" class="anchor"></a><code><span class="keyword">val</span> add_clause_permanent : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <span><a href="index.html#type-lit">lit</a> list</span> <span>-></span> <a href="index.html#type-proof">proof</a> <span>-></span> unit</code></dt><dd><p>Add toplevel clause to the SAT solver. This clause will not be backtracked.</p></dd></dl><dl><dt class="spec value" id="val-mk_lit"><a href="#val-mk_lit" class="anchor"></a><code><span class="keyword">val</span> mk_lit : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <span>?⁠sign:bool</span> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-lit">lit</a></code></dt><dd><p>Create a literal. This automatically preprocesses the term.</p></dd></dl><dl><dt class="spec value" id="val-preprocess_term"><a href="#val-preprocess_term" class="anchor"></a><code><span class="keyword">val</span> preprocess_term : <a href="index.html#type-t">t</a> <span>-></span> <span>add_clause:<span>(<span><a href="Lit/index.html#type-t">Lit.t</a> list</span> <span>-></span> <a href="index.html#type-proof">proof</a> <span>-></span> unit)</span></span> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-term">term</a> * <a href="index.html#type-proof">proof</a></code></dt><dd><p>Preprocess a term.</p></dd></dl><dl><dt class="spec value" id="val-add_lit"><a href="#val-add_lit" class="anchor"></a><code><span class="keyword">val</span> add_lit : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <a href="index.html#type-lit">lit</a> <span>-></span> unit</code></dt><dd><p>Add the given literal to the SAT solver, so it gets assigned a boolean value</p></dd></dl><dl><dt class="spec value" id="val-add_lit_t"><a href="#val-add_lit_t" class="anchor"></a><code><span class="keyword">val</span> add_lit_t : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <span>?⁠sign:bool</span> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> unit</code></dt><dd><p>Add the given (signed) bool term to the SAT solver, so it gets assigned a boolean value</p></dd></dl><dl><dt class="spec value" id="val-cc_raise_conflict_expl"><a href="#val-cc_raise_conflict_expl" class="anchor"></a><code><span class="keyword">val</span> cc_raise_conflict_expl : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <a href="CC/Expl/index.html#type-t">CC.Expl.t</a> <span>-></span> <span class="type-var">'a</span></code></dt><dd><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></dd></dl><dl><dt class="spec value" id="val-cc_find"><a href="#val-cc_find" class="anchor"></a><code><span class="keyword">val</span> cc_find : <a href="index.html#type-t">t</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a></code></dt><dd><p>Find representative of the node</p></dd></dl><dl><dt class="spec value" id="val-cc_are_equal"><a href="#val-cc_are_equal" class="anchor"></a><code><span class="keyword">val</span> cc_are_equal : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> bool</code></dt><dd><p>Are these two terms equal in the congruence closure?</p></dd></dl><dl><dt class="spec value" id="val-cc_merge"><a href="#val-cc_merge" class="anchor"></a><code><span class="keyword">val</span> cc_merge : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a> <span>-></span> <a href="CC/Expl/index.html#type-t">CC.Expl.t</a> <span>-></span> unit</code></dt><dd><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></dd></dl><dl><dt class="spec value" id="val-cc_merge_t"><a href="#val-cc_merge_t" class="anchor"></a><code><span class="keyword">val</span> cc_merge_t : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="CC/Expl/index.html#type-t">CC.Expl.t</a> <span>-></span> unit</code></dt><dd><p>Merge these two terms in the congruence closure, given this explanation. See <a href="index.html#val-cc_merge"><code>cc_merge</code></a></p></dd></dl><dl><dt class="spec value" id="val-cc_add_term"><a href="#val-cc_add_term" class="anchor"></a><code><span class="keyword">val</span> cc_add_term : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a></code></dt><dd><p>Add/retrieve congruence closure node for this term. To be used in theories</p></dd></dl><dl><dt class="spec value" id="val-cc_mem_term"><a href="#val-cc_mem_term" class="anchor"></a><code><span class="keyword">val</span> cc_mem_term : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> bool</code></dt><dd><p>Return <code>true</code> if the term is explicitly in the congruence closure. To be used in theories</p></dd></dl><dl><dt class="spec value" id="val-on_cc_pre_merge"><a href="#val-on_cc_pre_merge" class="anchor"></a><code><span class="keyword">val</span> on_cc_pre_merge : <a href="index.html#type-t">t</a> <span>-></span> <span>(<a href="CC/index.html#type-t">CC.t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a> <span>-></span> <a href="CC/Expl/index.html#type-t">CC.Expl.t</a> <span>-></span> unit)</span> <span>-></span> unit</code></dt><dd><p>Callback for when two classes containing data for this key are merged (called before)</p></dd></dl><dl><dt class="spec value" id="val-on_cc_post_merge"><a href="#val-on_cc_post_merge" class="anchor"></a><code><span class="keyword">val</span> on_cc_post_merge : <a href="index.html#type-t">t</a> <span>-></span> <span>(<a href="CC/index.html#type-t">CC.t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a> <span>-></span> unit)</span> <span>-></span> unit</code></dt><dd><p>Callback for when two classes containing data for this key are merged (called after)</p></dd></dl><dl><dt class="spec value" id="val-on_cc_new_term"><a href="#val-on_cc_new_term" class="anchor"></a><code><span class="keyword">val</span> on_cc_new_term : <a href="index.html#type-t">t</a> <span>-></span> <span>(<a href="CC/index.html#type-t">CC.t</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> unit)</span> <span>-></span> unit</code></dt><dd><p>Callback to add data on terms when they are added to the congruence closure</p></dd></dl><dl><dt class="spec value" id="val-on_cc_is_subterm"><a href="#val-on_cc_is_subterm" class="anchor"></a><code><span class="keyword">val</span> on_cc_is_subterm : <a href="index.html#type-t">t</a> <span>-></span> <span>(<a href="CC/N/index.html#type-t">CC.N.t</a> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> unit)</span> <span>-></span> unit</code></dt><dd><p>Callback for when a term is a subterm of another term in the congruence closure</p></dd></dl><dl><dt class="spec value" id="val-on_cc_conflict"><a href="#val-on_cc_conflict" class="anchor"></a><code><span class="keyword">val</span> on_cc_conflict : <a href="index.html#type-t">t</a> <span>-></span> <span>(<a href="CC/index.html#type-t">CC.t</a> <span>-></span> <span>th:bool</span> <span>-></span> <span><a href="index.html#type-lit">lit</a> list</span> <span>-></span> unit)</span> <span>-></span> unit</code></dt><dd><p>Callback called on every CC conflict</p></dd></dl><dl><dt class="spec value" id="val-on_cc_propagate"><a href="#val-on_cc_propagate" class="anchor"></a><code><span class="keyword">val</span> on_cc_propagate : <a href="index.html#type-t">t</a> <span>-></span> <span>(<a href="CC/index.html#type-t">CC.t</a> <span>-></span> <a href="index.html#type-lit">lit</a> <span>-></span> <span>(unit <span>-></span> <span><a href="index.html#type-lit">lit</a> list</span> * <a href="index.html#type-proof">proof</a>)</span> <span>-></span> unit)</span> <span>-></span> unit</code></dt><dd><p>Callback called on every CC propagation</p></dd></dl><dl><dt class="spec value" id="val-on_partial_check"><a href="#val-on_partial_check" class="anchor"></a><code><span class="keyword">val</span> on_partial_check : <a href="index.html#type-t">t</a> <span>-></span> <span>(<a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <span><a href="index.html#type-lit">lit</a> Iter.t</span> <span>-></span> unit)</span> <span>-></span> unit</code></dt><dd><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></dd></dl><dl><dt class="spec value" id="val-on_final_check"><a href="#val-on_final_check" class="anchor"></a><code><span class="keyword">val</span> on_final_check : <a href="index.html#type-t">t</a> <span>-></span> <span>(<a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-actions">actions</a> <span>-></span> <span><a href="index.html#type-lit">lit</a> Iter.t</span> <span>-></span> unit)</span> <span>-></span> unit</code></dt><dd><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></dd></dl></section><section><header><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></header><dl><dt class="spec type" id="type-preprocess_hook"><a href="#type-preprocess_hook" class="anchor"></a><code><span class="keyword">type</span> preprocess_hook</code><code> = <a href="index.html#type-t">t</a> <span>-></span> <span>mk_lit:<span>(<a href="index.html#type-term">term</a> <span>-></span> <a href="index.html#type-lit">lit</a>)</span></span> <span>-></span> <span>add_clause:<span>(<span><a href="index.html#type-lit">lit</a> list</span> <span>-></span> <a href="index.html#type-proof">proof</a> <span>-></span> unit)</span></span> <span>-></span> <a href="index.html#type-term">term</a> <span>-></span> <span><span>(<a href="index.html#type-term">term</a> * <a href="index.html#type-proof">proof</a>)</span> option</span></code></dt><dd><p>Given a term, try to preprocess it. Return <code>None</code> if it didn't change, or <code>Some (u,p)</code> if <code>t=u</code> and <code>p</code> is a proof of <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><dl><dt>parameter mk_lit</dt><dd><p>creates a new literal for a boolean term.</p></dd></dl><dl><dt>parameter add_clause</dt><dd><p>pushes a new clause into the SAT solver.</p></dd></dl></dd></dl><dl><dt class="spec value" id="val-on_preprocess"><a href="#val-on_preprocess" class="anchor"></a><code><span class="keyword">val</span> on_preprocess : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-preprocess_hook">preprocess_hook</a> <span>-></span> unit</code></dt><dd><p>Add a hook that will be called when terms are preprocessed</p></dd></dl></section><section><header><h4 id="model-production"><a href="#model-production" class="anchor"></a>Model production</h4></header><dl><dt class="spec type" id="type-model_hook"><a href="#type-model_hook" class="anchor"></a><code><span class="keyword">type</span> model_hook</code><code> = <span>recurse:<span>(<a href="index.html#type-t">t</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a> <span>-></span> <a href="index.html#type-term">term</a>)</span></span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="CC/N/index.html#type-t">CC.N.t</a> <span>-></span> <span><a href="index.html#type-term">term</a> option</span></code></dt><dd><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></dd></dl><dl><dt class="spec value" id="val-on_model_gen"><a href="#val-on_model_gen" class="anchor"></a><code><span class="keyword">val</span> on_model_gen : <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-model_hook">model_hook</a> <span>-></span> unit</code></dt><dd><p>Add a hook that will be called when a model is being produced</p></dd></dl></section></div></body></html> |