1 (* Title: HOL/Tools/sat_funcs.ML |
|
2 Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) |
|
3 Author: Tjark Weber, TU Muenchen |
|
4 |
|
5 Proof reconstruction from SAT solvers. |
|
6 |
|
7 Description: |
|
8 This file defines several tactics to invoke a proof-producing |
|
9 SAT solver on a propositional goal in clausal form. |
|
10 |
|
11 We use a sequent presentation of clauses to speed up resolution |
|
12 proof reconstruction. |
|
13 We call such clauses "raw clauses", which are of the form |
|
14 [x1, ..., xn, P] |- False |
|
15 (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here), |
|
16 where each xi is a literal (see also comments in cnf_funcs.ML). |
|
17 |
|
18 This does not work for goals containing schematic variables! |
|
19 |
|
20 The tactic produces a clause representation of the given goal |
|
21 in DIMACS format and invokes a SAT solver, which should return |
|
22 a proof consisting of a sequence of resolution steps, indicating |
|
23 the two input clauses, and resulting in new clauses, leading to |
|
24 the empty clause (i.e. "False"). The tactic replays this proof |
|
25 in Isabelle and thus solves the overall goal. |
|
26 |
|
27 There are three SAT tactics available. They differ in the CNF transformation |
|
28 used. "sat_tac" uses naive CNF transformation to transform the theorem to be |
|
29 proved before giving it to the SAT solver. The naive transformation in the |
|
30 worst case can lead to an exponential blow up in formula size. Another |
|
31 tactic, "satx_tac", uses "definitional CNF transformation" which attempts to |
|
32 produce a formula of linear size increase compared to the input formula, at |
|
33 the cost of possibly introducing new variables. See cnf_funcs.ML for more |
|
34 comments on the CNF transformation. "rawsat_tac" should be used with |
|
35 caution: no CNF transformation is performed, and the tactic's behavior is |
|
36 undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False, |
|
37 where each Ci is a disjunction. |
|
38 |
|
39 The SAT solver to be used can be set via the "solver" reference. See |
|
40 sat_solvers.ML for possible values, and etc/settings for required (solver- |
|
41 dependent) configuration settings. To replay SAT proofs in Isabelle, you |
|
42 must of course use a proof-producing SAT solver in the first place. |
|
43 |
|
44 Proofs are replayed only if "quick_and_dirty" is false. If |
|
45 "quick_and_dirty" is true, the theorem (in case the SAT solver claims its |
|
46 negation to be unsatisfiable) is proved via an oracle. |
|
47 *) |
|
48 |
|
49 signature SAT = |
|
50 sig |
|
51 val trace_sat: bool Unsynchronized.ref (* input: print trace messages *) |
|
52 val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *) |
|
53 val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *) |
|
54 val rawsat_thm: Proof.context -> cterm list -> thm |
|
55 val rawsat_tac: Proof.context -> int -> tactic |
|
56 val sat_tac: Proof.context -> int -> tactic |
|
57 val satx_tac: Proof.context -> int -> tactic |
|
58 end |
|
59 |
|
60 functor SATFunc(cnf : CNF) : SAT = |
|
61 struct |
|
62 |
|
63 val trace_sat = Unsynchronized.ref false; |
|
64 |
|
65 val solver = Unsynchronized.ref "zchaff_with_proofs"; |
|
66 (*see HOL/Tools/sat_solver.ML for possible values*) |
|
67 |
|
68 val counter = Unsynchronized.ref 0; |
|
69 |
|
70 val resolution_thm = |
|
71 @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)} |
|
72 |
|
73 val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT)); |
|
74 |
|
75 (* ------------------------------------------------------------------------- *) |
|
76 (* lit_ord: an order on integers that considers their absolute values only, *) |
|
77 (* thereby treating integers that represent the same atom (positively *) |
|
78 (* or negatively) as equal *) |
|
79 (* ------------------------------------------------------------------------- *) |
|
80 |
|
81 fun lit_ord (i, j) = int_ord (abs i, abs j); |
|
82 |
|
83 (* ------------------------------------------------------------------------- *) |
|
84 (* CLAUSE: during proof reconstruction, three kinds of clauses are *) |
|
85 (* distinguished: *) |
|
86 (* 1. NO_CLAUSE: clause not proved (yet) *) |
|
87 (* 2. ORIG_CLAUSE: a clause as it occurs in the original problem *) |
|
88 (* 3. RAW_CLAUSE: a raw clause, with additional precomputed information *) |
|
89 (* (a mapping from int's to its literals) for faster proof *) |
|
90 (* reconstruction *) |
|
91 (* ------------------------------------------------------------------------- *) |
|
92 |
|
93 datatype CLAUSE = |
|
94 NO_CLAUSE |
|
95 | ORIG_CLAUSE of thm |
|
96 | RAW_CLAUSE of thm * (int * cterm) list; |
|
97 |
|
98 (* ------------------------------------------------------------------------- *) |
|
99 (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *) |
|
100 (* resolution over the list (starting with its head), i.e. with two raw *) |
|
101 (* clauses *) |
|
102 (* [P, x1, ..., a, ..., xn] |- False *) |
|
103 (* and *) |
|
104 (* [Q, y1, ..., a', ..., ym] |- False *) |
|
105 (* (where a and a' are dual to each other), we convert the first clause *) |
|
106 (* to *) |
|
107 (* [P, x1, ..., xn] |- a ==> False , *) |
|
108 (* the second clause to *) |
|
109 (* [Q, y1, ..., ym] |- a' ==> False *) |
|
110 (* and then perform resolution with *) |
|
111 (* [| ?P ==> False; ~?P ==> False |] ==> False *) |
|
112 (* to produce *) |
|
113 (* [P, Q, x1, ..., xn, y1, ..., ym] |- False *) |
|
114 (* Each clause is accompanied with an association list mapping integers *) |
|
115 (* (positive for positive literals, negative for negative literals, and *) |
|
116 (* the same absolute value for dual literals) to the actual literals as *) |
|
117 (* cterms. *) |
|
118 (* ------------------------------------------------------------------------- *) |
|
119 |
|
120 fun resolve_raw_clauses _ [] = |
|
121 raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, []) |
|
122 | resolve_raw_clauses ctxt (c::cs) = |
|
123 let |
|
124 (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *) |
|
125 fun merge xs [] = xs |
|
126 | merge [] ys = ys |
|
127 | merge (x :: xs) (y :: ys) = |
|
128 (case (lit_ord o pairself fst) (x, y) of |
|
129 LESS => x :: merge xs (y :: ys) |
|
130 | EQUAL => x :: merge xs ys |
|
131 | GREATER => y :: merge (x :: xs) ys) |
|
132 |
|
133 (* find out which two hyps are used in the resolution *) |
|
134 fun find_res_hyps ([], _) _ = |
|
135 raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) |
|
136 | find_res_hyps (_, []) _ = |
|
137 raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) |
|
138 | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc = |
|
139 (case (lit_ord o pairself fst) (h1, h2) of |
|
140 LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc) |
|
141 | EQUAL => |
|
142 let |
|
143 val (i1, chyp1) = h1 |
|
144 val (i2, chyp2) = h2 |
|
145 in |
|
146 if i1 = ~ i2 then |
|
147 (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2) |
|
148 else (* i1 = i2 *) |
|
149 find_res_hyps (hyps1, hyps2) (h1 :: acc) |
|
150 end |
|
151 | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc)) |
|
152 |
|
153 fun resolution (c1, hyps1) (c2, hyps2) = |
|
154 let |
|
155 val _ = |
|
156 if ! trace_sat then (* FIXME !? *) |
|
157 tracing ("Resolving clause: " ^ Display.string_of_thm ctxt c1 ^ |
|
158 " (hyps: " ^ ML_Syntax.print_list |
|
159 (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1) |
|
160 ^ ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^ |
|
161 " (hyps: " ^ ML_Syntax.print_list |
|
162 (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")") |
|
163 else () |
|
164 |
|
165 (* the two literals used for resolution *) |
|
166 val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) [] |
|
167 |
|
168 val c1' = Thm.implies_intr hyp1 c1 (* Gamma1 |- hyp1 ==> False *) |
|
169 val c2' = Thm.implies_intr hyp2 c2 (* Gamma2 |- hyp2 ==> False *) |
|
170 |
|
171 val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *) |
|
172 let |
|
173 val cLit = |
|
174 snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *) |
|
175 in |
|
176 Thm.instantiate ([], [(cP, cLit)]) resolution_thm |
|
177 end |
|
178 |
|
179 val _ = |
|
180 if !trace_sat then |
|
181 tracing ("Resolution theorem: " ^ Display.string_of_thm ctxt res_thm) |
|
182 else () |
|
183 |
|
184 (* Gamma1, Gamma2 |- False *) |
|
185 val c_new = |
|
186 Thm.implies_elim |
|
187 (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1')) |
|
188 (if hyp1_is_neg then c1' else c2') |
|
189 |
|
190 val _ = |
|
191 if !trace_sat then |
|
192 tracing ("Resulting clause: " ^ Display.string_of_thm ctxt c_new ^ |
|
193 " (hyps: " ^ ML_Syntax.print_list |
|
194 (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")") |
|
195 else () |
|
196 val _ = Unsynchronized.inc counter |
|
197 in |
|
198 (c_new, new_hyps) |
|
199 end |
|
200 in |
|
201 fold resolution cs c |
|
202 end; |
|
203 |
|
204 (* ------------------------------------------------------------------------- *) |
|
205 (* replay_proof: replays the resolution proof returned by the SAT solver; *) |
|
206 (* cf. SatSolver.proof for details of the proof format. Updates the *) |
|
207 (* 'clauses' array with derived clauses, and returns the derived clause *) |
|
208 (* at index 'empty_id' (which should just be "False" if proof *) |
|
209 (* reconstruction was successful, with the used clauses as hyps). *) |
|
210 (* 'atom_table' must contain an injective mapping from all atoms that *) |
|
211 (* occur (as part of a literal) in 'clauses' to positive integers. *) |
|
212 (* ------------------------------------------------------------------------- *) |
|
213 |
|
214 fun replay_proof ctxt atom_table clauses (clause_table, empty_id) = |
|
215 let |
|
216 fun index_of_literal chyp = |
|
217 (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of |
|
218 (Const (@{const_name Not}, _) $ atom) => |
|
219 SOME (~ (the (Termtab.lookup atom_table atom))) |
|
220 | atom => SOME (the (Termtab.lookup atom_table atom))) |
|
221 handle TERM _ => NONE; (* 'chyp' is not a literal *) |
|
222 |
|
223 fun prove_clause id = |
|
224 (case Array.sub (clauses, id) of |
|
225 RAW_CLAUSE clause => clause |
|
226 | ORIG_CLAUSE thm => |
|
227 (* convert the original clause *) |
|
228 let |
|
229 val _ = |
|
230 if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else () |
|
231 val raw = cnf.clause2raw_thm thm |
|
232 val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp => |
|
233 Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw))) |
|
234 val clause = (raw, hyps) |
|
235 val _ = Array.update (clauses, id, RAW_CLAUSE clause) |
|
236 in |
|
237 clause |
|
238 end |
|
239 | NO_CLAUSE => |
|
240 (* prove the clause, using information from 'clause_table' *) |
|
241 let |
|
242 val _ = |
|
243 if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else () |
|
244 val ids = the (Inttab.lookup clause_table id) |
|
245 val clause = resolve_raw_clauses ctxt (map prove_clause ids) |
|
246 val _ = Array.update (clauses, id, RAW_CLAUSE clause) |
|
247 val _ = |
|
248 if !trace_sat then |
|
249 tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) |
|
250 else () |
|
251 in |
|
252 clause |
|
253 end) |
|
254 |
|
255 val _ = counter := 0 |
|
256 val empty_clause = fst (prove_clause empty_id) |
|
257 val _ = |
|
258 if !trace_sat then |
|
259 tracing ("Proof reconstruction successful; " ^ |
|
260 string_of_int (!counter) ^ " resolution step(s) total.") |
|
261 else () |
|
262 in |
|
263 empty_clause |
|
264 end; |
|
265 |
|
266 (* ------------------------------------------------------------------------- *) |
|
267 (* string_of_prop_formula: return a human-readable string representation of *) |
|
268 (* a 'prop_formula' (just for tracing) *) |
|
269 (* ------------------------------------------------------------------------- *) |
|
270 |
|
271 fun string_of_prop_formula Prop_Logic.True = "True" |
|
272 | string_of_prop_formula Prop_Logic.False = "False" |
|
273 | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i |
|
274 | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm |
|
275 | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) = |
|
276 "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")" |
|
277 | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) = |
|
278 "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")"; |
|
279 |
|
280 (* ------------------------------------------------------------------------- *) |
|
281 (* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) |
|
282 (* a proof from the resulting proof trace of the SAT solver. The *) |
|
283 (* theorem returned is just "False" (with some of the given clauses as *) |
|
284 (* hyps). *) |
|
285 (* ------------------------------------------------------------------------- *) |
|
286 |
|
287 fun rawsat_thm ctxt clauses = |
|
288 let |
|
289 (* remove premises that equal "True" *) |
|
290 val clauses' = filter (fn clause => |
|
291 (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause |
|
292 handle TERM ("dest_Trueprop", _) => true) clauses |
|
293 (* remove non-clausal premises -- of course this shouldn't actually *) |
|
294 (* remove anything as long as 'rawsat_tac' is only called after the *) |
|
295 (* premises have been converted to clauses *) |
|
296 val clauses'' = filter (fn clause => |
|
297 ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause |
|
298 handle TERM ("dest_Trueprop", _) => false) |
|
299 orelse ( |
|
300 warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause)); |
|
301 false)) clauses' |
|
302 (* remove trivial clauses -- this is necessary because zChaff removes *) |
|
303 (* trivial clauses during preprocessing, and otherwise our clause *) |
|
304 (* numbering would be off *) |
|
305 val nontrivial_clauses = |
|
306 filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses'' |
|
307 (* sort clauses according to the term order -- an optimization, *) |
|
308 (* useful because forming the union of hypotheses, as done by *) |
|
309 (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *) |
|
310 (* terms sorted in descending order, while only linear for terms *) |
|
311 (* sorted in ascending order *) |
|
312 val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses |
|
313 val _ = |
|
314 if !trace_sat then |
|
315 tracing ("Sorted non-trivial clauses:\n" ^ |
|
316 cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) |
|
317 else () |
|
318 (* translate clauses from HOL terms to Prop_Logic.prop_formula *) |
|
319 val (fms, atom_table) = |
|
320 fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) |
|
321 sorted_clauses Termtab.empty |
|
322 val _ = |
|
323 if !trace_sat then |
|
324 tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) |
|
325 else () |
|
326 val fm = Prop_Logic.all fms |
|
327 fun make_quick_and_dirty_thm () = |
|
328 let |
|
329 val _ = |
|
330 if !trace_sat then |
|
331 tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead." |
|
332 else () |
|
333 val False_thm = Skip_Proof.make_thm_cterm @{cprop False} |
|
334 in |
|
335 (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *) |
|
336 (* Thm.weaken sorted_clauses' would be quadratic, since we sorted *) |
|
337 (* clauses in ascending order (which is linear for *) |
|
338 (* 'Conjunction.intr_balanced', used below) *) |
|
339 fold Thm.weaken (rev sorted_clauses) False_thm |
|
340 end |
|
341 in |
|
342 case |
|
343 let val the_solver = ! solver |
|
344 in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end |
|
345 of |
|
346 SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => |
|
347 (if !trace_sat then |
|
348 tracing ("Proof trace from SAT solver:\n" ^ |
|
349 "clauses: " ^ ML_Syntax.print_list |
|
350 (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int)) |
|
351 (Inttab.dest clause_table) ^ "\n" ^ |
|
352 "empty clause: " ^ string_of_int empty_id) |
|
353 else (); |
|
354 if Config.get ctxt quick_and_dirty then |
|
355 make_quick_and_dirty_thm () |
|
356 else |
|
357 let |
|
358 (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i"; *) |
|
359 (* this avoids accumulation of hypotheses during resolution *) |
|
360 (* [c_1, ..., c_n] |- c_1 && ... && c_n *) |
|
361 val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses) |
|
362 (* [c_1 && ... && c_n] |- c_1 && ... && c_n *) |
|
363 val cnf_cterm = cprop_of clauses_thm |
|
364 val cnf_thm = Thm.assume cnf_cterm |
|
365 (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *) |
|
366 val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm |
|
367 (* initialize the clause array with the given clauses *) |
|
368 val max_idx = fst (the (Inttab.max clause_table)) |
|
369 val clause_arr = Array.array (max_idx + 1, NO_CLAUSE) |
|
370 val _ = |
|
371 fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) |
|
372 cnf_clauses 0 |
|
373 (* replay the proof to derive the empty clause *) |
|
374 (* [c_1 && ... && c_n] |- False *) |
|
375 val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id) |
|
376 in |
|
377 (* [c_1, ..., c_n] |- False *) |
|
378 Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm |
|
379 end) |
|
380 | SatSolver.UNSATISFIABLE NONE => |
|
381 if Config.get ctxt quick_and_dirty then |
|
382 (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"; |
|
383 make_quick_and_dirty_thm ()) |
|
384 else |
|
385 raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, []) |
|
386 | SatSolver.SATISFIABLE assignment => |
|
387 let |
|
388 val msg = |
|
389 "SAT solver found a countermodel:\n" ^ |
|
390 (commas o map (fn (term, idx) => |
|
391 Syntax.string_of_term_global @{theory} term ^ ": " ^ |
|
392 (case assignment idx of NONE => "arbitrary" |
|
393 | SOME true => "true" | SOME false => "false"))) |
|
394 (Termtab.dest atom_table) |
|
395 in |
|
396 raise THM (msg, 0, []) |
|
397 end |
|
398 | SatSolver.UNKNOWN => |
|
399 raise THM ("SAT solver failed to decide the formula", 0, []) |
|
400 end; |
|
401 |
|
402 (* ------------------------------------------------------------------------- *) |
|
403 (* Tactics *) |
|
404 (* ------------------------------------------------------------------------- *) |
|
405 |
|
406 (* ------------------------------------------------------------------------- *) |
|
407 (* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal *) |
|
408 (* should be of the form *) |
|
409 (* [| c1; c2; ...; ck |] ==> False *) |
|
410 (* where each cj is a non-empty clause (i.e. a disjunction of literals) *) |
|
411 (* or "True" *) |
|
412 (* ------------------------------------------------------------------------- *) |
|
413 |
|
414 fun rawsat_tac ctxt i = |
|
415 Subgoal.FOCUS (fn {context = ctxt', prems, ...} => |
|
416 rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i; |
|
417 |
|
418 (* ------------------------------------------------------------------------- *) |
|
419 (* pre_cnf_tac: converts the i-th subgoal *) |
|
420 (* [| A1 ; ... ; An |] ==> B *) |
|
421 (* to *) |
|
422 (* [| A1; ... ; An ; ~B |] ==> False *) |
|
423 (* (handling meta-logical connectives in B properly before negating), *) |
|
424 (* then replaces meta-logical connectives in the premises (i.e. "==>", *) |
|
425 (* "!!" and "==") by connectives of the HOL object-logic (i.e. by *) |
|
426 (* "-->", "!", and "="), then performs beta-eta-normalization on the *) |
|
427 (* subgoal *) |
|
428 (* ------------------------------------------------------------------------- *) |
|
429 |
|
430 fun pre_cnf_tac ctxt = |
|
431 rtac ccontr THEN' |
|
432 Object_Logic.atomize_prems_tac ctxt THEN' |
|
433 CONVERSION Drule.beta_eta_conversion; |
|
434 |
|
435 (* ------------------------------------------------------------------------- *) |
|
436 (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *) |
|
437 (* if not, eliminates conjunctions (i.e. each clause of the CNF formula *) |
|
438 (* becomes a separate premise), then applies 'rawsat_tac' to solve the *) |
|
439 (* subgoal *) |
|
440 (* ------------------------------------------------------------------------- *) |
|
441 |
|
442 fun cnfsat_tac ctxt i = |
|
443 (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i); |
|
444 |
|
445 (* ------------------------------------------------------------------------- *) |
|
446 (* cnfxsat_tac: checks if the empty clause "False" occurs among the *) |
|
447 (* premises; if not, eliminates conjunctions (i.e. each clause of the *) |
|
448 (* CNF formula becomes a separate premise) and existential quantifiers, *) |
|
449 (* then applies 'rawsat_tac' to solve the subgoal *) |
|
450 (* ------------------------------------------------------------------------- *) |
|
451 |
|
452 fun cnfxsat_tac ctxt i = |
|
453 (etac FalseE i) ORELSE |
|
454 (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i); |
|
455 |
|
456 (* ------------------------------------------------------------------------- *) |
|
457 (* sat_tac: tactic for calling an external SAT solver, taking as input an *) |
|
458 (* arbitrary formula. The input is translated to CNF, possibly causing *) |
|
459 (* an exponential blowup. *) |
|
460 (* ------------------------------------------------------------------------- *) |
|
461 |
|
462 fun sat_tac ctxt i = |
|
463 pre_cnf_tac ctxt i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i; |
|
464 |
|
465 (* ------------------------------------------------------------------------- *) |
|
466 (* satx_tac: tactic for calling an external SAT solver, taking as input an *) |
|
467 (* arbitrary formula. The input is translated to CNF, possibly *) |
|
468 (* introducing new literals. *) |
|
469 (* ------------------------------------------------------------------------- *) |
|
470 |
|
471 fun satx_tac ctxt i = |
|
472 pre_cnf_tac ctxt i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i; |
|
473 |
|
474 end; |
|