mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 03:35:38 -05:00
Removed old hardcoded documentation.
This commit is contained in:
Guillaume Bury
parent
dc43c28a02
commit
05aa984081
37 changed files with 32 additions and 2024 deletions
|
|
@ -1,25 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="next" href="Hstring.HSet.html">
|
||||
<link rel="Up" href="Hstring.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Hstring.H</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"> <a href="Hstring.html">Up</a>
|
||||
<a href="Hstring.HSet.html">Next</a>
|
||||
</div>
|
||||
<center><h1>Module <a href="type_Hstring.H.html">Hstring.H</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module</span> H: <code class="type">Hashtbl.S</code><code class="type"> with type key = t</code></pre>Hash-tables indexed by hash-consed strings<br>
|
||||
<hr width="100%">
|
||||
</body></html>
|
||||
|
|
@ -1,25 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="previous" href="Hstring.HSet.html">
|
||||
<link rel="Up" href="Hstring.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Hstring.HMap</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"><a href="Hstring.HSet.html">Previous</a>
|
||||
<a href="Hstring.html">Up</a>
|
||||
</div>
|
||||
<center><h1>Module <a href="type_Hstring.HMap.html">Hstring.HMap</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module</span> HMap: <code class="type">Map.S</code><code class="type"> with type key = t</code></pre>Maps indexed by hash-consed strings<br>
|
||||
<hr width="100%">
|
||||
</body></html>
|
||||
|
|
@ -1,27 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="previous" href="Hstring.H.html">
|
||||
<link rel="next" href="Hstring.HMap.html">
|
||||
<link rel="Up" href="Hstring.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Hstring.HSet</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"><a href="Hstring.H.html">Previous</a>
|
||||
<a href="Hstring.html">Up</a>
|
||||
<a href="Hstring.HMap.html">Next</a>
|
||||
</div>
|
||||
<center><h1>Module <a href="type_Hstring.HSet.html">Hstring.HSet</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module</span> HSet: <code class="type">Set.S</code><code class="type"> with type elt = t</code></pre>Sets of hash-consed strings<br>
|
||||
<hr width="100%">
|
||||
</body></html>
|
||||
|
|
@ -1,90 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="previous" href="Smt.html">
|
||||
<link rel="Up" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Hstring</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"><a href="Smt.html">Previous</a>
|
||||
<a href="index.html">Up</a>
|
||||
</div>
|
||||
<center><h1>Module <a href="type_Hstring.html">Hstring</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module</span> Hstring: <code class="code">sig</code> <a href="Hstring.html">..</a> <code class="code">end</code></pre><b>Hash-consed strings</b>
|
||||
<p>
|
||||
|
||||
Hash-consing is a technique to share values that are structurally
|
||||
equal. More details on
|
||||
<a href="http://en.wikipedia.org/wiki/Hash_consing"> Wikipedia</a> and
|
||||
<a href="http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf"> here</a>.
|
||||
<p>
|
||||
|
||||
This module provides an easy way to use hash-consing for strings.<br>
|
||||
<hr width="100%">
|
||||
<pre><span id="TYPEt"><span class="keyword">type</span> <code class="type"></code>t</span> = <code class="type">string Hashcons.hash_consed</code> </pre>
|
||||
<div class="info">
|
||||
The type of Hash-consed string<br>
|
||||
</div>
|
||||
|
||||
<pre><span id="VALmake"><span class="keyword">val</span> make</span> : <code class="type">string -> <a href="Hstring.html#TYPEt">t</a></code></pre><div class="info">
|
||||
<code class="code">make s</code> builds ans returns a hash-consed string from <code class="code">s</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALview"><span class="keyword">val</span> view</span> : <code class="type"><a href="Hstring.html#TYPEt">t</a> -> string</code></pre><div class="info">
|
||||
<code class="code">view hs</code> returns the string corresponding to <code class="code">hs</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALequal"><span class="keyword">val</span> equal</span> : <code class="type"><a href="Hstring.html#TYPEt">t</a> -> <a href="Hstring.html#TYPEt">t</a> -> bool</code></pre><div class="info">
|
||||
<code class="code">equal x y</code> returns <code class="code">true</code> if <code class="code">x</code> and <code class="code">y</code> are the same hash-consed string
|
||||
(constant time).<br>
|
||||
</div>
|
||||
<pre><span id="VALcompare"><span class="keyword">val</span> compare</span> : <code class="type"><a href="Hstring.html#TYPEt">t</a> -> <a href="Hstring.html#TYPEt">t</a> -> int</code></pre><div class="info">
|
||||
<code class="code">compares x y</code> returns <code class="code">0</code> if <code class="code">x</code> and <code class="code">y</code> are equal, and is unspecified
|
||||
otherwise but provides a total ordering on hash-consed strings.<br>
|
||||
</div>
|
||||
<pre><span id="VALhash"><span class="keyword">val</span> hash</span> : <code class="type"><a href="Hstring.html#TYPEt">t</a> -> int</code></pre><div class="info">
|
||||
<code class="code">hash x</code> returns the integer (hash) associated to <code class="code">x</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALempty"><span class="keyword">val</span> empty</span> : <code class="type"><a href="Hstring.html#TYPEt">t</a></code></pre><div class="info">
|
||||
the empty (<code class="code">""</code>) hash-consed string.<br>
|
||||
</div>
|
||||
<pre><span id="VALlist_assoc"><span class="keyword">val</span> list_assoc</span> : <code class="type"><a href="Hstring.html#TYPEt">t</a> -> (<a href="Hstring.html#TYPEt">t</a> * 'a) list -> 'a</code></pre><div class="info">
|
||||
<code class="code">list_assoc x l</code> returns the element associated with <code class="code">x</code> in the list of
|
||||
pairs <code class="code">l</code>.<br>
|
||||
<b>Raises</b> <code>Not_found</code> if there is no value associated with <code class="code">x</code> in the list <code class="code">l</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALlist_mem_assoc"><span class="keyword">val</span> list_mem_assoc</span> : <code class="type"><a href="Hstring.html#TYPEt">t</a> -> (<a href="Hstring.html#TYPEt">t</a> * 'a) list -> bool</code></pre><div class="info">
|
||||
Same as <a href="Hstring.html#VALlist_assoc"><code class="code">Hstring.list_assoc</code></a>, but simply returns <code class="code">true</code> if a binding exists, and
|
||||
<code class="code">false</code> if no bindings exist for the given key.<br>
|
||||
</div>
|
||||
<pre><span id="VALlist_mem"><span class="keyword">val</span> list_mem</span> : <code class="type"><a href="Hstring.html#TYPEt">t</a> -> <a href="Hstring.html#TYPEt">t</a> list -> bool</code></pre><div class="info">
|
||||
<code class="code">list_mem x l</code> is <code class="code">true</code> if and only if <code class="code">x</code> is equal to an element of <code class="code">l</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALlist_mem_couple"><span class="keyword">val</span> list_mem_couple</span> : <code class="type"><a href="Hstring.html#TYPEt">t</a> * <a href="Hstring.html#TYPEt">t</a> -> (<a href="Hstring.html#TYPEt">t</a> * <a href="Hstring.html#TYPEt">t</a>) list -> bool</code></pre><div class="info">
|
||||
<code class="code">list_mem_couple (x,y) l</code> is <code class="code">true</code> if and only if <code class="code">(x,y)</code> is equal to an
|
||||
element of <code class="code">l</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALcompare_list"><span class="keyword">val</span> compare_list</span> : <code class="type"><a href="Hstring.html#TYPEt">t</a> list -> <a href="Hstring.html#TYPEt">t</a> list -> int</code></pre><div class="info">
|
||||
<code class="code">compare_list l1 l2</code> returns <code class="code">0</code> if and only if <code class="code">l1</code> is equal to <code class="code">l2</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALprint"><span class="keyword">val</span> print</span> : <code class="type">Format.formatter -> <a href="Hstring.html#TYPEt">t</a> -> unit</code></pre><div class="info">
|
||||
Prints a list of hash-consed strings on a formatter.<br>
|
||||
</div>
|
||||
<pre><span class="keyword">module</span> <a href="Hstring.H.html">H</a>: <code class="type">Hashtbl.S</code><code class="type"> with type key = t</code></pre><div class="info">
|
||||
Hash-tables indexed by hash-consed strings
|
||||
</div>
|
||||
<pre><span class="keyword">module</span> <a href="Hstring.HSet.html">HSet</a>: <code class="type">Set.S</code><code class="type"> with type elt = t</code></pre><div class="info">
|
||||
Sets of hash-consed strings
|
||||
</div>
|
||||
<pre><span class="keyword">module</span> <a href="Hstring.HMap.html">HMap</a>: <code class="type">Map.S</code><code class="type"> with type key = t</code></pre><div class="info">
|
||||
Maps indexed by hash-consed strings
|
||||
</div>
|
||||
</body></html>
|
||||
|
|
@ -1,135 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="previous" href="Smt.Term.html">
|
||||
<link rel="next" href="Smt.Make.html">
|
||||
<link rel="Up" href="Smt.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt.Formula</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"><a href="Smt.Term.html">Previous</a>
|
||||
<a href="Smt.html">Up</a>
|
||||
<a href="Smt.Make.html">Next</a>
|
||||
</div>
|
||||
<center><h1>Module <a href="type_Smt.Formula.html">Smt.Formula</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module</span> Formula: <code class="code">sig</code> <a href="Smt.Formula.html">..</a> <code class="code">end</code></pre><hr width="100%">
|
||||
<br><code><span id="TYPEcomparator"><span class="keyword">type</span> <code class="type"></code>comparator</span> = </code><table class="typetable">
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Eq</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >equality (<code class="code">=</code>)</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Neq</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >disequality (<code class="code"><></code>)</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Le</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >inequality (<code class="code"><=</code>)</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Lt</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >strict inequality (<code class="code"><</code>)</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr></table>
|
||||
|
||||
<div class="info">
|
||||
The type of comparators:<br>
|
||||
</div>
|
||||
|
||||
<br><code><span id="TYPEcombinator"><span class="keyword">type</span> <code class="type"></code>combinator</span> = </code><table class="typetable">
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">And</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >conjunction</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Or</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >disjunction</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Imp</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >implication</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Not</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >negation</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr></table>
|
||||
|
||||
<div class="info">
|
||||
The type of operators<br>
|
||||
</div>
|
||||
|
||||
<br><code><span id="TYPEt"><span class="keyword">type</span> <code class="type"></code>t</span> = </code><table class="typetable">
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Lit</span> <span class="keyword">of</span> <code class="type">Literal.LT.t</code></code></td>
|
||||
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Comb</span> <span class="keyword">of</span> <code class="type"><a href="Smt.Formula.html#TYPEcombinator">combinator</a> * <a href="Smt.Formula.html#TYPEt">t</a> list</code></code></td>
|
||||
|
||||
</tr></table>
|
||||
|
||||
<div class="info">
|
||||
The type of ground formulas<br>
|
||||
</div>
|
||||
|
||||
<pre><span id="VALf_true"><span class="keyword">val</span> f_true</span> : <code class="type"><a href="Smt.Formula.html#TYPEt">t</a></code></pre><div class="info">
|
||||
The formula which represents <code class="code">true</code><br>
|
||||
</div>
|
||||
<pre><span id="VALf_false"><span class="keyword">val</span> f_false</span> : <code class="type"><a href="Smt.Formula.html#TYPEt">t</a></code></pre><div class="info">
|
||||
The formula which represents <code class="code">false</code><br>
|
||||
</div>
|
||||
<pre><span id="VALmake_lit"><span class="keyword">val</span> make_lit</span> : <code class="type"><a href="Smt.Formula.html#TYPEcomparator">comparator</a> -> <a href="Smt.Term.html#TYPEt">Smt.Term.t</a> list -> <a href="Smt.Formula.html#TYPEt">t</a></code></pre><div class="info">
|
||||
<code class="code">make_lit cmp [t1; t2]</code> creates the literal <code class="code">(t1 <cmp> t2)</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALmake"><span class="keyword">val</span> make</span> : <code class="type"><a href="Smt.Formula.html#TYPEcombinator">combinator</a> -> <a href="Smt.Formula.html#TYPEt">t</a> list -> <a href="Smt.Formula.html#TYPEt">t</a></code></pre><div class="info">
|
||||
<code class="code">make cmb [f_1; ...; f_n]</code> creates the formula
|
||||
<code class="code">(f_1 <cmb> ... <cmb> f_n)</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALmake_cnf"><span class="keyword">val</span> make_cnf</span> : <code class="type"><a href="Smt.Formula.html#TYPEt">t</a> -> Literal.LT.t list list</code></pre><div class="info">
|
||||
<code class="code">make_cnf f</code> returns a conjunctive normal form of <code class="code">f</code> under the form: a
|
||||
list (which is a conjunction) of lists (which are disjunctions) of
|
||||
literals.<br>
|
||||
</div>
|
||||
<pre><span id="VALprint"><span class="keyword">val</span> print</span> : <code class="type">Format.formatter -> <a href="Smt.Formula.html#TYPEt">t</a> -> unit</code></pre><div class="info">
|
||||
<code class="code">print fmt f</code> prints the formula on the formatter <code class="code">fmt</code>.<br>
|
||||
</div>
|
||||
</body></html>
|
||||
|
|
@ -1,105 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="previous" href="Smt.Formula.html">
|
||||
<link rel="Up" href="Smt.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><link title="Profiling functions" rel="Section" href="#2_Profilingfunctions">
|
||||
<link title="Main API of the solver" rel="Section" href="#2_MainAPIofthesolver">
|
||||
<title>Smt.Make</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"><a href="Smt.Formula.html">Previous</a>
|
||||
<a href="Smt.html">Up</a>
|
||||
</div>
|
||||
<center><h1>Functor <a href="type_Smt.Make.html">Smt.Make</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module</span> Make: <div class="sig_block"><code class="code">functor (</code><code class="code">Dummy</code><code class="code"> : </code><code class="code">sig</code><div class="sig_block"></div><code class="code">end</code><code class="code">) -> </code><code class="type"><a href="Smt.Solver.html">Solver</a></code><code class="type"> </code></div></pre>Functor to create several instances of the solver<br>
|
||||
<table border="0" cellpadding="3" width="100%">
|
||||
<tr>
|
||||
<td align="left" valign="top" width="1%%"><b>Parameters: </b></td>
|
||||
<td>
|
||||
<table class="paramstable">
|
||||
<tr>
|
||||
<td align="center" valign="top" width="15%">
|
||||
<code>Dummy</code></td>
|
||||
<td align="center" valign="top">:</td>
|
||||
<td><code class="type">sig end</code>
|
||||
</table>
|
||||
</td>
|
||||
</tr>
|
||||
</table>
|
||||
<hr width="100%">
|
||||
<br>
|
||||
This SMT solver is imperative in the sense that it maintains a global
|
||||
context. To create different instances of Alt-Ergo Zero use the
|
||||
functor <a href="Smt.Make.html"><code class="code">Smt.Make</code></a>.
|
||||
<p>
|
||||
|
||||
A typical use of this solver is to do the following :<pre><code class="code"> clear ();
|
||||
assume f_1;
|
||||
...
|
||||
assume f_n;
|
||||
check ();</code></pre><br>
|
||||
<pre><span id="TYPEstate"><span class="keyword">type</span> <code class="type"></code>state</span> </pre>
|
||||
<div class="info">
|
||||
The type of the internal state of the solver (see <a href="Smt.Solver.html#VALsave_state"><code class="code">Smt.Solver.save_state</code></a> and
|
||||
<a href="Smt.Solver.html#VALrestore_state"><code class="code">Smt.Solver.restore_state</code></a>).<br>
|
||||
</div>
|
||||
|
||||
<br>
|
||||
<span id="2_Profilingfunctions"><h2>Profiling functions</h2></span><br>
|
||||
<pre><span id="VALget_time"><span class="keyword">val</span> get_time</span> : <code class="type">unit -> float</code></pre><div class="info">
|
||||
<code class="code">get_time ()</code> returns the cumulated time spent in the solver in seconds.<br>
|
||||
</div>
|
||||
<pre><span id="VALget_calls"><span class="keyword">val</span> get_calls</span> : <code class="type">unit -> int</code></pre><div class="info">
|
||||
<code class="code">get_calls ()</code> returns the cumulated number of calls to <a href="Smt.Solver.html#VALcheck"><code class="code">Smt.Solver.check</code></a>.<br>
|
||||
</div>
|
||||
<br>
|
||||
<span id="2_MainAPIofthesolver"><h2>Main API of the solver</h2></span><br>
|
||||
<pre><span id="VALclear"><span class="keyword">val</span> clear</span> : <code class="type">unit -> unit</code></pre><div class="info">
|
||||
<code class="code">clear ()</code> clears the context of the solver. Use this after <a href="Smt.Solver.html#VALcheck"><code class="code">Smt.Solver.check</code></a>
|
||||
raised <a href="Smt.html#EXCEPTIONUnsat"><code class="code">Smt.Unsat</code></a> or if you want to restart the solver.<br>
|
||||
</div>
|
||||
<pre><span id="VALassume"><span class="keyword">val</span> assume</span> : <code class="type">?profiling:bool -> id:int -> <a href="Smt.Formula.html#TYPEt">Smt.Formula.t</a> -> unit</code></pre><div class="info">
|
||||
<code class="code">assume ~profiling:b f id</code> adds the formula <code class="code">f</code> to the context of the
|
||||
solver with idetifier <code class="code">id</code>.
|
||||
This function only performs unit propagation.<br>
|
||||
</div>
|
||||
<div class="param_info"><code class="code">profiling</code> : if set to <code class="code">true</code> then profiling information (time) will
|
||||
be computed (expensive because of system calls).
|
||||
<p>
|
||||
|
||||
<b>Raises</b> <a href="Smt.html#EXCEPTIONUnsat"><code class="code">Smt.Unsat</code></a> if the context becomes inconsistent after unit
|
||||
propagation.</div>
|
||||
<pre><span id="VALcheck"><span class="keyword">val</span> check</span> : <code class="type">?profiling:bool -> unit -> unit</code></pre><div class="info">
|
||||
<code class="code">check ()</code> runs Alt-Ergo Zero on its context. If <code class="code">()</code> is
|
||||
returned then the context is satifiable.<br>
|
||||
</div>
|
||||
<div class="param_info"><code class="code">profiling</code> : if set to <code class="code">true</code> then profiling information (time) will
|
||||
be computed (expensive because of system calls).
|
||||
<p>
|
||||
|
||||
<b>Raises</b> <a href="Smt.html#EXCEPTIONUnsat"><code class="code">Smt.Unsat</code></a> <code class="code">[id_1; ...; id_n]</code> if the context is unsatisfiable.
|
||||
<code class="code">id_1, ..., id_n</code> is the unsat core (returned as the identifiers of the
|
||||
formulas given to the solver).</div>
|
||||
<pre><span id="VALsave_state"><span class="keyword">val</span> save_state</span> : <code class="type">unit -> <a href="Smt.Solver.html#TYPEstate">state</a></code></pre><div class="info">
|
||||
<code class="code">save_state ()</code> returns a <b>copy</b> of the current state of the solver.<br>
|
||||
</div>
|
||||
<pre><span id="VALrestore_state"><span class="keyword">val</span> restore_state</span> : <code class="type"><a href="Smt.Solver.html#TYPEstate">state</a> -> unit</code></pre><div class="info">
|
||||
<code class="code">restore_state s</code> restores a previously saved state <code class="code">s</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALentails"><span class="keyword">val</span> entails</span> : <code class="type">?profiling:bool -> id:int -> <a href="Smt.Formula.html#TYPEt">Smt.Formula.t</a> -> bool</code></pre><div class="info">
|
||||
<code class="code">entails ~id f</code> returns <code class="code">true</code> if the context of the solver entails
|
||||
the formula <code class="code">f</code>. It doesn't modify the context of the solver (the state
|
||||
is saved when this function is called and restored on exit).<br>
|
||||
</div>
|
||||
</body></html>
|
||||
|
|
@ -1,88 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="Up" href="Smt.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><link title="Profiling functions" rel="Section" href="#2_Profilingfunctions">
|
||||
<link title="Main API of the solver" rel="Section" href="#2_MainAPIofthesolver">
|
||||
<title>Smt.Solver</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"> <a href="Smt.html">Up</a>
|
||||
</div>
|
||||
<center><h1>Module type <a href="type_Smt.Solver.html">Smt.Solver</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module type</span> Solver = <code class="code">sig</code> <a href="Smt.Solver.html">..</a> <code class="code">end</code></pre><hr width="100%">
|
||||
<br>
|
||||
This SMT solver is imperative in the sense that it maintains a global
|
||||
context. To create different instances of Alt-Ergo Zero use the
|
||||
functor <a href="Smt.Make.html"><code class="code">Smt.Make</code></a>.
|
||||
<p>
|
||||
|
||||
A typical use of this solver is to do the following :<pre><code class="code"> clear ();
|
||||
assume f_1;
|
||||
...
|
||||
assume f_n;
|
||||
check ();</code></pre><br>
|
||||
<pre><span id="TYPEstate"><span class="keyword">type</span> <code class="type"></code>state</span> </pre>
|
||||
<div class="info">
|
||||
The type of the internal state of the solver (see <a href="Smt.Solver.html#VALsave_state"><code class="code">Smt.Solver.save_state</code></a> and
|
||||
<a href="Smt.Solver.html#VALrestore_state"><code class="code">Smt.Solver.restore_state</code></a>).<br>
|
||||
</div>
|
||||
|
||||
<br>
|
||||
<span id="2_Profilingfunctions"><h2>Profiling functions</h2></span><br>
|
||||
<pre><span id="VALget_time"><span class="keyword">val</span> get_time</span> : <code class="type">unit -> float</code></pre><div class="info">
|
||||
<code class="code">get_time ()</code> returns the cumulated time spent in the solver in seconds.<br>
|
||||
</div>
|
||||
<pre><span id="VALget_calls"><span class="keyword">val</span> get_calls</span> : <code class="type">unit -> int</code></pre><div class="info">
|
||||
<code class="code">get_calls ()</code> returns the cumulated number of calls to <a href="Smt.Solver.html#VALcheck"><code class="code">Smt.Solver.check</code></a>.<br>
|
||||
</div>
|
||||
<br>
|
||||
<span id="2_MainAPIofthesolver"><h2>Main API of the solver</h2></span><br>
|
||||
<pre><span id="VALclear"><span class="keyword">val</span> clear</span> : <code class="type">unit -> unit</code></pre><div class="info">
|
||||
<code class="code">clear ()</code> clears the context of the solver. Use this after <a href="Smt.Solver.html#VALcheck"><code class="code">Smt.Solver.check</code></a>
|
||||
raised <a href="Smt.html#EXCEPTIONUnsat"><code class="code">Smt.Unsat</code></a> or if you want to restart the solver.<br>
|
||||
</div>
|
||||
<pre><span id="VALassume"><span class="keyword">val</span> assume</span> : <code class="type">?profiling:bool -> id:int -> <a href="Smt.Formula.html#TYPEt">Smt.Formula.t</a> -> unit</code></pre><div class="info">
|
||||
<code class="code">assume ~profiling:b f id</code> adds the formula <code class="code">f</code> to the context of the
|
||||
solver with idetifier <code class="code">id</code>.
|
||||
This function only performs unit propagation.<br>
|
||||
</div>
|
||||
<div class="param_info"><code class="code">profiling</code> : if set to <code class="code">true</code> then profiling information (time) will
|
||||
be computed (expensive because of system calls).
|
||||
<p>
|
||||
|
||||
<b>Raises</b> <a href="Smt.html#EXCEPTIONUnsat"><code class="code">Smt.Unsat</code></a> if the context becomes inconsistent after unit
|
||||
propagation.</div>
|
||||
<pre><span id="VALcheck"><span class="keyword">val</span> check</span> : <code class="type">?profiling:bool -> unit -> unit</code></pre><div class="info">
|
||||
<code class="code">check ()</code> runs Alt-Ergo Zero on its context. If <code class="code">()</code> is
|
||||
returned then the context is satifiable.<br>
|
||||
</div>
|
||||
<div class="param_info"><code class="code">profiling</code> : if set to <code class="code">true</code> then profiling information (time) will
|
||||
be computed (expensive because of system calls).
|
||||
<p>
|
||||
|
||||
<b>Raises</b> <a href="Smt.html#EXCEPTIONUnsat"><code class="code">Smt.Unsat</code></a> <code class="code">[id_1; ...; id_n]</code> if the context is unsatisfiable.
|
||||
<code class="code">id_1, ..., id_n</code> is the unsat core (returned as the identifiers of the
|
||||
formulas given to the solver).</div>
|
||||
<pre><span id="VALsave_state"><span class="keyword">val</span> save_state</span> : <code class="type">unit -> <a href="Smt.Solver.html#TYPEstate">state</a></code></pre><div class="info">
|
||||
<code class="code">save_state ()</code> returns a <b>copy</b> of the current state of the solver.<br>
|
||||
</div>
|
||||
<pre><span id="VALrestore_state"><span class="keyword">val</span> restore_state</span> : <code class="type"><a href="Smt.Solver.html#TYPEstate">state</a> -> unit</code></pre><div class="info">
|
||||
<code class="code">restore_state s</code> restores a previously saved state <code class="code">s</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALentails"><span class="keyword">val</span> entails</span> : <code class="type">?profiling:bool -> id:int -> <a href="Smt.Formula.html#TYPEt">Smt.Formula.t</a> -> bool</code></pre><div class="info">
|
||||
<code class="code">entails ~id f</code> returns <code class="code">true</code> if the context of the solver entails
|
||||
the formula <code class="code">f</code>. It doesn't modify the context of the solver (the state
|
||||
is saved when this function is called and restored on exit).<br>
|
||||
</div>
|
||||
</body></html>
|
||||
|
|
@ -1,49 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="previous" href="Smt.Type.html">
|
||||
<link rel="next" href="Smt.Variant.html">
|
||||
<link rel="Up" href="Smt.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt.Symbol</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"><a href="Smt.Type.html">Previous</a>
|
||||
<a href="Smt.html">Up</a>
|
||||
<a href="Smt.Variant.html">Next</a>
|
||||
</div>
|
||||
<center><h1>Module <a href="type_Smt.Symbol.html">Smt.Symbol</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module</span> Symbol: <code class="code">sig</code> <a href="Smt.Symbol.html">..</a> <code class="code">end</code></pre><span id="3_Functionsymbols"><h3>Function symbols</h3></span><br>
|
||||
<hr width="100%">
|
||||
<pre><span id="TYPEt"><span class="keyword">type</span> <code class="type"></code>t</span> = <code class="type"><a href="Hstring.html#TYPEt">Hstring.t</a></code> </pre>
|
||||
<div class="info">
|
||||
The type of function symbols<br>
|
||||
</div>
|
||||
|
||||
<pre><span id="VALdeclare"><span class="keyword">val</span> declare</span> : <code class="type"><a href="Hstring.html#TYPEt">Hstring.t</a> -> <a href="Smt.Type.html#TYPEt">Smt.Type.t</a> list -> <a href="Smt.Type.html#TYPEt">Smt.Type.t</a> -> unit</code></pre><div class="info">
|
||||
<code class="code">declare s [arg_1; ... ; arg_n] out</code> declares a new function
|
||||
symbol with type <code class="code"> (arg_1, ... , arg_n) -> out</code><br>
|
||||
</div>
|
||||
<pre><span id="VALtype_of"><span class="keyword">val</span> type_of</span> : <code class="type"><a href="Smt.Symbol.html#TYPEt">t</a> -> <a href="Smt.Type.html#TYPEt">Smt.Type.t</a> list * <a href="Smt.Type.html#TYPEt">Smt.Type.t</a></code></pre><div class="info">
|
||||
<code class="code">type_of x</code> returns the type of x.<br>
|
||||
</div>
|
||||
<pre><span id="VALhas_abstract_type"><span class="keyword">val</span> has_abstract_type</span> : <code class="type"><a href="Smt.Symbol.html#TYPEt">t</a> -> bool</code></pre><div class="info">
|
||||
<code class="code">has_abstract_type x</code> is <code class="code">true</code> if the type of x is abstract.<br>
|
||||
</div>
|
||||
<pre><span id="VALhas_type_proc"><span class="keyword">val</span> has_type_proc</span> : <code class="type"><a href="Smt.Symbol.html#TYPEt">t</a> -> bool</code></pre><div class="info">
|
||||
<code class="code">has_type_proc x</code> is <code class="code">true</code> if x has the type of a process
|
||||
identifier.<br>
|
||||
</div>
|
||||
<pre><span id="VALdeclared"><span class="keyword">val</span> declared</span> : <code class="type"><a href="Smt.Symbol.html#TYPEt">t</a> -> bool</code></pre><div class="info">
|
||||
<code class="code">declared x</code> is <code class="code">true</code> if <code class="code">x</code> is already declared.<br>
|
||||
</div>
|
||||
</body></html>
|
||||
|
|
@ -1,100 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="previous" href="Smt.Variant.html">
|
||||
<link rel="next" href="Smt.Formula.html">
|
||||
<link rel="Up" href="Smt.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt.Term</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"><a href="Smt.Variant.html">Previous</a>
|
||||
<a href="Smt.html">Up</a>
|
||||
<a href="Smt.Formula.html">Next</a>
|
||||
</div>
|
||||
<center><h1>Module <a href="type_Smt.Term.html">Smt.Term</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module</span> Term: <code class="code">sig</code> <a href="Smt.Term.html">..</a> <code class="code">end</code></pre><hr width="100%">
|
||||
<pre><span id="TYPEt"><span class="keyword">type</span> <code class="type"></code>t</span> </pre>
|
||||
<div class="info">
|
||||
The type of terms<br>
|
||||
</div>
|
||||
|
||||
<br><code><span id="TYPEoperator"><span class="keyword">type</span> <code class="type"></code>operator</span> = </code><table class="typetable">
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Plus</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><code class="code">+</code></td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Minus</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><code class="code">-</code></td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Mult</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><code class="code">*</code></td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Div</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><code class="code">/</code></td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">Modulo</span></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><code class="code">mod</code></td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr></table>
|
||||
|
||||
<div class="info">
|
||||
The type of operators<br>
|
||||
</div>
|
||||
|
||||
<pre><span id="VALmake_int"><span class="keyword">val</span> make_int</span> : <code class="type">Num.num -> <a href="Smt.Term.html#TYPEt">t</a></code></pre><div class="info">
|
||||
<code class="code">make_int n</code> creates an integer constant of value <code class="code">n</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALmake_real"><span class="keyword">val</span> make_real</span> : <code class="type">Num.num -> <a href="Smt.Term.html#TYPEt">t</a></code></pre><div class="info">
|
||||
<code class="code">make_real n</code> creates an real constant of value <code class="code">n</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALmake_app"><span class="keyword">val</span> make_app</span> : <code class="type"><a href="Smt.Symbol.html#TYPEt">Smt.Symbol.t</a> -> <a href="Smt.Term.html#TYPEt">t</a> list -> <a href="Smt.Term.html#TYPEt">t</a></code></pre><div class="info">
|
||||
<code class="code">make_app f l</code> creates the application of function symbol <code class="code">f</code> to a list
|
||||
of terms <code class="code">l</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALmake_arith"><span class="keyword">val</span> make_arith</span> : <code class="type"><a href="Smt.Term.html#TYPEoperator">operator</a> -> <a href="Smt.Term.html#TYPEt">t</a> -> <a href="Smt.Term.html#TYPEt">t</a> -> <a href="Smt.Term.html#TYPEt">t</a></code></pre><div class="info">
|
||||
<code class="code">make_arith op t1 t2</code> creates the term <code class="code">t1 <op> t2</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALmake_ite"><span class="keyword">val</span> make_ite</span> : <code class="type"><a href="Smt.Formula.html#TYPEt">Smt.Formula.t</a> -> <a href="Smt.Term.html#TYPEt">t</a> -> <a href="Smt.Term.html#TYPEt">t</a> -> <a href="Smt.Term.html#TYPEt">t</a></code></pre><div class="info">
|
||||
<code class="code">make_ite f t1 t2</code> creates the term <code class="code">if f then t1 else t2</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALis_int"><span class="keyword">val</span> is_int</span> : <code class="type"><a href="Smt.Term.html#TYPEt">t</a> -> bool</code></pre><div class="info">
|
||||
<code class="code">is_int x</code> is <code class="code">true</code> if the term <code class="code">x</code> has type int<br>
|
||||
</div>
|
||||
<pre><span id="VALis_real"><span class="keyword">val</span> is_real</span> : <code class="type"><a href="Smt.Term.html#TYPEt">t</a> -> bool</code></pre><div class="info">
|
||||
<code class="code">is_real x</code> is <code class="code">true</code> if the term <code class="code">x</code> has type real<br>
|
||||
</div>
|
||||
<pre><span id="VALt_true"><span class="keyword">val</span> t_true</span> : <code class="type"><a href="Smt.Term.html#TYPEt">t</a></code></pre><div class="info">
|
||||
<code class="code">t_true</code> is the boolean term <code class="code">true</code><br>
|
||||
</div>
|
||||
<pre><span id="VALt_false"><span class="keyword">val</span> t_false</span> : <code class="type"><a href="Smt.Term.html#TYPEt">t</a></code></pre><div class="info">
|
||||
<code class="code">t_false</code> is the boolean term <code class="code">false</code><br>
|
||||
</div>
|
||||
</body></html>
|
||||
|
|
@ -1,63 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="next" href="Smt.Symbol.html">
|
||||
<link rel="Up" href="Smt.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><link title="Builtin types " rel="Section" href="#4_Builtintypes">
|
||||
<link title="Declaring new types " rel="Section" href="#4_Declaringnewtypes">
|
||||
<title>Smt.Type</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"> <a href="Smt.html">Up</a>
|
||||
<a href="Smt.Symbol.html">Next</a>
|
||||
</div>
|
||||
<center><h1>Module <a href="type_Smt.Type.html">Smt.Type</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module</span> Type: <code class="code">sig</code> <a href="Smt.Type.html">..</a> <code class="code">end</code></pre><span id="3_Typing"><h3>Typing </h3></span><br>
|
||||
<hr width="100%">
|
||||
<pre><span id="TYPEt"><span class="keyword">type</span> <code class="type"></code>t</span> = <code class="type"><a href="Hstring.html#TYPEt">Hstring.t</a></code> </pre>
|
||||
<div class="info">
|
||||
The type of types in Alt-Ergo Zero<br>
|
||||
</div>
|
||||
|
||||
<br>
|
||||
<span id="4_Builtintypes"><h4>Builtin types </h4></span><br>
|
||||
<pre><span id="VALtype_int"><span class="keyword">val</span> type_int</span> : <code class="type"><a href="Smt.Type.html#TYPEt">t</a></code></pre><div class="info">
|
||||
The type of integers<br>
|
||||
</div>
|
||||
<pre><span id="VALtype_real"><span class="keyword">val</span> type_real</span> : <code class="type"><a href="Smt.Type.html#TYPEt">t</a></code></pre><div class="info">
|
||||
The type of reals<br>
|
||||
</div>
|
||||
<pre><span id="VALtype_bool"><span class="keyword">val</span> type_bool</span> : <code class="type"><a href="Smt.Type.html#TYPEt">t</a></code></pre><div class="info">
|
||||
The type of booleans<br>
|
||||
</div>
|
||||
<pre><span id="VALtype_proc"><span class="keyword">val</span> type_proc</span> : <code class="type"><a href="Smt.Type.html#TYPEt">t</a></code></pre><div class="info">
|
||||
The type processes (identifiers)<br>
|
||||
</div>
|
||||
<br>
|
||||
<span id="4_Declaringnewtypes"><h4>Declaring new types </h4></span><br>
|
||||
<pre><span id="VALdeclare"><span class="keyword">val</span> declare</span> : <code class="type"><a href="Hstring.html#TYPEt">Hstring.t</a> -> <a href="Hstring.html#TYPEt">Hstring.t</a> list -> unit</code></pre><div class="info">
|
||||
<ul>
|
||||
<li><code class="code">declare n cstrs</code> declares a new enumerated data-type with
|
||||
name <code class="code">n</code> and constructors <code class="code">cstrs</code>.</li>
|
||||
<li><code class="code">declare n []</code> declares a new abstract type with name <code class="code">n</code>.</li>
|
||||
</ul>
|
||||
<br>
|
||||
</div>
|
||||
<pre><span id="VALall_constructors"><span class="keyword">val</span> all_constructors</span> : <code class="type">unit -> <a href="Hstring.html#TYPEt">Hstring.t</a> list</code></pre><div class="info">
|
||||
<code class="code">all_constructors ()</code> returns a list of all the defined constructors.<br>
|
||||
</div>
|
||||
<pre><span id="VALconstructors"><span class="keyword">val</span> constructors</span> : <code class="type"><a href="Smt.Type.html#TYPEt">t</a> -> <a href="Hstring.html#TYPEt">Hstring.t</a> list</code></pre><div class="info">
|
||||
<code class="code">constructors ty</code> returns the list of constructors of <code class="code">ty</code> when type is
|
||||
an enumerated data-type, otherwise returns <code class="code">[]</code>.<br>
|
||||
</div>
|
||||
</body></html>
|
||||
|
|
@ -1,62 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="previous" href="Smt.Symbol.html">
|
||||
<link rel="next" href="Smt.Term.html">
|
||||
<link rel="Up" href="Smt.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt.Variant</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"><a href="Smt.Symbol.html">Previous</a>
|
||||
<a href="Smt.html">Up</a>
|
||||
<a href="Smt.Term.html">Next</a>
|
||||
</div>
|
||||
<center><h1>Module <a href="type_Smt.Variant.html">Smt.Variant</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module</span> Variant: <code class="code">sig</code> <a href="Smt.Variant.html">..</a> <code class="code">end</code></pre><span id="3_Variants"><h3>Variants</h3></span>
|
||||
<p>
|
||||
|
||||
The types of symbols (when they are enumerated data types) can be refined
|
||||
to substypes of their original type (i.e. a subset of their constructors).<br>
|
||||
<hr width="100%">
|
||||
<pre><span id="VALinit"><span class="keyword">val</span> init</span> : <code class="type">(<a href="Smt.Symbol.html#TYPEt">Smt.Symbol.t</a> * <a href="Smt.Type.html#TYPEt">Smt.Type.t</a>) list -> unit</code></pre><div class="info">
|
||||
<code class="code">init l</code> where <code class="code">l</code> is a list of pairs <code class="code">(s, ty)</code> initializes the
|
||||
type (and associated constructors) of each <code class="code">s</code> to its original type <code class="code">ty</code>.
|
||||
<p>
|
||||
|
||||
This function must be called with a list of all symbols before
|
||||
attempting to refine the types.<br>
|
||||
</div>
|
||||
<pre><span id="VALclose"><span class="keyword">val</span> close</span> : <code class="type">unit -> unit</code></pre><div class="info">
|
||||
<code class="code">close ()</code> will compute the smallest type possible for each symbol.
|
||||
<p>
|
||||
|
||||
This function must be called when all information has been added.<br>
|
||||
</div>
|
||||
<pre><span id="VALassign_constr"><span class="keyword">val</span> assign_constr</span> : <code class="type"><a href="Smt.Symbol.html#TYPEt">Smt.Symbol.t</a> -> <a href="Hstring.html#TYPEt">Hstring.t</a> -> unit</code></pre><div class="info">
|
||||
<code class="code">assign_constr s cstr</code> will add the constraint that the constructor
|
||||
<code class="code">cstr</code> must be in the type of <code class="code">s</code><br>
|
||||
</div>
|
||||
<pre><span id="VALassign_var"><span class="keyword">val</span> assign_var</span> : <code class="type"><a href="Smt.Symbol.html#TYPEt">Smt.Symbol.t</a> -> <a href="Smt.Symbol.html#TYPEt">Smt.Symbol.t</a> -> unit</code></pre><div class="info">
|
||||
<code class="code">assign_var x y</code> will add the constraint that the type of <code class="code">y</code> is a
|
||||
subtype of <code class="code">x</code> (use this function when <code class="code">x := y</code> appear in your
|
||||
program<br>
|
||||
</div>
|
||||
<pre><span id="VALprint"><span class="keyword">val</span> print</span> : <code class="type">unit -> unit</code></pre><div class="info">
|
||||
<code class="code">print ()</code> will output the computed refined types on std_err. This
|
||||
function is here only for debugging purposes. Use it afer <code class="code">close ()</code>.<br>
|
||||
</div>
|
||||
<pre><span id="VALget_variants"><span class="keyword">val</span> get_variants</span> : <code class="type"><a href="Smt.Symbol.html#TYPEt">Smt.Symbol.t</a> -> Hstring.HSet.t</code></pre><div class="info">
|
||||
<code class="code">get_variants s</code> returns a set of constructors, which is the refined
|
||||
type of <code class="code">s</code>.<br>
|
||||
</div>
|
||||
</body></html>
|
||||
105
doc/Smt.html
105
doc/Smt.html
|
|
@ -1,105 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link rel="next" href="Hstring.html">
|
||||
<link rel="Up" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><link title="Error handling " rel="Section" href="#2_Errorhandling">
|
||||
<link title="Typing " rel="Section" href="#2_Typing">
|
||||
<link title="Building terms" rel="Section" href="#2_Buildingterms">
|
||||
<link title="Building formulas" rel="Section" href="#2_Buildingformulas">
|
||||
<link title="The SMT solver" rel="Section" href="#2_TheSMTsolver">
|
||||
<title>Smt</title>
|
||||
</head>
|
||||
<body>
|
||||
<div class="navbar"> <a href="index.html">Up</a>
|
||||
<a href="Hstring.html">Next</a>
|
||||
</div>
|
||||
<center><h1>Module <a href="type_Smt.html">Smt</a></h1></center>
|
||||
<br>
|
||||
<pre><span class="keyword">module</span> Smt: <code class="code">sig</code> <a href="Smt.html">..</a> <code class="code">end</code></pre><b>The Alt-Ergo Zero SMT library</b>
|
||||
<p>
|
||||
|
||||
This SMT solver is derived from <a href="http://alt-ergo.lri.fr"> Alt-Ergo</a>. It
|
||||
uses an efficient SAT solver and supports the following quantifier free
|
||||
theories:<ul>
|
||||
<li>Equality and uninterpreted functions</li>
|
||||
<li>Arithmetic (linear, non-linear, integer, reals)</li>
|
||||
<li>Enumerated data-types</li>
|
||||
</ul>
|
||||
|
||||
This API makes heavy use of hash-consed strings. Please take a moment to
|
||||
look at <a href="Hstring.html"><code class="code">Hstring</code></a>.<br>
|
||||
<hr width="100%">
|
||||
<br>
|
||||
<span id="2_Errorhandling"><h2>Error handling </h2></span><br>
|
||||
<br><code><span id="TYPEerror"><span class="keyword">type</span> <code class="type"></code>error</span> = </code><table class="typetable">
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">DuplicateTypeName</span> <span class="keyword">of</span> <code class="type"><a href="Hstring.html#TYPEt">Hstring.t</a></code></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >raised when a type is already declared</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">DuplicateSymb</span> <span class="keyword">of</span> <code class="type"><a href="Hstring.html#TYPEt">Hstring.t</a></code></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >raised when a symbol is already declared</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">UnknownType</span> <span class="keyword">of</span> <code class="type"><a href="Hstring.html#TYPEt">Hstring.t</a></code></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >raised when the given type is not declared</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="keyword">|</span></code></td>
|
||||
<td align="left" valign="top" >
|
||||
<code><span class="constructor">UnknownSymb</span> <span class="keyword">of</span> <code class="type"><a href="Hstring.html#TYPEt">Hstring.t</a></code></code></td>
|
||||
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" >raised when the given symbol is not declared</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
|
||||
</tr></table>
|
||||
|
||||
|
||||
<pre><span id="EXCEPTIONError"><span class="keyword">exception</span> Error</span> <span class="keyword">of</span> <code class="type"><a href="Smt.html#TYPEerror">error</a></code></pre>
|
||||
<br>
|
||||
<span id="2_Typing"><h2>Typing </h2></span><br>
|
||||
<pre><span class="keyword">module</span> <a href="Smt.Type.html">Type</a>: <code class="code">sig</code> <a href="Smt.Type.html">..</a> <code class="code">end</code></pre><div class="info">
|
||||
Typing
|
||||
</div>
|
||||
<pre><span class="keyword">module</span> <a href="Smt.Symbol.html">Symbol</a>: <code class="code">sig</code> <a href="Smt.Symbol.html">..</a> <code class="code">end</code></pre><div class="info">
|
||||
Function symbols
|
||||
</div>
|
||||
<pre><span class="keyword">module</span> <a href="Smt.Variant.html">Variant</a>: <code class="code">sig</code> <a href="Smt.Variant.html">..</a> <code class="code">end</code></pre><div class="info">
|
||||
Variants
|
||||
</div>
|
||||
<br>
|
||||
<span id="2_Buildingterms"><h2>Building terms</h2></span><br>
|
||||
<pre><span class="keyword">module</span> <a href="Smt.Term.html">Term</a>: <code class="code">sig</code> <a href="Smt.Term.html">..</a> <code class="code">end</code></pre><br>
|
||||
<span id="2_Buildingformulas"><h2>Building formulas</h2></span><br>
|
||||
<pre><span class="keyword">module</span> <a href="Smt.Formula.html">Formula</a>: <code class="code">sig</code> <a href="Smt.Formula.html">..</a> <code class="code">end</code></pre><br>
|
||||
<span id="2_TheSMTsolver"><h2>The SMT solver</h2></span><br>
|
||||
<pre><span id="EXCEPTIONUnsat"><span class="keyword">exception</span> Unsat</span> <span class="keyword">of</span> <code class="type">int list</code></pre>
|
||||
<div class="info">
|
||||
The exception raised by <a href="Smt.Solver.html#VALcheck"><code class="code">Smt.Solver.check</code></a> and <a href="Smt.Solver.html#VALassume"><code class="code">Smt.Solver.assume</code></a> when
|
||||
the formula is unsatisfiable.<br>
|
||||
</div>
|
||||
<pre><span id="VALset_cc"><span class="keyword">val</span> set_cc</span> : <code class="type">bool -> unit</code></pre><div class="info">
|
||||
set_cc <code class="code">false</code> deactivates congruence closure algorithm
|
||||
(<code class="code">true</code> by default).<br>
|
||||
</div>
|
||||
<pre><span class="keyword">module type</span> <a href="Smt.Solver.html">Solver</a> = <code class="code">sig</code> <a href="Smt.Solver.html">..</a> <code class="code">end</code></pre><pre><span class="keyword">module</span> <a href="Smt.Make.html">Make</a>: <div class="sig_block"><code class="code">functor (</code><code class="code">Dummy</code><code class="code"> : </code><code class="code">sig</code><div class="sig_block"></div><code class="code">end</code><code class="code">) -> </code><code class="type"><a href="Smt.Solver.html">Solver</a></code><code class="type"> </code></div></pre><div class="info">
|
||||
Functor to create several instances of the solver
|
||||
</div>
|
||||
</body></html>
|
||||
|
|
@ -1,34 +0,0 @@
|
|||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
||||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title></title>
|
||||
</head>
|
||||
<body>
|
||||
<center><h1></h1></center>
|
||||
<a href="index_types.html">Index of types</a><br>
|
||||
<a href="index_exceptions.html">Index of exceptions</a><br>
|
||||
<a href="index_values.html">Index of values</a><br>
|
||||
<a href="index_modules.html">Index of modules</a><br>
|
||||
<a href="index_module_types.html">Index of module types</a><br>
|
||||
<br/><br>
|
||||
<table class="indextable">
|
||||
<tr><td><a href="Smt.html">Smt</a></td><td><div class="info">
|
||||
<b>The Alt-Ergo Zero SMT library</b>
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Hstring.html">Hstring</a></td><td><div class="info">
|
||||
<b>Hash-consed strings</b>
|
||||
</div>
|
||||
</td></tr>
|
||||
</table>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Index of class attributes</title>
|
||||
</head>
|
||||
<body>
|
||||
<center><h1>Index of class attributes</h1></center>
|
||||
<table>
|
||||
</table><br>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Index of class types</title>
|
||||
</head>
|
||||
<body>
|
||||
<center><h1>Index of class types</h1></center>
|
||||
<table>
|
||||
</table><br>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Index of classes</title>
|
||||
</head>
|
||||
<body>
|
||||
<center><h1>Index of classes</h1></center>
|
||||
<table>
|
||||
</table><br>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,29 +0,0 @@
|
|||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Index of exceptions</title>
|
||||
</head>
|
||||
<body>
|
||||
<center><h1>Index of exceptions</h1></center>
|
||||
<table>
|
||||
<tr><td align="left"><br>E</td></tr>
|
||||
<tr><td><a href="Smt.html#EXCEPTIONError">Error</a> [<a href="Smt.html">Smt</a>]</td>
|
||||
<td></td></tr>
|
||||
<tr><td align="left"><br>U</td></tr>
|
||||
<tr><td><a href="Smt.html#EXCEPTIONUnsat">Unsat</a> [<a href="Smt.html">Smt</a>]</td>
|
||||
<td><div class="info">
|
||||
The exception raised by <a href="Smt.Solver.html#VALcheck"><code class="code">Smt.Solver.check</code></a> and <a href="Smt.Solver.html#VALassume"><code class="code">Smt.Solver.assume</code></a> when
|
||||
the formula is unsatisfiable.
|
||||
</div>
|
||||
</td></tr>
|
||||
</table><br>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Index of class methods</title>
|
||||
</head>
|
||||
<body>
|
||||
<center><h1>Index of class methods</h1></center>
|
||||
<table>
|
||||
</table><br>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Index of module types</title>
|
||||
</head>
|
||||
<body>
|
||||
<center><h1>Index of module types</h1></center>
|
||||
<table>
|
||||
<tr><td align="left"><br>S</td></tr>
|
||||
<tr><td><a href="Smt.Solver.html">Solver</a> [<a href="Smt.html">Smt</a>]</td>
|
||||
<td></td></tr>
|
||||
</table><br>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,74 +0,0 @@
|
|||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Index of modules</title>
|
||||
</head>
|
||||
<body>
|
||||
<center><h1>Index of modules</h1></center>
|
||||
<table>
|
||||
<tr><td align="left"><br>F</td></tr>
|
||||
<tr><td><a href="Smt.Formula.html">Formula</a> [<a href="Smt.html">Smt</a>]</td>
|
||||
<td></td></tr>
|
||||
<tr><td align="left"><br>H</td></tr>
|
||||
<tr><td><a href="Hstring.H.html">H</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
Hash-tables indexed by hash-consed strings
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Hstring.HMap.html">HMap</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
Maps indexed by hash-consed strings
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Hstring.HSet.html">HSet</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
Sets of hash-consed strings
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Hstring.html">Hstring</a> </td>
|
||||
<td><div class="info">
|
||||
<b>Hash-consed strings</b>
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>M</td></tr>
|
||||
<tr><td><a href="Smt.Make.html">Make</a> [<a href="Smt.html">Smt</a>]</td>
|
||||
<td><div class="info">
|
||||
Functor to create several instances of the solver
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>S</td></tr>
|
||||
<tr><td><a href="Smt.html">Smt</a> </td>
|
||||
<td><div class="info">
|
||||
<b>The Alt-Ergo Zero SMT library</b>
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Symbol.html">Symbol</a> [<a href="Smt.html">Smt</a>]</td>
|
||||
<td><div class="info">
|
||||
Function symbols
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>T</td></tr>
|
||||
<tr><td><a href="Smt.Term.html">Term</a> [<a href="Smt.html">Smt</a>]</td>
|
||||
<td></td></tr>
|
||||
<tr><td><a href="Smt.Type.html">Type</a> [<a href="Smt.html">Smt</a>]</td>
|
||||
<td><div class="info">
|
||||
Typing
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>V</td></tr>
|
||||
<tr><td><a href="Smt.Variant.html">Variant</a> [<a href="Smt.html">Smt</a>]</td>
|
||||
<td><div class="info">
|
||||
Variants
|
||||
</div>
|
||||
</td></tr>
|
||||
</table><br>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,72 +0,0 @@
|
|||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Index of types</title>
|
||||
</head>
|
||||
<body>
|
||||
<center><h1>Index of types</h1></center>
|
||||
<table>
|
||||
<tr><td align="left"><br>C</td></tr>
|
||||
<tr><td><a href="Smt.Formula.html#TYPEcombinator">combinator</a> [<a href="Smt.Formula.html">Smt.Formula</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of operators
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Formula.html#TYPEcomparator">comparator</a> [<a href="Smt.Formula.html">Smt.Formula</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of comparators:
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>E</td></tr>
|
||||
<tr><td><a href="Smt.html#TYPEerror">error</a> [<a href="Smt.html">Smt</a>]</td>
|
||||
<td></td></tr>
|
||||
<tr><td align="left"><br>O</td></tr>
|
||||
<tr><td><a href="Smt.Term.html#TYPEoperator">operator</a> [<a href="Smt.Term.html">Smt.Term</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of operators
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>S</td></tr>
|
||||
<tr><td><a href="Smt.Solver.html#TYPEstate">state</a> [<a href="Smt.Solver.html">Smt.Solver</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of the internal state of the solver (see <a href="Smt.Solver.html#VALsave_state"><code class="code">Smt.Solver.save_state</code></a> and
|
||||
<a href="Smt.Solver.html#VALrestore_state"><code class="code">Smt.Solver.restore_state</code></a>).
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>T</td></tr>
|
||||
<tr><td><a href="Hstring.html#TYPEt">t</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of Hash-consed string
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Formula.html#TYPEt">t</a> [<a href="Smt.Formula.html">Smt.Formula</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of ground formulas
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Term.html#TYPEt">t</a> [<a href="Smt.Term.html">Smt.Term</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of terms
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Symbol.html#TYPEt">t</a> [<a href="Smt.Symbol.html">Smt.Symbol</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of function symbols
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Type.html#TYPEt">t</a> [<a href="Smt.Type.html">Smt.Type</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of types in Alt-Ergo Zero
|
||||
</div>
|
||||
</td></tr>
|
||||
</table><br>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,325 +0,0 @@
|
|||
<html>
|
||||
<head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Index of values</title>
|
||||
</head>
|
||||
<body>
|
||||
<center><h1>Index of values</h1></center>
|
||||
<table>
|
||||
<tr><td align="left"><br>A</td></tr>
|
||||
<tr><td><a href="Smt.Type.html#VALall_constructors">all_constructors</a> [<a href="Smt.Type.html">Smt.Type</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">all_constructors ()</code> returns a list of all the defined constructors.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Variant.html#VALassign_constr">assign_constr</a> [<a href="Smt.Variant.html">Smt.Variant</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">assign_constr s cstr</code> will add the constraint that the constructor
|
||||
<code class="code">cstr</code> must be in the type of <code class="code">s</code>
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Variant.html#VALassign_var">assign_var</a> [<a href="Smt.Variant.html">Smt.Variant</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">assign_var x y</code> will add the constraint that the type of <code class="code">y</code> is a
|
||||
subtype of <code class="code">x</code> (use this function when <code class="code">x := y</code> appear in your
|
||||
program
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Solver.html#VALassume">assume</a> [<a href="Smt.Solver.html">Smt.Solver</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">assume ~profiling:b f id</code> adds the formula <code class="code">f</code> to the context of the
|
||||
solver with idetifier <code class="code">id</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>C</td></tr>
|
||||
<tr><td><a href="Smt.Solver.html#VALcheck">check</a> [<a href="Smt.Solver.html">Smt.Solver</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">check ()</code> runs Alt-Ergo Zero on its context.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Solver.html#VALclear">clear</a> [<a href="Smt.Solver.html">Smt.Solver</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">clear ()</code> clears the context of the solver.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Variant.html#VALclose">close</a> [<a href="Smt.Variant.html">Smt.Variant</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">close ()</code> will compute the smallest type possible for each symbol.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALcompare">compare</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">compares x y</code> returns <code class="code">0</code> if <code class="code">x</code> and <code class="code">y</code> are equal, and is unspecified
|
||||
otherwise but provides a total ordering on hash-consed strings.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALcompare_list">compare_list</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">compare_list l1 l2</code> returns <code class="code">0</code> if and only if <code class="code">l1</code> is equal to <code class="code">l2</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Type.html#VALconstructors">constructors</a> [<a href="Smt.Type.html">Smt.Type</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">constructors ty</code> returns the list of constructors of <code class="code">ty</code> when type is
|
||||
an enumerated data-type, otherwise returns <code class="code">[]</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>D</td></tr>
|
||||
<tr><td><a href="Smt.Symbol.html#VALdeclare">declare</a> [<a href="Smt.Symbol.html">Smt.Symbol</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">declare s [arg_1; ... ; arg_n] out</code> declares a new function
|
||||
symbol with type <code class="code"> (arg_1, ... , arg_n) -> out</code>
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Type.html#VALdeclare">declare</a> [<a href="Smt.Type.html">Smt.Type</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">declare n cstrs</code> declares a new enumerated data-type with
|
||||
name <code class="code">n</code> and constructors <code class="code">cstrs</code>., <code class="code">declare n []</code> declares a new abstract type with name <code class="code">n</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Symbol.html#VALdeclared">declared</a> [<a href="Smt.Symbol.html">Smt.Symbol</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">declared x</code> is <code class="code">true</code> if <code class="code">x</code> is already declared.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>E</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALempty">empty</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
the empty (<code class="code">""</code>) hash-consed string.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Solver.html#VALentails">entails</a> [<a href="Smt.Solver.html">Smt.Solver</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">entails ~id f</code> returns <code class="code">true</code> if the context of the solver entails
|
||||
the formula <code class="code">f</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALequal">equal</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">equal x y</code> returns <code class="code">true</code> if <code class="code">x</code> and <code class="code">y</code> are the same hash-consed string
|
||||
(constant time).
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>F</td></tr>
|
||||
<tr><td><a href="Smt.Formula.html#VALf_false">f_false</a> [<a href="Smt.Formula.html">Smt.Formula</a>]</td>
|
||||
<td><div class="info">
|
||||
The formula which represents <code class="code">false</code>
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Formula.html#VALf_true">f_true</a> [<a href="Smt.Formula.html">Smt.Formula</a>]</td>
|
||||
<td><div class="info">
|
||||
The formula which represents <code class="code">true</code>
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>G</td></tr>
|
||||
<tr><td><a href="Smt.Solver.html#VALget_calls">get_calls</a> [<a href="Smt.Solver.html">Smt.Solver</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">get_calls ()</code> returns the cumulated number of calls to <a href="Smt.Solver.html#VALcheck"><code class="code">Smt.Solver.check</code></a>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Solver.html#VALget_time">get_time</a> [<a href="Smt.Solver.html">Smt.Solver</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">get_time ()</code> returns the cumulated time spent in the solver in seconds.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Variant.html#VALget_variants">get_variants</a> [<a href="Smt.Variant.html">Smt.Variant</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">get_variants s</code> returns a set of constructors, which is the refined
|
||||
type of <code class="code">s</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>H</td></tr>
|
||||
<tr><td><a href="Smt.Symbol.html#VALhas_abstract_type">has_abstract_type</a> [<a href="Smt.Symbol.html">Smt.Symbol</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">has_abstract_type x</code> is <code class="code">true</code> if the type of x is abstract.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Symbol.html#VALhas_type_proc">has_type_proc</a> [<a href="Smt.Symbol.html">Smt.Symbol</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">has_type_proc x</code> is <code class="code">true</code> if x has the type of a process
|
||||
identifier.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALhash">hash</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">hash x</code> returns the integer (hash) associated to <code class="code">x</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>I</td></tr>
|
||||
<tr><td><a href="Smt.Variant.html#VALinit">init</a> [<a href="Smt.Variant.html">Smt.Variant</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">init l</code> where <code class="code">l</code> is a list of pairs <code class="code">(s, ty)</code> initializes the
|
||||
type (and associated constructors) of each <code class="code">s</code> to its original type <code class="code">ty</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Term.html#VALis_int">is_int</a> [<a href="Smt.Term.html">Smt.Term</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">is_int x</code> is <code class="code">true</code> if the term <code class="code">x</code> has type int
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Term.html#VALis_real">is_real</a> [<a href="Smt.Term.html">Smt.Term</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">is_real x</code> is <code class="code">true</code> if the term <code class="code">x</code> has type real
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>L</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALlist_assoc">list_assoc</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">list_assoc x l</code> returns the element associated with <code class="code">x</code> in the list of
|
||||
pairs <code class="code">l</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALlist_mem">list_mem</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">list_mem x l</code> is <code class="code">true</code> if and only if <code class="code">x</code> is equal to an element of <code class="code">l</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALlist_mem_assoc">list_mem_assoc</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
Same as <a href="Hstring.html#VALlist_assoc"><code class="code">Hstring.list_assoc</code></a>, but simply returns <code class="code">true</code> if a binding exists, and
|
||||
<code class="code">false</code> if no bindings exist for the given key.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALlist_mem_couple">list_mem_couple</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">list_mem_couple (x,y) l</code> is <code class="code">true</code> if and only if <code class="code">(x,y)</code> is equal to an
|
||||
element of <code class="code">l</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>M</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALmake">make</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">make s</code> builds ans returns a hash-consed string from <code class="code">s</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Formula.html#VALmake">make</a> [<a href="Smt.Formula.html">Smt.Formula</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">make cmb [f_1; ...; f_n]</code> creates the formula
|
||||
<code class="code">(f_1 <cmb> ... <cmb> f_n)</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Term.html#VALmake_app">make_app</a> [<a href="Smt.Term.html">Smt.Term</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">make_app f l</code> creates the application of function symbol <code class="code">f</code> to a list
|
||||
of terms <code class="code">l</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Term.html#VALmake_arith">make_arith</a> [<a href="Smt.Term.html">Smt.Term</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">make_arith op t1 t2</code> creates the term <code class="code">t1 <op> t2</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Formula.html#VALmake_cnf">make_cnf</a> [<a href="Smt.Formula.html">Smt.Formula</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">make_cnf f</code> returns a conjunctive normal form of <code class="code">f</code> under the form: a
|
||||
list (which is a conjunction) of lists (which are disjunctions) of
|
||||
literals.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Term.html#VALmake_int">make_int</a> [<a href="Smt.Term.html">Smt.Term</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">make_int n</code> creates an integer constant of value <code class="code">n</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Term.html#VALmake_ite">make_ite</a> [<a href="Smt.Term.html">Smt.Term</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">make_ite f t1 t2</code> creates the term <code class="code">if f then t1 else t2</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Formula.html#VALmake_lit">make_lit</a> [<a href="Smt.Formula.html">Smt.Formula</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">make_lit cmp [t1; t2]</code> creates the literal <code class="code">(t1 <cmp> t2)</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Term.html#VALmake_real">make_real</a> [<a href="Smt.Term.html">Smt.Term</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">make_real n</code> creates an real constant of value <code class="code">n</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>P</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALprint">print</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
Prints a list of hash-consed strings on a formatter.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Formula.html#VALprint">print</a> [<a href="Smt.Formula.html">Smt.Formula</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">print fmt f</code> prints the formula on the formatter <code class="code">fmt</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Variant.html#VALprint">print</a> [<a href="Smt.Variant.html">Smt.Variant</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">print ()</code> will output the computed refined types on std_err.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>R</td></tr>
|
||||
<tr><td><a href="Smt.Solver.html#VALrestore_state">restore_state</a> [<a href="Smt.Solver.html">Smt.Solver</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">restore_state s</code> restores a previously saved state <code class="code">s</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>S</td></tr>
|
||||
<tr><td><a href="Smt.Solver.html#VALsave_state">save_state</a> [<a href="Smt.Solver.html">Smt.Solver</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">save_state ()</code> returns a <b>copy</b> of the current state of the solver.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.html#VALset_cc">set_cc</a> [<a href="Smt.html">Smt</a>]</td>
|
||||
<td><div class="info">
|
||||
set_cc <code class="code">false</code> deactivates congruence closure algorithm
|
||||
(<code class="code">true</code> by default).
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>T</td></tr>
|
||||
<tr><td><a href="Smt.Term.html#VALt_false">t_false</a> [<a href="Smt.Term.html">Smt.Term</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">t_false</code> is the boolean term <code class="code">false</code>
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Term.html#VALt_true">t_true</a> [<a href="Smt.Term.html">Smt.Term</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">t_true</code> is the boolean term <code class="code">true</code>
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Type.html#VALtype_bool">type_bool</a> [<a href="Smt.Type.html">Smt.Type</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of booleans
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Type.html#VALtype_int">type_int</a> [<a href="Smt.Type.html">Smt.Type</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of integers
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Symbol.html#VALtype_of">type_of</a> [<a href="Smt.Symbol.html">Smt.Symbol</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">type_of x</code> returns the type of x.
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Type.html#VALtype_proc">type_proc</a> [<a href="Smt.Type.html">Smt.Type</a>]</td>
|
||||
<td><div class="info">
|
||||
The type processes (identifiers)
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td><a href="Smt.Type.html#VALtype_real">type_real</a> [<a href="Smt.Type.html">Smt.Type</a>]</td>
|
||||
<td><div class="info">
|
||||
The type of reals
|
||||
</div>
|
||||
</td></tr>
|
||||
<tr><td align="left"><br>V</td></tr>
|
||||
<tr><td><a href="Hstring.html#VALview">view</a> [<a href="Hstring.html">Hstring</a>]</td>
|
||||
<td><div class="info">
|
||||
<code class="code">view hs</code> returns the string corresponding to <code class="code">hs</code>.
|
||||
</div>
|
||||
</td></tr>
|
||||
</table><br>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,34 +0,0 @@
|
|||
a:visited {color : #416DFF; text-decoration : none; }
|
||||
a:link {color : #416DFF; text-decoration : none;}
|
||||
a:hover {color : Red; text-decoration : none; background-color: #5FFF88}
|
||||
a:active {color : Red; text-decoration : underline; }
|
||||
.keyword { font-weight : bold ; color : Red }
|
||||
.keywordsign { color : #C04600 }
|
||||
.superscript { font-size : 4 }
|
||||
.subscript { font-size : 4 }
|
||||
.comment { color : Green }
|
||||
.constructor { color : Blue }
|
||||
.type { color : #5C6585 }
|
||||
.string { color : Maroon }
|
||||
.warning { color : Red ; font-weight : bold }
|
||||
.info { margin-left : 3em; margin-right : 3em }
|
||||
.param_info { margin-top: 4px; margin-left : 3em; margin-right : 3em }
|
||||
.code { color : #465F91 ; }
|
||||
h1 { font-size : 20pt ; text-align: center; }
|
||||
h2 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90BDFF ;padding: 2px; }
|
||||
h3 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90DDFF ;padding: 2px; }
|
||||
h4 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90EDFF ;padding: 2px; }
|
||||
h5 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90FDFF ;padding: 2px; }
|
||||
h6 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #C0FFFF ; padding: 2px; }
|
||||
div.h7 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #E0FFFF ; padding: 2px; }
|
||||
div.h8 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #F0FFFF ; padding: 2px; }
|
||||
div.h9 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #FFFFFF ; padding: 2px; }
|
||||
.typetable { border-style : hidden }
|
||||
.indextable { border-style : hidden }
|
||||
.paramstable { border-style : hidden ; padding: 5pt 5pt}
|
||||
body { background-color : White }
|
||||
tr { background-color : White }
|
||||
td.typefieldcomment { background-color : #FFFFFF ; font-size: smaller ;}
|
||||
pre { margin-bottom: 4px }
|
||||
div.sig_block {margin-left: 2em}
|
||||
*:target { background: yellow; }
|
||||
|
|
@ -1,29 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Hstring.H</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> key = t<br>
|
||||
<span class="keyword">type</span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> create : int <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> clear : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> copy : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> add : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> remove : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> find : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> find_all : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a list<br>
|
||||
<span class="keyword">val</span> replace : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> mem : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> iter : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> fold : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="keywordsign">'</span>b) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="keywordsign">'</span>b<br>
|
||||
<span class="keyword">val</span> length : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">end</span></code></body></html>
|
||||
|
|
@ -1,42 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Hstring.HMap</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> key = t<br>
|
||||
<span class="keyword">type</span> +<span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> empty : <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> is_empty : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> mem : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> add : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> singleton : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> remove : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> merge :<br>
|
||||
(key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a option <span class="keywordsign">-></span> <span class="keywordsign">'</span>b option <span class="keywordsign">-></span> <span class="keywordsign">'</span>c option) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>b t <span class="keywordsign">-></span> <span class="keywordsign">'</span>c t<br>
|
||||
<span class="keyword">val</span> compare : (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> int) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> equal : (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> iter : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> fold : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="keywordsign">'</span>b) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="keywordsign">'</span>b<br>
|
||||
<span class="keyword">val</span> for_all : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> exists : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> filter : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> partition : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t * <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> cardinal : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> bindings : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> (key * <span class="keywordsign">'</span>a) list<br>
|
||||
<span class="keyword">val</span> min_binding : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key * <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> max_binding : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key * <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> choose : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key * <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> split : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t * <span class="keywordsign">'</span>a option * <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> find : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> map : (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>b t<br>
|
||||
<span class="keyword">val</span> mapi : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>b t<br>
|
||||
<span class="keyword">end</span></code></body></html>
|
||||
|
|
@ -1,41 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Hstring.HSet</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> elt = t<br>
|
||||
<span class="keyword">type</span> t<br>
|
||||
<span class="keyword">val</span> empty : t<br>
|
||||
<span class="keyword">val</span> is_empty : t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> mem : elt <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> add : elt <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> singleton : elt <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> remove : elt <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> union : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> inter : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> diff : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> compare : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> equal : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> subset : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> iter : (elt <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> fold : (elt <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> for_all : (elt <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> exists : (elt <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> filter : (elt <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> partition : (elt <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t * t<br>
|
||||
<span class="keyword">val</span> cardinal : t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> elements : t <span class="keywordsign">-></span> elt list<br>
|
||||
<span class="keyword">val</span> min_elt : t <span class="keywordsign">-></span> elt<br>
|
||||
<span class="keyword">val</span> max_elt : t <span class="keywordsign">-></span> elt<br>
|
||||
<span class="keyword">val</span> choose : t <span class="keywordsign">-></span> elt<br>
|
||||
<span class="keyword">val</span> split : elt <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t * bool * t<br>
|
||||
<span class="keyword">end</span></code></body></html>
|
||||
|
|
@ -1,105 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Hstring</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> t = string <span class="constructor">Hashcons</span>.hash_consed<br>
|
||||
<span class="keyword">val</span> make : string <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t<br>
|
||||
<span class="keyword">val</span> view : <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> string<br>
|
||||
<span class="keyword">val</span> equal : <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> compare : <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> hash : <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> empty : <span class="constructor">Hstring</span>.t<br>
|
||||
<span class="keyword">val</span> list_assoc : <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> (<span class="constructor">Hstring</span>.t * <span class="keywordsign">'</span>a) list <span class="keywordsign">-></span> <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> list_mem_assoc : <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> (<span class="constructor">Hstring</span>.t * <span class="keywordsign">'</span>a) list <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> list_mem : <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t list <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> list_mem_couple :<br>
|
||||
<span class="constructor">Hstring</span>.t * <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> (<span class="constructor">Hstring</span>.t * <span class="constructor">Hstring</span>.t) list <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> compare_list : <span class="constructor">Hstring</span>.t list <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t list <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> print : <span class="constructor">Format</span>.formatter <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">module</span> <span class="constructor">H</span> :<br>
|
||||
<span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> key = t<br>
|
||||
<span class="keyword">type</span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> create : int <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> clear : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> copy : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> add : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> remove : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> find : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> find_all : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a list<br>
|
||||
<span class="keyword">val</span> replace : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> mem : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> iter : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> fold : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="keywordsign">'</span>b) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="keywordsign">'</span>b<br>
|
||||
<span class="keyword">val</span> length : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">end</span><br>
|
||||
<span class="keyword">module</span> <span class="constructor">HSet</span> :<br>
|
||||
<span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> elt = t<br>
|
||||
<span class="keyword">type</span> t<br>
|
||||
<span class="keyword">val</span> empty : t<br>
|
||||
<span class="keyword">val</span> is_empty : t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> mem : elt <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> add : elt <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> singleton : elt <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> remove : elt <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> union : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> inter : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> diff : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> compare : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> equal : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> subset : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> iter : (elt <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> fold : (elt <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> for_all : (elt <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> exists : (elt <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> filter : (elt <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t<br>
|
||||
<span class="keyword">val</span> partition : (elt <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t * t<br>
|
||||
<span class="keyword">val</span> cardinal : t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> elements : t <span class="keywordsign">-></span> elt list<br>
|
||||
<span class="keyword">val</span> min_elt : t <span class="keywordsign">-></span> elt<br>
|
||||
<span class="keyword">val</span> max_elt : t <span class="keywordsign">-></span> elt<br>
|
||||
<span class="keyword">val</span> choose : t <span class="keywordsign">-></span> elt<br>
|
||||
<span class="keyword">val</span> split : elt <span class="keywordsign">-></span> t <span class="keywordsign">-></span> t * bool * t<br>
|
||||
<span class="keyword">end</span><br>
|
||||
<span class="keyword">module</span> <span class="constructor">HMap</span> :<br>
|
||||
<span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> key = t<br>
|
||||
<span class="keyword">type</span> +<span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> empty : <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> is_empty : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> mem : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> add : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> singleton : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> remove : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> merge :<br>
|
||||
(key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a option <span class="keywordsign">-></span> <span class="keywordsign">'</span>b option <span class="keywordsign">-></span> <span class="keywordsign">'</span>c option) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>b t <span class="keywordsign">-></span> <span class="keywordsign">'</span>c t<br>
|
||||
<span class="keyword">val</span> compare : (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> int) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> equal : (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> iter : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> fold : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="keywordsign">'</span>b) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="keywordsign">'</span>b<br>
|
||||
<span class="keyword">val</span> for_all : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> exists : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> filter : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> partition : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t * <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> cardinal : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> bindings : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> (key * <span class="keywordsign">'</span>a) list<br>
|
||||
<span class="keyword">val</span> min_binding : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key * <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> max_binding : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key * <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> choose : <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> key * <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> split : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t * <span class="keywordsign">'</span>a option * <span class="keywordsign">'</span>a t<br>
|
||||
<span class="keyword">val</span> find : key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a<br>
|
||||
<span class="keyword">val</span> map : (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>b t<br>
|
||||
<span class="keyword">val</span> mapi : (key <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a t <span class="keywordsign">-></span> <span class="keywordsign">'</span>b t<br>
|
||||
<span class="keyword">end</span><br>
|
||||
<span class="keyword">end</span></code></body></html>
|
||||
|
|
@ -1,26 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt.Formula</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> comparator = <span class="constructor">Eq</span> <span class="keywordsign">|</span> <span class="constructor">Neq</span> <span class="keywordsign">|</span> <span class="constructor">Le</span> <span class="keywordsign">|</span> <span class="constructor">Lt</span><br>
|
||||
<span class="keyword">type</span> combinator = <span class="constructor">And</span> <span class="keywordsign">|</span> <span class="constructor">Or</span> <span class="keywordsign">|</span> <span class="constructor">Imp</span> <span class="keywordsign">|</span> <span class="constructor">Not</span><br>
|
||||
<span class="keyword">type</span> t =<br>
|
||||
<span class="constructor">Lit</span> <span class="keyword">of</span> <span class="constructor">Literal</span>.<span class="constructor">LT</span>.t<br>
|
||||
<span class="keywordsign">|</span> <span class="constructor">Comb</span> <span class="keyword">of</span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.combinator * <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t list<br>
|
||||
<span class="keyword">val</span> f_true : <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t<br>
|
||||
<span class="keyword">val</span> f_false : <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t<br>
|
||||
<span class="keyword">val</span> make_lit : <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.comparator <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t list <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t<br>
|
||||
<span class="keyword">val</span> make : <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.combinator <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t list <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t<br>
|
||||
<span class="keyword">val</span> make_cnf : <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t <span class="keywordsign">-></span> <span class="constructor">Literal</span>.<span class="constructor">LT</span>.t list list<br>
|
||||
<span class="keyword">val</span> print : <span class="constructor">Format</span>.formatter <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">end</span></code></body></html>
|
||||
|
|
@ -1,14 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt.Make</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">functor</span> (<span class="constructor">Dummy</span> : <span class="keyword">sig</span> <span class="keyword">end</span>) <span class="keywordsign">-></span> <span class="constructor">Solver</span></code></body></html>
|
||||
|
|
@ -1,24 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt.Solver</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> state<br>
|
||||
<span class="keyword">val</span> get_time : unit <span class="keywordsign">-></span> float<br>
|
||||
<span class="keyword">val</span> get_calls : unit <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> clear : unit <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> assume : ?profiling:bool <span class="keywordsign">-></span> id:int <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> check : ?profiling:bool <span class="keywordsign">-></span> unit <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> save_state : unit <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Solver</span>.state<br>
|
||||
<span class="keyword">val</span> restore_state : <span class="constructor">Smt</span>.<span class="constructor">Solver</span>.state <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> entails : ?profiling:bool <span class="keywordsign">-></span> id:int <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">end</span></code></body></html>
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt.Symbol</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> t = <span class="constructor">Hstring</span>.t<br>
|
||||
<span class="keyword">val</span> declare : <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t list <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> type_of : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t list * <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t<br>
|
||||
<span class="keyword">val</span> has_abstract_type : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> has_type_proc : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> declared : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">end</span></code></body></html>
|
||||
|
|
@ -1,27 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt.Term</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> t<br>
|
||||
<span class="keyword">type</span> operator = <span class="constructor">Plus</span> <span class="keywordsign">|</span> <span class="constructor">Minus</span> <span class="keywordsign">|</span> <span class="constructor">Mult</span> <span class="keywordsign">|</span> <span class="constructor">Div</span> <span class="keywordsign">|</span> <span class="constructor">Modulo</span><br>
|
||||
<span class="keyword">val</span> make_int : <span class="constructor">Num</span>.num <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> make_real : <span class="constructor">Num</span>.num <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> make_app : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t list <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> make_arith :<br>
|
||||
<span class="constructor">Smt</span>.<span class="constructor">Term</span>.operator <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> make_ite : <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> is_int : <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> is_real : <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> t_true : <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> t_false : <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">end</span></code></body></html>
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt.Type</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> t = <span class="constructor">Hstring</span>.t<br>
|
||||
<span class="keyword">val</span> type_int : <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t<br>
|
||||
<span class="keyword">val</span> type_real : <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t<br>
|
||||
<span class="keyword">val</span> type_bool : <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t<br>
|
||||
<span class="keyword">val</span> type_proc : <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t<br>
|
||||
<span class="keyword">val</span> declare : <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t list <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> all_constructors : unit <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t list<br>
|
||||
<span class="keyword">val</span> constructors : <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t list<br>
|
||||
<span class="keyword">end</span></code></body></html>
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt.Variant</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">sig</span><br>
|
||||
<span class="keyword">val</span> init : (<span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t * <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t) list <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> close : unit <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> assign_constr : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> assign_var : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> print : unit <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> get_variants : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.<span class="constructor">HSet</span>.t<br>
|
||||
<span class="keyword">end</span></code></body></html>
|
||||
|
|
@ -1,96 +0,0 @@
|
|||
<html><head>
|
||||
<link rel="stylesheet" href="style.css" type="text/css">
|
||||
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
|
||||
<link rel="Start" href="index.html">
|
||||
<link title="Index of types" rel=Appendix href="index_types.html">
|
||||
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
|
||||
<link title="Index of values" rel=Appendix href="index_values.html">
|
||||
<link title="Index of modules" rel=Appendix href="index_modules.html">
|
||||
<link title="Index of module types" rel=Appendix href="index_module_types.html">
|
||||
<link title="Smt" rel="Chapter" href="Smt.html">
|
||||
<link title="Hstring" rel="Chapter" href="Hstring.html"><title>Smt</title>
|
||||
</head>
|
||||
<body>
|
||||
<code class="code"><span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> error =<br>
|
||||
<span class="constructor">DuplicateTypeName</span> <span class="keyword">of</span> <span class="constructor">Hstring</span>.t<br>
|
||||
<span class="keywordsign">|</span> <span class="constructor">DuplicateSymb</span> <span class="keyword">of</span> <span class="constructor">Hstring</span>.t<br>
|
||||
<span class="keywordsign">|</span> <span class="constructor">UnknownType</span> <span class="keyword">of</span> <span class="constructor">Hstring</span>.t<br>
|
||||
<span class="keywordsign">|</span> <span class="constructor">UnknownSymb</span> <span class="keyword">of</span> <span class="constructor">Hstring</span>.t<br>
|
||||
<span class="keyword">exception</span> <span class="constructor">Error</span> <span class="keyword">of</span> <span class="constructor">Smt</span>.error<br>
|
||||
<span class="keyword">module</span> <span class="constructor">Type</span> :<br>
|
||||
<span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> t = <span class="constructor">Hstring</span>.t<br>
|
||||
<span class="keyword">val</span> type_int : <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t<br>
|
||||
<span class="keyword">val</span> type_real : <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t<br>
|
||||
<span class="keyword">val</span> type_bool : <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t<br>
|
||||
<span class="keyword">val</span> type_proc : <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t<br>
|
||||
<span class="keyword">val</span> declare : <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t list <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> all_constructors : unit <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t list<br>
|
||||
<span class="keyword">val</span> constructors : <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t list<br>
|
||||
<span class="keyword">end</span><br>
|
||||
<span class="keyword">module</span> <span class="constructor">Symbol</span> :<br>
|
||||
<span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> t = <span class="constructor">Hstring</span>.t<br>
|
||||
<span class="keyword">val</span> declare : <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t list <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> type_of : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t list * <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t<br>
|
||||
<span class="keyword">val</span> has_abstract_type : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> has_type_proc : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> declared : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">end</span><br>
|
||||
<span class="keyword">module</span> <span class="constructor">Variant</span> :<br>
|
||||
<span class="keyword">sig</span><br>
|
||||
<span class="keyword">val</span> init : (<span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t * <span class="constructor">Smt</span>.<span class="constructor">Type</span>.t) list <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> close : unit <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> assign_constr : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> assign_var : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> print : unit <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> get_variants : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> <span class="constructor">Hstring</span>.<span class="constructor">HSet</span>.t<br>
|
||||
<span class="keyword">end</span><br>
|
||||
<span class="keyword">module</span> <span class="keyword">rec</span> <span class="constructor">Term</span> :<br>
|
||||
<span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> t<br>
|
||||
<span class="keyword">type</span> operator = <span class="constructor">Plus</span> <span class="keywordsign">|</span> <span class="constructor">Minus</span> <span class="keywordsign">|</span> <span class="constructor">Mult</span> <span class="keywordsign">|</span> <span class="constructor">Div</span> <span class="keywordsign">|</span> <span class="constructor">Modulo</span><br>
|
||||
<span class="keyword">val</span> make_int : <span class="constructor">Num</span>.num <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> make_real : <span class="constructor">Num</span>.num <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> make_app : <span class="constructor">Smt</span>.<span class="constructor">Symbol</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t list <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> make_arith :<br>
|
||||
<span class="constructor">Smt</span>.<span class="constructor">Term</span>.operator <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> make_ite : <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> is_int : <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> is_real : <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">val</span> t_true : <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">val</span> t_false : <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t<br>
|
||||
<span class="keyword">end</span><br>
|
||||
<span class="keyword">and</span> <span class="constructor">Formula</span> :<br>
|
||||
<span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> comparator = <span class="constructor">Eq</span> <span class="keywordsign">|</span> <span class="constructor">Neq</span> <span class="keywordsign">|</span> <span class="constructor">Le</span> <span class="keywordsign">|</span> <span class="constructor">Lt</span><br>
|
||||
<span class="keyword">type</span> combinator = <span class="constructor">And</span> <span class="keywordsign">|</span> <span class="constructor">Or</span> <span class="keywordsign">|</span> <span class="constructor">Imp</span> <span class="keywordsign">|</span> <span class="constructor">Not</span><br>
|
||||
<span class="keyword">type</span> t =<br>
|
||||
<span class="constructor">Lit</span> <span class="keyword">of</span> <span class="constructor">Literal</span>.<span class="constructor">LT</span>.t<br>
|
||||
<span class="keywordsign">|</span> <span class="constructor">Comb</span> <span class="keyword">of</span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.combinator * <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t list<br>
|
||||
<span class="keyword">val</span> f_true : <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t<br>
|
||||
<span class="keyword">val</span> f_false : <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t<br>
|
||||
<span class="keyword">val</span> make_lit :<br>
|
||||
<span class="constructor">Smt</span>.<span class="constructor">Formula</span>.comparator <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Term</span>.t list <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t<br>
|
||||
<span class="keyword">val</span> make :<br>
|
||||
<span class="constructor">Smt</span>.<span class="constructor">Formula</span>.combinator <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t list <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t<br>
|
||||
<span class="keyword">val</span> make_cnf : <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t <span class="keywordsign">-></span> <span class="constructor">Literal</span>.<span class="constructor">LT</span>.t list list<br>
|
||||
<span class="keyword">val</span> print : <span class="constructor">Format</span>.formatter <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">end</span><br>
|
||||
<span class="keyword">exception</span> <span class="constructor">Unsat</span> <span class="keyword">of</span> int list<br>
|
||||
<span class="keyword">val</span> set_cc : bool <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">module</span> <span class="keyword">type</span> <span class="constructor">Solver</span> =<br>
|
||||
<span class="keyword">sig</span><br>
|
||||
<span class="keyword">type</span> state<br>
|
||||
<span class="keyword">val</span> get_time : unit <span class="keywordsign">-></span> float<br>
|
||||
<span class="keyword">val</span> get_calls : unit <span class="keywordsign">-></span> int<br>
|
||||
<span class="keyword">val</span> clear : unit <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> assume : ?profiling:bool <span class="keywordsign">-></span> id:int <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> check : ?profiling:bool <span class="keywordsign">-></span> unit <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> save_state : unit <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Solver</span>.state<br>
|
||||
<span class="keyword">val</span> restore_state : <span class="constructor">Smt</span>.<span class="constructor">Solver</span>.state <span class="keywordsign">-></span> unit<br>
|
||||
<span class="keyword">val</span> entails : ?profiling:bool <span class="keywordsign">-></span> id:int <span class="keywordsign">-></span> <span class="constructor">Smt</span>.<span class="constructor">Formula</span>.t <span class="keywordsign">-></span> bool<br>
|
||||
<span class="keyword">end</span><br>
|
||||
<span class="keyword">module</span> <span class="constructor">Make</span> : <span class="keyword">functor</span> (<span class="constructor">Dummy</span> : <span class="keyword">sig</span> <span class="keyword">end</span>) <span class="keywordsign">-></span> <span class="constructor">Solver</span><br>
|
||||
<span class="keyword">end</span></code></body></html>
|
||||
17
msat.mlpack
17
msat.mlpack
|
|
@ -3,3 +3,20 @@ Formula_intf
|
|||
Solver
|
||||
Solver_types
|
||||
Theory_intf
|
||||
|
||||
#Arith
|
||||
#Cc
|
||||
#Combine
|
||||
#Exception
|
||||
#Fm
|
||||
#Intervals
|
||||
#Literal
|
||||
#Polynome
|
||||
#Smt
|
||||
#Sum
|
||||
#Symbols
|
||||
#Term
|
||||
#Ty
|
||||
#Uf
|
||||
#Use
|
||||
|
||||
|
|
|
|||
30
msat.odocl
30
msat.odocl
|
|
@ -4,19 +4,19 @@ sat/Solver
|
|||
sat/Solver_types
|
||||
sat/Theory_intf
|
||||
|
||||
smt/Arith
|
||||
smt/Cc
|
||||
smt/Combine
|
||||
smt/Exception
|
||||
smt/Fm
|
||||
smt/Intervals
|
||||
smt/Literal
|
||||
smt/Polynome
|
||||
smt/Smt
|
||||
smt/Sum
|
||||
smt/Symbols
|
||||
smt/Term
|
||||
smt/Ty
|
||||
smt/Uf
|
||||
smt/Use
|
||||
#smt/Arith
|
||||
#smt/Cc
|
||||
#smt/Combine
|
||||
#smt/Exception
|
||||
#smt/Fm
|
||||
#smt/Intervals
|
||||
#smt/Literal
|
||||
#smt/Polynome
|
||||
#smt/Smt
|
||||
#smt/Sum
|
||||
#smt/Symbols
|
||||
#smt/Term
|
||||
#smt/Ty
|
||||
#smt/Uf
|
||||
#smt/Use
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue