webertj@17618: (* Title: HOL/Tools/sat_funcs.ML webertj@17618: Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) wenzelm@29269: Author: Tjark Weber, TU Muenchen webertj@17618: webertj@17618: Proof reconstruction from SAT solvers. webertj@17618: webertj@17618: Description: webertj@17618: This file defines several tactics to invoke a proof-producing webertj@17618: SAT solver on a propositional goal in clausal form. webertj@17618: webertj@17618: We use a sequent presentation of clauses to speed up resolution webertj@17695: proof reconstruction. webertj@17695: We call such clauses "raw clauses", which are of the form webertj@20440: [x1, ..., xn, P] |- False webertj@19236: (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here), webertj@20440: where each xi is a literal (see also comments in cnf_funcs.ML). webertj@17618: webertj@19236: This does not work for goals containing schematic variables! webertj@19236: webertj@20039: The tactic produces a clause representation of the given goal webertj@20039: in DIMACS format and invokes a SAT solver, which should return webertj@20039: a proof consisting of a sequence of resolution steps, indicating webertj@20039: the two input clauses, and resulting in new clauses, leading to webertj@20039: the empty clause (i.e. "False"). The tactic replays this proof webertj@20039: in Isabelle and thus solves the overall goal. webertj@17618: webertj@20440: There are three SAT tactics available. They differ in the CNF transformation webertj@20039: used. "sat_tac" uses naive CNF transformation to transform the theorem to be webertj@20039: proved before giving it to the SAT solver. The naive transformation in the webertj@20440: worst case can lead to an exponential blow up in formula size. Another webertj@20039: tactic, "satx_tac", uses "definitional CNF transformation" which attempts to webertj@20039: produce a formula of linear size increase compared to the input formula, at webertj@20039: the cost of possibly introducing new variables. See cnf_funcs.ML for more webertj@20440: comments on the CNF transformation. "rawsat_tac" should be used with webertj@20440: caution: no CNF transformation is performed, and the tactic's behavior is webertj@20440: undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False, webertj@20440: where each Ci is a disjunction. webertj@17618: webertj@20039: The SAT solver to be used can be set via the "solver" reference. See webertj@20039: sat_solvers.ML for possible values, and etc/settings for required (solver- webertj@20039: dependent) configuration settings. To replay SAT proofs in Isabelle, you webertj@20039: must of course use a proof-producing SAT solver in the first place. webertj@20039: webertj@20039: Proofs are replayed only if "!quick_and_dirty" is false. If webertj@20039: "!quick_and_dirty" is true, the theorem (in case the SAT solver claims its webertj@20039: negation to be unsatisfiable) is proved via an oracle. webertj@17618: *) webertj@17618: webertj@17618: signature SAT = webertj@17618: sig wenzelm@41447: val trace_sat: bool Unsynchronized.ref (* input: print trace messages *) wenzelm@41447: val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *) wenzelm@41447: val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *) wenzelm@41447: val rawsat_thm: Proof.context -> cterm list -> thm wenzelm@41447: val rawsat_tac: Proof.context -> int -> tactic wenzelm@41447: val sat_tac: Proof.context -> int -> tactic wenzelm@41447: val satx_tac: Proof.context -> int -> tactic webertj@17618: end webertj@17618: wenzelm@32232: functor SATFunc(cnf : CNF) : SAT = webertj@17622: struct webertj@17618: wenzelm@32740: val trace_sat = Unsynchronized.ref false; webertj@17622: wenzelm@32740: val solver = Unsynchronized.ref "zchaff_with_proofs"; wenzelm@32740: (*see HOL/Tools/sat_solver.ML for possible values*) webertj@20039: wenzelm@32740: val counter = Unsynchronized.ref 0; webertj@17622: wenzelm@32010: val resolution_thm = wenzelm@32010: @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)} webertj@17622: wenzelm@32010: val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT)); webertj@20278: webertj@20278: (* ------------------------------------------------------------------------- *) webertj@21768: (* lit_ord: an order on integers that considers their absolute values only, *) webertj@21768: (* thereby treating integers that represent the same atom (positively *) webertj@21768: (* or negatively) as equal *) webertj@21768: (* ------------------------------------------------------------------------- *) webertj@21768: wenzelm@41447: fun lit_ord (i, j) = int_ord (abs i, abs j); webertj@21768: webertj@21768: (* ------------------------------------------------------------------------- *) webertj@20278: (* CLAUSE: during proof reconstruction, three kinds of clauses are *) webertj@20278: (* distinguished: *) webertj@20278: (* 1. NO_CLAUSE: clause not proved (yet) *) webertj@20278: (* 2. ORIG_CLAUSE: a clause as it occurs in the original problem *) webertj@20278: (* 3. RAW_CLAUSE: a raw clause, with additional precomputed information *) webertj@20278: (* (a mapping from int's to its literals) for faster proof *) webertj@20278: (* reconstruction *) webertj@20278: (* ------------------------------------------------------------------------- *) webertj@20278: wenzelm@41447: datatype CLAUSE = wenzelm@41447: NO_CLAUSE wenzelm@41447: | ORIG_CLAUSE of thm wenzelm@41447: | RAW_CLAUSE of thm * (int * cterm) list; webertj@20278: webertj@17622: (* ------------------------------------------------------------------------- *) webertj@17809: (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *) webertj@17809: (* resolution over the list (starting with its head), i.e. with two raw *) webertj@17809: (* clauses *) webertj@20440: (* [P, x1, ..., a, ..., xn] |- False *) webertj@17622: (* and *) webertj@20440: (* [Q, y1, ..., a', ..., ym] |- False *) webertj@19976: (* (where a and a' are dual to each other), we convert the first clause *) webertj@19976: (* to *) webertj@20440: (* [P, x1, ..., xn] |- a ==> False , *) webertj@19976: (* the second clause to *) webertj@20440: (* [Q, y1, ..., ym] |- a' ==> False *) webertj@19976: (* and then perform resolution with *) webertj@19976: (* [| ?P ==> False; ~?P ==> False |] ==> False *) webertj@19976: (* to produce *) webertj@20440: (* [P, Q, x1, ..., xn, y1, ..., ym] |- False *) webertj@21768: (* Each clause is accompanied with an association list mapping integers *) webertj@21768: (* (positive for positive literals, negative for negative literals, and *) webertj@21768: (* the same absolute value for dual literals) to the actual literals as *) webertj@21768: (* cterms. *) webertj@17622: (* ------------------------------------------------------------------------- *) webertj@17618: webertj@17809: fun resolve_raw_clauses [] = wenzelm@32091: raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, []) webertj@17809: | resolve_raw_clauses (c::cs) = wenzelm@41447: let wenzelm@41447: (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *) wenzelm@41447: fun merge xs [] = xs wenzelm@41447: | merge [] ys = ys wenzelm@41447: | merge (x :: xs) (y :: ys) = wenzelm@41447: (case (lit_ord o pairself fst) (x, y) of wenzelm@41447: LESS => x :: merge xs (y :: ys) wenzelm@41447: | EQUAL => x :: merge xs ys wenzelm@41447: | GREATER => y :: merge (x :: xs) ys) webertj@21768: wenzelm@41447: (* find out which two hyps are used in the resolution *) wenzelm@41447: fun find_res_hyps ([], _) _ = wenzelm@41447: raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) wenzelm@41447: | find_res_hyps (_, []) _ = wenzelm@41447: raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) wenzelm@41447: | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc = wenzelm@41447: (case (lit_ord o pairself fst) (h1, h2) of wenzelm@41447: LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc) wenzelm@41447: | EQUAL => wenzelm@41447: let wenzelm@41447: val (i1, chyp1) = h1 wenzelm@41447: val (i2, chyp2) = h2 wenzelm@41447: in wenzelm@41447: if i1 = ~ i2 then wenzelm@41447: (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2) wenzelm@41447: else (* i1 = i2 *) wenzelm@41447: find_res_hyps (hyps1, hyps2) (h1 :: acc) wenzelm@41447: end wenzelm@41447: | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc)) webertj@19976: wenzelm@41447: fun resolution (c1, hyps1) (c2, hyps2) = wenzelm@41447: let wenzelm@41447: val _ = wenzelm@44058: if ! trace_sat then (* FIXME !? *) wenzelm@41447: tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^ wenzelm@44058: " (hyps: " ^ ML_Syntax.print_list wenzelm@44058: (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1) wenzelm@41447: ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^ wenzelm@44058: " (hyps: " ^ ML_Syntax.print_list wenzelm@44058: (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")") wenzelm@41447: else () webertj@17809: wenzelm@41447: (* the two literals used for resolution *) wenzelm@41447: val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) [] webertj@19236: wenzelm@41447: val c1' = Thm.implies_intr hyp1 c1 (* Gamma1 |- hyp1 ==> False *) wenzelm@41447: val c2' = Thm.implies_intr hyp2 c2 (* Gamma2 |- hyp2 ==> False *) webertj@17618: wenzelm@41447: val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *) wenzelm@41447: let wenzelm@41447: val cLit = wenzelm@41447: snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *) wenzelm@41447: in wenzelm@41447: Thm.instantiate ([], [(cP, cLit)]) resolution_thm wenzelm@41447: end webertj@19236: wenzelm@41447: val _ = wenzelm@41447: if !trace_sat then wenzelm@41447: tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm) wenzelm@41447: else () webertj@19236: wenzelm@41447: (* Gamma1, Gamma2 |- False *) wenzelm@41447: val c_new = wenzelm@41447: Thm.implies_elim wenzelm@41447: (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1')) wenzelm@41447: (if hyp1_is_neg then c1' else c2') webertj@20278: wenzelm@41447: val _ = wenzelm@41447: if !trace_sat then wenzelm@41447: tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^ wenzelm@41447: " (hyps: " ^ ML_Syntax.print_list wenzelm@44058: (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")") wenzelm@41447: else () wenzelm@41447: val _ = Unsynchronized.inc counter wenzelm@41447: in wenzelm@41447: (c_new, new_hyps) wenzelm@41447: end wenzelm@41447: in wenzelm@41447: fold resolution cs c wenzelm@41447: end; webertj@17618: webertj@17622: (* ------------------------------------------------------------------------- *) webertj@17809: (* replay_proof: replays the resolution proof returned by the SAT solver; *) webertj@17809: (* cf. SatSolver.proof for details of the proof format. Updates the *) webertj@17809: (* 'clauses' array with derived clauses, and returns the derived clause *) webertj@17809: (* at index 'empty_id' (which should just be "False" if proof *) webertj@17809: (* reconstruction was successful, with the used clauses as hyps). *) webertj@20278: (* 'atom_table' must contain an injective mapping from all atoms that *) webertj@20278: (* occur (as part of a literal) in 'clauses' to positive integers. *) webertj@17622: (* ------------------------------------------------------------------------- *) webertj@17622: webertj@20278: fun replay_proof atom_table clauses (clause_table, empty_id) = wenzelm@41447: let wenzelm@41447: fun index_of_literal chyp = wenzelm@41447: (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of wenzelm@41447: (Const (@{const_name Not}, _) $ atom) => wenzelm@41447: SOME (~ (the (Termtab.lookup atom_table atom))) wenzelm@41447: | atom => SOME (the (Termtab.lookup atom_table atom))) wenzelm@41447: handle TERM _ => NONE; (* 'chyp' is not a literal *) webertj@20278: wenzelm@41447: fun prove_clause id = wenzelm@41447: (case Array.sub (clauses, id) of wenzelm@41447: RAW_CLAUSE clause => clause wenzelm@41447: | ORIG_CLAUSE thm => wenzelm@41447: (* convert the original clause *) wenzelm@41447: let wenzelm@41447: val _ = wenzelm@41447: if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else () wenzelm@41447: val raw = cnf.clause2raw_thm thm wenzelm@41447: val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp => wenzelm@41447: Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw))) wenzelm@41447: val clause = (raw, hyps) wenzelm@41447: val _ = Array.update (clauses, id, RAW_CLAUSE clause) wenzelm@41447: in wenzelm@41447: clause wenzelm@41447: end wenzelm@41447: | NO_CLAUSE => wenzelm@41447: (* prove the clause, using information from 'clause_table' *) wenzelm@41447: let wenzelm@41447: val _ = wenzelm@41447: if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else () wenzelm@41447: val ids = the (Inttab.lookup clause_table id) wenzelm@41447: val clause = resolve_raw_clauses (map prove_clause ids) wenzelm@41447: val _ = Array.update (clauses, id, RAW_CLAUSE clause) wenzelm@41447: val _ = wenzelm@41447: if !trace_sat then wenzelm@41447: tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) wenzelm@41447: else () wenzelm@41447: in wenzelm@41447: clause wenzelm@41447: end) webertj@17618: wenzelm@41447: val _ = counter := 0 wenzelm@41447: val empty_clause = fst (prove_clause empty_id) wenzelm@41447: val _ = wenzelm@41447: if !trace_sat then wenzelm@41447: tracing ("Proof reconstruction successful; " ^ wenzelm@41447: string_of_int (!counter) ^ " resolution step(s) total.") wenzelm@41447: else () wenzelm@41447: in wenzelm@41447: empty_clause wenzelm@41447: end; webertj@17622: webertj@20278: (* ------------------------------------------------------------------------- *) webertj@20278: (* string_of_prop_formula: return a human-readable string representation of *) webertj@20278: (* a 'prop_formula' (just for tracing) *) webertj@20278: (* ------------------------------------------------------------------------- *) webertj@20278: wenzelm@41471: fun string_of_prop_formula Prop_Logic.True = "True" wenzelm@41471: | string_of_prop_formula Prop_Logic.False = "False" wenzelm@41471: | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i wenzelm@41471: | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm wenzelm@41471: | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) = wenzelm@41447: "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")" wenzelm@41471: | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) = wenzelm@41447: "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")"; webertj@17622: webertj@17622: (* ------------------------------------------------------------------------- *) webertj@21267: (* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) webertj@21267: (* a proof from the resulting proof trace of the SAT solver. The *) webertj@21267: (* theorem returned is just "False" (with some of the given clauses as *) webertj@21267: (* hyps). *) webertj@21267: (* ------------------------------------------------------------------------- *) webertj@21267: wenzelm@32432: fun rawsat_thm ctxt clauses = wenzelm@41447: let wenzelm@41447: (* remove premises that equal "True" *) wenzelm@41447: val clauses' = filter (fn clause => wenzelm@41447: (not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause wenzelm@41447: handle TERM ("dest_Trueprop", _) => true) clauses wenzelm@41447: (* remove non-clausal premises -- of course this shouldn't actually *) wenzelm@41447: (* remove anything as long as 'rawsat_tac' is only called after the *) wenzelm@41447: (* premises have been converted to clauses *) wenzelm@41447: val clauses'' = filter (fn clause => wenzelm@41447: ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause wenzelm@41447: handle TERM ("dest_Trueprop", _) => false) wenzelm@41447: orelse ( wenzelm@41447: warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause)); wenzelm@41447: false)) clauses' wenzelm@41447: (* remove trivial clauses -- this is necessary because zChaff removes *) wenzelm@41447: (* trivial clauses during preprocessing, and otherwise our clause *) wenzelm@41447: (* numbering would be off *) wenzelm@41447: val nontrivial_clauses = wenzelm@41447: filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses'' wenzelm@41447: (* sort clauses according to the term order -- an optimization, *) wenzelm@41447: (* useful because forming the union of hypotheses, as done by *) wenzelm@41447: (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *) wenzelm@41447: (* terms sorted in descending order, while only linear for terms *) wenzelm@41447: (* sorted in ascending order *) wenzelm@41447: val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses wenzelm@41447: val _ = wenzelm@41447: if !trace_sat then wenzelm@41447: tracing ("Sorted non-trivial clauses:\n" ^ wenzelm@41447: cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) wenzelm@41447: else () wenzelm@41471: (* translate clauses from HOL terms to Prop_Logic.prop_formula *) wenzelm@41447: val (fms, atom_table) = wenzelm@41471: fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) wenzelm@41447: sorted_clauses Termtab.empty wenzelm@41447: val _ = wenzelm@41447: if !trace_sat then wenzelm@41447: tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) wenzelm@41447: else () wenzelm@41471: val fm = Prop_Logic.all fms wenzelm@41447: (* unit -> Thm.thm *) wenzelm@41447: fun make_quick_and_dirty_thm () = wenzelm@41447: let wenzelm@41447: val _ = wenzelm@41447: if !trace_sat then wenzelm@41447: tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead." wenzelm@41447: else () wenzelm@41447: val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const) wenzelm@41447: in wenzelm@41447: (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *) wenzelm@41447: (* Thm.weaken sorted_clauses' would be quadratic, since we sorted *) wenzelm@41447: (* clauses in ascending order (which is linear for *) wenzelm@41447: (* 'Conjunction.intr_balanced', used below) *) wenzelm@41447: fold Thm.weaken (rev sorted_clauses) False_thm wenzelm@41447: end wenzelm@41447: in wenzelm@41447: case wenzelm@41447: let val the_solver = ! solver wenzelm@41447: in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end wenzelm@41447: of wenzelm@41447: SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => wenzelm@41447: (if !trace_sat then wenzelm@41447: tracing ("Proof trace from SAT solver:\n" ^ wenzelm@41447: "clauses: " ^ ML_Syntax.print_list wenzelm@41491: (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int)) wenzelm@41447: (Inttab.dest clause_table) ^ "\n" ^ wenzelm@41491: "empty clause: " ^ string_of_int empty_id) wenzelm@41447: else (); wenzelm@41447: if !quick_and_dirty then wenzelm@41447: make_quick_and_dirty_thm () wenzelm@41447: else wenzelm@41447: let wenzelm@41447: (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i"; *) wenzelm@41447: (* this avoids accumulation of hypotheses during resolution *) wenzelm@41447: (* [c_1, ..., c_n] |- c_1 && ... && c_n *) wenzelm@41447: val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses) wenzelm@41447: (* [c_1 && ... && c_n] |- c_1 && ... && c_n *) wenzelm@41447: val cnf_cterm = cprop_of clauses_thm wenzelm@41447: val cnf_thm = Thm.assume cnf_cterm wenzelm@41447: (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *) wenzelm@41447: val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm wenzelm@41447: (* initialize the clause array with the given clauses *) wenzelm@41447: val max_idx = the (Inttab.max_key clause_table) wenzelm@41447: val clause_arr = Array.array (max_idx + 1, NO_CLAUSE) wenzelm@41447: val _ = wenzelm@41447: fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) wenzelm@41447: cnf_clauses 0 wenzelm@41447: (* replay the proof to derive the empty clause *) wenzelm@41447: (* [c_1 && ... && c_n] |- False *) wenzelm@41447: val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id) wenzelm@41447: in wenzelm@41447: (* [c_1, ..., c_n] |- False *) wenzelm@41447: Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm wenzelm@41447: end) wenzelm@41447: | SatSolver.UNSATISFIABLE NONE => wenzelm@41447: if !quick_and_dirty then wenzelm@41447: (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"; wenzelm@41447: make_quick_and_dirty_thm ()) wenzelm@41447: else wenzelm@41447: raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, []) wenzelm@41447: | SatSolver.SATISFIABLE assignment => wenzelm@41447: let wenzelm@41447: val msg = wenzelm@41447: "SAT solver found a countermodel:\n" ^ wenzelm@41447: (commas o map (fn (term, idx) => wenzelm@41447: Syntax.string_of_term_global @{theory} term ^ ": " ^ wenzelm@41447: (case assignment idx of NONE => "arbitrary" wenzelm@41447: | SOME true => "true" | SOME false => "false"))) wenzelm@41447: (Termtab.dest atom_table) wenzelm@41447: in wenzelm@41447: raise THM (msg, 0, []) wenzelm@41447: end wenzelm@41447: | SatSolver.UNKNOWN => wenzelm@41447: raise THM ("SAT solver failed to decide the formula", 0, []) wenzelm@41447: end; webertj@17618: webertj@17622: (* ------------------------------------------------------------------------- *) webertj@17622: (* Tactics *) webertj@17622: (* ------------------------------------------------------------------------- *) webertj@17618: webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17809: (* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal *) webertj@17809: (* should be of the form *) webertj@17809: (* [| c1; c2; ...; ck |] ==> False *) webertj@17809: (* where each cj is a non-empty clause (i.e. a disjunction of literals) *) webertj@17809: (* or "True" *) webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17809: wenzelm@32232: fun rawsat_tac ctxt i = wenzelm@32432: Subgoal.FOCUS (fn {context = ctxt', prems, ...} => wenzelm@32432: rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i; webertj@17618: webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17809: (* pre_cnf_tac: converts the i-th subgoal *) webertj@17809: (* [| A1 ; ... ; An |] ==> B *) webertj@17809: (* to *) webertj@17809: (* [| A1; ... ; An ; ~B |] ==> False *) webertj@17809: (* (handling meta-logical connectives in B properly before negating), *) webertj@17809: (* then replaces meta-logical connectives in the premises (i.e. "==>", *) webertj@17809: (* "!!" and "==") by connectives of the HOL object-logic (i.e. by *) webertj@19553: (* "-->", "!", and "="), then performs beta-eta-normalization on the *) webertj@19553: (* subgoal *) webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17809: wenzelm@23533: val pre_cnf_tac = wenzelm@41447: rtac ccontr THEN' wenzelm@41447: Object_Logic.atomize_prems_tac THEN' wenzelm@41447: CONVERSION Drule.beta_eta_conversion; webertj@17809: webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17809: (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *) webertj@17809: (* if not, eliminates conjunctions (i.e. each clause of the CNF formula *) webertj@17809: (* becomes a separate premise), then applies 'rawsat_tac' to solve the *) webertj@17809: (* subgoal *) webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17697: wenzelm@32232: fun cnfsat_tac ctxt i = wenzelm@41447: (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i); webertj@17618: webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17809: (* cnfxsat_tac: checks if the empty clause "False" occurs among the *) webertj@17809: (* premises; if not, eliminates conjunctions (i.e. each clause of the *) webertj@17809: (* CNF formula becomes a separate premise) and existential quantifiers, *) webertj@17809: (* then applies 'rawsat_tac' to solve the subgoal *) webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17809: wenzelm@32232: fun cnfxsat_tac ctxt i = wenzelm@41447: (etac FalseE i) ORELSE wenzelm@41447: (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i); webertj@17618: webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17809: (* sat_tac: tactic for calling an external SAT solver, taking as input an *) webertj@17809: (* arbitrary formula. The input is translated to CNF, possibly causing *) webertj@17809: (* an exponential blowup. *) webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17809: wenzelm@32232: fun sat_tac ctxt i = wenzelm@41447: pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i; webertj@17809: webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17809: (* satx_tac: tactic for calling an external SAT solver, taking as input an *) webertj@17809: (* arbitrary formula. The input is translated to CNF, possibly *) webertj@17809: (* introducing new literals. *) webertj@17809: (* ------------------------------------------------------------------------- *) webertj@17809: wenzelm@32232: fun satx_tac ctxt i = wenzelm@41447: pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i; webertj@17618: wenzelm@23533: end;