Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 2f126161

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

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

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

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

    
192
    let rec visitParentStates (core : core) : unit =
193
      print_endline ("Looking at Core " ^ (string_of_int (coreGetIdx core)));
194
      if not (setMemCore allowedCores core)
195
      then begin
196
        setAddCore allowedCores core;
197
        print_endline ("Adding Core " ^ (string_of_int (coreGetIdx 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
          else print_endline ("Not considering state "^(string_of_int (stateGetIdx state)))
207
        in
208
        List.iter verifyParent (coreGetParents core)
209
      end
210

    
211
    and visitParentCores (state : state) : unit =
212
      print_endline ("Looking at State " ^ (string_of_int (stateGetIdx state)));
213
      if not (setMemState allowedStates state)
214
      then begin
215
        setAddState allowedStates state;
216
        print_endline ("Adding State " ^ (string_of_int (stateGetIdx state)));
217
        let verifyParent core =
218
          let acceptable =
219
            List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
220
              (coreGetChildren core)
221
          in
222
          if acceptable
223
          then visitParentStates core
224
          else print_endline ("Not considering state "^(string_of_int (coreGetIdx core)))
225
        in
226
        List.iter verifyParent (stateGetParents state)
227
      end
228
    in
229

    
230
    (* All rule applications need to still be potentially Sat for a
231
     * finishing State to be a valid startingpoint for this fixpoint.
232
     *)
233
    let checkFinishingState (state : state) =
234
      let ruleiter (dependencies, corelist) : bool =
235
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist
236
      in
237
      if not (List.exists ruleiter (stateGetRules state)) then begin
238
        print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as proper starting node");
239
        visitParentCores state
240
      end
241

    
242
    (* There needs to be a State still potentially Sat for this core
243
     * to be considered for the fixpoint
244
     *)
245
    and checkFinishingCore (core : core) =
246
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state))
247
                           (coreGetChildren core))
248
      then begin
249
        print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as proper starting node");
250
        visitParentStates core
251
      end
252
    in
253
    setIterState checkFinishingState setFinishingStates;
254
    setIterCore checkFinishingCore setFinishingCores;
255

    
256

    
257
    if (setLengthState setStates) = (setLengthState allowedStates) &&
258
         (setLengthCore setCores) = (setLengthCore allowedCores)
259
    then begin
260
        setIterState (fun state -> stateSetStatus state Sat) setStates;
261
        setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot () then raise (CoAlg_finished true) else ()) setCores;
262
      end else
263
      fixpointstep allowedStates allowedCores
264
  in
265
  fixpointstep setStates setCores
266

    
267

    
268
(*****************************************************************************)
269
(*                     Propagation of Unsatisfiability                       *)
270
(*****************************************************************************)
271

    
272
let isConstraintUnsat cset =
273
  match graphFindCnstr cset with
274
  | None -> assert false
275
  | Some UnsatC -> true
276
  | _ -> false
277

    
278
let fhtMustFind fht f =
279
  match fhtFind fht f with
280
  | Some l -> l
281
  | None -> assert false
282

    
283
let lhtMustFind lht l =
284
  match lhtFind lht l with
285
  | Some f -> f
286
  | None -> assert false
287

    
288

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

    
414

    
415
(*****************************************************************************)
416
(*                   Propagation of Nominal Constraints                      *)
417
(*****************************************************************************)
418

    
419
let extractAts sort bs =
420
  let ats = csetMake () in
421
  let procNom nom f =
422
    match lfGetType sort f with
423
    | AndF
424
    | OrF -> ()
425
    | TrueFalseF
426
    | AtF -> ()
427
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
428
  in
429
  let getAts f =
430
    match lfGetType sort f with
431
    | AtF -> csetAdd ats (lfToAt sort f)
432
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
433
    | _ -> ()
434
  in
435
  bsetIter getAts bs;
436
  ats
437

    
438
let detConstraintsState state =
439
  let procRule accR (_, chldrn) =
440
    let procChldrn accC core =
441
      if coreGetStatus core = Unsat then accC
442
      else cssUnion accC (coreGetConstraints core)
443
    in
444
    let orset = List.fold_left procChldrn cssEmpty chldrn in
445
    let procOrset csetO accO =
446
      let mkUnion csetU accU =
447
        let cset = csetUnion csetO csetU in
448
        cssAdd cset accU
449
      in
450
      cssFold mkUnion accR accO
451
    in
452
    cssFold procOrset orset cssEmpty
453
  in
454
  let sort = stateGetSort state in
455
  let bs = stateGetBs state in
456
  let ats = extractAts sort bs in
457
  if stateGetStatus state = Expandable then csetAddDot ats else ();
458
  List.fold_left procRule (cssSingleton ats) (stateGetRules state)
459

    
460
let detConstraintsCore core =
461
  let sort = coreGetSort core in
462
  let bs = coreGetBs core in
463
  let ats = extractAts sort bs in
464
  let addCnstr acc state =
465
    if stateGetStatus state = Unsat then acc
466
    else
467
      let csets = stateGetConstraints state in
468
      (* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *)
469
      cssUnion csets acc
470
  in
471
  let initInner =
472
    if coreGetStatus core = Expandable then
473
      (* let cset = csetCopy ats in *)
474
      let cset = ats in
475
      csetAddDot cset;
476
      cssSingleton cset
477
    else cssEmpty
478
  in
479
  List.fold_left addCnstr initInner (coreGetChildren core)
480

    
481
let rec propNom = function
482
  | [] -> ()
483
  | node::tl ->
484
      let tl1 =
485
        match node with
486
        | State state ->
487
            if stateGetStatus state = Unsat then tl
488
            else
489
              let csets = detConstraintsState state in
490
              let oldcsets = stateGetConstraints state in
491
              if cssEqual csets oldcsets then tl
492
              else begin
493
                stateSetConstraints state csets;
494
                List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state)
495
              end
496
        | Core core ->
497
            if coreGetStatus core = Unsat then tl
498
            else
499
              let csets = detConstraintsCore core in
500
              let oldcsets = coreGetConstraints core in
501
              if cssEqual csets oldcsets then tl
502
              else begin
503
                coreSetConstraints core csets;
504
                List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core)
505
              end
506
      in
507
      propNom tl1
508

    
509
let updateConstraints node elemU csets =
510
  let update cset acc =
511
    let cnstr =
512
      match graphFindCnstr cset with
513
      | Some cn -> cn
514
      | None ->
515
          let cn = UnexpandedC [] in
516
          graphInsertCnstr cset cn;
517
          queueInsertCnstr cset;
518
          cn
519
    in
520
    match cnstr with
521
    | UnsatC -> acc
522
    | UnexpandedC parents ->
523
        graphReplaceCnstr cset (UnexpandedC (node::parents));
524
        false
525
    | OpenC parents ->
526
        graphReplaceCnstr cset (OpenC (node::parents));
527
        false
528
    | SatC -> false
529
  in
530
  let isUnsat = cssFold update csets true in
531
  if isUnsat then propagateUnsat [elemU] else ()
532

    
533
let propagateNominals () =
534
  let init = cssSingleton (csetMake ()) in
535
  graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init);
536
  graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init);
537
  graphIterStates (fun s -> propNom [State s]);
538
  graphIterCores (fun c -> propNom [Core c]);
539
  graphClearCnstr ();
540
  let fktS state =
541
    if stateGetStatus state = Unsat then ()
542
    else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state)
543
  in
544
  graphIterStates fktS;
545
  let fktC core =
546
    if coreGetStatus core = Unsat then ()
547
    else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core)
548
  in
549
  graphIterCores fktC
550

    
551

    
552
(*****************************************************************************)
553
(*                           Node Expansions                                 *)
554
(*****************************************************************************)
555

    
556
let getLit sort fht solver f =
557
  match fhtFind fht f with
558
  | Some lit -> lit
559
  | None ->
560
      let var = M.new_variable solver in
561
      let lit = M.var_to_lit var true in
562
      fhtAdd fht f lit;
563
      let () =
564
        match lfGetNeg sort f with
565
        | None -> ()
566
        | Some nf ->
567
            let nlit = M.neg_lit lit in
568
            fhtAdd fht nf nlit;
569
      in
570
      lit
571

    
572
let newCore sort bs defer =
573
  (* when creating a now core from a set of formulas bs
574
        bs = { x_1, ...., x_n }
575
           = "x_1 /\ .... /\ x_n"
576
     Then we do this by:
577

    
578
        1. creating a new literal in the sat solver for each
579
           "boolean subformula" from the x_i. "boolean subformula" means that
580
           this subformula is not hidden under modalities but only under
581
           boolean connectives (/\, \/).
582
        2. encoding the relation between a formula and its intermediate boolean
583
           subformulas by a clause:
584
  *)
585
  let fht = fhtInit () in
586
  let solver = M.new_solver () in
587
  let rec addClauses f =
588
    (* step 1: create a literal in the satsolver representing the formula f *)
589
    let lf = getLit sort fht solver f in
590
    (* step 2: encode relation to possible subformulas *)
591
    match lfGetType sort f with
592
    | OrF ->
593
        (*
594
           case 2.(a)   f =  f1 \/ f2
595
                   fill fht such that it says:
596

    
597
                        f  |---> lf
598
                        f1 |---> lf1
599
                        f2 |---> lf2
600
        *)
601
        let f1 = lfGetDest1 sort f in
602
        let f2 = lfGetDest2 sort f in
603
        addClauses f1;
604
        addClauses f2;
605
        let lf1 = fhtMustFind fht f1 in
606
        let lf2 = fhtMustFind fht f2 in
607
        (*
608
            encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
609
        *)
610
        let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
611
        assert (okay)
612
    | AndF ->
613
        (*
614
           case 2.(b)   f =  f1 /\ f2
615
                   fill fht such that it says:
616

    
617
                        f  |---> lf
618
                        f1 |---> lf1
619
                        f2 |---> lf2
620
        *)
621
        let f1 = lfGetDest1 sort f in
622
        let f2 = lfGetDest2 sort f in
623
        addClauses f1;
624
        addClauses f2;
625
        let lf1 = fhtMustFind fht f1 in
626
        let lf2 = fhtMustFind fht f2 in
627
        (*
628
            encode the structure of f by adding the clauses
629
                    (lf -> lf1) /\ (lf -> lf2)
630
        *)
631
        let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
632
        assert (okay1);
633
        let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
634
        assert (okay2)
635
    | MuF
636
    | NuF ->
637
       (*
638
          Dest of a fixpoint is it's unfolded version. This adds just
639
          an simple forward implication that could be optimised out
640
          though not without nontrivial transformation of code
641

    
642
            f = μ X . φ   |---> lf
643
            φ[X |-> f]    |---> lf1
644

    
645
          Then adding lf -> lf1 to minisat
646
        *)
647
       let f1 = lfGetDest1 sort f in
648
       addClauses f1;
649
       let lf1 = fhtMustFind fht f1 in
650
       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
651
       assert (okay1);
652
    | _ -> ()
653
        (* case 2.(c)
654
            We don't need to do anything except adding f to the fht
655
        *)
656
  in
657
  bsetIter addClauses bs;
658
  coreMake sort bs defer solver fht
659

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

    
692
            newbs = l_1 /\ ... /\ l_n
693

    
694
       then we can get essentially different satisfying assignments of bs by
695
       adding another clause
696

    
697
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
698

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

    
756
let newState sort bs defer =
757
  let (func, sl) = !sortTable.(sort) in
758
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
759
  let exp = producer sort bs defer sl in
760
  stateMake sort bs defer exp
761

    
762
let insertState parent sort bs defer =
763
  let child =
764
    match graphFindState sort (bs, defer) with
765
    | None ->
766
        let s = newState sort bs defer in
767
        graphInsertState sort (bs, defer) s;
768
        queueInsertState s;
769
        s
770
    | Some s -> s
771
  in
772
  coreAddChild parent child;
773
  stateAddParent child parent
774

    
775
let expandCore core =
776
  match getNextState core with
777
  | Some (sort, bs, defer) ->
778
      insertState core sort bs defer;
779
      queueInsertCore core
780
  | None ->
781
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
782
      if isUnsat then propagateUnsat [UCore (core, false)]
783
      else coreSetStatus core Open
784

    
785

    
786
let insertCore sort bs defer =
787
  match graphFindCore sort (bs, defer) with
788
  | None ->
789
     let c = newCore sort bs defer in
790
     graphInsertCore sort (bs, defer) c;
791
     queueInsertCore c;
792
     c
793
  | Some c -> c
794

    
795
let insertRule state dep chldrn =
796
  let chldrn = listFromLazylist chldrn in
797
  let insert (isUns, acc) (sort, bs, defer) =
798
    let bs1 = bsetAddTBox sort bs in
799
    let core = insertCore sort bs1 defer in
800
    let isUns1 = if coreGetStatus core = Unsat then isUns else false in
801
    (isUns1, core::acc)
802
  in
803
  let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
804
  let idx = stateAddRule state dep (List.rev children) in
805
  List.iter (fun c -> coreAddParent c state idx) children;
806
  if isUnsat then begin
807
    propagateUnsat [UState (state, Some idx)];
808
    false
809
  end else true
810

    
811
let rec insertAllRules state = function
812
  | [] -> true
813
  | (dep, chldrn)::tl ->
814
      let notUnsat = insertRule state dep chldrn in
815
      if notUnsat then insertAllRules state tl else false
816

    
817
let expandState state =
818
  match stateNextRule state with
819
  | MultipleElements rules ->
820
      let notUnsat = insertAllRules state rules in
821
      if notUnsat then stateSetStatus state Open
822
  | SingleElement (dep, chldrn) ->
823
      let notUnsat = insertRule state dep chldrn in
824
      if notUnsat then queueInsertState state else ()
825
  | NoMoreElements -> stateSetStatus state Open
826

    
827

    
828
let expandCnstr cset =
829
  let nht = nhtInit () in
830
  let mkCores f =
831
    let (sort, lf) as nom = atFormulaGetNominal f in
832
    let nomset =
833
      match nhtFind nht nom with
834
      | Some ns -> ns
835
      | None ->
836
          let cset1 = csetCopy cset in
837
          csetRemDot cset1;
838
          let bs = csetAddTBox sort cset1 in
839
          bsetAdd bs lf;
840
          nhtAdd nht nom bs;
841
          bs
842
    in
843
    bsetAdd nomset (atFormulaGetSubformula f)
844
  in
845
  csetIter cset mkCores;
846
  let inCores (sort, _) bs (isUns, acc) =
847
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
848
    coreAddConstraintParent core cset;
849
    (coreGetStatus core = Unsat || isUns, core::acc)
850
  in
851
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
852
  if isUnsat then propagateUnsat [UCnstr cset]
853
  else
854
    match graphFindCnstr cset with
855
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
856
    | _ -> assert false
857

    
858

    
859
(*****************************************************************************)
860
(*                           The Main Loop                                   *)
861
(*****************************************************************************)
862

    
863
let expandNodesLoop (recursiveAction: unit -> unit) =
864
  match queueGetElement () with
865
  | QState state ->
866
      if stateGetStatus state = Expandable then begin
867
        expandState state;
868
        if doNominalPropagation () then begin
869
          propagateNominals ();
870
          if doSatPropagation () then propagateSatMu ()
871
        end else ()
872
      end else ();
873
      recursiveAction ()
874
  | QCore core ->
875
      if coreGetStatus core = Expandable then begin
876
        expandCore core;
877
        if doNominalPropagation () then begin
878
          propagateNominals ();
879
          if doSatPropagation () then propagateSatMu ()
880
        end else ()
881
      end else ();
882
      recursiveAction ()
883
  | QCnstr cset ->
884
      expandCnstr cset;
885
      recursiveAction ()
886
  | QEmpty -> ()
887

    
888
let runReasonerStep () =
889
  let void () = () in
890
  expandNodesLoop void; (* expand at most one node *)
891
  (* if this emptied the queue *)
892
  if queueIsEmpty () then begin
893
    (* then check whether the nominals would add further queue elements *)
894
    print_endline "Propagating nominals...";
895
    propagateNominals ()
896
  end else () (* else: the next step would be to expand another node *)
897

    
898
let rec buildGraphLoop () =
899
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
900
  expandNodesFurther (); (* expand as many queue elements as possible *)
901
  propagateNominals ();
902
  (* if propagating nominals added some more queue members, do all again.. *)
903
  if queueIsEmpty () then () else buildGraphLoop ()
904

    
905
let initReasoner sorts nomTable tbox sf =
906
  sortTable := Array.copy sorts;
907
  let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
908
  let sort = fst sf in
909
  let bs1 = bsetAddTBox sort bs in
910
  let deferrals = bsetMakeRealEmpty() in
911
  let markDeferral f =
912
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
913
      bsetAdd deferrals f;)
914
  in
915
  bsetIter markDeferral bs;
916
  graphInit ();
917
  queueInit ();
918
  let root = insertCore sort bs1 deferrals in
919
  graphAddRoot root
920

    
921
let isRootSat () =
922
  match coreGetStatus (graphGetRoot ()) with
923
  | Expandable -> None
924
  | Unsat -> Some false
925
  | Sat -> if (queueIsEmpty()) then Some true else None
926
  | Open -> if (queueIsEmpty()) then Some false else None
927

    
928
let reasonerFinished () =
929
  match coreGetStatus (graphGetRoot ()) with
930
  | Expandable -> false
931
  | Unsat
932
  | Sat  -> true
933
  | Open -> queueIsEmpty ()
934

    
935

    
936
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
937
    @param verbose An optional switch which determines
938
    whether the procedure shall print some information on the standard output.
939
    The default is false.
940
    @param sorts An array mapping each sort (represented as an integer)
941
    to a functor and a list of sorts which are the arguments of the functor.
942
    @param nomTable A partial function mapping nominals (represented as strings)
943
    to their sorts.
944
    @param tbox A list of sorted formulae.
945
    @param sf A sorted formula.
946
    @return True if sf is satisfiable wrt tbox, false otherwise.
947
 *)
948

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