Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / Nom2fix.ml @ bc0691dc

History | View | Annotate | Download (7.17 KB)

1
module CA = CoAlgFormula
2
module StringMap = Map.Make(String)
3

    
4
type nomTbl = string -> CoAlgFormula.sort option
5
let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
6

    
7

    
8
let rename f nomsub noms =
9
  let rec rename_formula1 f = 
10
    let name = Stream.next gensym in
11
    match f with
12
    | CoAlgFormula.FALSE -> CoAlgFormula.FALSE
13
    | CoAlgFormula.TRUE -> CoAlgFormula.TRUE
14
    | CoAlgFormula.AP s ->
15
        if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then noms := name :: !noms;
16
        if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then nomsub := StringMap.add s name !nomsub;
17
        if (CoAlgFormula.isNominal s) then CoAlgFormula.AP (StringMap.find s !nomsub)
18
        else CoAlgFormula.AP s
19
    | CoAlgFormula.NOT f -> CoAlgFormula.NOT (rename_formula1 f)
20
    | CoAlgFormula.OR (f1, f2) -> CoAlgFormula.OR ((rename_formula1 f1), (rename_formula1 f2))
21
    | CoAlgFormula.AND (f1, f2) -> CoAlgFormula.AND ((rename_formula1 f1), (rename_formula1 f2))
22
    | CoAlgFormula.EQU (f1, f2) -> CoAlgFormula.EQU ((rename_formula1 f1), (rename_formula1 f2))
23
    | CoAlgFormula.IMP (f1, f2) -> CoAlgFormula.IMP ((rename_formula1 f1), (rename_formula1 f2))
24
    | CoAlgFormula.EX (s, f) -> CoAlgFormula.EX (s, (rename_formula1 f))
25
    | CoAlgFormula.AX (s, f) -> CoAlgFormula.AX (s, (rename_formula1 f))
26
    | CoAlgFormula.ENFORCES (l, f) -> CoAlgFormula.ENFORCES(l, (rename_formula1 f))
27
    | CoAlgFormula.ALLOWS (l, f) -> CoAlgFormula.ALLOWS(l, (rename_formula1 f))
28
    | CoAlgFormula.MIN (i, s, f) -> CoAlgFormula.MIN(i, s, (rename_formula1 f))
29
    | CoAlgFormula.MAX (i, s, f) -> CoAlgFormula.MAX(i, s, (rename_formula1 f))
30
    | CoAlgFormula.MORETHAN (i, s, f) -> CoAlgFormula.MORETHAN(i, s, (rename_formula1 f))
31
    | CoAlgFormula.MAXEXCEPT (i, s, f) -> CoAlgFormula.MAXEXCEPT(i, s, (rename_formula1 f))
32
    | CoAlgFormula.ATLEASTPROB (r, f) -> CoAlgFormula.ATLEASTPROB(r, (rename_formula1 f))
33
    | CoAlgFormula.LESSPROBFAIL (r, f) -> CoAlgFormula.LESSPROBFAIL (r, (rename_formula1 f))
34
    | CoAlgFormula.ID f -> CoAlgFormula.ID (rename_formula1 f)
35
    | CoAlgFormula.MU (s, f) -> CoAlgFormula.MU (s, (rename_formula1 f))
36
    | CoAlgFormula.NU (s, f) -> CoAlgFormula.NU (s, (rename_formula1 f))
37
    | CoAlgFormula.AF f -> CoAlgFormula.AF (rename_formula1 f)
38
    | CoAlgFormula.EF f -> CoAlgFormula.EF (rename_formula1 f)
39
    | CoAlgFormula.AG f -> CoAlgFormula.AG (rename_formula1 f)
40
    | CoAlgFormula.EG f -> CoAlgFormula.EG (rename_formula1 f)
41
    | CoAlgFormula.VAR s -> CoAlgFormula.VAR s
42
  in
43
  rename_formula1 f
44

    
45
(*calculates inner term of inv for one subformula*)
46
let calcforsub subf noms funct =
47
  let ret = ref CoAlgFormula.TRUE in
48
  for i = 0 to (List.length !noms) - 1 do
49
    let aktnom = CoAlgFormula.AP(List.nth !noms i) in
50
    let add = match funct with
51
    | CoAlgMisc.MultiModalK
52
    | CoAlgMisc.MultiModalKD -> CoAlgFormula.IMP(CoAlgFormula.EF(CoAlgFormula.AND(subf, aktnom)),CoAlgFormula.AG(CoAlgFormula.IMP(aktnom, subf)))
53
    (*| CoAlgMisc.Monotone ->*)
54
    (*| CoAlgMisc.CoalitionLogic -> CoAlgFormula.IMP(CoAlgFormula.MU(x, CoAlgFormula.OR(CoAlgFormula.AND(subf, aktnom), )))
55
    | CoAlgMisc.GML ->
56
    | CoAlgMisc.PML ->*)
57
    in
58
        ret := AND(!ret, add);
59
  done;
60

    
61
  !ret
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

    
99
let calcinv f noms nomTbl sorts s =
100
  (*calc flc*)
101
  let card = Array.length sorts in
102
  let hcF = CoAlgFormula.HcFormula.create true in
103
  let fset = Array.init card (fun _ -> CoAlgFormula.HcFHt.create 128) in
104
  let vset = Array.init card (fun _ -> CoAlgFormula.HcFHt.create 128) in
105
  let atset = CoAlgFormula.HcFHt.create 64 in
106
  let nomset = Hashtbl.create 16 in
107

    
108
  let hcform = CoAlgFormula.hc_formula hcF f in
109

    
110
  CoAlgMisc.sortTable := Array.copy sorts;
111
  CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform;
112

    
113
  let (funct, l) = Array.get sorts 0 in
114

    
115
  let hashedformulaList = ref [] in
116
  CoAlgFormula.HcFHt.iter (fun k v -> hashedformulaList := k :: (!hashedformulaList)) fset.(0);
117
  
118
  let formulaList = ref [] in
119

    
120
  for i = 0 to (List.length !hashedformulaList) - 1 do
121
    formulaList := (List.nth !hashedformulaList i).fml :: (!formulaList);
122
  done;
123
  (*end calc flc*)
124

    
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
143
    match akt with
144
    | CoAlgFormula.AND (f1,f2)
145
    | CoAlgFormula.OR (f1,f2) -> ret := !ret;
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
149
           ret := CoAlgFormula.AND(!ret, sub);
150
  done;
151

    
152
  !ret
153

    
154
let translate fu nomTbl sorts s opt =
155
  let f = (CA.nnf fu) in
156

    
157
  (*list of nominals*)
158
  let noms = ref [] in
159
  (*mapping from nominals to new syms*)
160
  let nomsub = ref StringMap.empty in
161

    
162
  (*first rename nominals then change type to eaformula*)
163
  let ren = rename f nomsub noms in
164
  (*print_string "using Formula: ";
165
  print_endline (CA.exportFormula ren);*)
166

    
167
  (*first calculate flc then rename nominals*)
168
  let invhelp = match opt with
169
    | true -> calcinv f noms nomTbl sorts s
170
    | false -> calcinvnonopt f noms nomTbl sorts s
171
  in
172
  let inv = rename invhelp nomsub noms in
173

    
174
  let formula = if List.length !noms > 0 then CoAlgFormula.AND(ren, inv) else ren in
175
  (*print_string "Formula with EF/AG: ";
176
  print_endline (CA.exportFormula formula);*)
177
  let ret = CA.convertToMu formula in
178
 
179
  ret
180

    
181
(* vim: set et sw=2 sts=2 ts=8 : *)