changed default values for refute
authorwebertj
Wed Mar 10 22:37:33 2004 +0100 (2004-03-10)
changeset 14458c2b96948730d
parent 14457 6d5d6e78d851
child 14459 0a8619367a61
changed default values for refute
src/HOL/Main.thy
     1.1 --- a/src/HOL/Main.thy	Wed Mar 10 22:35:37 2004 +0100
     1.2 +++ b/src/HOL/Main.thy	Wed Mar 10 22:37:33 2004 +0100
     1.3 @@ -94,23 +94,13 @@
     1.4  subsection {* Configuration of the 'refute' command *}
     1.5  
     1.6  text {*
     1.7 -  The following are reasonable default parameters (for use with
     1.8 -  ZChaff 2003.12.04).  For an explanation of these parameters,
     1.9 -  see 'HOL/Refute.thy'.
    1.10 -
    1.11 -  \emph{Note}: If you want to use a different SAT solver (or
    1.12 -  install ZChaff to a different location), you will need to
    1.13 -  override at least the values for 'command' and (probably)
    1.14 -  'success' in your own theory file.
    1.15 +  The following are fairly reasonable default values.  For an
    1.16 +  explanation of these parameters, see 'HOL/Refute.thy'.
    1.17  *}
    1.18  
    1.19  refute_params [minsize=1,
    1.20                 maxsize=8,
    1.21 -               maxvars=200,
    1.22 -               satfile="refute.cnf",
    1.23 -               satformat="defcnf",
    1.24 -               resultfile="refute.out",
    1.25 -               success="Verify Solution successful. Instance satisfiable",
    1.26 -               command="$HOME/bin/zchaff refute.cnf 60 > refute.out"]
    1.27 +               maxvars=100,
    1.28 +               satsolver="auto"]
    1.29  
    1.30  end