--- a/src/HOL/Tools/refute.ML Thu Nov 09 16:14:43 2006 +0100
+++ b/src/HOL/Tools/refute.ML Thu Nov 09 18:48:45 2006 +0100
@@ -628,6 +628,8 @@
| Const ("List.op @", T) => collect_type_axioms (axs, T)
| Const ("Lfp.lfp", T) => collect_type_axioms (axs, T)
| Const ("Gfp.gfp", T) => collect_type_axioms (axs, T)
+ | Const ("fst", T) => collect_type_axioms (axs, T)
+ | Const ("snd", T) => collect_type_axioms (axs, T)
(* simply-typed lambda calculus *)
| Const (s, T) =>
let
@@ -2376,6 +2378,46 @@
| _ =>
NONE;
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
+
+ (* only an optimization: 'fst' could in principle be interpreted with *)
+ (* interpreters available already (using its definition), but the code *)
+ (* below is more efficient *)
+
+ fun Product_Type_fst_interpreter thy model args t =
+ case t of
+ Const ("fst", Type ("fun", [Type ("*", [T, U]), _])) =>
+ let
+ val (iT, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
+ val is_T = make_constants iT
+ val (iU, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", U))
+ val size_U = size_of_type iU
+ in
+ SOME (Node (List.concat (map (replicate size_U) is_T)), model, args)
+ end
+ | _ =>
+ NONE;
+
+ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
+
+ (* only an optimization: 'snd' could in principle be interpreted with *)
+ (* interpreters available already (using its definition), but the code *)
+ (* below is more efficient *)
+
+ fun Product_Type_snd_interpreter thy model args t =
+ case t of
+ Const ("snd", Type ("fun", [Type ("*", [T, U]), _])) =>
+ let
+ val (iT, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
+ val size_T = size_of_type iT
+ val (iU, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", U))
+ val is_U = make_constants iU
+ in
+ SOME (Node (List.concat (replicate size_T is_U)), model, args)
+ end
+ | _ =>
+ NONE;
+
(* ------------------------------------------------------------------------- *)
(* PRINTERS *)
@@ -2616,6 +2658,8 @@
add_interpreter "List.op @" List_append_interpreter #>
add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #>
add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #>
+ add_interpreter "fst" Product_Type_fst_interpreter #>
+ add_interpreter "snd" Product_Type_snd_interpreter #>
add_printer "stlc" stlc_printer #>
add_printer "set" set_printer #>
add_printer "IDT" IDT_printer;
--- a/src/HOL/Tools/sat_funcs.ML Thu Nov 09 16:14:43 2006 +0100
+++ b/src/HOL/Tools/sat_funcs.ML Thu Nov 09 18:48:45 2006 +0100
@@ -51,9 +51,10 @@
signature SAT =
sig
- val trace_sat : bool ref (* print trace messages *)
- val solver : string ref (* name of SAT solver to be used *)
- val counter : int ref (* number of resolution steps during last proof replay *)
+ val trace_sat : bool ref (* input: print trace messages *)
+ val solver : string ref (* input: name of SAT solver to be used *)
+ val counter : int ref (* output: number of resolution steps during last proof replay *)
+ val rawsat_thm : cterm list -> thm
val rawsat_tac : int -> Tactical.tactic
val sat_tac : int -> Tactical.tactic
val satx_tac : int -> Tactical.tactic
@@ -69,7 +70,7 @@
val counter = ref 0;
(* Thm.thm *)
-val resolution_thm = (* "[| P ==> False; ~P ==> False |] ==> False" *)
+val resolution_thm = (* "[| ?P ==> False; ~ ?P ==> False |] ==> False" *)
let
val cterm = cterm_of (the_context ())
val Q = Var (("Q", 0), HOLogic.boolT)
@@ -256,52 +257,70 @@
| string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
(* ------------------------------------------------------------------------- *)
-(* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *)
-(* a proof from the resulting proof trace of the SAT solver. Each *)
-(* premise in 'prems' that is not a clause is ignored, and the theorem *)
-(* returned is just "False" (with some clauses as hyps). *)
+(* take_prefix: *)
+(* take_prefix n [x_1, ..., x_k] = ([x_1, ..., x_n], [x_n+1, ..., x_k]) *)
(* ------------------------------------------------------------------------- *)
-(* Thm.thm list -> Thm.thm *)
+(* int -> 'a list -> 'a list * 'a list *)
+
+fun take_prefix n xs =
+let
+ fun take 0 (rxs, xs) = (rev rxs, xs)
+ | take _ (rxs, []) = (rev rxs, [])
+ | take n (rxs, x :: xs) = take (n-1) (x :: rxs, xs)
+in
+ take n ([], xs)
+end;
-fun rawsat_thm prems =
+(* ------------------------------------------------------------------------- *)
+(* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *)
+(* a proof from the resulting proof trace of the SAT solver. The *)
+(* theorem returned is just "False" (with some of the given clauses as *)
+(* hyps). *)
+(* ------------------------------------------------------------------------- *)
+
+(* Thm.cterm list -> Thm.thm *)
+
+fun rawsat_thm clauses =
let
(* remove premises that equal "True" *)
- val non_triv_prems = filter (fn thm =>
- (not_equal HOLogic.true_const o HOLogic.dest_Trueprop o prop_of) thm
- handle TERM ("dest_Trueprop", _) => true) prems
+ val clauses' = filter (fn clause =>
+ (not_equal HOLogic.true_const o HOLogic.dest_Trueprop o term_of) clause
+ handle TERM ("dest_Trueprop", _) => true) clauses
(* remove non-clausal premises -- of course this shouldn't actually *)
- (* remove anything as long as 'rawsat_thm' is only called after the *)
+ (* remove anything as long as 'rawsat_tac' is only called after the *)
(* premises have been converted to clauses *)
- val clauses = filter (fn thm =>
- ((cnf.is_clause o HOLogic.dest_Trueprop o prop_of) thm handle TERM ("dest_Trueprop", _) => false)
- orelse (warning ("Ignoring non-clausal premise " ^ (string_of_cterm o cprop_of) thm); false)) non_triv_prems
+ val clauses'' = filter (fn clause =>
+ ((cnf.is_clause o HOLogic.dest_Trueprop o term_of) clause
+ handle TERM ("dest_Trueprop", _) => false)
+ orelse (
+ warning ("Ignoring non-clausal premise " ^ string_of_cterm clause);
+ false)) clauses'
(* remove trivial clauses -- this is necessary because zChaff removes *)
(* trivial clauses during preprocessing, and otherwise our clause *)
(* numbering would be off *)
- val non_triv_clauses = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o prop_of) clauses
- val _ = if !trace_sat then
- tracing ("Non-trivial clauses:\n" ^ space_implode "\n" (map (string_of_cterm o cprop_of) non_triv_clauses))
+ val clauses''' = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o term_of) clauses''
+ val _ = if !trace_sat then
+ tracing ("Non-trivial clauses:\n" ^ space_implode "\n" (map string_of_cterm clauses'''))
else ()
(* translate clauses from HOL terms to PropLogic.prop_formula *)
- val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o prop_of) non_triv_clauses Termtab.empty
- val _ = if !trace_sat then
+ val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o term_of) clauses''' Termtab.empty
+ val _ = if !trace_sat then
tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms))
else ()
val fm = PropLogic.all fms
(* unit -> Thm.thm *)
- fun make_quick_and_dirty_thm () = (
- if !trace_sat then
- tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
- else ();
- (* of course just returning "False" is unsound; what we should return *)
- (* instead is "False" with all 'non_triv_clauses' as hyps -- but this *)
- (* might be rather slow, and it makes no real difference as long as *)
- (* 'rawsat_thm' is only called from 'rawsat_tac' *)
- SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const)
- )
+ fun make_quick_and_dirty_thm () =
+ let
+ val _ = if !trace_sat then
+ tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
+ else ()
+ val False_thm = SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const)
+ in
+ fold Thm.weaken clauses''' False_thm
+ end
in
- case SatSolver.invoke_solver (!solver) fm of
+ case (tracing "Invoking solver"; timeap (SatSolver.invoke_solver (!solver)) fm) of (*TODO*)
SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
if !trace_sat then
tracing ("Proof trace from SAT solver:\n" ^
@@ -312,35 +331,28 @@
make_quick_and_dirty_thm ()
else
let
- (* optimization: convert the given clauses from "[c_i] |- c_i" to *)
- (* "[c_1 && ... && c_n] |- c_i"; this avoids accumulation of *)
- (* hypotheses during resolution *)
+ (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i"; *)
+ (* this avoids accumulation of hypotheses during resolution *)
+ (* [c_1, ..., c_n] |- c_1 && ... && c_n *)
+ val _ = tracing "Conjunction.intr_list" (*TODO*)
+ val clauses_thm = timeap Conjunction.intr_list (map Thm.assume clauses''') (*TODO*)
(* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
- val cnf_cterm = Conjunction.mk_conjunction_list (map cprop_of non_triv_clauses)
+ val cnf_cterm = cprop_of clauses_thm
val cnf_thm = Thm.assume cnf_cterm
- (* cf. Conjunction.elim_list *)
- fun right_elim_list th =
- let val (th1, th2) = Conjunction.elim th
- in th1 :: right_elim_list th2 end handle THM _ => [th]
(* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
- val converted_clauses = right_elim_list cnf_thm
+ val _ = tracing "Conjunction.elim_list" (*TODO*)
+ val cnf_clauses = timeap Conjunction.elim_list cnf_thm (*TODO*)
(* initialize the clause array with the given clauses *)
val max_idx = valOf (Inttab.max_key clause_table)
val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
- val _ = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) converted_clauses 0
+ val _ = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) cnf_clauses 0
(* replay the proof to derive the empty clause *)
(* [c_1 && ... && c_n] |- False *)
- val FalseThm = replay_proof atom_table clause_arr (clause_table, empty_id)
+ val _ = tracing "replay_proof" (*TODO*)
+ val raw_thm = timeap (replay_proof atom_table clause_arr) (clause_table, empty_id) (*TODO*)
in
- (* convert the &&-hyp back to the original clauses format *)
- FalseThm
- (* [] |- c_1 && ... && c_n ==> False *)
- |> Thm.implies_intr cnf_cterm
- (* c_1 ==> ... ==> c_n ==> False *)
- |> Conjunction.curry ~1
(* [c_1, ..., c_n] |- False *)
- |> (fn thm => fold (fn cprem => fn thm' =>
- Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm)
+ Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
end)
| SatSolver.UNSATISFIABLE NONE =>
if !quick_and_dirty then (
@@ -377,7 +389,7 @@
(* int -> Tactical.tactic *)
-fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm prems) 1) i;
+fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
(* ------------------------------------------------------------------------- *)
(* pre_cnf_tac: converts the i-th subgoal *)
--- a/src/HOL/Tools/sat_solver.ML Thu Nov 09 16:14:43 2006 +0100
+++ b/src/HOL/Tools/sat_solver.ML Thu Nov 09 18:48:45 2006 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Tools/sat_solver.ML
ID: $Id$
Author: Tjark Weber
- Copyright 2004-2005
+ Copyright 2004-2006
Interface to external SAT solvers, and (simple) built-in SAT solvers.
*)
@@ -580,25 +580,60 @@
SatSolver.UNSATISFIABLE NONE =>
(let
(* string list *)
- val proof_lines = ((split_lines o File.read) proofpath)
+ val proof_lines = (split_lines o File.read) proofpath
handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
- (* a simple representation of the CNF formula as list of clauses (paired with their ID), *)
- (* where each clause is a sorted list of literals, where each literal is an int *)
- (* removes duplicates from an ordered list *)
- (* int list -> int list *)
- fun remove_dups [] = []
- | remove_dups [x] = [x]
- | remove_dups (x :: y :: xs) = if x = y then remove_dups (y :: xs) else x :: remove_dups (y :: xs)
+ (* representation of clauses as ordered lists of literals (with duplicates removed) *)
(* prop_formula -> int list *)
- fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) = clause_to_lit_list fm1 @ clause_to_lit_list fm2
- | clause_to_lit_list (PropLogic.BoolVar i) = [i]
- | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = [~i]
- | clause_to_lit_list _ = raise INVALID_PROOF "Error: invalid clause in CNF formula."
- (* prop_formula -> int list list *)
- fun cnf_to_clause_list (PropLogic.And (fm1, fm2)) = cnf_to_clause_list fm1 @ cnf_to_clause_list fm2
- | cnf_to_clause_list fm = [(remove_dups o sort int_ord o clause_to_lit_list) fm]
- (* (int list * int) list * int *)
- val (clauses, length_clauses) = fold_map (fn clause => fn n => ((clause, n), n+1)) (cnf_to_clause_list cnf) 0
+ fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
+ OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
+ | clause_to_lit_list (PropLogic.BoolVar i) =
+ [i]
+ | clause_to_lit_list (PropLogic.Not (PropLogic.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)) =
+ cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
+ | cnf_number_of_clauses _ =
+ 1
+ val number_of_clauses = cnf_number_of_clauses cnf
+ (* int list array *)
+ val clauses = Array.array (number_of_clauses, [])
+ (* initialize the 'clauses' array *)
+ (* prop_formula * int -> int *)
+ fun init_array (PropLogic.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)
+ val _ = init_array (cnf, 0)
+ (* optimization for the common case where MiniSat "R"s clauses in their *)
+ (* original order: *)
+ val last_ref_clause = ref (number_of_clauses - 1)
+ (* search the 'clauses' array for the given list of literals 'lits', *)
+ (* starting at index '!last_ref_clause + 1' *)
+ (* int list -> int option *)
+ fun original_clause_id lits =
+ let
+ fun original_clause_id_from index =
+ if index = number_of_clauses then
+ (* search from beginning again *)
+ original_clause_id_from 0
+ (* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
+ (* testing for equality should suffice -- barring duplicate literals *)
+ else if Array.sub (clauses, index) = lits then (
+ (* success *)
+ last_ref_clause := index;
+ SOME index
+ ) else if index = !last_ref_clause then
+ (* failure *)
+ NONE
+ else
+ (* continue search *)
+ original_clause_id_from (index + 1)
+ in
+ original_clause_id_from (!last_ref_clause + 1)
+ end
(* string -> int *)
fun int_from_string s = (
case Int.fromString s of
@@ -606,6 +641,8 @@
| NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
)
(* parse the proof file *)
+ val clause_table = ref (Inttab.empty : int list Inttab.table)
+ val empty_id = ref ~1
(* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
(* our proof format, where original clauses are numbered starting from 0 *)
val clause_id_map = ref (Inttab.empty : int Inttab.table)
@@ -614,30 +651,27 @@
SOME id' => id'
| NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.")
)
- val next_id = ref (length_clauses - 1)
- (* string list -> proof -> proof *)
- fun process_tokens [] proof =
- proof
- | process_tokens (tok::toks) (clause_table, empty_id) =
+ val next_id = ref (number_of_clauses - 1)
+ (* string list -> unit *)
+ fun process_tokens [] =
+ ()
+ | process_tokens (tok::toks) =
if tok="R" then (
case toks of
id::sep::lits =>
let
- val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
+ val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
val cid = int_from_string id
val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
val ls = sort int_ord (map int_from_string lits)
- val proof_id = (* both 'ls' and the list of literals used as key in 'clauses' are sorted, *)
- (* so testing for equality should suffice -- barring duplicate literals *)
- case AList.lookup (op =) clauses ls of
+ val proof_id = case original_clause_id ls of
SOME orig_id => orig_id
- | NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
+ | NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
+ in
(* extend the mapping of clause IDs with this newly defined ID *)
- val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
- handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
- in
+ clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
+ handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
(* the proof itself doesn't change *)
- (clause_table, empty_id)
end
| _ =>
raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
@@ -645,7 +679,7 @@
case toks of
id::sep::ids =>
let
- val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
+ val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
val cid = int_from_string id
val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
(* ignore the pivot literals in MiniSat's trace *)
@@ -659,7 +693,7 @@
handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
in
(* update clause table *)
- (Inttab.update_new (proof_id, rs) clause_table, empty_id)
+ clause_table := Inttab.update_new (proof_id, rs) (!clause_table)
handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
end
| _ =>
@@ -668,11 +702,11 @@
case toks of
[id] =>
let
- val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
+ val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
val _ = sat_to_proof (int_from_string id)
in
(* simply ignore "D" *)
- (clause_table, empty_id)
+ ()
end
| _ =>
raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
@@ -680,27 +714,29 @@
case toks of
[id1, id2] =>
let
- val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
+ val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
val _ = sat_to_proof (int_from_string id1)
val new_empty_id = sat_to_proof (int_from_string id2)
in
(* update conflict id *)
- (clause_table, new_empty_id)
+ empty_id := new_empty_id
end
| _ =>
raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
) else
raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
- (* string list -> proof -> proof *)
- fun process_lines [] proof =
- proof
- | process_lines (l::ls) proof =
- process_lines ls (process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l) proof)
+ (* string list -> unit *)
+ fun process_lines [] =
+ ()
+ | process_lines (l::ls) = (
+ process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
+ process_lines ls
+ )
(* proof *)
- val (clause_table, empty_id) = process_lines proof_lines (Inttab.empty, ~1)
- val _ = if empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
+ val _ = process_lines proof_lines
+ val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
in
- SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id))
+ SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
| result =>
result
@@ -856,7 +892,8 @@
process_lines ls
)
(* proof *)
- val _ = process_lines proof_lines
+ val _ = tracing "process_lines" (*TODO*)
+ val _ = timeap process_lines proof_lines (*TODO*)
val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
in
SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))