-
Notifications
You must be signed in to change notification settings - Fork 8
/
atms.lisp
556 lines (476 loc) · 18.4 KB
/
atms.lisp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
;;; -*- Mode: LISP; Syntax: Common-lisp; -*-
;;; Assumption-based truth maintenance system, version 61 of 7/21/92.
;;; Copyright (c) 1986-1993, Kenneth D. Forbus, Northwestern University,
;;; and Johan de Kleer, the Xerox Corporation.
;;; All rights reserved.
;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty. The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.
(in-package :COMMON-LISP-USER)
;;; Definitions.
(defstruct (atms (:PRINT-FUNCTION print-atms))
(title nil)
(node-counter 0) ; unique namer for nodes.
(just-counter 0) ; unique namer for justifications.
(env-counter 0) ; Unique id for environments.
(nodes nil) ; List of all atms nodes.
(justs nil) ; List of all justifications.
(contradictions nil) ; List of contradiction nodes.
(assumptions nil) ; List of all atms assumptions.
(debugging nil) ; Trace grungy details.
(nogood-table nil)
(contra-node nil) ; A dummy contradiction node.
(env-table nil)
(empty-env nil) ; Empty environment.
(node-string nil)
(enqueue-procedure nil))
(defun print-atms (atms stream ignore)
(declare (ignore ignore))
(format stream "#<ATMS: ~A>" (atms-title atms)))
(defstruct (tms-node (:PRINT-FUNCTION print-tms-node))
(index 0) ;; Unique name.
(datum nil) ; Pointer to IE data structures.
(label nil) ; minimal envs believed under
(justs nil) ; providers of support
(consequences nil) ; provides support for.
(contradictory? nil) ; flag marking it as contradictory.
(assumption? nil) ; flag marking it as n assumption.
(rules nil) ; run when label non-empty.
(atms nil))
(defun print-tms-node (node stream ignore)
(declare (ignore ignore))
(if (tms-node-assumption? node)
(format stream "A-~D" (tms-node-index node))
(format stream "#<NODE: ~A>" (node-string node))))
(defstruct (just (:PRINT-FUNCTION print-just))
(index 0)
(informant nil)
(consequence nil)
(antecedents nil))
(defun print-just (just stream ignore)
(declare (ignore ignore))
(format stream "<~A ~D>" (just-informant just)
(just-index just)))
(defstruct (env (:PREDICATE env?)
(:PRINT-FUNCTION print-env-structure))
(index 0)
(count 0) ; Number of assumptions.
(assumptions nil)
(nodes nil)
(nogood? nil)
(rules nil)) ; Call this if becomes nogood.
(defun print-env-structure (env stream ignore)
(declare (ignore ignore))
(format stream "E-~D" (env-index env)))
(defun node-string (node)
(funcall (atms-node-string (tms-node-atms node)) node))
(defmacro debugging (atms msg &optional node &rest args)
`(when (atms-debugging ,atms)
(format *trace-output*
,msg (if ,node (node-string ,node)) ,@args)))
(defun default-node-string (n) (format nil "~A" (tms-node-datum n)))
(defun ordered-insert (item list test)
(cond ((null list) (list item))
((funcall test item (car list)) (cons item list))
((eq item (car list)) list)
(t (cons (car list) (ordered-insert item (cdr list) test)))))
(defmacro ordered-push (item list test)
`(setq ,list (ordered-insert ,item ,list ,test)))
(defun assumption-order (a1 a2)
(< (tms-node-index a1) (tms-node-index a2)))
(defun env-order (e1 e2)
(< (env-index e1) (env-index e2)))
;;; Basic inference engine interface.
(defun create-atms (title &key (node-string 'default-node-string)
(debugging NIL)
(enqueue-procedure NIL))
(let ((atms (make-atms :TITLE title
:NODE-STRING node-string
:DEBUGGING debugging
:ENQUEUE-PROCEDURE enqueue-procedure)))
(setf (atms-contra-node atms)
(tms-create-node atms "The contradiction"
:CONTRADICTORYP t))
(setf (atms-empty-env atms) (create-env atms nil))
atms))
(defun change-atms (atms &key node-string
enqueue-procedure debugging)
(if node-string (setf (atms-node-string atms) node-string))
(if debugging (setf (atms-debugging atms) debugging))
(if enqueue-procedure
(setf (atms-enqueue-procedure atms) enqueue-procedure)))
(defun true-node? (node)
(eq (car (tms-node-label node))
(atms-empty-env (tms-node-atms node))))
(defun in-node? (n &optional env)
(if env
(some #'(lambda (le) (subset-env? le env))
(tms-node-label n))
(not (null (tms-node-label n)))))
(defun out-node? (n env) (not (in-node? n env)))
(defun node-consistent-with? (n env)
(some #'(lambda (le) (not (env-nogood? (union-env le env))))
(tms-node-label n)))
(defun tms-create-node (atms datum &key assumptionp contradictoryp
&aux node)
(setq node (make-tms-node :INDEX (incf (atms-node-counter atms))
:DATUM datum
:ASSUMPTION? assumptionp
:CONTRADICTORY? contradictoryp
:ATMS atms))
(push node (atms-nodes atms))
(if contradictoryp (push node (atms-contradictions atms)))
(when assumptionp
(push node (atms-assumptions atms))
(push (create-env atms (list node)) (tms-node-label node)))
node)
(defun assume-node (node &aux atms)
(unless (tms-node-assumption? node)
(setq atms (tms-node-atms node))
(debugging atms "~%Converting ~A into an assumption" node)
(setf (tms-node-assumption? node) t)
(push node (atms-assumptions atms))
(update (list (create-env atms (list node)))
node
'ASSUME-NODE)))
(defun make-contradiction
(node &aux (atms (tms-node-atms node)) nogood)
(unless (tms-node-contradictory? node)
(setf (tms-node-contradictory? node) t)
(push node (atms-contradictions atms))
(do nil (nil)
(if (setq nogood (car (tms-node-label node)))
(new-nogood atms nogood 'MAKE-CONTRADICTION)
(return nil)))))
(defun justify-node (informant consequence antecedents &aux just atms)
(setq atms (tms-node-atms consequence)
just (make-just :INDEX (incf (atms-just-counter atms))
:INFORMANT informant
:CONSEQUENCE consequence
:ANTECEDENTS antecedents))
(push just (tms-node-justs consequence))
(dolist (node antecedents) (push just (tms-node-consequences node)))
(push just (atms-justs atms))
(debugging atms
"~%Justifying ~A in terms of ~A on ~A"
consequence
informant
(mapcar #'node-string antecedents))
(propagate just nil (list (atms-empty-env atms)))
just)
(defun nogood-nodes (informant nodes)
(justify-node informant
(atms-contra-node (tms-node-atms (car nodes)))
nodes))
;;; Label updating
(defun propagate (just antecedent envs &aux new-envs)
(if (setq new-envs (weave antecedent envs (just-antecedents just)))
(update new-envs (just-consequence just) just)))
(defun update (new-envs consequence just &aux atms enqueuef)
(setq atms (tms-node-atms consequence))
(when (tms-node-contradictory? consequence)
(dolist (env new-envs) (new-nogood atms env just))
(return-from update nil))
(setq new-envs (update-label consequence new-envs))
(unless new-envs (return-from update nil))
(when (setq enqueuef (atms-enqueue-procedure atms))
(dolist (rule (tms-node-rules consequence))
(funcall enqueuef rule))
(setf (tms-node-rules consequence) nil))
(dolist (supported-just (tms-node-consequences consequence))
(propagate supported-just consequence new-envs)
(do ((new-envs new-envs (cdr new-envs)))
((null new-envs))
(unless (member (car new-envs) (tms-node-label consequence))
(rplaca new-envs nil)))
(setq new-envs (delete nil new-envs :TEST #'eq))
(unless new-envs (return-from update nil))))
(defun update-label (node new-envs &aux envs)
(setq envs (tms-node-label node))
(do ((new-envs new-envs (cdr new-envs)))
((null new-envs))
(do ((nenvs envs (cdr nenvs)))
((null nenvs) (push (car new-envs) envs))
(cond ((null (car nenvs)))
((null (car new-envs)))
((case (compare-env (car new-envs) (car nenvs))
((:EQ :S21) (rplaca new-envs nil))
(:S12 (setf (env-nodes (car nenvs))
(delete node (env-nodes (car nenvs))
:COUNT 1))
(rplaca nenvs nil)))))))
(setq new-envs (delete nil new-envs :TEST #'eq))
(dolist (new-env new-envs) (push node (env-nodes new-env)))
(setf (tms-node-label node) (delete nil envs :TEST #'eq))
new-envs)
(defun weave (antecedent envs antecedents &aux new-envs new-env)
(setq envs (copy-list envs))
(dolist (node antecedents)
(unless (eq node antecedent)
(setq new-envs nil)
(dolist (env envs)
(if env
(dolist (node-env (tms-node-label node))
(setq new-env (union-env env node-env))
(unless (env-nogood? new-env)
(do ((nnew-envs new-envs (cdr nnew-envs)))
((null nnew-envs) (push new-env new-envs))
(when (car nnew-envs)
(case (compare-env new-env (car nnew-envs))
((:EQ :S21) (return nil))
(:S12 (rplaca nnew-envs nil)))))))))
(setq envs (delete nil new-envs :TEST #'eq))
(unless envs (return-from weave nil))))
envs)
(defun in-antecedent? (nodes)
(or (null nodes)
(weave? (atms-empty-env (tms-node-atms (car nodes))) nodes)))
(defun weave? (env nodes &aux new-env)
(cond ((null nodes) t)
(t (dolist (e (tms-node-label (car nodes)))
(setq new-env (union-env e env))
(unless (env-nogood? new-env)
(if (weave? new-env (cdr nodes))
(return T)))))))
(defun supporting-antecedent? (nodes env)
(dolist (node nodes t) (unless (in-node? node env) (return nil))))
(defun remove-node (node &aux atms)
(if (tms-node-consequences node)
(error "Can't remove node with consequences"))
(setq atms (tms-node-atms node))
(setf (atms-nodes atms)
(delete node (atms-nodes atms) :test #'eq :count 1))
(dolist (just (tms-node-justs node))
(dolist (ant (just-antecedents just))
(setf (tms-node-consequences ant)
(delete just (tms-node-consequences ant)
:test #'eq :count 1))))
(dolist (env (tms-node-label node))
(setf (env-nodes env)
(delete node (env-nodes env) :test #'eq :count 1))))
;;; Creating and extending environments.
(defun create-env (atms assumptions &aux e)
(setq e (make-env :INDEX (incf (atms-env-counter atms))
:ASSUMPTIONS assumptions
:COUNT (length assumptions)))
(setf (atms-env-table atms)
(insert-in-table (atms-env-table atms) e))
(set-env-contradictory atms e)
e)
(defun union-env (e1 e2)
(when (> (env-count e1)
(env-count e2))
(psetq e1 e2 e2 e1))
(dolist (assume (env-assumptions e1))
(setq e2 (cons-env assume e2))
(if (env-nogood? e2) (return nil)))
e2)
(defun cons-env (assumption env &aux nassumes)
(setq nassumes (ordered-insert assumption
(env-assumptions env)
#'assumption-order))
(or (lookup-env nassumes)
(create-env (tms-node-atms assumption) nassumes)))
(defun find-or-make-env (assumptions atms)
(unless assumptions
(return-from find-or-make-env (atms-empty-env atms)))
;; Presumes the list of assumptions is ordered properly
(or (lookup-env assumptions)
(create-env atms assumptions)))
;;; Env tables.
(defun insert-in-table (table env &aux count entry)
(setq count (env-count env)
entry (assoc count table :TEST #'=))
(cond (entry (setf (cdr entry) (cons env (cdr entry))) table)
(t (ordered-insert
(list count env) table
#'(lambda (entry1 entry2)
(< (car entry1) (car entry2)))))))
(defun lookup-env (assumes)
(dolist (env (cdr (assoc (length assumes)
(atms-env-table (tms-node-atms (car assumes)))
:TEST #'=))
nil)
(if (equal (env-assumptions env) assumes)
(return env))))
(defun subset-env? (e1 e2)
(cond ((eq e1 e2) t)
((> (env-count e1)
(env-count e2)) nil)
((subsetp (env-assumptions e1)
(env-assumptions e2)))))
(defun compare-env (e1 e2)
(cond ((eq e1 e2) :EQ)
((< (env-count e1) (env-count e2))
(if (subsetp (env-assumptions e1)
(env-assumptions e2))
:S12))
((subsetp (env-assumptions e2) (env-assumptions e1))
:S21)))
;;; Processing nogoods
(defun new-nogood (atms cenv just &aux count)
(debugging atms (format nil "~% ~A new minimal nogood." cenv))
(setf (env-nogood? cenv) just)
(remove-env-from-labels cenv atms)
(setf (atms-nogood-table atms)
(insert-in-table (atms-nogood-table atms) cenv))
(setq count (env-count cenv))
(dolist (entry (atms-nogood-table atms))
(when (> (car entry) count)
(dolist (old (cdr entry))
(if (subset-env? cenv old)
(setf (cdr entry) (delete old (cdr entry) :COUNT 1))))))
(dolist (entry (atms-env-table atms))
(when (> (car entry) count)
(dolist (old (cdr entry))
(when (and (not (env-nogood? old))
(subset-env? cenv old))
(setf (env-nogood? old) cenv)
(remove-env-from-labels old atms))))))
(defun set-env-contradictory (atms env &aux count)
(cond ((env-nogood? env) t)
(t (setq count (env-count env))
(dolist (entry (atms-nogood-table atms))
(cond ((> (car entry) count)
(return nil))
(t (dolist (cenv (cdr entry))
(when (subset-env? cenv env)
(setf (env-nogood? env)
cenv)
(return t)))))))))
(defun remove-env-from-labels (env atms &aux enqueuef)
(when (setq enqueuef (atms-enqueue-procedure atms))
(dolist (rule (env-rules env))
(funcall enqueuef rule))
(setf (env-rules env) nil))
(dolist (node (env-nodes env))
(setf (tms-node-label node)
(delete env (tms-node-label node) :COUNT 1))))
;;; Interpretation construction
(proclaim '(special *solutions*))
(defun interpretations (atms choice-sets
&optional defaults &aux solutions)
(if (atms-debugging atms)
(format *trace-output*
"~% Constructing interpretations depth-first..."))
(let ((*solutions* nil)
(choice-sets
(mapcar #'(lambda (alt-set)
(mapcan #'(lambda (alt)
(copy-list (tms-node-label alt)))
alt-set))
choice-sets)))
(dolist (choice (car choice-sets))
(get-depth-solutions1 choice (cdr choice-sets)))
(setq *solutions* (delete nil *solutions* :TEST #'eq))
(unless *solutions*
(if choice-sets (return-from interpretations nil)
(setq *solutions* (list (atms-empty-env atms)))))
(when defaults
(setq solutions *solutions* *solutions* nil)
(dolist (solution solutions)
(extend-via-defaults solution defaults defaults)))
(delete nil *solutions* :TEST #'eq)))
(defun get-depth-solutions1 (solution choice-sets
&aux new-solution)
(cond ((null choice-sets)
(unless (do ((old-solutions *solutions* (cdr old-solutions)))
((null old-solutions))
(when (car old-solutions)
(case (compare-env (car old-solutions) solution)
((:EQ :S12) (return t))
(:S21 (rplaca old-solutions nil)))))
(push solution *solutions*)))
((env-nogood? solution)) ;something died.
(t (dolist (choice (car choice-sets))
(setq new-solution (union-env solution choice))
(unless (env-nogood? new-solution)
(get-depth-solutions1 new-solution
(cdr choice-sets)))))))
(defun extend-via-defaults (solution remaining original)
(do ((new-solution)
(defaults remaining (cdr defaults)))
((null defaults)
(or (member solution *solutions* :TEST #'eq)
(dolist (default original)
(or (member default (env-assumptions solution)
:TEST #'eq)
(env-nogood? (cons-env default solution))
(return t)))
(push solution *solutions*)))
(setq new-solution (cons-env (car defaults) solution))
(unless (env-nogood? new-solution)
(extend-via-defaults new-solution (cdr defaults) original))))
;;; Generating explanations
;;; This returns a list of justifications which form a DAG for the
;;; derivation. This is quite complicated because this is really a
;;; simple consequent JTMS.
(defun explain-node (node env) (explain-node-1 env node nil nil))
(defun explain-node-1 (env node queued-nodes explanation)
(cond ((member node queued-nodes) nil)
((and (tms-node-assumption? node)
(member node (env-assumptions env)))
(cons (cons 'ASSUME node) explanation))
((dolist (just explanation)
(if (if (listp just)
(eq (cdr just) node) (eq (just-consequence just) node))
(return explanation))))
(t (setq queued-nodes (cons node queued-nodes))
(dolist (just (tms-node-justs node))
(unless (dolist (a (just-antecedents just))
(unless (in-node? a env) (return t)))
(let ((new-explanation explanation))
(dolist (a (just-antecedents just)
(return-from explain-node-1 (cons just new-explanation)))
(setq new-explanation
(explain-node-1 env a queued-nodes new-explanation))
(unless new-explanation (return nil)))))))))
;;; Printing
(defun why-node (node &optional (stream t) (prefix ""))
(format stream "~%<~A~A,{" prefix (tms-node-datum node))
(dolist (e (tms-node-label node))
(env-string e stream))
(format stream "}>"))
(defun why-nodes (atms &optional (stream t))
(dolist (n (reverse (atms-nodes atms))) (why-node n stream)))
(defun node-justifications (node &optional (stream t))
(format t "~% For ~A:" (node-string node))
(dolist (j (tms-node-justs node))
(print-justification j stream)))
(defun print-justification (j &optional (stream t))
(format stream "~% ~A, " (just-informant j))
(dolist (a (just-antecedents j))
(why-node a stream " ")))
(defun e (atms n)
(dolist (bucket (atms-env-table atms))
(dolist (env (cdr bucket))
(if (= (env-index env) n) (return-from e env)))))
(defun print-env (e &optional (stream t))
(format stream "~%~A:~A"
e (if (env-nogood? e)
"* " " "))
(env-string e stream))
(defun env-string (e &optional stream
&aux assumptions strings printer)
(setq assumptions (env-assumptions e))
(when assumptions
(setq printer (atms-node-string (tms-node-atms (car assumptions)))))
(dolist (a assumptions) (push (funcall printer a) strings))
(format stream "{~{~A~^,~}}" (sort strings #'string-lessp)))
;;; Printing global data
(defun print-nogoods (atms &optional (stream t))
(print-env-table (atms-nogood-table atms) stream))
(defun print-envs (atms &optional (stream t))
(print-env-table (atms-env-table atms) stream))
(defun print-env-table (table stream)
(dolist (bucket table)
(dolist (env (cdr bucket))
(print-env env stream))))
(defun print-atms-statistics (atms)
(print-table "~% For env table:" (atms-env-table atms))
(print-table "~% For nogood table:" (atms-nogood-table atms)))
(defun print-table (msg table)
(format t msg)
(dolist (entry table)
(format t "~% Length ~D, ~D" (car entry)
(length (cdr entry)))))