author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 35625  9c818cab0dd0 
child 38549  d0385f2764d8 
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 

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

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

32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32283
diff
changeset

54 
val rawsat_thm: Proof.context > cterm list > thm 
32232  55 
val rawsat_tac: Proof.context > int > tactic 
56 
val sat_tac: Proof.context > int > tactic 

57 
val satx_tac: Proof.context > int > tactic 

17618  58 
end 
59 

32232  60 
functor SATFunc(cnf : CNF) : SAT = 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

61 
struct 
17618  62 

32740  63 
val trace_sat = Unsynchronized.ref false; 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

64 

32740  65 
val solver = Unsynchronized.ref "zchaff_with_proofs"; 
66 
(*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

67 

32740  68 
val counter = Unsynchronized.ref 0; 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

69 

32010  70 
val resolution_thm = 
71 
@{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)} 

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

72 

32010  73 
val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT)); 
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

74 

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

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

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

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

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

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

80 

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

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

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

83 

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

84 
(*  *) 
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

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

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

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

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

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

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

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

92 
(*  *) 
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 

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 
datatype CLAUSE = NO_CLAUSE 
33243  95 
 ORIG_CLAUSE of thm 
96 
 RAW_CLAUSE of thm * (int * 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

97 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

118 
(*  *) 
17618  119 

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

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

121 

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

122 
fun resolve_raw_clauses [] = 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

134 

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

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

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

137 
fun find_res_hyps ([], _) _ = 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

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

139 
 find_res_hyps (_, []) _ = 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

154 

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

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

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

157 
let 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

158 
val _ = 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

159 
if ! trace_sat then 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

160 
tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

161 
" (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1)) 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

162 
^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

163 
" (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

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

165 

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

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

167 
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

168 

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

169 
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

170 
val c2' = Thm.implies_intr hyp2 c2 (* Gamma2  hyp2 ==> False *) 
17618  171 

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

172 
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

173 
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

174 
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

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

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

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

178 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

179 
val _ = 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

180 
if !trace_sat then 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

181 
tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm) 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

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

183 

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

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

185 
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

186 
(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

187 
(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

188 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

189 
val _ = 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

190 
if !trace_sat then 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

191 
tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

192 
" (hyps: " ^ ML_Syntax.print_list 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset

193 
(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

194 
else () 
32740  195 
val _ = Unsynchronized.inc counter 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

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

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

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

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

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

201 
end; 
17618  202 

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

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

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

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

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

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

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

209 
(* '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

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

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

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 
(* int Termtab.table > CLAUSE Array.array > SatSolver.proof > Thm.thm *) 
17618  214 

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 
fun replay_proof atom_table clauses (clause_table, empty_id) = 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

216 
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

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

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

219 
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

220 
(Const ("Not", _) $ atom) => 
33035  221 
SOME (~ (the (Termtab.lookup atom_table atom))) 
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

222 
 atom => 
33035  223 
SOME (the (Termtab.lookup atom_table atom)) 
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

224 
) 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

225 

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

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

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

228 
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

229 
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

230 
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

231 
 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

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

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

234 
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

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

236 
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

237 
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

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

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

240 
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

241 
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 
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

243 
 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

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

245 
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

246 
val _ = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else () 
33035  247 
val ids = the (Inttab.lookup clause_table id) 
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

248 
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

249 
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

250 
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

251 
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

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

253 
end 
17618  254 

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

255 
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

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

257 
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

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

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

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

261 

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

262 
(*  *) 
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 
(* 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

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

265 
(*  *) 
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 
(* 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

268 

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

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

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

271 
 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

272 
 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

273 
 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

274 
 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

275 

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

276 
(*  *) 
21267  277 
(* take_prefix: *) 
278 
(* 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

279 
(*  *) 
17618  280 

21267  281 
(* int > 'a list > 'a list * 'a list *) 
282 

283 
fun take_prefix n xs = 

284 
let 

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

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

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

288 
in 

289 
take n ([], xs) 

290 
end; 

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

291 

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

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

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

296 
(* hyps). *) 

297 
(*  *) 

298 

32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32283
diff
changeset

299 
fun rawsat_thm ctxt 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 ( 

32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32283
diff
changeset

312 
warning ("Ignoring nonclausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of 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 *) 
35408  323 
val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses 
21267  324 
val _ = if !trace_sat then 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32283
diff
changeset

325 
tracing ("Sorted nontrivial clauses:\n" ^ 
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32283
diff
changeset

326 
cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) 
19534  327 
else () 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

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

329 
val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty 
21267  330 
val _ = if !trace_sat then 
26931  331 
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

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

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

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

337 
val _ = if !trace_sat then 

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

339 
else () 

32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32740
diff
changeset

340 
val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const) 
21267  341 
in 
21586
8da782143bde
clauses sorted according to term order (significant speedup in some cases)
webertj
parents:
21474
diff
changeset

342 
(* '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

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

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

346 
fold Thm.weaken (rev sorted_clauses) False_thm 
21267  347 
end 
17618  348 
in 
33228  349 
case 
350 
let val the_solver = ! solver 

351 
in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end 

352 
of 

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

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

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

355 
tracing ("Proof trace from SAT solver:\n" ^ 
33228  356 
"clauses: " ^ ML_Syntax.print_list 
357 
(ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) 

358 
(Inttab.dest clause_table) ^ "\n" ^ 

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

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

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

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

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

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

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

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

23533  368 
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

369 
(* [c_1 && ... && c_n]  c_1 && ... && c_n *) 
21267  370 
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

371 
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

372 
(* [[c_1 && ... && c_n]  c_1, ..., [c_1 && ... && c_n]  c_n] *) 
23533  373 
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

374 
(* initialize the clause array with the given clauses *) 
33035  375 
val max_idx = the (Inttab.max_key clause_table) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

376 
val clause_arr = Array.array (max_idx + 1, NO_CLAUSE) 
21267  377 
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

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

379 
(* [c_1 && ... && c_n]  False *) 
21268  380 
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

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

382 
(* [c_1, ..., c_n]  False *) 
21267  383 
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

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

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

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

387 
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

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

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

390 
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

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

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

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

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

395 
o map (fn (term, idx) => 
33228  396 
Syntax.string_of_term_global @{theory} term ^ ": " ^ 
397 
(case assignment idx of NONE => "arbitrary" 

398 
 SOME true => "true"  SOME false => "false"))) 

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

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

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

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

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

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

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

405 
end; 
17618  406 

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

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

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

409 
(*  *) 
17618  410 

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

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

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

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

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

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

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

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

418 

32232  419 
fun rawsat_tac ctxt i = 
32432
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32283
diff
changeset

420 
Subgoal.FOCUS (fn {context = ctxt', prems, ...} => 
64f30bdd3ba1
modernized messages  eliminated ctyp/cterm operations;
wenzelm
parents:
32283
diff
changeset

421 
rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i; 
17618  422 

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

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

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

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

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

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

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

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

430 
(* "!!" 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

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

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

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

434 

23533  435 
val pre_cnf_tac = 
436 
rtac ccontr THEN' 

35625  437 
Object_Logic.atomize_prems_tac THEN' 
23533  438 
CONVERSION Drule.beta_eta_conversion; 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

439 

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

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

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

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

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

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

445 
(*  *) 
17697  446 

32232  447 
fun cnfsat_tac ctxt i = 
448 
(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i); 

17618  449 

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

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

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

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

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

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

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

456 

32232  457 
fun cnfxsat_tac ctxt i = 
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 
(etac FalseE i) ORELSE 
32232  459 
(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i); 
17618  460 

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

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

464 
(* an exponential blowup. *) 
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 

32232  467 
fun sat_tac ctxt i = 
468 
pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i; 

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

469 

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

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

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

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

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

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

475 

32232  476 
fun satx_tac ctxt i = 
477 
pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i; 

17618  478 

23533  479 
end; 