-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsort-system.lisp
106 lines (76 loc) · 3.18 KB
/
sort-system.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
(in-package :snark-user)
(defun declare-ec-sort-system ()
(declare-sort 'Fluent)
(declare-sort 'Event)
(declare-subsort 'Action 'Event)
(declare-sort 'ActionType)
(declare-relation 'Initiates 3 :sort '(Event Fluent Number))
(declare-relation 'Terminates 3 :sort '(Event Fluent Number))
(declare-relation 'Releases 3 :sort '(Event Fluent Number))
(declare-relation 'InitiallyP 1 :sort '(Fluent))
(declare-relation 'InitiallyN 1 :sort '(Fluent))
(declare-relation 'Happens 2 :sort '(Event Number))
(declare-relation 'Happens 3 :sort '(Event Number Number))
(declare-relation 'HoldsAt 2 :sort '(Fluent Number))
(declare-relation 'Clipped 3 :sort '(Number Fluent Number))
(declare-relation 'DeClipped 3 :sort '(Number Fluent Number))
(declare-relation 'Trajectory 4 :sort '(Fluent Number Fluent Number))
(declare-relation 'Prior 2 :sort '(Number Number))
(declare-constant 't0 :sort 'Number)
(declare-constant 't1 :sort 'Number)
(declare-constant 't2 :sort 'Number)
(declare-constant 't3 :sort 'Number)
(declare-constant 't4 :sort 'Number)
(declare-constant 'unit :sort 'Number))
(defun declare-dde-commons ()
(declare-ec-sort-system)
(snark:declare-sort 'Track)
(snark:declare-sort 'Moveable :subsorts-incompatible t)
(snark:declare-subsort 'Agent 'Moveable)
(snark:declare-subsort 'Trolley 'Moveable)
(declare-function 'action 2 :sort '(Action Agent ActionType))
(declare-constant 'I :sort 'Agent)
(snark:declare-constant 'P1 :sort 'Agent)
(snark:declare-constant 'P2 :sort 'Agent)
(snark:declare-constant 'P3 :sort 'Agent)
(snark:declare-constant 'trolley :sort 'Trolley)
(snark:declare-constant 'track1 :sort 'Track)
(snark:declare-constant 'track2 :sort 'Track)
(snark:declare-function '+ 2 :sort '(Number Number Number))
(snark:declare-function 'position 3 :sort '(Fluent Moveable Track Number))
(snark:declare-function 'switch 2 :sort '(ActionType Track Track))
(snark:declare-relation 'SwitchPoint 2 :sort '(Track Number))
(snark:declare-relation 'Heavy 1 :sort '(Agent))
(snark:declare-function 'dead 1 :sort '(Fluent Agent))
(snark:declare-function 'onrails 2 :sort '(Fluent Trolley Track))
(snark:declare-function 'damage 1 :sort '(Event Trolley))
(snark:declare-constant 'start :sort 'Event)
(snark:declare-constant 'motion :sort 'Fluent)
(snark:declare-function 'drop 3 :sort '(ActionType Agent Track Number)))
(defun +-REWRITER (term subst)
(let ((c1 (first (args term)))
(c2 (second (args term))))
(dereference c1 subst
:if-constant
(dereference c2 subst
:if-constant
(+ c1 c2)
:if-variable none
:if-compound none)
:if-variable none
:if-compound none)))
(defun assert-add-table (end)
(loop for i from 0 to end do
(loop for j from 0 to end do
(if (< i j)
(assert `(Prior ,i ,j)))
(if (< j i)
(assert `(Prior ,j ,i)))
(assert `(= ,(+ i j) (+ ,i ,j)))
(assert `(= ,(+ i j) (+ ,j ,i ))))))
(defun assert-domain (end)
(assert `(forall ((?p Number))
(implies (Prior ?p ,end)
,(cons 'or (loop for i from 0 to end collect
`(= ,i ?p)))))))
(defun )