author  webertj 
Sun, 09 Oct 2005 17:06:03 +0200  
changeset 17809  195045659c06 
parent 16913  1d8a8d010e69 
child 20442  04621ea9440e 
permissions  rwrr 
14452  1 
(* Title: HOL/Tools/prop_logic.ML 
2 
ID: $Id$ 

3 
Author: Tjark Weber 

16907  4 
Copyright 20042005 
14452  5 

6 
Formulas of propositional logic. 

7 
*) 

8 

9 
signature PROP_LOGIC = 

10 
sig 

11 
datatype prop_formula = 

12 
True 

13 
 False 

14 
 BoolVar of int (* NOTE: only use indices >= 1 *) 

15 
 Not of prop_formula 

16 
 Or of prop_formula * prop_formula 

17 
 And of prop_formula * prop_formula 

18 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

19 
val SNot : prop_formula > prop_formula 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

20 
val SOr : prop_formula * prop_formula > prop_formula 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

21 
val SAnd : prop_formula * prop_formula > prop_formula 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

22 
val simplify : prop_formula > prop_formula (* eliminates True/False and doublenegation *) 
14452  23 

14681  24 
val indices : prop_formula > int list (* set of all variable indices *) 
15301  25 
val maxidx : prop_formula > int (* maximal variable index *) 
14452  26 

27 
val exists : prop_formula list > prop_formula (* finite disjunction *) 

28 
val all : prop_formula list > prop_formula (* finite conjunction *) 

29 
val dot_product : prop_formula list * prop_formula list > prop_formula 

30 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

31 
val nnf : prop_formula > prop_formula (* negation normal form *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

32 
val cnf : prop_formula > prop_formula (* conjunctive normal form *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

33 
val auxcnf : prop_formula > prop_formula (* cnf with auxiliary variables *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

34 
val defcnf : prop_formula > prop_formula (* definitional cnf *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

35 

14452  36 
val eval : (int > bool) > prop_formula > bool (* semantics *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

37 

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

38 
val prop_formula_of_term : Term.term > int Termtab.table > prop_formula * int Termtab.table 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

39 
(* propositional representation of HOL terms *) 
14452  40 
end; 
41 

42 
structure PropLogic : PROP_LOGIC = 

43 
struct 

44 

45 
(*  *) 

14753  46 
(* prop_formula: formulas of propositional logic, built from Boolean *) 
14452  47 
(* variables (referred to by index) and True/False using *) 
48 
(* not/or/and *) 

49 
(*  *) 

50 

51 
datatype prop_formula = 

52 
True 

53 
 False 

54 
 BoolVar of int (* NOTE: only use indices >= 1 *) 

55 
 Not of prop_formula 

56 
 Or of prop_formula * prop_formula 

57 
 And of prop_formula * prop_formula; 

58 

59 
(*  *) 

60 
(* The following constructor functions make sure that True and False do not *) 

61 
(* occur within any of the other connectives (i.e. Not, Or, And), and *) 

62 
(* perform doublenegation elimination. *) 

63 
(*  *) 

64 

65 
(* prop_formula > prop_formula *) 

66 

67 
fun SNot True = False 

68 
 SNot False = True 

69 
 SNot (Not fm) = fm 

70 
 SNot fm = Not fm; 

71 

72 
(* prop_formula * prop_formula > prop_formula *) 

73 

74 
fun SOr (True, _) = True 

75 
 SOr (_, True) = True 

76 
 SOr (False, fm) = fm 

77 
 SOr (fm, False) = fm 

78 
 SOr (fm1, fm2) = Or (fm1, fm2); 

79 

80 
(* prop_formula * prop_formula > prop_formula *) 

81 

82 
fun SAnd (True, fm) = fm 

83 
 SAnd (fm, True) = fm 

84 
 SAnd (False, _) = False 

85 
 SAnd (_, False) = False 

86 
 SAnd (fm1, fm2) = And (fm1, fm2); 

87 

88 
(*  *) 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

89 
(* simplify: eliminates True/False below other connectives, and double *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

90 
(* negation *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

91 
(*  *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

92 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

93 
(* prop_formula > prop_formula *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

94 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

95 
fun simplify (Not fm) = SNot (simplify fm) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

96 
 simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

97 
 simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

98 
 simplify fm = fm; 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

99 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

100 
(*  *) 
14753  101 
(* indices: collects all indices of Boolean variables that occur in a *) 
14452  102 
(* propositional formula 'fm'; no duplicates *) 
103 
(*  *) 

104 

105 
(* prop_formula > int list *) 

106 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

107 
fun indices True = [] 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

108 
 indices False = [] 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

109 
 indices (BoolVar i) = [i] 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

110 
 indices (Not fm) = indices fm 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

111 
 indices (Or (fm1, fm2)) = (indices fm1) union_int (indices fm2) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

112 
 indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2); 
14452  113 

114 
(*  *) 

115 
(* maxidx: computes the maximal variable index occuring in a formula of *) 

116 
(* propositional logic 'fm'; 0 if 'fm' contains no variable *) 

117 
(*  *) 

118 

119 
(* prop_formula > int *) 

120 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

121 
fun maxidx True = 0 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

122 
 maxidx False = 0 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

123 
 maxidx (BoolVar i) = i 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

124 
 maxidx (Not fm) = maxidx fm 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

125 
 maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

126 
 maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2); 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

127 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

128 
(*  *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

129 
(* exists: computes the disjunction over a list 'xs' of propositional *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

130 
(* formulas *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

131 
(*  *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

132 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

133 
(* prop_formula list > prop_formula *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

134 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

135 
fun exists xs = Library.foldl SOr (False, xs); 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

136 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

137 
(*  *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

138 
(* all: computes the conjunction over a list 'xs' of propositional formulas *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

139 
(*  *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

140 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

141 
(* prop_formula list > prop_formula *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

142 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

143 
fun all xs = Library.foldl SAnd (True, xs); 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

144 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

145 
(*  *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

146 
(* dot_product: ([x1,...,xn], [y1,...,yn]) > x1*y1+...+xn*yn *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

147 
(*  *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

148 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

149 
(* prop_formula list * prop_formula list > prop_formula *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

150 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

151 
fun dot_product (xs,ys) = exists (map SAnd (xs~~ys)); 
14452  152 

153 
(*  *) 

154 
(* nnf: computes the negation normal form of a formula 'fm' of propositional *) 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

155 
(* logic (i.e. only variables may be negated, but not subformulas). *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

156 
(* Simplification (c.f. 'simplify') is performed as well. *) 
14452  157 
(*  *) 
158 

159 
(* prop_formula > prop_formula *) 

160 

161 
fun 

162 
(* constants *) 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

163 
nnf True = True 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

164 
 nnf False = False 
14452  165 
(* variables *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

166 
 nnf (BoolVar i) = (BoolVar i) 
14452  167 
(* 'or' and 'and' as outermost connectives are left untouched *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

168 
 nnf (Or (fm1, fm2)) = SOr (nnf fm1, nnf fm2) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

169 
 nnf (And (fm1, fm2)) = SAnd (nnf fm1, nnf fm2) 
14452  170 
(* 'not' + constant *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

171 
 nnf (Not True) = False 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

172 
 nnf (Not False) = True 
14452  173 
(* 'not' + variable *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

174 
 nnf (Not (BoolVar i)) = Not (BoolVar i) 
14452  175 
(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

176 
 nnf (Not (Or (fm1, fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2)) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

177 
 nnf (Not (And (fm1, fm2))) = SOr (nnf (SNot fm1), nnf (SNot fm2)) 
14452  178 
(* doublenegation elimination *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

179 
 nnf (Not (Not fm)) = nnf fm; 
14452  180 

181 
(*  *) 

14681  182 
(* cnf: computes the conjunctive normal form (i.e. a conjunction of *) 
183 
(* disjunctions) of a formula 'fm' of propositional logic. The result *) 

184 
(* formula may be exponentially longer than 'fm'. *) 

14452  185 
(*  *) 
186 

187 
(* prop_formula > prop_formula *) 

188 

189 
fun cnf fm = 

190 
let 

191 
fun 

192 
(* constants *) 

14939  193 
cnf_from_nnf True = True 
194 
 cnf_from_nnf False = False 

14452  195 
(* literals *) 
14939  196 
 cnf_from_nnf (BoolVar i) = BoolVar i 
197 
 cnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *) 

14452  198 
(* pushing 'or' inside of 'and' using distributive laws *) 
14939  199 
 cnf_from_nnf (Or (fm1, fm2)) = 
14452  200 
let 
14939  201 
fun cnf_or (And (fm11, fm12), fm2) = 
202 
And (cnf_or (fm11, fm2), cnf_or (fm12, fm2)) 

203 
 cnf_or (fm1, And (fm21, fm22)) = 

204 
And (cnf_or (fm1, fm21), cnf_or (fm1, fm22)) 

205 
(* neither subformula contains 'and' *) 

206 
 cnf_or (fm1, fm2) = 

207 
Or (fm1, fm2) 

14452  208 
in 
14939  209 
cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2) 
14452  210 
end 
211 
(* 'and' as outermost connective is left untouched *) 

14939  212 
 cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2) 
14452  213 
in 
214 
(cnf_from_nnf o nnf) fm 

215 
end; 

216 

217 
(*  *) 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

218 
(* auxcnf: computes the definitional conjunctive normal form of a formula *) 
14681  219 
(* 'fm' of propositional logic, introducing auxiliary variables if *) 
220 
(* necessary to avoid an exponential blowup of the formula. The result *) 

221 
(* formula is satisfiable if and only if 'fm' is satisfiable. *) 

16907  222 
(* Auxiliary variables are introduced as switches for ORnodes, based *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

223 
(* on the observation that e.g. "fm1 OR (fm21 AND fm22)" is *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

224 
(* equisatisfiable with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

225 
(* aux)". *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

226 
(*  *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

227 

acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

228 
(*  *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

229 
(* Note: 'auxcnf' tends to use fewer variables and fewer clauses than *) 
16913  230 
(* 'defcnf' below, but sometimes generates much larger SAT problems *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

231 
(* overall (hence it must sometimes generate longer clauses than *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

232 
(* 'defcnf' does). It is currently not quite clear to me if one of the *) 
16913  233 
(* algorithms is clearly superior to the other, but I suggest using *) 
234 
(* 'defcnf' instead. *) 

14452  235 
(*  *) 
236 

237 
(* prop_formula > prop_formula *) 

238 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

239 
fun auxcnf fm = 
14452  240 
let 
16907  241 
(* convert formula to NNF first *) 
242 
val fm' = nnf fm 

14452  243 
(* 'new' specifies the next index that is available to introduce an auxiliary variable *) 
16907  244 
(* int ref *) 
245 
val new = ref (maxidx fm' + 1) 

246 
(* unit > int *) 

247 
fun new_idx () = let val idx = !new in new := idx+1; idx end 

248 
(* prop_formula > prop_formula *) 

14452  249 
fun 
250 
(* constants *) 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

251 
auxcnf_from_nnf True = True 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

252 
 auxcnf_from_nnf False = False 
14452  253 
(* literals *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

254 
 auxcnf_from_nnf (BoolVar i) = BoolVar i 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

255 
 auxcnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *) 
14939  256 
(* pushing 'or' inside of 'and' using auxiliary variables *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

257 
 auxcnf_from_nnf (Or (fm1, fm2)) = 
14452  258 
let 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

259 
val fm1' = auxcnf_from_nnf fm1 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

260 
val fm2' = auxcnf_from_nnf fm2 
16907  261 
(* prop_formula * prop_formula > prop_formula *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

262 
fun auxcnf_or (And (fm11, fm12), fm2) = 
14964  263 
(case fm2 of 
264 
(* do not introduce an auxiliary variable for literals *) 

265 
BoolVar _ => 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

266 
And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2)) 
14964  267 
 Not _ => 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

268 
And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2)) 
14964  269 
 _ => 
270 
let 

16907  271 
val aux = BoolVar (new_idx ()) 
14964  272 
in 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

273 
And (And (auxcnf_or (fm11, aux), auxcnf_or (fm12, aux)), auxcnf_or (fm2, Not aux)) 
14964  274 
end) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

275 
 auxcnf_or (fm1, And (fm21, fm22)) = 
14964  276 
(case fm1 of 
277 
(* do not introduce an auxiliary variable for literals *) 

278 
BoolVar _ => 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

279 
And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22)) 
14964  280 
 Not _ => 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

281 
And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22)) 
14964  282 
 _ => 
283 
let 

16907  284 
val aux = BoolVar (new_idx ()) 
14964  285 
in 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

286 
And (auxcnf_or (fm1, Not aux), And (auxcnf_or (fm21, aux), auxcnf_or (fm22, aux))) 
14964  287 
end) 
14939  288 
(* neither subformula contains 'and' *) 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

289 
 auxcnf_or (fm1, fm2) = 
16907  290 
Or (fm1, fm2) 
14939  291 
in 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

292 
auxcnf_or (fm1', fm2') 
14452  293 
end 
294 
(* 'and' as outermost connective is left untouched *) 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

295 
 auxcnf_from_nnf (And (fm1, fm2)) = 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

296 
And (auxcnf_from_nnf fm1, auxcnf_from_nnf fm2) 
14452  297 
in 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

298 
auxcnf_from_nnf fm' 
14452  299 
end; 
300 

301 
(*  *) 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

302 
(* defcnf: computes the definitional conjunctive normal form of a formula *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

303 
(* 'fm' of propositional logic, introducing auxiliary variables to *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

304 
(* avoid an exponential blowup of the formula. The result formula is *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

305 
(* satisfiable if and only if 'fm' is satisfiable. Auxiliary variables *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

306 
(* are introduced as abbreviations for AND, OR, and NOTnodes, based *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

307 
(* on the following equisatisfiabilities (+/ indicates polarity): *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

308 
(* LITERAL+ == LITERAL *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

309 
(* LITERAL == NOT LITERAL *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

310 
(* (NOT fm1)+ == aux AND (NOT aux OR fm1) *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

311 
(* (fm1 OR fm2)+ == aux AND (NOT aux OR fm1+ OR fm2+) *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

312 
(* (fm1 AND fm2)+ == aux AND (NOT aux OR fm1+) AND (NOT aux OR fm2+) *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

313 
(* (NOT fm1) == aux AND (NOT aux OR fm1+) *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

314 
(* (fm1 OR fm2) == aux AND (NOT aux OR fm1) AND (NOT aux OR fm2) *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

315 
(* (fm1 AND fm2) == aux AND (NOT aux OR fm1 OR fm2) *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

316 
(* Example: *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

317 
(* NOT (a AND b) == aux1 AND (NOT aux1 OR aux2) *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

318 
(* AND (NOT aux2 OR NOT a OR NOT b) *) 
14452  319 
(*  *) 
320 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

321 
(* prop_formula > prop_formula *) 
14452  322 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

323 
fun defcnf fm = 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

324 
let 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

325 
(* simplify formula first *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

326 
val fm' = simplify fm 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

327 
(* 'new' specifies the next index that is available to introduce an auxiliary variable *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

328 
(* int ref *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

329 
val new = ref (maxidx fm' + 1) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

330 
(* unit > int *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

331 
fun new_idx () = let val idx = !new in new := idx+1; idx end 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

332 
(* optimization for nary disjunction/conjunction *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

333 
(* prop_formula > prop_formula list *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

334 
fun disjuncts (Or (fm1, fm2)) = (disjuncts fm1) @ (disjuncts fm2) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

335 
 disjuncts fm1 = [fm1] 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

336 
(* prop_formula > prop_formula list *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

337 
fun conjuncts (And (fm1, fm2)) = (conjuncts fm1) @ (conjuncts fm2) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

338 
 conjuncts fm1 = [fm1] 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

339 
(* polarity > formula > (defining clauses, literal) *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

340 
(* bool > prop_formula > prop_formula * prop_formula *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

341 
fun 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

342 
(* constants *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

343 
defcnf' true True = (True, True) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

344 
 defcnf' false True = (*(True, False)*) error "formula is not simplified, True occurs with negative polarity" 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

345 
 defcnf' true False = (True, False) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

346 
 defcnf' false False = (*(True, True)*) error "formula is not simplified, False occurs with negative polarity" 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

347 
(* literals *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

348 
 defcnf' true (BoolVar i) = (True, BoolVar i) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

349 
 defcnf' false (BoolVar i) = (True, Not (BoolVar i)) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

350 
 defcnf' true (Not (BoolVar i)) = (True, Not (BoolVar i)) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

351 
 defcnf' false (Not (BoolVar i)) = (True, BoolVar i) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

352 
(* 'not' *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

353 
 defcnf' polarity (Not fm1) = 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

354 
let 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

355 
val (def1, aux1) = defcnf' (not polarity) fm1 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

356 
val aux = BoolVar (new_idx ()) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

357 
val def = Or (Not aux, aux1) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

358 
in 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

359 
(SAnd (def1, def), aux) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

360 
end 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

361 
(* 'or' *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

362 
 defcnf' polarity (Or (fm1, fm2)) = 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

363 
let 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

364 
val fms = disjuncts (Or (fm1, fm2)) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

365 
val (defs, auxs) = split_list (map (defcnf' polarity) fms) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

366 
val aux = BoolVar (new_idx ()) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

367 
val def = if polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

368 
in 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

369 
(SAnd (all defs, def), aux) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

370 
end 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

371 
(* 'and' *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

372 
 defcnf' polarity (And (fm1, fm2)) = 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

373 
let 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

374 
val fms = conjuncts (And (fm1, fm2)) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

375 
val (defs, auxs) = split_list (map (defcnf' polarity) fms) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

376 
val aux = BoolVar (new_idx ()) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

377 
val def = if not polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

378 
in 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

379 
(SAnd (all defs, def), aux) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

380 
end 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

381 
(* optimization: do not introduce auxiliary variables for parts of the formula that are in CNF already *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

382 
(* prop_formula > prop_formula * prop_formula *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

383 
fun defcnf_or (Or (fm1, fm2)) = 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

384 
let 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

385 
val (def1, aux1) = defcnf_or fm1 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

386 
val (def2, aux2) = defcnf_or fm2 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

387 
in 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

388 
(SAnd (def1, def2), Or (aux1, aux2)) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

389 
end 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

390 
 defcnf_or fm = 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

391 
defcnf' true fm 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

392 
(* prop_formula > prop_formula * prop_formula *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

393 
fun defcnf_and (And (fm1, fm2)) = 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

394 
let 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

395 
val (def1, aux1) = defcnf_and fm1 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

396 
val (def2, aux2) = defcnf_and fm2 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

397 
in 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

398 
(SAnd (def1, def2), And (aux1, aux2)) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

399 
end 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

400 
 defcnf_and (Or (fm1, fm2)) = 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

401 
let 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

402 
val (def1, aux1) = defcnf_or fm1 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

403 
val (def2, aux2) = defcnf_or fm2 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

404 
in 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

405 
(SAnd (def1, def2), Or (aux1, aux2)) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

406 
end 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

407 
 defcnf_and fm = 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

408 
defcnf' true fm 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

409 
in 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

410 
SAnd (defcnf_and fm') 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

411 
end; 
14452  412 

413 
(*  *) 

14753  414 
(* eval: given an assignment 'a' of Boolean values to variable indices, the *) 
14452  415 
(* truth value of a propositional formula 'fm' is computed *) 
416 
(*  *) 

417 

418 
(* (int > bool) > prop_formula > bool *) 

419 

420 
fun eval a True = true 

421 
 eval a False = false 

422 
 eval a (BoolVar i) = (a i) 

423 
 eval a (Not fm) = not (eval a fm) 

424 
 eval a (Or (fm1,fm2)) = (eval a fm1) orelse (eval a fm2) 

425 
 eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2); 

426 

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

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

428 
(* prop_formula_of_term: returns the propositional structure of a HOL term, *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

429 
(* with subterms replaced by Boolean variables. Also returns a table *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

430 
(* of terms and corresponding variables that extends the table that was *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

431 
(* given as an argument. Usually, you'll just want to use *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

432 
(* 'Termtab.empty' as value for 'table'. *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

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

434 

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

435 
(* Note: The implementation is somewhat optimized; the next index to be used *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

436 
(* is computed only when it is actually needed. However, when *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

437 
(* 'prop_formula_of_term' is invoked many times, it might be more *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

438 
(* efficient to pass and return this value as an additional parameter, *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

439 
(* so that it does not have to be recomputed (by folding over the *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

440 
(* table) for each invocation. *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

441 

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

442 
(* Term.term > int Termtab.table > prop_formula * int Termtab.table *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

443 
fun prop_formula_of_term t table = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

444 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

445 
val next_idx_is_valid = ref false 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

446 
val next_idx = ref 0 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

447 
fun get_next_idx () = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

448 
if !next_idx_is_valid then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

449 
inc next_idx 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

450 
else ( 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

451 
next_idx := Termtab.fold (curry Int.max o snd) table 0; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

452 
next_idx_is_valid := true; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

453 
inc next_idx 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

454 
) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

455 
fun aux (Const ("True", _)) table = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

456 
(True, table) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

457 
 aux (Const ("False", _)) table = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

458 
(False, table) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

459 
 aux (Const ("Not", _) $ x) table = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

460 
apfst Not (aux x table) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

461 
 aux (Const ("op ", _) $ x $ y) table = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

462 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

463 
val (fm1, table1) = aux x table 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

464 
val (fm2, table2) = aux y table1 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

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

466 
(Or (fm1, fm2), table2) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

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

468 
 aux (Const ("op &", _) $ x $ y) table = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

469 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

470 
val (fm1, table1) = aux x table 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

471 
val (fm2, table2) = aux y table1 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

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

473 
(And (fm1, fm2), table2) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

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

475 
 aux x table = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

476 
(case Termtab.lookup table x of 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

477 
SOME i => 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

478 
(BoolVar i, table) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

479 
 NONE => 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

480 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

481 
val i = get_next_idx () 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

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

483 
(BoolVar i, Termtab.update (x, i) table) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

484 
end) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

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

486 
aux t table 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

487 
end; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

488 

14452  489 
end; 