# HG changeset patch # User webertj # Date 1127539306 -7200 # Node ID 5d03a69481b6fcd7f9c76a58459bac9255ee088e # Parent afffade1697e673757e3c4a71d4b85917013e218 code reformatted and restructured, many minor modifications diff -r afffade1697e -r 5d03a69481b6 src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Sat Sep 24 07:10:57 2005 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Sat Sep 24 07:21:46 2005 +0200 @@ -1,6 +1,7 @@ (* Title: HOL/Tools/sat_funcs.ML ID: $Id$ Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) + Author: Tjark Weber Copyright 2005 @@ -39,7 +40,6 @@ This transformation introduces new variables. See also cnf_funcs.ML for more comments. - Notes for the current revision: - The current version supports only zChaff prover. - The environment variable ZCHAFF_HOME must be set to point to @@ -47,282 +47,245 @@ - The environment variable ZCHAFF_VERSION must be set according to the version of zChaff used. Current supported version of zChaff: zChaff version 2004.11.15 - *) -(***************************************************************************) -(** Array of clauses **) - -signature CLAUSEARR = -sig - val init : int -> unit - val register_at : int -> Thm.thm -> unit - val register_list : Thm.thm list -> unit - val getClause : int -> Thm.thm option -end - -structure ClauseArr : CLAUSEARR = -struct - -val clauses : ((Thm.thm option) array) ref = ref (Array.array(1, NONE)); - -fun init size = (clauses := Array.array(size, NONE)) - -fun register_at i c = Array.update (!clauses, i, (SOME c)) - -fun reg_list n nil = () - | reg_list n (x::l) = - (register_at n x; reg_list (n+1) l) - -fun register_list l = reg_list 0 l - -fun getClause i = Array.sub (!clauses, i) - -end - - -(***************************************************************************) - signature SAT = sig - val trace_sat : bool ref (* trace tactic *) - val sat_tac : Tactical.tactic - val satx_tac : Tactical.tactic -end - -functor SATFunc (structure cnf_struct : CNF) : SAT = -struct - -structure cnf = cnf_struct - -val trace_sat = ref false; (* debugging flag *) - - -(* Look up the Isabelle atom corresponding to a DIMACS index in the - reverse dictionary. This entry should exist, otherwise an error - is raised. -*) -fun rev_lookup idx dictionary = -let - fun rev_assoc [] = NONE - | rev_assoc ((key, entry)::list) = - if entry = idx then SOME key else rev_assoc list -in - the (rev_assoc dictionary) -end; - - -(* Convert rules of the form - l1 ==> l2 ==> .. ==> li ==> .. ==> False - to - l1 ==> l2 ==> .... ==> ~li -*) -fun swap_prem rslv c = -let - val thm1 = rule_by_tactic (metacut_tac c 1 THEN - (atac 1) THEN (REPEAT_SOME atac)) rslv -in - rule_by_tactic (ALLGOALS (cnf.weakening_tac)) thm1 -end - -(*** Proof reconstruction: given two clauses - [| x1 ; .. ; a ; .. ; xn |] ==> False - and - [| y1 ; .. ; ~a ; .. ; ym |] ==> False , - - we firt convert the first clause into - - [| x1 ; ... ; xn |] ==> ~a (using swap_prem) - - and do a resolution with the second clause to produce - [| y1 ; ... ; x1 ; ... ; xn ; ... ; yn |] ==> False - -***) - -fun dual (Const("Trueprop",_) $ x) (Const("Trueprop",_) $ y) = dual x y - | dual (Const("Not",_) $ x) y = (x = y) - | dual x (Const("Not",_) $ y) = (x = y) - | dual x y = false - -(* Check if an atom has a dual in a list of atoms *) - -fun dual_mem x nil = false - | dual_mem x (y::l) = if (dual x y) then true else dual_mem x l - - -fun replay_chain sg idx (c::cs) = -let - val (SOME fc) = ClauseArr.getClause c; - - fun strip_neg (Const("Trueprop", _) $ x) = strip_neg x - | strip_neg (Const("Not",_) $ x) = x - | strip_neg x = x - - (* Find out which atom (literal) is used in the resolution *) - fun res_atom nil l = raise THM ("Proof reconstruction failed!", 0, []) - | res_atom (x::l1) l2 = - if (dual_mem x l2) then strip_neg x - else res_atom l1 l2 - - fun replay old [] = old - | replay old (cls :: clss) = - let - val (SOME icls) = ClauseArr.getClause cls; - val var = res_atom (prems_of old) (prems_of icls); - val atom = cterm_of sg var; - val rslv = instantiate' [] [SOME atom] notI; - - val _ = if (!trace_sat) then - ( - writeln "-- resolving clause:"; - print_thm old; - writeln "-- with clause: "; - print_thm icls; - writeln "-- using "; - writeln (string_of_cterm atom) - ) else (); - - val thm1 = ( - rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv old))) icls - handle THM _ => - rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv icls))) old ); - - val new = rule_by_tactic distinct_subgoals_tac thm1; - val _ = if (!trace_sat) then (writeln "-- resulting clause:"; print_thm new) - else () - in - replay new clss - end -in - ClauseArr.register_at idx (replay fc cs); - if (!trace_sat) then ( - writeln ("-- Replay chain successful. " ^ - "The resulting clause stored at #" ^ (Int.toString idx)) - ) else () + val trace_sat : bool ref (* print trace messages *) + val sat_tac : Tactical.tactic + val satx_tac : Tactical.tactic end +functor SATFunc (structure cnf : CNF) : SAT = +struct -(* Replay the resolution proof from file prf_file with hypotheses hyps. - Returns the theorem established by the proof (which is just False). -*) -fun replay_prf sg tab size = - let - val prf = Inttab.dest tab; +val trace_sat = ref false; + +val counter = ref 0; + +(* ------------------------------------------------------------------------- *) +(* rev_lookup: look up the Isabelle/HOL atom corresponding to a DIMACS *) +(* variable index in the dictionary. This index should exist in the *) +(* dictionary, otherwise exception Option is raised. *) +(* ------------------------------------------------------------------------- *) + +(* 'b -> ('a * 'b) list -> 'a *) + +fun rev_lookup idx [] = raise Option + | rev_lookup idx ((key, entry)::dict) = if entry=idx then key else rev_lookup idx dict; - fun complete nil = true - | complete (x::l) = ( - case ClauseArr.getClause x of - NONE => false - | (SOME _) => complete l) +(* ------------------------------------------------------------------------- *) +(* swap_prem: convert rules of the form *) +(* l1 ==> l2 ==> .. ==> li ==> .. ==> False *) +(* to *) +(* l1 ==> l2 ==> .... ==> ~li *) +(* ------------------------------------------------------------------------- *) + +fun swap_prem rslv c = +let + val thm1 = rule_by_tactic (metacut_tac c 1 THEN (atac 1) THEN (REPEAT_SOME atac)) rslv +in + rule_by_tactic (ALLGOALS (cnf.weakening_tac)) thm1 +end; + +(* ------------------------------------------------------------------------- *) +(* is_dual: check if two atoms are dual to each other *) +(* ------------------------------------------------------------------------- *) + +(* Term.term -> Term.term -> bool *) - fun do_chains [] = () - | do_chains (pr :: rs) = - let val (idx, cls) = pr - in - if (complete cls) then - (replay_chain sg idx cls; do_chains rs) - else do_chains (rs @ [pr]) - end - in - if (!trace_sat) then ( - writeln "Proof trace from SAT solver: "; - print prf ; () - ) else () ; - do_chains prf; - ClauseArr.getClause size - end; +fun is_dual (Const ("Trueprop", _) $ x) y = is_dual x y + | is_dual x (Const ("Trueprop", _) $ y) = is_dual x y + | is_dual (Const ("Not", _) $ x) y = (x = y) + | is_dual x (Const ("Not", _) $ y) = (x = y) + | is_dual x y = false; + +(* ------------------------------------------------------------------------- *) +(* dual_mem: check if an atom has a dual in a list of atoms *) +(* ------------------------------------------------------------------------- *) + +(* Term.term -> Term.term list -> bool *) + +fun dual_mem x [] = false + | dual_mem x (y::ys) = is_dual x y orelse dual_mem x ys; +(* ------------------------------------------------------------------------- *) +(* replay_chain: proof reconstruction: given two clauses *) +(* [| x1 ; .. ; a ; .. ; xn |] ==> False *) +(* and *) +(* [| y1 ; .. ; ~a ; .. ; ym |] ==> False , *) +(* we first convert the first clause into *) +(* [| x1 ; ... ; xn |] ==> ~a (using swap_prem) *) +(* and do a resolution with the second clause to produce *) +(* [| y1 ; ... ; x1 ; ... ; xn ; ... ; yn |] ==> False *) +(* ------------------------------------------------------------------------- *) -(***************************************************************************) -(*** Functions to build the sat tactic ***) +(* Theory.theory -> Thm.thm option Array.array -> int -> int list -> unit *) + +fun replay_chain sg clauses idx (c::cs) = +let + val (SOME fc) = Array.sub (clauses, c) + + fun strip_neg (Const ("Trueprop", _) $ x) = strip_neg x + | strip_neg (Const ("Not", _) $ x) = x + | strip_neg x = x + + (* find out which atom (literal) is used in the resolution *) + fun res_atom [] _ = raise THM ("Proof reconstruction failed!", 0, []) + | res_atom (x::xs) ys = if dual_mem x ys then strip_neg x else res_atom xs ys -(* A trivial tactic, used in preprocessing before calling the main - tactic *) - -val pre_sat_tac = (REPEAT (etac conjE 1)) THEN - (REPEAT ((atac 1) ORELSE (etac FalseE 1))) + fun replay old [] = + old + | replay old (cl::cls) = + let + val icl = (valOf o Array.sub) (clauses, cl) + val var = res_atom (prems_of old) (prems_of icl) + val atom = cterm_of sg var + val rslv = instantiate' [] [SOME atom] notI + val _ = if !trace_sat then + tracing ("Resolving clause: " ^ string_of_thm old ^ + "\nwith clause: " ^ string_of_thm icl ^ + "\nusing literal " ^ string_of_cterm atom ^ ".") + else () + val thm1 = (rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv old))) icl + handle THM _ => rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv icl))) old) + val new = rule_by_tactic distinct_subgoals_tac thm1 + val _ = if !trace_sat then tracing ("Resulting clause: " ^ string_of_thm new) else () + val _ = inc counter + in + replay new cls + end -fun collect_atoms (Const("Trueprop",_) $ x) l = collect_atoms x l - | collect_atoms (Const("op |", _) $ x $ y) l = - collect_atoms x (collect_atoms y l) - | collect_atoms x l = if (x mem l) then l else (x::l) + val _ = Array.update (clauses, idx, SOME (replay fc cs)) -fun has_duals nil = false - | has_duals (x::l) = if (dual_mem x l) then true else has_duals l + val _ = if !trace_sat then + tracing ("Replay chain successful; clause stored at #" ^ string_of_int idx) + else () +in + () +end; -fun trivial_clause (Const("True",_)) = true - | trivial_clause c = has_duals (collect_atoms c nil) +(* ------------------------------------------------------------------------- *) +(* replay_proof: replay the resolution proof returned by the SAT solver; cf. *) +(* SatSolver.proof for details of the proof format. Returns the *) +(* theorem established by the proof (which is just False). *) +(* ------------------------------------------------------------------------- *) + +(* Theory.theory -> Thm.thm option Array.array -> SatSolver.proof -> Thm.thm *) -(* Remove trivial clauses *) -fun filter_clauses nil = nil - | filter_clauses (x::l) = - if (trivial_clause (term_of (cprop_of x))) then filter_clauses l - else (x:: filter_clauses l) +fun replay_proof sg clauses (clause_table, empty_id) = +let + fun complete [] = + true + | complete (x::xs) = + (isSome o Array.sub) (clauses, x) andalso complete xs -fun is_true assignment x = - case (assignment x) of - NONE => false - | SOME b => b + fun do_chains [] = + () + | do_chains (ch::chs) = + let + val (idx, cls) = ch + in + if complete cls then ( + replay_chain sg clauses idx cls; + do_chains chs + ) else + do_chains (chs @ [ch]) + end + + val _ = do_chains (Inttab.dest clause_table) -fun get_model dict assignment = - map (fn (x,y) => x) (List.filter (fn (x,y) => is_true assignment y) dict) + val _ = if !trace_sat then + tracing (string_of_int (!counter) ^ " resolution steps total.") + else () +in + (valOf o Array.sub) (clauses, empty_id) +end; + +(* ------------------------------------------------------------------------- *) +(* Functions to build the sat tactic *) +(* ------------------------------------------------------------------------- *) + +(* A trivial tactic, used in preprocessing before calling the main tactic *) +val pre_sat_tac = (REPEAT (etac conjE 1)) THEN (REPEAT ((atac 1) ORELSE (etac FalseE 1))); -fun string_of_model sg nil = "" - | string_of_model sg [x] = Sign.string_of_term sg x - | string_of_model sg (x::l) = (Sign.string_of_term sg x) ^ ", " ^ (string_of_model sg l) +fun collect_atoms (Const ("Trueprop", _) $ x) ls = collect_atoms x ls + | collect_atoms (Const ("op |", _) $ x $ y) ls = collect_atoms x (collect_atoms y ls) + | collect_atoms x ls = x ins ls; + +fun has_duals [] = false + | has_duals (x::xs) = dual_mem x xs orelse has_duals xs; -(* Run external SAT solver with the given clauses. Reconstruct a proof from - the resulting proof trace of the SAT solver. -*) +fun is_trivial_clause (Const ("True", _)) = true + | is_trivial_clause c = has_duals (collect_atoms c []); + +(* ------------------------------------------------------------------------- *) +(* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) +(* a proof from the resulting proof trace of the SAT solver. *) +(* ------------------------------------------------------------------------- *) fun rawsat_thm sg prems = -let val thms = filter_clauses prems - val (fm, dict) = cnf.cnf2prop thms - val raw_thms = cnf.cnf2raw_thms thms +let + val thms = filter (not o is_trivial_clause o term_of o cprop_of) prems (* remove trivial clauses *) + val (fm, dict) = cnf.cnf2prop thms + val _ = if !trace_sat then tracing "Invoking SAT solver ..." else () in - let - val result = SatSolver.invoke_solver "zchaff_with_proofs" fm; - in - case result of - (SatSolver.UNSATISFIABLE (SOME (table, size))) => - let val _ = ClauseArr.init (size + 1); - val _ = ClauseArr.register_list - (map (fn x => (rule_by_tactic distinct_subgoals_tac x)) raw_thms); - val (SOME thm1) = replay_prf sg table size - in - thm1 - end - | (SatSolver.SATISFIABLE model) => - let val msg = "\nSAT solver found a countermodel:\n{ " ^ - (string_of_model sg (get_model dict model)) ^ " }\n" - in - raise THM (msg, 0, []) - end - | _ => raise THM ("SAT solver failed!\n", 0, []) + case SatSolver.invoke_solver "zchaff_with_proofs" fm of + SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => + let + val _ = if !trace_sat then + tracing ("Proof trace from SAT solver:\n" ^ + "clauses: [" ^ commas (map (fn (c, cs) => + "(" ^ string_of_int c ^ ", [" ^ commas (map string_of_int cs) ^ "])") (Inttab.dest clause_table)) ^ "]\n" ^ + "empty clause: " ^ string_of_int empty_id) + else () + val raw_thms = cnf.cnf2raw_thms thms + val raw_thms' = map (rule_by_tactic distinct_subgoals_tac) raw_thms + (* initialize the clause array with the original clauses *) + val max_idx = valOf (Inttab.max_key clause_table) + val clauses = Array.array (max_idx + 1, NONE) + val _ = fold (fn thm => fn idx => (Array.update (clauses, idx, SOME thm); idx+1)) raw_thms' 0 + in + replay_proof sg clauses (clause_table, empty_id) + end + | SatSolver.UNSATISFIABLE NONE => + raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, []) + | SatSolver.SATISFIABLE assignment => + let + val msg = "SAT solver found a countermodel:\n" + ^ (enclose "{" "}" + o commas + o map (Sign.string_of_term sg o fst) + o filter (fn (_, idx) => getOpt (assignment idx, false))) dict + in + raise THM (msg, 0, []) + end + | SatSolver.UNKNOWN => + raise THM ("SAT solver failed to decide the formula", 0, []) +end; - end -end +(* ------------------------------------------------------------------------- *) +(* Tactics *) +(* ------------------------------------------------------------------------- *) -fun cnfsat_basic_tac state = -let val sg = Thm.sign_of_thm state -in - METAHYPS (fn prems => rtac (rawsat_thm sg prems) 1) 1 state -end +fun cnfsat_basic_tac state = +let + val sg = Thm.sign_of_thm state +in + METAHYPS (fn prems => rtac (rawsat_thm sg prems) 1) 1 state +end; (* Tactic for calling external SAT solver, taking as input CNF clauses *) -val cnfsat_tac = pre_sat_tac THEN (IF_UNSOLVED cnfsat_basic_tac) - +val cnfsat_tac = pre_sat_tac THEN (IF_UNSOLVED cnfsat_basic_tac); -(* - Tactic for calling external SAT solver, taking as input arbitrary formula. -*) +(* Tactic for calling external SAT solver, taking as input arbitrary formula *) val sat_tac = cnf.cnf_thin_tac THEN cnfsat_tac; -(* - Tactic for calling external SAT solver, taking as input arbitratry formula. +(* + Tactic for calling external SAT solver, taking as input arbitrary formula. The input is translated to CNF (in primitive form), possibly introducing - new literals. + new literals. *) val satx_tac = cnf.cnfx_thin_tac THEN cnfsat_tac; -end (*of structure*) +end; (* of structure *) diff -r afffade1697e -r 5d03a69481b6 src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Sat Sep 24 07:10:57 2005 +0200 +++ b/src/HOL/ex/SAT_Examples.thy Sat Sep 24 07:21:46 2005 +0200 @@ -4,12 +4,14 @@ Copyright 2005 *) -header {* Examples for the 'sat' command *} +header {* Examples for the 'sat' and 'satx' tactic *} theory SAT_Examples imports Main begin +ML {* set sat.trace_sat; *} + (* Translated from TPTP problem library: PUZ015-2.006.dimacs *) lemma assumes 1: "~x0"