author | wenzelm |
Sat, 13 Mar 2010 14:44:47 +0100 | |
changeset 35743 | c506c029a082 |
parent 34120 | f9920a3ddf50 |
child 39036 | dff91b90d74c |
permissions | -rw-r--r-- |
17618 | 1 |
(* Title: HOL/SAT.thy |
2 |
Author: Alwen Tiu, Tjark Weber |
|
3 |
Copyright 2005 |
|
4 |
||
17627 | 5 |
Basic setup for the 'sat' and 'satx' tactic. |
17618 | 6 |
*) |
7 |
||
8 |
header {* Reconstructing external resolution proofs for propositional logic *} |
|
9 |
||
26521 | 10 |
theory SAT |
11 |
imports Refute |
|
17722 | 12 |
uses |
26521 | 13 |
"Tools/cnf_funcs.ML" |
14 |
"Tools/sat_funcs.ML" |
|
17618 | 15 |
begin |
16 |
||
17722 | 17 |
text {* \medskip Late package setup: default values for refute, see |
21588 | 18 |
also theory @{theory Refute}. *} |
17722 | 19 |
|
20 |
refute_params |
|
21 |
["itself"=1, |
|
22 |
minsize=1, |
|
23 |
maxsize=8, |
|
24 |
maxvars=10000, |
|
25 |
maxtime=60, |
|
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
32232
diff
changeset
|
26 |
satsolver="auto", |
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
32232
diff
changeset
|
27 |
no_assms="false"] |
17722 | 28 |
|
32232 | 29 |
ML {* structure sat = SATFunc(cnf) *} |
17618 | 30 |
|
32232 | 31 |
method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *} |
17618 | 32 |
"SAT solver" |
33 |
||
32232 | 34 |
method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *} |
17618 | 35 |
"SAT solver (with definitional CNF)" |
36 |
||
37 |
end |