Project

General

Profile

Revision bc0691dc src/lib/CoAlgFormula.ml

View differences:

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

Also available in: Unified diff