## 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