Revision e3cf4ca2 src/lib/EAFormula.ml
src/lib/EAFormula.ml  

94  94 

95  95 
let gensym = Stream.from (fun i > Some (Printf.sprintf "#gensym%x#" i)) 
96  96  
97 
(* every nominal is translated to a fresh propositional atom *) 

98 
let formula1 f = 

99 
let nomsub = ref StringMap.empty in 

100 
let noms = ref [] in 

101 
let rec nom2EA_formula1 f = 

97 
let rename f nomsub noms = 

98 
let rec rename_formula1 f = 

102  99 
let name = Stream.next gensym in 
103  100 
match f with 
104 
 CoAlgFormula.FALSE > FALSE 

105 
 CoAlgFormula.TRUE > TRUE 

101 
 CoAlgFormula.FALSE > CoAlgFormula.FALSE


102 
 CoAlgFormula.TRUE > CoAlgFormula.TRUE


106  103 
 CoAlgFormula.AP s > 
107  104 
if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then noms := name :: !noms; 
108  105 
if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then nomsub := StringMap.add s name !nomsub; 
109 
if (CoAlgFormula.isNominal s) then AP (StringMap.find s !nomsub) 

110 
else AP s 

106 
if (CoAlgFormula.isNominal s) then CoAlgFormula.AP (StringMap.find s !nomsub) 

107 
else CoAlgFormula.AP s 

108 
 CoAlgFormula.NOT f > CoAlgFormula.NOT (rename_formula1 f) 

109 
 CoAlgFormula.OR (f1, f2) > CoAlgFormula.OR ((rename_formula1 f1), (rename_formula1 f2)) 

110 
 CoAlgFormula.AND (f1, f2) > CoAlgFormula.AND ((rename_formula1 f1), (rename_formula1 f2)) 

111 
 CoAlgFormula.EQU (f1, f2) > CoAlgFormula.EQU ((rename_formula1 f1), (rename_formula1 f2)) 

112 
 CoAlgFormula.IMP (f1, f2) > CoAlgFormula.IMP ((rename_formula1 f1), (rename_formula1 f2)) 

113 
 CoAlgFormula.EX (s, f) > CoAlgFormula.EX (s, (rename_formula1 f)) 

114 
 CoAlgFormula.AX (s, f) > CoAlgFormula.AX (s, (rename_formula1 f)) 

115 
 CoAlgFormula.ID f > CoAlgFormula.ID (rename_formula1 f) 

116 
 CoAlgFormula.MU (s, f) > CoAlgFormula.MU (s, (rename_formula1 f)) 

117 
 CoAlgFormula.NU (s, f) > CoAlgFormula.NU (s, (rename_formula1 f)) 

118 
 CoAlgFormula.AF f > CoAlgFormula.AF (rename_formula1 f) 

119 
 CoAlgFormula.EF f > CoAlgFormula.EF (rename_formula1 f) 

120 
 CoAlgFormula.AG f > CoAlgFormula.AG (rename_formula1 f) 

121 
 CoAlgFormula.EG f > CoAlgFormula.EG (rename_formula1 f) 

122 
in 

123 
rename_formula1 f 

124  
125  
126 
let coalgtoea f = 

127 
let rec nom2EA_formula1 f = 

128 
match f with 

129 
 CoAlgFormula.FALSE > FALSE 

130 
 CoAlgFormula.TRUE > TRUE 

131 
 CoAlgFormula.AP s > AP s 

111  132 
 CoAlgFormula.NOT f > NOT (nom2EA_formula1 f) 
112  133 
 CoAlgFormula.OR (f1, f2) > OR ((nom2EA_formula1 f1), (nom2EA_formula1 f2)) 
113  134 
 CoAlgFormula.AND (f1, f2) > AND ((nom2EA_formula1 f1), (nom2EA_formula1 f2)) 
...  ...  
123  144 
 CoAlgFormula.AG f > AG (nom2EA_formula1 f) 
124  145 
 CoAlgFormula.EG f > EG (nom2EA_formula1 f) 
125  146 
in 
126 
(noms, (nom2EA_formula1 f))


147 
nom2EA_formula1 f


127  148  
128  149 
let formula2 f noms nomTbl sorts = 
129  150 
let card = Array.length sorts in 
...  ...  
139  160 
CoAlgMisc.sortTable := Array.copy sorts; 
140  161 
CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform; 
141  162  
163 
let hashedformulaList = ref [] in 

164 
CoAlgFormula.HcFHt.iter (fun k v > hashedformulaList := k :: (!hashedformulaList)) fset.(0); 

165 


166 
let formulaList = ref [] in 

167  
168 
for i = 0 to (List.length !hashedformulaList)  1 do 

169 
formulaList := (List.nth !hashedformulaList i).fml :: (!formulaList); 

170 
done; 

171  
142  172 
(*TODO ueber alle Klauseln iterieren*) 
143 
let form = ref TRUE in 

173 
let ret = ref (List.hd !formulaList) in 

174 
for i = 1 to (List.length !formulaList)  1 do 

175 
ret := CoAlgFormula.AND(!ret, (List.nth !formulaList i)); 

176 
done; 

144  177  
145 
A TRUE


178 
!ret


146  179  
147 
(* every new symbol is added to the formula (with conjunction) *) 

148  180 
let formula3 noms = 
149  181 
let formula = ref (E_AP (List.nth noms 0)) in 
150  182 
for i = 1 to (List.length noms)  1 do 
...  ...  
152  184 
done; 
153  185 
!formula 
154  186  
155 
(* calculates the translation from formulas with nominals to formulas with E and A*) 

156 
let nom2EA f nomTbl sorts = 

157 
let (noms, form1) = formula1 f in 

158 
let form2 = formula2 f noms nomTbl sorts in 

187 
(* calculates the translation from formulas with nominals to formulas with E and A*) 

188 
(* form_new = form1 & form2 & form3 where 

189 
* form1 = form [qi > nomi] 

190 
* form2 = inv (form1) 

191 
* form3 = /\ E(qi) 

192 
* *) 

193 
let nom2EA f nomTbl sorts = 

194 
(*list of nominals*) 

195 
let noms = ref [] in 

196 
(*mapping from nominals to new syms*) 

197 
let nomsub = ref StringMap.empty in 

198  
199 
(*first rename nominals then change type to eaformula*) 

200 
let form1help = rename f nomsub noms in 

201 
let form1 = coalgtoea form1help in 

202  
203 
(*first calculate flc (and in future the other stuff) then rename nominals then change type to eaformula*) 

204 
(*TODO Wont work for this A in translation.. Fix it!*) 

205 
let form2help = formula2 f noms nomTbl sorts in 

206 
let form22 = rename form2help nomsub noms in 

207 
let form2 = coalgtoea form22 in 

208 


209 
(*conjunction of all new nominalsymbols*) 

159  210 
let form3 = if List.length !noms > 0 then formula3 !noms else TRUE in 
211 


160  212 
let formula = if List.length !noms > 0 then AND(AND(form1, form2), form3) else form1 in 
213 


161  214 
formula 
162  215  
163  216 
(* vim: set et sw=2 sts=2 ts=8 : *) 
Also available in: Unified diff