# HG changeset patch # User webertj # Date 1085587598 -7200 # Node ID 1bf198c9828f67d50f899be88dcf6427f2165f88 # Parent e8ccb13d7774d708c3ed682eab32f45eda37c0fb documentation updated diff -r e8ccb13d7774 -r 1bf198c9828f src/HOL/Refute.thy --- a/src/HOL/Refute.thy Wed May 26 18:03:52 2004 +0200 +++ b/src/HOL/Refute.thy Wed May 26 18:06:38 2004 +0200 @@ -32,7 +32,8 @@ (* *) (* I strongly recommend that you install a stand-alone SAT solver if you *) (* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. If you *) -(* have installed ZChaff, simply set 'ZCHAFF_HOME' in 'etc/settings'. *) +(* have installed ZChaff Version 2003.12.04, simply set 'ZCHAFF_HOME' in *) +(* 'etc/settings'. *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) @@ -47,20 +48,18 @@ (* *) (* 'refute' currently accepts formulas of higher-order predicate logic (with *) (* equality), including free/bound/schematic variables, lambda abstractions, *) -(* sets and set membership, "arbitrary", "The", and "Eps". Constants for *) -(* which a defining equation exists are unfolded automatically. Non- *) -(* recursive inductive datatypes are supported. *) +(* sets and set membership, "arbitrary", "The", and "Eps". Defining *) +(* equations for constants are added automatically. Inductive datatypes are *) +(* supported, but may lead to spurious countermodels. *) (* *) -(* The (space) complexity of the algorithm is exponential in both the length *) -(* of the formula and the size of the model. *) +(* The (space) complexity of the algorithm is non-elementary. *) (* *) (* NOT (YET) SUPPORTED ARE *) (* *) (* - schematic type variables *) (* - axioms, sorts *) -(* - type constructors other than bool, =>, set, non-recursive IDTs *) (* - inductively defined sets *) -(* - recursive functions *) +(* - recursive functions on IDTs (case, recursion operators, size) *) (* - ... *) (* ------------------------------------------------------------------------- *) @@ -78,9 +77,16 @@ (* "maxvars" int If >0, use at most 'maxvars' boolean variables *) (* when transforming the term into a propositional *) (* formula. *) +(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) +(* This value is ignored under some ML compilers. *) (* "satsolver" string Name of the SAT solver to be used. *) (* *) (* See 'HOL/Main.thy' for default values. *) +(* *) +(* The size of particular types can be specified in the form type=size *) +(* (where 'type' is a string, and 'size' is an int). Examples: *) +(* "'a"=1 *) +(* "List.list"=2 *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) @@ -89,7 +95,7 @@ (* HOL/Tools/prop_logic.ML Propositional logic *) (* HOL/Tools/sat_solver.ML SAT solvers *) (* HOL/Tools/refute.ML Translation HOL -> propositional logic and *) -(* boolean assignment -> HOL model *) +(* Boolean assignment -> HOL model *) (* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *) (* syntax *) (* HOL/Refute.thy This file: loads the ML files, basic setup, *)