author | immler@in.tum.de |
Sat, 14 Mar 2009 16:50:25 +0100 | |
changeset 30537 | 0dd8dfe424cf |
parent 30510 | 4120fc59dd85 |
child 30549 | d2d7874648bd |
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 |
||
26521 | 11 |
theory SAT |
12 |
imports Refute |
|
17722 | 13 |
uses |
26521 | 14 |
"Tools/cnf_funcs.ML" |
15 |
"Tools/sat_funcs.ML" |
|
17618 | 16 |
begin |
17 |
||
17722 | 18 |
text {* \medskip Late package setup: default values for refute, see |
21588 | 19 |
also theory @{theory Refute}. *} |
17722 | 20 |
|
21 |
refute_params |
|
22 |
["itself"=1, |
|
23 |
minsize=1, |
|
24 |
maxsize=8, |
|
25 |
maxvars=10000, |
|
26 |
maxtime=60, |
|
27 |
satsolver="auto"] |
|
28 |
||
17627 | 29 |
ML {* structure sat = SATFunc(structure cnf = cnf); *} |
17618 | 30 |
|
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
26521
diff
changeset
|
31 |
method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *} |
17618 | 32 |
"SAT solver" |
33 |
||
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
26521
diff
changeset
|
34 |
method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *} |
17618 | 35 |
"SAT solver (with definitional CNF)" |
36 |
||
37 |
end |