equal
deleted
inserted
replaced
1 (* Title: HOL/SAT.thy |
1 (* Title: HOL/SAT.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Alwen Tiu, Tjark Weber |
3 Author: Alwen Tiu, Tjark Weber |
4 Copyright 2005 |
4 Copyright 2005 |
5 |
5 |
6 Basic setup for the 'sat' tactic. |
6 Basic setup for the 'sat' and 'satx' tactic. |
7 *) |
7 *) |
8 |
8 |
9 header {* Reconstructing external resolution proofs for propositional logic *} |
9 header {* Reconstructing external resolution proofs for propositional logic *} |
10 |
10 |
11 theory SAT imports HOL |
11 theory SAT imports HOL |
14 "Tools/cnf_funcs.ML" |
14 "Tools/cnf_funcs.ML" |
15 "Tools/sat_funcs.ML" |
15 "Tools/sat_funcs.ML" |
16 |
16 |
17 begin |
17 begin |
18 |
18 |
19 (* |
19 ML {* structure sat = SATFunc(structure cnf = cnf); *} |
20 ML {* structure sat = SATFunc(structure cnf_struct = cnf); *} |
|
21 |
20 |
22 method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *} |
21 method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *} |
23 "SAT solver" |
22 "SAT solver" |
24 |
23 |
25 method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *} |
24 method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *} |
26 "SAT solver (with definitional CNF)" |
25 "SAT solver (with definitional CNF)" |
27 |
26 |
28 |
27 (* |
29 method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *} |
28 method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *} |
30 "Transforming hypotheses in a goal into CNF" |
29 "Transforming hypotheses in a goal into CNF" |
31 |
30 |
32 method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *} |
31 method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *} |
33 "Transforming the conclusion of a goal to CNF" |
32 "Transforming the conclusion of a goal to CNF" |