build based on e414042

dev/.documenter-siteinfo.json

@@ -1 +1 @@
-{"documenter":{"julia_version":"1.10.4","generation_timestamp":"2024-08-20T05:30:56","documenter_version":"1.5.0"}}
+{"documenter":{"julia_version":"1.10.4","generation_timestamp":"2024-08-26T14:52:28","documenter_version":"1.6.0"}}

dev/advanced/index.html

@@ -20,4 +20,4 @@
 # more interactions via `send_command`...
 
 # it's good form to clean up your open solver process
-close(interactive_solver)</code></pre><p>When using this functionality, you are responsible for keeping track of the solver mode and parsing the result of <code>send_command</code>. For convenience, <code>parse_model(model::String)</code> can parse the result of the SMT-LIB command <code>(get-model)</code>, returning a dictionary with variable names as keys and satisfying assignments as values.</p><p><strong>Checking if the response is complete</strong> Receiving a complete solver response is not as simple as it sounds, for two reasons.</p><ol><li>The solver may take a long time to respond, for example when calling <code>(check-sat)</code>.</li><li>The solver&#39;s response may be large, thus it may be received in several chunks.</li></ol><p>The <code>send_command</code> function has an optional argument <code>is_done</code> for checking whether the full response has been received. Two convenience functions are provided: <code>nested_parens_match(response::String)</code> returns <code>true</code> if <code>response</code> begins with <code>(</code> and ends with a matching <code>)</code>. This ensures the entire output is returned when issuing commands such as <code>(get-model)</code> where the entire response is wrapped in 1 set of parentheses. Many solver responses follow this format. <code>is_sat_or_unsat</code> is very simple: if the response contains <code>sat</code> or <code>unsat</code> it returns <code>true</code>, otherwise it&#39;s <code>false</code>.</p><p>!!! warning Multiple parenthesized statements</p><p>If your command produces a response with multiple separate statements, for example <code>(statement_1)\n(statement_2)</code>, <code>nested_parens_match</code> is not guaranteed to return the entire response. The intended use case is <code>((statement_1)\n(statement_2))</code>. This should only happen if you issue two SMT-LIB commands at once.</p><p><strong>Customizing <code>is_done</code></strong></p><p>A custom function <code>is_done(response::String)::Bool</code>, should have the following behavior:</p><ul><li><code>is_done</code> returns <code>true</code> if the given <code>response</code> is valid (in whatever sense you define) and <code>false</code> if not.</li><li><code>send_command</code> will WAIT for more output while <code>is_done</code> is false.</li></ul><p>SAT solvers can be slow and some commands produce long outputs. Without <code>is_done</code>, <code>send_command</code> could receive a partial response and prematurely return.</p><p>For full implementation details, please see the <a href="https://github.com/elsoroka/Satisfiability.jl/blob/main/src/call_solver.jl">source code</a> of <code>call_solver.jl</code>.</p></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../example_uninterpreted_func/">« Uninterpreted Functions</a><a class="docs-footer-nextpage" href="../faq/">FAQ »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="auto">Automatic (OS)</option><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option><option value="catppuccin-latte">catppuccin-latte</option><option value="catppuccin-frappe">catppuccin-frappe</option><option value="catppuccin-macchiato">catppuccin-macchiato</option><option value="catppuccin-mocha">catppuccin-mocha</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 1.5.0 on <span class="colophon-date" title="Tuesday 20 August 2024 05:30">Tuesday 20 August 2024</span>. Using Julia version 1.10.4.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>
+close(interactive_solver)</code></pre><p>When using this functionality, you are responsible for keeping track of the solver mode and parsing the result of <code>send_command</code>. For convenience, <code>parse_model(model::String)</code> can parse the result of the SMT-LIB command <code>(get-model)</code>, returning a dictionary with variable names as keys and satisfying assignments as values.</p><p><strong>Checking if the response is complete</strong> Receiving a complete solver response is not as simple as it sounds, for two reasons.</p><ol><li>The solver may take a long time to respond, for example when calling <code>(check-sat)</code>.</li><li>The solver&#39;s response may be large, thus it may be received in several chunks.</li></ol><p>The <code>send_command</code> function has an optional argument <code>is_done</code> for checking whether the full response has been received. Two convenience functions are provided: <code>nested_parens_match(response::String)</code> returns <code>true</code> if <code>response</code> begins with <code>(</code> and ends with a matching <code>)</code>. This ensures the entire output is returned when issuing commands such as <code>(get-model)</code> where the entire response is wrapped in 1 set of parentheses. Many solver responses follow this format. <code>is_sat_or_unsat</code> is very simple: if the response contains <code>sat</code> or <code>unsat</code> it returns <code>true</code>, otherwise it&#39;s <code>false</code>.</p><p>!!! warning Multiple parenthesized statements</p><p>If your command produces a response with multiple separate statements, for example <code>(statement_1)\n(statement_2)</code>, <code>nested_parens_match</code> is not guaranteed to return the entire response. The intended use case is <code>((statement_1)\n(statement_2))</code>. This should only happen if you issue two SMT-LIB commands at once.</p><p><strong>Customizing <code>is_done</code></strong></p><p>A custom function <code>is_done(response::String)::Bool</code>, should have the following behavior:</p><ul><li><code>is_done</code> returns <code>true</code> if the given <code>response</code> is valid (in whatever sense you define) and <code>false</code> if not.</li><li><code>send_command</code> will WAIT for more output while <code>is_done</code> is false.</li></ul><p>SAT solvers can be slow and some commands produce long outputs. Without <code>is_done</code>, <code>send_command</code> could receive a partial response and prematurely return.</p><p>For full implementation details, please see the <a href="https://github.com/elsoroka/Satisfiability.jl/blob/main/src/call_solver.jl">source code</a> of <code>call_solver.jl</code>.</p></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../example_uninterpreted_func/">« Uninterpreted Functions</a><a class="docs-footer-nextpage" href="../faq/">FAQ »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="auto">Automatic (OS)</option><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option><option value="catppuccin-latte">catppuccin-latte</option><option value="catppuccin-frappe">catppuccin-frappe</option><option value="catppuccin-macchiato">catppuccin-macchiato</option><option value="catppuccin-mocha">catppuccin-mocha</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 1.6.0 on <span class="colophon-date" title="Monday 26 August 2024 14:52">Monday 26 August 2024</span>. Using Julia version 1.10.4.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>