Polyhedron abstraction with Z3 for cardinality propagation

author: Kristóf Marussy <kris7topher@gmail.com> 2019-07-14 00:56:19 +0200
committer: Kristóf Marussy <kris7topher@gmail.com> 2019-07-14 00:56:19 +0200
commit: fc505b6b171a2d54c3bad6078031b028b55131d3 (patch)
tree: 8eaa033e053e21ca60bd7f958055cc46e93b7cba /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
parent: Try fix statecode bug (diff)
download: VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.tar.gz
VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.tar.zst
VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.zip
1 files changed, 149 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..c8fb3409
--- /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,149 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+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
+enum ScopePropagatorStrategy {
+        BasicTypeHierarchy,
+        PolyhedralTypeHierarchy
+}
+class ScopePropagator {
+        @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation
+        Map<PartialTypeInterpratation, Scope> type2Scope
+        val Map<Scope, Set<Scope>> superScopes
+        val Map<Scope, Set<Scope>> subScopes
+        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 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)
+        }
+        def 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!''')
+                }
+                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) {
+                        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
+                }
+        }
+}
author	Kristóf Marussy <kris7topher@gmail.com>	2019-07-14 00:56:19 +0200
committer	Kristóf Marussy <kris7topher@gmail.com>	2019-07-14 00:56:19 +0200
commit	fc505b6b171a2d54c3bad6078031b028b55131d3 (patch)
tree	8eaa033e053e21ca60bd7f958055cc46e93b7cba /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
parent	Try fix statecode bug (diff)
download	VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.tar.gz VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.tar.zst VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.zip

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