Deploying to gh-pages from @ 292f306 🚀

Author: Halbaroth

next/API/alt-ergo-lib/AltErgoLib/Satml/Make/index.html

@@ -21,4 +21,4 @@
   <span><a href="../../Satml_types/Flat_Formula/index.html#type-hcons_env">Satml_types.Flat_Formula.hcons_env</a> <span class="arrow">&#45;&gt;</span></span>
   <span class="xref-unresolved">AltErgoLib</span>.Satml_types.Atom.Set.t</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-current_tbox"><a href="#val-current_tbox" class="anchor"></a><code><span><span class="keyword">val</span> current_tbox : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-th">th</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-set_current_tbox"><a href="#val-set_current_tbox" class="anchor"></a><code><span><span class="keyword">val</span> set_current_tbox : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-th">th</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../Satml_types/Atom/index.html#type-hcons_env">Satml_types.Atom.hcons_env</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-assume_th_elt"><a href="#val-assume_th_elt" class="anchor"></a><code><span><span class="keyword">val</span> assume_th_elt : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Expr/index.html#type-th_elt">Expr.th_elt</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Explanation/index.html#type-t">Explanation.t</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-decision_level"><a href="#val-decision_level" class="anchor"></a><code><span><span class="keyword">val</span> decision_level : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> int</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-assertion_level"><a href="#val-assertion_level" class="anchor"></a><code><span><span class="keyword">val</span> assertion_level : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> int</span></code></div><div class="spec-doc"><p>Returns the number of active assertion levels, that is the number of levels introduced with <code>push</code> that have not yet been popped.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-cancel_until"><a href="#val-cancel_until" class="anchor"></a><code><span><span class="keyword">val</span> cancel_until : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span>int <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-exists_in_lazy_cnf"><a href="#val-exists_in_lazy_cnf" class="anchor"></a><code><span><span class="keyword">val</span> exists_in_lazy_cnf : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Satml_types/Flat_Formula/index.html#type-t">Satml_types.Flat_Formula.t</a> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-known_lazy_formulas"><a href="#val-known_lazy_formulas" class="anchor"></a><code><span><span class="keyword">val</span> known_lazy_formulas : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span>int <span class="xref-unresolved">AltErgoLib</span>.Satml_types.Flat_Formula.Map.t</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-reason_of_deduction"><a href="#val-reason_of_deduction" class="anchor"></a><code><span><span class="keyword">val</span> reason_of_deduction : 
   <span><a href="../../Satml_types/Atom/index.html#type-atom">Satml_types.Atom.atom</a> <span class="arrow">&#45;&gt;</span></span>
-  <span class="xref-unresolved">AltErgoLib</span>.Satml_types.Atom.Set.t</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-do_case_split"><a href="#val-do_case_split" class="anchor"></a><code><span><span class="keyword">val</span> do_case_split : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Util/index.html#type-case_split_policy">Util.case_split_policy</a> <span class="arrow">&#45;&gt;</span></span> <a href="../index.html#type-conflict_origin">conflict_origin</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-conflict_analyze_and_fix"><a href="#val-conflict_analyze_and_fix" class="anchor"></a><code><span><span class="keyword">val</span> conflict_analyze_and_fix : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../index.html#type-conflict_origin">conflict_origin</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push"><a href="#val-push" class="anchor"></a><code><span><span class="keyword">val</span> push : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Satml_types/Atom/index.html#type-atom">Satml_types.Atom.atom</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>push env g</code> adds a new assertion level. The formula <code>g</code> is used in <code>Satml_frontend</code> to guard all formulas asserted at this level.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop"><a href="#val-pop" class="anchor"></a><code><span><span class="keyword">val</span> pop : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>pop env</code> pops the latest assertion level.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-optimize"><a href="#val-optimize" class="anchor"></a><code><span><span class="keyword">val</span> optimize : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Objective/Function/index.html#type-t">Objective.Function.t</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>optimize env fn</code> adds the objection <code>fn</code> to the environment <code>env</code>.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <code>invalid_argurment</code> <p>if the decision level of <code>env</code> is not zero.</p></li></ul></div></div></div></body></html>
+  <span class="xref-unresolved">AltErgoLib</span>.Satml_types.Atom.Set.t</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-do_case_split"><a href="#val-do_case_split" class="anchor"></a><code><span><span class="keyword">val</span> do_case_split : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Util/index.html#type-case_split_policy">Util.case_split_policy</a> <span class="arrow">&#45;&gt;</span></span> <a href="../index.html#type-conflict_origin">conflict_origin</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-conflict_analyze_and_fix"><a href="#val-conflict_analyze_and_fix" class="anchor"></a><code><span><span class="keyword">val</span> conflict_analyze_and_fix : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../index.html#type-conflict_origin">conflict_origin</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push"><a href="#val-push" class="anchor"></a><code><span><span class="keyword">val</span> push : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <a href="../../Expr/index.html#type-t">Expr.t</a></span></code></div><div class="spec-doc"><p><code>push env</code> adds a new assertion level and returns a guard <code>g</code> that must be used to guard all formulas asserted at this level.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop"><a href="#val-pop" class="anchor"></a><code><span><span class="keyword">val</span> pop : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>pop env</code> pops the latest assertion level.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-optimize"><a href="#val-optimize" class="anchor"></a><code><span><span class="keyword">val</span> optimize : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Objective/Function/index.html#type-t">Objective.Function.t</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>optimize env fn</code> adds the objection <code>fn</code> to the environment <code>env</code>.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <code>invalid_argurment</code> <p>if the decision level of <code>env</code> is not zero.</p></li></ul></div></div></div></body></html>

next/API/alt-ergo-lib/AltErgoLib/Satml/module-type-SAT_ML/index.html

@@ -21,4 +21,4 @@
   <span><a href="../../Satml_types/Flat_Formula/index.html#type-hcons_env">Satml_types.Flat_Formula.hcons_env</a> <span class="arrow">&#45;&gt;</span></span>
   <span class="xref-unresolved">AltErgoLib</span>.Satml_types.Atom.Set.t</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-current_tbox"><a href="#val-current_tbox" class="anchor"></a><code><span><span class="keyword">val</span> current_tbox : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-th">th</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-set_current_tbox"><a href="#val-set_current_tbox" class="anchor"></a><code><span><span class="keyword">val</span> set_current_tbox : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-th">th</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../Satml_types/Atom/index.html#type-hcons_env">Satml_types.Atom.hcons_env</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-assume_th_elt"><a href="#val-assume_th_elt" class="anchor"></a><code><span><span class="keyword">val</span> assume_th_elt : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Expr/index.html#type-th_elt">Expr.th_elt</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Explanation/index.html#type-t">Explanation.t</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-decision_level"><a href="#val-decision_level" class="anchor"></a><code><span><span class="keyword">val</span> decision_level : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> int</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-assertion_level"><a href="#val-assertion_level" class="anchor"></a><code><span><span class="keyword">val</span> assertion_level : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> int</span></code></div><div class="spec-doc"><p>Returns the number of active assertion levels, that is the number of levels introduced with <code>push</code> that have not yet been popped.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-cancel_until"><a href="#val-cancel_until" class="anchor"></a><code><span><span class="keyword">val</span> cancel_until : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span>int <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-exists_in_lazy_cnf"><a href="#val-exists_in_lazy_cnf" class="anchor"></a><code><span><span class="keyword">val</span> exists_in_lazy_cnf : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Satml_types/Flat_Formula/index.html#type-t">Satml_types.Flat_Formula.t</a> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-known_lazy_formulas"><a href="#val-known_lazy_formulas" class="anchor"></a><code><span><span class="keyword">val</span> known_lazy_formulas : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span>int <span class="xref-unresolved">AltErgoLib</span>.Satml_types.Flat_Formula.Map.t</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-reason_of_deduction"><a href="#val-reason_of_deduction" class="anchor"></a><code><span><span class="keyword">val</span> reason_of_deduction : 
   <span><a href="../../Satml_types/Atom/index.html#type-atom">Satml_types.Atom.atom</a> <span class="arrow">&#45;&gt;</span></span>
-  <span class="xref-unresolved">AltErgoLib</span>.Satml_types.Atom.Set.t</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-do_case_split"><a href="#val-do_case_split" class="anchor"></a><code><span><span class="keyword">val</span> do_case_split : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Util/index.html#type-case_split_policy">Util.case_split_policy</a> <span class="arrow">&#45;&gt;</span></span> <a href="../index.html#type-conflict_origin">conflict_origin</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-conflict_analyze_and_fix"><a href="#val-conflict_analyze_and_fix" class="anchor"></a><code><span><span class="keyword">val</span> conflict_analyze_and_fix : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../index.html#type-conflict_origin">conflict_origin</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push"><a href="#val-push" class="anchor"></a><code><span><span class="keyword">val</span> push : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Satml_types/Atom/index.html#type-atom">Satml_types.Atom.atom</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>push env g</code> adds a new assertion level. The formula <code>g</code> is used in <code>Satml_frontend</code> to guard all formulas asserted at this level.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop"><a href="#val-pop" class="anchor"></a><code><span><span class="keyword">val</span> pop : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>pop env</code> pops the latest assertion level.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-optimize"><a href="#val-optimize" class="anchor"></a><code><span><span class="keyword">val</span> optimize : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Objective/Function/index.html#type-t">Objective.Function.t</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>optimize env fn</code> adds the objection <code>fn</code> to the environment <code>env</code>.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <code>invalid_argurment</code> <p>if the decision level of <code>env</code> is not zero.</p></li></ul></div></div></div></body></html>
+  <span class="xref-unresolved">AltErgoLib</span>.Satml_types.Atom.Set.t</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-do_case_split"><a href="#val-do_case_split" class="anchor"></a><code><span><span class="keyword">val</span> do_case_split : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Util/index.html#type-case_split_policy">Util.case_split_policy</a> <span class="arrow">&#45;&gt;</span></span> <a href="../index.html#type-conflict_origin">conflict_origin</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-conflict_analyze_and_fix"><a href="#val-conflict_analyze_and_fix" class="anchor"></a><code><span><span class="keyword">val</span> conflict_analyze_and_fix : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../index.html#type-conflict_origin">conflict_origin</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push"><a href="#val-push" class="anchor"></a><code><span><span class="keyword">val</span> push : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <a href="../../Expr/index.html#type-t">Expr.t</a></span></code></div><div class="spec-doc"><p><code>push env</code> adds a new assertion level and returns a guard <code>g</code> that must be used to guard all formulas asserted at this level.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop"><a href="#val-pop" class="anchor"></a><code><span><span class="keyword">val</span> pop : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>pop env</code> pops the latest assertion level.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-optimize"><a href="#val-optimize" class="anchor"></a><code><span><span class="keyword">val</span> optimize : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../Objective/Function/index.html#type-t">Objective.Function.t</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>optimize env fn</code> adds the objection <code>fn</code> to the environment <code>env</code>.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <code>invalid_argurment</code> <p>if the decision level of <code>env</code> is not zero.</p></li></ul></div></div></div></body></html>