author  webertj 
Fri, 10 Mar 2006 16:31:50 +0100  
changeset 19236  150e8b0fb991 
parent 17843  0a451f041853 
child 19534  1724ec4032c5 
permissions  rwrr 
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 20052006 
17618  6 

7 

8 
Proof reconstruction from SAT solvers. 

9 

10 
Description: 

11 
This file defines several tactics to invoke a proofproducing 

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 nonempty 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 nonclausal 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 nonclausal 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 ith 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 nonempty 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 ith 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 metalogical connectives in B properly before negating), *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

334 
(* then replaces metalogical 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 objectlogic (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 *) 