Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 6aa0e444

History | View | Annotate | Download (38.2 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
module CU = CoolUtils
11

    
12
type sortTable = CoAlgMisc.sortTable
13

    
14
type nomTable = string -> CoAlgFormula.sort option
15

    
16
type assumptions = CoAlgFormula.sortedFormula list
17

    
18
type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
19

    
20
exception ReasonerError of string
21

    
22
(*****************************************************************************)
23
(*                     Propagation of Satisfiability                         *)
24
(*****************************************************************************)
25

    
26
let propSatFindSucc setCnstr cset =
27
  if csetHasDot cset then false
28
  else
29
    match graphFindCnstr cset with
30
    | None -> raise (ReasonerError "?")
31
    | Some SatC -> true
32
    | Some (OpenC _) -> setMemCnstr setCnstr cset
33
    | Some (UnexpandedC _)
34
    | Some UnsatC -> false
35

    
36

    
37
let rec propSat setStates setCores setCnstr = function
38
  | [] -> ()
39
  | propElem::tl ->
40
      let tl1 =
41
        match propElem with
42
        | UState (state, _) ->
43
            if setMemState setStates state then
44
              let cnstrs = stateGetConstraints state in
45
              let isStillOpen = cssExists (fun c -> propSatFindSucc setCnstr c) cnstrs in
46
              if isStillOpen then () else setRemoveState setStates state
47
            else ();
48
            tl
49
        | UCore (core, _) ->
50
            if setMemCore setCores core then
51
              let cnstrs = coreGetConstraints core in
52
              let isStillOpen = cssExists (fun c -> propSatFindSucc setCnstr c) cnstrs in
53
              if isStillOpen then tl else begin
54
                setRemoveCore setCores core;
55
                let cnstrPar = coreGetConstraintParents core in
56
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl cnstrPar
57
              end
58
            else tl
59
        | UCnstr cset ->
60
            if setMemCnstr setCnstr cset then begin
61
              setRemoveCnstr setCnstr cset;
62
              match graphFindCnstr cset with
63
              | Some (OpenC nodes) ->
64
                  let prop acc node =
65
                    match node with
66
                    | Core core -> (UCore (core, true))::acc
67
                    | State state -> (UState (state, None))::acc
68
                  in
69
                  List.fold_left prop tl nodes
70
              | _ -> assert false
71
            end else tl
72
      in
73
      propSat setStates setCores setCnstr tl1
74

    
75
let propagateSat () =
76
  let setStates = setEmptyState () in
77
  let setCores = setEmptyCore () in
78
  let setCnstr = setEmptyCnstr () in
79
  let fktS1 state =
80
    match stateGetStatus state with
81
    | Expandable
82
    | Open -> setAddState setStates state
83
    | Unsat
84
    | Sat -> ()
85
  in
86
  graphIterStates fktS1;
87
  let fktC1 core =
88
    match coreGetStatus core with
89
    | Expandable
90
    | Open -> setAddCore setCores core
91
    | Unsat
92
    | Sat -> ()
93
  in
94
  graphIterCores fktC1;
95
  let cfkt1 cset cnstr =
96
    if csetHasDot cset then ()
97
    else
98
      match cnstr with
99
      | OpenC _ -> setAddCnstr setCnstr cset
100
      | UnsatC
101
      | SatC
102
      | UnexpandedC _ -> ()
103
  in
104
  graphIterCnstrs cfkt1;
105
  graphIterStates (fun state -> propSat setStates setCores setCnstr [UState (state, None)]);
106
  graphIterCores (fun core -> propSat setStates setCores setCnstr [UCore (core, false)]);
107
  setIterState (fun state -> stateSetStatus state Sat) setStates;
108
  let setCoreSat core =
109
    coreSetStatus core Sat;
110
    if core == graphGetRoot () then raise (CoAlg_finished true) else ()
111
  in
112
  setIterCore setCoreSat setCores;
113
  setIterCnstr (fun cset -> graphReplaceCnstr cset SatC) setCnstr
114

    
115

    
116
let propagateSatMu () =
117
  let setFinishingStates = setEmptyState () in
118
  let setFinishingCores = setEmptyCore () in
119
  let setStates = setEmptyState () in
120
  let setCores = setEmptyCore () in
121
  let emptySet = bsetMakeRealEmpty () in
122
  let openstates = ref 0 in
123

    
124
  (* Collect two sets of nodes. All nodes that may be satisfiable
125
   * after this iteration are collected into setStates/setCores.
126
   *
127
   * As every cycle containing a node with empty focus or an
128
   * satisfiable node should be considered satisfiable, collect these
129
   * decisive nodes into setFinishingStates/setFinishingCores
130
   *
131
   * This also marks in trivial cases nodes as satisfiable.
132
   *)
133
  let stateCollector state =
134
    match stateGetStatus state with
135
    | Unsat -> ()
136
    | Sat ->
137
       setAddState setStates state;
138
      setAddState setFinishingStates state
139
    | Expandable -> ()
140
    | Open ->
141
       openstates := !openstates + 1;
142
       if List.length (stateGetRules state) == 0 || (* States with no rules are satisfiable *)
143
         bsetCompare (bsetMake ()) (stateGetBs state) == 0 (* KD generates nodes with just True as formula *)
144
       then begin
145
         setAddState setFinishingStates state;
146
         stateSetStatus state Sat
147
       end else begin
148
         setAddState setStates state;
149
         if bsetCompare (stateGetDeferral state) emptySet == 0
150
         then begin
151
           setAddState setFinishingStates state
152
         end
153
         else ()
154
       end
155

    
156
  (* As it is enough for a core to have one successfull child, we can
157
   * also handle (some) expandable cores.
158
   *)
159
  and coreCollector core =
160
    match coreGetStatus core with
161
    | Unsat -> ()
162
    | Sat ->
163
       setAddCore setCores core;
164
       setAddCore setFinishingCores core
165
    | Expandable
166
    | Open ->
167
       setAddCore setCores core;
168
      if bsetCompare (coreGetDeferral core) emptySet == 0
169
      then begin
170
        setAddCore setFinishingCores core
171
      end
172
      else ()
173
  in
174
  graphIterStates stateCollector;
175
  graphIterCores coreCollector;
176

    
177
  setPropagationCounter !openstates;
178

    
179
  (* In a fixpoint the set called setStates / setCores is narrowed
180
   * down.
181
   *
182
   * In each step only those states and cores are retained in setStates
183
   * / setCores which reach one of setFinishing{States,Cores} in
184
   * finitely many steps. This new set of States / Cores is collected
185
   * as allowed{States,Cores} during each fixpoint iteration.
186
   *
187
   * Only those finishing nodes are retained that have allowed or
188
   * Successfull Children.
189
   *)
190
  let rec fixpointstep setStates setCores =
191
    let allowedStates = setEmptyState () in
192
    let allowedCores = setEmptyCore () in
193

    
194
    let rec visitParentStates (core : core) : unit =
195
      if not (setMemCore allowedCores core)
196
      then begin
197
        setAddCore allowedCores core;
198
        let verifyParent (state,_) =
199
          let rules = stateGetRules state in
200
          let ruleiter (dependencies, corelist) =
201
            List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat)
202
              corelist
203
          in
204
          if List.for_all ruleiter rules
205
          then visitParentCores state
206
        in
207
        List.iter verifyParent (coreGetParents core)
208
      end
209

    
210
    and visitParentCores (state : state) : unit =
211
      if not (setMemState allowedStates state)
212
      then begin
213
        setAddState allowedStates state;
214
        let verifyParent core =
215
          let acceptable =
216
            List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
217
              (coreGetChildren core)
218
          in
219
          if acceptable
220
          then visitParentStates core
221
        in
222
        List.iter verifyParent (stateGetParents state)
223
      end
224
    in
225

    
226
    (* All rule applications need to still be potentially Sat for a
227
     * finishing State to be a valid startingpoint for this fixpoint.
228
     *)
229
    let checkFinishingState (state : state) =
230
      let ruleiter (dependencies, corelist) : bool =
231
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist
232
      in
233
      if not (List.exists ruleiter (stateGetRules state)) then begin
234
        visitParentCores state
235
      end
236

    
237
    (* There needs to be a State still potentially Sat for this core
238
     * to be considered for the fixpoint
239
     *)
240
    and checkFinishingCore (core : core) =
241
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state))
242
                           (coreGetChildren core))
243
      then begin
244
        visitParentStates core
245
      end
246
    in
247
    setIterState checkFinishingState setFinishingStates;
248
    setIterCore checkFinishingCore setFinishingCores;
249

    
250

    
251
    if (setLengthState setStates) = (setLengthState allowedStates) &&
252
         (setLengthCore setCores) = (setLengthCore allowedCores)
253
    then begin
254
        setIterState (fun state -> stateSetStatus state Sat) setStates;
255
        setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot () then raise (CoAlg_finished true) else ()) setCores;
256
      end else
257
      fixpointstep allowedStates allowedCores
258
  in
259
  fixpointstep setStates setCores
260

    
261

    
262
(*****************************************************************************)
263
(*                     Propagation of Unsatisfiability                       *)
264
(*****************************************************************************)
265

    
266
let isConstraintUnsat cset =
267
  match graphFindCnstr cset with
268
  | None -> assert false
269
  | Some UnsatC -> true
270
  | _ -> false
271

    
272
let fhtMustFind fht f =
273
  match fhtFind fht f with
274
  | Some l -> l
275
  | None -> assert false
276

    
277
let lhtMustFind lht l =
278
  match lhtFind lht l with
279
  | Some f -> f
280
  | None -> assert false
281

    
282

    
283
(* Gets a list of Things we know are unsatisfiable and propagates this
284
   information backwards *)
285
let rec propagateUnsat = function
286
  | [] -> ()
287
  | propElem::tl ->
288
      let tl1 =
289
        match propElem with
290
        | UState (state, idxopt) -> begin
291
            match stateGetStatus state with
292
            | Unsat -> tl
293
            | Sat -> raise (ReasonerError ("Propagation tells state "
294
                                           ^(string_of_int (stateGetIdx state))
295
                                           ^" would be unsat, but it is already sat"))
296
            | Open
297
            | Expandable ->
298
                let mbs =
299
                  match idxopt with
300
                  | None -> stateGetBs state
301
                  | Some idx ->
302
                      let (dep, children) = stateGetRule state idx in
303
                      let getBs core =
304
                        assert (coreGetStatus core = Unsat);
305
                        coreGetBs core
306
                      in
307
                      dep (List.map getBs children)
308
                in
309
                stateSetBs state mbs;
310
                stateSetStatus state Unsat;
311
                let prop acc core =
312
                  let turnsUnsat =
313
                    match coreGetStatus core with
314
                    | Open -> List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core)
315
                    | Expandable
316
                    | Unsat
317
                    | Sat -> false
318
                  in
319
                  if turnsUnsat then (UCore (core, false))::acc else acc
320
                in
321
                List.fold_left prop tl (stateGetParents state)
322
          end
323
        | UCore (core, comesFromCnstr) -> begin
324
            match coreGetStatus core with
325
            | Unsat -> tl
326
            | Sat -> raise (ReasonerError ("Propagation tells core "
327
                                           ^(string_of_int (coreGetIdx core))
328
                                           ^" would be unsat, but it is already sat"))
329
            | Open
330
            | Expandable ->
331
                let mbs =
332
                  if comesFromCnstr then coreGetBs core
333
                  else
334
                    let bs = coreGetBs core in
335
                    let Some solver = coreGetSolver core in
336
                    let fht = coreGetFht core in
337
                    let lht = lhtInit () in
338
                    let addLits f acc =
339
                      let lit = fhtMustFind fht f in
340
                      lhtAdd lht lit f;
341
                      lit::acc
342
                    in
343
                    let litset = bsetFold addLits bs [] in
344
                    let addClauses state =
345
                      let cbs = stateGetBs state in
346
                      let clause = bsetFold (fun f acc -> (M.neg_lit (fhtMustFind fht f))::acc) cbs [] in
347
                      let okay = M.add_clause solver clause in
348
                      assert okay
349
                    in
350
                    List.iter addClauses (coreGetChildren core);
351
                    let isSat = M.invoke_solver solver litset in
352
                    assert (not isSat);
353
                    let res = bsetMake () in
354
                    let confls = M.get_conflict solver in
355
                    List.iter (fun l -> bsetAdd res (lhtMustFind lht l)) confls;
356
                    res
357
                in
358
                coreSetBs core mbs;
359
                coreSetStatus core Unsat;
360
                coreDeallocateSolver core;
361
                if core == graphGetRoot () then raise (CoAlg_finished false) else ();
362
                let prop acc (state, idx) =
363
                  let turnsUnsat =
364
                    match stateGetStatus state with
365
                    | Open
366
                    | Expandable ->
367
                        List.for_all (fun c -> coreGetStatus c = Unsat) (snd (stateGetRule state idx))
368
                    | Unsat
369
                    | Sat -> false
370
                  in
371
                  if turnsUnsat then (UState (state, Some idx))::acc else acc
372
                in
373
                let tl2 = List.fold_left prop tl (coreGetParents core) in
374
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl2 (coreGetConstraintParents core)
375
          end
376
        | UCnstr cset ->
377
            match graphFindCnstr cset with
378
            | None
379
            | Some SatC -> assert false
380
            | Some UnsatC -> tl
381
            | Some (UnexpandedC nodes)
382
            | Some (OpenC nodes) ->
383
                graphReplaceCnstr cset UnsatC;
384
                let prop acc node =
385
                  match node with
386
                  | State state ->
387
                      let turnsUnsat =
388
                        match stateGetStatus state with
389
                        | Expandable
390
                        | Open -> cssForall isConstraintUnsat (stateGetConstraints state)
391
                        | Unsat
392
                        | Sat -> false
393
                      in
394
                      if turnsUnsat then (UState (state, None))::acc else acc
395
                  | Core core ->
396
                      let turnsUnsat =
397
                        match coreGetStatus core with
398
                        | Expandable
399
                        | Open -> cssForall isConstraintUnsat (coreGetConstraints core)
400
                        | Unsat
401
                        | Sat -> false
402
                      in
403
                      if turnsUnsat then (UCore (core, true))::acc else acc
404
                in
405
                List.fold_left prop tl nodes
406
      in
407
      propagateUnsat tl1
408

    
409
let propagateUnsatMu () =
410
  let setFinishingStates = setEmptyState () in
411
  let setFinishingCores = setEmptyCore () in
412
  let setStates = setEmptyState () in
413
  let setCores = setEmptyCore () in
414
  let emptySet = bsetMakeRealEmpty () in
415

    
416
  (* Collect two sets of nodes. All nodes that may be unsatisfiable
417
   * after this iteration are collected into setStates/setCores.
418
   *
419
   * Nodes reaching Points with empty focus as well as Expandable nodes
420
   * (if not Unsat) can not be declared Unsat so we collect these into
421
   * setFinishingStates/setFinishingCores.
422
   *)
423
  let stateCollector state =
424
    match stateGetStatus state with
425
    | Unsat -> ()
426
    | Sat
427
    | Expandable ->
428
       setAddState setStates state;
429
      setAddState setFinishingStates state
430
    | Open ->
431
       setAddState setStates state;
432
      if bsetCompare (stateGetDeferral state) emptySet == 0
433
      then begin
434
        setAddState setFinishingStates state
435
      end
436
      else ()
437

    
438
  and coreCollector core =
439
    match coreGetStatus core with
440
    | Unsat -> ()
441
    | Expandable
442
    | Sat ->
443
       setAddCore setCores core;
444
      setAddCore setFinishingCores core
445
    | Open ->
446
       setAddCore setCores core;
447
      if bsetCompare (coreGetDeferral core) emptySet == 0
448
      then begin
449
        setAddCore setFinishingCores core
450
      end
451
      else ()
452
  in
453
  graphIterStates stateCollector;
454
  graphIterCores coreCollector;
455

    
456
  (* In a fixpoint the set called setFinishingStates/setFinishingCores
457
   * is narrowed down
458
   *
459
   * In each iteration we start with all Nodes and remove all that can
460
   * reach a finishing Node. We then remove all finishing Nodes from the
461
   * respective set which are becoming Unsat and start with the next
462
   * iteration until the fixpoint is reached
463
   *
464
   *
465
   *)
466
  let rec fixpointstep setPrevUnsatStates setPrevUnsatCores =
467
    let setUnsatStates = setCopyState setStates in
468
    let setUnsatCores = setCopyCore setCores in
469

    
470
    let rec visitParentStates (core : core) : unit =
471
      if setMemCore setUnsatCores core
472
      then begin
473
        setRemoveCore setUnsatCores core;
474
        let verifyParent (state,_) =
475
          let rules = stateGetRules state in
476
          let ruleiter (dependencies, corelist) =
477
            List.exists (fun (core : core) -> not (setMemCore setUnsatCores core) || coreGetStatus core == Sat)
478
              corelist
479
          in
480
          if List.for_all ruleiter rules
481
          then visitParentCores state
482
        in
483
        List.iter verifyParent (coreGetParents core)
484
      end
485

    
486
    and visitParentCores (state : state) : unit =
487
      if setMemState setUnsatStates state
488
      then begin
489
        setRemoveState setUnsatStates state;
490
        let verifyParent core =
491
          let acceptable =
492
            List.exists (fun (state : state) -> not (setMemState setUnsatStates state) || stateGetStatus state == Sat)
493
              (coreGetChildren core)
494
          in
495
          if acceptable
496
          then visitParentStates core
497
        in
498
        List.iter verifyParent (stateGetParents state)
499
      end
500
    in
501

    
502
    (* All rule applications need to still be potentially Sat for a
503
     * finishing State to be a valid startingpoint for this fixpoint.
504
     *)
505
    let checkFinishingState (state : state) =
506
      let ruleiter (dependencies, corelist) : bool =
507
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || setMemCore setPrevUnsatCores core) corelist
508
      in
509
      if not (List.exists ruleiter (stateGetRules state)) || stateGetStatus state == Expandable then begin
510
        visitParentCores state
511
      end
512

    
513
    (* There needs to be a State still potentially Sat for this core
514
     * to be considered for the fixpoint
515
     *)
516
    and checkFinishingCore (core : core) =
517
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || setMemState setPrevUnsatStates state)
518
                (coreGetChildren core)) ||
519
        coreGetStatus core == Expandable
520
      then begin
521
        visitParentStates core
522
      end
523
    in
524
    setIterState checkFinishingState setFinishingStates;
525
    setIterCore checkFinishingCore setFinishingCores;
526

    
527
    if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) &&
528
      (setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores)
529
    then begin
530
        setIterState (fun state -> stateSetStatus state Unsat) setUnsatStates;
531
        setIterCore (fun core -> propagateUnsat [UCore (core, false)]) setUnsatCores;
532
      end else
533
      fixpointstep setUnsatStates setUnsatCores
534
  in
535
  fixpointstep (setEmptyState ()) (setEmptyCore ())
536

    
537

    
538
(*****************************************************************************)
539
(*                   Propagation of Nominal Constraints                      *)
540
(*****************************************************************************)
541

    
542
let extractAts sort bs =
543
  let ats = csetMake () in
544
  let procNom nom f =
545
    match lfGetType sort f with
546
    | AndF
547
    | OrF -> ()
548
    | TrueFalseF
549
    | AtF -> ()
550
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
551
  in
552
  let getAts f =
553
    match lfGetType sort f with
554
    | AtF -> csetAdd ats (lfToAt sort f)
555
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
556
    | _ -> ()
557
  in
558
  bsetIter getAts bs;
559
  ats
560

    
561
let detConstraintsState state =
562
  let procRule accR (_, chldrn) =
563
    let procChldrn accC core =
564
      if coreGetStatus core = Unsat then accC
565
      else cssUnion accC (coreGetConstraints core)
566
    in
567
    let orset = List.fold_left procChldrn cssEmpty chldrn in
568
    let procOrset csetO accO =
569
      let mkUnion csetU accU =
570
        let cset = csetUnion csetO csetU in
571
        cssAdd cset accU
572
      in
573
      cssFold mkUnion accR accO
574
    in
575
    cssFold procOrset orset cssEmpty
576
  in
577
  let sort = stateGetSort state in
578
  let bs = stateGetBs state in
579
  let ats = extractAts sort bs in
580
  if stateGetStatus state = Expandable then csetAddDot ats else ();
581
  List.fold_left procRule (cssSingleton ats) (stateGetRules state)
582

    
583
let detConstraintsCore core =
584
  let sort = coreGetSort core in
585
  let bs = coreGetBs core in
586
  let ats = extractAts sort bs in
587
  let addCnstr acc state =
588
    if stateGetStatus state = Unsat then acc
589
    else
590
      let csets = stateGetConstraints state in
591
      (* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *)
592
      cssUnion csets acc
593
  in
594
  let initInner =
595
    if coreGetStatus core = Expandable then
596
      (* let cset = csetCopy ats in *)
597
      let cset = ats in
598
      csetAddDot cset;
599
      cssSingleton cset
600
    else cssEmpty
601
  in
602
  List.fold_left addCnstr initInner (coreGetChildren core)
603

    
604
let rec propNom = function
605
  | [] -> ()
606
  | node::tl ->
607
      let tl1 =
608
        match node with
609
        | State state ->
610
            if stateGetStatus state = Unsat then tl
611
            else
612
              let csets = detConstraintsState state in
613
              let oldcsets = stateGetConstraints state in
614
              if cssEqual csets oldcsets then tl
615
              else begin
616
                stateSetConstraints state csets;
617
                List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state)
618
              end
619
        | Core core ->
620
            if coreGetStatus core = Unsat then tl
621
            else
622
              let csets = detConstraintsCore core in
623
              let oldcsets = coreGetConstraints core in
624
              if cssEqual csets oldcsets then tl
625
              else begin
626
                coreSetConstraints core csets;
627
                List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core)
628
              end
629
      in
630
      propNom tl1
631

    
632
let updateConstraints node elemU csets =
633
  let update cset acc =
634
    let cnstr =
635
      match graphFindCnstr cset with
636
      | Some cn -> cn
637
      | None ->
638
          let cn = UnexpandedC [] in
639
          graphInsertCnstr cset cn;
640
          queueInsertCnstr cset;
641
          cn
642
    in
643
    match cnstr with
644
    | UnsatC -> acc
645
    | UnexpandedC parents ->
646
        graphReplaceCnstr cset (UnexpandedC (node::parents));
647
        false
648
    | OpenC parents ->
649
        graphReplaceCnstr cset (OpenC (node::parents));
650
        false
651
    | SatC -> false
652
  in
653
  let isUnsat = cssFold update csets true in
654
  if isUnsat then propagateUnsat [elemU] else ()
655

    
656
let propagateNominals () =
657
  let init = cssSingleton (csetMake ()) in
658
  graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init);
659
  graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init);
660
  graphIterStates (fun s -> propNom [State s]);
661
  graphIterCores (fun c -> propNom [Core c]);
662
  graphClearCnstr ();
663
  let fktS state =
664
    if stateGetStatus state = Unsat then ()
665
    else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state)
666
  in
667
  graphIterStates fktS;
668
  let fktC core =
669
    if coreGetStatus core = Unsat then ()
670
    else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core)
671
  in
672
  graphIterCores fktC
673

    
674

    
675
(*****************************************************************************)
676
(*                           Node Expansions                                 *)
677
(*****************************************************************************)
678

    
679
let getLit sort fht solver f =
680
  match fhtFind fht f with
681
  | Some lit -> lit
682
  | None ->
683
      let var = M.new_variable solver in
684
      let lit = M.var_to_lit var true in
685
      fhtAdd fht f lit;
686
      let () =
687
        match lfGetNeg sort f with
688
        | None -> ()
689
        | Some nf ->
690
            let nlit = M.neg_lit lit in
691
            fhtAdd fht nf nlit;
692
      in
693
      lit
694

    
695
let newCore sort bs defer =
696
  (* when creating a now core from a set of formulas bs
697
        bs = { x_1, ...., x_n }
698
           = "x_1 /\ .... /\ x_n"
699
     Then we do this by:
700

    
701
        1. creating a new literal in the sat solver for each
702
           "boolean subformula" from the x_i. "boolean subformula" means that
703
           this subformula is not hidden under modalities but only under
704
           boolean connectives (/\, \/).
705
        2. encoding the relation between a formula and its intermediate boolean
706
           subformulas by a clause:
707
  *)
708
  let fht = fhtInit () in
709
  let solver = M.new_solver () in
710
  let rec addClauses f =
711
    (* step 1: create a literal in the satsolver representing the formula f *)
712
    let lf = getLit sort fht solver f in
713
    (* step 2: encode relation to possible subformulas *)
714
    match lfGetType sort f with
715
    | OrF ->
716
        (*
717
           case 2.(a)   f =  f1 \/ f2
718
                   fill fht such that it says:
719

    
720
                        f  |---> lf
721
                        f1 |---> lf1
722
                        f2 |---> lf2
723
        *)
724
        let f1 = lfGetDest1 sort f in
725
        let f2 = lfGetDest2 sort f in
726
        addClauses f1;
727
        addClauses f2;
728
        let lf1 = fhtMustFind fht f1 in
729
        let lf2 = fhtMustFind fht f2 in
730
        (*
731
            encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
732
        *)
733
        let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
734
        assert (okay)
735
    | AndF ->
736
        (*
737
           case 2.(b)   f =  f1 /\ f2
738
                   fill fht such that it says:
739

    
740
                        f  |---> lf
741
                        f1 |---> lf1
742
                        f2 |---> lf2
743
        *)
744
        let f1 = lfGetDest1 sort f in
745
        let f2 = lfGetDest2 sort f in
746
        addClauses f1;
747
        addClauses f2;
748
        let lf1 = fhtMustFind fht f1 in
749
        let lf2 = fhtMustFind fht f2 in
750
        (*
751
            encode the structure of f by adding the clauses
752
                    (lf -> lf1) /\ (lf -> lf2)
753
        *)
754
        let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
755
        assert (okay1);
756
        let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
757
        assert (okay2)
758
    | MuF
759
    | NuF ->
760
       (*
761
          Dest of a fixpoint is it's unfolded version. This adds just
762
          an simple forward implication that could be optimised out
763
          though not without nontrivial transformation of code
764

    
765
            f = μ X . φ   |---> lf
766
            φ[X |-> f]    |---> lf1
767

    
768
          Then adding lf -> lf1 to minisat
769
        *)
770
       let f1 = lfGetDest1 sort f in
771
       addClauses f1;
772
       let lf1 = fhtMustFind fht f1 in
773
       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
774
       assert (okay1);
775
    | _ -> ()
776
        (* case 2.(c)
777
            We don't need to do anything except adding f to the fht
778
        *)
779
  in
780
  bsetIter addClauses bs;
781
  coreMake sort bs defer (Some solver) fht
782

    
783
let getNextState core =
784
  (* Create a new state, which is obtained by a satisfying assignment of the
785
     literals of the minisat solver.
786
     In addition to that, feed the negation of the satisfying assignment back
787
     to the minisat solver in order to obtain different solutions on successive
788
     minisat calls.
789
  *)
790
  let bs = coreGetBs core in
791
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
792
  let deferralS =
793
    if refocusing then
794
      bsetCopy bs
795
    else
796
      coreGetDeferral core
797
  in
798
  let fht = coreGetFht core in
799
  let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
800
  let Some solver = coreGetSolver core in
801
  let isSat = M.invoke_solver solver litset in
802
  (* Clearly, if the current core is unsatisfiable, no further child state can
803
     be created *)
804
  if not isSat then None
805
  else
806
    let sort = coreGetSort core in
807
    (* create a new set of formulas newbs with the property:
808
       if the conjunction of newbs is satisfiable, then the present core is
809
       satisfiable.
810
    *)
811
    let newbs = bsetMake () in
812
    let newdefer = bsetMakeRealEmpty () in
813
    (* if newbs = { l_1, .... l_n }, i.e.
814

    
815
            newbs = l_1 /\ ... /\ l_n
816

    
817
       then we can get essentially different satisfying assignments of bs by
818
       adding another clause
819

    
820
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
821

    
822
       By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
823
    *)
824
    let rec mkExclClause deferral f acc =
825
      (* f is a formula that is true in the current satisfying assignment *)
826
      match lfGetType sort f with
827
      | OrF ->
828
          (* if f is true and a disjunction, then one of its disjuncts is true *)
829
          let f1 = lfGetDest1 sort f in
830
          let lf1 = fhtMustFind fht f1 in
831
          (* if the first disjunct f1 is true, then we need to add subformulas
832
             of f1 to newbs&clause *)
833
          if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
834
          else
835
            (* otherwise f2 must be true *)
836
            let f2 = lfGetDest2 sort f in
837
            let lf2 = fhtMustFind fht f2 in
838
            assert (M.literal_status solver lf2 = M.LTRUE);
839
            mkExclClause deferral f2 acc
840
      | AndF ->
841
          (* if the true f is a conjuction, then both conjunctions must be true *)
842
          let f1 = lfGetDest1 sort f in
843
          let lf1 = fhtMustFind fht f1 in
844
          assert (M.literal_status solver lf1 = M.LTRUE);
845
          let acc1 = mkExclClause deferral f1 acc in
846
          let f2 = lfGetDest2 sort f in
847
          let lf2 = fhtMustFind fht f2 in
848
          assert (M.literal_status solver lf2 = M.LTRUE);
849
          mkExclClause deferral f2 acc1
850
      | MuF
851
      | NuF ->
852
         let f1 = lfGetDest1 sort f in
853
         mkExclClause deferral f1 acc
854
      | _ ->
855
         (* if f is a trivial formula or modality, then add it ... *)
856
         (* ... to newbs *)
857
         bsetAdd newbs f;
858
         let defercandidate = lfGetDeferral sort f in
859
         (if (defercandidate != (Hashtbl.hash "ε") &&
860
                (refocusing || deferral = defercandidate)) then
861
            bsetAdd newdefer f);
862
         (* ... and to the new clause *)
863
         (M.neg_lit (fhtMustFind fht f))::acc
864
    in
865
    let init_clause f acc =
866
      let deferral =
867
        (* for each deferral determine which variable it belongs to *)
868
        if bsetMem deferralS f then (
869
          lfGetDeferral sort f)
870
        else
871
          (Hashtbl.hash "ε")
872
      in
873
      mkExclClause deferral f acc
874
    in
875
    let clause = bsetFold init_clause bs [] in
876
    let okay = M.add_clause solver clause in
877
    assert (okay);
878
    Some (sort, newbs, newdefer)
879

    
880
let newState sort bs defer =
881
  let (func, sl) = !sortTable.(sort) in
882
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
883
  let exp = producer sort bs defer sl in
884
  stateMake sort bs defer exp
885

    
886
let insertState parent sort bs defer =
887
  let child =
888
    match graphFindState sort (bs, defer) with
889
    | None ->
890
        let s = newState sort bs defer in
891
        graphInsertState sort (bs, defer) s;
892
        queueInsertState s;
893
        s
894
    | Some s -> s
895
  in
896
  coreAddChild parent child;
897
  stateAddParent child parent
898

    
899
let expandCore core =
900
  match getNextState core with
901
  | Some (sort, bs, defer) ->
902
      insertState core sort bs defer;
903
      queueInsertCore core
904
  | None ->
905
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
906
      if isUnsat
907
      then
908
          propagateUnsat [UCore (core, false)]
909
      else
910
          coreSetStatus core Open
911

    
912

    
913
let insertCore sort bs defer =
914
  match graphFindCore sort (bs, defer) with
915
  | None ->
916
     let c = newCore sort bs defer in
917
     graphInsertCore sort (bs, defer) c;
918
     queueInsertCore c;
919
     c
920
  | Some c -> c
921

    
922
let insertRule state dep chldrn =
923
  let chldrn = listFromLazylist chldrn in
924
  let insert (isUns, acc) (sort, bs, defer) =
925
    let bs1 = bsetAddTBox sort bs in
926
    let core = insertCore sort bs1 defer in
927
    let isUns1 = if coreGetStatus core = Unsat then isUns else false in
928
    (isUns1, core::acc)
929
  in
930
  let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
931
  let idx = stateAddRule state dep (List.rev children) in
932
  List.iter (fun c -> coreAddParent c state idx) children;
933
  if isUnsat then begin
934
    propagateUnsat [UState (state, Some idx)];
935
    false
936
  end else true
937

    
938
let rec insertAllRules state = function
939
  | [] -> true
940
  | (dep, chldrn)::tl ->
941
      let notUnsat = insertRule state dep chldrn in
942
      if notUnsat then insertAllRules state tl else false
943

    
944
let expandState state =
945
  match stateNextRule state with
946
  | MultipleElements rules ->
947
      let notUnsat = insertAllRules state rules in
948
      if notUnsat then stateSetStatus state Open
949
  | SingleElement (dep, chldrn) ->
950
      let notUnsat = insertRule state dep chldrn in
951
      if notUnsat then queueInsertState state else ()
952
  | NoMoreElements -> stateSetStatus state Open
953

    
954

    
955
let expandCnstr cset =
956
  let nht = nhtInit () in
957
  let mkCores f =
958
    let (sort, lf) as nom = atFormulaGetNominal f in
959
    let nomset =
960
      match nhtFind nht nom with
961
      | Some ns -> ns
962
      | None ->
963
          let cset1 = csetCopy cset in
964
          csetRemDot cset1;
965
          let bs = csetAddTBox sort cset1 in
966
          bsetAdd bs lf;
967
          nhtAdd nht nom bs;
968
          bs
969
    in
970
    bsetAdd nomset (atFormulaGetSubformula f)
971
  in
972
  csetIter cset mkCores;
973
  let inCores (sort, _) bs (isUns, acc) =
974
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
975
    coreAddConstraintParent core cset;
976
    (coreGetStatus core = Unsat || isUns, core::acc)
977
  in
978
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
979
  if isUnsat then propagateUnsat [UCnstr cset]
980
  else
981
    match graphFindCnstr cset with
982
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
983
    | _ -> assert false
984

    
985

    
986
(*****************************************************************************)
987
(*                           The Main Loop                                   *)
988
(*****************************************************************************)
989

    
990
let expandNodesLoop (recursiveAction: unit -> unit) =
991
  match queueGetElement () with
992
  | QState state ->
993
      if stateGetStatus state = Expandable then begin
994
        expandState state;
995
        if doNominalPropagation () then begin
996
          (* propagateNominals (); *)
997
          if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
998
        end else ()
999
      end else ();
1000
      recursiveAction ()
1001
  | QCore core ->
1002
      if coreGetStatus core = Expandable then begin
1003
        expandCore core;
1004
        if doNominalPropagation () then begin
1005
          (* propagateNominals (); *)
1006
          if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
1007
        end else ()
1008
      end else ();
1009
      recursiveAction ()
1010
  | QCnstr cset ->
1011
      expandCnstr cset;
1012
      recursiveAction ()
1013
  | QEmpty -> ()
1014

    
1015
let runReasonerStep () =
1016
  let void () = () in
1017
  expandNodesLoop void; (* expand at most one node *)
1018
  (* if this emptied the queue *)
1019
  if queueIsEmpty () then begin
1020
    (* then check whether the nominals would add further queue elements *)
1021
    (* print_endline "Propagating nominals..."; *)
1022
    (* propagateNominals () *)
1023
  end else () (* else: the next step would be to expand another node *)
1024

    
1025
let rec buildGraphLoop () =
1026
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
1027
  expandNodesFurther (); (* expand as many queue elements as possible *)
1028
  (* propagateNominals (); *)
1029
  (* if propagating nominals added some more queue members, do all again.. *)
1030
  if queueIsEmpty () then () else buildGraphLoop ()
1031

    
1032
let initReasoner sorts nomTable tbox sf =
1033
  sortTable := Array.copy sorts;
1034
  let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
1035
  let sort = fst sf in
1036
  let bs1 = bsetAddTBox sort bs in
1037
  let deferrals = bsetMakeRealEmpty() in
1038
  let markDeferral f =
1039
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
1040
      bsetAdd deferrals f;)
1041
  in
1042
  bsetIter markDeferral bs;
1043
  graphInit ();
1044
  queueInit ();
1045
  let root = insertCore sort bs1 deferrals in
1046
  graphAddRoot root
1047

    
1048
let isRootSat () =
1049
  match coreGetStatus (graphGetRoot ()) with
1050
  | Expandable -> None
1051
  | Unsat -> Some false
1052
  | Sat -> Some true
1053
  | Open -> if (queueIsEmpty()) then Some true else None
1054

    
1055
let reasonerFinished () =
1056
  match coreGetStatus (graphGetRoot ()) with
1057
  | Expandable -> false
1058
  | Unsat
1059
  | Sat  -> true
1060
  | Open -> queueIsEmpty ()
1061

    
1062

    
1063
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
1064
    @param verbose An optional switch which determines
1065
    whether the procedure shall print some information on the standard output.
1066
    The default is false.
1067
    @param sorts An array mapping each sort (represented as an integer)
1068
    to a functor and a list of sorts which are the arguments of the functor.
1069
    @param nomTable A partial function mapping nominals (represented as strings)
1070
    to their sorts.
1071
    @param tbox A list of sorted formulae.
1072
    @param sf A sorted formula.
1073
    @return True if sf is satisfiable wrt tbox, false otherwise.
1074
 *)
1075

    
1076
let isSat ?(verbose = false) sorts nomTable tbox sf =
1077
  let start = if verbose then Unix.gettimeofday () else 0. in
1078
  initReasoner sorts nomTable tbox sf;
1079
  let sat =
1080
    try
1081
      buildGraphLoop ();
1082
      propagateUnsatMu ();
1083
      (* get whether the root is satisfiable *)
1084
      (* we know that the reasoner finished, so the value is there, *)
1085
      (* i.e. isRootSat() will give a "Some x" and not "None" *)
1086
      CU.fromSome (isRootSat())
1087
    with CoAlg_finished res -> res
1088
  in
1089
  (* print some statistics *)
1090
  if verbose then
1091
    let stop = Unix.gettimeofday () in
1092
    let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
1093
    print_newline ();
1094
    print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
1095
    let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
1096
    print_endline ("Added Size: " ^ (string_of_int size));
1097
    (*
1098
    print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
1099
    let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
1100
    print_endline ("Added Size: " ^ (string_of_int nsize));
1101
    *)
1102
    print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
1103
    print_endline ("Time: " ^ (string_of_float (stop -. start)));
1104
    print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
1105
    print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ())));
1106
    print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ())));
1107
    print_newline ()
1108
  else ();
1109
  sat