Project

General

Profile

Revision e3cf4ca2

View differences:

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 : *)
src/lib/EAFormula.mli
27 27

  
28 28

  
29 29
val exportFormula : eaformula -> string
30
val formula1 : CoAlgFormula.formula -> string list ref * eaformula
31
val formula2 : CoAlgFormula.formula -> string list -> (string -> int option) -> CoAlgReasoner.sortTable -> eaformula
30
val rename : CoAlgFormula.formula -> string Map.Make(String).t ref -> string list ref -> CoAlgFormula.formula
31
val coalgtoea : CoAlgFormula.formula -> eaformula
32
val formula2 : CoAlgFormula.formula -> string list -> (string -> int option) -> CoAlgReasoner.sortTable -> CoAlgFormula.formula
32 33
val formula3 : string list -> eaformula
33 34
val nom2EA : CoAlgFormula.formula -> (string -> int option) -> CoAlgReasoner.sortTable -> eaformula
34 35

  

Also available in: Unified diff