mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
96 lines
No EOL
17 KiB
HTML
96 lines
No EOL
17 KiB
HTML
<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> |