1 files changed, 156 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend
new file mode 100644
index 00000000..38633c07
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend
@@ -0,0 +1,156 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
+import java.util.HashMap
+import java.util.Map
+import java.util.Set
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
+import java.util.HashSet
+class ScopePropagator {
+        PartialInterpretation partialInterpretation
+        Map<PartialTypeInterpratation,Scope> type2Scope
+        
+        val Map<Scope, Set<Scope>> superScopes
+        val Map<Scope, Set<Scope>> subScopes
+        
+        public new(PartialInterpretation p) {
+                partialInterpretation = p
+                type2Scope = new HashMap
+                for(scope : p.scopes) {
+                        type2Scope.put(scope.targetTypeInterpretation,scope)
+                }
+                
+                superScopes = new HashMap
+                subScopes = new HashMap
+                for(scope : p.scopes) {
+                        superScopes.put(scope,new HashSet)
+                        subScopes.put(scope,new HashSet)
+                }
+                
+                for(scope : p.scopes) {
+                        val target = scope.targetTypeInterpretation
+                        if(target instanceof PartialComplexTypeInterpretation) {
+                                val supertypeInterpretations = target.supertypeInterpretation
+                                for(supertypeInterpretation : supertypeInterpretations) {
+                                        val supertypeScope = type2Scope.get(supertypeInterpretation)
+                                        superScopes.get(scope).add(supertypeScope)
+                                        subScopes.get(supertypeScope).add(scope)
+                                }
+                        }
+                }
+        }
+        
+        def public propagateAllScopeConstraints() {
+                var boolean hadChanged
+                do{
+                        hadChanged = false
+                        for(superScopeEntry : superScopes.entrySet) {
+                                val sub = superScopeEntry.key
+                                hadChanged = propagateLowerLimitUp(sub,partialInterpretation) || hadChanged
+                                hadChanged = propagateUpperLimitDown(sub,partialInterpretation) || hadChanged
+                                for(sup: superScopeEntry.value) {
+                                        hadChanged = propagateLowerLimitUp(sub,sup) || hadChanged
+                                        hadChanged = propagateUpperLimitDown(sub,sup) || hadChanged
+                                }
+                        }
+                } while(hadChanged)
+//              println('''All constraints are propagated.''')
+        }
+        
+        def public propagateAdditionToType(PartialTypeInterpratation t) {
+//              println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
+                val targetScope = type2Scope.get(t)
+                targetScope.removeOne
+                val sups = superScopes.get(targetScope)
+                sups.forEach[removeOne]
+                if(this.partialInterpretation.minNewElements > 0) {
+                        this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1
+                }
+                if(this.partialInterpretation.maxNewElements > 0) {
+                        this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1
+                } else if(this.partialInterpretation.maxNewElements === 0) {
+                        throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''')
+                }
+                
+//              subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)]
+//              for(sup: sups) {
+//                      subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)]
+//              }
+//              for(scope : type2Scope.values) {
+//                      propagateUpperLimitDown(scope,partialInterpretation)
+//              }
+                propagateAllScopeConstraints
+                
+//              println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''')
+//              println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''')
+//              this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')]
+//              println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
+        }
+        
+        private def propagateLowerLimitUp(Scope subScope, Scope superScope) {
+                if(subScope.minNewElements>superScope.minNewElements) {
+//                      println('''
+//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»
+//                      superScope.minNewElements «superScope.minNewElements» = subScope.minNewElements «subScope.minNewElements»
+//                      ''')
+                        superScope.minNewElements = subScope.minNewElements
+                        return true
+                } else {
+                        return false
+                }
+        }
+        
+        private def propagateUpperLimitDown(Scope subScope, Scope superScope) {
+                if(superScope.maxNewElements>=0 && (superScope.maxNewElements<subScope.maxNewElements || subScope.maxNewElements<0)) {
+//                      println('''
+//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»
+//                      subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements»
+//                      ''')
+                        subScope.maxNewElements = superScope.maxNewElements
+                        return true
+                } else {
+                        return false
+                }
+        }
+        
+        private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) {
+                if(subScope.minNewElements>p.minNewElements) {
+//                      println('''
+//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes
+//                      p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements»
+//                      ''')
+                        p.minNewElements = subScope.minNewElements
+                        return true
+                } else {
+                        return false
+                }
+        }
+        
+        private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) {
+                if(p.maxNewElements>=0 && (p.maxNewElements<subScope.maxNewElements || subScope.maxNewElements<0)) {
+//                      println('''
+//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes
+//                      subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements»
+//                      ''')
+                        subScope.maxNewElements = p.maxNewElements
+                        return true
+                } else {
+                        return false
+                }
+        }
+        private def removeOne(Scope scope) {
+                if(scope.maxNewElements===0) {
+                        throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''')
+                } else if(scope.maxNewElements>0) {
+                        scope.maxNewElements= scope.maxNewElements-1
+                }
+                if(scope.minNewElements>0) {
+                        scope.minNewElements= scope.minNewElements-1
+                }
+        }
+}
+                        
+\ No newline at end of file

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend new file mode 100644 index 00000000..38633c07 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend
@@ -0,0 +1,156 @@
	1	package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra
	2
	3	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
	4	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
	5	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
	6	import java.util.HashMap
	7	import java.util.Map
	8	import java.util.Set
	9	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
	10	import java.util.HashSet
	11
	12	class ScopePropagator {
	13	PartialInterpretation partialInterpretation
	14	Map<PartialTypeInterpratation,Scope> type2Scope
	15
	16	val Map<Scope, Set<Scope>> superScopes
	17	val Map<Scope, Set<Scope>> subScopes
	18
	19	public new(PartialInterpretation p) {
	20	partialInterpretation = p
	21	type2Scope = new HashMap
	22	for(scope : p.scopes) {
	23	type2Scope.put(scope.targetTypeInterpretation,scope)
	24	}
	25
	26	superScopes = new HashMap
	27	subScopes = new HashMap
	28	for(scope : p.scopes) {
	29	superScopes.put(scope,new HashSet)
	30	subScopes.put(scope,new HashSet)
	31	}
	32
	33	for(scope : p.scopes) {
	34	val target = scope.targetTypeInterpretation
	35	if(target instanceof PartialComplexTypeInterpretation) {
	36	val supertypeInterpretations = target.supertypeInterpretation
	37	for(supertypeInterpretation : supertypeInterpretations) {
	38	val supertypeScope = type2Scope.get(supertypeInterpretation)
	39	superScopes.get(scope).add(supertypeScope)
	40	subScopes.get(supertypeScope).add(scope)
	41	}
	42	}
	43	}
	44	}
	45
	46	def public propagateAllScopeConstraints() {
	47	var boolean hadChanged
	48	do{
	49	hadChanged = false
	50	for(superScopeEntry : superScopes.entrySet) {
	51	val sub = superScopeEntry.key
	52	hadChanged = propagateLowerLimitUp(sub,partialInterpretation) \|\| hadChanged
	53	hadChanged = propagateUpperLimitDown(sub,partialInterpretation) \|\| hadChanged
	54	for(sup: superScopeEntry.value) {
	55	hadChanged = propagateLowerLimitUp(sub,sup) \|\| hadChanged
	56	hadChanged = propagateUpperLimitDown(sub,sup) \|\| hadChanged
	57	}
	58	}
	59	} while(hadChanged)
	60	// println('''All constraints are propagated.''')
	61	}
	62
	63	def public propagateAdditionToType(PartialTypeInterpratation t) {
	64	// println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
	65	val targetScope = type2Scope.get(t)
	66	targetScope.removeOne
	67	val sups = superScopes.get(targetScope)
	68	sups.forEach[removeOne]
	69	if(this.partialInterpretation.minNewElements > 0) {
	70	this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1
	71	}
	72	if(this.partialInterpretation.maxNewElements > 0) {
	73	this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1
	74	} else if(this.partialInterpretation.maxNewElements === 0) {
	75	throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''')
	76	}
	77
	78	// subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)]
	79	// for(sup: sups) {
	80	// subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)]
	81	// }
	82	// for(scope : type2Scope.values) {
	83	// propagateUpperLimitDown(scope,partialInterpretation)
	84	// }
	85
	86	propagateAllScopeConstraints
	87
	88	// println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''')
	89	// println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''')
	90	// this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')]
	91	// println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
	92	}
	93
	94	private def propagateLowerLimitUp(Scope subScope, Scope superScope) {
	95	if(subScope.minNewElements>superScope.minNewElements) {
	96	// println('''
	97	// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»
	98	// superScope.minNewElements «superScope.minNewElements» = subScope.minNewElements «subScope.minNewElements»
	99	// ''')
	100	superScope.minNewElements = subScope.minNewElements
	101	return true
	102	} else {
	103	return false
	104	}
	105	}
	106
	107	private def propagateUpperLimitDown(Scope subScope, Scope superScope) {
	108	if(superScope.maxNewElements>=0 && (superScope.maxNewElements<subScope.maxNewElements \|\| subScope.maxNewElements<0)) {
	109	// println('''
	110	// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»
	111	// subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements»
	112	// ''')
	113	subScope.maxNewElements = superScope.maxNewElements
	114	return true
	115	} else {
	116	return false
	117	}
	118	}
	119
	120	private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) {
	121	if(subScope.minNewElements>p.minNewElements) {
	122	// println('''
	123	// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes
	124	// p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements»
	125	// ''')
	126	p.minNewElements = subScope.minNewElements
	127	return true
	128	} else {
	129	return false
	130	}
	131	}
	132
	133	private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) {
	134	if(p.maxNewElements>=0 && (p.maxNewElements<subScope.maxNewElements \|\| subScope.maxNewElements<0)) {
	135	// println('''
	136	// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes
	137	// subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements»
	138	// ''')
	139	subScope.maxNewElements = p.maxNewElements
	140	return true
	141	} else {
	142	return false
	143	}
	144	}
	145	private def removeOne(Scope scope) {
	146	if(scope.maxNewElements===0) {
	147	throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''')
	148	} else if(scope.maxNewElements>0) {
	149	scope.maxNewElements= scope.maxNewElements-1
	150	}
	151	if(scope.minNewElements>0) {
	152	scope.minNewElements= scope.minNewElements-1
	153	}
	154	}
	155	}
	156	\ No newline at end of file