cool / src / lib / CoAlgReasoner.ml @ 7c4d2eb4
History  View  Annotate  Download (22 KB)
1 
(** A graphtableaubased decision procedure framework for coalgebraic logics. 

2 
@author Florian Widmann 
3 
*) 
4  
5  
6 
open CoAlgMisc 
7  
8 
module M = Minisat 
9  
10 
type sortTable = CoAlgMisc.sortTable 
11  
12  
13 
(*****************************************************************************) 
14 
(* Propagation of Satisfiability *) 
15 
(*****************************************************************************) 
16  
17 
let propSatFindSucc setCnstr cset = 
18 
if csetHasDot cset then false 
19 
else 
20 
match graphFindCnstr cset with 
21 
 None > assert false 
22 
 Some SatC > true 
23 
 Some (OpenC _) > setMemCnstr setCnstr cset 
24 
 Some (UnexpandedC _) 
25 
 Some UnsatC > false 
26  
27 
let rec propSat setStates setCores setCnstr = function 
28 
 [] > () 
29 
 propElem::tl > 
30 
let tl1 = 
31 
match propElem with 
32 
 UState (state, _) > 
33 
if setMemState setStates state then 
34 
let cnstrs = stateGetConstraints state in 
35 
let isStillOpen = cssExists (fun c > propSatFindSucc setCnstr c) cnstrs in 
36 
if isStillOpen then () else setRemoveState setStates state 
37 
else (); 
38 
tl 
39 
 UCore (core, _) > 
40 
if setMemCore setCores core then 
41 
let cnstrs = coreGetConstraints core in 
42 
let isStillOpen = cssExists (fun c > propSatFindSucc setCnstr c) cnstrs in 
43 
if isStillOpen then tl else begin 
44 
setRemoveCore setCores core; 
45 
let cnstrPar = coreGetConstraintParents core in 
46 
List.fold_left (fun acc cset > (UCnstr cset)::acc) tl cnstrPar 
47 
end 
48 
else tl 
49 
 UCnstr cset > 
50 
if setMemCnstr setCnstr cset then begin 
51 
setRemoveCnstr setCnstr cset; 
52 
match graphFindCnstr cset with 
53 
 Some (OpenC nodes) > 
54 
let prop acc node = 
55 
match node with 
56 
 Core core > (UCore (core, true))::acc 
57 
 State state > (UState (state, None))::acc 
58 
in 
59 
List.fold_left prop tl nodes 
60 
 _ > assert false 
61 
end else tl 
62 
in 
63 
propSat setStates setCores setCnstr tl1 
64  
65 
let propagateSat () = 
66 
let setStates = setEmptyState () in 
67 
let setCores = setEmptyCore () in 
68 
let setCnstr = setEmptyCnstr () in 
69 
let fktS1 state = 
70 
match stateGetStatus state with 
71 
 Expandable 
72 
 Open > setAddState setStates state 
73 
 Unsat 
74 
 Sat > () 
75 
in 
76 
graphIterStates fktS1; 
77 
let fktC1 core = 
78 
match coreGetStatus core with 
79 
 Expandable 
80 
 Open > setAddCore setCores core 
81 
 Unsat 
82 
 Sat > () 
83 
in 
84 
graphIterCores fktC1; 
85 
let cfkt1 cset cnstr = 
86 
if csetHasDot cset then () 
87 
else 
88 
match cnstr with 
89 
 OpenC _ > setAddCnstr setCnstr cset 
90 
 UnsatC 
91 
 SatC 
92 
 UnexpandedC _ > () 
93 
in 
94 
graphIterCnstrs cfkt1; 
95 
graphIterStates (fun state > propSat setStates setCores setCnstr [UState (state, None)]); 
96 
graphIterCores (fun core > propSat setStates setCores setCnstr [UCore (core, false)]); 
97 
setIterState (fun state > stateSetStatus state Sat) setStates; 
98 
let setCoreSat core = 
99 
coreSetStatus core Sat; 
100 
if core == graphGetRoot () then raise (CoAlg_finished true) else () 
101 
in 
102 
setIterCore setCoreSat setCores; 
103 
setIterCnstr (fun cset > graphReplaceCnstr cset SatC) setCnstr 
104  
105  
106 
(*****************************************************************************) 
107 
(* Propagation of Unsatisfiability *) 
108 
(*****************************************************************************) 
109  
110 
let isConstraintUnsat cset = 
111 
match graphFindCnstr cset with 
112 
 None > assert false 
113 
 Some UnsatC > true 
114 
 _ > false 
115  
116 
let fhtMustFind fht f = 
117 
match fhtFind fht f with 
118 
 Some l > l 
119 
 None > assert false 
120  
121 
let lhtMustFind lht l = 
122 
match lhtFind lht l with 
123 
 Some f > f 
124 
 None > assert false 
125  
126 
let rec propagateUnsat = function 
127 
 [] > () 
128 
 propElem::tl > 
129 
let tl1 = 
130 
match propElem with 
131 
 UState (state, idxopt) > begin 
132 
match stateGetStatus state with 
133 
 Unsat > tl 
134 
 Sat > assert false 
135 
 Open 
136 
 Expandable > 
137 
let mbs = 
138 
match idxopt with 
139 
 None > stateGetBs state 
140 
 Some idx > 
141 
let (dep, children) = stateGetRule state idx in 
142 
let getBs core = 
143 
assert (coreGetStatus core = Unsat); 
144 
coreGetBs core 
145 
in 
146 
dep (List.map getBs children) 
147 
in 
148 
stateSetBs state mbs; 
149 
stateSetStatus state Unsat; 
150 
let prop acc core = 
151 
let turnsUnsat = 
152 
match coreGetStatus core with 
153 
 Open > List.for_all (fun s > stateGetStatus s = Unsat) (coreGetChildren core) 
154 
 Expandable 
155 
 Unsat 
156 
 Sat > false 
157 
in 
158 
if turnsUnsat then (UCore (core, false))::acc else acc 
159 
in 
160 
List.fold_left prop tl (stateGetParents state) 
161 
end 
162 
 UCore (core, comesFromCnstr) > begin 
163 
match coreGetStatus core with 
164 
 Unsat > tl 
165 
 Sat > assert false 
166 
 Open 
167 
 Expandable > 
168 
let mbs = 
169 
if comesFromCnstr then coreGetBs core 
170 
else 
171 
let bs = coreGetBs core in 
172 
let solver = coreGetSolver core in 
173 
let fht = coreGetFht core in 
174 
let lht = lhtInit () in 
175 
let addLits f acc = 
176 
let lit = fhtMustFind fht f in 
177 
lhtAdd lht lit f; 
178 
lit::acc 
179 
in 
180 
let litset = bsetFold addLits bs [] in 
181 
let addClauses state = 
182 
let cbs = stateGetBs state in 
183 
let clause = bsetFold (fun f acc > (M.neg_lit (fhtMustFind fht f))::acc) cbs [] in 
184 
let okay = M.add_clause solver clause in 
185 
assert okay 
186 
in 
187 
List.iter addClauses (coreGetChildren core); 
188 
let isSat = M.invoke_solver solver litset in 
189 
assert (not isSat); 
190 
let res = bsetMake () in 
191 
let confls = M.get_conflict solver in 
192 
List.iter (fun l > bsetAdd res (lhtMustFind lht l)) confls; 
193 
res 
194 
in 
195 
coreSetBs core mbs; 
196 
coreSetStatus core Unsat; 
197 
if core == graphGetRoot () then raise (CoAlg_finished false) else (); 
198 
let prop acc (state, idx) = 
199 
let turnsUnsat = 
200 
match stateGetStatus state with 
201 
 Open 
202 
 Expandable > 
203 
List.for_all (fun c > coreGetStatus c = Unsat) (snd (stateGetRule state idx)) 
204 
 Unsat 
205 
 Sat > false 
206 
in 
207 
if turnsUnsat then (UState (state, Some idx))::acc else acc 
208 
in 
209 
let tl2 = List.fold_left prop tl (coreGetParents core) in 
210 
List.fold_left (fun acc cset > (UCnstr cset)::acc) tl2 (coreGetConstraintParents core) 
211 
end 
212 
 UCnstr cset > 
213 
match graphFindCnstr cset with 
214 
 None 
215 
 Some SatC > assert false 
216 
 Some UnsatC > tl 
217 
 Some (UnexpandedC nodes) 
218 
 Some (OpenC nodes) > 
219 
graphReplaceCnstr cset UnsatC; 
220 
let prop acc node = 
221 
match node with 
222 
 State state > 
223 
let turnsUnsat = 
224 
match stateGetStatus state with 
225 
 Expandable 
226 
 Open > cssForall isConstraintUnsat (stateGetConstraints state) 
227 
 Unsat 
228 
 Sat > false 
229 
in 
230 
if turnsUnsat then (UState (state, None))::acc else acc 
231 
 Core core > 
232 
let turnsUnsat = 
233 
match coreGetStatus core with 
234 
 Expandable 
235 
 Open > cssForall isConstraintUnsat (coreGetConstraints core) 
236 
 Unsat 
237 
 Sat > false 
238 
in 
239 
if turnsUnsat then (UCore (core, true))::acc else acc 
240 
in 
241 
List.fold_left prop tl nodes 
242 
in 
243 
propagateUnsat tl1 
244  
245  
246 
(*****************************************************************************) 
247 
(* Propagation of Nominal Constraints *) 
248 
(*****************************************************************************) 
249  
250 
let extractAts sort bs = 
251 
let ats = csetMake () in 
252 
let procNom nom f = 
253 
match lfGetType sort f with 
254 
 AndF 
255 
 OrF > () 
256 
 ConstF 
257 
 AtF > () 
258 
 _ > csetAdd ats (lfGetAt (sort, nom) f) 
259 
in 
260 
let getAts f = 
261 
match lfGetType sort f with 
262 
 AtF > csetAdd ats (lfToAt sort f) 
263 
 NomF > bsetIter (fun f1 > procNom f f1) bs 
264 
 _ > () 
265 
in 
266 
bsetIter getAts bs; 
267 
ats 
268  
269 
let detConstraintsState state = 
270 
let procRule accR (_, chldrn) = 
271 
let procChldrn accC core = 
272 
if coreGetStatus core = Unsat then accC 
273 
else cssUnion accC (coreGetConstraints core) 
274 
in 
275 
let orset = List.fold_left procChldrn cssEmpty chldrn in 
276 
let procOrset csetO accO = 
277 
let mkUnion csetU accU = 
278 
let cset = csetUnion csetO csetU in 
279 
cssAdd cset accU 
280 
in 
281 
cssFold mkUnion accR accO 
282 
in 
283 
cssFold procOrset orset cssEmpty 
284 
in 
285 
let sort = stateGetSort state in 
286 
let bs = stateGetBs state in 
287 
let ats = extractAts sort bs in 
288 
if stateGetStatus state = Expandable then csetAddDot ats else (); 
289 
List.fold_left procRule (cssSingleton ats) (stateGetRules state) 
290  
291 
let detConstraintsCore core = 
292 
let sort = coreGetSort core in 
293 
let bs = coreGetBs core in 
294 
let ats = extractAts sort bs in 
295 
let addCnstr acc state = 
296 
if stateGetStatus state = Unsat then acc 
297 
else 
298 
let csets = stateGetConstraints state in 
299 
(* cssFold (fun c a > cssAdd (csetUnion c ats) a) csets acc *) 
300 
cssUnion csets acc 
301 
in 
302 
let initInner = 
303 
if coreGetStatus core = Expandable then 
304 
(* let cset = csetCopy ats in *) 
305 
let cset = ats in 
306 
csetAddDot cset; 
307 
cssSingleton cset 
308 
else cssEmpty 
309 
in 
310 
List.fold_left addCnstr initInner (coreGetChildren core) 
311  
312 
let rec propNom = function 
313 
 [] > () 
314 
 node::tl > 
315 
let tl1 = 
316 
match node with 
317 
 State state > 
318 
if stateGetStatus state = Unsat then tl 
319 
else 
320 
let csets = detConstraintsState state in 
321 
let oldcsets = stateGetConstraints state in 
322 
if cssEqual csets oldcsets then tl 
323 
else begin 
324 
stateSetConstraints state csets; 
325 
List.fold_left (fun acc c > (Core c)::acc) tl (stateGetParents state) 
326 
end 
327 
 Core core > 
328 
if coreGetStatus core = Unsat then tl 
329 
else 
330 
let csets = detConstraintsCore core in 
331 
let oldcsets = coreGetConstraints core in 
332 
if cssEqual csets oldcsets then tl 
333 
else begin 
334 
coreSetConstraints core csets; 
335 
List.fold_left (fun acc (s, _) > (State s)::acc) tl (coreGetParents core) 
336 
end 
337 
in 
338 
propNom tl1 
339  
340 
let updateConstraints node elemU csets = 
341 
let update cset acc = 
342 
let cnstr = 
343 
match graphFindCnstr cset with 
344 
 Some cn > cn 
345 
 None > 
346 
let cn = UnexpandedC [] in 
347 
graphInsertCnstr cset cn; 
348 
queueInsertCnstr cset; 
349 
cn 
350 
in 
351 
match cnstr with 
352 
 UnsatC > acc 
353 
 UnexpandedC parents > 
354 
graphReplaceCnstr cset (UnexpandedC (node::parents)); 
355 
false 
356 
 OpenC parents > 
357 
graphReplaceCnstr cset (OpenC (node::parents)); 
358 
false 
359 
 SatC > false 
360 
in 
361 
let isUnsat = cssFold update csets true in 
362 
if isUnsat then propagateUnsat [elemU] else () 
363  
364 
let propagateNominals () = 
365 
let init = cssSingleton (csetMake ()) in 
366 
graphIterStates (fun s > if stateGetStatus s = Unsat then () else stateSetConstraints s init); 
367 
graphIterCores (fun c > if coreGetStatus c = Unsat then () else coreSetConstraints c init); 
368 
graphIterStates (fun s > propNom [State s]); 
369 
graphIterCores (fun c > propNom [Core c]); 
370 
graphClearCnstr (); 
371 
let fktS state = 
372 
if stateGetStatus state = Unsat then () 
373 
else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state) 
374 
in 
375 
graphIterStates fktS; 
376 
let fktC core = 
377 
if coreGetStatus core = Unsat then () 
378 
else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core) 
379 
in 
380 
graphIterCores fktC 
381  
382  
383 
(*****************************************************************************) 
384 
(* Node Expansions *) 
385 
(*****************************************************************************) 
386  
387 
let getLit sort fht solver f = 
388 
match fhtFind fht f with 
389 
 Some lit > lit 
390 
 None > 
391 
let var = M.new_variable solver in 
392 
let lit = M.var_to_lit var true in 
393 
fhtAdd fht f lit; 
394 
let () = 
395 
match lfGetNeg sort f with 
396 
 None > () 
397 
 Some nf > 
398 
let nlit = M.neg_lit lit in 
399 
fhtAdd fht nf nlit; 
400 
in 
401 
lit 
402  
403 
let newCore sort bs = 
404 
let fht = fhtInit () in 
405 
let solver = M.new_solver () in 
406 
let rec addClauses f = 
407 
let lf = getLit sort fht solver f in 
408 
match lfGetType sort f with 
409 
 OrF > 
410 
let f1 = lfGetDest1 sort f in 
411 
let f2 = lfGetDest2 sort f in 
412 
addClauses f1; 
413 
addClauses f2; 
414 
let lf1 = fhtMustFind fht f1 in 
415 
let lf2 = fhtMustFind fht f2 in 
416 
let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in 
417 
assert (okay) 
418 
 AndF > 
419 
let f1 = lfGetDest1 sort f in 
420 
let f2 = lfGetDest2 sort f in 
421 
addClauses f1; 
422 
addClauses f2; 
423 
let lf1 = fhtMustFind fht f1 in 
424 
let lf2 = fhtMustFind fht f2 in 
425 
let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in 
426 
assert (okay1); 
427 
let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in 
428 
assert (okay2) 
429 
 _ > () 
430 
in 
431 
bsetIter addClauses bs; 
432 
coreMake sort bs solver fht 
433  
434 
let getNextState core = 
435 
let bs = coreGetBs core in 
436 
let fht = coreGetFht core in 
437 
let litset = bsetFold (fun f acc > (fhtMustFind fht f)::acc) bs [] in 
438 
let solver = coreGetSolver core in 
439 
let isSat = M.invoke_solver solver litset in 
440 
if not isSat then None 
441 
else 
442 
let sort = coreGetSort core in 
443 
let newbs = bsetMake () in 
444 
let rec mkExclClause f acc = 
445 
match lfGetType sort f with 
446 
 OrF > 
447 
let f1 = lfGetDest1 sort f in 
448 
let lf1 = fhtMustFind fht f1 in 
449 
if M.literal_status solver lf1 = M.LTRUE then mkExclClause f1 acc 
450 
else 
451 
let f2 = lfGetDest2 sort f in 
452 
let lf2 = fhtMustFind fht f2 in 
453 
assert (M.literal_status solver lf2 = M.LTRUE); 
454 
mkExclClause f2 acc 
455 
 AndF > 
456 
let f1 = lfGetDest1 sort f in 
457 
let lf1 = fhtMustFind fht f1 in 
458 
assert (M.literal_status solver lf1 = M.LTRUE); 
459 
let acc1 = mkExclClause f1 acc in 
460 
let f2 = lfGetDest2 sort f in 
461 
let lf2 = fhtMustFind fht f2 in 
462 
assert (M.literal_status solver lf2 = M.LTRUE); 
463 
mkExclClause f2 acc1 
464 
 _ > 
465 
bsetAdd newbs f; 
466 
(M.neg_lit (fhtMustFind fht f))::acc 
467 
in 
468 
let clause = bsetFold mkExclClause bs [] in 
469 
let okay = M.add_clause solver clause in 
470 
assert (okay); 
471 
Some (sort, newbs) 
472  
473 
let newState sort bs = 
474 
let (func, sl) = !sortTable.(sort) in 
475 
let producer = CoAlgLogics.getExpandingFunctionProducer func in 
476 
let exp = producer sort bs sl in 
477 
stateMake sort bs exp 
478  
479 
let insertState parent sort bs = 
480 
let child = 
481 
match graphFindState sort bs with 
482 
 None > 
483 
let s = newState sort bs in 
484 
graphInsertState sort bs s; 
485 
queueInsertState s; 
486 
s 
487 
 Some s > s 
488 
in 
489 
coreAddChild parent child; 
490 
stateAddParent child parent 
491  
492 
let expandCore core = 
493 
match getNextState core with 
494 
 Some (sort, bs) > 
495 
insertState core sort bs; 
496 
queueInsertCore core 
497 
 None > 
498 
let isUnsat = List.for_all (fun s > stateGetStatus s = Unsat) (coreGetChildren core) in 
499 
if isUnsat then propagateUnsat [UCore (core, false)] 
500 
else coreSetStatus core Open 
501  
502  
503 
let insertCore sort bs = 
504 
match graphFindCore sort bs with 
505 
 None > 
506 
let c = newCore sort bs in 
507 
graphInsertCore sort bs c; 
508 
queueInsertCore c; 
509 
c 
510 
 Some c > c 
511  
512 
let insertRule state dep chldrn = 
513 
let insert (isUns, acc) (sort, bs) = 
514 
let bs1 = bsetAddTBox sort bs in 
515 
let core = insertCore sort bs1 in 
516 
let isUns1 = if coreGetStatus core = Unsat then isUns else false in 
517 
(isUns1, core::acc) 
518 
in 
519 
let (isUnsat, children) = List.fold_left insert (true, []) chldrn in 
520 
let idx = stateAddRule state dep (List.rev children) in 
521 
List.iter (fun c > coreAddParent c state idx) children; 
522 
if isUnsat then begin 
523 
propagateUnsat [UState (state, Some idx)]; 
524 
false 
525 
end else true 
526  
527 
let rec insertAllRules state = function 
528 
 [] > true 
529 
 (dep, chldrn)::tl > 
530 
let notUnsat = insertRule state dep chldrn in 
531 
if notUnsat then insertAllRules state tl else false 
532  
533 
let expandState state = 
534 
match stateNextRule state with 
535 
 AllInOne rules > 
536 
let notUnsat = insertAllRules state rules in 
537 
if notUnsat then stateSetStatus state Open 
538 
 NextRule (dep, chldrn) > 
539 
let notUnsat = insertRule state dep chldrn in 
540 
if notUnsat then queueInsertState state else () 
541 
 NoMoreRules > stateSetStatus state Open 
542  
543  
544 
let expandCnstr cset = 
545 
let nht = nhtInit () in 
546 
let mkCores f = 
547 
let (sort, lf) as nom = atFormulaGetNominal f in 
548 
let nomset = 
549 
match nhtFind nht nom with 
550 
 Some ns > ns 
551 
 None > 
552 
let cset1 = csetCopy cset in 
553 
csetRemDot cset1; 
554 
let bs = csetAddTBox sort cset1 in 
555 
bsetAdd bs lf; 
556 
nhtAdd nht nom bs; 
557 
bs 
558 
in 
559 
bsetAdd nomset (atFormulaGetSubformula f) 
560 
in 
561 
csetIter cset mkCores; 
562 
let inCores (sort, _) bs (isUns, acc) = 
563 
let core = insertCore sort bs in 
564 
coreAddConstraintParent core cset; 
565 
(coreGetStatus core = Unsat  isUns, core::acc) 
566 
in 
567 
let (isUnsat, children) = nhtFold inCores nht (false, []) in 
568 
if isUnsat then propagateUnsat [UCnstr cset] 
569 
else 
570 
match graphFindCnstr cset with 
571 
 Some (UnexpandedC parents) > graphReplaceCnstr cset (OpenC parents) 
572 
 _ > assert false 
573  
574  
575 
(*****************************************************************************) 
576 
(* The Main Loop *) 
577 
(*****************************************************************************) 
578  
579 
let rec expandNodesLoop () = 
580 
match queueGetElement () with 
581 
 QState state > 
582 
if stateGetStatus state = Expandable then begin 
583 
expandState state; 
584 
if doNominalPropagation () then begin 
585 
propagateNominals (); 
586 
if doSatPropagation () then propagateSat () 
587 
end else () 
588 
end else (); 
589 
expandNodesLoop () 
590 
 QCore core > 
591 
if coreGetStatus core = Expandable then begin 
592 
expandCore core; 
593 
if doNominalPropagation () then begin 
594 
propagateNominals (); 
595 
if doSatPropagation () then propagateSat () 
596 
end else () 
597 
end else (); 
598 
expandNodesLoop () 
599 
 QCnstr cset > 
600 
expandCnstr cset; 
601 
expandNodesLoop () 
602 
 QEmpty > () 
603  
604 
let rec buildGraphLoop () = 
605 
expandNodesLoop (); 
606 
propagateNominals (); 
607 
if queueIsEmpty () then () else buildGraphLoop () 
608 

609 
(** A graphtableaubased decision procedure framework for coalgebraic logics. 
610 
@param verbose An optional switch which determines 
611 
whether the procedure shall print some information on the standard output. 
612 
The default is false. 
613 
@param sorts An array mapping each sort (represented as an integer) 
614 
to a functor and a list of sorts which are the arguments of the functor. 
615 
@param nomTable A partial function mapping nominals (represented as strings) 
616 
to their sorts. 
617 
@param tbox A list of sorted formulae. 
618 
@param sf A sorted formula. 
619 
@return True if sf is satisfiable wrt tbox, false otherwise. 
620 
*) 
621 
let isSat ?(verbose = false) sorts nomTable tbox sf = 
622 
let start = if verbose then Unix.gettimeofday () else 0. in 
623 
sortTable := Array.copy sorts; 
624 
let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in 
625 
let sort = fst sf in 
626 
let bs1 = bsetAddTBox sort bs in 
627 
graphInit (); 
628 
queueInit (); 
629 
let root = insertCore sort bs1 in 
630 
graphAddRoot root; 
631 
let sat = 
632 
try 
633 
buildGraphLoop (); 
634 
match coreGetStatus (graphGetRoot ()) with 
635 
 Expandable > assert false 
636 
 Unsat > false 
637 
 Sat 
638 
 Open > true 
639 
with CoAlg_finished res > res 
640 
in 
641 
if verbose then 
642 
let stop = Unix.gettimeofday () in 
643 
let addup lst = List.fold_left (fun acc sf > acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in 
644 
print_newline (); 
645 
print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf)); 
646 
let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in 
647 
print_endline ("Added Size: " ^ (string_of_int size)); 
648 
print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1)); 
649 
let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in 
650 
print_endline ("Added Size: " ^ (string_of_int nsize)); 
651 
print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable."); 
652 
print_endline ("Time: " ^ (string_of_float (stop . start))); 
653 
print_endline ("Generated states: " ^ (string_of_int (graphSizeState ()))); 
654 
print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ()))); 
655 
print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ()))); 
656 
print_newline () 
657 
else (); 
658 
sat 