2089 variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the |
2089 variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the |
2090 \texttt{HaifaSat} executable. The \cpp{} sources for HaifaSat are available at |
2090 \texttt{HaifaSat} executable. The \cpp{} sources for HaifaSat are available at |
2091 \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}. |
2091 \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}. |
2092 |
2092 |
2093 \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to |
2093 \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to |
2094 \textit{smart}, Nitpick selects the first solver among MiniSat, PicoSAT, zChaff, |
2094 \textit{smart}, Nitpick selects the first solver among MiniSatJNI, MiniSat, |
2095 RSat, BerkMin, BerkMinAlloy, and Jerusat that is recognized by Isabelle. If none |
2095 PicoSAT, zChaffJNI, zChaff, RSat, BerkMin, BerkMinAlloy, and Jerusat that is |
2096 is found, it falls back on SAT4J, which should always be available. If |
2096 recognized by Isabelle. If none is found, it falls back on SAT4J, which should |
2097 \textit{verbose} is enabled, Nitpick displays which SAT solver was chosen. |
2097 always be available. If \textit{verbose} is enabled, Nitpick displays which SAT |
2098 |
2098 solver was chosen. |
2099 \end{enum} |
2099 \end{enum} |
2100 \fussy |
2100 \fussy |
2101 |
2101 |
2102 \opt{batch\_size}{int\_or\_smart}{smart} |
2102 \opt{batch\_size}{int\_or\_smart}{smart} |
2103 Specifies the maximum number of Kodkod problems that should be lumped together |
2103 Specifies the maximum number of Kodkod problems that should be lumped together |