1 files changed, 303 insertions, 12 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend
index aad43716..ec1502e5 100644
--- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend
@@ -1,5 +1,6 @@
 package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
@@ -42,13 +43,17 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr
@@ -60,6 +65,7 @@ import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType
 import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
+import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil
 import java.util.ArrayList
 import java.util.HashMap
 import java.util.LinkedHashMap
@@ -72,18 +78,14 @@ import org.eclipse.xtend.lib.annotations.Accessors
 import org.eclipse.xtext.xbase.lib.Functions.Function0
 import org.eclipse.xtext.xbase.lib.Functions.Function1
 import org.eclipse.xtext.xbase.lib.Functions.Function2
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
-import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
 class Logic2SmtMapper{
        val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
        val Logic2SmtMapper_UnfoldingSupport unfolder = new Logic2SmtMapper_UnfoldingSupport
        @Accessors val Logic2Smt_TypeMapper typeMapper;
        
-        LogicProblemBuilder b
-        
        new(Logic2Smt_TypeMapper typeMapper) {
                this.typeMapper = typeMapper
        }
@@ -109,11 +111,16 @@ class Logic2SmtMapper{
                
                problem.relations.filter(RelationDefinition).forEach[it.transformRelationDefinition_definition(documentInput,trace)]
                documentInput.assertions += problem.assertions.map[transformAssertion(trace)]
+                
+                if(!problem.containmentHierarchies.empty) {
+                        transformContainmentV1(documentInput,problem.containmentHierarchies.head,trace)
+                }
                // End trafo
                
                document.input.assertions.forEach[it.value.nameAllUnnamedVariable]
                document.input.functionDefinition.forEach[it.value.nameAllUnnamedVariable]
                document.cleanDocument
+                document.orderDefinitions
                return new TracedOutput(document,trace)
        }
        
@@ -1000,15 +1007,269 @@ class Logic2SmtMapper{
        
        ///////////
        
-        /*def transformContainment(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) {
+        def transformContainmentV1(SMTInput document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) {
-                val containmentRelation_oo = createSMTFunctionDefinition=>[
+                val extension builder = new LogicProblemBuilder
-                        it.name="containment!oo"
+                val types = h.typesOrderedInHierarchy
-                        it.range=createSMTBoolTypeReference
+                
-                        val child = createSMTSortedVariable => [
+                val rootRelations = new HashMap<Type,Relation>
-                                it.name = 
+                for(type: types) {
+                        val rootRelation = RelationDeclaration('''Root «type.name»''',type)
+                        rootRelations.put(type,rootRelation)
+                        this.transformRelationDeclaration(rootRelation,document,trace)
+                }
+                val possibleParentRelations = types.toInvertedMap[type|
+                        h.containmentRelations.filter[it.parameters.get(1) === type]
+                        //TODO inheritance
+                ]
+                
+                // root is true only for at most one element in every root type
+                for(root: rootRelations.entrySet) {
+                        val a1 = Assertion(Forall[
+                                val r1 = addVar(root.key)
+                                val r2 = addVar(root.key)
+                                (root.value.call(r1) && root.value.call(r2)) => (r1 == r2)
+                        ])
+                        document.assertions+=this.transformAssertion(a1,trace)
+                }
+                // only one of the root entries is true
+//              val a2 = Assertion(
+//                      rootRelations.entrySet.map[selected|
+//                              rootRelations.entrySet.map[other|
+//                                      if(selected == other) {
+//                                              Exists[
+//                                                      val r = addVar(other.key)
+//                                                      other.value.call(r)
+//                                              ]
+//                                      } else {
+//                                              Forall[
+//                                                      val r = addVar(other.key)
+//                                                      !other.value.call(r)
+//                                              ]
+//                                      }
+//                              ].And
+//                      ].Or
+//              )
+//              document.assertions+=this.transformAssertion(a2,trace)
+//              // the root has no parent
+//              for(root : rootRelations.entrySet) {
+//                      val parentRelations = root.key.lookup(possibleParentRelations)
+//                      val a3 = Assertion(Forall[
+//                              val r = addVar(root.key)
+//                              root.value.call(r) => parentRelations.map[containment |
+//                                      Forall[
+//                                              val container = addVar(containment.parameters.get(0))
+//                                              !containment.call(container,r)
+//                                      ]
+//                              ].And
+//                      ])
+//                      document.assertions+=this.transformAssertion(a3,trace)
+//              }
+//              // no element has two parents
+//              for(root : rootRelations.entrySet) {
+//                      val parentRelations = root.key.lookup(possibleParentRelations)
+//                      val a4 = Assertion(Forall[
+//                              val element = addVar(root.key)
+//                              parentRelations.map[selected |
+//                                      Forall[
+//                                              val container = addVar(selected.parameters.get(0))
+//                                              selected.call(container,element) => (
+//                                                      Forall[
+//                                                              val other = addVar(selected.parameters.get(0))
+//                                                              (!selected.call(other,element)) || (other == element)
+//                                                      ] &&
+//                                                      parentRelations.filter[it !==selected].map[otherContainment |
+//                                                                      Forall[
+//                                                                      val other = addVar(otherContainment.parameters.get(0))
+//                                                                      otherContainment.call(other,element)
+//                                                              ]
+//                                                      ].And)
+//                                              
+//                                              ]
+//                              ].And
+//                      ])
+//                      document.assertions+=this.transformAssertion(a4,trace)
+//              }
+        
+                // an element is not root, then it has a container
+                for(root : rootRelations.entrySet) {
+                        val parentRelations = root.key.lookup(possibleParentRelations)
+                        val a5 = Assertion(Forall[
+                                val element = addVar(root.key)
+                                !root.value.call(element) =>
+                                parentRelations.map[selected |
+                                        Exists[
+                                                val container = addVar(selected.parameters.get(0))
+                                                selected.call(container,element)
+                                        ]
+                                ].Or
+                        ])
+                        document.assertions+=this.transformAssertion(a5,trace)
+                }
+//              
+//              // no circle in containment
+//              for(length : 1..5) {
+//                      val paths = h.containmentRelations.paths(length)
+//                      val loopPaths = paths.filter[path|
+//                              val first = (path.head.parameters.get(0) as ComplexTypeReference).referred
+//                              val last = (path.last.parameters.get(1) as ComplexTypeReference).referred
+//                              hasCommonElement(first,last)
+//                      ]
+//                      for(loopPath : loopPaths) {
+//                              val variableIndexes = 0..<length
+//                              val a6 = Assertion(!Exists[e|
+//                                      val variables = new ArrayList
+//                                      for(variableIndex : variableIndexes) {
+//                                              variables += e.addVar('''c«variableIndex»''',(loopPath.get(variableIndex).parameters.get(0) as ComplexTypeReference).referred)
+//                                      }
+//                                      val pathElements = new ArrayList
+//                                      for(variableIndex : variableIndexes) {
+//                                              val from = variableIndex
+//                                              val to = variableIndex+1
+//                                              if(variableIndexes.contains(to)) {
+//                                                      pathElements += loopPath.get(variableIndex).call(variables.get(from),variables.get(to))
+//                                              }
+//                                      }
+//                                      pathElements += loopPath.last.call(variables.last,variables.head)
+//                                      
+//                                      pathElements.And
+//                              ])
+//                              document.assertions+=this.transformAssertion(a6,trace)
+//                      }
+//              }
+//      }
+//      
+//      def private Iterable<List<Relation>> paths(Iterable<Relation> relations, int length) {
+//              if(length == 0) {
+//                      return #[]
+//              } else if(length == 1) {
+//                      return relations.map[#[it]]
+//              } else {
+//                      val previous = paths(relations,length-1)
+//                      val List<List<Relation>> res = new ArrayList(previous.size*relations.size)
+//                      for(p:previous) {
+//                              for(r:relations) {
+//                                      val lastType = (p.last.parameters.get(1) as ComplexTypeReference).referred
+//                                      val firstType = (r.parameters.get(0) as ComplexTypeReference).referred
+//                                      val hasCommonElement = hasCommonElement(lastType, firstType)
+//                                      if(hasCommonElement) {
+//                                              res.add(new ArrayList(p) => [add(r)])
+//                                      }
+//                              }
+//                      }
+//                      return res
+//              }
+        }
+        
+        protected def boolean hasCommonElement(Type lastType, Type firstType) {
+                val a = lastType.transitiveClosureStar[subtypes]
+                val b = firstType.transitiveClosureStar[subtypes]
+                return a.exists[b.contains(it)]
+        }
+        
+        def transformContainmentV2(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) {
+                val typeConstraintsOfTypesInContainment = h.typesOrderedInHierarchy
+                        .map[typeMapper.transformTypeReference(it,trace)].flatten
+                val relationsOfTypeConstraints = h.containmentRelations.map[it]
+                val typesOfTypeConstraints = typeConstraintsOfTypesInContainment
+                        .map[(it.type as SMTComplexTypeReference).referred]
+                        .toSet
+                
+                // Root declaration
+                val rootRelations = new HashMap<SMTType,SMTFunctionDeclaration>
+                for(t : typesOfTypeConstraints) {
+                        val rootRelation = createSMTFunctionDeclaration => [
+                                it.name = toID('''root «t.name»''')
+                                it.range = createSMTBoolTypeReference
+                                it.parameters += createSMTComplexTypeReference => [
+                                        it.referred = t
+                                ]
+                        ]
+                        document.input.functionDeclarations += rootRelation
+                        rootRelations.put(t,rootRelation)
+                }
+                // root is true only for one element in every root type
+                for(entry : rootRelations.entrySet) {
+                        document.input.assertions += createSMTAssertion => [
+                                it.value = createSMTForall => [
+                                        val r1 = createSMTSortedVariable => [
+                                                it.name = "r1"
+                                                it.range = createSMTComplexTypeReference => [it.referred = entry.key]
+                                        ]
+                                        val r2 = createSMTSortedVariable => [
+                                                it.name = "r2"
+                                                it.range = createSMTComplexTypeReference => [it.referred = entry.key]
+                                        ]
+                                        
+                                        it.quantifiedVariables += r1
+                                        it.quantifiedVariables += r2
+                                        
+                                        it.expression = createSMTImpl => [
+                                                it.leftOperand = createSMTAnd => [
+                                                        it.operands += createSMTSymbolicValue => [
+                                                                it.symbolicReference = entry.value
+                                                                it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r1]
+                                                        ]
+                                                        it.operands += createSMTSymbolicValue => [
+                                                                it.symbolicReference = entry.value
+                                                                it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r2]
+                                                        ]
+                                                ]
+                                                it.rightOperand = createSMTEquals => [
+                                                        it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = r1]
+                                                        it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = r2]
+                                                ]
+                                        ]
+                                ]
+                        ]
+                }
+                // only one of the root entries is true
+                document.input.assertions += createSMTAssertion => [
+                        it.value = createSMTOr =>[or |
+                                for(selectedCombination : rootRelations.entrySet) {
+                                        or.operands += createSMTAnd => [and |
+                                                for(otherCombination : rootRelations.entrySet) {
+                                                        if(selectedCombination == otherCombination) {
+                                                                and.operands += createSMTExists => [
+                                                                        val r = createSMTSortedVariable => [
+                                                                                it.name = "r"
+                                                                                it.range = createSMTComplexTypeReference => [it.referred = otherCombination.key]
+                                                                        ]
+                                                                        it.quantifiedVariables += r
+                                                                        it.expression = createSMTSymbolicValue => [
+                                                                                it.symbolicReference = otherCombination.value
+                                                                                it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r]
+                                                                        ]
+                                                                ]
+                                                        } else {
+                                                                and.operands += createSMTForall => [
+                                                                        val r = createSMTSortedVariable => [
+                                                                                it.name = "r"
+                                                                                it.range = createSMTComplexTypeReference => [it.referred = otherCombination.key]
+                                                                        ]
+                                                                        it.quantifiedVariables += r
+                                                                        it.expression = createSMTNot=> [
+                                                                                it.operand = createSMTSymbolicValue => [
+                                                                                        it.symbolicReference = otherCombination.value
+                                                                                        it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r]
+                                                                                ]
+                                                                        ]
+                                                                ]
+                                                        }
+                                                }
+                                        ]
+                                }
                        ]
                ]
-        }*/
+                
+                // the root has no parent
+                throw new UnsupportedOperationException('''Unfinished version''')
+                
+                // no element has two parents
+        
+                // an element is either root or has parent
+                
+                // no circle in containment
+        }
        
        ///////////
        
@@ -1052,4 +1313,34 @@ class Logic2SmtMapper{
        def private dispatch replaceWith(EObject object)  {
                null
        }
+        
+        def orderDefinitions(SMTDocument document) {
+                val definitionsInDocument = document.input.functionDefinition
+                val List<SMTFunctionDefinition> definitionsInOrder = new ArrayList(definitionsInDocument.size)
+                while(!definitionsInDocument.empty) {
+                        val selection = definitionsInDocument.selectOneUnreferenced
+                        definitionsInOrder.add(selection)
+                        definitionsInDocument.remove(selection)
+                }
+                document.input.functionDefinition.addAll(definitionsInOrder)
+        }
+        
+        def referencedDefinitions(SMTFunctionDefinition definition) {
+                definition
+                        .eAllContents
+                        .filter(SMTSymbolicValue)
+                        .map[it.symbolicReference]
+                        .filter(SMTFunctionDefinition)
+                        .toList
+        }
+        
+        def selectOneUnreferenced(List<SMTFunctionDefinition> definitions) {
+                for(definition : definitions) {
+                        val references = definition.referencedDefinitions
+                        if(references.forall[!definitions.contains(it)]) {
+                                return definition
+                        }
+                }
+                throw new AssertionError('''Recursion in function definitions! definitions: «definitions.map[name].toList»''')
+        }
 }
 \ No newline at end of file

diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend index aad43716..ec1502e5 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend
@@ -1,5 +1,6 @@
1	package hu.bme.mit.inf.dslreasoner.smt.reasoner	1	package hu.bme.mit.inf.dslreasoner.smt.reasoner
2		2
		3	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
3	import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput	4	import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
4	import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes	5	import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
5	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And	6	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
@@ -42,13 +43,17 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
42	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition	43	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
43	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue	44	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
44	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term	45	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
		46	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
45	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable	47	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
		48	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
46	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem	49	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
47	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd	50	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd
48	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion	51	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion
49	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference	52	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference
50	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference	53	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
51	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument	54	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
		55	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
		56	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
52	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput	57	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
53	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference	58	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference
54	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr	59	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr
@@ -60,6 +65,7 @@ import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
60	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm	65	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
61	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType	66	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType
62	import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory	67	import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
		68	import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil
63	import java.util.ArrayList	69	import java.util.ArrayList
64	import java.util.HashMap	70	import java.util.HashMap
65	import java.util.LinkedHashMap	71	import java.util.LinkedHashMap
@@ -72,18 +78,14 @@ import org.eclipse.xtend.lib.annotations.Accessors
72	import org.eclipse.xtext.xbase.lib.Functions.Function0	78	import org.eclipse.xtext.xbase.lib.Functions.Function0
73	import org.eclipse.xtext.xbase.lib.Functions.Function1	79	import org.eclipse.xtext.xbase.lib.Functions.Function1
74	import org.eclipse.xtext.xbase.lib.Functions.Function2	80	import org.eclipse.xtext.xbase.lib.Functions.Function2
		81
75	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*	82	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
76	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
77	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
78	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
79		83
80	class Logic2SmtMapper{	84	class Logic2SmtMapper{
81	val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE	85	val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
82	val Logic2SmtMapper_UnfoldingSupport unfolder = new Logic2SmtMapper_UnfoldingSupport	86	val Logic2SmtMapper_UnfoldingSupport unfolder = new Logic2SmtMapper_UnfoldingSupport
83	@Accessors val Logic2Smt_TypeMapper typeMapper;	87	@Accessors val Logic2Smt_TypeMapper typeMapper;
84		88
85	LogicProblemBuilder b
86
87	new(Logic2Smt_TypeMapper typeMapper) {	89	new(Logic2Smt_TypeMapper typeMapper) {
88	this.typeMapper = typeMapper	90	this.typeMapper = typeMapper
89	}	91	}
@@ -109,11 +111,16 @@ class Logic2SmtMapper{
109		111
110	problem.relations.filter(RelationDefinition).forEach[it.transformRelationDefinition_definition(documentInput,trace)]	112	problem.relations.filter(RelationDefinition).forEach[it.transformRelationDefinition_definition(documentInput,trace)]
111	documentInput.assertions += problem.assertions.map[transformAssertion(trace)]	113	documentInput.assertions += problem.assertions.map[transformAssertion(trace)]
		114
		115	if(!problem.containmentHierarchies.empty) {
		116	transformContainmentV1(documentInput,problem.containmentHierarchies.head,trace)
		117	}
112	// End trafo	118	// End trafo
113		119
114	document.input.assertions.forEach[it.value.nameAllUnnamedVariable]	120	document.input.assertions.forEach[it.value.nameAllUnnamedVariable]
115	document.input.functionDefinition.forEach[it.value.nameAllUnnamedVariable]	121	document.input.functionDefinition.forEach[it.value.nameAllUnnamedVariable]
116	document.cleanDocument	122	document.cleanDocument
		123	document.orderDefinitions
117	return new TracedOutput(document,trace)	124	return new TracedOutput(document,trace)
118	}	125	}
119		126
@@ -1000,15 +1007,269 @@ class Logic2SmtMapper{
1000		1007
1001	///////////	1008	///////////
1002		1009
1003	/*def transformContainment(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) {	1010	def transformContainmentV1(SMTInput document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) {
1004	val containmentRelation_oo = createSMTFunctionDefinition=>[	1011	val extension builder = new LogicProblemBuilder
1005	it.name="containment!oo"	1012	val types = h.typesOrderedInHierarchy
1006	it.range=createSMTBoolTypeReference	1013
1007	val child = createSMTSortedVariable => [	1014	val rootRelations = new HashMap<Type,Relation>
1008	it.name =	1015	for(type: types) {
		1016	val rootRelation = RelationDeclaration('''Root «type.name»''',type)
		1017	rootRelations.put(type,rootRelation)
		1018	this.transformRelationDeclaration(rootRelation,document,trace)
		1019	}
		1020	val possibleParentRelations = types.toInvertedMap[type\|
		1021	h.containmentRelations.filter[it.parameters.get(1) === type]
		1022	//TODO inheritance
		1023	]
		1024
		1025	// root is true only for at most one element in every root type
		1026	for(root: rootRelations.entrySet) {
		1027	val a1 = Assertion(Forall[
		1028	val r1 = addVar(root.key)
		1029	val r2 = addVar(root.key)
		1030	(root.value.call(r1) && root.value.call(r2)) => (r1 == r2)
		1031	])
		1032	document.assertions+=this.transformAssertion(a1,trace)
		1033	}
		1034	// only one of the root entries is true
		1035	// val a2 = Assertion(
		1036	// rootRelations.entrySet.map[selected\|
		1037	// rootRelations.entrySet.map[other\|
		1038	// if(selected == other) {
		1039	// Exists[
		1040	// val r = addVar(other.key)
		1041	// other.value.call(r)
		1042	// ]
		1043	// } else {
		1044	// Forall[
		1045	// val r = addVar(other.key)
		1046	// !other.value.call(r)
		1047	// ]
		1048	// }
		1049	// ].And
		1050	// ].Or
		1051	// )
		1052	// document.assertions+=this.transformAssertion(a2,trace)
		1053	// // the root has no parent
		1054	// for(root : rootRelations.entrySet) {
		1055	// val parentRelations = root.key.lookup(possibleParentRelations)
		1056	// val a3 = Assertion(Forall[
		1057	// val r = addVar(root.key)
		1058	// root.value.call(r) => parentRelations.map[containment \|
		1059	// Forall[
		1060	// val container = addVar(containment.parameters.get(0))
		1061	// !containment.call(container,r)
		1062	// ]
		1063	// ].And
		1064	// ])
		1065	// document.assertions+=this.transformAssertion(a3,trace)
		1066	// }
		1067	// // no element has two parents
		1068	// for(root : rootRelations.entrySet) {
		1069	// val parentRelations = root.key.lookup(possibleParentRelations)
		1070	// val a4 = Assertion(Forall[
		1071	// val element = addVar(root.key)
		1072	// parentRelations.map[selected \|
		1073	// Forall[
		1074	// val container = addVar(selected.parameters.get(0))
		1075	// selected.call(container,element) => (
		1076	// Forall[
		1077	// val other = addVar(selected.parameters.get(0))
		1078	// (!selected.call(other,element)) \|\| (other == element)
		1079	// ] &&
		1080	// parentRelations.filter[it !==selected].map[otherContainment \|
		1081	// Forall[
		1082	// val other = addVar(otherContainment.parameters.get(0))
		1083	// otherContainment.call(other,element)
		1084	// ]
		1085	// ].And)
		1086	//
		1087	// ]
		1088	// ].And
		1089	// ])
		1090	// document.assertions+=this.transformAssertion(a4,trace)
		1091	// }
		1092
		1093	// an element is not root, then it has a container
		1094	for(root : rootRelations.entrySet) {
		1095	val parentRelations = root.key.lookup(possibleParentRelations)
		1096	val a5 = Assertion(Forall[
		1097	val element = addVar(root.key)
		1098	!root.value.call(element) =>
		1099	parentRelations.map[selected \|
		1100	Exists[
		1101	val container = addVar(selected.parameters.get(0))
		1102	selected.call(container,element)
		1103	]
		1104	].Or
		1105	])
		1106	document.assertions+=this.transformAssertion(a5,trace)
		1107	}
		1108	//
		1109	// // no circle in containment
		1110	// for(length : 1..5) {
		1111	// val paths = h.containmentRelations.paths(length)
		1112	// val loopPaths = paths.filter[path\|
		1113	// val first = (path.head.parameters.get(0) as ComplexTypeReference).referred
		1114	// val last = (path.last.parameters.get(1) as ComplexTypeReference).referred
		1115	// hasCommonElement(first,last)
		1116	// ]
		1117	// for(loopPath : loopPaths) {
		1118	// val variableIndexes = 0..<length
		1119	// val a6 = Assertion(!Exists[e\|
		1120	// val variables = new ArrayList
		1121	// for(variableIndex : variableIndexes) {
		1122	// variables += e.addVar('''c«variableIndex»''',(loopPath.get(variableIndex).parameters.get(0) as ComplexTypeReference).referred)
		1123	// }
		1124	// val pathElements = new ArrayList
		1125	// for(variableIndex : variableIndexes) {
		1126	// val from = variableIndex
		1127	// val to = variableIndex+1
		1128	// if(variableIndexes.contains(to)) {
		1129	// pathElements += loopPath.get(variableIndex).call(variables.get(from),variables.get(to))
		1130	// }
		1131	// }
		1132	// pathElements += loopPath.last.call(variables.last,variables.head)
		1133	//
		1134	// pathElements.And
		1135	// ])
		1136	// document.assertions+=this.transformAssertion(a6,trace)
		1137	// }
		1138	// }
		1139	// }
		1140	//
		1141	// def private Iterable<List<Relation>> paths(Iterable<Relation> relations, int length) {
		1142	// if(length == 0) {
		1143	// return #[]
		1144	// } else if(length == 1) {
		1145	// return relations.map[#[it]]
		1146	// } else {
		1147	// val previous = paths(relations,length-1)
		1148	// val List<List<Relation>> res = new ArrayList(previous.size*relations.size)
		1149	// for(p:previous) {
		1150	// for(r:relations) {
		1151	// val lastType = (p.last.parameters.get(1) as ComplexTypeReference).referred
		1152	// val firstType = (r.parameters.get(0) as ComplexTypeReference).referred
		1153	// val hasCommonElement = hasCommonElement(lastType, firstType)
		1154	// if(hasCommonElement) {
		1155	// res.add(new ArrayList(p) => [add(r)])
		1156	// }
		1157	// }
		1158	// }
		1159	// return res
		1160	// }
		1161	}
		1162
		1163	protected def boolean hasCommonElement(Type lastType, Type firstType) {
		1164	val a = lastType.transitiveClosureStar[subtypes]
		1165	val b = firstType.transitiveClosureStar[subtypes]
		1166	return a.exists[b.contains(it)]
		1167	}
		1168
		1169	def transformContainmentV2(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) {
		1170	val typeConstraintsOfTypesInContainment = h.typesOrderedInHierarchy
		1171	.map[typeMapper.transformTypeReference(it,trace)].flatten
		1172	val relationsOfTypeConstraints = h.containmentRelations.map[it]
		1173	val typesOfTypeConstraints = typeConstraintsOfTypesInContainment
		1174	.map[(it.type as SMTComplexTypeReference).referred]
		1175	.toSet
		1176
		1177	// Root declaration
		1178	val rootRelations = new HashMap<SMTType,SMTFunctionDeclaration>
		1179	for(t : typesOfTypeConstraints) {
		1180	val rootRelation = createSMTFunctionDeclaration => [
		1181	it.name = toID('''root «t.name»''')
		1182	it.range = createSMTBoolTypeReference
		1183	it.parameters += createSMTComplexTypeReference => [
		1184	it.referred = t
		1185	]
		1186	]
		1187	document.input.functionDeclarations += rootRelation
		1188	rootRelations.put(t,rootRelation)
		1189	}
		1190	// root is true only for one element in every root type
		1191	for(entry : rootRelations.entrySet) {
		1192	document.input.assertions += createSMTAssertion => [
		1193	it.value = createSMTForall => [
		1194	val r1 = createSMTSortedVariable => [
		1195	it.name = "r1"
		1196	it.range = createSMTComplexTypeReference => [it.referred = entry.key]
		1197	]
		1198	val r2 = createSMTSortedVariable => [
		1199	it.name = "r2"
		1200	it.range = createSMTComplexTypeReference => [it.referred = entry.key]
		1201	]
		1202
		1203	it.quantifiedVariables += r1
		1204	it.quantifiedVariables += r2
		1205
		1206	it.expression = createSMTImpl => [
		1207	it.leftOperand = createSMTAnd => [
		1208	it.operands += createSMTSymbolicValue => [
		1209	it.symbolicReference = entry.value
		1210	it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r1]
		1211	]
		1212	it.operands += createSMTSymbolicValue => [
		1213	it.symbolicReference = entry.value
		1214	it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r2]
		1215	]
		1216	]
		1217	it.rightOperand = createSMTEquals => [
		1218	it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = r1]
		1219	it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = r2]
		1220	]
		1221	]
		1222	]
		1223	]
		1224	}
		1225	// only one of the root entries is true
		1226	document.input.assertions += createSMTAssertion => [
		1227	it.value = createSMTOr =>[or \|
		1228	for(selectedCombination : rootRelations.entrySet) {
		1229	or.operands += createSMTAnd => [and \|
		1230	for(otherCombination : rootRelations.entrySet) {
		1231	if(selectedCombination == otherCombination) {
		1232	and.operands += createSMTExists => [
		1233	val r = createSMTSortedVariable => [
		1234	it.name = "r"
		1235	it.range = createSMTComplexTypeReference => [it.referred = otherCombination.key]
		1236	]
		1237	it.quantifiedVariables += r
		1238	it.expression = createSMTSymbolicValue => [
		1239	it.symbolicReference = otherCombination.value
		1240	it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r]
		1241	]
		1242	]
		1243	} else {
		1244	and.operands += createSMTForall => [
		1245	val r = createSMTSortedVariable => [
		1246	it.name = "r"
		1247	it.range = createSMTComplexTypeReference => [it.referred = otherCombination.key]
		1248	]
		1249	it.quantifiedVariables += r
		1250	it.expression = createSMTNot=> [
		1251	it.operand = createSMTSymbolicValue => [
		1252	it.symbolicReference = otherCombination.value
		1253	it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r]
		1254	]
		1255	]
		1256	]
		1257	}
		1258	}
		1259	]
		1260	}
1009	]	1261	]
1010	]	1262	]
1011	}*/	1263
		1264	// the root has no parent
		1265	throw new UnsupportedOperationException('''Unfinished version''')
		1266
		1267	// no element has two parents
		1268
		1269	// an element is either root or has parent
		1270
		1271	// no circle in containment
		1272	}
1012		1273
1013	///////////	1274	///////////
1014		1275
@@ -1052,4 +1313,34 @@ class Logic2SmtMapper{
1052	def private dispatch replaceWith(EObject object) {	1313	def private dispatch replaceWith(EObject object) {
1053	null	1314	null
1054	}	1315	}
		1316
		1317	def orderDefinitions(SMTDocument document) {
		1318	val definitionsInDocument = document.input.functionDefinition
		1319	val List<SMTFunctionDefinition> definitionsInOrder = new ArrayList(definitionsInDocument.size)
		1320	while(!definitionsInDocument.empty) {
		1321	val selection = definitionsInDocument.selectOneUnreferenced
		1322	definitionsInOrder.add(selection)
		1323	definitionsInDocument.remove(selection)
		1324	}
		1325	document.input.functionDefinition.addAll(definitionsInOrder)
		1326	}
		1327
		1328	def referencedDefinitions(SMTFunctionDefinition definition) {
		1329	definition
		1330	.eAllContents
		1331	.filter(SMTSymbolicValue)
		1332	.map[it.symbolicReference]
		1333	.filter(SMTFunctionDefinition)
		1334	.toList
		1335	}
		1336
		1337	def selectOneUnreferenced(List<SMTFunctionDefinition> definitions) {
		1338	for(definition : definitions) {
		1339	val references = definition.referencedDefinitions
		1340	if(references.forall[!definitions.contains(it)]) {
		1341	return definition
		1342	}
		1343	}
		1344	throw new AssertionError('''Recursion in function definitions! definitions: «definitions.map[name].toList»''')
		1345	}
1055	} \ No newline at end of file	1346	} \ No newline at end of file