doc-src/Nitpick/nitpick.tex
changeset 33229 fba7527c3ef1
parent 33196 5fe67e108651
child 33232 f93390060bbe
equal deleted inserted replaced
33204:79bd3fbf5d61 33229:fba7527c3ef1
  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