blob: 7ca3b74ed29ddbce7f5ce2e8f7221b82392f9b33 (
plain)
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
|
package rba.tool.editor.generator.z3;
interface GeneratorConstants {
static final String CMT_AREA_LIST = "// Area definition";
static final String CMT_AREA_VISIBILITY_LABEL_LIST = "// Visibility-constrained labeling";
static final String CMT_AREA_ZORDER_LABEL_LIST = "// Constraint expression labeling";
static final String CMT_CONTENT_STATE_LIST = "// Content definition";
static final String CMT_CONTENT_STATE_LABEL_LIST = "// Labeling Priority Constraint Expressions";
static final String CMT_CONTENT_STATE_PRIORITY_COMMENT_CONNECTOR = "Priority conditional expression";
static final String CMT_CONTENT_MULTI_START = "/**";
static final String CMT_CONTENT_MULTI_END = " */";
static final String CMT_CONTENT_IMPLIES_METHOD1 = " * Contradiction verification of implication partial constraints";
static final String CMT_CONTENT_IMPLIES_METHOD2 = " * %s == TRUE holds";
static final String CMT_CONTENT_IMPLIES_METHOD3 = " * target name : ";
static final String CMT_CONTENT_IMPLIES_METHOD4 = " * expression text : ";
static final String CMT_NAME_CLOSE = "]";
static final String CMT_NAME_OPEN = "[";
static final String EX_NON = "non";
static final String EX_STD = "std";
static final String EX_MAX = "max";
static final String EX_MIN = "min";
static final String FUNC_ALLO_LIST = "createAlloList";
static final String FUNC_ALLO_VIS_CONSTR = "createAlloVisConstrList";
static final String FUNC_ALLO_VIS_CONSTR_LBL = "createAlloVisConstrLbl";
static final String FUNC_AREA_LIST = "createAreaList";
static final String FUNC_AREA_ZORDR_CONSTR = "createAreaZorderConstrList";
static final String FUNC_AREA_ZORDR_CONSTR_LBL = "createAreaZorderConstrLbl";
static final String FUNC_CST_LIST = "createContentList";
static final String FUNC_CST_CONSTR = "createConstrList";
static final String FUNC_CST_CONSTR_LBL = "createConstrLabelList";
static final String EX_CTX_MK_EQ = "ctx.mkEq";
static final String EX_CTX_MK_GT = "ctx.mkGt";
static final String EX_CTX_MK_LT = "ctx.mkLt";
static final String EX_CTX_MK_AND = "ctx.mkAnd";
static final String EX_CTX_MK_ADD = "ctx.mkAdd";
static final String EX_CTX_MK_INT = "ctx.mkInt";
static final String EX_CTX_MK_OR = "ctx.mkOr";
static final String EX_CTX_MK_XOR = "ctx.mkXor";
static final String EX_CTX_MK_NOT = "ctx.mkNot";
static final String EX_CTX_MK_IMPLIES = "ctx.mkImplies";
static final String EX_CTX_MK_GE = "ctx.mkGe";
static final String EX_CTX_MK_LE = "ctx.mkLe";
static final String EX_CTX_MK_SELECT = "ctx.mkSelect";
static final String EX_CTX_MK_STORE = "ctx.mkStore";
static final String EX_CTX_MK_EXISTS = "ctx.mkExists";
static final String EX_CTX_MK_FORALL = "ctx.mkForall";
static final String EX_CTX_MK_SYMBOL = "ctx.mkSymbol";
static final String EX_CTX_MK_ITE = "ctx.mkITE";
static final String EX_CTX_MK_TRUE = "ctx.mkTrue()";
static final String EX_CTX_MK_FALSE = "ctx.mkFalse()";
static final String EX_INT_EXPR = "(IntExpr) ";
static final String EX_BOOL_EXPR = "(BoolExpr) ";
static final String EX_ARITH_EXPR = "(ArithExpr) ";
static final String EX_ARRAY_EXPR_CATS = "(ArrayExpr) ";
static final String EX_CTX_MK_BOOL_CONST = "ctx.mkBoolConst";
static final String EX_CTX_MK_INT_CONST = "ctx.mkIntConst";
static final String EX_CTX_MK_ARRAY_CONST = "ctx.mkArrayConst";
static final String AREA_LIST_NAME = "areaList";
static final String CONSTR_LIST_NAME = "constrList";
static final String CONSTR_LABEL_LIST_NAME = "constrLabelList";
static final String CONTENT_LIST_NAME = "contentList";
static final String CONTENT_LIST_ADD = "contentList.add";
static final String CONSTR_LIST_ADD = "constrList.add";
static final String AREA_LIST_ADD = "areaList.add";
static final String CONSTR_LABEL_LIST_ADD = "constrLabelList.add";
static final String VISIBILITY = " Visibility : ";
static final String ZORDER = " Zorder : ";
static final String GET = ".get";
static final String CONST_ADDED_VALUE = "10";
static final String STR_QUOTE = "\"";
static final String _4SPACES = " ";
static final String _8SPACES = " ";
static final String OPEN = "(";
static final String CLOSE = ")";
static final String NAME_SEPARATOR = "_";
static final String COMMA = ", ";
static final String DOT = ".";
static final String NULL_STRING = "null";
static final String SL_COMMENT = "//";
static final String NL = "\r\n";
static final String END = ";";
static final String NUMBER = "#";
static final String NUMBER_ZERO = "#0:";
static final String VARIABLE_CMT = "// Variable ";
static final String VARIABLE_DEFINE = "Expr[] %s = new Expr[1];";
static final String VARIABLE_VAR_NAME = "variable_";
static final String AREASET_VAR_NAME = "areaSet_";
static final String ZONESET_VAR_NAME = "zoneSet_";
static final String VIEW_CONTENTSET_VAR_NAME = "vcontentSet_";
static final String SOUND_CONTENTSET_VAR_NAME = "scontentSet_";
static final String SETOF_OP_VAR_NAME = "setOfOperator_";
static final String ARRAY_TOP = "[0]";
static final String SET_VARIABLE_VALUE = " = ctx.mkConst(ctx.mkSymbol(\"%s\"), ctx.getIntSort());";
static final String OP_IS_DISPLAYED = "isDisplayed";
static final String OP_DISPLAYING_CONTENT = "displayingContent";
static final String OP_ALLOCATED_CONTENT = "allocatedContent";
static final String OP_CONTENTS_LIST = "contentsList";
static final String OP_IS_HIDDEN = "isHidden";
static final String OP_IS_ACTIVE = "isActive";
static final String OP_IS_VISIBLE = "isVisible";
static final String OP_ALLOCATABLE = "allocatable";
static final String OP_CONTENT_VALUE = "contentValue";
static final String OP_PRE_IS_DISPLAYED = "preIsDisplayed";
static final String OP_PRE_DISPLAYING_CONTENT = "preDisplayingContent";
static final String OP_PRE_ALLOCATED_CONTENT = "preAllocatedContent";
static final String OP_PRE_CONTENTS_LIST = "preContentsList";
static final String OP_PRE_IS_HIDDEN = "preIsHidden";
static final String OP_PRE_IS_ACTIVE = "preIsActive";
static final String OP_PRE_IS_VISIBLE = "preIsVisible";
static final String OP_PRE_ALLOCATABLE = "preAllocatable";
static final String OP_PRE_CONTENT_VALUE = "preContentValue";
static final String OP_IS_MUTED = "isMuted";
static final String OP_PRE_IS_MUTED = "preIsMuted";
static final String OP_IS_ATTENUATED = "isAttenuated";
static final String OP_PRE_IS_ATTENUATED = "preIsAttenuated";
static final String OP_IS_SOUNDING = "isSounding";
static final String OP_PRE_IS_SOUNDING = "preIsSounding";
static final String OP_OUTPUTTING_SOUND = "outputtingSound";
static final String OP_PRE_OUTPUTTING_SOUND = "preOutputtingSound";
static final String OP_IS_OUTPUTTED = "isOutputted";
static final String OP_PRE_IS_OUTPUTTED = "preIsOutputted";
static final String OP_GET_PROPERTY = "getProperty";
static final String OP_PRE_GET_PROPERTY = "preGetProperty";
static final String OP_IS_ON = "isOn";
static final String OP_PRE_IS_ON = "preIsOn";
static final String OP_IS_DEFEATED_BY = "isDefeatedBy";
static final String OP_PRE_IS_DEFEATED_BY = "preIsDefeatedBy\"";
static final String OP_DEFEATS = "defeats";
static final String OP_PRE_DEFEATS = "preDefeats";
static final String OP_IS_DISAPPEARED = "isDisappeared";
static final String OP_PRE_IS_DISAPPEARED = "preIsDisappeared";
static final String OP_IS_CANCELED = "isCanceled";
static final String OP_PRE_IS_CANCELED = "preIsCanceled";
static final String OP_HAS_BEEN_DISPLAYED = "hasBeenDisplayed";
static final String OP_PRE_HAS_BEEN_DISPLAYED = "preHasBeenDisplayed";
static final String OP_HAS_COME_EARLIER_THAN = "hasComeEarlierThan";
static final String OP_HAS_COME_LATER_THAN = "hasComeLaterThan";
static final String OP_ACTIVE_CONTENTS = "activeContents";
static final String OP_PRE_ACTIVE_CONTENTS = "preActiveContents";
static final String EMP_ARRAY_CONST = "empArrayConst";
static final String ALL_AREA_CONST = "allInstanceOfAreaConst";
static final String ALL_ZONE_CONST = "allInstanceOfZoneConst";
static final String ALL_SOUNDCONTENT_CONST = "allInstanceOfSoundContentConst";
static final String ALL_VIEWCONTENT_CONST = "allInstanceOfViewContentConst";
static final String ALLOCATABLE_SIZE = "allocatableSize";
static final String CONTENT_SIZE = "contentSize";
static final String ARRAY_EXPR_SORT = "ArrayExpr ";
static final String CONSTRAINT_PREFIX = "Constraint:";
static final String EQUAL = " = ";
static final String INT_TYPE = "int_type";
static final String BOOL_TYPE = "bool_type";
static final String IMPLIES_CONSTRAINT_METHOD_NAME = "doCalculateImpliesConstraint_%s()";
static final String IMPLIES_CONSTRAINT_METHOD = "private List<String> %s {";
static final String IMPLIES_CONSTRAINT_METHOD_DETAIL1 = "List<String> constraint_%s" + EQUAL;
static final String IMPLIES_CONSTRAINT_METHOD_DETAIL2 = "if(!constraint_%s.isEmpty() && !constraint_%s.get(0).equals(\"SAT\")) {";
static final String IMPLIES_CONSTRAINT_METHOD_DETAIL3 = "map.put(\"#%s:%s\", constraint_%s)";
static final String IMPLIES_CONSTRAINT_METHOD_DETAIL4 = "if(constraint_%s.get(0).equals(\"UNSAT\")) {";
static final String IMPLIES_CONSTRAINT_METHOD_DETAIL5 = "return map";
static final String BLOCK_CLOSE = "}";
static final String IF_OFFLINE = "if(!onlyOnline) {";
static final String STORE_TEMPLATE = EX_CTX_MK_STORE + OPEN + "%s" + COMMA + EX_CTX_MK_INT + OPEN + "%s" + CLOSE + COMMA + EX_CTX_MK_TRUE + CLOSE;;
}
|
