Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ de84f40d

History | View | Annotate | Download (33.3 KB)

1 4fd28192 Thorsten Wißmann
(** 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 c2cc0c2e Thorsten Wißmann
module CU = CoolUtils
11
12 4fd28192 Thorsten Wißmann
type sortTable = CoAlgMisc.sortTable
13
14 c78c1ce0 Thorsten Wißmann
type nomTable = string -> CoAlgFormula.sort option
15
16
type assumptions = CoAlgFormula.sortedFormula list
17
18
type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
19
20 f335015f Thorsten Wißmann
exception ReasonerError of string
21 4fd28192 Thorsten Wißmann
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 6d64bc5a Christoph Egger
    | None -> raise (ReasonerError "?")
31
    | Some SatC -> true
32
    | Some (OpenC _) -> setMemCnstr setCnstr cset
33
    | Some (UnexpandedC _)
34
    | Some UnsatC -> false
35
36 4fd28192 Thorsten Wißmann
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 6bbde09c Christoph Egger
let propagateSatMu () =
117
  let setFinishingStates = setEmptyState () in
118
  let setFinishingCores = setEmptyCore () in
119
  let setStates = setEmptyState () in
120
  let setCores = setEmptyCore () in
121 07a36b24 Christoph Egger
  let setSatStates = setEmptyState () in
122
  let setSatCores = setEmptyCore () in
123 6bbde09c Christoph Egger
  let emptySet = bsetMakeRealEmpty () in
124
125
  let stateCollector state =
126
    match stateGetStatus state with
127 07a36b24 Christoph Egger
    | Unsat -> ()
128
    | Sat ->
129
       setAddState setSatStates state
130 6bbde09c Christoph Egger
    | Expandable
131
    | Open ->
132 46cd6856 Christoph Egger
       if stateGetStatus state == Open && List.length (stateGetRules state) == 0
133 6bbde09c Christoph Egger
       then begin
134 46cd6856 Christoph Egger
         setAddState setSatStates state;
135
         stateSetStatus state Sat
136
       end else begin
137
         setAddState setStates state;
138
         if bsetCompare (stateGetDeferral state) emptySet == 0
139
         then begin
140 6bbde09c Christoph Egger
           print_endline (stateToString state);
141
           setAddState setFinishingStates state
142
         end
143 46cd6856 Christoph Egger
         else ()
144
       end
145 6bbde09c Christoph Egger
  in
146
  let coreCollector core =
147
    match coreGetStatus core with
148 07a36b24 Christoph Egger
    | Unsat -> ()
149
    | Sat ->
150
       setAddCore setSatCores core
151 6bbde09c Christoph Egger
    | 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 67b07e54 Christoph Egger
    let allowedStates = setEmptyState () in
178
    let allowedCores = setEmptyCore () in
179 6bbde09c Christoph Egger
180
    let rec visitParentStates (core : core) : unit =
181 2fba43c0 Christoph Egger
      if not (setMemCore setCores core || setMemCore setSatCores core) then ()
182 67b07e54 Christoph Egger
      else begin
183 6bbde09c Christoph Egger
        let children = coreGetChildren core in
184 67b07e54 Christoph Egger
        let acceptable =
185
          List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
186
            children
187
        in
188 6bbde09c Christoph Egger
        if acceptable then begin
189
          print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as allowed");
190
          setAddCore allowedCores core;
191
          List.iter (fun (state, _) -> visitParentCores state)
192
            (coreGetParents core)
193
        end
194
      end
195
196
    and visitParentCores (state : state) : unit =
197 2fba43c0 Christoph Egger
      if not (setMemState setStates state || setMemState setSatStates state) then ()
198 67b07e54 Christoph Egger
      else begin
199 6bbde09c Christoph Egger
        let rules = stateGetRules state in
200
        let ruleiter (dependencies, corelist) =
201 67b07e54 Christoph Egger
          List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat)
202
            corelist
203 6bbde09c Christoph Egger
        in
204
        let acceptable = List.for_all ruleiter rules in
205
        if acceptable then begin
206
          print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as allowed");
207
          setAddState allowedStates state;
208 67b07e54 Christoph Egger
          List.iter (fun core -> if not (setMemCore allowedCores core) then visitParentStates core)
209 6bbde09c Christoph Egger
            (stateGetParents state)
210
        end
211
      end
212
    in
213
214 07a36b24 Christoph Egger
    (* All rule applications need to still be potentially Sat for a
215
     * finishing State to be a valid startingpoint for this fixpoint.
216
     *)
217
    let checkFinishingState (state : state) =
218
      let ruleiter (dependencies, corelist) : bool =
219 0a6a3df5 Christoph Egger
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist
220 07a36b24 Christoph Egger
      in
221
      if not (List.exists ruleiter (stateGetRules state)) then begin
222
        setAddState allowedStates state;
223
        visitParentCores state
224
      end
225
226
    (* There needs to be a State still potentially Sat for this core
227
     * to be considered for the fixpoint
228
     *)
229
    and checkFinishingCore (core : core) =
230 0a6a3df5 Christoph Egger
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state))
231 07a36b24 Christoph Egger
                           (coreGetChildren core))
232
      then begin
233
        setAddCore allowedCores core;
234
        visitParentStates core
235
      end
236
    in
237
    setIterState checkFinishingState setFinishingStates;
238
    setIterCore checkFinishingCore setFinishingCores;
239
    setIterState visitParentCores setSatStates;
240
    setIterCore visitParentStates setSatCores;
241
242 6bbde09c Christoph Egger
243
    if (setLengthState setStates) = (setLengthState allowedStates) &&
244 07a36b24 Christoph Egger
         (setLengthCore setCores) = (setLengthCore allowedCores)
245 6bbde09c Christoph Egger
    then begin
246 07a36b24 Christoph Egger
        setIterState (fun state -> stateSetStatus state Sat) setStates;
247
        setIterCore (fun core -> coreSetStatus core Sat) setCores;
248
      end else
249 6bbde09c Christoph Egger
      fixpointstep allowedStates allowedCores
250
  in
251
  fixpointstep setStates setCores
252
253
254 4fd28192 Thorsten Wißmann
(*****************************************************************************)
255
(*                     Propagation of Unsatisfiability                       *)
256
(*****************************************************************************)
257
258
let isConstraintUnsat cset =
259
  match graphFindCnstr cset with
260
  | None -> assert false
261
  | Some UnsatC -> true
262
  | _ -> false
263
264 433c8a2e Thorsten Wißmann
let fhtMustFind fht f =
265 4fd28192 Thorsten Wißmann
  match fhtFind fht f with
266
  | Some l -> l
267
  | None -> assert false
268
269 433c8a2e Thorsten Wißmann
let lhtMustFind lht l =
270
  match lhtFind lht l with
271 4fd28192 Thorsten Wißmann
  | Some f -> f
272
  | None -> assert false
273 01bf25db Thorsten Wißmann
274 7b21fbae Christoph Egger
275
(* Gets a list of Things we know are unsatisfiable and propagates this
276
   information backwards *)
277 433c8a2e Thorsten Wißmann
let rec propagateUnsat = function
278 4fd28192 Thorsten Wißmann
  | [] -> ()
279
  | propElem::tl ->
280
      let tl1 =
281
        match propElem with
282
        | UState (state, idxopt) -> begin
283
            match stateGetStatus state with
284
            | Unsat -> tl
285 73762b19 Thorsten Wißmann
            | Sat -> raise (ReasonerError ("Propagation tells state "
286
                                           ^(string_of_int (stateGetIdx state))
287
                                           ^" would be unsat, but it is already sat"))
288 4fd28192 Thorsten Wißmann
            | Open
289
            | Expandable ->
290
                let mbs =
291
                  match idxopt with
292
                  | None -> stateGetBs state
293
                  | Some idx ->
294
                      let (dep, children) = stateGetRule state idx in
295
                      let getBs core =
296
                        assert (coreGetStatus core = Unsat);
297
                        coreGetBs core
298
                      in
299
                      dep (List.map getBs children)
300
                in
301
                stateSetBs state mbs;
302
                stateSetStatus state Unsat;
303
                let prop acc core =
304
                  let turnsUnsat =
305
                    match coreGetStatus core with
306
                    | Open -> List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core)
307
                    | Expandable
308
                    | Unsat
309
                    | Sat -> false
310
                  in
311
                  if turnsUnsat then (UCore (core, false))::acc else acc
312
                in
313
                List.fold_left prop tl (stateGetParents state)
314
          end
315
        | UCore (core, comesFromCnstr) -> begin
316
            match coreGetStatus core with
317
            | Unsat -> tl
318 73762b19 Thorsten Wißmann
            | Sat -> raise (ReasonerError ("Propagation tells core "
319
                                           ^(string_of_int (coreGetIdx core))
320
                                           ^" would be unsat, but it is already sat"))
321 4fd28192 Thorsten Wißmann
            | Open
322
            | Expandable ->
323
                let mbs =
324
                  if comesFromCnstr then coreGetBs core
325
                  else
326
                    let bs = coreGetBs core in
327
                    let solver = coreGetSolver core in
328
                    let fht = coreGetFht core in
329
                    let lht = lhtInit () in
330
                    let addLits f acc =
331
                      let lit = fhtMustFind fht f in
332
                      lhtAdd lht lit f;
333
                      lit::acc
334
                    in
335
                    let litset = bsetFold addLits bs [] in
336
                    let addClauses state =
337
                      let cbs = stateGetBs state in
338
                      let clause = bsetFold (fun f acc -> (M.neg_lit (fhtMustFind fht f))::acc) cbs [] in
339
                      let okay = M.add_clause solver clause in
340
                      assert okay
341
                    in
342
                    List.iter addClauses (coreGetChildren core);
343
                    let isSat = M.invoke_solver solver litset in
344
                    assert (not isSat);
345
                    let res = bsetMake () in
346
                    let confls = M.get_conflict solver in
347
                    List.iter (fun l -> bsetAdd res (lhtMustFind lht l)) confls;
348
                    res
349
                in
350
                coreSetBs core mbs;
351
                coreSetStatus core Unsat;
352
                if core == graphGetRoot () then raise (CoAlg_finished false) else ();
353
                let prop acc (state, idx) =
354
                  let turnsUnsat =
355
                    match stateGetStatus state with
356
                    | Open
357
                    | Expandable ->
358
                        List.for_all (fun c -> coreGetStatus c = Unsat) (snd (stateGetRule state idx))
359
                    | Unsat
360
                    | Sat -> false
361
                  in
362
                  if turnsUnsat then (UState (state, Some idx))::acc else acc
363
                in
364
                let tl2 = List.fold_left prop tl (coreGetParents core) in
365
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl2 (coreGetConstraintParents core)
366
          end
367
        | UCnstr cset ->
368
            match graphFindCnstr cset with
369
            | None
370
            | Some SatC -> assert false
371
            | Some UnsatC -> tl
372
            | Some (UnexpandedC nodes)
373
            | Some (OpenC nodes) ->
374
                graphReplaceCnstr cset UnsatC;
375
                let prop acc node =
376
                  match node with
377
                  | State state ->
378 3eb8fabd Christoph Egger
                      let turnsUnsat =
379 4fd28192 Thorsten Wißmann
                        match stateGetStatus state with
380
                        | Expandable
381
                        | Open -> cssForall isConstraintUnsat (stateGetConstraints state)
382
                        | Unsat
383
                        | Sat -> false
384
                      in
385
                      if turnsUnsat then (UState (state, None))::acc else acc
386
                  | Core core ->
387
                      let turnsUnsat =
388
                        match coreGetStatus core with
389
                        | Expandable
390
                        | Open -> cssForall isConstraintUnsat (coreGetConstraints core)
391
                        | Unsat
392
                        | Sat -> false
393
                      in
394
                      if turnsUnsat then (UCore (core, true))::acc else acc
395
                in
396
                List.fold_left prop tl nodes
397
      in
398
      propagateUnsat tl1
399
400
401
(*****************************************************************************)
402
(*                   Propagation of Nominal Constraints                      *)
403
(*****************************************************************************)
404
405 433c8a2e Thorsten Wißmann
let extractAts sort bs =
406 4fd28192 Thorsten Wißmann
  let ats = csetMake () in
407
  let procNom nom f =
408
    match lfGetType sort f with
409
    | AndF
410
    | OrF -> ()
411 3b055ae8 dirk
    | TrueFalseF
412 4fd28192 Thorsten Wißmann
    | AtF -> ()
413
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
414
  in
415
  let getAts f =
416
    match lfGetType sort f with
417
    | AtF -> csetAdd ats (lfToAt sort f)
418
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
419
    | _ -> ()
420
  in
421
  bsetIter getAts bs;
422
  ats
423
424 433c8a2e Thorsten Wißmann
let detConstraintsState state =
425 4fd28192 Thorsten Wißmann
  let procRule accR (_, chldrn) =
426
    let procChldrn accC core =
427
      if coreGetStatus core = Unsat then accC
428
      else cssUnion accC (coreGetConstraints core)
429
    in
430
    let orset = List.fold_left procChldrn cssEmpty chldrn in
431
    let procOrset csetO accO =
432
      let mkUnion csetU accU =
433
        let cset = csetUnion csetO csetU in
434
        cssAdd cset accU
435
      in
436
      cssFold mkUnion accR accO
437
    in
438
    cssFold procOrset orset cssEmpty
439
  in
440
  let sort = stateGetSort state in
441
  let bs = stateGetBs state in
442
  let ats = extractAts sort bs in
443
  if stateGetStatus state = Expandable then csetAddDot ats else ();
444
  List.fold_left procRule (cssSingleton ats) (stateGetRules state)
445
446 433c8a2e Thorsten Wißmann
let detConstraintsCore core =
447 4fd28192 Thorsten Wißmann
  let sort = coreGetSort core in
448
  let bs = coreGetBs core in
449
  let ats = extractAts sort bs in
450
  let addCnstr acc state =
451
    if stateGetStatus state = Unsat then acc
452
    else
453
      let csets = stateGetConstraints state in
454
      (* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *)
455
      cssUnion csets acc
456
  in
457
  let initInner =
458
    if coreGetStatus core = Expandable then
459
      (* let cset = csetCopy ats in *)
460
      let cset = ats in
461
      csetAddDot cset;
462
      cssSingleton cset
463
    else cssEmpty
464
  in
465
  List.fold_left addCnstr initInner (coreGetChildren core)
466
467 433c8a2e Thorsten Wißmann
let rec propNom = function
468 4fd28192 Thorsten Wißmann
  | [] -> ()
469
  | node::tl ->
470
      let tl1 =
471
        match node with
472
        | State state ->
473
            if stateGetStatus state = Unsat then tl
474
            else
475
              let csets = detConstraintsState state in
476
              let oldcsets = stateGetConstraints state in
477
              if cssEqual csets oldcsets then tl
478
              else begin
479
                stateSetConstraints state csets;
480
                List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state)
481
              end
482
        | Core core ->
483
            if coreGetStatus core = Unsat then tl
484
            else
485
              let csets = detConstraintsCore core in
486
              let oldcsets = coreGetConstraints core in
487
              if cssEqual csets oldcsets then tl
488
              else begin
489
                coreSetConstraints core csets;
490
                List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core)
491
              end
492
      in
493
      propNom tl1
494
495
let updateConstraints node elemU csets =
496
  let update cset acc =
497
    let cnstr =
498
      match graphFindCnstr cset with
499
      | Some cn -> cn
500
      | None ->
501
          let cn = UnexpandedC [] in
502
          graphInsertCnstr cset cn;
503
          queueInsertCnstr cset;
504
          cn
505
    in
506
    match cnstr with
507
    | UnsatC -> acc
508
    | UnexpandedC parents ->
509
        graphReplaceCnstr cset (UnexpandedC (node::parents));
510
        false
511
    | OpenC parents ->
512
        graphReplaceCnstr cset (OpenC (node::parents));
513
        false
514
    | SatC -> false
515
  in
516
  let isUnsat = cssFold update csets true in
517
  if isUnsat then propagateUnsat [elemU] else ()
518
519 433c8a2e Thorsten Wißmann
let propagateNominals () =
520 4fd28192 Thorsten Wißmann
  let init = cssSingleton (csetMake ()) in
521
  graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init);
522
  graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init);
523
  graphIterStates (fun s -> propNom [State s]);
524
  graphIterCores (fun c -> propNom [Core c]);
525
  graphClearCnstr ();
526
  let fktS state =
527
    if stateGetStatus state = Unsat then ()
528
    else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state)
529
  in
530
  graphIterStates fktS;
531
  let fktC core =
532
    if coreGetStatus core = Unsat then ()
533
    else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core)
534
  in
535
  graphIterCores fktC
536
537
538
(*****************************************************************************)
539
(*                           Node Expansions                                 *)
540
(*****************************************************************************)
541
542 433c8a2e Thorsten Wißmann
let getLit sort fht solver f =
543 4fd28192 Thorsten Wißmann
  match fhtFind fht f with
544
  | Some lit -> lit
545
  | None ->
546
      let var = M.new_variable solver in
547
      let lit = M.var_to_lit var true in
548
      fhtAdd fht f lit;
549
      let () =
550
        match lfGetNeg sort f with
551
        | None -> ()
552
        | Some nf ->
553
            let nlit = M.neg_lit lit in
554
            fhtAdd fht nf nlit;
555
      in
556
      lit
557
558 16af388e Christoph Egger
let newCore sort bs defer =
559 e0f19999 Thorsten Wißmann
  (* when creating a now core from a set of formulas bs
560
        bs = { x_1, ...., x_n }
561
           = "x_1 /\ .... /\ x_n"
562
     Then we do this by:
563
564
        1. creating a new literal in the sat solver for each
565
           "boolean subformula" from the x_i. "boolean subformula" means that
566
           this subformula is not hidden under modalities but only under
567
           boolean connectives (/\, \/).
568
        2. encoding the relation between a formula and its intermediate boolean
569
           subformulas by a clause:
570
  *)
571 4fd28192 Thorsten Wißmann
  let fht = fhtInit () in
572
  let solver = M.new_solver () in
573 433c8a2e Thorsten Wißmann
  let rec addClauses f =
574 e0f19999 Thorsten Wißmann
    (* step 1: create a literal in the satsolver representing the formula f *)
575 433c8a2e Thorsten Wißmann
    let lf = getLit sort fht solver f in
576 e0f19999 Thorsten Wißmann
    (* step 2: encode relation to possible subformulas *)
577 4fd28192 Thorsten Wißmann
    match lfGetType sort f with
578
    | OrF ->
579 e0f19999 Thorsten Wißmann
        (*
580
           case 2.(a)   f =  f1 \/ f2
581
                   fill fht such that it says:
582
583
                        f  |---> lf
584
                        f1 |---> lf1
585
                        f2 |---> lf2
586
        *)
587 4fd28192 Thorsten Wißmann
        let f1 = lfGetDest1 sort f in
588
        let f2 = lfGetDest2 sort f in
589
        addClauses f1;
590
        addClauses f2;
591
        let lf1 = fhtMustFind fht f1 in
592
        let lf2 = fhtMustFind fht f2 in
593 e0f19999 Thorsten Wißmann
        (*
594
            encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
595
        *)
596 4fd28192 Thorsten Wißmann
        let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
597
        assert (okay)
598
    | AndF ->
599 e0f19999 Thorsten Wißmann
        (*
600
           case 2.(b)   f =  f1 /\ f2
601
                   fill fht such that it says:
602
603
                        f  |---> lf
604
                        f1 |---> lf1
605
                        f2 |---> lf2
606
        *)
607 4fd28192 Thorsten Wißmann
        let f1 = lfGetDest1 sort f in
608
        let f2 = lfGetDest2 sort f in
609
        addClauses f1;
610
        addClauses f2;
611
        let lf1 = fhtMustFind fht f1 in
612
        let lf2 = fhtMustFind fht f2 in
613 e0f19999 Thorsten Wißmann
        (*
614
            encode the structure of f by adding the clauses
615
                    (lf -> lf1) /\ (lf -> lf2)
616
        *)
617 4fd28192 Thorsten Wißmann
        let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
618
        assert (okay1);
619
        let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
620
        assert (okay2)
621 3eb8fabd Christoph Egger
    | MuF
622
    | NuF ->
623
       (*
624 9b6bdd74 Christoph Egger
          Dest of a fixpoint is it's unfolded version. This adds just
625
          an simple forward implication that could be optimised out
626
          though not without nontrivial transformation of code
627
628
            f = μ X . φ   |---> lf
629
            φ[X |-> f]    |---> lf1
630
631
          Then adding lf -> lf1 to minisat
632 3eb8fabd Christoph Egger
        *)
633
       let f1 = lfGetDest1 sort f in
634
       addClauses f1;
635
       let lf1 = fhtMustFind fht f1 in
636
       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
637 9b6bdd74 Christoph Egger
       assert (okay1);
638 4fd28192 Thorsten Wißmann
    | _ -> ()
639 e0f19999 Thorsten Wißmann
        (* case 2.(c)
640
            We don't need to do anything except adding f to the fht
641
        *)
642 4fd28192 Thorsten Wißmann
  in
643
  bsetIter addClauses bs;
644 16af388e Christoph Egger
  coreMake sort bs defer solver fht
645 4fd28192 Thorsten Wißmann
646 433c8a2e Thorsten Wißmann
let getNextState core =
647 e0f19999 Thorsten Wißmann
  (* Create a new state, which is obtained by a satisfying assignment of the
648
     literals of the minisat solver.
649
     In addition to that, feed the negation of the satisfying assignment back
650
     to the minisat solver in order to obtain different solutions on successive
651
     minisat calls.
652
  *)
653 4fd28192 Thorsten Wißmann
  let bs = coreGetBs core in
654 16af388e Christoph Egger
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
655
  let deferralS =
656
    if refocusing then
657
      bsetCopy bs
658
    else
659
      coreGetDeferral core
660
  in
661 4fd28192 Thorsten Wißmann
  let fht = coreGetFht core in
662
  let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
663
  let solver = coreGetSolver core in
664
  let isSat = M.invoke_solver solver litset in
665 e0f19999 Thorsten Wißmann
  (* Clearly, if the current core is unsatisfiable, no further child state can
666
     be created *)
667 4fd28192 Thorsten Wißmann
  if not isSat then None
668
  else
669
    let sort = coreGetSort core in
670 e0f19999 Thorsten Wißmann
    (* create a new set of formulas newbs with the property:
671
       if the conjunction of newbs is satisfiable, then the present core is
672
       satisfiable.
673
    *)
674 4fd28192 Thorsten Wißmann
    let newbs = bsetMake () in
675 16af388e Christoph Egger
    let newdefer = bsetMakeRealEmpty () in
676 e0f19999 Thorsten Wißmann
    (* if newbs = { l_1, .... l_n }, i.e.
677
678
            newbs = l_1 /\ ... /\ l_n
679
680
       then we can get essentially different satisfying assignments of bs by
681
       adding another clause
682
683
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
684
685
       By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
686
    *)
687 b395c870 Christoph Egger
    let rec mkExclClause deferral f acc =
688 e0f19999 Thorsten Wißmann
      (* f is a formula that is true in the current satisfying assignment *)
689 4fd28192 Thorsten Wißmann
      match lfGetType sort f with
690 433c8a2e Thorsten Wißmann
      | OrF ->
691 e0f19999 Thorsten Wißmann
          (* if f is true and a disjunction, then one of its disjuncts is true *)
692 4fd28192 Thorsten Wißmann
          let f1 = lfGetDest1 sort f in
693 433c8a2e Thorsten Wißmann
          let lf1 = fhtMustFind fht f1 in
694 e0f19999 Thorsten Wißmann
          (* if the first disjunct f1 is true, then we need to add subformulas
695
             of f1 to newbs&clause *)
696 b395c870 Christoph Egger
          if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
697 4fd28192 Thorsten Wißmann
          else
698 e0f19999 Thorsten Wißmann
            (* otherwise f2 must be true *)
699 4fd28192 Thorsten Wißmann
            let f2 = lfGetDest2 sort f in
700
            let lf2 = fhtMustFind fht f2 in
701
            assert (M.literal_status solver lf2 = M.LTRUE);
702 b395c870 Christoph Egger
            mkExclClause deferral f2 acc
703 4fd28192 Thorsten Wißmann
      | AndF ->
704 e0f19999 Thorsten Wißmann
          (* if the true f is a conjuction, then both conjunctions must be true *)
705 4fd28192 Thorsten Wißmann
          let f1 = lfGetDest1 sort f in
706
          let lf1 = fhtMustFind fht f1 in
707
          assert (M.literal_status solver lf1 = M.LTRUE);
708 b395c870 Christoph Egger
          let acc1 = mkExclClause deferral f1 acc in
709 4fd28192 Thorsten Wißmann
          let f2 = lfGetDest2 sort f in
710
          let lf2 = fhtMustFind fht f2 in
711
          assert (M.literal_status solver lf2 = M.LTRUE);
712 b395c870 Christoph Egger
          mkExclClause deferral f2 acc1
713 3eb8fabd Christoph Egger
      | MuF
714
      | NuF ->
715
         let f1 = lfGetDest1 sort f in
716 b395c870 Christoph Egger
         mkExclClause deferral f1 acc
717 4fd28192 Thorsten Wißmann
      | _ ->
718 b395c870 Christoph Egger
         (* if f is a trivial formula or modality, then add it ... *)
719
         (* ... to newbs *)
720
         bsetAdd newbs f;
721
         let defercandidate = lfGetDeferral sort f in
722 16af388e Christoph Egger
         (if (defercandidate != (Hashtbl.hash "ε") &&
723
                (refocusing || deferral = defercandidate)) then
724 b395c870 Christoph Egger
            bsetAdd newdefer f);
725
         (* ... and to the new clause *)
726
         (M.neg_lit (fhtMustFind fht f))::acc
727 4fd28192 Thorsten Wißmann
    in
728 b395c870 Christoph Egger
    let init_clause f acc =
729
      let deferral =
730 16af388e Christoph Egger
        if bsetMem deferralS f then (
731
          lfGetDeferral sort f)
732 b395c870 Christoph Egger
        else
733
          (Hashtbl.hash "ε")
734
      in
735
      mkExclClause deferral f acc
736
    in
737
    let clause = bsetFold init_clause bs [] in
738 433c8a2e Thorsten Wißmann
    let okay = M.add_clause solver clause in
739 4fd28192 Thorsten Wißmann
    assert (okay);
740 b395c870 Christoph Egger
    Some (sort, newbs, newdefer)
741 4fd28192 Thorsten Wißmann
742 b395c870 Christoph Egger
let newState sort bs defer =
743 4fd28192 Thorsten Wißmann
  let (func, sl) = !sortTable.(sort) in
744
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
745 16af388e Christoph Egger
  let exp = producer sort bs defer sl in
746 b395c870 Christoph Egger
  stateMake sort bs defer exp
747 4fd28192 Thorsten Wißmann
748 b395c870 Christoph Egger
let insertState parent sort bs defer =
749 4fd28192 Thorsten Wißmann
  let child =
750 16af388e Christoph Egger
    match graphFindState sort (bs, defer) with
751 4fd28192 Thorsten Wißmann
    | None ->
752 b395c870 Christoph Egger
        let s = newState sort bs defer in
753 16af388e Christoph Egger
        graphInsertState sort (bs, defer) s;
754 4fd28192 Thorsten Wißmann
        queueInsertState s;
755
        s
756
    | Some s -> s
757
  in
758
  coreAddChild parent child;
759
  stateAddParent child parent
760
761
let expandCore core =
762
  match getNextState core with
763 b395c870 Christoph Egger
  | Some (sort, bs, defer) ->
764
      insertState core sort bs defer;
765 4fd28192 Thorsten Wißmann
      queueInsertCore core
766
  | None ->
767
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
768
      if isUnsat then propagateUnsat [UCore (core, false)]
769
      else coreSetStatus core Open
770
771
772 16af388e Christoph Egger
let insertCore sort bs defer =
773
  match graphFindCore sort (bs, defer) with
774 4fd28192 Thorsten Wißmann
  | None ->
775 16af388e Christoph Egger
     let c = newCore sort bs defer in
776
     graphInsertCore sort (bs, defer) c;
777
     queueInsertCore c;
778
     c
779 4fd28192 Thorsten Wißmann
  | Some c -> c
780
781 433c8a2e Thorsten Wißmann
let insertRule state dep chldrn =
782
  let chldrn = listFromLazylist chldrn in
783 16af388e Christoph Egger
  let insert (isUns, acc) (sort, bs, defer) =
784 4fd28192 Thorsten Wißmann
    let bs1 = bsetAddTBox sort bs in
785 16af388e Christoph Egger
    let core = insertCore sort bs1 defer in
786 433c8a2e Thorsten Wißmann
    let isUns1 = if coreGetStatus core = Unsat then isUns else false in
787
    (isUns1, core::acc)
788 4fd28192 Thorsten Wißmann
  in
789 433c8a2e Thorsten Wißmann
  let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
790 4fd28192 Thorsten Wißmann
  let idx = stateAddRule state dep (List.rev children) in
791
  List.iter (fun c -> coreAddParent c state idx) children;
792 433c8a2e Thorsten Wißmann
  if isUnsat then begin
793
    propagateUnsat [UState (state, Some idx)];
794
    false
795
  end else true
796
797
let rec insertAllRules state = function
798
  | [] -> true
799
  | (dep, chldrn)::tl ->
800
      let notUnsat = insertRule state dep chldrn in
801
      if notUnsat then insertAllRules state tl else false
802 4fd28192 Thorsten Wißmann
803
let expandState state =
804 433c8a2e Thorsten Wißmann
  match stateNextRule state with
805 69243f7f Thorsten Wißmann
  | MultipleElements rules ->
806 433c8a2e Thorsten Wißmann
      let notUnsat = insertAllRules state rules in
807
      if notUnsat then stateSetStatus state Open
808 69243f7f Thorsten Wißmann
  | SingleElement (dep, chldrn) ->
809 433c8a2e Thorsten Wißmann
      let notUnsat = insertRule state dep chldrn in
810
      if notUnsat then queueInsertState state else ()
811 69243f7f Thorsten Wißmann
  | NoMoreElements -> stateSetStatus state Open
812 4fd28192 Thorsten Wißmann
813
814
let expandCnstr cset =
815
  let nht = nhtInit () in
816
  let mkCores f =
817
    let (sort, lf) as nom = atFormulaGetNominal f in
818
    let nomset =
819
      match nhtFind nht nom with
820
      | Some ns -> ns
821
      | None ->
822
          let cset1 = csetCopy cset in
823
          csetRemDot cset1;
824
          let bs = csetAddTBox sort cset1 in
825
          bsetAdd bs lf;
826
          nhtAdd nht nom bs;
827
          bs
828
    in
829
    bsetAdd nomset (atFormulaGetSubformula f)
830
  in
831
  csetIter cset mkCores;
832
  let inCores (sort, _) bs (isUns, acc) =
833 16af388e Christoph Egger
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
834 4fd28192 Thorsten Wißmann
    coreAddConstraintParent core cset;
835
    (coreGetStatus core = Unsat || isUns, core::acc)
836
  in
837
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
838
  if isUnsat then propagateUnsat [UCnstr cset]
839
  else
840
    match graphFindCnstr cset with
841
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
842
    | _ -> assert false
843
844
845
(*****************************************************************************)
846
(*                           The Main Loop                                   *)
847
(*****************************************************************************)
848
849 2679ab63 Thorsten Wißmann
let expandNodesLoop (recursiveAction: unit -> unit) =
850 4fd28192 Thorsten Wißmann
  match queueGetElement () with
851
  | QState state ->
852
      if stateGetStatus state = Expandable then begin
853
        expandState state;
854
        if doNominalPropagation () then begin
855
          propagateNominals ();
856 1d5d9896 Christoph Egger
          if doSatPropagation () then propagateSatMu ()
857 4fd28192 Thorsten Wißmann
        end else ()
858
      end else ();
859 2679ab63 Thorsten Wißmann
      recursiveAction ()
860 4fd28192 Thorsten Wißmann
  | QCore core ->
861
      if coreGetStatus core = Expandable then begin
862
        expandCore core;
863
        if doNominalPropagation () then begin
864
          propagateNominals ();
865 1d5d9896 Christoph Egger
          if doSatPropagation () then propagateSatMu ()
866 4fd28192 Thorsten Wißmann
        end else ()
867
      end else ();
868 2679ab63 Thorsten Wißmann
      recursiveAction ()
869 4fd28192 Thorsten Wißmann
  | QCnstr cset ->
870
      expandCnstr cset;
871 2679ab63 Thorsten Wißmann
      recursiveAction ()
872 4fd28192 Thorsten Wißmann
  | QEmpty -> ()
873
874 c2cc0c2e Thorsten Wißmann
let runReasonerStep () =
875 2679ab63 Thorsten Wißmann
  let void () = () in
876
  expandNodesLoop void; (* expand at most one node *)
877
  (* if this emptied the queue *)
878
  if queueIsEmpty () then begin
879
    (* then check whether the nominals would add further queue elements *)
880
    print_endline "Propagating nominals...";
881
    propagateNominals ()
882
  end else () (* else: the next step would be to expand another node *)
883 c2cc0c2e Thorsten Wißmann
884
let rec buildGraphLoop () =
885 2679ab63 Thorsten Wißmann
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
886
  expandNodesFurther (); (* expand as many queue elements as possible *)
887
  propagateNominals ();
888
  (* if propagating nominals added some more queue members, do all again.. *)
889 4fd28192 Thorsten Wißmann
  if queueIsEmpty () then () else buildGraphLoop ()
890 c2cc0c2e Thorsten Wißmann
891
let initReasoner sorts nomTable tbox sf =
892
  sortTable := Array.copy sorts;
893
  let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
894
  let sort = fst sf in
895
  let bs1 = bsetAddTBox sort bs in
896 16af388e Christoph Egger
  let deferrals = bsetMakeRealEmpty() in
897
  let markDeferral f =
898
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
899
      bsetAdd deferrals f;)
900
  in
901
  bsetIter markDeferral bs;
902 c2cc0c2e Thorsten Wißmann
  graphInit ();
903
  queueInit ();
904 16af388e Christoph Egger
  let root = insertCore sort bs1 deferrals in
905 c2cc0c2e Thorsten Wißmann
  graphAddRoot root
906
907
let isRootSat () =
908
  match coreGetStatus (graphGetRoot ()) with
909
  | Expandable -> None
910
  | Unsat -> Some false
911
  | Sat
912
  | Open -> if (queueIsEmpty()) then Some true else None
913
914
let reasonerFinished () =
915
  match coreGetStatus (graphGetRoot ()) with
916
  | Expandable -> false
917
  | Unsat
918
  | Sat  -> true
919
  | Open -> queueIsEmpty ()
920 3eb8fabd Christoph Egger
921 c2cc0c2e Thorsten Wißmann
922 4fd28192 Thorsten Wißmann
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
923
    @param verbose An optional switch which determines
924
    whether the procedure shall print some information on the standard output.
925
    The default is false.
926
    @param sorts An array mapping each sort (represented as an integer)
927
    to a functor and a list of sorts which are the arguments of the functor.
928
    @param nomTable A partial function mapping nominals (represented as strings)
929
    to their sorts.
930
    @param tbox A list of sorted formulae.
931
    @param sf A sorted formula.
932
    @return True if sf is satisfiable wrt tbox, false otherwise.
933
 *)
934 c2cc0c2e Thorsten Wißmann
935 4fd28192 Thorsten Wißmann
let isSat ?(verbose = false) sorts nomTable tbox sf =
936
  let start = if verbose then Unix.gettimeofday () else 0. in
937 c2cc0c2e Thorsten Wißmann
  initReasoner sorts nomTable tbox sf;
938 4fd28192 Thorsten Wißmann
  let sat =
939
    try
940
      buildGraphLoop ();
941 c2cc0c2e Thorsten Wißmann
      (* get whether the root is satisfiable *)
942
      (* we know that the reasoner finished, so the value is there, *)
943
      (* i.e. isRootSat() will give a "Some x" and not "None" *)
944
      CU.fromSome (isRootSat())
945 4fd28192 Thorsten Wißmann
    with CoAlg_finished res -> res
946
  in
947 c2cc0c2e Thorsten Wißmann
  (* print some statistics *)
948 4fd28192 Thorsten Wißmann
  if verbose then
949
    let stop = Unix.gettimeofday () in
950
    let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
951
    print_newline ();
952
    print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
953
    let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
954
    print_endline ("Added Size: " ^ (string_of_int size));
955 c2cc0c2e Thorsten Wißmann
    (*
956 4fd28192 Thorsten Wißmann
    print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
957
    let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
958
    print_endline ("Added Size: " ^ (string_of_int nsize));
959 c2cc0c2e Thorsten Wißmann
    *)
960 4fd28192 Thorsten Wißmann
    print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
961
    print_endline ("Time: " ^ (string_of_float (stop -. start)));
962
    print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
963
    print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ())));
964
    print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ())));
965
    print_newline ()
966
  else ();
967
  sat