+ <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_let"><a href="#val-mk_let" class="anchor"></a><code><span><span class="keyword">val</span> mk_let : <span><a href="../Var/index.html#type-t">Var.t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-skolemize"><a href="#val-skolemize" class="anchor"></a><code><span><span class="keyword">val</span> skolemize : <span><a href="#type-quantified">quantified</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-elim_let"><a href="#val-elim_let" class="anchor"></a><code><span><span class="keyword">val</span> elim_let : <span><span class="label">recursive</span>:bool <span class="arrow">-></span></span> <span><a href="#type-letin">letin</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-elim_iff"><a href="#val-elim_iff" class="anchor"></a><code><span><span class="keyword">val</span> elim_iff : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span class="label">with_conj</span>:bool <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-purify_form"><a href="#val-purify_form" class="anchor"></a><code><span><span class="keyword">val</span> purify_form : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-gformula"><a href="#type-gformula" class="anchor"></a><code><span><span class="keyword">type</span> gformula</span><span> = </span><span>{</span></code><ol><li id="type-gformula.ff" class="def record field anchored"><a href="#type-gformula.ff" class="anchor"></a><code><span>ff : <a href="#type-t">t</a>;</span></code></li><li id="type-gformula.nb_reductions" class="def record field anchored"><a href="#type-gformula.nb_reductions" class="anchor"></a><code><span>nb_reductions : int;</span></code></li><li id="type-gformula.trigger_depth" class="def record field anchored"><a href="#type-gformula.trigger_depth" class="anchor"></a><code><span>trigger_depth : int;</span></code></li><li id="type-gformula.age" class="def record field anchored"><a href="#type-gformula.age" class="anchor"></a><code><span>age : int;</span></code></li><li id="type-gformula.lem" class="def record field anchored"><a href="#type-gformula.lem" class="anchor"></a><code><span>lem : <span><a href="#type-t">t</a> option</span>;</span></code></li><li id="type-gformula.origin_name" class="def record field anchored"><a href="#type-gformula.origin_name" class="anchor"></a><code><span>origin_name : string;</span></code></li><li id="type-gformula.from_terms" class="def record field anchored"><a href="#type-gformula.from_terms" class="anchor"></a><code><span>from_terms : <span><a href="#type-t">t</a> list</span>;</span></code></li><li id="type-gformula.mf" class="def record field anchored"><a href="#type-gformula.mf" class="anchor"></a><code><span>mf : bool;</span></code></li><li id="type-gformula.gf" class="def record field anchored"><a href="#type-gformula.gf" class="anchor"></a><code><span>gf : bool;</span></code></li><li id="type-gformula.gdist" class="def record field anchored"><a href="#type-gformula.gdist" class="anchor"></a><code><span>gdist : int;</span></code></li><li id="type-gformula.hdist" class="def record field anchored"><a href="#type-gformula.hdist" class="anchor"></a><code><span>hdist : int;</span></code></li><li id="type-gformula.theory_elim" class="def record field anchored"><a href="#type-gformula.theory_elim" class="anchor"></a><code><span>theory_elim : bool;</span></code></li></ol><code><span>}</span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-th_elt"><a href="#type-th_elt" class="anchor"></a><code><span><span class="keyword">type</span> th_elt</span><span> = </span><span>{</span></code><ol><li id="type-th_elt.th_name" class="def record field anchored"><a href="#type-th_elt.th_name" class="anchor"></a><code><span>th_name : string;</span></code></li><li id="type-th_elt.ax_name" class="def record field anchored"><a href="#type-th_elt.ax_name" class="anchor"></a><code><span>ax_name : string;</span></code></li><li id="type-th_elt.ax_form" class="def record field anchored"><a href="#type-th_elt.ax_form" class="anchor"></a><code><span>ax_form : <a href="#type-t">t</a>;</span></code></li><li id="type-th_elt.extends" class="def record field anchored"><a href="#type-th_elt.extends" class="anchor"></a><code><span>extends : <a href="../Util/index.html#type-theories_extensions">Util.theories_extensions</a>;</span></code></li><li id="type-th_elt.axiom_kind" class="def record field anchored"><a href="#type-th_elt.axiom_kind" class="anchor"></a><code><span>axiom_kind : <a href="../Util/index.html#type-axiom_kind">Util.axiom_kind</a>;</span></code></li></ol><code><span>}</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-print_th_elt"><a href="#val-print_th_elt" class="anchor"></a><code><span><span class="keyword">val</span> print_th_elt : <span><span class="xref-unresolved">Stdlib</span>.Format.formatter <span class="arrow">-></span></span> <span><a href="#type-th_elt">th_elt</a> <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_pure"><a href="#val-is_pure" class="anchor"></a><code><span><span class="keyword">val</span> is_pure : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_model_term"><a href="#val-is_model_term" class="anchor"></a><code><span><span class="keyword">val</span> is_model_term : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p><code>is_model_term e</code> checks if the expression <code>e</code> is a model terms. A model term can be:</p><ul><li>A constructor application involving only model terms,</li><li>A literal of a basic type (integer, real, boolean, unit or bitvector),</li><li>An abstract name, representing an abstract value (following SMT-LIB terminology).</li></ul><p>The definition of model term maps to value terms in the SMT-LIB standard.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-save_cache"><a href="#val-save_cache" class="anchor"></a><code><span><span class="keyword">val</span> save_cache : <span>unit <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Saves the modules cache</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-reinit_cache"><a href="#val-reinit_cache" class="anchor"></a><code><span><span class="keyword">val</span> reinit_cache : <span>unit <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Reinitializes the module's cache</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Core"><a href="#module-Core" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Core/index.html">Core</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Constructors from the smtlib core theory. https://smtlib.cs.uiowa.edu/theories-Core.shtml</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Ints"><a href="#module-Ints" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Ints/index.html">Ints</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Constructors from the smtlib theory of integers. https://smtlib.cs.uiowa.edu/theories-Ints.shtml</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Reals"><a href="#module-Reals" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Reals/index.html">Reals</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Constructors from the smtlib theory of reals. https://smtlib.cs.uiowa.edu/theories-Reals.shtml</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-BV"><a href="#module-BV" class="anchor"></a><code><span><span class="keyword">module</span> <a href="BV/index.html">BV</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Constructors from the smtlib theory of fixed-size bit-vectors and the QF_BV logic.</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-ArraysEx"><a href="#module-ArraysEx" class="anchor"></a><code><span><span class="keyword">module</span> <a href="ArraysEx/index.html">ArraysEx</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Constructors from the smtlib theory of functional arrays with extensionality logic.</p></div></div></div></body></html>
0 commit comments