src/HOL/SAT.thy
author haftmann
Fri, 20 Jul 2007 14:28:25 +0200
changeset 23881 851c74f1bb69
parent 21588 cd0dc678a205
child 26521 f8c4e79db153
permissions -rw-r--r--
moved class ord from Orderings.thy to HOL.thy
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
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    11
theory SAT imports Refute
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    12
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    13
uses
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    14
     "Tools/cnf_funcs.ML"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    15
     "Tools/sat_funcs.ML"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    16
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    17
begin
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    18
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    19
text {* \medskip Late package setup: default values for refute, see
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 17809
diff changeset
    20
  also theory @{theory Refute}. *}
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    21
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    22
refute_params
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    23
 ["itself"=1,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    24
  minsize=1,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    25
  maxsize=8,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    26
  maxvars=10000,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    27
  maxtime=60,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    28
  satsolver="auto"]
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    29
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    30
17627
ff1923b1978b cnf_struct renamed to cnf
webertj
parents: 17625
diff changeset
    31
ML {* structure sat = SATFunc(structure cnf = cnf); *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    32
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 17809
diff changeset
    33
method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    34
  "SAT solver"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    35
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 17809
diff changeset
    36
method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD' sat.satx_tac) *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    37
  "SAT solver (with definitional CNF)"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    38
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    39
end