# HG changeset patch # User blanchet # Date 1316969005 -7200 # Node ID bdb00fad5687d58cefd4800745590d5c46d9ed0b # Parent dbf6612461dcfd794063f3b47685df4bf8aae9bd killed JNI version of zChaff, since Kodkod 1.5 does not support it anymore diff -r dbf6612461dc -r bdb00fad5687 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Sun Sep 25 18:43:25 2011 +0200 +++ b/doc-src/Nitpick/nitpick.tex Sun Sep 25 18:43:25 2011 +0200 @@ -2381,11 +2381,6 @@ \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with versions 2004-05-13, 2004-11-15, and 2007-03-12. -\item[$\bullet$] \textbf{\textit{zChaff\_JNI}:} The JNI version of zChaff is -bundled with Kodkodi and is precompiled for the major -platforms. It is also available from \texttt{native\-solver.\allowbreak tgz}, -which you will find on Kodkod's web site \cite{kodkod-2009}. - \item[$\bullet$] \textbf{\textit{RSat}:} RSat is an efficient solver written in \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the directory that contains the \texttt{rsat} executable.% diff -r dbf6612461dc -r bdb00fad5687 src/HOL/Tools/Nitpick/kodkod_sat.ML --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Sun Sep 25 18:43:25 2011 +0200 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Sun Sep 25 18:43:25 2011 +0200 @@ -40,7 +40,6 @@ ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [], "Instance Satisfiable", "", "Instance Unsatisfiable")), - ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])), ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"], "s SATISFIABLE", "v ", "s UNSATISFIABLE")), ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",