aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend156
1 files changed, 122 insertions, 34 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
index d4c76bb4..379e334a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
@@ -170,6 +170,7 @@ class PatternGenerator {
170 ///////////////////////// 170 /////////////////////////
171 // 0.1 Existence 171 // 0.1 Existence
172 ///////////////////////// 172 /////////////////////////
173 /** [[exist(element)]]=1 */
173 private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 174 private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
174 find interpretation(problem,interpretation); 175 find interpretation(problem,interpretation);
175 LogicProblem.elements(problem,element); 176 LogicProblem.elements(problem,element);
@@ -178,6 +179,7 @@ class PatternGenerator {
178 PartialInterpretation.newElements(interpretation,element); 179 PartialInterpretation.newElements(interpretation,element);
179 } 180 }
180 181
182 /** [[exist(element)]]>=1/2 */
181 private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 183 private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
182 find mustExist(problem,interpretation,element); 184 find mustExist(problem,interpretation,element);
183 } or { 185 } or {
@@ -198,57 +200,143 @@ class PatternGenerator {
198 //////////////////////// 200 ////////////////////////
199 // 0.2 Equivalence 201 // 0.2 Equivalence
200 //////////////////////// 202 ////////////////////////
201 pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { 203 pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement)
204 // For non-primitive type. Boolean types always must equivalent or cannot equivalent
205 {
202 find mayExist(problem,interpretation,a); 206 find mayExist(problem,interpretation,a);
203 find mayExist(problem,interpretation,b); 207 find mayExist(problem,interpretation,b);
204 a == b; 208 a == b;
209 } or {
210 find mayExist(problem,interpretation,a);
211 find mayExist(problem,interpretation,b);
212 IntegerElement(a);
213 IntegerElement(b);
214 PrimitiveElement.valueSet(a,false);
215 } or {
216 find mayExist(problem,interpretation,a);
217 find mayExist(problem,interpretation,b);
218 IntegerElement(a);
219 IntegerElement(b);
220 PrimitiveElement.valueSet(b,false);
221 } or {
222 find mayExist(problem,interpretation,a);
223 find mayExist(problem,interpretation,b);
224 RealElement(a);
225 RealElement(b);
226 PrimitiveElement.valueSet(a,false);
227 } or {
228 find mayExist(problem,interpretation,a);
229 find mayExist(problem,interpretation,b);
230 RealElement(a);
231 RealElement(b);
232 PrimitiveElement.valueSet(b,false);
233 } or {
234 find mayExist(problem,interpretation,a);
235 find mayExist(problem,interpretation,b);
236 RealElement(a);
237 IntegerElement(b);
238 PrimitiveElement.valueSet(a,false);
239 } or {
240 find mayExist(problem,interpretation,a);
241 find mayExist(problem,interpretation,b);
242 RealElement(a);
243 IntegerElement(b);
244 PrimitiveElement.valueSet(b,false);
245 } or {
246 find mayExist(problem,interpretation,a);
247 find mayExist(problem,interpretation,b);
248 IntegerElement(a);
249 RealElement(b);
250 PrimitiveElement.valueSet(a,false);
251 } or {
252 find mayExist(problem,interpretation,a);
253 find mayExist(problem,interpretation,b);
254 IntegerElement(a);
255 RealElement(b);
256 PrimitiveElement.valueSet(b,false);
257 } or {
258 find mayExist(problem,interpretation,a);
259 find mayExist(problem,interpretation,b);
260 StringElement(a);
261 StringElement(b);
262 PrimitiveElement.valueSet(a,false);
263 } or {
264 find mayExist(problem,interpretation,a);
265 find mayExist(problem,interpretation,b);
266 StringElement(a);
267 StringElement(b);
268 PrimitiveElement.valueSet(b,false);
205 } 269 }
270
206 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { 271 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) {
272 // For non-primitive and Boolean primitive type
207 find mustExist(problem,interpretation,a); 273 find mustExist(problem,interpretation,a);
208 find mustExist(problem,interpretation,b); 274 find mustExist(problem,interpretation,b);
209 a == b; 275 a == b;
276 } or {
277 find mustExist(problem,interpretation,a);
278 find mustExist(problem,interpretation,b);
279 PrimitiveElement.valueSet(a,true);
280 PrimitiveElement.valueSet(b,true);
281 IntegerElement.value(a,value);
282 IntegerElement.value(b,value);
283 } or {
284 find mustExist(problem,interpretation,a);
285 find mustExist(problem,interpretation,b);
286 PrimitiveElement.valueSet(a,true);
287 PrimitiveElement.valueSet(b,true);
288 RealElement.value(a,value);
289 RealElement.value(b,value);
290 } or {
291 find mustExist(problem,interpretation,a);
292 find mustExist(problem,interpretation,b);
293 PrimitiveElement.valueSet(a,true);
294 PrimitiveElement.valueSet(b,true);
295 RealElement.value(a,value);
296 IntegerElement.value(b,value);
297 } or {
298 find mustExist(problem,interpretation,a);
299 find mustExist(problem,interpretation,b);
300 PrimitiveElement.valueSet(a,true);
301 PrimitiveElement.valueSet(b,true);
302 IntegerElement.value(a,value);
303 RealElement.value(b,value);
304 } or {
305 find mustExist(problem,interpretation,a);
306 find mustExist(problem,interpretation,b);
307 PrimitiveElement.valueSet(a,true);
308 PrimitiveElement.valueSet(b,true);
309 StringElement.value(a,value);
310 StringElement.value(b,value);
210 } 311 }
211 312
212 ////////////////////////
213 // 0.3 Required Patterns by TypeIndexer
214 ////////////////////////
215 «typeIndexer.requiredQueries»
216
217 ////////// 313 //////////
218 // 1. Problem-Specific Base Indexers 314 // 1. Problem-Specific Base Indexers
219 ////////// 315 //////////
220 // 1.1 Type Indexers 316 // 1.1 Type Indexers
221 ////////// 317 //////////
222 // 1.1.1 primitive Type Indexers 318 // 1.1.1 Required Patterns by TypeIndexer
223 ////////// 319 //////////
224««« pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 320 «typeIndexer.requiredQueries»
225««« find interpretation(problem,interpretation); 321 //////////
226««« PartialInterpretation.booleanelements(interpretation,element); 322 // 1.1.2 primitive Type Indexers
227««« } 323 //////////
228««« pattern instanceofInteger(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 324 // Currently unused. Refer primitive types as:
229««« find interpretation(problem,interpretation); 325 // > PrimitiveElement(element)
230««« PartialInterpretation.integerelements(interpretation,element); 326 // specific types are referred as:
231««« } or { 327 // > BooleanElement(variableName)
232««« find interpretation(problem,interpretation); 328 // > IntegerElement(variableName)
233««« PartialInterpretation.newIntegers(interpetation,element); 329 // > RealElement(variableName)
234««« } 330 // > StringElement(variableName)
235««« pattern instanceofReal(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 331 // And their value as
236««« find interpretation(problem,interpretation); 332 // > BooleanElement.value(variableName,value)
237««« PartialInterpretation.realelements(interpretation,element); 333 // > IntegerElement.value(variableName,value)
238««« } or { 334 // > RealElement.value(variableName,value)
239««« find interpretation(problem,interpretation); 335 // > StringElement.value(variableName,value)
240««« PartialInterpretation.newReals(interpetation,element); 336 // Whether a value is set is defined by:
241««« } 337 // > PrimitiveElement.valueSet(variableName,isFilled);
242««« pattern instanceofString(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
243««« find interpretation(problem,interpretation);
244««« PartialInterpretation.stringelements(interpretation,element);
245««« } or {
246««« find interpretation(problem,interpretation);
247««« PartialInterpretation.newStrings(interpetation,element);
248««« }
249
250 ////////// 338 //////////
251 // 1.1.2 domain-specific Type Indexers 339 // 1.1.3 domain-specific Type Indexers
252 ////////// 340 //////////
253 «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)» 341 «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)»
254 342