# HG changeset patch # User wenzelm # Date 1294498911 -3600 # Node ID 54a58904a598bdde86f322aeccb31e2eefcda0af # Parent 890b25753bf70d43919b57fe4d5db17959c466f1 modernized structure Prop_Logic; avoid ML structure aliases; diff -r 890b25753bf7 -r 54a58904a598 src/HOL/Tools/Function/scnp_solve.ML --- a/src/HOL/Tools/Function/scnp_solve.ML Sat Jan 08 14:32:55 2011 +0100 +++ b/src/HOL/Tools/Function/scnp_solve.ML Sat Jan 08 16:01:51 2011 +0100 @@ -51,11 +51,11 @@ (** Propositional formulas **) -val Not = PropLogic.Not and And = PropLogic.And and Or = PropLogic.Or -val BoolVar = PropLogic.BoolVar +val Not = Prop_Logic.Not and And = Prop_Logic.And and Or = Prop_Logic.Or +val BoolVar = Prop_Logic.BoolVar fun Implies (p, q) = Or (Not p, q) fun Equiv (p, q) = And (Implies (p, q), Implies (q, p)) -val all = PropLogic.all +val all = Prop_Logic.all (* finite indexed quantifiers: @@ -64,7 +64,7 @@ 0<=i fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0)) (bits - 1 downto 0) 0) diff -r 890b25753bf7 -r 54a58904a598 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Jan 08 14:32:55 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Jan 08 16:01:51 2011 +0100 @@ -20,8 +20,6 @@ open Nitpick_Util open Nitpick_HOL -structure PL = PropLogic - datatype sign = Plus | Minus type var = int @@ -474,36 +472,36 @@ val bools_from_annotation = AList.lookup (op =) bool_table #> the val annotation_from_bools = AList.find (op =) bool_table #> the_single -fun prop_for_bool b = if b then PL.True else PL.False +fun prop_for_bool b = if b then Prop_Logic.True else Prop_Logic.False fun prop_for_bool_var_equality (v1, v2) = - PL.SAnd (PL.SOr (PL.BoolVar v1, PL.SNot (PL.BoolVar v2)), - PL.SOr (PL.SNot (PL.BoolVar v1), PL.BoolVar v2)) + Prop_Logic.SAnd (Prop_Logic.SOr (Prop_Logic.BoolVar v1, Prop_Logic.SNot (Prop_Logic.BoolVar v2)), + Prop_Logic.SOr (Prop_Logic.SNot (Prop_Logic.BoolVar v1), Prop_Logic.BoolVar v2)) fun prop_for_assign (x, a) = let val (b1, b2) = bools_from_annotation a in - PL.SAnd (PL.BoolVar (fst_var x) |> not b1 ? PL.SNot, - PL.BoolVar (snd_var x) |> not b2 ? PL.SNot) + Prop_Logic.SAnd (Prop_Logic.BoolVar (fst_var x) |> not b1 ? Prop_Logic.SNot, + Prop_Logic.BoolVar (snd_var x) |> not b2 ? Prop_Logic.SNot) end fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a) - | prop_for_assign_literal (x, (Minus, a)) = PL.SNot (prop_for_assign (x, a)) + | prop_for_assign_literal (x, (Minus, a)) = Prop_Logic.SNot (prop_for_assign (x, a)) fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a') | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a)) fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2) | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1) | prop_for_atom_equality (V x1, V x2) = - PL.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)), + Prop_Logic.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)), prop_for_bool_var_equality (pairself snd_var (x1, x2))) -val prop_for_assign_clause = PL.exists o map prop_for_assign_literal +val prop_for_assign_clause = Prop_Logic.exists o map prop_for_assign_literal fun prop_for_exists_var_assign_literal xs a = - PL.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs) + Prop_Logic.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs) fun prop_for_comp (aa1, aa2, Eq, []) = - PL.SAnd (prop_for_comp (aa1, aa2, Leq, []), + Prop_Logic.SAnd (prop_for_comp (aa1, aa2, Leq, []), prop_for_comp (aa2, aa1, Leq, [])) | prop_for_comp (aa1, aa2, Neq, []) = - PL.SNot (prop_for_comp (aa1, aa2, Eq, [])) + Prop_Logic.SNot (prop_for_comp (aa1, aa2, Eq, [])) | prop_for_comp (aa1, aa2, Leq, []) = - PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen)) + Prop_Logic.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen)) | prop_for_comp (aa1, aa2, cmp, xs) = - PL.SOr (prop_for_exists_var_assign_literal xs Gen, + Prop_Logic.SOr (prop_for_exists_var_assign_literal xs Gen, prop_for_comp (aa1, aa2, cmp, [])) fun extract_assigns max_var assigns asgs = @@ -542,11 +540,11 @@ SOME (extract_assigns max_var assigns asgs |> tap print_solution) val _ = print_problem comps clauses val prop = - PL.all (map prop_for_comp comps @ map prop_for_assign_clause clauses) + Prop_Logic.all (map prop_for_comp comps @ map prop_for_assign_clause clauses) in - if PL.eval (K false) prop then + if Prop_Logic.eval (K false) prop then do_assigns (K (SOME false)) - else if PL.eval (K true) prop then + else if Prop_Logic.eval (K true) prop then do_assigns (K (SOME true)) else let diff -r 890b25753bf7 -r 54a58904a598 src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Sat Jan 08 14:32:55 2011 +0100 +++ b/src/HOL/Tools/prop_logic.ML Sat Jan 08 16:01:51 2011 +0100 @@ -42,7 +42,7 @@ val term_of_prop_formula: prop_formula -> term end; -structure PropLogic : PROP_LOGIC = +structure Prop_Logic : PROP_LOGIC = struct (* ------------------------------------------------------------------------- *) diff -r 890b25753bf7 -r 54a58904a598 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Sat Jan 08 14:32:55 2011 +0100 +++ b/src/HOL/Tools/refute.ML Sat Jan 08 16:01:51 2011 +0100 @@ -77,7 +77,7 @@ structure Refute : REFUTE = struct -open PropLogic; +open Prop_Logic; (* We use 'REFUTE' only for internal error conditions that should *) (* never occur in the first place (i.e. errors caused by bugs in our *) @@ -1118,8 +1118,8 @@ (* make 'u' either true or false, and make all axioms true, and *) (* add the well-formedness side condition *) val fm_u = (if negate then toFalse else toTrue) (hd intrs) - val fm_ax = PropLogic.all (map toTrue (tl intrs)) - val fm = PropLogic.all [#wellformed args, fm_ax, fm_u] + val fm_ax = Prop_Logic.all (map toTrue (tl intrs)) + val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u] val _ = (if satsolver = "dpll" orelse satsolver = "enumerate" then warning ("Using SAT solver " ^ quote satsolver ^ @@ -1394,22 +1394,22 @@ (case i1 of Leaf xs => (case i2 of - Leaf ys => PropLogic.dot_product (xs, ys) (* defined and equal *) + Leaf ys => Prop_Logic.dot_product (xs, ys) (* defined and equal *) | Node _ => raise REFUTE ("make_equality", "second interpretation is higher")) | Node xs => (case i2 of Leaf _ => raise REFUTE ("make_equality", "first interpretation is higher") - | Node ys => PropLogic.all (map equal (xs ~~ ys)))) + | Node ys => Prop_Logic.all (map equal (xs ~~ ys)))) (* interpretation * interpretation -> prop_formula *) fun not_equal (i1, i2) = (case i1 of Leaf xs => (case i2 of (* defined and not equal *) - Leaf ys => PropLogic.all ((PropLogic.exists xs) - :: (PropLogic.exists ys) + Leaf ys => Prop_Logic.all ((Prop_Logic.exists xs) + :: (Prop_Logic.exists ys) :: (map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys))) | Node _ => raise REFUTE ("make_equality", "second interpretation is higher")) @@ -1417,7 +1417,7 @@ (case i2 of Leaf _ => raise REFUTE ("make_equality", "first interpretation is higher") - | Node ys => PropLogic.exists (map not_equal (xs ~~ ys)))) + | Node ys => Prop_Logic.exists (map not_equal (xs ~~ ys)))) in (* a value may be undefined; therefore 'not_equal' is not just the *) (* negation of 'equal' *) @@ -1443,15 +1443,15 @@ Leaf xs => (case i2 of (* defined and equal, or both undefined *) - Leaf ys => SOr (PropLogic.dot_product (xs, ys), - SAnd (PropLogic.all (map SNot xs), PropLogic.all (map SNot ys))) + Leaf ys => SOr (Prop_Logic.dot_product (xs, ys), + SAnd (Prop_Logic.all (map SNot xs), Prop_Logic.all (map SNot ys))) | Node _ => raise REFUTE ("make_def_equality", "second interpretation is higher")) | Node xs => (case i2 of Leaf _ => raise REFUTE ("make_def_equality", "first interpretation is higher") - | Node ys => PropLogic.all (map equal (xs ~~ ys)))) + | Node ys => Prop_Logic.all (map equal (xs ~~ ys)))) (* interpretation *) val eq = equal (i1, i2) in @@ -1499,7 +1499,7 @@ (* interpretation -> prop_formula list *) fun interpretation_to_prop_formula_list (Leaf xs) = xs | interpretation_to_prop_formula_list (Node trees) = - map PropLogic.all (pick_all + map Prop_Logic.all (pick_all (map interpretation_to_prop_formula_list trees)) in case i1 of @@ -1571,7 +1571,7 @@ val intr = Leaf fms (* prop_formula list -> prop_formula *) fun one_of_two_false [] = True - | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => + | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs) (* prop_formula *) val wf = one_of_two_false fms @@ -1672,8 +1672,8 @@ Node xs => (* 3-valued logic *) let - val fmTrue = PropLogic.all (map toTrue xs) - val fmFalse = PropLogic.exists (map toFalse xs) + val fmTrue = Prop_Logic.all (map toTrue xs) + val fmFalse = Prop_Logic.exists (map toFalse xs) in SOME (Leaf [fmTrue, fmFalse], m, a) end @@ -1701,8 +1701,8 @@ let val (i1, m1, a1) = interpret ctxt model args t1 val (i2, m2, a2) = interpret ctxt m1 a1 t2 - val fmTrue = PropLogic.SOr (toFalse i1, toTrue i2) - val fmFalse = PropLogic.SAnd (toTrue i1, toFalse i2) + val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2) + val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2) in SOME (Leaf [fmTrue, fmFalse], m2, a2) end @@ -1735,8 +1735,8 @@ Node xs => (* 3-valued logic *) let - val fmTrue = PropLogic.all (map toTrue xs) - val fmFalse = PropLogic.exists (map toFalse xs) + val fmTrue = Prop_Logic.all (map toTrue xs) + val fmFalse = Prop_Logic.exists (map toFalse xs) in SOME (Leaf [fmTrue, fmFalse], m, a) end @@ -1754,8 +1754,8 @@ Node xs => (* 3-valued logic *) let - val fmTrue = PropLogic.exists (map toTrue xs) - val fmFalse = PropLogic.all (map toFalse xs) + val fmTrue = Prop_Logic.exists (map toTrue xs) + val fmFalse = Prop_Logic.all (map toFalse xs) in SOME (Leaf [fmTrue, fmFalse], m, a) end @@ -1781,8 +1781,8 @@ let val (i1, m1, a1) = interpret ctxt model args t1 val (i2, m2, a2) = interpret ctxt m1 a1 t2 - val fmTrue = PropLogic.SAnd (toTrue i1, toTrue i2) - val fmFalse = PropLogic.SOr (toFalse i1, toFalse i2) + val fmTrue = Prop_Logic.SAnd (toTrue i1, toTrue i2) + val fmFalse = Prop_Logic.SOr (toFalse i1, toFalse i2) in SOME (Leaf [fmTrue, fmFalse], m2, a2) end @@ -1798,8 +1798,8 @@ let val (i1, m1, a1) = interpret ctxt model args t1 val (i2, m2, a2) = interpret ctxt m1 a1 t2 - val fmTrue = PropLogic.SOr (toTrue i1, toTrue i2) - val fmFalse = PropLogic.SAnd (toFalse i1, toFalse i2) + val fmTrue = Prop_Logic.SOr (toTrue i1, toTrue i2) + val fmFalse = Prop_Logic.SAnd (toFalse i1, toFalse i2) in SOME (Leaf [fmTrue, fmFalse], m2, a2) end @@ -1815,8 +1815,8 @@ let val (i1, m1, a1) = interpret ctxt model args t1 val (i2, m2, a2) = interpret ctxt m1 a1 t2 - val fmTrue = PropLogic.SOr (toFalse i1, toTrue i2) - val fmFalse = PropLogic.SAnd (toTrue i1, toFalse i2) + val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2) + val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2) in SOME (Leaf [fmTrue, fmFalse], m2, a2) end @@ -1890,7 +1890,7 @@ val intr = Leaf fms (* prop_formula list -> prop_formula *) fun one_of_two_false [] = True - | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => + | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs) (* prop_formula *) val wf = one_of_two_false fms @@ -2961,7 +2961,7 @@ strip_leading_quote x ^ string_of_int i (* interpretation -> int *) fun index_from_interpretation (Leaf xs) = - find_index (PropLogic.eval assignment) xs + find_index (Prop_Logic.eval assignment) xs | index_from_interpretation _ = raise REFUTE ("stlc_printer", "interpretation for ground type is not a leaf") @@ -3045,7 +3045,7 @@ (* the index of the element in the datatype *) val element = (case intr of - Leaf xs => find_index (PropLogic.eval assignment) xs + Leaf xs => find_index (Prop_Logic.eval assignment) xs | Node _ => raise REFUTE ("IDT_printer", "interpretation is not a leaf")) in diff -r 890b25753bf7 -r 54a58904a598 src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Sat Jan 08 14:32:55 2011 +0100 +++ b/src/HOL/Tools/sat_funcs.ML Sat Jan 08 16:01:51 2011 +0100 @@ -266,13 +266,13 @@ (* a 'prop_formula' (just for tracing) *) (* ------------------------------------------------------------------------- *) -fun string_of_prop_formula PropLogic.True = "True" - | string_of_prop_formula PropLogic.False = "False" - | string_of_prop_formula (PropLogic.BoolVar i) = "x" ^ string_of_int i - | string_of_prop_formula (PropLogic.Not fm) = "~" ^ string_of_prop_formula fm - | string_of_prop_formula (PropLogic.Or (fm1, fm2)) = +fun string_of_prop_formula Prop_Logic.True = "True" + | string_of_prop_formula Prop_Logic.False = "False" + | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i + | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm + | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")" - | string_of_prop_formula (PropLogic.And (fm1, fm2)) = + | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")"; (* ------------------------------------------------------------------------- *) @@ -313,15 +313,15 @@ tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) else () - (* translate clauses from HOL terms to PropLogic.prop_formula *) + (* translate clauses from HOL terms to Prop_Logic.prop_formula *) val (fms, atom_table) = - fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) + fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty val _ = if !trace_sat then tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) else () - val fm = PropLogic.all fms + val fm = Prop_Logic.all fms (* unit -> Thm.thm *) fun make_quick_and_dirty_thm () = let diff -r 890b25753bf7 -r 54a58904a598 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Sat Jan 08 14:32:55 2011 +0100 +++ b/src/HOL/Tools/sat_solver.ML Sat Jan 08 16:01:51 2011 +0100 @@ -14,16 +14,16 @@ datatype result = SATISFIABLE of assignment | UNSATISFIABLE of proof option | UNKNOWN - type solver = PropLogic.prop_formula -> result + type solver = Prop_Logic.prop_formula -> result (* auxiliary functions to create external SAT solvers *) - val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit - val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit - val read_std_result_file : Path.T -> string * string * string -> result - val make_external_solver : string -> (PropLogic.prop_formula -> unit) -> - (unit -> result) -> solver + val write_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula -> unit + val write_dimacs_sat_file : Path.T -> Prop_Logic.prop_formula -> unit + val read_std_result_file : Path.T -> string * string * string -> result + val make_external_solver : string -> (Prop_Logic.prop_formula -> unit) -> + (unit -> result) -> solver - val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula + val read_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula (* generic solver interface *) val solvers : (string * solver) list Unsynchronized.ref @@ -34,7 +34,7 @@ structure SatSolver : SAT_SOLVER = struct - open PropLogic; + open Prop_Logic; (* ------------------------------------------------------------------------- *) (* should be raised by an external SAT solver to indicate that the solver is *) @@ -279,8 +279,6 @@ (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn' *) (* ------------------------------------------------------------------------- *) - (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *) - fun make_external_solver cmd writefn readfn fm = (writefn fm; bash cmd; readfn ()); @@ -289,8 +287,6 @@ (* a SAT problem given in DIMACS CNF format *) (* ------------------------------------------------------------------------- *) - (* Path.T -> PropLogic.prop_formula *) - fun read_dimacs_cnf_file path = let (* string list -> string list *) @@ -323,27 +319,24 @@ | (0::tl) => xs1 :: clauses tl | _ => raise Fail "SatSolver.clauses" end - (* int -> PropLogic.prop_formula *) fun literal_from_int i = (i<>0 orelse error "variable index in DIMACS CNF file is 0"; if i>0 then - PropLogic.BoolVar i + Prop_Logic.BoolVar i else - PropLogic.Not (PropLogic.BoolVar (~i))) - (* PropLogic.prop_formula list -> PropLogic.prop_formula *) + Prop_Logic.Not (Prop_Logic.BoolVar (~i))) fun disjunction [] = error "empty clause in DIMACS CNF file" | disjunction (x::xs) = (case xs of [] => x - | _ => PropLogic.Or (x, disjunction xs)) - (* PropLogic.prop_formula list -> PropLogic.prop_formula *) + | _ => Prop_Logic.Or (x, disjunction xs)) fun conjunction [] = error "no clause in DIMACS CNF file" | conjunction (x::xs) = (case xs of [] => x - | _ => PropLogic.And (x, conjunction xs)) + | _ => Prop_Logic.And (x, conjunction xs)) in (conjunction o (map disjunction) @@ -405,7 +398,7 @@ fun enum_solver fm = let (* int list *) - val indices = PropLogic.indices fm + val indices = Prop_Logic.indices fm (* int list -> int list -> int list option *) (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *) fun next_list _ ([]:int list) = @@ -424,7 +417,7 @@ member (op =) xs i (* int list -> SatSolver.result *) fun solver_loop xs = - if PropLogic.eval (assignment_from_list xs) fm then + if Prop_Logic.eval (assignment_from_list xs) fm then SatSolver.SATISFIABLE (SOME o (assignment_from_list xs)) else (case next_list xs indices of @@ -446,16 +439,16 @@ let local - open PropLogic + open Prop_Logic in fun dpll_solver fm = let - (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *) + (* We could use 'Prop_Logic.defcnf fm' instead of 'Prop_Logic.nnf fm' *) (* but that sometimes leads to worse performance due to the *) (* introduction of additional variables. *) - val fm' = PropLogic.nnf fm + val fm' = Prop_Logic.nnf fm (* int list *) - val indices = PropLogic.indices fm' + val indices = Prop_Logic.indices fm' (* int list -> int -> prop_formula *) fun partial_var_eval [] i = BoolVar i | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i @@ -587,7 +580,7 @@ fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () - val cnf = PropLogic.defcnf fm + val cnf = Prop_Logic.defcnf fm val result = SatSolver.make_external_solver cmd writefn readfn cnf val _ = try File.rm inpath val _ = try File.rm outpath @@ -599,16 +592,16 @@ handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" (* representation of clauses as ordered lists of literals (with duplicates removed) *) (* prop_formula -> int list *) - fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) = + fun clause_to_lit_list (Prop_Logic.Or (fm1, fm2)) = Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2) - | clause_to_lit_list (PropLogic.BoolVar i) = + | clause_to_lit_list (Prop_Logic.BoolVar i) = [i] - | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = + | clause_to_lit_list (Prop_Logic.Not (Prop_Logic.BoolVar i)) = [~i] | clause_to_lit_list _ = raise INVALID_PROOF "Error: invalid clause in CNF formula." (* prop_formula -> int *) - fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = + fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 | cnf_number_of_clauses _ = 1 @@ -617,7 +610,7 @@ val clauses = Array.array (number_of_clauses, []) (* initialize the 'clauses' array *) (* prop_formula * int -> int *) - fun init_array (PropLogic.And (fm1, fm2), n) = + fun init_array (Prop_Logic.And (fm1, fm2), n) = init_array (fm2, init_array (fm1, n)) | init_array (fm, n) = (Array.update (clauses, n, clause_to_lit_list fm); n+1) @@ -768,7 +761,7 @@ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val cmd = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " > /dev/null" - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () @@ -806,9 +799,9 @@ (* string list *) val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" - (* PropLogic.prop_formula -> int *) - fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 - | cnf_number_of_clauses _ = 1 + fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = + cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 + | cnf_number_of_clauses _ = 1 (* string -> int *) fun int_from_string s = ( case Int.fromString s of @@ -848,7 +841,7 @@ val _ = if !clause_offset = ~1 then clause_offset := (case Inttab.max_key (!clause_table) of SOME id => id - | NONE => cnf_number_of_clauses (PropLogic.defcnf fm) - 1 (* the first clause ID is 0, not 1 *)) + | NONE => cnf_number_of_clauses (Prop_Logic.defcnf fm) - 1 (* the first clause ID is 0, not 1 *)) else () val vid = int_from_string id @@ -927,7 +920,7 @@ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val cmd = getenv "ZCHAFF_HOME" ^ "/zchaff " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () @@ -954,7 +947,7 @@ val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val exec = getenv "BERKMIN_EXE" val cmd = getenv "BERKMIN_HOME" ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () @@ -980,7 +973,7 @@ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val cmd = getenv "JERUSAT_HOME" ^ "/Jerusat1.3 " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () diff -r 890b25753bf7 -r 54a58904a598 src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Sat Jan 08 14:32:55 2011 +0100 +++ b/src/HOL/ex/SAT_Examples.thy Sat Jan 08 16:01:51 2011 +0100 @@ -533,12 +533,10 @@ fun benchmark dimacsfile = let val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile) - fun and_to_list (PropLogic.And (fm1, fm2)) acc = - and_to_list fm2 (fm1 :: acc) - | and_to_list fm acc = - rev (fm :: acc) + fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc) + | and_to_list fm acc = rev (fm :: acc) val clauses = and_to_list prop_fm [] - val terms = map (HOLogic.mk_Trueprop o PropLogic.term_of_prop_formula) + val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses val cterms = map (Thm.cterm_of @{theory}) terms val timer = start_timing ()