1 files changed, 146 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend
new file mode 100644
index 00000000..39d8a365
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend
@@ -0,0 +1,146 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.HashSet
+import java.util.Map
+import java.util.Set
+import org.eclipse.xtend.lib.annotations.Data
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+@Data class PartialInterpretation2Logic_Trace {
+        Map<TypeDeclaration, TypeDefinition> definedPart = new HashMap
+        Map<TypeDeclaration, TypeDeclaration> undefinedPart = new HashMap
+        Set<Type> originalTypes = new HashSet
+        Set<TypeDeclaration> splittedTypes = new HashSet
+}
+class PartialInterpretation2Logic {
+        val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        val extension LogicProblemBuilder builder = new LogicProblemBuilder
+        
+        def transformPartialIntepretation2Logic(LogicProblem p, PartialInterpretation i) {
+                val trace = new PartialInterpretation2Logic_Trace()
+                trace.originalTypes.addAll(p.types)
+                if(! i.newElements.empty) {
+                        
+                        // Elements adding
+                        addExistingElementToProblem(p,i)
+                        
+                        // Types
+                        for(partialTypeDeclaration : i.partialtypeinterpratation) {
+                                splitTypeIntoTwo(p,partialTypeDeclaration,trace)
+                        }
+                        connectSplittings(p,trace)
+                        
+                        // Relations
+                        for(partialRelationInterpretation : i.partialrelationinterpretation) {
+                                relationLinksToAssertion(p,partialRelationInterpretation,trace)
+                        }
+                }
+        }
+        
+        private def addExistingElementToProblem(LogicProblem p, PartialInterpretation i) {
+                val newElements = new ArrayList(i.newElements)
+                var newElementIndex = 1
+                for(newElement : newElements) {
+                        newElement.name = '''DefinedElement «newElementIndex++»'''
+                        p.elements += newElement
+                }
+        }
+        
+        private def splitTypeIntoTwo(LogicProblem p, PartialTypeInterpratation partialTypeDeclaration,PartialInterpretation2Logic_Trace trace) {
+                if(!partialTypeDeclaration.elements.empty) {
+                        val declaration = partialTypeDeclaration.interpretationOf
+                        
+                        val definedPart = createTypeDefinition => [
+                                it.name = '''DefinedPartOf «declaration.name»'''
+                                it.elements += partialTypeDeclaration.elements
+                                it.isAbstract = declaration.isIsAbstract
+                        ]
+                        val undefinedPart = createTypeDeclaration => [
+                                it.name = '''UndefinedPartOf «declaration.name»'''
+                                it.isAbstract = declaration.isIsAbstract
+                        ]
+                        declaration.isAbstract = true
+                        
+                        trace.definedPart.put(declaration,definedPart)
+                        trace.undefinedPart.put(declaration,undefinedPart)
+                        trace.splittedTypes.add(declaration)
+                        p.add(definedPart)
+                        p.add(undefinedPart)
+                        Supertype(definedPart,declaration)
+                        Supertype(undefinedPart,declaration)
+                }
+        }
+        
+        private def connectSplittings(LogicProblem p,PartialInterpretation2Logic_Trace trace)  {
+                val originalTypes = p.types.filter[originalType(trace)].toList
+                for(type : originalTypes) {
+                        val superTypes = new ArrayList(type.supertypes.filter[originalType(trace)].toList)
+                        for(supertype : superTypes) {
+                                if(type.isSplitted(trace)) {
+                                        if(supertype.isSplitted(trace)) {
+                                                Supertype((type as TypeDeclaration).lookup(trace.definedPart), (supertype as TypeDeclaration).lookup(trace.definedPart))
+                                                Supertype((type as TypeDeclaration).lookup(trace.undefinedPart), (supertype as TypeDeclaration).lookup(trace.undefinedPart))
+                                        } else {
+                                                // Do nothing
+                                        }
+                                } else {
+                                        if(supertype.isSplitted(trace)) {
+                                                Supertype(type, (supertype as TypeDeclaration).lookup(trace.undefinedPart))
+                                        } else if(supertype instanceof TypeDefinition) {
+                                                // Do nothing
+                                        }
+                                }
+                        }
+                }
+        }
+        
+        private def originalType(Type type,PartialInterpretation2Logic_Trace trace) {
+                return trace.originalTypes.contains(type)
+        }
+        private def isSplitted(Type t, PartialInterpretation2Logic_Trace trace) {
+                trace.splittedTypes.contains(t)
+        }
+        
+        private def relationLinksToAssertion(LogicProblem p, PartialRelationInterpretation r,PartialInterpretation2Logic_Trace trace) {
+                val relation = r.interpretationOf
+                val links = r.relationlinks
+                if(links.size == 0) {
+                        return
+                } else {
+                        val term = if(links.size == 1) {
+                                createLink(links.head,relation)
+                        } else {
+                                links.map[link|createLink(link,relation)].And
+                        }
+                        val assertion = Assertion('''PartialInterpretation «r.interpretationOf.name»''',term)
+                        p.add(assertion)
+                }
+                
+        }
+        
+        def private createLink(RelationLink link, SymbolicDeclaration relationDeclaration) {
+                if(link instanceof BinaryElementRelationLink) {
+                        return createSymbolicValue=>[
+                                it.symbolicReference=relationDeclaration
+                                it.parameterSubstitutions += createSymbolicValue => [link.param1]
+                                it.parameterSubstitutions += createSymbolicValue => [link.param2]
+                        ]
+                } else throw new UnsupportedOperationException
+        }
+}
+\ No newline at end of file

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend new file mode 100644 index 00000000..39d8a365 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend
@@ -0,0 +1,146 @@
	1	package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic
	2
	3	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
	4	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
	5	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration
	6	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
	7	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
	8	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
	9	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
	10	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
	11	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
	12	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
	13	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
	14	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink
	15	import java.util.ArrayList
	16	import java.util.HashMap
	17	import java.util.HashSet
	18	import java.util.Map
	19	import java.util.Set
	20	import org.eclipse.xtend.lib.annotations.Data
	21
	22	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
	23
	24	@Data class PartialInterpretation2Logic_Trace {
	25	Map<TypeDeclaration, TypeDefinition> definedPart = new HashMap
	26	Map<TypeDeclaration, TypeDeclaration> undefinedPart = new HashMap
	27	Set<Type> originalTypes = new HashSet
	28	Set<TypeDeclaration> splittedTypes = new HashSet
	29	}
	30
	31	class PartialInterpretation2Logic {
	32	val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
	33	val extension LogicProblemBuilder builder = new LogicProblemBuilder
	34
	35	def transformPartialIntepretation2Logic(LogicProblem p, PartialInterpretation i) {
	36	val trace = new PartialInterpretation2Logic_Trace()
	37	trace.originalTypes.addAll(p.types)
	38	if(! i.newElements.empty) {
	39
	40	// Elements adding
	41	addExistingElementToProblem(p,i)
	42
	43	// Types
	44	for(partialTypeDeclaration : i.partialtypeinterpratation) {
	45	splitTypeIntoTwo(p,partialTypeDeclaration,trace)
	46	}
	47	connectSplittings(p,trace)
	48
	49	// Relations
	50	for(partialRelationInterpretation : i.partialrelationinterpretation) {
	51	relationLinksToAssertion(p,partialRelationInterpretation,trace)
	52	}
	53	}
	54	}
	55
	56	private def addExistingElementToProblem(LogicProblem p, PartialInterpretation i) {
	57	val newElements = new ArrayList(i.newElements)
	58	var newElementIndex = 1
	59	for(newElement : newElements) {
	60	newElement.name = '''DefinedElement «newElementIndex++»'''
	61	p.elements += newElement
	62	}
	63	}
	64
	65	private def splitTypeIntoTwo(LogicProblem p, PartialTypeInterpratation partialTypeDeclaration,PartialInterpretation2Logic_Trace trace) {
	66	if(!partialTypeDeclaration.elements.empty) {
	67	val declaration = partialTypeDeclaration.interpretationOf
	68
	69	val definedPart = createTypeDefinition => [
	70	it.name = '''DefinedPartOf «declaration.name»'''
	71	it.elements += partialTypeDeclaration.elements
	72	it.isAbstract = declaration.isIsAbstract
	73	]
	74	val undefinedPart = createTypeDeclaration => [
	75	it.name = '''UndefinedPartOf «declaration.name»'''
	76	it.isAbstract = declaration.isIsAbstract
	77	]
	78	declaration.isAbstract = true
	79
	80	trace.definedPart.put(declaration,definedPart)
	81	trace.undefinedPart.put(declaration,undefinedPart)
	82	trace.splittedTypes.add(declaration)
	83	p.add(definedPart)
	84	p.add(undefinedPart)
	85	Supertype(definedPart,declaration)
	86	Supertype(undefinedPart,declaration)
	87	}
	88	}
	89
	90	private def connectSplittings(LogicProblem p,PartialInterpretation2Logic_Trace trace) {
	91	val originalTypes = p.types.filter[originalType(trace)].toList
	92	for(type : originalTypes) {
	93	val superTypes = new ArrayList(type.supertypes.filter[originalType(trace)].toList)
	94	for(supertype : superTypes) {
	95	if(type.isSplitted(trace)) {
	96	if(supertype.isSplitted(trace)) {
	97	Supertype((type as TypeDeclaration).lookup(trace.definedPart), (supertype as TypeDeclaration).lookup(trace.definedPart))
	98	Supertype((type as TypeDeclaration).lookup(trace.undefinedPart), (supertype as TypeDeclaration).lookup(trace.undefinedPart))
	99	} else {
	100	// Do nothing
	101	}
	102	} else {
	103	if(supertype.isSplitted(trace)) {
	104	Supertype(type, (supertype as TypeDeclaration).lookup(trace.undefinedPart))
	105	} else if(supertype instanceof TypeDefinition) {
	106	// Do nothing
	107	}
	108	}
	109	}
	110	}
	111	}
	112
	113	private def originalType(Type type,PartialInterpretation2Logic_Trace trace) {
	114	return trace.originalTypes.contains(type)
	115	}
	116	private def isSplitted(Type t, PartialInterpretation2Logic_Trace trace) {
	117	trace.splittedTypes.contains(t)
	118	}
	119
	120	private def relationLinksToAssertion(LogicProblem p, PartialRelationInterpretation r,PartialInterpretation2Logic_Trace trace) {
	121	val relation = r.interpretationOf
	122	val links = r.relationlinks
	123	if(links.size == 0) {
	124	return
	125	} else {
	126	val term = if(links.size == 1) {
	127	createLink(links.head,relation)
	128	} else {
	129	links.map[link\|createLink(link,relation)].And
	130	}
	131	val assertion = Assertion('''PartialInterpretation «r.interpretationOf.name»''',term)
	132	p.add(assertion)
	133	}
	134
	135	}
	136
	137	def private createLink(RelationLink link, SymbolicDeclaration relationDeclaration) {
	138	if(link instanceof BinaryElementRelationLink) {
	139	return createSymbolicValue=>[
	140	it.symbolicReference=relationDeclaration
	141	it.parameterSubstitutions += createSymbolicValue => [link.param1]
	142	it.parameterSubstitutions += createSymbolicValue => [link.param2]
	143	]
	144	} else throw new UnsupportedOperationException
	145	}
	146	} \ No newline at end of file