author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 29269  5c25a2012975 
child 32010  cb1a1c94b4cd 
permissions  rwrr 
17618  1 
(* Title: HOL/Tools/sat_funcs.ML 
2 
Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27115
diff
changeset

3 
Author: Tjark Weber, TU Muenchen 
17618  4 

5 
Proof reconstruction from SAT solvers. 

6 

7 
Description: 

8 
This file defines several tactics to invoke a proofproducing 

9 
SAT solver on a propositional goal in clausal form. 

10 

11 
We use a sequent presentation of clauses to speed up resolution 

17695  12 
proof reconstruction. 
13 
We call such clauses "raw clauses", which are of the form 

20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

14 
[x1, ..., xn, P]  False 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

15 
(note the use of  instead of ==>, i.e. of Isabelle's (meta)hyps here), 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

16 
where each xi is a literal (see also comments in cnf_funcs.ML). 
17618  17 

19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

18 
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

19 

20039
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

20 
The tactic produces a clause representation of the given goal 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

21 
in DIMACS format and invokes a SAT solver, which should return 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

22 
a proof consisting of a sequence of resolution steps, indicating 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

23 
the two input clauses, and resulting in new clauses, leading to 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

24 
the empty clause (i.e. "False"). The tactic replays this proof 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

25 
in Isabelle and thus solves the overall goal. 
17618  26 

20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

27 
There are three SAT tactics available. They differ in the CNF transformation 
20039
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

28 
used. "sat_tac" uses naive CNF transformation to transform the theorem to be 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

29 
proved before giving it to the SAT solver. The naive transformation in the 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

30 
worst case can lead to an exponential blow up in formula size. Another 
20039
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

31 
tactic, "satx_tac", uses "definitional CNF transformation" which attempts to 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

32 
produce a formula of linear size increase compared to the input formula, at 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

33 
the cost of possibly introducing new variables. See cnf_funcs.ML for more 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

34 
comments on the CNF transformation. "rawsat_tac" should be used with 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

35 
caution: no CNF transformation is performed, and the tactic's behavior is 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

36 
undefined if the subgoal is not already given as [ C1; ...; Cn ] ==> False, 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

37 
where each Ci is a disjunction. 
17618  38 

20039
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

39 
The SAT solver to be used can be set via the "solver" reference. See 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

40 
sat_solvers.ML for possible values, and etc/settings for required (solver 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

41 
dependent) configuration settings. To replay SAT proofs in Isabelle, you 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

42 
must of course use a proofproducing SAT solver in the first place. 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

43 

4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

44 
Proofs are replayed only if "!quick_and_dirty" is false. If 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

45 
"!quick_and_dirty" is true, the theorem (in case the SAT solver claims its 
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

46 
negation to be unsatisfiable) is proved via an oracle. 
17618  47 
*) 
48 

49 
signature SAT = 

50 
sig 

21267  51 
val trace_sat : bool ref (* input: print trace messages *) 
52 
val solver : string ref (* input: name of SAT solver to be used *) 

53 
val counter : int ref (* output: number of resolution steps during last proof replay *) 

54 
val rawsat_thm : cterm list > thm 

20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

55 
val rawsat_tac : int > Tactical.tactic 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

56 
val sat_tac : int > Tactical.tactic 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

57 
val satx_tac : int > Tactical.tactic 
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 

20170  65 
val solver = ref "zchaff_with_proofs"; (* see HOL/Tools/sat_solver.ML for possible values *) 
20039
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

66 

17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

67 
val counter = ref 0; 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

68 

21267  69 
val resolution_thm = (* "[ ?P ==> False; ~ ?P ==> False ] ==> False" *) 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

70 
let 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

71 
val cterm = cterm_of (the_context ()) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

72 
val Q = Var (("Q", 0), HOLogic.boolT) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

73 
val False = HOLogic.false_const 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

74 
in 
27115
0dcafa5c9e3f
eliminated obsolete case_split_thm  use case_split;
wenzelm
parents:
26939
diff
changeset

75 
Thm.instantiate ([], [(cterm Q, cterm False)]) @{thm case_split} 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

76 
end; 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

77 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

78 
val cP = cterm_of (theory_of_thm resolution_thm) (Var (("P", 0), HOLogic.boolT)); 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

79 

28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

80 
(*  *) 
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

81 
(* lit_ord: an order on integers that considers their absolute values only, *) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

82 
(* thereby treating integers that represent the same atom (positively *) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

83 
(* or negatively) as equal *) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

84 
(*  *) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

85 

69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

86 
fun lit_ord (i, j) = 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

87 
int_ord (abs i, abs j); 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

88 

69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

89 
(*  *) 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

90 
(* CLAUSE: during proof reconstruction, three kinds of clauses are *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

91 
(* distinguished: *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

92 
(* 1. NO_CLAUSE: clause not proved (yet) *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

93 
(* 2. ORIG_CLAUSE: a clause as it occurs in the original problem *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

94 
(* 3. RAW_CLAUSE: a raw clause, with additional precomputed information *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

95 
(* (a mapping from int's to its literals) for faster proof *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

96 
(* reconstruction *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

97 
(*  *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

98 

28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

99 
datatype CLAUSE = NO_CLAUSE 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

100 
 ORIG_CLAUSE of Thm.thm 
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

101 
 RAW_CLAUSE of Thm.thm * (int * Thm.cterm) list; 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

102 

17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

103 
(*  *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

104 
(* 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

105 
(* 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

106 
(* clauses *) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

107 
(* [P, x1, ..., a, ..., xn]  False *) 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

108 
(* and *) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

109 
(* [Q, y1, ..., a', ..., ym]  False *) 
19976
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset

110 
(* (where a and a' are dual to each other), we convert the first clause *) 
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset

111 
(* to *) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

112 
(* [P, x1, ..., xn]  a ==> False , *) 
19976
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset

113 
(* the second clause to *) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

114 
(* [Q, y1, ..., ym]  a' ==> False *) 
19976
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset

115 
(* and then perform resolution with *) 
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset

116 
(* [ ?P ==> False; ~?P ==> False ] ==> False *) 
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset

117 
(* to produce *) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

118 
(* [P, Q, x1, ..., xn, y1, ..., ym]  False *) 
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

119 
(* Each clause is accompanied with an association list mapping integers *) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

120 
(* (positive for positive literals, negative for negative literals, and *) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

121 
(* the same absolute value for dual literals) to the actual literals as *) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

122 
(* cterms. *) 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

123 
(*  *) 
17618  124 

21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

125 
(* (Thm.thm * (int * Thm.cterm) list) list > Thm.thm * (int * Thm.cterm) list *) 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

126 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

127 
fun resolve_raw_clauses [] = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

128 
raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, []) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

129 
 resolve_raw_clauses (c::cs) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

130 
let 
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

131 
(* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

132 
fun merge xs [] = xs 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

133 
 merge [] ys = ys 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

134 
 merge (x::xs) (y::ys) = 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

135 
(case (lit_ord o pairself fst) (x, y) of 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

136 
LESS => x :: merge xs (y::ys) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

137 
 EQUAL => x :: merge xs ys 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

138 
 GREATER => y :: merge (x::xs) ys) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

139 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

140 
(* find out which two hyps are used in the resolution *) 
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

141 
(* (int * Thm.cterm) list * (int * Thm.cterm) list > (int * Thm.cterm) list > bool * Thm.cterm * Thm.cterm * (int * Thm.cterm) list *) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

142 
fun find_res_hyps ([], _) _ = 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

143 
raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

144 
 find_res_hyps (_, []) _ = 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

145 
raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

146 
 find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc = 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

147 
(case (lit_ord o pairself fst) (h1, h2) of 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

148 
LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

149 
 EQUAL => let 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

150 
val (i1, chyp1) = h1 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

151 
val (i2, chyp2) = h2 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

152 
in 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

153 
if i1 = ~ i2 then 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

154 
(i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

155 
else (* i1 = i2 *) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

156 
find_res_hyps (hyps1, hyps2) (h1 :: acc) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

157 
end 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

158 
 GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc)) 
19976
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset

159 

21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

160 
(* Thm.thm * (int * Thm.cterm) list > Thm.thm * (int * Thm.cterm) list > Thm.thm * (int * Thm.cterm) list *) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

161 
fun resolution (c1, hyps1) (c2, hyps2) = 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

162 
let 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

163 
val _ = if !trace_sat then 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset

164 
tracing ("Resolving clause: " ^ Display.string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1)) 
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset

165 
^ ")\nwith clause: " ^ Display.string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")") 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

166 
else () 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

167 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

168 
(* the two literals used for resolution *) 
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

169 
val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) [] 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

170 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

171 
val c1' = Thm.implies_intr hyp1 c1 (* Gamma1  hyp1 ==> False *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

172 
val c2' = Thm.implies_intr hyp2 c2 (* Gamma2  hyp2 ==> False *) 
17618  173 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

174 
val res_thm = (*  (lit ==> False) ==> (~lit ==> False) ==> False *) 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

175 
let 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

176 
val cLit = snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *) 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

177 
in 
19976
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset

178 
Thm.instantiate ([], [(cP, cLit)]) resolution_thm 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

179 
end 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

180 

150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

181 
val _ = if !trace_sat then 
26928  182 
tracing ("Resolution theorem: " ^ Display.string_of_thm res_thm) 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

183 
else () 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

184 

20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

185 
(* Gamma1, Gamma2  False *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

186 
val c_new = Thm.implies_elim 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

187 
(Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1')) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

188 
(if hyp1_is_neg then c1' else c2') 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

189 

19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

190 
val _ = if !trace_sat then 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset

191 
tracing ("Resulting clause: " ^ Display.string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")") 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

192 
else () 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

193 
val _ = inc counter 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

194 
in 
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

195 
(c_new, new_hyps) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

196 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

197 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

198 
fold resolution cs c 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

199 
end; 
17618  200 

17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

201 
(*  *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

202 
(* replay_proof: replays the resolution proof returned by the SAT solver; *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

203 
(* cf. SatSolver.proof for details of the proof format. Updates the *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

204 
(* 'clauses' array with derived clauses, and returns the derived clause *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

205 
(* at index 'empty_id' (which should just be "False" if proof *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

206 
(* reconstruction was successful, with the used clauses as hyps). *) 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

207 
(* 'atom_table' must contain an injective mapping from all atoms that *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

208 
(* occur (as part of a literal) in 'clauses' to positive integers. *) 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

209 
(*  *) 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

210 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

211 
(* int Termtab.table > CLAUSE Array.array > SatSolver.proof > Thm.thm *) 
17618  212 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

213 
fun replay_proof atom_table clauses (clause_table, empty_id) = 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

214 
let 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

215 
(* Thm.cterm > int option *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

216 
fun index_of_literal chyp = ( 
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

217 
case (HOLogic.dest_Trueprop o Thm.term_of) chyp of 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

218 
(Const ("Not", _) $ atom) => 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

219 
SOME (~(valOf (Termtab.lookup atom_table atom))) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

220 
 atom => 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

221 
SOME (valOf (Termtab.lookup atom_table atom)) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

222 
) handle TERM _ => NONE; (* 'chyp' is not a literal *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

223 

21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

224 
(* int > Thm.thm * (int * Thm.cterm) list *) 
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset

225 
fun prove_clause id = 
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset

226 
case Array.sub (clauses, id) of 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

227 
RAW_CLAUSE clause => 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

228 
clause 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

229 
 ORIG_CLAUSE thm => 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

230 
(* convert the original clause *) 
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset

231 
let 
21768
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

232 
val _ = if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else () 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

233 
val raw = cnf.clause2raw_thm thm 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

234 
val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp => 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

235 
Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw))) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

236 
val clause = (raw, hyps) 
69165d27b55b
ordered lists instead of tables for resolving hyps; speedup
webertj
parents:
21756
diff
changeset

237 
val _ = Array.update (clauses, id, RAW_CLAUSE clause) 
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset

238 
in 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

239 
clause 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

240 
end 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

241 
 NO_CLAUSE => 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

242 
(* prove the clause, using information from 'clause_table' *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

243 
let 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

244 
val _ = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else () 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

245 
val ids = valOf (Inttab.lookup clause_table id) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

246 
val clause = resolve_raw_clauses (map prove_clause ids) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

247 
val _ = Array.update (clauses, id, RAW_CLAUSE clause) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

248 
val _ = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else () 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

249 
in 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

250 
clause 
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset

251 
end 
17618  252 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

253 
val _ = counter := 0 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

254 
val empty_clause = fst (prove_clause empty_id) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

255 
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

256 
in 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

257 
empty_clause 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

258 
end; 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

259 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

260 
(*  *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

261 
(* string_of_prop_formula: return a humanreadable string representation of *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

262 
(* a 'prop_formula' (just for tracing) *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

263 
(*  *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

264 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

265 
(* PropLogic.prop_formula > string *) 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

266 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

267 
fun string_of_prop_formula PropLogic.True = "True" 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

268 
 string_of_prop_formula PropLogic.False = "False" 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

269 
 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

270 
 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

271 
 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

272 
 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

273 

5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

274 
(*  *) 
21267  275 
(* take_prefix: *) 
276 
(* take_prefix n [x_1, ..., x_k] = ([x_1, ..., x_n], [x_n+1, ..., x_k]) *) 

17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

277 
(*  *) 
17618  278 

21267  279 
(* int > 'a list > 'a list * 'a list *) 
280 

281 
fun take_prefix n xs = 

282 
let 

283 
fun take 0 (rxs, xs) = (rev rxs, xs) 

284 
 take _ (rxs, []) = (rev rxs, []) 

285 
 take n (rxs, x :: xs) = take (n1) (x :: rxs, xs) 

286 
in 

287 
take n ([], xs) 

288 
end; 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

289 

21267  290 
(*  *) 
291 
(* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) 

292 
(* a proof from the resulting proof trace of the SAT solver. The *) 

293 
(* theorem returned is just "False" (with some of the given clauses as *) 

294 
(* hyps). *) 

295 
(*  *) 

296 

297 
(* Thm.cterm list > Thm.thm *) 

298 

299 
fun rawsat_thm clauses = 

17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

300 
let 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

301 
(* remove premises that equal "True" *) 
21267  302 
val clauses' = filter (fn clause => 
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

303 
(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause 
21267  304 
handle TERM ("dest_Trueprop", _) => true) clauses 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

305 
(* remove nonclausal premises  of course this shouldn't actually *) 
21267  306 
(* remove anything as long as 'rawsat_tac' is only called after the *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

307 
(* premises have been converted to clauses *) 
21267  308 
val clauses'' = filter (fn clause => 
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

309 
((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause 
21267  310 
handle TERM ("dest_Trueprop", _) => false) 
311 
orelse ( 

26928  312 
warning ("Ignoring nonclausal premise " ^ Display.string_of_cterm clause); 
21267  313 
false)) clauses' 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

314 
(* remove trivial clauses  this is necessary because zChaff removes *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

315 
(* trivial clauses during preprocessing, and otherwise our clause *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

316 
(* numbering would be off *) 
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

317 
val nontrivial_clauses = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses'' 
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

318 
(* sort clauses according to the term order  an optimization, *) 
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

319 
(* useful because forming the union of hypotheses, as done by *) 
23533  320 
(* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *) 
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

321 
(* terms sorted in descending order, while only linear for terms *) 
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

322 
(* sorted in ascending order *) 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27115
diff
changeset

323 
val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses 
21267  324 
val _ = if !trace_sat then 
26931  325 
tracing ("Sorted nontrivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses)) 
19534  326 
else () 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

327 
(* translate clauses from HOL terms to PropLogic.prop_formula *) 
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

328 
val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty 
21267  329 
val _ = if !trace_sat then 
26931  330 
tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

331 
else () 
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

332 
val fm = PropLogic.all fms 
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

333 
(* unit > Thm.thm *) 
21267  334 
fun make_quick_and_dirty_thm () = 
335 
let 

336 
val _ = if !trace_sat then 

337 
tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead." 

338 
else () 

339 
val False_thm = SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const) 

340 
in 

21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

341 
(* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *) 
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

342 
(* Thm.weaken sorted_clauses' would be quadratic, since we sorted *) 
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

343 
(* clauses in ascending order (which is linear for *) 
23533  344 
(* 'Conjunction.intr_balanced', used below) *) 
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

345 
fold Thm.weaken (rev sorted_clauses) False_thm 
21267  346 
end 
17618  347 
in 
21268  348 
case (tracing ("Invoking solver " ^ (!solver)); SatSolver.invoke_solver (!solver) fm) of 
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

349 
SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => ( 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

350 
if !trace_sat then 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

351 
tracing ("Proof trace from SAT solver:\n" ^ 
21756  352 
"clauses: " ^ ML_Syntax.print_list (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) (Inttab.dest clause_table) ^ "\n" ^ 
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

353 
"empty clause: " ^ Int.toString empty_id) 
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

354 
else (); 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

355 
if !quick_and_dirty then 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

356 
make_quick_and_dirty_thm () 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

357 
else 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

358 
let 
21267  359 
(* optimization: convert the given clauses to "[c_1 && ... && c_n]  c_i"; *) 
360 
(* this avoids accumulation of hypotheses during resolution *) 

361 
(* [c_1, ..., c_n]  c_1 && ... && c_n *) 

23533  362 
val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

363 
(* [c_1 && ... && c_n]  c_1 && ... && c_n *) 
21267  364 
val cnf_cterm = cprop_of clauses_thm 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

365 
val cnf_thm = Thm.assume cnf_cterm 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

366 
(* [[c_1 && ... && c_n]  c_1, ..., [c_1 && ... && c_n]  c_n] *) 
23533  367 
val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm 
20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

368 
(* initialize the clause array with the given clauses *) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

369 
val max_idx = valOf (Inttab.max_key clause_table) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

370 
val clause_arr = Array.array (max_idx + 1, NO_CLAUSE) 
21267  371 
val _ = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) cnf_clauses 0 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

372 
(* replay the proof to derive the empty clause *) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

373 
(* [c_1 && ... && c_n]  False *) 
21268  374 
val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id) 
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

375 
in 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

376 
(* [c_1, ..., c_n]  False *) 
21267  377 
Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm 
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

378 
end) 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

379 
 SatSolver.UNSATISFIABLE NONE => 
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

380 
if !quick_and_dirty then ( 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

381 
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

382 
make_quick_and_dirty_thm () 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

383 
) else 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

384 
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

385 
 SatSolver.SATISFIABLE assignment => 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

386 
let 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

387 
val msg = "SAT solver found a countermodel:\n" 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

388 
^ (commas 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

389 
o map (fn (term, idx) => 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset

390 
Syntax.string_of_term_global (the_context ()) term ^ ": " 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

391 
^ (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

392 
(Termtab.dest atom_table) 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

393 
in 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

394 
raise THM (msg, 0, []) 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

395 
end 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

396 
 SatSolver.UNKNOWN => 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

397 
raise THM ("SAT solver failed to decide the formula", 0, []) 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

398 
end; 
17618  399 

17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

400 
(*  *) 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

401 
(* Tactics *) 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

402 
(*  *) 
17618  403 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

404 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

405 
(* 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

406 
(* should be of the form *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

407 
(* [ c1; c2; ...; ck ] ==> False *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

408 
(* 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

409 
(* or "True" *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

410 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

411 

21267  412 
fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i; 
17618  413 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

414 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

415 
(* pre_cnf_tac: converts the ith subgoal *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

416 
(* [ A1 ; ... ; An ] ==> B *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

417 
(* to *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

418 
(* [ A1; ... ; An ; ~B ] ==> False *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

419 
(* (handling metalogical connectives in B properly before negating), *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

420 
(* then replaces metalogical connectives in the premises (i.e. "==>", *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

421 
(* "!!" and "==") by connectives of the HOL objectlogic (i.e. by *) 
19553
9d15911f1893
pre_cnf_tac: betaetanormalization restricted to the current subgoal
webertj
parents:
19534
diff
changeset

422 
(* ">", "!", and "="), then performs betaetanormalization on the *) 
9d15911f1893
pre_cnf_tac: betaetanormalization restricted to the current subgoal
webertj
parents:
19534
diff
changeset

423 
(* subgoal *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

424 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

425 

23533  426 
val pre_cnf_tac = 
427 
rtac ccontr THEN' 

23590
ad95084a5c63
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23533
diff
changeset

428 
ObjectLogic.atomize_prems_tac THEN' 
23533  429 
CONVERSION Drule.beta_eta_conversion; 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

430 

195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

431 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

432 
(* 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

433 
(* 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

434 
(* becomes a separate premise), then applies 'rawsat_tac' to solve the *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

435 
(* subgoal *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

436 
(*  *) 
17697  437 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

438 
fun cnfsat_tac i = 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

439 
(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i); 
17618  440 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

441 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

442 
(* cnfxsat_tac: checks if the empty clause "False" occurs among the *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

443 
(* premises; if not, eliminates conjunctions (i.e. each clause of the *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

444 
(* CNF formula becomes a separate premise) and existential quantifiers, *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

445 
(* then applies 'rawsat_tac' to solve the subgoal *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

446 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

447 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

448 
fun cnfxsat_tac i = 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

449 
(etac FalseE i) ORELSE 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

450 
(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i); 
17618  451 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

452 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

453 
(* 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

454 
(* arbitrary formula. The input is translated to CNF, possibly causing *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

455 
(* an exponential blowup. *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

456 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

457 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

458 
fun sat_tac i = 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

459 
pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i; 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

460 

195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

461 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

462 
(* 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

463 
(* arbitrary formula. The input is translated to CNF, possibly *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

464 
(* introducing new literals. *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

465 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

466 

20278
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

467 
fun satx_tac i = 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

468 
pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i; 
17618  469 

23533  470 
end; 