Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 3c05e89f

History | View | Annotate | Download (33.7 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

    
123
  let stateCollector state =
124
    match stateGetStatus state with
125
    | Unsat -> ()
126
    | Sat ->
127
       setAddState setStates state;
128
       setAddState setFinishingStates state
129
    | Expandable -> ()
130
    | Open ->
131
       if stateGetStatus state == Open && List.length (stateGetRules state) == 0 || bsetCompare (bsetMake ()) (stateGetBs state) == 0
132
       then begin
133
         setAddState setFinishingStates state;
134
         stateSetStatus state Sat
135
       end else begin
136
         setAddState setStates state;
137
         if bsetCompare (stateGetDeferral state) emptySet == 0
138
         then begin
139
           print_endline (stateToString state);
140
           setAddState setFinishingStates state
141
         end
142
         else ()
143
       end
144
  in
145
  let coreCollector core =
146
    match coreGetStatus core with
147
    | Unsat -> ()
148
    | Sat ->
149
       setAddCore setCores core;
150
       setAddCore setFinishingCores core
151
    | Expandable
152
    | Open ->
153
       setAddCore setCores core;
154
       if bsetCompare (coreGetDeferral core) emptySet == 0
155
       then begin
156
           print_endline (coreToString core);
157
           setAddCore setFinishingCores core
158
         end
159
       else ()
160
  in
161
  graphIterStates stateCollector;
162
  graphIterCores coreCollector;
163

    
164
  (*
165
    In a fixpoint the set called setStates / setCores is narrowed down.
166

    
167
    In each step only those states and cores are retained in setStates
168
    / setCores which reach one of setFinishing{States,Cores} in
169
    finitely many steps. This new set of States / Cores is collected
170
    as allowed{States,Cores} during each fixpoint iteration.
171

    
172
    Only those finishing nodes are retained that have allowed or
173
    Successfull Children.
174
  *)
175

    
176
  let rec fixpointstep setStates setCores =
177
    let allowedStates = setEmptyState () in
178
    let allowedCores = setEmptyCore () in
179

    
180
    let rec visitParentStates (core : core) : unit =
181
      print_endline ("Looking at Core " ^ (string_of_int (coreGetIdx core)));
182
      if not (setMemCore allowedCores core)
183
      then begin
184
        setAddCore allowedCores core;
185
        print_endline ("Adding Core " ^ (string_of_int (coreGetIdx core)));
186
        let verifyParent (state,_) =
187
          let rules = stateGetRules state in
188
          let ruleiter (dependencies, corelist) =
189
            List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat)
190
              corelist
191
          in
192
          if List.for_all ruleiter rules
193
          then visitParentCores state
194
          else print_endline ("Not considering state "^(string_of_int (stateGetIdx state)))
195
        in
196
        List.iter verifyParent (coreGetParents core)
197
      end
198

    
199
    and visitParentCores (state : state) : unit =
200
      print_endline ("Looking at State " ^ (string_of_int (stateGetIdx state)));
201
      if not (setMemState allowedStates state)
202
      then begin
203
        setAddState allowedStates state;
204
        print_endline ("Adding State " ^ (string_of_int (stateGetIdx state)));
205
        let verifyParent core =
206
          let acceptable =
207
            List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
208
              (coreGetChildren core)
209
          in
210
          if acceptable
211
          then visitParentStates core
212
          else print_endline ("Not considering state "^(string_of_int (coreGetIdx core)))
213
        in
214
        List.iter verifyParent (stateGetParents state)
215
      end
216
    in
217

    
218
    (* All rule applications need to still be potentially Sat for a
219
     * finishing State to be a valid startingpoint for this fixpoint.
220
     *)
221
    let checkFinishingState (state : state) =
222
      let ruleiter (dependencies, corelist) : bool =
223
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist
224
      in
225
      if not (List.exists ruleiter (stateGetRules state)) then begin
226
        print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as proper starting node");
227
        visitParentCores state
228
      end
229

    
230
    (* There needs to be a State still potentially Sat for this core
231
     * to be considered for the fixpoint
232
     *)
233
    and checkFinishingCore (core : core) =
234
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state))
235
                           (coreGetChildren core))
236
      then begin
237
        print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as proper starting node");
238
        visitParentStates core
239
      end
240
    in
241
    setIterState checkFinishingState setFinishingStates;
242
    setIterCore checkFinishingCore setFinishingCores;
243

    
244

    
245
    if (setLengthState setStates) = (setLengthState allowedStates) &&
246
         (setLengthCore setCores) = (setLengthCore allowedCores)
247
    then begin
248
        setIterState (fun state -> stateSetStatus state Sat) setStates;
249
        setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot () then raise (CoAlg_finished true) else ()) setCores;
250
      end else
251
      fixpointstep allowedStates allowedCores
252
  in
253
  fixpointstep setStates setCores
254

    
255

    
256
(*****************************************************************************)
257
(*                     Propagation of Unsatisfiability                       *)
258
(*****************************************************************************)
259

    
260
let isConstraintUnsat cset =
261
  match graphFindCnstr cset with
262
  | None -> assert false
263
  | Some UnsatC -> true
264
  | _ -> false
265

    
266
let fhtMustFind fht f =
267
  match fhtFind fht f with
268
  | Some l -> l
269
  | None -> assert false
270

    
271
let lhtMustFind lht l =
272
  match lhtFind lht l with
273
  | Some f -> f
274
  | None -> assert false
275

    
276

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

    
402

    
403
(*****************************************************************************)
404
(*                   Propagation of Nominal Constraints                      *)
405
(*****************************************************************************)
406

    
407
let extractAts sort bs =
408
  let ats = csetMake () in
409
  let procNom nom f =
410
    match lfGetType sort f with
411
    | AndF
412
    | OrF -> ()
413
    | TrueFalseF
414
    | AtF -> ()
415
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
416
  in
417
  let getAts f =
418
    match lfGetType sort f with
419
    | AtF -> csetAdd ats (lfToAt sort f)
420
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
421
    | _ -> ()
422
  in
423
  bsetIter getAts bs;
424
  ats
425

    
426
let detConstraintsState state =
427
  let procRule accR (_, chldrn) =
428
    let procChldrn accC core =
429
      if coreGetStatus core = Unsat then accC
430
      else cssUnion accC (coreGetConstraints core)
431
    in
432
    let orset = List.fold_left procChldrn cssEmpty chldrn in
433
    let procOrset csetO accO =
434
      let mkUnion csetU accU =
435
        let cset = csetUnion csetO csetU in
436
        cssAdd cset accU
437
      in
438
      cssFold mkUnion accR accO
439
    in
440
    cssFold procOrset orset cssEmpty
441
  in
442
  let sort = stateGetSort state in
443
  let bs = stateGetBs state in
444
  let ats = extractAts sort bs in
445
  if stateGetStatus state = Expandable then csetAddDot ats else ();
446
  List.fold_left procRule (cssSingleton ats) (stateGetRules state)
447

    
448
let detConstraintsCore core =
449
  let sort = coreGetSort core in
450
  let bs = coreGetBs core in
451
  let ats = extractAts sort bs in
452
  let addCnstr acc state =
453
    if stateGetStatus state = Unsat then acc
454
    else
455
      let csets = stateGetConstraints state in
456
      (* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *)
457
      cssUnion csets acc
458
  in
459
  let initInner =
460
    if coreGetStatus core = Expandable then
461
      (* let cset = csetCopy ats in *)
462
      let cset = ats in
463
      csetAddDot cset;
464
      cssSingleton cset
465
    else cssEmpty
466
  in
467
  List.fold_left addCnstr initInner (coreGetChildren core)
468

    
469
let rec propNom = function
470
  | [] -> ()
471
  | node::tl ->
472
      let tl1 =
473
        match node with
474
        | State state ->
475
            if stateGetStatus state = Unsat then tl
476
            else
477
              let csets = detConstraintsState state in
478
              let oldcsets = stateGetConstraints state in
479
              if cssEqual csets oldcsets then tl
480
              else begin
481
                stateSetConstraints state csets;
482
                List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state)
483
              end
484
        | Core core ->
485
            if coreGetStatus core = Unsat then tl
486
            else
487
              let csets = detConstraintsCore core in
488
              let oldcsets = coreGetConstraints core in
489
              if cssEqual csets oldcsets then tl
490
              else begin
491
                coreSetConstraints core csets;
492
                List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core)
493
              end
494
      in
495
      propNom tl1
496

    
497
let updateConstraints node elemU csets =
498
  let update cset acc =
499
    let cnstr =
500
      match graphFindCnstr cset with
501
      | Some cn -> cn
502
      | None ->
503
          let cn = UnexpandedC [] in
504
          graphInsertCnstr cset cn;
505
          queueInsertCnstr cset;
506
          cn
507
    in
508
    match cnstr with
509
    | UnsatC -> acc
510
    | UnexpandedC parents ->
511
        graphReplaceCnstr cset (UnexpandedC (node::parents));
512
        false
513
    | OpenC parents ->
514
        graphReplaceCnstr cset (OpenC (node::parents));
515
        false
516
    | SatC -> false
517
  in
518
  let isUnsat = cssFold update csets true in
519
  if isUnsat then propagateUnsat [elemU] else ()
520

    
521
let propagateNominals () =
522
  let init = cssSingleton (csetMake ()) in
523
  graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init);
524
  graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init);
525
  graphIterStates (fun s -> propNom [State s]);
526
  graphIterCores (fun c -> propNom [Core c]);
527
  graphClearCnstr ();
528
  let fktS state =
529
    if stateGetStatus state = Unsat then ()
530
    else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state)
531
  in
532
  graphIterStates fktS;
533
  let fktC core =
534
    if coreGetStatus core = Unsat then ()
535
    else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core)
536
  in
537
  graphIterCores fktC
538

    
539

    
540
(*****************************************************************************)
541
(*                           Node Expansions                                 *)
542
(*****************************************************************************)
543

    
544
let getLit sort fht solver f =
545
  match fhtFind fht f with
546
  | Some lit -> lit
547
  | None ->
548
      let var = M.new_variable solver in
549
      let lit = M.var_to_lit var true in
550
      fhtAdd fht f lit;
551
      let () =
552
        match lfGetNeg sort f with
553
        | None -> ()
554
        | Some nf ->
555
            let nlit = M.neg_lit lit in
556
            fhtAdd fht nf nlit;
557
      in
558
      lit
559

    
560
let newCore sort bs defer =
561
  (* when creating a now core from a set of formulas bs
562
        bs = { x_1, ...., x_n }
563
           = "x_1 /\ .... /\ x_n"
564
     Then we do this by:
565

    
566
        1. creating a new literal in the sat solver for each
567
           "boolean subformula" from the x_i. "boolean subformula" means that
568
           this subformula is not hidden under modalities but only under
569
           boolean connectives (/\, \/).
570
        2. encoding the relation between a formula and its intermediate boolean
571
           subformulas by a clause:
572
  *)
573
  let fht = fhtInit () in
574
  let solver = M.new_solver () in
575
  let rec addClauses f =
576
    (* step 1: create a literal in the satsolver representing the formula f *)
577
    let lf = getLit sort fht solver f in
578
    (* step 2: encode relation to possible subformulas *)
579
    match lfGetType sort f with
580
    | OrF ->
581
        (*
582
           case 2.(a)   f =  f1 \/ f2
583
                   fill fht such that it says:
584

    
585
                        f  |---> lf
586
                        f1 |---> lf1
587
                        f2 |---> lf2
588
        *)
589
        let f1 = lfGetDest1 sort f in
590
        let f2 = lfGetDest2 sort f in
591
        addClauses f1;
592
        addClauses f2;
593
        let lf1 = fhtMustFind fht f1 in
594
        let lf2 = fhtMustFind fht f2 in
595
        (*
596
            encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
597
        *)
598
        let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
599
        assert (okay)
600
    | AndF ->
601
        (*
602
           case 2.(b)   f =  f1 /\ f2
603
                   fill fht such that it says:
604

    
605
                        f  |---> lf
606
                        f1 |---> lf1
607
                        f2 |---> lf2
608
        *)
609
        let f1 = lfGetDest1 sort f in
610
        let f2 = lfGetDest2 sort f in
611
        addClauses f1;
612
        addClauses f2;
613
        let lf1 = fhtMustFind fht f1 in
614
        let lf2 = fhtMustFind fht f2 in
615
        (*
616
            encode the structure of f by adding the clauses
617
                    (lf -> lf1) /\ (lf -> lf2)
618
        *)
619
        let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
620
        assert (okay1);
621
        let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
622
        assert (okay2)
623
    | MuF
624
    | NuF ->
625
       (*
626
          Dest of a fixpoint is it's unfolded version. This adds just
627
          an simple forward implication that could be optimised out
628
          though not without nontrivial transformation of code
629

    
630
            f = μ X . φ   |---> lf
631
            φ[X |-> f]    |---> lf1
632

    
633
          Then adding lf -> lf1 to minisat
634
        *)
635
       let f1 = lfGetDest1 sort f in
636
       addClauses f1;
637
       let lf1 = fhtMustFind fht f1 in
638
       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
639
       assert (okay1);
640
    | _ -> ()
641
        (* case 2.(c)
642
            We don't need to do anything except adding f to the fht
643
        *)
644
  in
645
  bsetIter addClauses bs;
646
  coreMake sort bs defer solver fht
647

    
648
let getNextState core =
649
  (* Create a new state, which is obtained by a satisfying assignment of the
650
     literals of the minisat solver.
651
     In addition to that, feed the negation of the satisfying assignment back
652
     to the minisat solver in order to obtain different solutions on successive
653
     minisat calls.
654
  *)
655
  let bs = coreGetBs core in
656
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
657
  let deferralS =
658
    if refocusing then
659
      bsetCopy bs
660
    else
661
      coreGetDeferral core
662
  in
663
  let fht = coreGetFht core in
664
  let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
665
  let solver = coreGetSolver core in
666
  let isSat = M.invoke_solver solver litset in
667
  (* Clearly, if the current core is unsatisfiable, no further child state can
668
     be created *)
669
  if not isSat then None
670
  else
671
    let sort = coreGetSort core in
672
    (* create a new set of formulas newbs with the property:
673
       if the conjunction of newbs is satisfiable, then the present core is
674
       satisfiable.
675
    *)
676
    let newbs = bsetMake () in
677
    let newdefer = bsetMakeRealEmpty () in
678
    (* if newbs = { l_1, .... l_n }, i.e.
679

    
680
            newbs = l_1 /\ ... /\ l_n
681

    
682
       then we can get essentially different satisfying assignments of bs by
683
       adding another clause
684

    
685
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
686

    
687
       By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
688
    *)
689
    let rec mkExclClause deferral f acc =
690
      (* f is a formula that is true in the current satisfying assignment *)
691
      match lfGetType sort f with
692
      | OrF ->
693
          (* if f is true and a disjunction, then one of its disjuncts is true *)
694
          let f1 = lfGetDest1 sort f in
695
          let lf1 = fhtMustFind fht f1 in
696
          (* if the first disjunct f1 is true, then we need to add subformulas
697
             of f1 to newbs&clause *)
698
          if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
699
          else
700
            (* otherwise f2 must be true *)
701
            let f2 = lfGetDest2 sort f in
702
            let lf2 = fhtMustFind fht f2 in
703
            assert (M.literal_status solver lf2 = M.LTRUE);
704
            mkExclClause deferral f2 acc
705
      | AndF ->
706
          (* if the true f is a conjuction, then both conjunctions must be true *)
707
          let f1 = lfGetDest1 sort f in
708
          let lf1 = fhtMustFind fht f1 in
709
          assert (M.literal_status solver lf1 = M.LTRUE);
710
          let acc1 = mkExclClause deferral f1 acc in
711
          let f2 = lfGetDest2 sort f in
712
          let lf2 = fhtMustFind fht f2 in
713
          assert (M.literal_status solver lf2 = M.LTRUE);
714
          mkExclClause deferral f2 acc1
715
      | MuF
716
      | NuF ->
717
         let f1 = lfGetDest1 sort f in
718
         mkExclClause deferral f1 acc
719
      | _ ->
720
         (* if f is a trivial formula or modality, then add it ... *)
721
         (* ... to newbs *)
722
         bsetAdd newbs f;
723
         let defercandidate = lfGetDeferral sort f in
724
         (if (defercandidate != (Hashtbl.hash "ε") &&
725
                (refocusing || deferral = defercandidate)) then
726
            bsetAdd newdefer f);
727
         (* ... and to the new clause *)
728
         (M.neg_lit (fhtMustFind fht f))::acc
729
    in
730
    let init_clause f acc =
731
      let deferral =
732
        if bsetMem deferralS f then (
733
          lfGetDeferral sort f)
734
        else
735
          (Hashtbl.hash "ε")
736
      in
737
      mkExclClause deferral f acc
738
    in
739
    let clause = bsetFold init_clause bs [] in
740
    let okay = M.add_clause solver clause in
741
    assert (okay);
742
    Some (sort, newbs, newdefer)
743

    
744
let newState sort bs defer =
745
  let (func, sl) = !sortTable.(sort) in
746
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
747
  let exp = producer sort bs defer sl in
748
  stateMake sort bs defer exp
749

    
750
let insertState parent sort bs defer =
751
  let child =
752
    match graphFindState sort (bs, defer) with
753
    | None ->
754
        let s = newState sort bs defer in
755
        graphInsertState sort (bs, defer) s;
756
        queueInsertState s;
757
        s
758
    | Some s -> s
759
  in
760
  coreAddChild parent child;
761
  stateAddParent child parent
762

    
763
let expandCore core =
764
  match getNextState core with
765
  | Some (sort, bs, defer) ->
766
      insertState core sort bs defer;
767
      queueInsertCore core
768
  | None ->
769
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
770
      if isUnsat then propagateUnsat [UCore (core, false)]
771
      else coreSetStatus core Open
772

    
773

    
774
let insertCore sort bs defer =
775
  match graphFindCore sort (bs, defer) with
776
  | None ->
777
     let c = newCore sort bs defer in
778
     graphInsertCore sort (bs, defer) c;
779
     queueInsertCore c;
780
     c
781
  | Some c -> c
782

    
783
let insertRule state dep chldrn =
784
  let chldrn = listFromLazylist chldrn in
785
  let insert (isUns, acc) (sort, bs, defer) =
786
    let bs1 = bsetAddTBox sort bs in
787
    let core = insertCore sort bs1 defer in
788
    let isUns1 = if coreGetStatus core = Unsat then isUns else false in
789
    (isUns1, core::acc)
790
  in
791
  let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
792
  let idx = stateAddRule state dep (List.rev children) in
793
  List.iter (fun c -> coreAddParent c state idx) children;
794
  if isUnsat then begin
795
    propagateUnsat [UState (state, Some idx)];
796
    false
797
  end else true
798

    
799
let rec insertAllRules state = function
800
  | [] -> true
801
  | (dep, chldrn)::tl ->
802
      let notUnsat = insertRule state dep chldrn in
803
      if notUnsat then insertAllRules state tl else false
804

    
805
let expandState state =
806
  match stateNextRule state with
807
  | MultipleElements rules ->
808
      let notUnsat = insertAllRules state rules in
809
      if notUnsat then stateSetStatus state Open
810
  | SingleElement (dep, chldrn) ->
811
      let notUnsat = insertRule state dep chldrn in
812
      if notUnsat then queueInsertState state else ()
813
  | NoMoreElements -> stateSetStatus state Open
814

    
815

    
816
let expandCnstr cset =
817
  let nht = nhtInit () in
818
  let mkCores f =
819
    let (sort, lf) as nom = atFormulaGetNominal f in
820
    let nomset =
821
      match nhtFind nht nom with
822
      | Some ns -> ns
823
      | None ->
824
          let cset1 = csetCopy cset in
825
          csetRemDot cset1;
826
          let bs = csetAddTBox sort cset1 in
827
          bsetAdd bs lf;
828
          nhtAdd nht nom bs;
829
          bs
830
    in
831
    bsetAdd nomset (atFormulaGetSubformula f)
832
  in
833
  csetIter cset mkCores;
834
  let inCores (sort, _) bs (isUns, acc) =
835
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
836
    coreAddConstraintParent core cset;
837
    (coreGetStatus core = Unsat || isUns, core::acc)
838
  in
839
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
840
  if isUnsat then propagateUnsat [UCnstr cset]
841
  else
842
    match graphFindCnstr cset with
843
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
844
    | _ -> assert false
845

    
846

    
847
(*****************************************************************************)
848
(*                           The Main Loop                                   *)
849
(*****************************************************************************)
850

    
851
let expandNodesLoop (recursiveAction: unit -> unit) =
852
  match queueGetElement () with
853
  | QState state ->
854
      if stateGetStatus state = Expandable then begin
855
        expandState state;
856
        if doNominalPropagation () then begin
857
          propagateNominals ();
858
          if doSatPropagation () then propagateSatMu ()
859
        end else ()
860
      end else ();
861
      recursiveAction ()
862
  | QCore core ->
863
      if coreGetStatus core = Expandable then begin
864
        expandCore core;
865
        if doNominalPropagation () then begin
866
          propagateNominals ();
867
          if doSatPropagation () then propagateSatMu ()
868
        end else ()
869
      end else ();
870
      recursiveAction ()
871
  | QCnstr cset ->
872
      expandCnstr cset;
873
      recursiveAction ()
874
  | QEmpty -> ()
875

    
876
let runReasonerStep () =
877
  let void () = () in
878
  expandNodesLoop void; (* expand at most one node *)
879
  (* if this emptied the queue *)
880
  if queueIsEmpty () then begin
881
    (* then check whether the nominals would add further queue elements *)
882
    print_endline "Propagating nominals...";
883
    propagateNominals ()
884
  end else () (* else: the next step would be to expand another node *)
885

    
886
let rec buildGraphLoop () =
887
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
888
  expandNodesFurther (); (* expand as many queue elements as possible *)
889
  propagateNominals ();
890
  (* if propagating nominals added some more queue members, do all again.. *)
891
  if queueIsEmpty () then () else buildGraphLoop ()
892

    
893
let initReasoner sorts nomTable tbox sf =
894
  sortTable := Array.copy sorts;
895
  let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
896
  let sort = fst sf in
897
  let bs1 = bsetAddTBox sort bs in
898
  let deferrals = bsetMakeRealEmpty() in
899
  let markDeferral f =
900
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
901
      bsetAdd deferrals f;)
902
  in
903
  bsetIter markDeferral bs;
904
  graphInit ();
905
  queueInit ();
906
  let root = insertCore sort bs1 deferrals in
907
  graphAddRoot root
908

    
909
let isRootSat () =
910
  match coreGetStatus (graphGetRoot ()) with
911
  | Expandable -> None
912
  | Unsat -> Some false
913
  | Sat -> if (queueIsEmpty()) then Some true else None
914
  | Open -> if (queueIsEmpty()) then Some false else None
915

    
916
let reasonerFinished () =
917
  match coreGetStatus (graphGetRoot ()) with
918
  | Expandable -> false
919
  | Unsat
920
  | Sat  -> true
921
  | Open -> queueIsEmpty ()
922

    
923

    
924
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
925
    @param verbose An optional switch which determines
926
    whether the procedure shall print some information on the standard output.
927
    The default is false.
928
    @param sorts An array mapping each sort (represented as an integer)
929
    to a functor and a list of sorts which are the arguments of the functor.
930
    @param nomTable A partial function mapping nominals (represented as strings)
931
    to their sorts.
932
    @param tbox A list of sorted formulae.
933
    @param sf A sorted formula.
934
    @return True if sf is satisfiable wrt tbox, false otherwise.
935
 *)
936

    
937
let isSat ?(verbose = false) sorts nomTable tbox sf =
938
  let start = if verbose then Unix.gettimeofday () else 0. in
939
  initReasoner sorts nomTable tbox sf;
940
  let sat =
941
    try
942
      buildGraphLoop ();
943
      (* get whether the root is satisfiable *)
944
      (* we know that the reasoner finished, so the value is there, *)
945
      (* i.e. isRootSat() will give a "Some x" and not "None" *)
946
      CU.fromSome (isRootSat())
947
    with CoAlg_finished res -> res
948
  in
949
  (* print some statistics *)
950
  if verbose then
951
    let stop = Unix.gettimeofday () in
952
    let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
953
    print_newline ();
954
    print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
955
    let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
956
    print_endline ("Added Size: " ^ (string_of_int size));
957
    (*
958
    print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
959
    let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
960
    print_endline ("Added Size: " ^ (string_of_int nsize));
961
    *)
962
    print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
963
    print_endline ("Time: " ^ (string_of_float (stop -. start)));
964
    print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
965
    print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ())));
966
    print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ())));
967
    print_newline ()
968
  else ();
969
  sat