proper config options;
authorwenzelm
Sat Feb 01 21:43:23 2014 +0100 (2014-02-01)
changeset 55240efc4c0e0e14a
parent 55239 97921d23ebe3
child 55241 ef601c60ccbe
proper config options;
proper context for printing;
src/HOL/ROOT
src/HOL/Tools/sat.ML
src/HOL/ex/SAT_Examples.thy
     1.1 --- a/src/HOL/ROOT	Sat Feb 01 21:09:53 2014 +0100
     1.2 +++ b/src/HOL/ROOT	Sat Feb 01 21:43:23 2014 +0100
     1.3 @@ -572,8 +572,7 @@
     1.4      Sudoku
     1.5  (* FIXME
     1.6  (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
     1.7 -(*global side-effects ahead!*)
     1.8 -try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)
     1.9 +    SAT_Examples
    1.10  *)
    1.11    files "document/root.bib" "document/root.tex"
    1.12  
     2.1 --- a/src/HOL/Tools/sat.ML	Sat Feb 01 21:09:53 2014 +0100
     2.2 +++ b/src/HOL/Tools/sat.ML	Sat Feb 01 21:43:23 2014 +0100
     2.3 @@ -48,8 +48,8 @@
     2.4  
     2.5  signature SAT =
     2.6  sig
     2.7 -  val trace_sat: bool Unsynchronized.ref    (* input: print trace messages *)
     2.8 -  val solver: string Unsynchronized.ref  (* input: name of SAT solver to be used *)
     2.9 +  val trace: bool Config.T  (* print trace messages *)
    2.10 +  val solver: string Config.T  (* name of SAT solver to be used *)
    2.11    val counter: int Unsynchronized.ref     (* output: number of resolution steps during last proof replay *)
    2.12    val rawsat_thm: Proof.context -> cterm list -> thm
    2.13    val rawsat_tac: Proof.context -> int -> tactic
    2.14 @@ -60,9 +60,12 @@
    2.15  structure SAT : SAT =
    2.16  struct
    2.17  
    2.18 -val trace_sat = Unsynchronized.ref false;
    2.19 +val trace = Attrib.setup_config_bool @{binding sat_trace} (K false);
    2.20  
    2.21 -val solver = Unsynchronized.ref "zchaff_with_proofs";
    2.22 +fun cond_tracing ctxt msg =
    2.23 +  if Config.get ctxt trace then tracing (msg ()) else ();
    2.24 +
    2.25 +val solver = Attrib.setup_config_string @{binding sat_solver} (K "zchaff_with_proofs");
    2.26    (*see HOL/Tools/sat_solver.ML for possible values*)
    2.27  
    2.28  val counter = Unsynchronized.ref 0;
    2.29 @@ -153,14 +156,11 @@
    2.30          fun resolution (c1, hyps1) (c2, hyps2) =
    2.31            let
    2.32              val _ =
    2.33 -              if ! trace_sat then  (* FIXME !? *)
    2.34 -                tracing ("Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
    2.35 -                  " (hyps: " ^ ML_Syntax.print_list
    2.36 -                    (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
    2.37 -                  ^ ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
    2.38 -                  " (hyps: " ^ ML_Syntax.print_list
    2.39 -                    (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
    2.40 -              else ()
    2.41 +              cond_tracing ctxt (fn () =>
    2.42 +                "Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
    2.43 +                " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c1) ^
    2.44 +                ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
    2.45 +                " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c2) ^ ")")
    2.46  
    2.47              (* the two literals used for resolution *)
    2.48              val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) []
    2.49 @@ -177,9 +177,8 @@
    2.50                end
    2.51  
    2.52              val _ =
    2.53 -              if !trace_sat then
    2.54 -                tracing ("Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
    2.55 -              else ()
    2.56 +              cond_tracing ctxt
    2.57 +                (fn () => "Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
    2.58  
    2.59              (* Gamma1, Gamma2 |- False *)
    2.60              val c_new =
    2.61 @@ -188,11 +187,11 @@
    2.62                  (if hyp1_is_neg then c1' else c2')
    2.63  
    2.64              val _ =
    2.65 -              if !trace_sat then
    2.66 -                tracing ("Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
    2.67 -                  " (hyps: " ^ ML_Syntax.print_list
    2.68 -                      (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
    2.69 -              else ()
    2.70 +              cond_tracing ctxt (fn () =>
    2.71 +                "Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
    2.72 +                " (hyps: " ^
    2.73 +                ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c_new) ^ ")")
    2.74 +
    2.75              val _ = Unsynchronized.inc counter
    2.76            in
    2.77              (c_new, new_hyps)
    2.78 @@ -226,8 +225,7 @@
    2.79        | ORIG_CLAUSE thm =>
    2.80            (* convert the original clause *)
    2.81            let
    2.82 -            val _ =
    2.83 -              if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else ()
    2.84 +            val _ = cond_tracing ctxt (fn () => "Using original clause #" ^ string_of_int id)
    2.85              val raw = CNF.clause2raw_thm thm
    2.86              val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
    2.87                Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
    2.88 @@ -239,15 +237,13 @@
    2.89        | NO_CLAUSE =>
    2.90            (* prove the clause, using information from 'clause_table' *)
    2.91            let
    2.92 -            val _ =
    2.93 -              if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
    2.94 +            val _ = cond_tracing ctxt (fn () => "Proving clause #" ^ string_of_int id ^ " ...")
    2.95              val ids = the (Inttab.lookup clause_table id)
    2.96              val clause = resolve_raw_clauses ctxt (map prove_clause ids)
    2.97              val _ = Array.update (clauses, id, RAW_CLAUSE clause)
    2.98              val _ =
    2.99 -              if !trace_sat then
   2.100 -                tracing ("Replay chain successful; clause stored at #" ^ string_of_int id)
   2.101 -              else ()
   2.102 +              cond_tracing ctxt
   2.103 +                (fn () => "Replay chain successful; clause stored at #" ^ string_of_int id)
   2.104            in
   2.105              clause
   2.106            end)
   2.107 @@ -255,10 +251,9 @@
   2.108      val _ = counter := 0
   2.109      val empty_clause = fst (prove_clause empty_id)
   2.110      val _ =
   2.111 -      if !trace_sat then
   2.112 -        tracing ("Proof reconstruction successful; " ^
   2.113 -          string_of_int (!counter) ^ " resolution step(s) total.")
   2.114 -      else ()
   2.115 +      cond_tracing ctxt (fn () =>
   2.116 +        "Proof reconstruction successful; " ^
   2.117 +        string_of_int (!counter) ^ " resolution step(s) total.")
   2.118    in
   2.119      empty_clause
   2.120    end;
   2.121 @@ -311,25 +306,22 @@
   2.122      (* sorted in ascending order                                          *)
   2.123      val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
   2.124      val _ =
   2.125 -      if !trace_sat then
   2.126 -        tracing ("Sorted non-trivial clauses:\n" ^
   2.127 -          cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
   2.128 -      else ()
   2.129 +      cond_tracing ctxt (fn () =>
   2.130 +        "Sorted non-trivial clauses:\n" ^
   2.131 +        cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
   2.132      (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
   2.133      val (fms, atom_table) =
   2.134        fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
   2.135          sorted_clauses Termtab.empty
   2.136      val _ =
   2.137 -      if !trace_sat then
   2.138 -        tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
   2.139 -      else ()
   2.140 +      cond_tracing ctxt
   2.141 +        (fn () => "Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
   2.142      val fm = Prop_Logic.all fms
   2.143      fun make_quick_and_dirty_thm () =
   2.144        let
   2.145          val _ =
   2.146 -          if !trace_sat then
   2.147 -            tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
   2.148 -          else ()
   2.149 +          cond_tracing ctxt
   2.150 +            (fn () => "quick_and_dirty is set: proof reconstruction skipped, using oracle instead")
   2.151          val False_thm = Skip_Proof.make_thm_cterm @{cprop False}
   2.152        in
   2.153          (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
   2.154 @@ -340,17 +332,16 @@
   2.155        end
   2.156    in
   2.157      case
   2.158 -      let val the_solver = ! solver
   2.159 +      let val the_solver = Config.get ctxt solver
   2.160        in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
   2.161      of
   2.162        SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
   2.163 -       (if !trace_sat then
   2.164 -          tracing ("Proof trace from SAT solver:\n" ^
   2.165 -            "clauses: " ^ ML_Syntax.print_list
   2.166 -              (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
   2.167 -              (Inttab.dest clause_table) ^ "\n" ^
   2.168 -            "empty clause: " ^ string_of_int empty_id)
   2.169 -        else ();
   2.170 +       (cond_tracing ctxt (fn () =>
   2.171 +          "Proof trace from SAT solver:\n" ^
   2.172 +          "clauses: " ^ ML_Syntax.print_list
   2.173 +            (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
   2.174 +            (Inttab.dest clause_table) ^ "\n" ^
   2.175 +          "empty clause: " ^ string_of_int empty_id);
   2.176          if Config.get ctxt quick_and_dirty then
   2.177            make_quick_and_dirty_thm ()
   2.178          else
     3.1 --- a/src/HOL/ex/SAT_Examples.thy	Sat Feb 01 21:09:53 2014 +0100
     3.2 +++ b/src/HOL/ex/SAT_Examples.thy	Sat Feb 01 21:43:23 2014 +0100
     3.3 @@ -3,14 +3,17 @@
     3.4      Copyright   2005-2009
     3.5  *)
     3.6  
     3.7 -header {* Examples for the 'sat' and 'satx' tactic *}
     3.8 +header {* Examples for proof methods "sat" and "satx" *}
     3.9  
    3.10  theory SAT_Examples imports Main
    3.11  begin
    3.12  
    3.13 -(* ML {* SAT.solver := "zchaff_with_proofs"; *} *)
    3.14 -(* ML {* SAT.solver := "minisat_with_proofs"; *} *)
    3.15 -ML {* SAT.trace_sat := true; *}
    3.16 +(*
    3.17 +declare [[sat_solver = zchaff_with_proofs]]
    3.18 +declare [[sat_solver = minisat_with_proofs]]
    3.19 +*)
    3.20 +
    3.21 +declare [[sat_trace]]
    3.22  declare [[quick_and_dirty]]
    3.23  
    3.24  lemma "True"
    3.25 @@ -24,13 +27,13 @@
    3.26  
    3.27  lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
    3.28  (*
    3.29 -apply (tactic {* CNF.cnf_rewrite_tac 1 *})
    3.30 +apply (tactic {* CNF.cnf_rewrite_tac @{context} 1 *})
    3.31  *)
    3.32  by sat
    3.33  
    3.34  lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
    3.35  (*
    3.36 -apply (tactic {* CNF.cnfx_rewrite_tac 1 *})
    3.37 +apply (tactic {* CNF.cnfx_rewrite_tac @{context} 1 *})
    3.38  apply (erule exE | erule conjE)+
    3.39  *)
    3.40  by satx
    3.41 @@ -38,14 +41,14 @@
    3.42  lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
    3.43    \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
    3.44  (*
    3.45 -apply (tactic {* CNF.cnf_rewrite_tac 1 *})
    3.46 +apply (tactic {* CNF.cnf_rewrite_tac @{context} 1 *})
    3.47  *)
    3.48  by sat
    3.49  
    3.50  lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
    3.51    \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
    3.52  (*
    3.53 -apply (tactic {* CNF.cnfx_rewrite_tac 1 *})
    3.54 +apply (tactic {* CNF.cnfx_rewrite_tac @{context} 1 *})
    3.55  apply (erule exE | erule conjE)+
    3.56  *)
    3.57  by satx
    3.58 @@ -77,7 +80,7 @@
    3.59  lemma "(ALL x. P x) | ~ All P"
    3.60  by sat
    3.61  
    3.62 -ML {* SAT.trace_sat := false; *}
    3.63 +declare [[sat_trace = false]]
    3.64  declare [[quick_and_dirty = false]]
    3.65  
    3.66  method_setup rawsat = {*
    3.67 @@ -519,13 +522,11 @@
    3.68  the number of resolution steps in the proof.
    3.69  *}
    3.70  
    3.71 -(* ML {*
    3.72 -SAT.solver := "zchaff_with_proofs";
    3.73 -SAT.trace_sat := false;
    3.74 -*}
    3.75 +(*
    3.76 +declare [[sat_solver = zchaff_with_proofs]]
    3.77 +declare [[sat_trace = false]]
    3.78  declare [[quick_and_dirty = false]]
    3.79  *)
    3.80 -
    3.81  ML {*
    3.82    fun benchmark dimacsfile =
    3.83      let