Project

General

Profile

Revision 2d58f46f

View differences:

src/coalg/coalg.ml
170 170
      done
171 171
    with End_of_file -> ()
172 172

  
173
let choiceNom2fixNonOpt opts =
174
  let verb = opts.verbose in
175
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
176
    let printRes sat =
177
      if not verb then
178
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
179
      else ()
180
    in
181
  (*CoAlgMisc.sortTable = ref sorts;*)
182
  try
183
    while true do
184
      let input = read_line () in
185
      if not (GenAndComp.isEmptyString input) then
186
        let (s, f) = CoAlgFormula.importSortedFormula input in
187
        let (tbox, fu) = CoAlgFormula.importQuery input in
188
        let g = Nom2fix.translate f nomTable sorts s false in
189
        let str = CoAlgFormula.exportFormula g in
190
        incr counter;
191
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
192
        flush stdout;
193
      else ()
194
    done
195
  with End_of_file -> ()
196

  
173 197
let choiceNom2fix opts =
174 198
  let verb = opts.verbose in
175 199
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
......
185 209
      if not (GenAndComp.isEmptyString input) then
186 210
        let (s, f) = CoAlgFormula.importSortedFormula input in
187 211
        let (tbox, fu) = CoAlgFormula.importQuery input in
188
        let g = Nom2fix.translate f nomTable sorts s in
212
        let g = Nom2fix.translate f nomTable sorts s true in
213
        let str = CoAlgFormula.exportFormula g in
214
        incr counter;
215
        (*print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");*)
216
        flush stdout;
217
      else ()
218
    done
219
  with End_of_file -> ()
220

  
221
let choiceSolveNomNonOpt opts =
222
  let verb = opts.verbose in
223
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
224
    let printRes sat =
225
      if not verb then
226
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
227
      else ()
228
    in
229
  (*CoAlgMisc.sortTable = ref sorts;*)
230
  try
231
    while true do
232
      let input = read_line () in
233
      if not (GenAndComp.isEmptyString input) then
234
        let (s, f) = CoAlgFormula.importSortedFormula input in
235
        let (tbox, fu) = CoAlgFormula.importQuery input in
236
        let g = Nom2fix.translate f nomTable sorts s false in
189 237
        let str = CoAlgFormula.exportFormula g in
190 238
        incr counter;
191 239
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
240
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
192 241
        flush stdout;
193 242
      else ()
194 243
    done
......
209 258
      if not (GenAndComp.isEmptyString input) then
210 259
        let (s, f) = CoAlgFormula.importSortedFormula input in
211 260
        let (tbox, fu) = CoAlgFormula.importQuery input in
212
        let g = Nom2fix.translate f nomTable sorts s in
261
        let g = Nom2fix.translate f nomTable sorts s true in
213 262
        let str = CoAlgFormula.exportFormula g in
214 263
        incr counter;
215
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
264
        (*print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");*)
216 265
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
217 266
        flush stdout;
218 267
      else ()
......
273 322
       | "verify" -> choiceVerify opts
274 323
       | "graph" -> choiceGraph opts
275 324
       | "nom2fix" -> choiceNom2fix opts
325
       | "nom2fixN" -> choiceNom2fixNonOpt opts
276 326
       | "solveNom" -> choiceSolveNom opts
327
       | "solveNomN" -> choiceSolveNomNonOpt opts
277 328
       | _ -> printUsage (Sys.argv.(0))
278 329

  
279 330
(* vim: set et sw=2 sts=2 ts=8 : *)
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
src/lib/Nom2fix.mli
4 4

  
5 5
val rename : CoAlgFormula.formula -> string Map.Make(String).t ref -> string list ref ->  CoAlgFormula.formula
6 6
val calcinv : CoAlgFormula.formula -> string list ref -> (string -> int option) -> CoAlgReasoner.sortTable -> int -> CoAlgFormula.formula
7
val translate : CoAlgFormula.formula -> (string -> int option) -> CoAlgReasoner.sortTable -> int -> CoAlgFormula.formula
7
val translate : CoAlgFormula.formula -> (string -> int option) -> CoAlgReasoner.sortTable -> int -> bool ->  CoAlgFormula.formula
8 8

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

Also available in: Unified diff