killed JNI version of zChaff, since Kodkod 1.5 does not support it anymore
authorblanchet
Sun, 25 Sep 2011 18:43:25 +0200
changeset 45950bdb00fad5687
parent 45949 dbf6612461dc
child 45951 b4f1beba1897
killed JNI version of zChaff, since Kodkod 1.5 does not support it anymore
doc-src/Nitpick/nitpick.tex
src/HOL/Tools/Nitpick/kodkod_sat.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Sun Sep 25 18:43:25 2011 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Sun Sep 25 18:43:25 2011 +0200
     1.3 @@ -2381,11 +2381,6 @@
     1.4  \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
     1.5  versions 2004-05-13, 2004-11-15, and 2007-03-12.
     1.6  
     1.7 -\item[$\bullet$] \textbf{\textit{zChaff\_JNI}:} The JNI version of zChaff is
     1.8 -bundled with Kodkodi and is precompiled for the major
     1.9 -platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
    1.10 -which you will find on Kodkod's web site \cite{kodkod-2009}.
    1.11 -
    1.12  \item[$\bullet$] \textbf{\textit{RSat}:} RSat is an efficient solver written in
    1.13  \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
    1.14  directory that contains the \texttt{rsat} executable.%
     2.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sun Sep 25 18:43:25 2011 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sun Sep 25 18:43:25 2011 +0200
     2.3 @@ -40,7 +40,6 @@
     2.4     ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
     2.5                            "Instance Satisfiable", "",
     2.6                            "Instance Unsatisfiable")),
     2.7 -   ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
     2.8     ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
     2.9                          "s SATISFIABLE", "v ", "s UNSATISFIABLE")),
    2.10     ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",