--- 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<n
*)
fun iforall n f = all (map_range f n)
-fun iexists n f = PropLogic.exists (map_range f n)
+fun iexists n f = Prop_Logic.exists (map_range f n)
fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1)))
@@ -112,7 +112,7 @@
val ng = num_graphs gp
val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp
- fun encode_constraint_strict 0 (x, y) = PropLogic.False
+ fun encode_constraint_strict 0 (x, y) = Prop_Logic.False
| encode_constraint_strict k (x, y) =
Or (And (TAG x (k - 1), Not (TAG y (k - 1))),
And (Equiv (TAG x (k - 1), TAG y (k - 1)),
@@ -212,7 +212,7 @@
fun mk_certificate bits label gp f =
let
val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp
- fun assign (PropLogic.BoolVar v) = the_default false (f v)
+ fun assign (Prop_Logic.BoolVar v) = the_default false (f v)
fun assignTag i j =
(fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0))
(bits - 1 downto 0) 0)
--- 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
--- 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
(* ------------------------------------------------------------------------- *)
--- 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
--- 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
--- 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 ()
--- 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 ()