# HG changeset patch # User webertj # Date 1163094525 -3600 # Node ID 5294ecae6708300bda874f0183c24833249e8ca5 # Parent 288a504c24d644589592bcfa0d0f7598041658e9 interpreters for fst and snd added diff -r 288a504c24d6 -r 5294ecae6708 src/HOL/Tools/refute.ML --- 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; diff -r 288a504c24d6 -r 5294ecae6708 src/HOL/Tools/sat_funcs.ML --- 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 *) diff -r 288a504c24d6 -r 5294ecae6708 src/HOL/Tools/sat_solver.ML --- 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))