src/HOL/SAT.thy
changeset 17722 8e098e040c2e
parent 17631 152ab92e1009
child 17809 195045659c06
     1.1 --- a/src/HOL/SAT.thy	Thu Sep 29 15:50:44 2005 +0200
     1.2 +++ b/src/HOL/SAT.thy	Thu Sep 29 15:50:45 2005 +0200
     1.3 @@ -8,14 +8,26 @@
     1.4  
     1.5  header {* Reconstructing external resolution proofs for propositional logic *}
     1.6  
     1.7 -theory SAT imports HOL
     1.8 +theory SAT imports Refute
     1.9  
    1.10 -uses (* "Tools/sat_solver.ML" -- already loaded by Refute.thy *)
    1.11 +uses
    1.12       "Tools/cnf_funcs.ML"
    1.13       "Tools/sat_funcs.ML"
    1.14  
    1.15  begin
    1.16  
    1.17 +text {* \medskip Late package setup: default values for refute, see
    1.18 +  also theory @{text Refute}. *}
    1.19 +
    1.20 +refute_params
    1.21 + ["itself"=1,
    1.22 +  minsize=1,
    1.23 +  maxsize=8,
    1.24 +  maxvars=10000,
    1.25 +  maxtime=60,
    1.26 +  satsolver="auto"]
    1.27 +
    1.28 +
    1.29  ML {* structure sat = SATFunc(structure cnf = cnf); *}
    1.30  
    1.31  method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
    1.32 @@ -24,18 +36,4 @@
    1.33  method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
    1.34    "SAT solver (with definitional CNF)"
    1.35  
    1.36 -(*
    1.37 -method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
    1.38 -  "Transforming hypotheses in a goal into CNF"
    1.39 -
    1.40 -method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *}
    1.41 -  "Transforming the conclusion of a goal to CNF"
    1.42 -
    1.43 -method_setup cnf_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_thin_tac) *}
    1.44 -  "Same as cnf, but remove the original hypotheses"
    1.45 -
    1.46 -method_setup cnfx_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnfx_thin_tac) *}
    1.47 -  "Same as cnf_thin, but may introduce extra variables"
    1.48 -*)
    1.49 -
    1.50  end