src/HOL/SAT.thy
author wenzelm
Mon, 27 Jul 2009 23:17:40 +0200
changeset 32232 6c394343360f
parent 30549 d2d7874648bd
child 34120 f9920a3ddf50
permissions -rw-r--r--
proper context for SAT tactics; eliminated METAHYPS; tuned signatures;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     1
(*  Title:      HOL/SAT.thy
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     2
    Author:     Alwen Tiu, Tjark Weber
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     3
    Copyright   2005
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     4
17627
ff1923b1978b cnf_struct renamed to cnf
webertj
parents: 17625
diff changeset
     5
Basic setup for the 'sat' and 'satx' tactic.
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     6
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     7
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     8
header {* Reconstructing external resolution proofs for propositional logic *}
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     9
26521
f8c4e79db153 tuned imports
haftmann
parents: 21588
diff changeset
    10
theory SAT
f8c4e79db153 tuned imports
haftmann
parents: 21588
diff changeset
    11
imports Refute
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    12
uses
26521
f8c4e79db153 tuned imports
haftmann
parents: 21588
diff changeset
    13
  "Tools/cnf_funcs.ML"
f8c4e79db153 tuned imports
haftmann
parents: 21588
diff changeset
    14
  "Tools/sat_funcs.ML"
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    15
begin
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    16
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    17
text {* \medskip Late package setup: default values for refute, see
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 17809
diff changeset
    18
  also theory @{theory Refute}. *}
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    19
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    20
refute_params
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    21
 ["itself"=1,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    22
  minsize=1,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    23
  maxsize=8,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    24
  maxvars=10000,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    25
  maxtime=60,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    26
  satsolver="auto"]
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    27
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 30549
diff changeset
    28
ML {* structure sat = SATFunc(cnf) *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    29
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 30549
diff changeset
    30
method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    31
  "SAT solver"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    32
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 30549
diff changeset
    33
method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    34
  "SAT solver (with definitional CNF)"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    35
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    36
end