author  webertj 
Thu, 31 Aug 2006 02:59:08 +0200  
changeset 20442  04621ea9440e 
parent 17809  195045659c06 
child 22441  7da872d34ace 
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 

20442  38 
(* propositional representation of HOL terms *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

39 
val prop_formula_of_term : Term.term > int Termtab.table > prop_formula * int Termtab.table 
20442  40 
(* HOL term representation of propositional formulae *) 
41 
val term_of_prop_formula : prop_formula > Term.term 

14452  42 
end; 
43 

44 
structure PropLogic : PROP_LOGIC = 

45 
struct 

46 

47 
(*  *) 

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

51 
(*  *) 

52 

53 
datatype prop_formula = 

54 
True 

55 
 False 

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

57 
 Not of prop_formula 

58 
 Or of prop_formula * prop_formula 

59 
 And of prop_formula * prop_formula; 

60 

61 
(*  *) 

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

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

64 
(* perform doublenegation elimination. *) 

65 
(*  *) 

66 

67 
(* prop_formula > prop_formula *) 

68 

69 
fun SNot True = False 

70 
 SNot False = True 

71 
 SNot (Not fm) = fm 

72 
 SNot fm = Not fm; 

73 

74 
(* prop_formula * prop_formula > prop_formula *) 

75 

76 
fun SOr (True, _) = True 

77 
 SOr (_, True) = True 

78 
 SOr (False, fm) = fm 

79 
 SOr (fm, False) = fm 

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

81 

82 
(* prop_formula * prop_formula > prop_formula *) 

83 

84 
fun SAnd (True, fm) = fm 

85 
 SAnd (fm, True) = fm 

86 
 SAnd (False, _) = False 

87 
 SAnd (_, False) = False 

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

89 

90 
(*  *) 

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

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

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

93 
(*  *) 
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 
(* prop_formula > prop_formula *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

96 

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

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

98 
 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

99 
 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

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

101 

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

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

106 

107 
(* prop_formula > int list *) 

108 

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

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

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

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

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

113 
 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

114 
 indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2); 
14452  115 

116 
(*  *) 

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

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

119 
(*  *) 

120 

121 
(* prop_formula > int *) 

122 

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

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

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

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

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

127 
 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

128 
 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

129 

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

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

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

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

133 
(*  *) 
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 
(* prop_formula list > prop_formula *) 
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 
fun exists xs = Library.foldl SOr (False, xs); 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

138 

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

141 
(*  *) 
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 
(* prop_formula list > prop_formula *) 
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 
fun all xs = Library.foldl SAnd (True, xs); 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

146 

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

149 
(*  *) 
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 
(* prop_formula list * prop_formula list > prop_formula *) 
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

152 

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

153 
fun dot_product (xs,ys) = exists (map SAnd (xs~~ys)); 
14452  154 

155 
(*  *) 

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

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

158 
(* Simplification (c.f. 'simplify') is performed as well. *) 
14452  159 
(*  *) 
160 

161 
(* prop_formula > prop_formula *) 

162 

163 
fun 

164 
(* constants *) 

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

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

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

168 
 nnf (BoolVar i) = (BoolVar i) 
14452  169 
(* '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

170 
 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

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

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

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

176 
 nnf (Not (BoolVar i)) = Not (BoolVar i) 
14452  177 
(* 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

178 
 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

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

181 
 nnf (Not (Not fm)) = nnf fm; 
14452  182 

183 
(*  *) 

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

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

14452  187 
(*  *) 
188 

189 
(* prop_formula > prop_formula *) 

190 

191 
fun cnf fm = 

192 
let 

193 
fun 

194 
(* constants *) 

14939  195 
cnf_from_nnf True = True 
196 
 cnf_from_nnf False = False 

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

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

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

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

207 
(* neither subformula contains 'and' *) 

208 
 cnf_or (fm1, fm2) = 

209 
Or (fm1, fm2) 

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

14939  214 
 cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2) 
14452  215 
in 
216 
(cnf_from_nnf o nnf) fm 

217 
end; 

218 

219 
(*  *) 

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

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

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

16907  224 
(* 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

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

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

227 
(* aux)". *) 
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 

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

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

231 
(* Note: 'auxcnf' tends to use fewer variables and fewer clauses than *) 
16913  232 
(* '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

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

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

14452  237 
(*  *) 
238 

239 
(* prop_formula > prop_formula *) 

240 

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

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

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

248 
(* unit > int *) 

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

250 
(* prop_formula > prop_formula *) 

14452  251 
fun 
252 
(* constants *) 

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

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

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

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

257 
 auxcnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *) 
14939  258 
(* 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

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

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

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

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

267 
BoolVar _ => 

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 
 Not _ => 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

270 
And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2)) 
14964  271 
 _ => 
272 
let 

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

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

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

280 
BoolVar _ => 

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 
 Not _ => 
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

283 
And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22)) 
14964  284 
 _ => 
285 
let 

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

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

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

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

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

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

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

300 
auxcnf_from_nnf fm' 
14452  301 
end; 
302 

303 
(*  *) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

320 
(* AND (NOT aux2 OR NOT a OR NOT b) *) 
14452  321 
(*  *) 
322 

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

323 
(* prop_formula > prop_formula *) 
14452  324 

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

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

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

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

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

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

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

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

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

333 
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

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

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

336 
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

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

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

339 
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

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

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

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

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

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

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

346 
 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

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

348 
 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

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

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

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

352 
 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

367 
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

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

369 
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

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

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

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

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

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

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

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

377 
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

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

379 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

413 
end; 
14452  414 

415 
(*  *) 

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

419 

420 
(* (int > bool) > prop_formula > bool *) 

421 

422 
fun eval a True = true 

423 
 eval a False = false 

424 
 eval a (BoolVar i) = (a i) 

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

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

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

428 

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

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

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

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

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

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

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

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

436 

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

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

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

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

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

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

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

443 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

490 

20442  491 
(*  *) 
492 
(* term_of_prop_formula: returns a HOL term that corresponds to a *) 

493 
(* propositional formula, with Boolean variables replaced by Free's *) 

494 
(*  *) 

495 

496 
(* Note: A more generic implementation should take another argument of type *) 

497 
(* Term.term Inttab.table (or so) that specifies HOL terms for some *) 

498 
(* Boolean variables in the formula, similar to 'prop_formula_of_term' *) 

499 
(* (but the other way round). *) 

500 

501 
(* prop_formula > Term.term *) 

502 
fun term_of_prop_formula True = 

503 
HOLogic.true_const 

504 
 term_of_prop_formula False = 

505 
HOLogic.false_const 

506 
 term_of_prop_formula (BoolVar i) = 

507 
Free ("v" ^ Int.toString i, HOLogic.boolT) 

508 
 term_of_prop_formula (Not fm) = 

509 
HOLogic.mk_not (term_of_prop_formula fm) 

510 
 term_of_prop_formula (Or (fm1, fm2)) = 

511 
HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2) 

512 
 term_of_prop_formula (And (fm1, fm2)) = 

513 
HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2); 

514 

14452  515 
end; 