30 (* ------------------------------------------------------------------------- *) |
30 (* ------------------------------------------------------------------------- *) |
31 (* NOTE *) |
31 (* NOTE *) |
32 (* *) |
32 (* *) |
33 (* I strongly recommend that you install a stand-alone SAT solver if you *) |
33 (* I strongly recommend that you install a stand-alone SAT solver if you *) |
34 (* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. If you *) |
34 (* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. If you *) |
35 (* have installed ZChaff, simply set 'ZCHAFF_HOME' in 'etc/settings'. *) |
35 (* have installed ZChaff Version 2003.12.04, simply set 'ZCHAFF_HOME' in *) |
|
36 (* 'etc/settings'. *) |
36 (* ------------------------------------------------------------------------- *) |
37 (* ------------------------------------------------------------------------- *) |
37 |
38 |
38 (* ------------------------------------------------------------------------- *) |
39 (* ------------------------------------------------------------------------- *) |
39 (* USAGE *) |
40 (* USAGE *) |
40 (* *) |
41 (* *) |
45 (* ------------------------------------------------------------------------- *) |
46 (* ------------------------------------------------------------------------- *) |
46 (* CURRENT LIMITATIONS *) |
47 (* CURRENT LIMITATIONS *) |
47 (* *) |
48 (* *) |
48 (* 'refute' currently accepts formulas of higher-order predicate logic (with *) |
49 (* 'refute' currently accepts formulas of higher-order predicate logic (with *) |
49 (* equality), including free/bound/schematic variables, lambda abstractions, *) |
50 (* equality), including free/bound/schematic variables, lambda abstractions, *) |
50 (* sets and set membership, "arbitrary", "The", and "Eps". Constants for *) |
51 (* sets and set membership, "arbitrary", "The", and "Eps". Defining *) |
51 (* which a defining equation exists are unfolded automatically. Non- *) |
52 (* equations for constants are added automatically. Inductive datatypes are *) |
52 (* recursive inductive datatypes are supported. *) |
53 (* supported, but may lead to spurious countermodels. *) |
53 (* *) |
54 (* *) |
54 (* The (space) complexity of the algorithm is exponential in both the length *) |
55 (* The (space) complexity of the algorithm is non-elementary. *) |
55 (* of the formula and the size of the model. *) |
|
56 (* *) |
56 (* *) |
57 (* NOT (YET) SUPPORTED ARE *) |
57 (* NOT (YET) SUPPORTED ARE *) |
58 (* *) |
58 (* *) |
59 (* - schematic type variables *) |
59 (* - schematic type variables *) |
60 (* - axioms, sorts *) |
60 (* - axioms, sorts *) |
61 (* - type constructors other than bool, =>, set, non-recursive IDTs *) |
|
62 (* - inductively defined sets *) |
61 (* - inductively defined sets *) |
63 (* - recursive functions *) |
62 (* - recursive functions on IDTs (case, recursion operators, size) *) |
64 (* - ... *) |
63 (* - ... *) |
65 (* ------------------------------------------------------------------------- *) |
64 (* ------------------------------------------------------------------------- *) |
66 |
65 |
67 (* ------------------------------------------------------------------------- *) |
66 (* ------------------------------------------------------------------------- *) |
68 (* PARAMETERS *) |
67 (* PARAMETERS *) |
76 (* "maxsize" int If >0, only search for models with size at most *) |
75 (* "maxsize" int If >0, only search for models with size at most *) |
77 (* 'maxsize'. *) |
76 (* 'maxsize'. *) |
78 (* "maxvars" int If >0, use at most 'maxvars' boolean variables *) |
77 (* "maxvars" int If >0, use at most 'maxvars' boolean variables *) |
79 (* when transforming the term into a propositional *) |
78 (* when transforming the term into a propositional *) |
80 (* formula. *) |
79 (* formula. *) |
|
80 (* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) |
|
81 (* This value is ignored under some ML compilers. *) |
81 (* "satsolver" string Name of the SAT solver to be used. *) |
82 (* "satsolver" string Name of the SAT solver to be used. *) |
82 (* *) |
83 (* *) |
83 (* See 'HOL/Main.thy' for default values. *) |
84 (* See 'HOL/Main.thy' for default values. *) |
|
85 (* *) |
|
86 (* The size of particular types can be specified in the form type=size *) |
|
87 (* (where 'type' is a string, and 'size' is an int). Examples: *) |
|
88 (* "'a"=1 *) |
|
89 (* "List.list"=2 *) |
84 (* ------------------------------------------------------------------------- *) |
90 (* ------------------------------------------------------------------------- *) |
85 |
91 |
86 (* ------------------------------------------------------------------------- *) |
92 (* ------------------------------------------------------------------------- *) |
87 (* FILES *) |
93 (* FILES *) |
88 (* *) |
94 (* *) |
89 (* HOL/Tools/prop_logic.ML Propositional logic *) |
95 (* HOL/Tools/prop_logic.ML Propositional logic *) |
90 (* HOL/Tools/sat_solver.ML SAT solvers *) |
96 (* HOL/Tools/sat_solver.ML SAT solvers *) |
91 (* HOL/Tools/refute.ML Translation HOL -> propositional logic and *) |
97 (* HOL/Tools/refute.ML Translation HOL -> propositional logic and *) |
92 (* boolean assignment -> HOL model *) |
98 (* Boolean assignment -> HOL model *) |
93 (* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *) |
99 (* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *) |
94 (* syntax *) |
100 (* syntax *) |
95 (* HOL/Refute.thy This file: loads the ML files, basic setup, *) |
101 (* HOL/Refute.thy This file: loads the ML files, basic setup, *) |
96 (* documentation *) |
102 (* documentation *) |
97 (* HOL/Main.thy Sets default parameters *) |
103 (* HOL/Main.thy Sets default parameters *) |