-
Notifications
You must be signed in to change notification settings - Fork 8
/
carnival.lisp
84 lines (74 loc) · 2.44 KB
/
carnival.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
;; inspired by
;; https://github.com/saezlab/CARNIVAL
(defvar *node-labels*)
(defun new-carnival (title)
(setq *ltms* (create-ltms (format nil "CARNIVAL ~A" title)))
(setq *node-labels* '()))
(defmacro node (val n &key (measured? nil) (top? nil))
(let ((label (ecase val (+ :TRUE) (- :FALSE))))
`(let ((node (tms-create-node *ltms* ',n :ASSUMPTIONP t)))
(push (cons ',n ',label) *node-labels*)
,(if top?
`(enable-assumption node ',label)
t))))
#|
(defmacro node (val n &key (measured? nil) (top? nil))
(let ((label (ecase val (+ :TRUE) (- :FALSE))))
`(progn
(push (cons ',n ',label) *node-labels*)
,(if top?
`(let ((node (tms-create-node *ltms* ',n :ASSUMPTIONP t)))
(enable-assumption node ',label)
node)
`(tms-create-node *ltms* ',n)))))
|#
(defun edge-name (val src dst)
(read-from-string (concatenate 'string (string src) (string val) (string dst))))
(defmacro edge (val src dst)
(let ((edge-name (edge-name val src dst)))
`(let ((edge (tms-create-node *ltms* ',edge-name :ASSUMPTIONP t)))
(enable-assumption edge :TRUE)
,(if (ecase val (+ t) (- nil))
`(compile-formula
*ltms*
'(:IMPLIES ,edge-name
(:AND
(:IMPLIES ,src ,dst)
(:IMPLIES (:NOT ,src) (:NOT ,dst)))))
`(compile-formula
*ltms*
'(:IMPLIES ,edge-name
(:AND
(:IMPLIES ,src (:NOT ,dst))
(:IMPLIES (:NOT ,src) ,dst))))))))
#|
(defmacro edge (val src dst)
(let ((edge-name (edge-name val src dst)))
(if (ecase val (+ t) (- nil))
`(compile-formula
*ltms*
'(:AND
(:IMPLIES ,src ,dst)
(:IMPLIES (:NOT ,src) (:NOT ,dst))))
`(compile-formula
*ltms*
'(:AND
(:IMPLIES ,src (:NOT ,dst))
(:IMPLIES (:NOT ,src) ,dst))))))
|#
(defun solve ()
'ok)
(defun check-consistency (&aux c)
(setq c t)
(mapc #'(lambda (x)
(let ((n (car x))
(v (cdr x)))
(let ((node (find-node *ltms* n)))
(unless (equal v (tms-node-label node))
(setq c nil)
(format t "~%Node ~A inconsistent." n)
(explain-node node)))))
*node-labels*)
c)
(defun what-node (n)
(explain-node (find-node *ltms* n)))