src/HOL/SAT.thy
author blanchet
Tue, 03 Jan 2012 18:33:18 +0100
changeset 46096 a00685a18e55
parent 39036 dff91b90d74c
child 48891 c0eafbd55de3
permissions -rw-r--r--
tuned Refute
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/sat_funcs.ML"
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    14
begin
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    15
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 30549
diff changeset
    16
ML {* structure sat = SATFunc(cnf) *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    17
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 30549
diff changeset
    18
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
    19
  "SAT solver"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    20
32232
6c394343360f proper context for SAT tactics;
wenzelm
parents: 30549
diff changeset
    21
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
    22
  "SAT solver (with definitional CNF)"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    23
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    24
end