Revision 2d58f46f src/lib/Nom2fix.ml
src/lib/Nom2fix.ml  

60  60  
61  61 
!ret 
62  62  
63 
let calcinvnonopt f noms nomTbl sorts s = 

64 
(*calc flc*) 

65 
let card = Array.length sorts in 

66 
let hcF = CoAlgFormula.HcFormula.create true in 

67 
let fset = Array.init card (fun _ > CoAlgFormula.HcFHt.create 128) in 

68 
let vset = Array.init card (fun _ > CoAlgFormula.HcFHt.create 128) in 

69 
let atset = CoAlgFormula.HcFHt.create 64 in 

70 
let nomset = Hashtbl.create 16 in 

71  
72 
let hcform = CoAlgFormula.hc_formula hcF f in 

73  
74 
CoAlgMisc.sortTable := Array.copy sorts; 

75 
CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform; 

76  
77 
let (funct, l) = Array.get sorts 0 in 

78  
79 
let hashedformulaList = ref [] in 

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

81 


82 
let formulaList = ref [] in 

83  
84 
for i = 0 to (List.length !hashedformulaList)  1 do 

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

86 
done; 

87 
(*end calc flc*) 

88  
89 
let ret = ref (calcforsub (List.hd !formulaList) noms funct) in 

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

91 
let akt = List.nth !formulaList i in 

92 
let sub = calcforsub (List.nth !formulaList i) noms funct in 

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

94 
done; 

95  
96 
!ret 

97  
98  
63  99 
let calcinv f noms nomTbl sorts s = 
64  100 
(*calc flc*) 
65  101 
let card = Array.length sorts in 
...  ...  
90  126 
for i = 1 to (List.length !formulaList)  1 do 
91  127 
let akt = List.nth !formulaList i in 
92  128 
match akt with 
129 
 CoAlgFormula.NOT f1 > ret := !ret; 

93  130 
 CoAlgFormula.AND (f1,f2) 
94  131 
 CoAlgFormula.OR (f1,f2) > ret := !ret; 
95  132 
 _ > let sub = calcforsub (List.nth !formulaList i) noms funct in 
...  ...  
98  135  
99  136 
!ret 
100  137  
101 
let translate fu nomTbl sorts s = 

138 
let translate fu nomTbl sorts s opt =


102  139 
let f = (CA.nnf fu) in 
103  140  
104  141 
(*list of nominals*) 
...  ...  
108  145  
109  146 
(*first rename nominals then change type to eaformula*) 
110  147 
let ren = rename f nomsub noms in 
111 
print_string "using Formula: "; 

112 
print_endline (CA.exportFormula ren); 

148 
(*print_string "using Formula: ";


149 
print_endline (CA.exportFormula ren);*)


113  150  
114  151 
(*first calculate flc then rename nominals*) 
115 
let invhelp = calcinv f noms nomTbl sorts s in 

152 
let invhelp = match opt with 

153 
 true > calcinv f noms nomTbl sorts s 

154 
 false > calcinvnonopt f noms nomTbl sorts s 

155 
in 

116  156 
let inv = rename invhelp nomsub noms in 
117  157  
118  158 
let formula = if List.length !noms > 0 then CoAlgFormula.AND(ren, inv) else ren in 
119 
print_string "Formula with EF/AG: "; 

120 
print_endline (CA.exportFormula formula); 

159 
(*print_string "Formula with EF/AG: ";


160 
print_endline (CA.exportFormula formula);*)


121  161 
let ret = CA.convertToMu formula in 
122  162 

123  163 
ret 
Also available in: Unified diff