-
Notifications
You must be signed in to change notification settings - Fork 7
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Deploying to gh-pages from @ formalsec/encoding@28ec323 🚀
- Loading branch information
Showing
74 changed files
with
1,749 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| <!DOCTYPE html> | ||
| <html xmlns="http://www.w3.org/1999/xhtml"><head><title>Ast (encoding.Encoding.Ast)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.3.1"/><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">encoding</a> » <a href="../index.html">Encoding</a> » Ast</nav><header class="odoc-preamble"><h1>Module <code><span>Encoding.Ast</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = </span></code><ol><li id="type-t.Declare" class="def variant constructor anchored"><a href="#type-t.Declare" class="anchor"></a><code><span>| </span><span><span class="constructor">Declare</span> <span class="keyword">of</span> <a href="../Symbol/index.html#type-t">Symbol.t</a></span></code></li><li id="type-t.Assert" class="def variant constructor anchored"><a href="#type-t.Assert" class="anchor"></a><code><span>| </span><span><span class="constructor">Assert</span> <span class="keyword">of</span> <a href="../Expr/index.html#type-t">Expr.t</a></span></code></li><li id="type-t.CheckSat" class="def variant constructor anchored"><a href="#type-t.CheckSat" class="anchor"></a><code><span>| </span><span><span class="constructor">CheckSat</span></span></code></li><li id="type-t.GetModel" class="def variant constructor anchored"><a href="#type-t.GetModel" class="anchor"></a><code><span>| </span><span><span class="constructor">GetModel</span></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><span class="xref-unresolved">Stdlib</span>.Format.formatter <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-to_string"><a href="#val-to_string" class="anchor"></a><code><span><span class="keyword">val</span> to_string : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> string</span></code></div></div></div></body></html> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| <!DOCTYPE html> | ||
| <html xmlns="http://www.w3.org/1999/xhtml"><head><title>M (encoding.Encoding.Batch.Make.M)</title><link rel="stylesheet" href="../../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.3.1"/><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">encoding</a> » <a href="../../../index.html">Encoding</a> » <a href="../../index.html">Batch</a> » <a href="../index.html">Make</a> » M</nav><header class="odoc-preamble"><h1>Parameter <code><span>Make.M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-model"><a href="#type-model" class="anchor"></a><code><span><span class="keyword">type</span> model</span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-solver"><a href="#type-solver" class="anchor"></a><code><span><span class="keyword">type</span> solver</span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-status"><a href="#type-status" class="anchor"></a><code><span><span class="keyword">type</span> status</span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-optimize"><a href="#type-optimize" class="anchor"></a><code><span><span class="keyword">type</span> optimize</span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-handle"><a href="#type-handle" class="anchor"></a><code><span><span class="keyword">type</span> handle</span></code></div></div><div class="odoc-spec"><div class="spec exception anchored" id="exception-Error"><a href="#exception-Error" class="anchor"></a><code><span><span class="keyword">exception</span> </span><span><span class="exception">Error</span> <span class="keyword">of</span> string</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-update_param_value"><a href="#val-update_param_value" class="anchor"></a><code><span><span class="keyword">val</span> update_param_value : <span><span><span class="type-var">'a</span> <a href="../../../Params/index.html#type-param">Params.param</a></span> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_solver"><a href="#val-mk_solver" class="anchor"></a><code><span><span class="keyword">val</span> mk_solver : <span>unit <span class="arrow">-></span></span> <a href="#type-solver">solver</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-interrupt"><a href="#val-interrupt" class="anchor"></a><code><span><span class="keyword">val</span> interrupt : <span>unit <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-translate"><a href="#val-translate" class="anchor"></a><code><span><span class="keyword">val</span> translate : <span><a href="#type-solver">solver</a> <span class="arrow">-></span></span> <a href="#type-solver">solver</a></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-solver">solver</a> <span class="arrow">-></span></span> unit</span></code></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-solver">solver</a> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-reset"><a href="#val-reset" class="anchor"></a><code><span><span class="keyword">val</span> reset : <span><a href="#type-solver">solver</a> <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-add_solver"><a href="#val-add_solver" class="anchor"></a><code><span><span class="keyword">val</span> add_solver : <span><a href="#type-solver">solver</a> <span class="arrow">-></span></span> <span><span><a href="../../../Expr/index.html#type-t">Expr.t</a> list</span> <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-check"><a href="#val-check" class="anchor"></a><code><span><span class="keyword">val</span> check : <span><a href="#type-solver">solver</a> <span class="arrow">-></span></span> <span><span><a href="../../../Expr/index.html#type-t">Expr.t</a> list</span> <span class="arrow">-></span></span> <a href="#type-status">status</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-satisfiability"><a href="#val-satisfiability" class="anchor"></a><code><span><span class="keyword">val</span> satisfiability : <span><a href="#type-status">status</a> <span class="arrow">-></span></span> <a href="../../../Mappings_intf/index.html#type-satisfiability">Mappings_intf.satisfiability</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-solver_model"><a href="#val-solver_model" class="anchor"></a><code><span><span class="keyword">val</span> solver_model : <span><a href="#type-solver">solver</a> <span class="arrow">-></span></span> <span><a href="#type-model">model</a> option</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-value"><a href="#val-value" class="anchor"></a><code><span><span class="keyword">val</span> value : <span><a href="#type-model">model</a> <span class="arrow">-></span></span> <span><a href="../../../Expr/index.html#type-t">Expr.t</a> <span class="arrow">-></span></span> <a href="../../../Value/index.html#type-t">Value.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-values_of_model"><a href="#val-values_of_model" class="anchor"></a><code><span><span class="keyword">val</span> values_of_model : <span><span class="optlabel">?symbols</span>:<span><a href="../../../Symbol/index.html#type-t">Symbol.t</a> list</span> <span class="arrow">-></span></span> <span><a href="#type-model">model</a> <span class="arrow">-></span></span> <a href="../../../Model/index.html#type-t">Model.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-expr_to_smtstring"><a href="#val-expr_to_smtstring" class="anchor"></a><code><span><span class="keyword">val</span> expr_to_smtstring : <span><span><a href="../../../Expr/index.html#type-t">Expr.t</a> list</span> <span class="arrow">-></span></span> <span>bool <span class="arrow">-></span></span> string</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_optimize"><a href="#val-mk_optimize" class="anchor"></a><code><span><span class="keyword">val</span> mk_optimize : <span>unit <span class="arrow">-></span></span> <a href="#type-optimize">optimize</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-add_optimize"><a href="#val-add_optimize" class="anchor"></a><code><span><span class="keyword">val</span> add_optimize : <span><a href="#type-optimize">optimize</a> <span class="arrow">-></span></span> <span><span><a href="../../../Expr/index.html#type-t">Expr.t</a> list</span> <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-maximize"><a href="#val-maximize" class="anchor"></a><code><span><span class="keyword">val</span> maximize : <span><a href="#type-optimize">optimize</a> <span class="arrow">-></span></span> <span><a href="../../../Expr/index.html#type-t">Expr.t</a> <span class="arrow">-></span></span> <a href="#type-handle">handle</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-minimize"><a href="#val-minimize" class="anchor"></a><code><span><span class="keyword">val</span> minimize : <span><a href="#type-optimize">optimize</a> <span class="arrow">-></span></span> <span><a href="../../../Expr/index.html#type-t">Expr.t</a> <span class="arrow">-></span></span> <a href="#type-handle">handle</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-optimize_model"><a href="#val-optimize_model" class="anchor"></a><code><span><span class="keyword">val</span> optimize_model : <span><a href="#type-optimize">optimize</a> <span class="arrow">-></span></span> <span><a href="#type-model">model</a> option</span></span></code></div></div></div></body></html> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| <!DOCTYPE html> | ||
| <html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (encoding.Encoding.Batch.Make)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.3.1"/><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">encoding</a> » <a href="../../index.html">Encoding</a> » <a href="../index.html">Batch</a> » Make</nav><header class="odoc-preamble"><h1>Module <code><span>Batch.Make</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#parameters">Parameters</a></li><li><a href="#signature">Signature</a></li></ul></nav><div class="odoc-content"><h2 id="parameters"><a href="#parameters" class="anchor"></a>Parameters</h2><div class="odoc-spec"><div class="spec parameter anchored" id="argument-1-M"><a href="#argument-1-M" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="argument-1-M/index.html">M</a></span><span> : <a href="../../Mappings_intf/module-type-S/index.html">Mappings_intf.S</a></span></code></div></div><h2 id="signature"><a href="#signature" class="anchor"></a>Signature</h2><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-solver"><a href="#type-solver" class="anchor"></a><code><span><span class="keyword">type</span> solver</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-solver_time"><a href="#val-solver_time" class="anchor"></a><code><span><span class="keyword">val</span> solver_time : <span>float <span class="xref-unresolved">Stdlib</span>.ref</span></span></code></div><div class="spec-doc"><p>Time spent inside SMT solver.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-solver_count"><a href="#val-solver_count" class="anchor"></a><code><span><span class="keyword">val</span> solver_count : <span>int <span class="xref-unresolved">Stdlib</span>.ref</span></span></code></div><div class="spec-doc"><p>Number of queries to the SMT solver.</p></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><span class="optlabel">?params</span>:<a href="../../Params/index.html#type-t">Params.t</a> <span class="arrow">-></span></span> <span>unit <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Create a new solver.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-interrupt"><a href="#val-interrupt" class="anchor"></a><code><span><span class="keyword">val</span> interrupt : <span>unit <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Interrupt solver.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-clone"><a href="#val-clone" class="anchor"></a><code><span><span class="keyword">val</span> clone : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Clone a given solver.</p></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">-></span></span> unit</span></code></div><div class="spec-doc"><p>Create a backtracking point.</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">-></span></span> <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>pop solver n</code> backtracks <code>n</code> backtracking points.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-reset"><a href="#val-reset" class="anchor"></a><code><span><span class="keyword">val</span> reset : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Resets the solver, i.e., remove all assertions from the solver.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-add"><a href="#val-add" class="anchor"></a><code><span><span class="keyword">val</span> add : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span><a href="../../Expr/index.html#type-t">Expr.t</a> list</span> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Assert one or multiple constraints into the solver.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get_assertions"><a href="#val-get_assertions" class="anchor"></a><code><span><span class="keyword">val</span> get_assertions : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="../../Expr/index.html#type-t">Expr.t</a> list</span></span></code></div><div class="spec-doc"><p>The set of assertions in the solver.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-check"><a href="#val-check" class="anchor"></a><code><span><span class="keyword">val</span> check : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span><a href="../../Expr/index.html#type-t">Expr.t</a> list</span> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Checks the satisfiability of the assertions.</p><p>Raises <code>Unknown</code> if SMT solver returns unknown.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get_value"><a href="#val-get_value" class="anchor"></a><code><span><span class="keyword">val</span> get_value : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="../../Expr/index.html#type-t">Expr.t</a> <span class="arrow">-></span></span> <a href="../../Expr/index.html#type-t">Expr.t</a></span></code></div><div class="spec-doc"><p><code>get_value solver e</code> get an expression denoting the model value of a given expression.</p><p>Requires that the last <a href="#val-check"><code>check</code></a> query returned <code>true</code>.</p><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">t</span> <p>The solver.</p></li></ul><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">e</span> <p>Expr to query a model for.</p></li></ul><ul class="at-tags"><li class="returns"><span class="at-tag">returns</span> <p>An expression denoting the model value of <code>e</code>.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-model"><a href="#val-model" class="anchor"></a><code><span><span class="keyword">val</span> model : <span><span class="optlabel">?symbols</span>:<span><a href="../../Symbol/index.html#type-t">Symbol.t</a> list</span> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="../../Model/index.html#type-t">Model.t</a> option</span></span></code></div><div class="spec-doc"><p>The model of the last <code>check</code>.</p><p>The result is <code>None</code> if <code>check</code> was not invoked before, or its result was not <code>Satisfiable</code>.</p></div></div></div></body></html> |
Oops, something went wrong.