author wenzelm Sat Jan 08 16:01:51 2011 +0100 (2011-01-08) changeset 41471 54a58904a598 parent 41470 890b25753bf7 child 41472 f6ab14e61604
modernized structure Prop_Logic;
avoid ML structure aliases;
 src/HOL/Tools/Function/scnp_solve.ML file | annotate | diff | revisions src/HOL/Tools/Nitpick/nitpick_mono.ML file | annotate | diff | revisions src/HOL/Tools/prop_logic.ML file | annotate | diff | revisions src/HOL/Tools/refute.ML file | annotate | diff | revisions src/HOL/Tools/sat_funcs.ML file | annotate | diff | revisions src/HOL/Tools/sat_solver.ML file | annotate | diff | revisions src/HOL/ex/SAT_Examples.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Tools/Function/scnp_solve.ML	Sat Jan 08 14:32:55 2011 +0100
1.2 +++ b/src/HOL/Tools/Function/scnp_solve.ML	Sat Jan 08 16:01:51 2011 +0100
1.3 @@ -51,11 +51,11 @@
1.4
1.5  (** Propositional formulas **)
1.6
1.7 -val Not = PropLogic.Not and And = PropLogic.And and Or = PropLogic.Or
1.8 -val BoolVar = PropLogic.BoolVar
1.9 +val Not = Prop_Logic.Not and And = Prop_Logic.And and Or = Prop_Logic.Or
1.10 +val BoolVar = Prop_Logic.BoolVar
1.11  fun Implies (p, q) = Or (Not p, q)
1.12  fun Equiv (p, q) = And (Implies (p, q), Implies (q, p))
1.13 -val all = PropLogic.all
1.14 +val all = Prop_Logic.all
1.15
1.16  (* finite indexed quantifiers:
1.17
1.18 @@ -64,7 +64,7 @@
1.19                        0<=i<n
1.20   *)
1.21  fun iforall n f = all (map_range f n)
1.22 -fun iexists n f = PropLogic.exists (map_range f n)
1.23 +fun iexists n f = Prop_Logic.exists (map_range f n)
1.24  fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
1.25
1.26  fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1)))
1.27 @@ -112,7 +112,7 @@
1.28      val ng = num_graphs gp
1.29      val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp
1.30
1.31 -    fun encode_constraint_strict 0 (x, y) = PropLogic.False
1.32 +    fun encode_constraint_strict 0 (x, y) = Prop_Logic.False
1.33        | encode_constraint_strict k (x, y) =
1.34          Or (And (TAG x (k - 1), Not (TAG y (k - 1))),
1.35              And (Equiv (TAG x (k - 1), TAG y (k - 1)),
1.36 @@ -212,7 +212,7 @@
1.37  fun mk_certificate bits label gp f =
1.38    let
1.39      val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp
1.40 -    fun assign (PropLogic.BoolVar v) = the_default false (f v)
1.41 +    fun assign (Prop_Logic.BoolVar v) = the_default false (f v)
1.42      fun assignTag i j =
1.43        (fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0))
1.44          (bits - 1 downto 0) 0)
```
```     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Jan 08 14:32:55 2011 +0100
2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Jan 08 16:01:51 2011 +0100
2.3 @@ -20,8 +20,6 @@
2.4  open Nitpick_Util
2.5  open Nitpick_HOL
2.6
2.7 -structure PL = PropLogic
2.8 -
2.9  datatype sign = Plus | Minus
2.10
2.11  type var = int
2.12 @@ -474,36 +472,36 @@
2.13  val bools_from_annotation = AList.lookup (op =) bool_table #> the
2.14  val annotation_from_bools = AList.find (op =) bool_table #> the_single
2.15
2.16 -fun prop_for_bool b = if b then PL.True else PL.False
2.17 +fun prop_for_bool b = if b then Prop_Logic.True else Prop_Logic.False
2.18  fun prop_for_bool_var_equality (v1, v2) =
2.19 -  PL.SAnd (PL.SOr (PL.BoolVar v1, PL.SNot (PL.BoolVar v2)),
2.20 -           PL.SOr (PL.SNot (PL.BoolVar v1), PL.BoolVar v2))
2.21 +  Prop_Logic.SAnd (Prop_Logic.SOr (Prop_Logic.BoolVar v1, Prop_Logic.SNot (Prop_Logic.BoolVar v2)),
2.22 +           Prop_Logic.SOr (Prop_Logic.SNot (Prop_Logic.BoolVar v1), Prop_Logic.BoolVar v2))
2.23  fun prop_for_assign (x, a) =
2.24    let val (b1, b2) = bools_from_annotation a in
2.25 -    PL.SAnd (PL.BoolVar (fst_var x) |> not b1 ? PL.SNot,
2.26 -             PL.BoolVar (snd_var x) |> not b2 ? PL.SNot)
2.27 +    Prop_Logic.SAnd (Prop_Logic.BoolVar (fst_var x) |> not b1 ? Prop_Logic.SNot,
2.28 +             Prop_Logic.BoolVar (snd_var x) |> not b2 ? Prop_Logic.SNot)
2.29    end
2.30  fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a)
2.31 -  | prop_for_assign_literal (x, (Minus, a)) = PL.SNot (prop_for_assign (x, a))
2.32 +  | prop_for_assign_literal (x, (Minus, a)) = Prop_Logic.SNot (prop_for_assign (x, a))
2.33  fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a')
2.34    | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a))
2.35  fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
2.36    | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1)
2.37    | prop_for_atom_equality (V x1, V x2) =
2.38 -    PL.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)),
2.39 +    Prop_Logic.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)),
2.40               prop_for_bool_var_equality (pairself snd_var (x1, x2)))
2.41 -val prop_for_assign_clause = PL.exists o map prop_for_assign_literal
2.42 +val prop_for_assign_clause = Prop_Logic.exists o map prop_for_assign_literal
2.43  fun prop_for_exists_var_assign_literal xs a =
2.44 -  PL.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs)
2.45 +  Prop_Logic.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs)
2.46  fun prop_for_comp (aa1, aa2, Eq, []) =
2.47 -    PL.SAnd (prop_for_comp (aa1, aa2, Leq, []),
2.48 +    Prop_Logic.SAnd (prop_for_comp (aa1, aa2, Leq, []),
2.49               prop_for_comp (aa2, aa1, Leq, []))
2.50    | prop_for_comp (aa1, aa2, Neq, []) =
2.51 -    PL.SNot (prop_for_comp (aa1, aa2, Eq, []))
2.52 +    Prop_Logic.SNot (prop_for_comp (aa1, aa2, Eq, []))
2.53    | prop_for_comp (aa1, aa2, Leq, []) =
2.54 -    PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
2.55 +    Prop_Logic.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
2.56    | prop_for_comp (aa1, aa2, cmp, xs) =
2.57 -    PL.SOr (prop_for_exists_var_assign_literal xs Gen,
2.58 +    Prop_Logic.SOr (prop_for_exists_var_assign_literal xs Gen,
2.59              prop_for_comp (aa1, aa2, cmp, []))
2.60
2.61  fun extract_assigns max_var assigns asgs =
2.62 @@ -542,11 +540,11 @@
2.63        SOME (extract_assigns max_var assigns asgs |> tap print_solution)
2.64      val _ = print_problem comps clauses
2.65      val prop =
2.66 -      PL.all (map prop_for_comp comps @ map prop_for_assign_clause clauses)
2.67 +      Prop_Logic.all (map prop_for_comp comps @ map prop_for_assign_clause clauses)
2.68    in
2.69 -    if PL.eval (K false) prop then
2.70 +    if Prop_Logic.eval (K false) prop then
2.71        do_assigns (K (SOME false))
2.72 -    else if PL.eval (K true) prop then
2.73 +    else if Prop_Logic.eval (K true) prop then
2.74        do_assigns (K (SOME true))
2.75      else
2.76        let
```
```     3.1 --- a/src/HOL/Tools/prop_logic.ML	Sat Jan 08 14:32:55 2011 +0100
3.2 +++ b/src/HOL/Tools/prop_logic.ML	Sat Jan 08 16:01:51 2011 +0100
3.3 @@ -42,7 +42,7 @@
3.4    val term_of_prop_formula: prop_formula -> term
3.5  end;
3.6
3.7 -structure PropLogic : PROP_LOGIC =
3.8 +structure Prop_Logic : PROP_LOGIC =
3.9  struct
3.10
3.11  (* ------------------------------------------------------------------------- *)
```
```     4.1 --- a/src/HOL/Tools/refute.ML	Sat Jan 08 14:32:55 2011 +0100
4.2 +++ b/src/HOL/Tools/refute.ML	Sat Jan 08 16:01:51 2011 +0100
4.3 @@ -77,7 +77,7 @@
4.4  structure Refute : REFUTE =
4.5  struct
4.6
4.7 -open PropLogic;
4.8 +open Prop_Logic;
4.9
4.10  (* We use 'REFUTE' only for internal error conditions that should    *)
4.11  (* never occur in the first place (i.e. errors caused by bugs in our *)
4.12 @@ -1118,8 +1118,8 @@
4.13              (* make 'u' either true or false, and make all axioms true, and *)
4.14              (* add the well-formedness side condition                       *)
4.15              val fm_u = (if negate then toFalse else toTrue) (hd intrs)
4.16 -            val fm_ax = PropLogic.all (map toTrue (tl intrs))
4.17 -            val fm = PropLogic.all [#wellformed args, fm_ax, fm_u]
4.18 +            val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
4.19 +            val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
4.20              val _ =
4.21                (if satsolver = "dpll" orelse satsolver = "enumerate" then
4.22                  warning ("Using SAT solver " ^ quote satsolver ^
4.23 @@ -1394,22 +1394,22 @@
4.24        (case i1 of
4.25          Leaf xs =>
4.26            (case i2 of
4.27 -            Leaf ys => PropLogic.dot_product (xs, ys)  (* defined and equal *)
4.28 +            Leaf ys => Prop_Logic.dot_product (xs, ys)  (* defined and equal *)
4.29            | Node _  => raise REFUTE ("make_equality",
4.30              "second interpretation is higher"))
4.31        | Node xs =>
4.32            (case i2 of
4.33              Leaf _  => raise REFUTE ("make_equality",
4.34              "first interpretation is higher")
4.35 -          | Node ys => PropLogic.all (map equal (xs ~~ ys))))
4.36 +          | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
4.37      (* interpretation * interpretation -> prop_formula *)
4.38      fun not_equal (i1, i2) =
4.39        (case i1 of
4.40          Leaf xs =>
4.41            (case i2 of
4.42              (* defined and not equal *)
4.43 -            Leaf ys => PropLogic.all ((PropLogic.exists xs)
4.44 -            :: (PropLogic.exists ys)
4.45 +            Leaf ys => Prop_Logic.all ((Prop_Logic.exists xs)
4.46 +            :: (Prop_Logic.exists ys)
4.47              :: (map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys)))
4.48            | Node _  => raise REFUTE ("make_equality",
4.49              "second interpretation is higher"))
4.50 @@ -1417,7 +1417,7 @@
4.51            (case i2 of
4.52              Leaf _  => raise REFUTE ("make_equality",
4.53              "first interpretation is higher")
4.54 -          | Node ys => PropLogic.exists (map not_equal (xs ~~ ys))))
4.55 +          | Node ys => Prop_Logic.exists (map not_equal (xs ~~ ys))))
4.56    in
4.57      (* a value may be undefined; therefore 'not_equal' is not just the *)
4.58      (* negation of 'equal'                                             *)
4.59 @@ -1443,15 +1443,15 @@
4.60          Leaf xs =>
4.61            (case i2 of
4.62              (* defined and equal, or both undefined *)
4.63 -            Leaf ys => SOr (PropLogic.dot_product (xs, ys),
4.64 -            SAnd (PropLogic.all (map SNot xs), PropLogic.all (map SNot ys)))
4.65 +            Leaf ys => SOr (Prop_Logic.dot_product (xs, ys),
4.66 +            SAnd (Prop_Logic.all (map SNot xs), Prop_Logic.all (map SNot ys)))
4.67            | Node _  => raise REFUTE ("make_def_equality",
4.68              "second interpretation is higher"))
4.69        | Node xs =>
4.70            (case i2 of
4.71              Leaf _  => raise REFUTE ("make_def_equality",
4.72              "first interpretation is higher")
4.73 -          | Node ys => PropLogic.all (map equal (xs ~~ ys))))
4.74 +          | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
4.75      (* interpretation *)
4.76      val eq = equal (i1, i2)
4.77    in
4.78 @@ -1499,7 +1499,7 @@
4.79      (* interpretation -> prop_formula list *)
4.80      fun interpretation_to_prop_formula_list (Leaf xs) = xs
4.81        | interpretation_to_prop_formula_list (Node trees) =
4.82 -          map PropLogic.all (pick_all
4.83 +          map Prop_Logic.all (pick_all
4.84              (map interpretation_to_prop_formula_list trees))
4.85    in
4.86      case i1 of
4.87 @@ -1571,7 +1571,7 @@
4.88              val intr = Leaf fms
4.89              (* prop_formula list -> prop_formula *)
4.90              fun one_of_two_false [] = True
4.91 -              | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' =>
4.92 +              | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
4.93                    SOr (SNot x, SNot x')) xs), one_of_two_false xs)
4.94              (* prop_formula *)
4.95              val wf = one_of_two_false fms
4.96 @@ -1672,8 +1672,8 @@
4.97            Node xs =>
4.98              (* 3-valued logic *)
4.99              let
4.100 -              val fmTrue  = PropLogic.all (map toTrue xs)
4.101 -              val fmFalse = PropLogic.exists (map toFalse xs)
4.102 +              val fmTrue  = Prop_Logic.all (map toTrue xs)
4.103 +              val fmFalse = Prop_Logic.exists (map toFalse xs)
4.104              in
4.105                SOME (Leaf [fmTrue, fmFalse], m, a)
4.106              end
4.107 @@ -1701,8 +1701,8 @@
4.108        let
4.109          val (i1, m1, a1) = interpret ctxt model args t1
4.110          val (i2, m2, a2) = interpret ctxt m1 a1 t2
4.111 -        val fmTrue       = PropLogic.SOr (toFalse i1, toTrue i2)
4.112 -        val fmFalse      = PropLogic.SAnd (toTrue i1, toFalse i2)
4.113 +        val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2)
4.114 +        val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2)
4.115        in
4.116          SOME (Leaf [fmTrue, fmFalse], m2, a2)
4.117        end
4.118 @@ -1735,8 +1735,8 @@
4.119            Node xs =>
4.120              (* 3-valued logic *)
4.121              let
4.122 -              val fmTrue  = PropLogic.all (map toTrue xs)
4.123 -              val fmFalse = PropLogic.exists (map toFalse xs)
4.124 +              val fmTrue = Prop_Logic.all (map toTrue xs)
4.125 +              val fmFalse = Prop_Logic.exists (map toFalse xs)
4.126              in
4.127                SOME (Leaf [fmTrue, fmFalse], m, a)
4.128              end
4.129 @@ -1754,8 +1754,8 @@
4.130            Node xs =>
4.131              (* 3-valued logic *)
4.132              let
4.133 -              val fmTrue  = PropLogic.exists (map toTrue xs)
4.134 -              val fmFalse = PropLogic.all (map toFalse xs)
4.135 +              val fmTrue = Prop_Logic.exists (map toTrue xs)
4.136 +              val fmFalse = Prop_Logic.all (map toFalse xs)
4.137              in
4.138                SOME (Leaf [fmTrue, fmFalse], m, a)
4.139              end
4.140 @@ -1781,8 +1781,8 @@
4.141        let
4.142          val (i1, m1, a1) = interpret ctxt model args t1
4.143          val (i2, m2, a2) = interpret ctxt m1 a1 t2
4.144 -        val fmTrue       = PropLogic.SAnd (toTrue i1, toTrue i2)
4.145 -        val fmFalse      = PropLogic.SOr (toFalse i1, toFalse i2)
4.146 +        val fmTrue = Prop_Logic.SAnd (toTrue i1, toTrue i2)
4.147 +        val fmFalse = Prop_Logic.SOr (toFalse i1, toFalse i2)
4.148        in
4.149          SOME (Leaf [fmTrue, fmFalse], m2, a2)
4.150        end
4.151 @@ -1798,8 +1798,8 @@
4.152        let
4.153          val (i1, m1, a1) = interpret ctxt model args t1
4.154          val (i2, m2, a2) = interpret ctxt m1 a1 t2
4.155 -        val fmTrue       = PropLogic.SOr (toTrue i1, toTrue i2)
4.156 -        val fmFalse      = PropLogic.SAnd (toFalse i1, toFalse i2)
4.157 +        val fmTrue = Prop_Logic.SOr (toTrue i1, toTrue i2)
4.158 +        val fmFalse = Prop_Logic.SAnd (toFalse i1, toFalse i2)
4.159        in
4.160          SOME (Leaf [fmTrue, fmFalse], m2, a2)
4.161        end
4.162 @@ -1815,8 +1815,8 @@
4.163        let
4.164          val (i1, m1, a1) = interpret ctxt model args t1
4.165          val (i2, m2, a2) = interpret ctxt m1 a1 t2
4.166 -        val fmTrue       = PropLogic.SOr (toFalse i1, toTrue i2)
4.167 -        val fmFalse      = PropLogic.SAnd (toTrue i1, toFalse i2)
4.168 +        val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2)
4.169 +        val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2)
4.170        in
4.171          SOME (Leaf [fmTrue, fmFalse], m2, a2)
4.172        end
4.173 @@ -1890,7 +1890,7 @@
4.174                      val intr     = Leaf fms
4.175                      (* prop_formula list -> prop_formula *)
4.176                      fun one_of_two_false [] = True
4.177 -                      | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' =>
4.178 +                      | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
4.179                            SOr (SNot x, SNot x')) xs), one_of_two_false xs)
4.180                      (* prop_formula *)
4.181                      val wf = one_of_two_false fms
4.182 @@ -2961,7 +2961,7 @@
4.183            strip_leading_quote x ^ string_of_int i
4.184      (* interpretation -> int *)
4.185      fun index_from_interpretation (Leaf xs) =
4.186 -          find_index (PropLogic.eval assignment) xs
4.187 +          find_index (Prop_Logic.eval assignment) xs
4.188        | index_from_interpretation _ =
4.189            raise REFUTE ("stlc_printer",
4.190              "interpretation for ground type is not a leaf")
4.191 @@ -3045,7 +3045,7 @@
4.192                (* the index of the element in the datatype *)
4.193                val element =
4.194                  (case intr of
4.195 -                  Leaf xs => find_index (PropLogic.eval assignment) xs
4.196 +                  Leaf xs => find_index (Prop_Logic.eval assignment) xs
4.197                  | Node _  => raise REFUTE ("IDT_printer",
4.198                    "interpretation is not a leaf"))
4.199              in
```
```     5.1 --- a/src/HOL/Tools/sat_funcs.ML	Sat Jan 08 14:32:55 2011 +0100
5.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sat Jan 08 16:01:51 2011 +0100
5.3 @@ -266,13 +266,13 @@
5.4  (*      a 'prop_formula' (just for tracing)                                  *)
5.5  (* ------------------------------------------------------------------------- *)
5.6
5.7 -fun string_of_prop_formula PropLogic.True = "True"
5.8 -  | string_of_prop_formula PropLogic.False = "False"
5.9 -  | string_of_prop_formula (PropLogic.BoolVar i) = "x" ^ string_of_int i
5.10 -  | string_of_prop_formula (PropLogic.Not fm) = "~" ^ string_of_prop_formula fm
5.11 -  | string_of_prop_formula (PropLogic.Or (fm1, fm2)) =
5.12 +fun string_of_prop_formula Prop_Logic.True = "True"
5.13 +  | string_of_prop_formula Prop_Logic.False = "False"
5.14 +  | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
5.15 +  | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
5.16 +  | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
5.17        "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
5.18 -  | string_of_prop_formula (PropLogic.And (fm1, fm2)) =
5.19 +  | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
5.20        "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
5.21
5.22  (* ------------------------------------------------------------------------- *)
5.23 @@ -313,15 +313,15 @@
5.24          tracing ("Sorted non-trivial clauses:\n" ^
5.25            cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
5.26        else ()
5.27 -    (* translate clauses from HOL terms to PropLogic.prop_formula *)
5.28 +    (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
5.29      val (fms, atom_table) =
5.30 -      fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
5.31 +      fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
5.32          sorted_clauses Termtab.empty
5.33      val _ =
5.34        if !trace_sat then
5.35          tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
5.36        else ()
5.37 -    val fm = PropLogic.all fms
5.38 +    val fm = Prop_Logic.all fms
5.39      (* unit -> Thm.thm *)
5.40      fun make_quick_and_dirty_thm () =
5.41        let
```
```     6.1 --- a/src/HOL/Tools/sat_solver.ML	Sat Jan 08 14:32:55 2011 +0100
6.2 +++ b/src/HOL/Tools/sat_solver.ML	Sat Jan 08 16:01:51 2011 +0100
6.3 @@ -14,16 +14,16 @@
6.4    datatype result = SATISFIABLE of assignment
6.5                    | UNSATISFIABLE of proof option
6.6                    | UNKNOWN
6.7 -  type solver     = PropLogic.prop_formula -> result
6.8 +  type solver     = Prop_Logic.prop_formula -> result
6.9
6.10    (* auxiliary functions to create external SAT solvers *)
6.11 -  val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
6.12 -  val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
6.13 -  val read_std_result_file  : Path.T -> string * string * string -> result
6.14 -  val make_external_solver  : string -> (PropLogic.prop_formula -> unit) ->
6.15 -                                (unit -> result) -> solver
6.16 +  val write_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula -> unit
6.17 +  val write_dimacs_sat_file : Path.T -> Prop_Logic.prop_formula -> unit
6.18 +  val read_std_result_file : Path.T -> string * string * string -> result
6.19 +  val make_external_solver : string -> (Prop_Logic.prop_formula -> unit) ->
6.20 +    (unit -> result) -> solver
6.21
6.22 -  val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
6.23 +  val read_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula
6.24
6.25    (* generic solver interface *)
6.26    val solvers       : (string * solver) list Unsynchronized.ref
6.27 @@ -34,7 +34,7 @@
6.28  structure SatSolver : SAT_SOLVER =
6.29  struct
6.30
6.31 -  open PropLogic;
6.32 +  open Prop_Logic;
6.33
6.34  (* ------------------------------------------------------------------------- *)
6.35  (* should be raised by an external SAT solver to indicate that the solver is *)
6.36 @@ -279,8 +279,6 @@
6.37  (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn'        *)
6.38  (* ------------------------------------------------------------------------- *)
6.39
6.40 -  (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *)
6.41 -
6.42    fun make_external_solver cmd writefn readfn fm =
6.43      (writefn fm; bash cmd; readfn ());
6.44
6.45 @@ -289,8 +287,6 @@
6.46  (*      a SAT problem given in DIMACS CNF format                             *)
6.47  (* ------------------------------------------------------------------------- *)
6.48
6.49 -  (* Path.T -> PropLogic.prop_formula *)
6.50 -
6.52    let
6.53      (* string list -> string list *)
6.54 @@ -323,27 +319,24 @@
6.55          | (0::tl) => xs1 :: clauses tl
6.56          | _       => raise Fail "SatSolver.clauses"
6.57        end
6.58 -    (* int -> PropLogic.prop_formula *)
6.59      fun literal_from_int i =
6.60        (i<>0 orelse error "variable index in DIMACS CNF file is 0";
6.61        if i>0 then
6.62 -        PropLogic.BoolVar i
6.63 +        Prop_Logic.BoolVar i
6.64        else
6.65 -        PropLogic.Not (PropLogic.BoolVar (~i)))
6.66 -    (* PropLogic.prop_formula list -> PropLogic.prop_formula *)
6.67 +        Prop_Logic.Not (Prop_Logic.BoolVar (~i)))
6.68      fun disjunction [] =
6.69        error "empty clause in DIMACS CNF file"
6.70        | disjunction (x::xs) =
6.71        (case xs of
6.72          [] => x
6.73 -      | _  => PropLogic.Or (x, disjunction xs))
6.74 -    (* PropLogic.prop_formula list -> PropLogic.prop_formula *)
6.75 +      | _  => Prop_Logic.Or (x, disjunction xs))
6.76      fun conjunction [] =
6.77        error "no clause in DIMACS CNF file"
6.78        | conjunction (x::xs) =
6.79        (case xs of
6.80          [] => x
6.81 -      | _  => PropLogic.And (x, conjunction xs))
6.82 +      | _  => Prop_Logic.And (x, conjunction xs))
6.83    in
6.84      (conjunction
6.85      o (map disjunction)
6.86 @@ -405,7 +398,7 @@
6.87    fun enum_solver fm =
6.88    let
6.89      (* int list *)
6.90 -    val indices = PropLogic.indices fm
6.91 +    val indices = Prop_Logic.indices fm
6.92      (* int list -> int list -> int list option *)
6.93      (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *)
6.94      fun next_list _ ([]:int list) =
6.95 @@ -424,7 +417,7 @@
6.96        member (op =) xs i
6.97      (* int list -> SatSolver.result *)
6.98      fun solver_loop xs =
6.99 -      if PropLogic.eval (assignment_from_list xs) fm then
6.100 +      if Prop_Logic.eval (assignment_from_list xs) fm then
6.101          SatSolver.SATISFIABLE (SOME o (assignment_from_list xs))
6.102        else
6.103          (case next_list xs indices of
6.104 @@ -446,16 +439,16 @@
6.105
6.106  let
6.107    local
6.108 -    open PropLogic
6.109 +    open Prop_Logic
6.110    in
6.111      fun dpll_solver fm =
6.112      let
6.113 -      (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *)
6.114 +      (* We could use 'Prop_Logic.defcnf fm' instead of 'Prop_Logic.nnf fm' *)
6.115        (* but that sometimes leads to worse performance due to the         *)
6.116        (* introduction of additional variables.                            *)
6.117 -      val fm' = PropLogic.nnf fm
6.118 +      val fm' = Prop_Logic.nnf fm
6.119        (* int list *)
6.120 -      val indices = PropLogic.indices fm'
6.121 +      val indices = Prop_Logic.indices fm'
6.122        (* int list -> int -> prop_formula *)
6.123        fun partial_var_eval []      i = BoolVar i
6.124          | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
6.125 @@ -587,7 +580,7 @@
6.127      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
6.128      val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
6.129 -    val cnf        = PropLogic.defcnf fm
6.130 +    val cnf        = Prop_Logic.defcnf fm
6.131      val result     = SatSolver.make_external_solver cmd writefn readfn cnf
6.132      val _          = try File.rm inpath
6.133      val _          = try File.rm outpath
6.134 @@ -599,16 +592,16 @@
6.135          handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
6.136        (* representation of clauses as ordered lists of literals (with duplicates removed) *)
6.137        (* prop_formula -> int list *)
6.138 -      fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
6.139 +      fun clause_to_lit_list (Prop_Logic.Or (fm1, fm2)) =
6.140          Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
6.141 -        | clause_to_lit_list (PropLogic.BoolVar i) =
6.142 +        | clause_to_lit_list (Prop_Logic.BoolVar i) =
6.143          [i]
6.144 -        | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) =
6.145 +        | clause_to_lit_list (Prop_Logic.Not (Prop_Logic.BoolVar i)) =
6.146          [~i]
6.147          | clause_to_lit_list _ =
6.148          raise INVALID_PROOF "Error: invalid clause in CNF formula."
6.149        (* prop_formula -> int *)
6.150 -      fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) =
6.151 +      fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
6.152          cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
6.153          | cnf_number_of_clauses _ =
6.154          1
6.155 @@ -617,7 +610,7 @@
6.156        val clauses = Array.array (number_of_clauses, [])
6.157        (* initialize the 'clauses' array *)
6.158        (* prop_formula * int -> int *)
6.159 -      fun init_array (PropLogic.And (fm1, fm2), n) =
6.160 +      fun init_array (Prop_Logic.And (fm1, fm2), n) =
6.161          init_array (fm2, init_array (fm1, n))
6.162          | init_array (fm, n) =
6.163          (Array.update (clauses, n, clause_to_lit_list fm); n+1)
6.164 @@ -768,7 +761,7 @@
6.165      val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
6.166      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
6.167      val cmd        = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " > /dev/null"
6.168 -    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
6.169 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
6.171      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
6.172      val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
6.173 @@ -806,9 +799,9 @@
6.174        (* string list *)
6.175        val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
6.176          handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
6.177 -      (* PropLogic.prop_formula -> int *)
6.178 -      fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
6.179 -        | cnf_number_of_clauses _                          = 1
6.180 +      fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
6.181 +            cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
6.182 +        | cnf_number_of_clauses _ = 1
6.183        (* string -> int *)
6.184        fun int_from_string s = (
6.185          case Int.fromString s of
6.186 @@ -848,7 +841,7 @@
6.187                val _   = if !clause_offset = ~1 then clause_offset :=
6.188                  (case Inttab.max_key (!clause_table) of
6.189                    SOME id => id
6.190 -                | NONE    => cnf_number_of_clauses (PropLogic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
6.191 +                | NONE => cnf_number_of_clauses (Prop_Logic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
6.192                  else
6.193                    ()
6.194                val vid = int_from_string id
6.195 @@ -927,7 +920,7 @@
6.196      val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
6.197      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
6.198      val cmd        = getenv "ZCHAFF_HOME" ^ "/zchaff " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
6.199 -    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
6.200 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
6.201      fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
6.202      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
6.203      val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
6.204 @@ -954,7 +947,7 @@
6.205      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
6.206      val exec       = getenv "BERKMIN_EXE"
6.207      val cmd        = getenv "BERKMIN_HOME" ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
6.208 -    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
6.209 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
6.210      fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
6.211      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
6.212      val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
6.213 @@ -980,7 +973,7 @@
6.214      val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
6.215      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
6.216      val cmd        = getenv "JERUSAT_HOME" ^ "/Jerusat1.3 " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
6.217 -    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
6.218 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
6.219      fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
6.220      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
6.221      val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
```
```     7.1 --- a/src/HOL/ex/SAT_Examples.thy	Sat Jan 08 14:32:55 2011 +0100
7.2 +++ b/src/HOL/ex/SAT_Examples.thy	Sat Jan 08 16:01:51 2011 +0100
7.3 @@ -533,12 +533,10 @@
7.4  fun benchmark dimacsfile =
7.5  let
7.6    val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile)
7.7 -  fun and_to_list (PropLogic.And (fm1, fm2)) acc =
7.8 -    and_to_list fm2 (fm1 :: acc)
7.9 -    | and_to_list fm acc =
7.10 -    rev (fm :: acc)
7.11 +  fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
7.12 +    | and_to_list fm acc = rev (fm :: acc)
7.13    val clauses = and_to_list prop_fm []
7.14 -  val terms   = map (HOLogic.mk_Trueprop o PropLogic.term_of_prop_formula)
7.15 +  val terms   = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula)
7.16      clauses
7.17    val cterms  = map (Thm.cterm_of @{theory}) terms
7.18    val timer   = start_timing ()
```