Revision 946e8213 src/lib/Nom2fix.ml
src/lib/Nom2fix.ml  

44  44  
45  45 
!ret 
46  46  
47 
let calcinv f noms nomTbl sorts = 

47 
let calcinv f noms nomTbl sorts s =


48  48 
(*calc flc*) 
49  49 
let card = Array.length sorts in 
50  50 
let hcF = CoAlgFormula.HcFormula.create true in 
...  ...  
52  52 
let vset = Array.init card (fun _ > CoAlgFormula.HcFHt.create 128) in 
53  53 
let atset = CoAlgFormula.HcFHt.create 64 in 
54  54 
let nomset = Hashtbl.create 16 in 
55 
let (s, fo) = CoAlgFormula.importSortedFormula (CoAlgFormula.exportFormula f) in 

56  55  
57  56 
let hcform = CoAlgFormula.hc_formula hcF f in 
58  57  
...  ...  
78  77  
79  78 
!ret 
80  79  
81 
let translate f nomTbl sorts = 

80 
let translate fu nomTbl sorts s = 

81 
let f = (CA.nnf fu) in 

82  
82  83 
(*list of nominals*) 
83  84 
let noms = ref [] in 
84  85 
(*mapping from nominals to new syms*) 
85  86 
let nomsub = ref StringMap.empty in 
86  87  
87 
print_endline (CA.exportFormula f); 

88  
89  88 
(*first rename nominals then change type to eaformula*) 
90  89 
let ren = rename f nomsub noms in 
91 
print_string "rename: ";


90 
print_string "using Formula: ";


92  91 
print_endline (CA.exportFormula ren); 
93  92  
94  93 
(*first calculate flc then rename nominals*) 
95 
let invhelp = calcinv f noms nomTbl sorts in 

96 
print_string "invhelp: "; 

97 
print_endline (CoAlgFormula.exportFormula invhelp); 

94 
let invhelp = calcinv f noms nomTbl sorts s in


95 
(*print_string "invhelp: ";


96 
print_endline (CoAlgFormula.exportFormula invhelp);*)


98  97  
99  98 
let inv = rename invhelp nomsub noms in 
100 
print_string "inv: "; 

101 
print_endline (CoAlgFormula.exportFormula inv); 

99 
(*print_string "inv: ";


100 
print_endline (CoAlgFormula.exportFormula inv);*)


102  101  
103  102 
let formula = if List.length !noms > 0 then CoAlgFormula.AND(ren, inv) else ren in 
103 
let ret = CA.convertToMu formula in 

104  104 

105 
formula


105 
ret


106  106  
107  107 
(* vim: set et sw=2 sts=2 ts=8 : *) 
Also available in: Unified diff