Revision bc0691dc
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