Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 7c4d2eb4

History | View | Annotate | Download (22 KB)

1
(** A graph-tableau-based 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 graph-tableau-based 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