Revision bc0691dc src/lib/CoAlgFormula.ml
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