equal
deleted
inserted
replaced
148 \textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\ |
148 \textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\ |
149 \textbf{begin} |
149 \textbf{begin} |
150 \postw |
150 \postw |
151 |
151 |
152 The results presented here were obtained using the JNI version of MiniSat and |
152 The results presented here were obtained using the JNI version of MiniSat and |
153 with multithreading disabled to reduce nondeterminism. This was done by adding |
153 with multithreading disabled to reduce nondeterminism and a time limit of |
154 the line |
154 15~seconds (instead of 30~seconds). This was done by adding the line |
155 |
155 |
156 \prew |
156 \prew |
157 \textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1] |
157 \textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\,\textit{timeout} = 15$\,s$] |
158 \postw |
158 \postw |
159 |
159 |
160 after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with |
160 after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with |
161 Kodkodi and is precompiled for the major platforms. Other SAT solvers can also |
161 Kodkodi and is precompiled for the major platforms. Other SAT solvers can also |
162 be installed, as explained in \S\ref{optimizations}. If you have already |
162 be installed, as explained in \S\ref{optimizations}. If you have already |
497 Some conjectures involving elementary number theory make Nitpick look like a |
497 Some conjectures involving elementary number theory make Nitpick look like a |
498 giant with feet of clay: |
498 giant with feet of clay: |
499 |
499 |
500 \prew |
500 \prew |
501 \textbf{lemma} ``$P~\textit{Suc}$'' \\ |
501 \textbf{lemma} ``$P~\textit{Suc}$'' \\ |
502 \textbf{nitpick} [\textit{card} = 1--6] \\[2\smallskipamount] |
502 \textbf{nitpick} \\[2\smallskipamount] |
503 \slshape |
503 \slshape |
504 Nitpick found no counterexample. |
504 Nitpick found no counterexample. |
505 \postw |
505 \postw |
506 |
506 |
507 On any finite set $N$, \textit{Suc} is a partial function; for example, if $N = |
507 On any finite set $N$, \textit{Suc} is a partial function; for example, if $N = |
1615 \textbf{theorem} \textit{S\_A\_B\_sound\_and\_complete}: \\ |
1615 \textbf{theorem} \textit{S\_A\_B\_sound\_and\_complete}: \\ |
1616 ``$w \in S \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b]$'' \\ |
1616 ``$w \in S \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b]$'' \\ |
1617 ``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\ |
1617 ``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\ |
1618 ``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\ |
1618 ``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\ |
1619 \textbf{nitpick} \\[2\smallskipamount] |
1619 \textbf{nitpick} \\[2\smallskipamount] |
1620 \slshape Nitpick found no counterexample. |
1620 \slshape Nitpick ran out of time after checking 7 of 8 scopes. |
1621 \postw |
1621 \postw |
1622 |
1622 |
1623 \subsection{AA Trees} |
1623 \subsection{AA Trees} |
1624 \label{aa-trees} |
1624 \label{aa-trees} |
1625 |
1625 |
1724 \prew |
1724 \prew |
1725 \textbf{theorem}~\textit{dataset\_skew\_split\/}:\\ |
1725 \textbf{theorem}~\textit{dataset\_skew\_split\/}:\\ |
1726 ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\ |
1726 ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\ |
1727 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\ |
1727 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\ |
1728 \textbf{nitpick} \\[2\smallskipamount] |
1728 \textbf{nitpick} \\[2\smallskipamount] |
1729 {\slshape Nitpick found no counterexample.} |
1729 {\slshape Nitpick ran out of time after checking 7 of 8 scopes.} |
1730 \postw |
1730 \postw |
1731 |
1731 |
1732 Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree |
1732 Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree |
1733 should not alter the tree: |
1733 should not alter the tree: |
1734 |
1734 |