build based on f86a1da

dev/advanced/index.html

@@ -18,4 +18,4 @@
 # more interactions via `send_command`...
 
 # it's good form to clean up your process
-close(proc)</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>.</p><p><strong>Checking if the response is complete</strong></p><p>The <code>send_command</code> function has an optional argument <code>is_done</code> for checking whether the full response has been received. The default is <code>nested_parens_match(output::String)</code> which returns <code>true</code> if <code>response</code> contains at least 1 matching pair of parentheses. This ensures the entire output is returned when issuing commands such as <code>(get-model)</code> where the response is wrapped in at least 1 set of parentheses.</p><p>!!! warning Multiple parenthesized statements 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>.</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/BooleanSatisfiability.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="../functions/">« Functions</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="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 0.27.25 on <span class="colophon-date" title="Saturday 19 August 2023 15:08">Saturday 19 August 2023</span>. Using Julia version 1.9.2.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>
+close(proc)</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>.</p><p><strong>Checking if the response is complete</strong></p><p>The <code>send_command</code> function has an optional argument <code>is_done</code> for checking whether the full response has been received. The default is <code>nested_parens_match(output::String)</code> which returns <code>true</code> if <code>response</code> contains at least 1 matching pair of parentheses. This ensures the entire output is returned when issuing commands such as <code>(get-model)</code> where the response is wrapped in at least 1 set of parentheses.</p><p>!!! warning Multiple parenthesized statements 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>.</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/BooleanSatisfiability.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="../functions/">« Functions</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="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 0.27.25 on <span class="colophon-date" title="Saturday 19 August 2023 15:50">Saturday 19 August 2023</span>. Using Julia version 1.9.2.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>

dev/example_bv_lcg/index.html

@@ -3,7 +3,8 @@
 
 @satvariable(states[1:10], BitVector, 32)
 @satvariable(output_prev, BitVector, 32)
-@satvariable(output_next, BitVector, 32)</code></pre><pre class="documenter-example-output"><code class="nohighlight hljs ansi">&lt;&lt; @example-block not executed in draft mode &gt;&gt;</code></pre><pre><code class="language-julia hljs">transitions = BoolExpr[states[i+1] == states[i] * 214013+2531011 for i=1:9]
+@satvariable(output_next, BitVector, 32)</code></pre><pre class="documenter-example-output"><code class="nohighlight hljs ansi">output_next
+</code></pre><pre><code class="language- hljs">transitions = BoolExpr[states[i+1] == states[i] * 214013+2531011 for i=1:9]
 remainders = BoolExpr[
     output_prev == urem(( states[1] &gt;&gt; 16 ) &amp; 0x7FFF, 100),
     urem(( states[2] &gt;&gt; 16) &amp; 0x7FFF, 100) == 29,
@@ -15,8 +16,8 @@
     urem(( states[8] &gt;&gt; 16) &amp; 0x7FFF, 100) == 58,
     urem(( states[9] &gt;&gt; 16) &amp; 0x7FFF, 100) == 61,
     output_next == urem(( states[10] &gt;&gt; 16) &amp; 0x7FFF, 100),
-]</code></pre><pre class="documenter-example-output"><code class="nohighlight hljs ansi">&lt;&lt; @example-block not executed in draft mode &gt;&gt;</code></pre><pre><code class="language-julia hljs">expr = and(all(transitions), all(remainders))
-status = sat!(expr, solver=CVC5())
+]</code></pre><pre><code class="language- hljs">expr = and(all(transitions), all(remainders))
+status = sat!(expr, solver=cvc5())
 println(&quot;status = $status&quot;)
 
 for (i,state) in enumerate(states)
@@ -25,4 +26,4 @@
 
 # According to SAT/SMT By Example the previous output is 37 and the next output is 17.
 println(&quot;prev = $(value(output_prev))&quot;)
-println(&quot;next = $(value(output_next))&quot;)</code></pre><pre class="documenter-example-output"><code class="nohighlight hljs ansi">&lt;&lt; @example-block not executed in draft mode &gt;&gt;</code></pre></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../example_job_shop/">« Job shop scheduling</a><a class="docs-footer-nextpage" href="../functions/">Functions »</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="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 0.27.25 on <span class="colophon-date" title="Saturday 19 August 2023 15:08">Saturday 19 August 2023</span>. Using Julia version 1.9.2.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>
+println(&quot;next = $(value(output_next))&quot;)</code></pre></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../example_job_shop/">« Job shop scheduling</a><a class="docs-footer-nextpage" href="../functions/">Functions »</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="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 0.27.25 on <span class="colophon-date" title="Saturday 19 August 2023 15:50">Saturday 19 August 2023</span>. Using Julia version 1.9.2.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>

dev/example_job_shop/index.html

@@ -5,11 +5,14 @@
 @satvariable(t1[1:n], Int)
 @satvariable(t2[1:n], Int)
 d1 = [2; 3; 2]
-d2 = [1; 1; 3]</code></pre><pre class="documenter-example-output"><code class="nohighlight hljs ansi">&lt;&lt; @example-block not executed in draft mode &gt;&gt;</code></pre><p>A start time of 0 corresponds to the first hour of the workday, and an end time of 8 corresponds to the last hour of the workday.</p><pre><code class="language-julia hljs">working_hours = all(and.(t1 .&gt;= 0, t2 .+ d2 .&lt;= 8))</code></pre><pre class="documenter-example-output"><code class="nohighlight hljs ansi">&lt;&lt; @example-block not executed in draft mode &gt;&gt;</code></pre><p>Sequencing constraint: For each job, A must complete the first task before B can start the second task</p><pre><code class="language-julia hljs">sequencing = and(t2 .&gt;= t1 .+ d1)</code></pre><pre class="documenter-example-output"><code class="nohighlight hljs ansi">&lt;&lt; @example-block not executed in draft mode &gt;&gt;</code></pre><p>Overlap constraint between all permutations</p><pre><code class="language-julia hljs">overlaps = [(1,2), (1,3), (2,3)]
+d2 = [1; 1; 3]</code></pre><pre class="documenter-example-output"><code class="nohighlight hljs ansi">3-element Vector{Int64}:
+ 1
+ 1
+ 3</code></pre><p>A start time of 0 corresponds to the first hour of the workday, and an end time of 8 corresponds to the last hour of the workday.</p><pre><code class="language- hljs">working_hours = all(and.(t1 .&gt;= 0, t2 .+ d2 .&lt;= 8))</code></pre><p>Sequencing constraint: For each job, A must complete the first task before B can start the second task</p><pre><code class="language- hljs">sequencing = and(t2 .&gt;= t1 .+ d1)</code></pre><p>Overlap constraint between all permutations</p><pre><code class="language- hljs">overlaps = [(1,2), (1,3), (2,3)]
 overlap_1 = all([or( t1[i] &gt;= t1[j] + d1[j], t1[j] &gt;= t1[i] + d1[i]) for (i,j) in overlaps])
-overlap_2 = all([or( t2[i] &gt;= t2[j] + d2[j], t2[j] &gt;= t2[i] + d2[i]) for (i,j) in overlaps])</code></pre><pre class="documenter-example-output"><code class="nohighlight hljs ansi">&lt;&lt; @example-block not executed in draft mode &gt;&gt;</code></pre><p>Solve the problem</p><pre><code class="language-julia hljs">status = sat!(working_hours, sequencing, overlap_1, overlap_2, solver=Z3())
+overlap_2 = all([or( t2[i] &gt;= t2[j] + d2[j], t2[j] &gt;= t2[i] + d2[i]) for (i,j) in overlaps])</code></pre><p>Solve the problem</p><pre><code class="language- hljs">status = sat!(working_hours, sequencing, overlap_1, overlap_2, solver=Z3())
 println(&quot;status = $status&quot;)
 if status == :SAT
     println(&quot;t1 = $(value(t1))&quot;)
     println(&quot;t2 = $(value(t2))&quot;)
-end</code></pre><pre class="documenter-example-output"><code class="nohighlight hljs ansi">&lt;&lt; @example-block not executed in draft mode &gt;&gt;</code></pre></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../example_scheduling/">« Finding a meeting time</a><a class="docs-footer-nextpage" href="../example_bv_lcg/">Predicting the output of a tiny LCG »</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="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 0.27.25 on <span class="colophon-date" title="Saturday 19 August 2023 15:08">Saturday 19 August 2023</span>. Using Julia version 1.9.2.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>
+end</code></pre></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../example_scheduling/">« Finding a meeting time</a><a class="docs-footer-nextpage" href="../example_bv_lcg/">Predicting the output of a tiny LCG »</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="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 0.27.25 on <span class="colophon-date" title="Saturday 19 August 2023 15:50">Saturday 19 August 2023</span>. Using Julia version 1.9.2.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>