author | webertj |
Fri, 10 Mar 2006 16:31:50 +0100 | |
changeset 19236 | 150e8b0fb991 |
parent 17843 | 0a451f041853 |
child 19534 | 1724ec4032c5 |
permissions | -rw-r--r-- |
17618 | 1 |
(* Title: HOL/Tools/sat_funcs.ML |
2 |
ID: $Id$ |
|
3 |
Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
4 |
Author: Tjark Weber |
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
5 |
Copyright 2005-2006 |
17618 | 6 |
|
7 |
||
8 |
Proof reconstruction from SAT solvers. |
|
9 |
||
10 |
Description: |
|
11 |
This file defines several tactics to invoke a proof-producing |
|
12 |
SAT solver on a propositional goal in clausal form. |
|
13 |
||
14 |
We use a sequent presentation of clauses to speed up resolution |
|
17695 | 15 |
proof reconstruction. |
16 |
We call such clauses "raw clauses", which are of the form |
|
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
17 |
x1; ...; xn; c1; c2; ...; ck |- False |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
18 |
(note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here), |
17618 | 19 |
where each clause ci is of the form |
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
20 |
~ (l1 | l2 | ... | lm) ==> False, |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
21 |
where each xi and each li is a literal (see also comments in cnf_funcs.ML). |
17618 | 22 |
|
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
23 |
This does not work for goals containing schematic variables! |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
24 |
|
17618 | 25 |
The tactic produces a clause representation of the given goal |
26 |
in DIMACS format and invokes a SAT solver, which should return |
|
27 |
a proof consisting of a sequence of resolution steps, indicating |
|
17695 | 28 |
the two input clauses, and resulting in new clauses, leading to |
29 |
the empty clause (i.e., False). The tactic replays this proof |
|
30 |
in Isabelle and thus solves the overall goal. |
|
17618 | 31 |
|
32 |
There are two SAT tactics available. They differ in the CNF transformation |
|
33 |
used. The "sat_tac" uses naive CNF transformation to transform the theorem |
|
17695 | 34 |
to be proved before giving it to SAT solver. The naive transformation in |
17618 | 35 |
some worst case can lead to explonential blow up in formula size. |
36 |
The other tactic, the "satx_tac" uses the "definitional CNF transformation" |
|
37 |
which produces formula of linear size increase compared to the input formula. |
|
38 |
This transformation introduces new variables. See also cnf_funcs.ML for |
|
39 |
more comments. |
|
40 |
||
41 |
Notes for the current revision: |
|
42 |
- The current version supports only zChaff prover. |
|
43 |
- The environment variable ZCHAFF_HOME must be set to point to |
|
44 |
the directory where zChaff executable resides |
|
45 |
- The environment variable ZCHAFF_VERSION must be set according to |
|
46 |
the version of zChaff used. Current supported version of zChaff: |
|
47 |
zChaff version 2004.11.15 |
|
17695 | 48 |
- zChaff must have been compiled with proof generation enabled |
49 |
(#define VERIFY_ON). |
|
17618 | 50 |
*) |
51 |
||
52 |
signature SAT = |
|
53 |
sig |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
54 |
val trace_sat : bool ref (* print trace messages *) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
55 |
val sat_tac : int -> Tactical.tactic |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
56 |
val satx_tac : int -> Tactical.tactic |
17843 | 57 |
val counter : int ref (* number of resolution steps during last proof replay *) |
17618 | 58 |
end |
59 |
||
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
60 |
functor SATFunc (structure cnf : CNF) : SAT = |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
61 |
struct |
17618 | 62 |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
63 |
val trace_sat = ref false; |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
64 |
|
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
65 |
val counter = ref 0; |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
66 |
|
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
67 |
(* Thm.thm *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
68 |
val resolution_thm = (* "[| P ==> False; ~P ==> False |] ==> False" *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
69 |
let |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
70 |
val cterm = cterm_of (the_context ()) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
71 |
val Q = Var (("Q", 0), HOLogic.boolT) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
72 |
val False = HOLogic.false_const |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
73 |
in |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
74 |
Thm.instantiate ([], [(cterm Q, cterm False)]) case_split_thm |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
75 |
end; |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
76 |
|
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
77 |
(* ------------------------------------------------------------------------- *) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
78 |
(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
79 |
(* resolution over the list (starting with its head), i.e. with two raw *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
80 |
(* clauses *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
81 |
(* [| x1; ... ; a; ...; xn |] ==> False *) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
82 |
(* and *) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
83 |
(* [| y1; ... ; a'; ...; ym |] ==> False *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
84 |
(* (where a and a' are dual to each other), we first convert the first *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
85 |
(* clause to *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
86 |
(* [| x1; ...; xn |] ==> a' *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
87 |
(* (using swap_prem and perhaps notnotD), and then do a resolution with *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
88 |
(* the second clause to produce *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
89 |
(* [| y1; ...; x1; ...; xn; ...; yn |] ==> False *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
90 |
(* amd finally remove duplicate literals. *) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
91 |
(* ------------------------------------------------------------------------- *) |
17618 | 92 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
93 |
(* Thm.thm list -> Thm.thm *) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
94 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
95 |
fun resolve_raw_clauses [] = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
96 |
raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, []) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
97 |
| resolve_raw_clauses (c::cs) = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
98 |
let |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
99 |
fun dual (Const ("Not", _) $ x) = x |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
100 |
| dual x = HOLogic.Not $ x |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
101 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
102 |
fun is_neg (Const ("Not", _) $ _) = true |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
103 |
| is_neg _ = false |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
104 |
|
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
105 |
(* find out which two hyps are used in the resolution *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
106 |
(* Term.term list -> Term.term list -> Term.term * Term.term *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
107 |
fun res_hyps [] _ = |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
108 |
raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
109 |
| res_hyps _ [] = |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
110 |
raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) |
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
111 |
| res_hyps ((Const ("Trueprop", _) $ x) :: xs) ys = |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
112 |
let val dx = dual x in |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
113 |
(* hyps are implemented as ordered list in the kernel, and *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
114 |
(* stripping 'Trueprop' should not change the order *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
115 |
if OrdList.member Term.fast_term_ord ys dx then |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
116 |
(x, dx) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
117 |
else |
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
118 |
res_hyps xs ys |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
119 |
end |
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
120 |
| res_hyps (_ :: xs) ys = |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
121 |
(* hyps are implemented as ordered list in the kernel, all hyps are of *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
122 |
(* the form 'Trueprop $ lit' or 'implies $ (negated clause) $ False', *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
123 |
(* and the former are LESS than the latter according to the order -- *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
124 |
(* therefore there is no need to continue the search via *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
125 |
(* 'res_hyps xs ys' here *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
126 |
raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
127 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
128 |
(* Thm.thm -> Thm.thm -> Thm.thm *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
129 |
fun resolution c1 c2 = |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
130 |
let |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
131 |
val _ = if !trace_sat then |
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
132 |
tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1))) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
133 |
^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2))) ^ ")") |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
134 |
else () |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
135 |
|
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
136 |
(* Term.term list -> Term.term list *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
137 |
fun dest_filter_Trueprop [] = [] |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
138 |
| dest_filter_Trueprop ((Const ("Trueprop", _) $ x) :: xs) = x :: dest_filter_Trueprop xs |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
139 |
| dest_filter_Trueprop (_ :: xs) = dest_filter_Trueprop xs |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
140 |
|
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
141 |
val hyps1 = (#hyps o rep_thm) c1 |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
142 |
(* minor optimization: dest/filter over the second list outside 'res_hyps' to do it only once *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
143 |
val hyps2 = (dest_filter_Trueprop o #hyps o rep_thm) c2 |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
144 |
|
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
145 |
val (l1, l2) = res_hyps hyps1 hyps2 (* the two literals used for resolution, with 'Trueprop' stripped *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
146 |
val is_neg = is_neg l1 |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
147 |
|
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
148 |
val c1' = Thm.implies_intr (cterm_of (theory_of_thm c1) (HOLogic.mk_Trueprop l1)) c1 (* Gamma1 |- l1 ==> False *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
149 |
val c2' = Thm.implies_intr (cterm_of (theory_of_thm c2) (HOLogic.mk_Trueprop l2)) c2 (* Gamma2 |- l2 ==> False *) |
17618 | 150 |
|
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
151 |
val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
152 |
let |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
153 |
val P = Var (("P", 0), HOLogic.boolT) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
154 |
val (lit, thy) = if is_neg then (l2, theory_of_thm c2') else (l1, theory_of_thm c1') |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
155 |
val cterm = cterm_of thy |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
156 |
in |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
157 |
Thm.instantiate ([], [(cterm P, cterm lit)]) resolution_thm |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
158 |
end |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
159 |
|
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
160 |
val _ = if !trace_sat then |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
161 |
tracing ("Resolution theorem: " ^ string_of_thm res_thm) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
162 |
else () |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
163 |
|
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
164 |
val c_new = Thm.implies_elim (Thm.implies_elim res_thm (if is_neg then c2' else c1')) (if is_neg then c1' else c2') (* Gamma1, Gamma2 |- False *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
165 |
|
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
166 |
val _ = if !trace_sat then |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
167 |
tracing ("Resulting clause: " ^ string_of_thm c_new ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new))) ^ ")") |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
168 |
else () |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
169 |
val _ = inc counter |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
170 |
in |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
171 |
c_new |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
172 |
end |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
173 |
in |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
174 |
fold resolution cs c |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
175 |
end; |
17618 | 176 |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
177 |
(* ------------------------------------------------------------------------- *) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
178 |
(* replay_proof: replays the resolution proof returned by the SAT solver; *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
179 |
(* cf. SatSolver.proof for details of the proof format. Updates the *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
180 |
(* 'clauses' array with derived clauses, and returns the derived clause *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
181 |
(* at index 'empty_id' (which should just be "False" if proof *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
182 |
(* reconstruction was successful, with the used clauses as hyps). *) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
183 |
(* ------------------------------------------------------------------------- *) |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
184 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
185 |
(* Thm.thm option Array.array -> SatSolver.proof -> Thm.thm *) |
17618 | 186 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
187 |
fun replay_proof clauses (clause_table, empty_id) = |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
188 |
let |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
189 |
(* int -> Thm.thm *) |
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset
|
190 |
fun prove_clause id = |
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset
|
191 |
case Array.sub (clauses, id) of |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
192 |
SOME thm => |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
193 |
thm |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
194 |
| NONE => |
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset
|
195 |
let |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
196 |
val _ = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else () |
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset
|
197 |
val ids = valOf (Inttab.lookup clause_table id) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
198 |
val thm = resolve_raw_clauses (map prove_clause ids) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
199 |
val _ = Array.update (clauses, id, SOME thm) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
200 |
val _ = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else () |
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset
|
201 |
in |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
202 |
thm |
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset
|
203 |
end |
17618 | 204 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
205 |
val _ = counter := 0 |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
206 |
val empty_clause = prove_clause empty_id |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
207 |
val _ = if !trace_sat then tracing ("Proof reconstruction successful; " ^ string_of_int (!counter) ^ " resolution step(s) total.") else () |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
208 |
in |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
209 |
empty_clause |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
210 |
end; |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
211 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
212 |
(* PropLogic.prop_formula -> string *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
213 |
fun string_of_prop_formula PropLogic.True = "True" |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
214 |
| string_of_prop_formula PropLogic.False = "False" |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
215 |
| string_of_prop_formula (PropLogic.BoolVar i) = "x" ^ string_of_int i |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
216 |
| string_of_prop_formula (PropLogic.Not fm) = "~" ^ string_of_prop_formula fm |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
217 |
| string_of_prop_formula (PropLogic.Or (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")" |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
218 |
| string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")"; |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
219 |
|
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
220 |
(* ------------------------------------------------------------------------- *) |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
221 |
(* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
222 |
(* a proof from the resulting proof trace of the SAT solver. Each *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
223 |
(* premise in 'prems' that is not a clause is ignored, and the theorem *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
224 |
(* returned is just "False" (with some clauses as hyps). *) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
225 |
(* ------------------------------------------------------------------------- *) |
17618 | 226 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
227 |
(* Thm.thm list -> Thm.thm *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
228 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
229 |
fun rawsat_thm prems = |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
230 |
let |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
231 |
(* remove premises that equal "True" *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
232 |
val non_triv_prems = filter (fn thm => |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
233 |
(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o prop_of) thm |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
234 |
handle TERM ("dest_Trueprop", _) => true) prems |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
235 |
(* remove non-clausal premises -- of course this shouldn't actually *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
236 |
(* remove anything as long as 'rawsat_thm' is only called after the *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
237 |
(* premises have been converted to clauses *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
238 |
val clauses = filter (fn thm => |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
239 |
((cnf.is_clause o HOLogic.dest_Trueprop o prop_of) thm handle TERM ("dest_Trueprop", _) => false) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
240 |
orelse (warning ("Ignoring non-clausal premise " ^ (string_of_cterm o cprop_of) thm); false)) non_triv_prems |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
241 |
(* remove trivial clauses -- this is necessary because zChaff removes *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
242 |
(* trivial clauses during preprocessing, and otherwise our clause *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
243 |
(* numbering would be off *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
244 |
val non_triv_clauses = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o prop_of) clauses |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
245 |
(* translate clauses from HOL terms to PropLogic.prop_formula *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
246 |
val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o prop_of) non_triv_clauses Termtab.empty |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
247 |
val _ = if !trace_sat then |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
248 |
tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms)) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
249 |
else () |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
250 |
val fm = PropLogic.all fms |
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
251 |
(* unit -> Thm.thm *) |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
252 |
fun make_quick_and_dirty_thm () = ( |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
253 |
if !trace_sat then |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
254 |
tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead." |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
255 |
else (); |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
256 |
(* of course just returning "False" is unsound; what we should return *) |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
257 |
(* instead is "False" with all 'non_triv_clauses' as hyps -- but this *) |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
258 |
(* might be rather slow, and it makes no real difference as long as *) |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
259 |
(* 'rawsat_thm' is only called from 'rawsat_tac' *) |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
260 |
SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const) |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
261 |
) |
17618 | 262 |
in |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
263 |
case SatSolver.invoke_solver "zchaff_with_proofs" fm of |
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
264 |
SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => ( |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
265 |
if !trace_sat then |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
266 |
tracing ("Proof trace from SAT solver:\n" ^ |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
267 |
"clauses: [" ^ commas (map (fn (c, cs) => |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
268 |
"(" ^ string_of_int c ^ ", [" ^ commas (map string_of_int cs) ^ "])") (Inttab.dest clause_table)) ^ "]\n" ^ |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
269 |
"empty clause: " ^ string_of_int empty_id) |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
270 |
else (); |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
271 |
if !quick_and_dirty then |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
272 |
make_quick_and_dirty_thm () |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
273 |
else |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
274 |
let |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
275 |
(* initialize the clause array with the given clauses, *) |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
276 |
(* but converted to raw clause format *) |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
277 |
val max_idx = valOf (Inttab.max_key clause_table) |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
278 |
val clause_arr = Array.array (max_idx + 1, NONE) |
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
279 |
val raw_clauses = map cnf.clause2raw_thm non_triv_clauses |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
280 |
(* Every raw clause has only its literals and itself as hyp, and hyps are *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
281 |
(* accumulated during resolution steps. Experimental results indicate *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
282 |
(* that it is NOT faster to weaken all raw_clauses to contain every *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
283 |
(* clause in the hyps beforehand. *) |
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
284 |
val _ = fold (fn thm => fn idx => (Array.update (clause_arr, idx, SOME thm); idx+1)) raw_clauses 0 |
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
285 |
(* replay the proof to derive the empty clause *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
286 |
val FalseThm = replay_proof clause_arr (clause_table, empty_id) |
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
287 |
in |
19236
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
288 |
(* convert the hyps back to the original format *) |
150e8b0fb991
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
webertj
parents:
17843
diff
changeset
|
289 |
cnf.rawhyps2clausehyps_thm FalseThm |
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
290 |
end) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
291 |
| SatSolver.UNSATISFIABLE NONE => |
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
292 |
if !quick_and_dirty then ( |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
293 |
warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"; |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
294 |
make_quick_and_dirty_thm () |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
295 |
) else |
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset
|
296 |
raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, []) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
297 |
| SatSolver.SATISFIABLE assignment => |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
298 |
let |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
299 |
val msg = "SAT solver found a countermodel:\n" |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
300 |
^ (commas |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
301 |
o map (fn (term, idx) => |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
302 |
Sign.string_of_term (the_context ()) term ^ ": " |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
303 |
^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false"))) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
304 |
(Termtab.dest atom_table) |
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
305 |
in |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
306 |
raise THM (msg, 0, []) |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
307 |
end |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
308 |
| SatSolver.UNKNOWN => |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
309 |
raise THM ("SAT solver failed to decide the formula", 0, []) |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
310 |
end; |
17618 | 311 |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
312 |
(* ------------------------------------------------------------------------- *) |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
313 |
(* Tactics *) |
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
314 |
(* ------------------------------------------------------------------------- *) |
17618 | 315 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
316 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
317 |
(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
318 |
(* should be of the form *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
319 |
(* [| c1; c2; ...; ck |] ==> False *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
320 |
(* where each cj is a non-empty clause (i.e. a disjunction of literals) *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
321 |
(* or "True" *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
322 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
323 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
324 |
(* int -> Tactical.tactic *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
325 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
326 |
fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm prems) 1) i; |
17618 | 327 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
328 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
329 |
(* pre_cnf_tac: converts the i-th subgoal *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
330 |
(* [| A1 ; ... ; An |] ==> B *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
331 |
(* to *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
332 |
(* [| A1; ... ; An ; ~B |] ==> False *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
333 |
(* (handling meta-logical connectives in B properly before negating), *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
334 |
(* then replaces meta-logical connectives in the premises (i.e. "==>", *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
335 |
(* "!!" and "==") by connectives of the HOL object-logic (i.e. by *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
336 |
(* "-->", "!", and "=") *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
337 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
338 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
339 |
(* int -> Tactical.tactic *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
340 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
341 |
fun pre_cnf_tac i = rtac ccontr i THEN ObjectLogic.atomize_tac i; |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
342 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
343 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
344 |
(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
345 |
(* if not, eliminates conjunctions (i.e. each clause of the CNF formula *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
346 |
(* becomes a separate premise), then applies 'rawsat_tac' to solve the *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
347 |
(* subgoal *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
348 |
(* ------------------------------------------------------------------------- *) |
17697 | 349 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
350 |
(* int -> Tactical.tactic *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
351 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
352 |
fun cnfsat_tac i = (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i); |
17618 | 353 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
354 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
355 |
(* cnfxsat_tac: checks if the empty clause "False" occurs among the *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
356 |
(* premises; if not, eliminates conjunctions (i.e. each clause of the *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
357 |
(* CNF formula becomes a separate premise) and existential quantifiers, *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
358 |
(* then applies 'rawsat_tac' to solve the subgoal *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
359 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
360 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
361 |
(* int -> Tactical.tactic *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
362 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
363 |
fun cnfxsat_tac i = (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i); |
17618 | 364 |
|
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
365 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
366 |
(* sat_tac: tactic for calling an external SAT solver, taking as input an *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
367 |
(* arbitrary formula. The input is translated to CNF, possibly causing *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
368 |
(* an exponential blowup. *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
369 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
370 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
371 |
(* int -> Tactical.tactic *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
372 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
373 |
fun sat_tac i = pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i; |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
374 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
375 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
376 |
(* satx_tac: tactic for calling an external SAT solver, taking as input an *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
377 |
(* arbitrary formula. The input is translated to CNF, possibly *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
378 |
(* introducing new literals. *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
379 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
380 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
381 |
(* int -> Tactical.tactic *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
382 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset
|
383 |
fun satx_tac i = pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i; |
17618 | 384 |
|
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset
|
385 |
end; (* of structure *) |