# HG changeset patch # User webertj # Date 1078954653 -3600 # Node ID c2b96948730d41e6291013fc28255ff57ae02797 # Parent 6d5d6e78d8519b0eb2ecfbb4205e93cece5371e0 changed default values for refute diff -r 6d5d6e78d851 -r c2b96948730d src/HOL/Main.thy --- a/src/HOL/Main.thy Wed Mar 10 22:35:37 2004 +0100 +++ b/src/HOL/Main.thy Wed Mar 10 22:37:33 2004 +0100 @@ -94,23 +94,13 @@ subsection {* Configuration of the 'refute' command *} text {* - The following are reasonable default parameters (for use with - ZChaff 2003.12.04). For an explanation of these parameters, - see 'HOL/Refute.thy'. - - \emph{Note}: If you want to use a different SAT solver (or - install ZChaff to a different location), you will need to - override at least the values for 'command' and (probably) - 'success' in your own theory file. + The following are fairly reasonable default values. For an + explanation of these parameters, see 'HOL/Refute.thy'. *} refute_params [minsize=1, maxsize=8, - maxvars=200, - satfile="refute.cnf", - satformat="defcnf", - resultfile="refute.out", - success="Verify Solution successful. Instance satisfiable", - command="$HOME/bin/zchaff refute.cnf 60 > refute.out"] + maxvars=100, + satsolver="auto"] end