1 files changed, 133 insertions, 0 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.ecore2logic/src/hu/bme/mit/inf/dslreasoner/ecore2logic/ContainmentMapper.xtend b/Framework/hu.bme.mit.inf.dslreasoner.ecore2logic/src/hu/bme/mit/inf/dslreasoner/ecore2logic/ContainmentMapper.xtend
new file mode 100644
index 00000000..492be59f
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.ecore2logic/src/hu/bme/mit/inf/dslreasoner/ecore2logic/ContainmentMapper.xtend
@@ -0,0 +1,133 @@
+package hu.bme.mit.inf.dslreasoner.ecore2logic
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import org.eclipse.emf.ecore.EReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
+interface ContainmentMapper {
+        def  void transformContainment(Ecore2Logic_Trace trace, LogicProblem problem, Iterable<EReference> references, boolean singleRoot);
+}
+class ContainmentMapper_ReferenceConjuction_Trace implements Trace<ContainmentMapper_ReferenceConjuction> {
+        public var Constant root;
+        public var Relation contains
+        public var Assertion containsDefinition;
+        public var Assertion rootIsNotContained;
+        public var Assertion everithingElseContained;
+        public var Assertion notContainedByMore;
+}
+class ContainmentMapper_ReferenceConjuction implements ContainmentMapper{
+        val extension LogicProblemBuilder builder = new LogicProblemBuilder
+        val extension EClassMapper classMapper;
+        val extension EReferenceMapper referenceMapper
+        val int containmentAcyclicityApproximationLevel;
+        
+        public new(EClassMapper classMapper, EReferenceMapper referenceMapper, int containmentAcyclicityApproximationLevel) {
+                this.classMapper = classMapper
+                this.referenceMapper = referenceMapper
+                this.containmentAcyclicityApproximationLevel = containmentAcyclicityApproximationLevel
+        }
+        
+        override transformContainment(Ecore2Logic_Trace trace, LogicProblem problem, Iterable<EReference> references, boolean singleRoot) {
+                val allClasses = classMapper.allClassesInScope(trace).map[classMapper.TypeofEClass(trace,it)]
+                val containmentRelation = references.filter[isContainment].map[referenceMapper.relationOfReference(trace,it)]
+                val containmentHierarchy = ContainmentHierarchy(allClasses,#[],containmentRelation,null)
+                problem.add(containmentHierarchy)
+        }
+}
+/*val containmentMapperTrace = new ContainmentMapper_ReferenceConjuction_Trace
+                        trace.containmentMapperTrace = containmentMapperTrace
+                        
+                        val containment = references.filter[containment]
+                                                
+                        val contains = problem.add(RelationDeclaration('''contains''', getType(trace,references),getType(trace,references)))
+                        containmentMapperTrace.contains = contains
+                        containmentMapperTrace.containsDefinition = problem.add(Assertion('''containsDefinition''',
+                                Forall[
+                                        val parent = addVar("parent",getType(trace,references))
+                                        val child = addVar("child",getType(trace,references))
+                                        contains.call(parent,child) <=> Or(containment.map[IsInReference(trace,parent,child,it)])
+                                ]
+                        ))
+                        
+                        
+                        
+                        containmentMapperTrace.notContainedByMore = problem.add(Assertion('''notContainedByMore''',
+                                Forall[
+                                        val child = addVar('''child''',getType(trace,references))
+                                        val parent1 = addVar('''parent 1''',getType(trace,references))
+                                        val parent2 = addVar('''parent 2''',getType(trace,references))
+                                        (contains.call(parent1,child) && contains.call(parent2,child)) => (parent1 == parent2)
+                                ]
+                        ))
+                        (2..containmentAcyclicityApproximationLevel).forEach[problem.add(getAcyclicityConstraint(trace,references,it))]
+                        
+                        if (singleRoot) {
+                                val root = problem.add(ConstantDeclaration('''root''', getType(trace, references)))
+                                containmentMapperTrace.root = root
+        
+                                containmentMapperTrace.rootIsNotContained = problem.add(
+                                        Assertion(
+                                                '''rootIsNotContained''',
+                                                Forall[
+                                                        val parent = addVar("parent", getType(trace, references))
+                                                        !contains.call(parent, root)
+                                                ]
+                                        ))
+        
+                                containmentMapperTrace.everithingElseContained = problem.add(
+                                        Assertion(
+                                                '''nonrootIsContained''',
+                                                Forall[
+                                                        val child = addVar("child", getType(trace, references))
+                                                        (child != root) => Exists[
+                                                                val parent = addVar("parent", getType(trace, references))
+                                                                contains.call(parent, child)
+                                                        ]
+                                                ]
+                                        ))
+                        }*/
+                        
+        
+//      def asTrace(Trace<? extends ContainmentMapper> trace) { trace as ContainmentMapper_ReferenceConjuction_Trace }
+//      
+//      def getAcyclicityConstraint(Ecore2Logic_Trace trace, Iterable<EReference> references,int circleSize) {
+//              val newTrace = trace.containmentMapperTrace.asTrace
+//              //val newTrace2 = trace.containmentMapperTrace as ContainmentMapper_ReferenceConjuction_Trace // ???
+//              
+//              Forall[context | 
+//                      val elements = (0..circleSize).map[context.addVar(getType(trace,references))].toList
+//                      !(And((0..circleSize-1).map[newTrace.contains.call(elements.get(it),elements.get(it+1))]) &&
+//                        newTrace.contains.call(elements.last,elements.head))
+//              ]
+//      }
+//      
+//      def private getType(Ecore2Logic_Trace trace, Iterable<EReference> references) {
+//              trace.TypeofEClass(references.head.EContainingClass)
+//      }
+        /*// This type is contained -> (From this type -> By those references)
+                        val Map<TypeDescriptor,Map<TypeDescriptor,Set<EReference>>> typeContainedBy = new HashMap
+                        for(reference: references.filter[containment]) {
+                                val sourceType = TypeofEClass(classMapperTrace, reference.EContainingClass)
+                                val targetType = TypeofEClass(classMapperTrace, reference.EType as EClass)
+                                if(typeContainedBy.containsKey(targetType)) {
+                                        val m = typeContainedBy.get(targetType)
+                                        if(m.containsKey(sourceType)) {
+                                                m.get(sourceType).add(reference)
+                                        } else {
+                                                m.put(sourceType,new HashSet => [add(reference)])
+                                        }
+                                } else { // initialise the collection
+                                        val Map<TypeDescriptor,Set<EReference>> m = new HashMap
+                                        m.put(sourceType,new HashSet => [add(reference)])
+                                        typeContainedBy.put(targetType,m)
+                                }
+                        }*/
+                        // Only one type
+\ No newline at end of file

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.ecore2logic/src/hu/bme/mit/inf/dslreasoner/ecore2logic/ContainmentMapper.xtend b/Framework/hu.bme.mit.inf.dslreasoner.ecore2logic/src/hu/bme/mit/inf/dslreasoner/ecore2logic/ContainmentMapper.xtend new file mode 100644 index 00000000..492be59f --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.ecore2logic/src/hu/bme/mit/inf/dslreasoner/ecore2logic/ContainmentMapper.xtend
@@ -0,0 +1,133 @@
	1	package hu.bme.mit.inf.dslreasoner.ecore2logic
	2
	3	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
	4	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
	5	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
	6	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
	7	import org.eclipse.emf.ecore.EReference
	8	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
	9
	10	interface ContainmentMapper {
	11	def void transformContainment(Ecore2Logic_Trace trace, LogicProblem problem, Iterable<EReference> references, boolean singleRoot);
	12	}
	13
	14	class ContainmentMapper_ReferenceConjuction_Trace implements Trace<ContainmentMapper_ReferenceConjuction> {
	15	public var Constant root;
	16	public var Relation contains
	17	public var Assertion containsDefinition;
	18	public var Assertion rootIsNotContained;
	19	public var Assertion everithingElseContained;
	20	public var Assertion notContainedByMore;
	21	}
	22
	23	class ContainmentMapper_ReferenceConjuction implements ContainmentMapper{
	24	val extension LogicProblemBuilder builder = new LogicProblemBuilder
	25	val extension EClassMapper classMapper;
	26	val extension EReferenceMapper referenceMapper
	27	val int containmentAcyclicityApproximationLevel;
	28
	29	public new(EClassMapper classMapper, EReferenceMapper referenceMapper, int containmentAcyclicityApproximationLevel) {
	30	this.classMapper = classMapper
	31	this.referenceMapper = referenceMapper
	32	this.containmentAcyclicityApproximationLevel = containmentAcyclicityApproximationLevel
	33	}
	34
	35	override transformContainment(Ecore2Logic_Trace trace, LogicProblem problem, Iterable<EReference> references, boolean singleRoot) {
	36	val allClasses = classMapper.allClassesInScope(trace).map[classMapper.TypeofEClass(trace,it)]
	37	val containmentRelation = references.filter[isContainment].map[referenceMapper.relationOfReference(trace,it)]
	38	val containmentHierarchy = ContainmentHierarchy(allClasses,#[],containmentRelation,null)
	39	problem.add(containmentHierarchy)
	40	}
	41	}
	42
	43	/*val containmentMapperTrace = new ContainmentMapper_ReferenceConjuction_Trace
	44	trace.containmentMapperTrace = containmentMapperTrace
	45
	46	val containment = references.filter[containment]
	47
	48	val contains = problem.add(RelationDeclaration('''contains''', getType(trace,references),getType(trace,references)))
	49	containmentMapperTrace.contains = contains
	50	containmentMapperTrace.containsDefinition = problem.add(Assertion('''containsDefinition''',
	51	Forall[
	52	val parent = addVar("parent",getType(trace,references))
	53	val child = addVar("child",getType(trace,references))
	54	contains.call(parent,child) <=> Or(containment.map[IsInReference(trace,parent,child,it)])
	55	]
	56	))
	57
	58
	59
	60	containmentMapperTrace.notContainedByMore = problem.add(Assertion('''notContainedByMore''',
	61	Forall[
	62	val child = addVar('''child''',getType(trace,references))
	63	val parent1 = addVar('''parent 1''',getType(trace,references))
	64	val parent2 = addVar('''parent 2''',getType(trace,references))
	65	(contains.call(parent1,child) && contains.call(parent2,child)) => (parent1 == parent2)
	66	]
	67	))
	68
	69	(2..containmentAcyclicityApproximationLevel).forEach[problem.add(getAcyclicityConstraint(trace,references,it))]
	70
	71	if (singleRoot) {
	72	val root = problem.add(ConstantDeclaration('''root''', getType(trace, references)))
	73	containmentMapperTrace.root = root
	74
	75	containmentMapperTrace.rootIsNotContained = problem.add(
	76	Assertion(
	77	'''rootIsNotContained''',
	78	Forall[
	79	val parent = addVar("parent", getType(trace, references))
	80	!contains.call(parent, root)
	81	]
	82	))
	83
	84	containmentMapperTrace.everithingElseContained = problem.add(
	85	Assertion(
	86	'''nonrootIsContained''',
	87	Forall[
	88	val child = addVar("child", getType(trace, references))
	89	(child != root) => Exists[
	90	val parent = addVar("parent", getType(trace, references))
	91	contains.call(parent, child)
	92	]
	93	]
	94	))
	95	}*/
	96
	97
	98	// def asTrace(Trace<? extends ContainmentMapper> trace) { trace as ContainmentMapper_ReferenceConjuction_Trace }
	99	//
	100	// def getAcyclicityConstraint(Ecore2Logic_Trace trace, Iterable<EReference> references,int circleSize) {
	101	// val newTrace = trace.containmentMapperTrace.asTrace
	102	// //val newTrace2 = trace.containmentMapperTrace as ContainmentMapper_ReferenceConjuction_Trace // ???
	103	//
	104	// Forall[context \|
	105	// val elements = (0..circleSize).map[context.addVar(getType(trace,references))].toList
	106	// !(And((0..circleSize-1).map[newTrace.contains.call(elements.get(it),elements.get(it+1))]) &&
	107	// newTrace.contains.call(elements.last,elements.head))
	108	// ]
	109	// }
	110	//
	111	// def private getType(Ecore2Logic_Trace trace, Iterable<EReference> references) {
	112	// trace.TypeofEClass(references.head.EContainingClass)
	113	// }
	114
	115	/*// This type is contained -> (From this type -> By those references)
	116	val Map<TypeDescriptor,Map<TypeDescriptor,Set<EReference>>> typeContainedBy = new HashMap
	117	for(reference: references.filter[containment]) {
	118	val sourceType = TypeofEClass(classMapperTrace, reference.EContainingClass)
	119	val targetType = TypeofEClass(classMapperTrace, reference.EType as EClass)
	120	if(typeContainedBy.containsKey(targetType)) {
	121	val m = typeContainedBy.get(targetType)
	122	if(m.containsKey(sourceType)) {
	123	m.get(sourceType).add(reference)
	124	} else {
	125	m.put(sourceType,new HashSet => [add(reference)])
	126	}
	127	} else { // initialise the collection
	128	val Map<TypeDescriptor,Set<EReference>> m = new HashMap
	129	m.put(sourceType,new HashSet => [add(reference)])
	130	typeContainedBy.put(targetType,m)
	131	}
	132	}*/
	133	// Only one type \ No newline at end of file