1 files changed, 134 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
new file mode 100644
index 00000000..8f3a5bb0
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
@@ -0,0 +1,134 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
+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.HashSet
+import java.util.Map
+import java.util.Set
+import org.eclipse.xtend.lib.annotations.Accessors
+class ScopePropagator {
+        @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation
+        @Accessors(PROTECTED_GETTER) val ModelGenerationStatistics statistics
+        val Map<PartialTypeInterpratation, Scope> type2Scope
+        @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes
+        @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes
+        new(PartialInterpretation p, ModelGenerationStatistics statistics) {
+                partialInterpretation = p
+                this.statistics = statistics
+                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)
+                                }
+                        }
+                }
+                var boolean changed
+                do {
+                        changed = false
+                        for (scope : p.scopes) {
+                                val subScopeSet = subScopes.get(scope)
+                                val superScopeSet = superScopes.get(scope)
+                                for (subScope : subScopeSet) {
+                                        changed = changed || superScopes.get(subScope).addAll(superScopeSet)
+                                }
+                                for (superScope : superScopeSet) {
+                                        changed = changed || subScopes.get(superScope).addAll(subScopeSet)
+                                }
+                        }
+                } while (changed)
+                
+                copyScopeBoundsToHeuristic()
+        }
+        def propagateAllScopeConstraints() {
+                statistics.incrementScopePropagationCount()
+                doPropagateAllScopeConstraints()
+        }
+        
+        protected def copyScopeBoundsToHeuristic() {
+                partialInterpretation.minNewElementsHeuristic = partialInterpretation.minNewElements
+                for (scope : partialInterpretation.scopes) {
+                        scope.minNewElementsHeuristic = scope.minNewElements
+                }
+        }
+        protected def void doPropagateAllScopeConstraints() {
+                // Nothing to propagate.
+        }
+        def decrementTypeScope(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.minNewElementsHeuristic > 0) {
+                        this.partialInterpretation.minNewElementsHeuristic = this.partialInterpretation.minNewElementsHeuristic - 1
+                }
+                if (this.partialInterpretation.maxNewElements > 0) {
+                        this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1
+                } else if (this.partialInterpretation.maxNewElements === 0) {
+                        setScopesInvalid()
+                }
+//              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»''')
+        }
+        
+        protected def setScopesInvalid() {
+                partialInterpretation.minNewElements = Integer.MAX_VALUE
+                partialInterpretation.maxNewElements = 0
+                for (scope : partialInterpretation.scopes) {
+                        scope.minNewElements = Integer.MAX_VALUE
+                        scope.maxNewElements = 0
+                }
+        }
+        def void propagateAdditionToRelation(Relation r) {
+                // Nothing to propagate.
+        }
+        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
+                }
+                if (scope.minNewElementsHeuristic > 0) {
+                        scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1
+                }
+        }
+}

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend new file mode 100644 index 00000000..8f3a5bb0 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
@@ -0,0 +1,134 @@
	1	package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
	2
	3	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
	4	import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
	5	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
	6	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
	7	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
	8	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
	9	import java.util.HashMap
	10	import java.util.HashSet
	11	import java.util.Map
	12	import java.util.Set
	13	import org.eclipse.xtend.lib.annotations.Accessors
	14
	15	class ScopePropagator {
	16	@Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation
	17	@Accessors(PROTECTED_GETTER) val ModelGenerationStatistics statistics
	18	val Map<PartialTypeInterpratation, Scope> type2Scope
	19	@Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes
	20	@Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes
	21
	22	new(PartialInterpretation p, ModelGenerationStatistics statistics) {
	23	partialInterpretation = p
	24	this.statistics = statistics
	25	type2Scope = new HashMap
	26	for (scope : p.scopes) {
	27	type2Scope.put(scope.targetTypeInterpretation, scope)
	28	}
	29
	30	superScopes = new HashMap
	31	subScopes = new HashMap
	32	for (scope : p.scopes) {
	33	superScopes.put(scope, new HashSet)
	34	subScopes.put(scope, new HashSet)
	35	}
	36
	37	for (scope : p.scopes) {
	38	val target = scope.targetTypeInterpretation
	39	if (target instanceof PartialComplexTypeInterpretation) {
	40	val supertypeInterpretations = target.supertypeInterpretation
	41	for (supertypeInterpretation : supertypeInterpretations) {
	42	val supertypeScope = type2Scope.get(supertypeInterpretation)
	43	superScopes.get(scope).add(supertypeScope)
	44	subScopes.get(supertypeScope).add(scope)
	45	}
	46	}
	47	}
	48	var boolean changed
	49	do {
	50	changed = false
	51	for (scope : p.scopes) {
	52	val subScopeSet = subScopes.get(scope)
	53	val superScopeSet = superScopes.get(scope)
	54	for (subScope : subScopeSet) {
	55	changed = changed \|\| superScopes.get(subScope).addAll(superScopeSet)
	56	}
	57	for (superScope : superScopeSet) {
	58	changed = changed \|\| subScopes.get(superScope).addAll(subScopeSet)
	59	}
	60	}
	61	} while (changed)
	62
	63	copyScopeBoundsToHeuristic()
	64	}
	65
	66	def propagateAllScopeConstraints() {
	67	statistics.incrementScopePropagationCount()
	68	doPropagateAllScopeConstraints()
	69	}
	70
	71	protected def copyScopeBoundsToHeuristic() {
	72	partialInterpretation.minNewElementsHeuristic = partialInterpretation.minNewElements
	73	for (scope : partialInterpretation.scopes) {
	74	scope.minNewElementsHeuristic = scope.minNewElements
	75	}
	76	}
	77
	78	protected def void doPropagateAllScopeConstraints() {
	79	// Nothing to propagate.
	80	}
	81
	82	def decrementTypeScope(PartialTypeInterpratation t) {
	83	// println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
	84	val targetScope = type2Scope.get(t)
	85	if (targetScope !== null) {
	86	targetScope.removeOne
	87	val sups = superScopes.get(targetScope)
	88	sups.forEach[removeOne]
	89	}
	90	if (this.partialInterpretation.minNewElements > 0) {
	91	this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1
	92	}
	93	if (this.partialInterpretation.minNewElementsHeuristic > 0) {
	94	this.partialInterpretation.minNewElementsHeuristic = this.partialInterpretation.minNewElementsHeuristic - 1
	95	}
	96	if (this.partialInterpretation.maxNewElements > 0) {
	97	this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1
	98	} else if (this.partialInterpretation.maxNewElements === 0) {
	99	setScopesInvalid()
	100	}
	101
	102	// println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''')
	103	// println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''')
	104	// this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')]
	105	// println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
	106	}
	107
	108	protected def setScopesInvalid() {
	109	partialInterpretation.minNewElements = Integer.MAX_VALUE
	110	partialInterpretation.maxNewElements = 0
	111	for (scope : partialInterpretation.scopes) {
	112	scope.minNewElements = Integer.MAX_VALUE
	113	scope.maxNewElements = 0
	114	}
	115	}
	116
	117	def void propagateAdditionToRelation(Relation r) {
	118	// Nothing to propagate.
	119	}
	120
	121	private def removeOne(Scope scope) {
	122	if (scope.maxNewElements === 0) {
	123	throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''')
	124	} else if (scope.maxNewElements > 0) {
	125	scope.maxNewElements = scope.maxNewElements - 1
	126	}
	127	if (scope.minNewElements > 0) {
	128	scope.minNewElements = scope.minNewElements - 1
	129	}
	130	if (scope.minNewElementsHeuristic > 0) {
	131	scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1
	132	}
	133	}
	134	}