-
Notifications
You must be signed in to change notification settings - Fork 1
/
solver-handling.maude
140 lines (129 loc) · 4.31 KB
/
solver-handling.maude
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
mod SOLVER-DATABASE-HANDLING is
inc FM-DATABASE-HANDLING .
pr SOLVER-COMMAND-PROCESSING .
pr SOLVER-HELP .
op db-ext :_ : DatabaseExt -> Attribute .
vars T T' T'' : Term .
vars T1 T2 T3 T4 T5 : Term .
vars ME ME' : ModuleExpression .
vars DB DB' DB'' : Database .
var Atts : AttributeSet .
var X@DatabaseClass : DatabaseClass .
var O : Oid .
var DB-EXT : DatabaseExt .
var QIL : QidList .
var RES : Tuple{Database,QidList,DatabaseExt} .
crl [initialize] :
< O : X@DatabaseClass | db : DB,
input : ('initialize`[_`,_`,_`,_`,_`,_`][T, T1, T2, T3, T4, T5]),
output : nil,
db-ext : DB-EXT,
default : ME, Atts >
=> < O : X@DatabaseClass |
db : getDatabase(RES),
input : nilTermList,
output : getQidList(RES),
db-ext : getDatabaseExt(RES),
default : parseHeader(T), Atts >
if RES := procInitializeCommand('initialize`[_`,_`,_`,_`,_`,_`][T, T1, T2, T3, T4, T5], ME, DB, DB-EXT) .
crl [layerCheck] :
< O : X@DatabaseClass |
db : DB,
input : ('layerCheck_[T]),
output : nil,
db-ext : DB-EXT,
default : ME, Atts >
=> < O : X@DatabaseClass |
db : getDatabase(RES),
input : nilTermList,
output : getQidList(RES),
db-ext : getDatabaseExt(RES),
default : ME, Atts >
if RES := procLayerCheckCommand('layerCheck_[T], ME, DB, DB-EXT) .
crl [lastCheck] :
< O : X@DatabaseClass |
db : DB,
input : ('lastCheck.@Command@),
output : nil,
db-ext : DB-EXT,
default : ME, Atts >
=> < O : X@DatabaseClass |
db : DB,
input : nilTermList,
output : getQidList(RES),
db-ext : getDatabaseExt(RES),
default : ME, Atts >
if RES := procLastCheckCommand('lastCheck.@Command@, ME, DB, DB-EXT) .
crl [check] :
< O : X@DatabaseClass |
db : DB,
input : ('check_[T]),
output : nil,
db-ext : DB-EXT,
default : ME, Atts >
=> < O : X@DatabaseClass |
db : getDatabase(RES),
input : nilTermList,
output : getQidList(RES),
db-ext : getDatabaseExt(RES),
default : ME, Atts >
if RES := procCheckCommand('check_[T], ME, DB, DB-EXT) .
crl [checkWithoutParams] :
< O : X@DatabaseClass |
db : DB,
input : ('check.@Command@),
output : nil,
db-ext : DB-EXT,
default : ME, Atts >
=> < O : X@DatabaseClass |
db : DB,
input : nilTermList,
output : getQidList(RES),
db-ext : getDatabaseExt(RES),
default : ME, Atts >
if RES := procLastCheckCommand('lastCheck.@Command@, ME, DB, DB-EXT) .
crl [showCx] :
< O : X@DatabaseClass |
db : DB,
input : ('showCx.@Command@),
output : nil,
db-ext : DB-EXT,
default : ME, Atts >
=> < O : X@DatabaseClass |
db : DB,
input : nilTermList,
output : getQidList(RES),
db-ext : getDatabaseExt(RES),
default : ME, Atts >
if RES := procShowCxCommand('showCx.@Command@, ME, DB, DB-EXT) .
rl [analyze] :
< O : X@DatabaseClass |
db : DB,
input : ('analyze.@Command@),
output : nil,
db-ext : DB-EXT,
default : ME, Atts >
=> < O : X@DatabaseClass |
db : DB,
input : nilTermList,
output : procAnalyzeCommand('analyze.@Command@, ME, DB, DB-EXT),
db-ext : DB-EXT,
default : ME, Atts > .
crl [clear] :
< O : X@DatabaseClass |
db : DB,
input : ('clear.@Command@),
output : nil,
db-ext : DB-EXT,
default : ME, Atts >
=> < O : X@DatabaseClass |
db : DB,
input : nilTermList,
output : getQidList(RES),
db-ext : getDatabaseExt(RES),
default : ME, Atts >
if RES := procClearCommand('clear.@Command@, ME, DB, DB-EXT) .
rl [solver-help] :
< O : X@DatabaseClass | input : ('solver-help.@Command@), output : QIL, Atts >
=> < O : X@DatabaseClass | input : nilTermList, output : solver-help, Atts > .
endm