1 files changed, 159 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..d1b29f01
--- /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,159 @@
+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)
+                if(targetScope != null){
+                        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..d1b29f01 --- /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,159 @@
	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	if(targetScope != null){
	67	targetScope.removeOne
	68	val sups = superScopes.get(targetScope)
	69	sups.forEach[removeOne]
	70	}
	71
	72	if(this.partialInterpretation.minNewElements > 0) {
	73	this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1
	74	}
	75	if(this.partialInterpretation.maxNewElements > 0) {
	76	this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1
	77	} else if(this.partialInterpretation.maxNewElements === 0) {
	78	throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''')
	79	}
	80
	81	// subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)]
	82	// for(sup: sups) {
	83	// subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)]
	84	// }
	85	// for(scope : type2Scope.values) {
	86	// propagateUpperLimitDown(scope,partialInterpretation)
	87	// }
	88
	89	propagateAllScopeConstraints
	90
	91	// println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''')
	92	// println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''')
	93	// this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')]
	94	// println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
	95	}
	96
	97	private def propagateLowerLimitUp(Scope subScope, Scope superScope) {
	98	if(subScope.minNewElements>superScope.minNewElements) {
	99	// println('''
	100	// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»
	101	// superScope.minNewElements «superScope.minNewElements» = subScope.minNewElements «subScope.minNewElements»
	102	// ''')
	103	superScope.minNewElements = subScope.minNewElements
	104	return true
	105	} else {
	106	return false
	107	}
	108	}
	109
	110	private def propagateUpperLimitDown(Scope subScope, Scope superScope) {
	111	if(superScope.maxNewElements>=0 && (superScope.maxNewElements<subScope.maxNewElements \|\| subScope.maxNewElements<0)) {
	112	// println('''
	113	// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»
	114	// subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements»
	115	// ''')
	116	subScope.maxNewElements = superScope.maxNewElements
	117	return true
	118	} else {
	119	return false
	120	}
	121	}
	122
	123	private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) {
	124	if(subScope.minNewElements>p.minNewElements) {
	125	// println('''
	126	// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes
	127	// p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements»
	128	// ''')
	129	p.minNewElements = subScope.minNewElements
	130	return true
	131	} else {
	132	return false
	133	}
	134	}
	135
	136	private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) {
	137	if(p.maxNewElements>=0 && (p.maxNewElements<subScope.maxNewElements \|\| subScope.maxNewElements<0)) {
	138	// println('''
	139	// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes
	140	// subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements»
	141	// ''')
	142	subScope.maxNewElements = p.maxNewElements
	143	return true
	144	} else {
	145	return false
	146	}
	147	}
	148	private def removeOne(Scope scope) {
	149	if(scope.maxNewElements===0) {
	150	throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''')
	151	} else if(scope.maxNewElements>0) {
	152	scope.maxNewElements= scope.maxNewElements-1
	153	}
	154	if(scope.minNewElements>0) {
	155	scope.minNewElements= scope.minNewElements-1
	156	}
	157	}
	158	}
	159	\ No newline at end of file