author | wenzelm |
Thu, 22 Dec 2005 00:28:36 +0100 | |
changeset 18457 | 356a9f711899 |
parent 17809 | 195045659c06 |
child 21588 | cd0dc678a205 |
permissions | -rw-r--r-- |
17618 | 1 |
(* Title: HOL/SAT.thy |
2 |
ID: $Id$ |
|
3 |
Author: Alwen Tiu, Tjark Weber |
|
4 |
Copyright 2005 |
|
5 |
||
17627 | 6 |
Basic setup for the 'sat' and 'satx' tactic. |
17618 | 7 |
*) |
8 |
||
9 |
header {* Reconstructing external resolution proofs for propositional logic *} |
|
10 |
||
17722 | 11 |
theory SAT imports Refute |
17618 | 12 |
|
17722 | 13 |
uses |
17618 | 14 |
"Tools/cnf_funcs.ML" |
15 |
"Tools/sat_funcs.ML" |
|
16 |
||
17 |
begin |
|
18 |
||
17722 | 19 |
text {* \medskip Late package setup: default values for refute, see |
20 |
also theory @{text Refute}. *} |
|
21 |
||
22 |
refute_params |
|
23 |
["itself"=1, |
|
24 |
minsize=1, |
|
25 |
maxsize=8, |
|
26 |
maxvars=10000, |
|
27 |
maxtime=60, |
|
28 |
satsolver="auto"] |
|
29 |
||
30 |
||
17627 | 31 |
ML {* structure sat = SATFunc(structure cnf = cnf); *} |
17618 | 32 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17722
diff
changeset
|
33 |
method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD (sat.sat_tac 1)) *} |
17618 | 34 |
"SAT solver" |
35 |
||
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17722
diff
changeset
|
36 |
method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD (sat.satx_tac 1)) *} |
17618 | 37 |
"SAT solver (with definitional CNF)" |
38 |
||
39 |
end |