src/HOL/SAT.thy
changeset 17722 8e098e040c2e
parent 17631 152ab92e1009
child 17809 195045659c06
equal deleted inserted replaced
17721:b943c01e1c6d 17722:8e098e040c2e
     6 Basic setup for the 'sat' and 'satx' tactic.
     6 Basic setup for the 'sat' and 'satx' tactic.
     7 *)
     7 *)
     8 
     8 
     9 header {* Reconstructing external resolution proofs for propositional logic *}
     9 header {* Reconstructing external resolution proofs for propositional logic *}
    10 
    10 
    11 theory SAT imports HOL
    11 theory SAT imports Refute
    12 
    12 
    13 uses (* "Tools/sat_solver.ML" -- already loaded by Refute.thy *)
    13 uses
    14      "Tools/cnf_funcs.ML"
    14      "Tools/cnf_funcs.ML"
    15      "Tools/sat_funcs.ML"
    15      "Tools/sat_funcs.ML"
    16 
    16 
    17 begin
    17 begin
       
    18 
       
    19 text {* \medskip Late package setup: default values for refute, see
       
    20   also theory @{text Refute}. *}
       
    21 
       
    22 refute_params
       
    23  ["itself"=1,
       
    24   minsize=1,
       
    25   maxsize=8,
       
    26   maxvars=10000,
       
    27   maxtime=60,
       
    28   satsolver="auto"]
       
    29 
    18 
    30 
    19 ML {* structure sat = SATFunc(structure cnf = cnf); *}
    31 ML {* structure sat = SATFunc(structure cnf = cnf); *}
    20 
    32 
    21 method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
    33 method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
    22   "SAT solver"
    34   "SAT solver"
    23 
    35 
    24 method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
    36 method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
    25   "SAT solver (with definitional CNF)"
    37   "SAT solver (with definitional CNF)"
    26 
    38 
    27 (*
       
    28 method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
       
    29   "Transforming hypotheses in a goal into CNF"
       
    30 
       
    31 method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *}
       
    32   "Transforming the conclusion of a goal to CNF"
       
    33 
       
    34 method_setup cnf_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_thin_tac) *}
       
    35   "Same as cnf, but remove the original hypotheses"
       
    36 
       
    37 method_setup cnfx_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnfx_thin_tac) *}
       
    38   "Same as cnf_thin, but may introduce extra variables"
       
    39 *)
       
    40 
       
    41 end
    39 end