author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 22441  7da872d34ace 
child 31220  f1c0ed85a33b 
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 

22441
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

31 
val is_nnf : prop_formula > bool (* returns true iff the formula is in negation normal form *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

32 
val is_cnf : prop_formula > bool (* returns true iff the formula is in conjunctive normal form *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

33 

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

34 
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

35 
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

36 
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

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

38 

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

40 

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

42 
val prop_formula_of_term : Term.term > int Termtab.table > prop_formula * int Termtab.table 
20442  43 
(* HOL term representation of propositional formulae *) 
44 
val term_of_prop_formula : prop_formula > Term.term 

14452  45 
end; 
46 

47 
structure PropLogic : PROP_LOGIC = 

48 
struct 

49 

50 
(*  *) 

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

54 
(*  *) 

55 

56 
datatype prop_formula = 

57 
True 

58 
 False 

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

60 
 Not of prop_formula 

61 
 Or of prop_formula * prop_formula 

62 
 And of prop_formula * prop_formula; 

63 

64 
(*  *) 

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

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

67 
(* perform doublenegation elimination. *) 

68 
(*  *) 

69 

70 
(* prop_formula > prop_formula *) 

71 

72 
fun SNot True = False 

73 
 SNot False = True 

74 
 SNot (Not fm) = fm 

75 
 SNot fm = Not fm; 

76 

77 
(* prop_formula * prop_formula > prop_formula *) 

78 

79 
fun SOr (True, _) = True 

80 
 SOr (_, True) = True 

81 
 SOr (False, fm) = fm 

82 
 SOr (fm, False) = fm 

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

84 

85 
(* prop_formula * prop_formula > prop_formula *) 

86 

87 
fun SAnd (True, fm) = fm 

88 
 SAnd (fm, True) = fm 

89 
 SAnd (False, _) = False 

90 
 SAnd (_, False) = False 

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

92 

93 
(*  *) 

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

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

95 
(* negation *) 
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 

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

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

101 
 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

102 
 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

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

104 

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

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

109 

110 
(* prop_formula > int list *) 

111 

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

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

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

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

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

116 
 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

117 
 indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2); 
14452  118 

119 
(*  *) 

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

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

122 
(*  *) 

123 

124 
(* prop_formula > int *) 

125 

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

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

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

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

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

130 
 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

131 
 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

132 

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

135 
(* formulas *) 
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 
(* prop_formula list > prop_formula *) 
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 
fun exists xs = Library.foldl SOr (False, xs); 
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 
(* 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

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 
(* prop_formula list > prop_formula *) 
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 
fun all xs = Library.foldl SAnd (True, xs); 
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 
(* 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

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

153 

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

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

155 

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

156 
fun dot_product (xs,ys) = exists (map SAnd (xs~~ys)); 
14452  157 

158 
(*  *) 

22441
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

159 
(* is_nnf: returns 'true' iff the formula is in negation normal form (i.e. *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

160 
(* only variables may be negated, but not subformulas). *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

161 
(*  *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

162 

7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

163 
local 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

164 
fun is_literal (BoolVar _) = true 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

165 
 is_literal (Not (BoolVar _)) = true 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

166 
 is_literal _ = false 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

167 
fun is_conj_disj (Or (fm1, fm2)) = 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

168 
is_conj_disj fm1 andalso is_conj_disj fm2 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

169 
 is_conj_disj (And (fm1, fm2)) = 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

170 
is_conj_disj fm1 andalso is_conj_disj fm2 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

171 
 is_conj_disj fm = 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

172 
is_literal fm 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

173 
in 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

174 
fun is_nnf True = true 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

175 
 is_nnf False = true 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

176 
 is_nnf fm = is_conj_disj fm 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

177 
end; 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

178 

7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

179 
(*  *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

180 
(* is_cnf: returns 'true' iff the formula is in conjunctive normal form *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

181 
(* (i.e. a conjunction of disjunctions). *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

182 
(*  *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

183 

7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

184 
local 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

185 
fun is_literal (BoolVar _) = true 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

186 
 is_literal (Not (BoolVar _)) = true 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

187 
 is_literal _ = false 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

188 
fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

189 
 is_disj fm = is_literal fm 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

190 
fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

191 
 is_conj fm = is_disj fm 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

192 
in 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

193 
fun is_cnf True = true 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

194 
 is_cnf False = true 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

195 
 is_cnf fm = is_conj fm 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

196 
end; 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

197 

7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

198 
(*  *) 
14452  199 
(* 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

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

201 
(* Simplification (c.f. 'simplify') is performed as well. *) 
14452  202 
(*  *) 
203 

204 
(* prop_formula > prop_formula *) 

205 

206 
fun 

207 
(* constants *) 

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

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

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

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

213 
 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

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

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

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

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

221 
 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

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

224 
 nnf (Not (Not fm)) = nnf fm; 
14452  225 

226 
(*  *) 

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

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

14452  230 
(*  *) 
231 

232 
(* prop_formula > prop_formula *) 

233 

234 
fun cnf fm = 

235 
let 

236 
fun 

237 
(* constants *) 

14939  238 
cnf_from_nnf True = True 
239 
 cnf_from_nnf False = False 

14452  240 
(* literals *) 
14939  241 
 cnf_from_nnf (BoolVar i) = BoolVar i 
242 
 cnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *) 

14452  243 
(* pushing 'or' inside of 'and' using distributive laws *) 
14939  244 
 cnf_from_nnf (Or (fm1, fm2)) = 
14452  245 
let 
14939  246 
fun cnf_or (And (fm11, fm12), fm2) = 
247 
And (cnf_or (fm11, fm2), cnf_or (fm12, fm2)) 

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

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

250 
(* neither subformula contains 'and' *) 

251 
 cnf_or (fm1, fm2) = 

252 
Or (fm1, fm2) 

14452  253 
in 
14939  254 
cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2) 
14452  255 
end 
256 
(* 'and' as outermost connective is left untouched *) 

14939  257 
 cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2) 
14452  258 
in 
259 
(cnf_from_nnf o nnf) fm 

260 
end; 

261 

262 
(*  *) 

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

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

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

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

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

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

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

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

272 

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

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

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

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

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

14452  280 
(*  *) 
281 

282 
(* prop_formula > prop_formula *) 

283 

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

284 
fun auxcnf fm = 
14452  285 
let 
16907  286 
(* convert formula to NNF first *) 
287 
val fm' = nnf fm 

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

291 
(* unit > int *) 

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

293 
(* prop_formula > prop_formula *) 

14452  294 
fun 
295 
(* constants *) 

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

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

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

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

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

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

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

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

307 
fun auxcnf_or (And (fm11, fm12), fm2) = 
14964  308 
(case fm2 of 
309 
(* do not introduce an auxiliary variable for literals *) 

310 
BoolVar _ => 

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

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

313 
And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2)) 
14964  314 
 _ => 
315 
let 

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

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

320 
 auxcnf_or (fm1, And (fm21, fm22)) = 
14964  321 
(case fm1 of 
322 
(* do not introduce an auxiliary variable for literals *) 

323 
BoolVar _ => 

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

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

326 
And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22)) 
14964  327 
 _ => 
328 
let 

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

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

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

337 
auxcnf_or (fm1', fm2') 
14452  338 
end 
339 
(* 'and' as outermost connective is left untouched *) 

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

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

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

343 
auxcnf_from_nnf fm' 
14452  344 
end; 
345 

346 
(*  *) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

363 
(* AND (NOT aux2 OR NOT a OR NOT b) *) 
14452  364 
(*  *) 
365 

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

366 
(* prop_formula > prop_formula *) 
14452  367 

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

368 
fun defcnf fm = 
22441
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

369 
if is_cnf fm then 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

370 
fm 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

371 
else let 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

372 
(* simplify formula first *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

373 
val fm' = simplify fm 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

374 
(* 'new' specifies the next index that is available to introduce an auxiliary variable *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

375 
(* int ref *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

376 
val new = ref (maxidx fm' + 1) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

377 
(* unit > int *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

378 
fun new_idx () = let val idx = !new in new := idx+1; idx end 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

379 
(* optimization for nary disjunction/conjunction *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

380 
(* prop_formula > prop_formula list *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

381 
fun disjuncts (Or (fm1, fm2)) = (disjuncts fm1) @ (disjuncts fm2) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

382 
 disjuncts fm1 = [fm1] 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

383 
(* prop_formula > prop_formula list *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

384 
fun conjuncts (And (fm1, fm2)) = (conjuncts fm1) @ (conjuncts fm2) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

385 
 conjuncts fm1 = [fm1] 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

386 
(* polarity > formula > (defining clauses, literal) *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

387 
(* bool > prop_formula > prop_formula * prop_formula *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

388 
fun 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

389 
(* constants *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

390 
defcnf' true True = (True, True) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

391 
 defcnf' false True = (*(True, False)*) error "formula is not simplified, True occurs with negative polarity" 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

392 
 defcnf' true False = (True, False) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

393 
 defcnf' false False = (*(True, True)*) error "formula is not simplified, False occurs with negative polarity" 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

394 
(* literals *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

395 
 defcnf' true (BoolVar i) = (True, BoolVar i) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

396 
 defcnf' false (BoolVar i) = (True, Not (BoolVar i)) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

397 
 defcnf' true (Not (BoolVar i)) = (True, Not (BoolVar i)) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

398 
 defcnf' false (Not (BoolVar i)) = (True, BoolVar i) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

399 
(* 'not' *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

400 
 defcnf' polarity (Not fm1) = 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

401 
let 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

402 
val (def1, aux1) = defcnf' (not polarity) fm1 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

403 
val aux = BoolVar (new_idx ()) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

404 
val def = Or (Not aux, aux1) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

405 
in 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

406 
(SAnd (def1, def), aux) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

407 
end 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

408 
(* 'or' *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

409 
 defcnf' polarity (Or (fm1, fm2)) = 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

410 
let 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

411 
val fms = disjuncts (Or (fm1, fm2)) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

412 
val (defs, auxs) = split_list (map (defcnf' polarity) fms) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

413 
val aux = BoolVar (new_idx ()) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

414 
val def = if polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

415 
in 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

416 
(SAnd (all defs, def), aux) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

417 
end 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

418 
(* 'and' *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

419 
 defcnf' polarity (And (fm1, fm2)) = 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

420 
let 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

421 
val fms = conjuncts (And (fm1, fm2)) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

422 
val (defs, auxs) = split_list (map (defcnf' polarity) fms) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

423 
val aux = BoolVar (new_idx ()) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

424 
val def = if not polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

425 
in 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

426 
(SAnd (all defs, def), aux) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

427 
end 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

428 
(* optimization: do not introduce auxiliary variables for parts of the formula that are in CNF already *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

429 
(* prop_formula > prop_formula * prop_formula *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

430 
fun defcnf_or (Or (fm1, fm2)) = 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

431 
let 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

432 
val (def1, aux1) = defcnf_or fm1 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

433 
val (def2, aux2) = defcnf_or fm2 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

434 
in 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

435 
(SAnd (def1, def2), Or (aux1, aux2)) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

436 
end 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

437 
 defcnf_or fm = 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

438 
defcnf' true fm 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

439 
(* prop_formula > prop_formula * prop_formula *) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

440 
fun defcnf_and (And (fm1, fm2)) = 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

441 
let 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

442 
val (def1, aux1) = defcnf_and fm1 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

443 
val (def2, aux2) = defcnf_and fm2 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

444 
in 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

445 
(SAnd (def1, def2), And (aux1, aux2)) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

446 
end 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

447 
 defcnf_and (Or (fm1, fm2)) = 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

448 
let 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

449 
val (def1, aux1) = defcnf_or fm1 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

450 
val (def2, aux2) = defcnf_or fm2 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

451 
in 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

452 
(SAnd (def1, def2), Or (aux1, aux2)) 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

453 
end 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

454 
 defcnf_and fm = 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

455 
defcnf' true fm 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

456 
in 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

457 
SAnd (defcnf_and fm') 
7da872d34ace
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents:
20442
diff
changeset

458 
end; 
14452  459 

460 
(*  *) 

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

464 

465 
(* (int > bool) > prop_formula > bool *) 

466 

467 
fun eval a True = true 

468 
 eval a False = false 

469 
 eval a (BoolVar i) = (a i) 

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

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

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

473 

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

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

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

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

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

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

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

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

481 

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

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

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

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

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

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

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

488 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

535 

20442  536 
(*  *) 
537 
(* term_of_prop_formula: returns a HOL term that corresponds to a *) 

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

539 
(*  *) 

540 

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

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

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

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

545 

546 
(* prop_formula > Term.term *) 

547 
fun term_of_prop_formula True = 

548 
HOLogic.true_const 

549 
 term_of_prop_formula False = 

550 
HOLogic.false_const 

551 
 term_of_prop_formula (BoolVar i) = 

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

553 
 term_of_prop_formula (Not fm) = 

554 
HOLogic.mk_not (term_of_prop_formula fm) 

555 
 term_of_prop_formula (Or (fm1, fm2)) = 

556 
HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2) 

557 
 term_of_prop_formula (And (fm1, fm2)) = 

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

559 

14452  560 
end; 