-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Commands (alt-ergo-lib.AltErgoLib.Commands)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 3.0.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/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">Index</a> » <a href="../../index.html">alt-ergo-lib</a> » <a href="../index.html">AltErgoLib</a> » Commands</nav><header class="odoc-preamble"><h1>Module <code><span>AltErgoLib.Commands</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-sat_decl_aux"><a href="#type-sat_decl_aux" class="anchor"></a><code><span><span class="keyword">type</span> sat_decl_aux</span><span> = </span></code><ol><li id="type-sat_decl_aux.Decl" class="def variant constructor anchored"><a href="#type-sat_decl_aux.Decl" class="anchor"></a><code><span>| </span><span><span class="constructor">Decl</span> <span class="keyword">of</span> <a href="../Id/index.html#type-typed">Id.typed</a></span></code></li><li id="type-sat_decl_aux.Assume" class="def variant constructor anchored"><a href="#type-sat_decl_aux.Assume" class="anchor"></a><code><span>| </span><span><span class="constructor">Assume</span> <span class="keyword">of</span> string * <a href="../Expr/index.html#type-t">Expr.t</a> * bool</span></code></li><li id="type-sat_decl_aux.PredDef" class="def variant constructor anchored"><a href="#type-sat_decl_aux.PredDef" class="anchor"></a><code><span>| </span><span><span class="constructor">PredDef</span> <span class="keyword">of</span> <a href="../Expr/index.html#type-t">Expr.t</a> * string</span></code></li><li id="type-sat_decl_aux.Optimize" class="def variant constructor anchored"><a href="#type-sat_decl_aux.Optimize" class="anchor"></a><code><span>| </span><span><span class="constructor">Optimize</span> <span class="keyword">of</span> <a href="../Objective/Function/index.html#type-t">Objective.Function.t</a></span></code></li><li id="type-sat_decl_aux.Query" class="def variant constructor anchored"><a href="#type-sat_decl_aux.Query" class="anchor"></a><code><span>| </span><span><span class="constructor">Query</span> <span class="keyword">of</span> string * <a href="../Expr/index.html#type-t">Expr.t</a> * <a href="../Ty/index.html#type-goal_sort">Ty.goal_sort</a></span></code></li><li id="type-sat_decl_aux.ThAssume" class="def variant constructor anchored"><a href="#type-sat_decl_aux.ThAssume" class="anchor"></a><code><span>| </span><span><span class="constructor">ThAssume</span> <span class="keyword">of</span> <a href="../Expr/index.html#type-th_elt">Expr.th_elt</a></span></code></li><li id="type-sat_decl_aux.Push" class="def variant constructor anchored"><a href="#type-sat_decl_aux.Push" class="anchor"></a><code><span>| </span><span><span class="constructor">Push</span> <span class="keyword">of</span> int</span></code></li><li id="type-sat_decl_aux.Pop" class="def variant constructor anchored"><a href="#type-sat_decl_aux.Pop" class="anchor"></a><code><span>| </span><span><span class="constructor">Pop</span> <span class="keyword">of</span> int</span></code></li></ol></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-sat_tdecl"><a href="#type-sat_tdecl" class="anchor"></a><code><span><span class="keyword">type</span> sat_tdecl</span><span> = </span><span>{</span></code><ol><li id="type-sat_tdecl.st_loc" class="def record field anchored"><a href="#type-sat_tdecl.st_loc" class="anchor"></a><code><span>st_loc : <span class="xref-unresolved">Dolmen</span>.Std.Loc.loc;</span></code></li><li id="type-sat_tdecl.st_decl" class="def record field anchored"><a href="#type-sat_tdecl.st_decl" class="anchor"></a><code><span>st_decl : <a href="#type-sat_decl_aux">sat_decl_aux</a>;</span></code></li></ol><code><span>}</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-src"><a href="#val-src" class="anchor"></a><code><span><span class="keyword">val</span> src : <span class="xref-unresolved">Logs</span>.src</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-print"><a href="#val-print" class="anchor"></a><code><span><span class="keyword">val</span> print : <span><span class="xref-unresolved">Stdlib</span>.Format.formatter <span class="arrow">-></span></span> <span><a href="#type-sat_tdecl">sat_tdecl</a> <span class="arrow">-></span></span> unit</span></code></div></div></div></body></html>
0 commit comments