Revision bc0691dc src/lib/Nom2fix.ml
src/lib/Nom2fix.ml  

122  122 
done; 
123  123 
(*end calc flc*) 
124  124  
125 
let ret = ref (calcforsub (List.hd !formulaList) noms funct) in 

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

127 
let akt = List.nth !formulaList i in 

125 
let formulaListSmall = ref [] in 

126  
127 
let rem = ref false in 

128  
129 
for i = 0 to (List.length !formulaList)  1 do 

130 
for j = i + 1 to (List.length !formulaList)  1 do 

131 
rem := if CoAlgFormula.equals (List.nth !formulaList i) (CoAlgFormula.nnfNeg (List.nth !formulaList j)) then true else !rem; 

132 
print_endline (if !rem == true then "true" else "false"); 

133 
print_endline (CoAlgFormula.exportFormula (CoAlgFormula.nnf (List.nth !formulaList i))); 

134 
print_endline (CoAlgFormula.exportFormula (CoAlgFormula.nnfNeg (List.nth !formulaList j))); 

135 
done; 

136 
if !rem == false then formulaListSmall := (List.nth !formulaList i) :: !formulaListSmall; 

137 
rem := false; 

138 
done; 

139  
140 
let ret = ref CoAlgFormula.TRUE in 

141 
for i = 0 to (List.length !formulaListSmall)  1 do 

142 
let akt = List.nth !formulaListSmall i in 

128  143 
match akt with 
129 
 CoAlgFormula.NOT f1 > ret := !ret; 

130  144 
 CoAlgFormula.AND (f1,f2) 
131  145 
 CoAlgFormula.OR (f1,f2) > ret := !ret; 
132 
 _ > let sub = calcforsub (List.nth !formulaList i) noms funct in 

146 
 CoAlgFormula.NOT f1 > let sub = calcforsub f1 noms funct in 

147 
ret := CoAlgFormula.AND(!ret, sub); 

148 
 _ > let sub = calcforsub (List.nth !formulaListSmall i) noms funct in 

133  149 
ret := CoAlgFormula.AND(!ret, sub); 
134  150 
done; 
135  151 
Also available in: Unified diff