author  webertj 
Wed, 06 Sep 2006 17:39:52 +0200  
changeset 20486  02ca20e33030 
parent 20464  2b3fc1459ffa 
child 21267  5294ecae6708 
permissions  rwrr 
17618  1 
(* Title: HOL/Tools/sat_funcs.ML 
2 
ID: $Id$ 

3 
Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) 

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

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

5 
Copyright 20052006 
17618  6 

7 

8 
Proof reconstruction from SAT solvers. 

9 

10 
Description: 

11 
This file defines several tactics to invoke a proofproducing 

12 
SAT solver on a propositional goal in clausal form. 

13 

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

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

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

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

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

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

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

21 
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

22 

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

23 
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

24 
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

25 
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

26 
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

27 
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

28 
in Isabelle and thus solves the overall goal. 
17618  29 

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

30 
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

31 
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

32 
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

33 
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

34 
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

35 
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

36 
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

37 
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

38 
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

39 
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

40 
where each Ci is a disjunction. 
17618  41 

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

42 
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

43 
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

44 
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

45 
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

46 

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

47 
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

48 
"!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

49 
negation to be unsatisfiable) is proved via an oracle. 
17618  50 
*) 
51 

52 
signature SAT = 

53 
sig 

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

54 
val trace_sat : bool ref (* print trace messages *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

55 
val solver : string ref (* name of SAT solver to be used *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

56 
val counter : int ref (* number of resolution steps during last proof replay *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

57 
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

58 
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

59 
val satx_tac : int > Tactical.tactic 
17618  60 
end 
61 

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

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

63 
struct 
17618  64 

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

65 
val trace_sat = ref false; 
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

66 

20170  67 
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

68 

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

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

70 

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

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

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

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

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

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

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

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

78 
Thm.instantiate ([], [(cterm Q, cterm False)]) case_split_thm 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

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

80 

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

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

82 
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

83 

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

84 
(*  *) 
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 
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 
 ORIG_CLAUSE of Thm.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

96 
 RAW_CLAUSE of Thm.thm * Thm.cterm Inttab.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

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

114 
(* Each clause is accompanied with a table mapping integers (positive *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

115 
(* for positive literals, negative for negative literals, and the same *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

116 
(* absolute value for dual literals) to the actual literals as cterms. *) 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

117 
(*  *) 
17618  118 

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

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

120 

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

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

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

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

124 
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

125 
(* find out which two hyps are used in the resolution *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

126 
local exception RESULT of int * Thm.cterm * Thm.cterm 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

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

128 
fun find_res_hyps hyp1_table hyp2_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

129 
Inttab.fold (fn (i, hyp1) => fn () => 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

130 
case Inttab.lookup hyp2_table (~i) 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

131 
SOME hyp2 => raise RESULT (i, hyp1, hyp2) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

132 
 NONE => ()) hyp1_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

133 
raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

134 
) handle RESULT x => x 
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 
end 
19976
aa35f8e27c73
comments fixed, minor optimization wrt. certifying terms
webertj
parents:
19553
diff
changeset

136 

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

137 
(* Thm.thm * Thm.cterm Inttab.table > Thm.thm * Thm.cterm Inttab.table > Thm.thm * Thm.cterm Inttab.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

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

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

140 
val _ = if !trace_sat then 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

141 
tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ string_of_list (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1)) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

142 
^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ string_of_list (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")") 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

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

144 

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

145 
(* the two literals used for resolution *) 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

146 
val (i1, hyp1, hyp2) = find_res_hyps hyp1_table hyp2_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

147 
val hyp1_is_neg = i1 < 0 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

148 

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

149 
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

150 
val c2' = Thm.implies_intr hyp2 c2 (* Gamma2  hyp2 ==> False *) 
17618  151 

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

152 
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

153 
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

154 
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

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

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

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

158 

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

159 
val _ = if !trace_sat then 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

160 
tracing ("Resolution theorem: " ^ string_of_thm res_thm) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

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

162 

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

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

164 
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

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

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

167 

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 
(* since the mapping from integers to literals should be injective *) 
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 
(* (over different clauses), 'K true' here should be equivalent to *) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

170 
(* 'op=' (but slightly faster) *) 
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 hypnew_table = Inttab.merge (K true) (Inttab.delete i1 hyp1_table, Inttab.delete (~i1) hyp2_table) 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17843
diff
changeset

172 

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

173 
val _ = if !trace_sat then 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

174 
tracing ("Resulting clause: " ^ string_of_thm c_new ^ " (hyps: " ^ string_of_list (Sign.string_of_term (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

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

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

177 
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

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

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

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

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

182 
end; 
17618  183 

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

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

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

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

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

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

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

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

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

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

193 

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

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

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

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

197 
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

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

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

200 
case (HOLogic.dest_Trueprop o term_of) chyp 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

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

202 
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

203 
 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

204 
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

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

206 

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 
(* int > Thm.thm * Thm.cterm Inttab.table *) 
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
diff
changeset

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

209 
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

210 
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

211 
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

212 
 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

213 
(* convert the original clause *) 
17623
ae4af66b3072
replay_proof optimized: now performs backwards proof search
webertj
parents:
17622
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 
val _ = if !trace_sat then tracing ("Using original 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

216 
val raw = cnf.clause2raw_thm 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

217 
val lit_table = fold (fn chyp => fn lit_table => (case index_of_literal chyp 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

218 
SOME i => Inttab.update_new (i, chyp) lit_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

219 
 NONE => lit_table)) (#hyps (Thm.crep_thm raw)) Inttab.empty 
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 
val clause = (raw, lit_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

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

222 
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

223 
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

224 
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

225 
 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

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

227 
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

228 
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

229 
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

230 
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

231 
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

232 
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

233 
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

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

235 
end 
17618  236 

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

237 
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

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

239 
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

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

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

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

243 

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

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

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

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

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

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

250 

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

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

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

253 
 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

254 
 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

255 
 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

256 
 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

257 

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

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

259 
(* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

260 
(* a proof from the resulting proof trace of the SAT solver. Each *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

261 
(* premise in 'prems' that is not a clause is ignored, and the theorem *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

262 
(* returned is just "False" (with some clauses as hyps). *) 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

263 
(*  *) 
17618  264 

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

265 
(* Thm.thm list > Thm.thm *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

266 

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

267 
fun rawsat_thm prems = 
17622
5d03a69481b6
code reformatted and restructured, many minor modifications
webertj
parents:
17618
diff
changeset

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

269 
(* remove premises that equal "True" *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

270 
val non_triv_prems = filter (fn thm => 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

271 
(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o prop_of) thm 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

272 
handle TERM ("dest_Trueprop", _) => true) prems 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

273 
(* remove nonclausal premises  of course this shouldn't actually *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

274 
(* remove anything as long as 'rawsat_thm' is only called after the *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

275 
(* premises have been converted to clauses *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

276 
val clauses = filter (fn thm => 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

277 
((cnf.is_clause o HOLogic.dest_Trueprop o prop_of) thm handle TERM ("dest_Trueprop", _) => false) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

278 
orelse (warning ("Ignoring nonclausal premise " ^ (string_of_cterm o cprop_of) thm); false)) non_triv_prems 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

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

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

281 
(* numbering would be off *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

282 
val non_triv_clauses = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o prop_of) clauses 
19534  283 
val _ = if !trace_sat then 
284 
tracing ("Nontrivial clauses:\n" ^ space_implode "\n" (map (string_of_cterm o cprop_of) non_triv_clauses)) 

285 
else () 

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

286 
(* translate clauses from HOL terms to PropLogic.prop_formula *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

287 
val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o prop_of) non_triv_clauses Termtab.empty 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

288 
val _ = if !trace_sat then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

289 
tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms)) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

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

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

292 
(* unit > Thm.thm *) 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

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

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

295 
tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead." 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

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

297 
(* of course just returning "False" is unsound; what we should return *) 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

298 
(* instead is "False" with all 'non_triv_clauses' as hyps  but this *) 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

299 
(* might be rather slow, and it makes no real difference as long as *) 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

300 
(* 'rawsat_thm' is only called from 'rawsat_tac' *) 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

301 
SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const) 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

302 
) 
17618  303 
in 
20039
4293f932fe83
"solver" reference added to make the SAT solver configurable
webertj
parents:
19976
diff
changeset

304 
case SatSolver.invoke_solver (!solver) fm of 
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

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

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

307 
tracing ("Proof trace from SAT solver:\n" ^ 
20371  308 
"clauses: " ^ string_of_list (string_of_pair string_of_int (string_of_list string_of_int)) (Inttab.dest clause_table) ^ "\n" ^ 
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

309 
"empty clause: " ^ string_of_int empty_id) 
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

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

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

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

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

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

315 
(* optimization: convert the given clauses from "[c_i]  c_i" to *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

316 
(* "[c_1 && ... && c_n]  c_i"; this avoids accumulation of *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

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

318 
(* [c_1 && ... && c_n]  c_1 && ... && c_n *) 
20486
02ca20e33030
rawsat_thm: mk_conjunction_list replaced by Conjunction.mk_conjunction_list
webertj
parents:
20464
diff
changeset

319 
val cnf_cterm = Conjunction.mk_conjunction_list (map cprop_of non_triv_clauses) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

320 
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

321 
(* cf. Conjunction.elim_list *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

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

323 
let val (th1, th2) = Conjunction.elim th 
20464  324 
in th1 :: right_elim_list th2 end handle THM _ => [th] 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

325 
(* [[c_1 && ... && c_n]  c_1, ..., [c_1 && ... && c_n]  c_n] *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

326 
val converted_clauses = right_elim_list 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

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

328 
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

329 
val clause_arr = Array.array (max_idx + 1, NO_CLAUSE) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

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

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

332 
(* [c_1 && ... && c_n]  False *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

333 
val FalseThm = 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

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

335 
(* convert the &&hyp back to the original clauses format *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

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

337 
(* []  c_1 && ... && c_n ==> False *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

338 
> Thm.implies_intr cnf_cterm 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

339 
(* c_1 ==> ... ==> c_n ==> False *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

340 
> Conjunction.curry ~1 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

341 
(* [c_1, ..., c_n]  False *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

342 
> (fn thm => fold (fn cprem => fn thm' => 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
20371
diff
changeset

343 
Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm) 
17842
e661a78472f0
no proof reconstruction when quick_and_dirty is set
webertj
parents:
17809
diff
changeset

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

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

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

347 
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

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

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

350 
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

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

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

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

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

355 
o map (fn (term, idx) => 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

356 
Sign.string_of_term (the_context ()) term ^ ": " 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

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

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

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

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

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

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

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

364 
end; 
17618  365 

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

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

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

368 
(*  *) 
17618  369 

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

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

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

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

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

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

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

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

377 

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

378 
(* int > Tactical.tactic *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

379 

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

380 
fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm prems) 1) i; 
17618  381 

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

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

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

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

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

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

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

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

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

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

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

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

393 

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

394 
(* int > Tactical.tactic *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

395 

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

396 
fun pre_cnf_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

397 
rtac ccontr i THEN ObjectLogic.atomize_tac i THEN 
28be10991666
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
webertj
parents:
20170
diff
changeset

398 
PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (Drule.beta_eta_conversion))); 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

399 

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

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

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

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

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

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

405 
(*  *) 
17697  406 

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

407 
(* int > Tactical.tactic *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

408 

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

409 
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

410 
(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i); 
17618  411 

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

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

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

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

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

416 
(* then applies 'rawsat_tac' to solve the subgoal *) 
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 

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

419 
(* int > Tactical.tactic *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

420 

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

421 
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

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

423 
(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i); 
17618  424 

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

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

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

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

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

429 
(*  *) 
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 
(* int > Tactical.tactic *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

432 

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

433 
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

434 
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

435 

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

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

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

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

439 
(* introducing new literals. *) 
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 

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

442 
(* int > Tactical.tactic *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17697
diff
changeset

443 

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

444 
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

445 
pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i; 
17618  446 

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

447 
end; (* of structure SATFunc *) 