src/HOL/SAT.thy
author wenzelm
Fri, 13 Mar 2009 19:58:26 +0100
changeset 30510 4120fc59dd85
parent 26521 f8c4e79db153
child 30549 d2d7874648bd
permissions -rw-r--r--
unified type Proof.method and pervasive METHOD combinators;
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
    ID:         $Id$
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     3
    Author:     Alwen Tiu, Tjark Weber
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     4
    Copyright   2005
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     5
17627
ff1923b1978b cnf_struct renamed to cnf
webertj
parents: 17625
diff changeset
     6
Basic setup for the 'sat' and 'satx' tactic.
17618
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
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     9
header {* Reconstructing external resolution proofs for propositional logic *}
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    10
26521
f8c4e79db153 tuned imports
haftmann
parents: 21588
diff changeset
    11
theory SAT
f8c4e79db153 tuned imports
haftmann
parents: 21588
diff changeset
    12
imports Refute
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    13
uses
26521
f8c4e79db153 tuned imports
haftmann
parents: 21588
diff changeset
    14
  "Tools/cnf_funcs.ML"
f8c4e79db153 tuned imports
haftmann
parents: 21588
diff changeset
    15
  "Tools/sat_funcs.ML"
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    16
begin
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    17
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    18
text {* \medskip Late package setup: default values for refute, see
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 17809
diff changeset
    19
  also theory @{theory Refute}. *}
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    20
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    21
refute_params
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    22
 ["itself"=1,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    23
  minsize=1,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    24
  maxsize=8,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    25
  maxvars=10000,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    26
  maxtime=60,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    27
  satsolver="auto"]
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    28
17627
ff1923b1978b cnf_struct renamed to cnf
webertj
parents: 17625
diff changeset
    29
ML {* structure sat = SATFunc(structure cnf = cnf); *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    30
30510
4120fc59dd85 unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents: 26521
diff changeset
    31
method_setup sat = {* Method.no_args (SIMPLE_METHOD' 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
30510
4120fc59dd85 unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents: 26521
diff changeset
    34
method_setup satx = {* Method.no_args (SIMPLE_METHOD' 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