src/HOL/SAT.thy
author wenzelm
Sat, 13 Mar 2010 14:44:47 +0100
changeset 35743 c506c029a082
parent 34120 f9920a3ddf50
child 39036 dff91b90d74c
permissions -rw-r--r--
adapted to localized typedef: handle single global interpretation only;
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,
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
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    28
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 30549
diff changeset
    29
ML {* structure sat = SATFunc(cnf) *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    30
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 30549
diff changeset
    31
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
    32
  "SAT solver"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    33
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 30549
diff changeset
    34
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
    35
  "SAT solver (with definitional CNF)"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    36
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    37
end