Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ e0906550

History | View | Annotate | Download (38.3 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
                if core == graphGetRoot () then raise (CoAlg_finished false) else ();
361
                let prop acc (state, idx) =
362
                  let turnsUnsat =
363
                    match stateGetStatus state with
364
                    | Open
365
                    | Expandable ->
366
                        List.for_all (fun c -> coreGetStatus c = Unsat) (snd (stateGetRule state idx))
367
                    | Unsat
368
                    | Sat -> false
369
                  in
370
                  if turnsUnsat then (UState (state, Some idx))::acc else acc
371
                in
372
                let tl2 = List.fold_left prop tl (coreGetParents core) in
373
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl2 (coreGetConstraintParents core)
374
          end
375
        | UCnstr cset ->
376
            match graphFindCnstr cset with
377
            | None
378
            | Some SatC -> assert false
379
            | Some UnsatC -> tl
380
            | Some (UnexpandedC nodes)
381
            | Some (OpenC nodes) ->
382
                graphReplaceCnstr cset UnsatC;
383
                let prop acc node =
384
                  match node with
385
                  | State state ->
386
                      let turnsUnsat =
387
                        match stateGetStatus state with
388
                        | Expandable
389
                        | Open -> cssForall isConstraintUnsat (stateGetConstraints state)
390
                        | Unsat
391
                        | Sat -> false
392
                      in
393
                      if turnsUnsat then (UState (state, None))::acc else acc
394
                  | Core core ->
395
                      let turnsUnsat =
396
                        match coreGetStatus core with
397
                        | Expandable
398
                        | Open -> cssForall isConstraintUnsat (coreGetConstraints core)
399
                        | Unsat
400
                        | Sat -> false
401
                      in
402
                      if turnsUnsat then (UCore (core, true))::acc else acc
403
                in
404
                List.fold_left prop tl nodes
405
      in
406
      propagateUnsat tl1
407

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

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

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

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

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

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

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

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

    
526
    if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) &&
527
      (setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores)
528
    then begin
529
        setIterState (fun state -> stateSetStatus state Unsat) setUnsatStates;
530
        setIterCore (fun core -> coreSetStatus core Unsat; if core == graphGetRoot () then raise (CoAlg_finished false) else ()) setUnsatCores;
531
      end else
532
      fixpointstep setUnsatStates setUnsatCores
533
  in
534
  fixpointstep (setEmptyState ()) (setEmptyCore ())
535

    
536

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

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

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

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

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

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

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

    
673

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
909

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

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

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

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

    
951

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

    
982

    
983
(*****************************************************************************)
984
(*                           The Main Loop                                   *)
985
(*****************************************************************************)
986

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

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

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

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

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

    
1052
let reasonerFinished () =
1053
  match coreGetStatus (graphGetRoot ()) with
1054
  | Expandable -> false
1055
  | Unsat
1056
  | Sat  -> true
1057
  | Open -> queueIsEmpty ()
1058

    
1059

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

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