Project

General

Profile

Revision bc0691dc

View differences:

src/coalg/coalg.ml
212 212
        let g = Nom2fix.translate f nomTable sorts s true in
213 213
        let str = CoAlgFormula.exportFormula g in
214 214
        incr counter;
215
        (*print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");*)
215
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
216 216
        flush stdout;
217 217
      else ()
218 218
    done
......
261 261
        let g = Nom2fix.translate f nomTable sorts s true in
262 262
        let str = CoAlgFormula.exportFormula g in
263 263
        incr counter;
264
        (*print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");*)
264
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": ");
265 265
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
266 266
        flush stdout;
267 267
      else ()
src/lib/CoAlgFormula.ml
1240 1240
    @return A formula in negation normal form and not containing "<=>" or "=>"
1241 1241
    that is equivalent to ~f.
1242 1242
 *)
1243

  
1244
let rec equals f_1 f_2 =
1245
  match f_1, f_2 with
1246
  | TRUE, TRUE -> true 
1247
  | FALSE, FALSE -> true
1248
  | AP s1, AP s2 -> compare s1 s2 = 0
1249
  | VAR f1, VAR f2 -> compare f1 f2 = 0
1250
  | NOT f1, NOT f2 -> equals f1 f2
1251
  | AT(s1,f1), AT(s2,f2) -> (compare s1 s2 = 0) && (equals f1 f2)
1252
  | AND(f1,g1), AND(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1253
  | OR(f1,g1), OR(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1254
  | EQU(f1,g1), EQU(f2,g2) -> (equals f1 f2) && (equals g1 g2) 
1255
  | IMP(f1,g1), IMP(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1256
  | EX(s1,g1), EX(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1257
  | AX(s1,g1), AX(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1258
  | ENFORCES(s1,g1), ENFORCES(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1259
  | ALLOWS(s1,g1), ALLOWS(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1260
  | MIN(n1,s1,g1), MIN(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1261
  | MAX(n1,s1,g1), MAX(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1262
  | MORETHAN(n1,s1,g1), MORETHAN(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1263
  | MAXEXCEPT(n1,s1,g1), MAXEXCEPT(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2)
1264
  | ATLEASTPROB(p1,g1), ATLEASTPROB(p2,g2) -> (compare p1 p2 = 0) && (equals g1 g2)
1265
  | LESSPROBFAIL(p1,g1), LESSPROBFAIL(p2,g2) -> (compare p1 p2 = 0) && (equals g1 g2)
1266
  | CONST s1, CONST s2 -> compare s1 s2 = 0
1267
  | CONSTN s1, CONSTN s2 -> compare s1 s2 = 0
1268
  | ID(f1), ID(f2) -> equals f1 f2
1269
  | NORM(f1,g1),NORM(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1270
  | NORMN(f1,g1), NORMN(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1271
  | CHC(f1,g1), CHC(f2,g2) -> (equals f1 f2) && (equals g1 g2)
1272
  | FUS(b1,g1), FUS(b2,g2) -> (compare b1 b2 = 0) && (equals g1 g2)
1273
  | MU(s1,g1), MU(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1274
  | NU(s1,g1),  NU(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2)
1275
  | _ -> false
1276

  
1277

  
1243 1278
let rec nnfNeg f =
1244 1279
  match f with
1245 1280
  | TRUE -> FALSE
src/lib/CoAlgFormula.mli
88 88

  
89 89
val verifyFormula : formula -> unit
90 90

  
91
val equals: formula -> formula -> bool
91 92
val nnfNeg : formula -> formula
92 93
val nnf : formula -> formula
93 94

  
src/lib/Nom2fix.ml
122 122
  done;
123 123
  (*end calc flc*)
124 124

  
125
  let ret = ref (calcforsub (List.hd !formulaList) noms funct) in
126
  for i = 1 to (List.length !formulaList) - 1 do
127
    let akt = List.nth !formulaList i in
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
128 143
    match akt with
129
    | CoAlgFormula.NOT f1 -> ret := !ret;
130 144
    | CoAlgFormula.AND (f1,f2)
131 145
    | CoAlgFormula.OR (f1,f2) -> ret := !ret;
132
    | _ -> let sub = calcforsub (List.nth !formulaList i) noms funct in
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
133 149
           ret := CoAlgFormula.AND(!ret, sub);
134 150
  done;
135 151

  

Also available in: Unified diff