Continue improving code style (need sleep)

author: ArenBabikian <aren.babikian@mail.mcgill.ca> 2019-03-06 02:59:19 -0500
committer: ArenBabikian <aren.babikian@mail.mcgill.ca> 2019-03-06 02:59:19 -0500
commit: edfd98b8fca74489ae338077f43521b6c5e6606f (patch)
tree: 68f6236435ea01471b37a8a6d55f8b2d49ff8190
parent: Partially improve coding style (leaving for soccer) (diff)
download: VIATRA-Generator-edfd98b8fca74489ae338077f43521b6c5e6606f.tar.gz
VIATRA-Generator-edfd98b8fca74489ae338077f43521b6c5e6606f.tar.zst
VIATRA-Generator-edfd98b8fca74489ae338077f43521b6c5e6606f.zip
29 files changed, 146 insertions, 292 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index 54c44c72..81af24e5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -40,6 +40,7 @@ import java.util.Map
 import org.eclipse.xtend.lib.annotations.Accessors
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
 class Logic2VampireLanguageMapper {
        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -227,18 +228,18 @@ class Logic2VampireLanguageMapper {
 //      
        def dispatch protected VLSTerm transformTerm(Forall forall, Logic2VampireLanguageMapperTrace trace,
                Map<Variable, VLSVariable> variables) {
-                support.createUniversallyQuantifiedExpression(this, forall, trace, variables)
+                support.createQuantifiedExpression(this, forall, trace, variables, true)
        }
        def dispatch protected VLSTerm transformTerm(Exists exists, Logic2VampireLanguageMapperTrace trace,
                Map<Variable, VLSVariable> variables) {
-                support.createExistentiallyQuantifiedExpression(this, exists, trace, variables)
+                support.createQuantifiedExpression(this, exists, trace, variables, false)
        }
        def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace,
                Map<Variable, VLSVariable> variables) {
                return createVLSFunction => [
-                        it.constant = support.toIDMultiple("t", (instanceOf.range as ComplexTypeReference).referred.name)
+                        it.constant = (instanceOf.range as ComplexTypeReference).referred.lookup(trace.type2Predicate).constant
                        it.terms += instanceOf.value.transformTerm(trace, variables)
                ]
        }
@@ -292,13 +293,8 @@ class Logic2VampireLanguageMapper {
                Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
                // cannot treat variable as function (constant) because of name ID not being the same
-                // below does not work
-                val res = createVLSVariable => [
-//                                              it.name = support.toIDMultiple("Var", variable.lookup(variables).name)
-                        it.name = support.toID(variable.lookup(variables).name)
-                ]
                // no need for potprocessing cuz booleans are supported
-                return res
+                return support.duplicate(variable.lookup(variables))
        }
        // TODO
@@ -383,7 +379,7 @@ class Logic2VampireLanguageMapper {
 //                                              it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
 //                                      ]
                return createVLSFunction => [
-                        it.constant = support.toIDMultiple("rel", relation.name)
+                        it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
                        it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
                ]
        }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index 23b57701..deb24778 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -30,15 +30,13 @@ class Logic2VampireLanguageMapper_RelationMapper {
                // 1.1 if variable has type, creating list of type declarations
                val List<VLSVariable> relVar2VLS = new ArrayList
                val List<VLSFunction> relVar2TypeDecComply = new ArrayList
-                val typedefs = new ArrayList<VLSTerm>
                for (i : 0 ..< r.parameters.length) {
                        val v = createVLSVariable => [
                                it.name = support.toIDMultiple("V", i.toString)
                        ]
                        relVar2VLS.add(v)
-                        
                        val relType = (r.parameters.get(i) as ComplexTypeReference).referred
                        val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v)
                        relVar2TypeDecComply.add(varTypeComply)
@@ -47,33 +45,26 @@ class Logic2VampireLanguageMapper_RelationMapper {
                val comply = createVLSFofFormula => [
                        val nameArray = r.name.split(" ")
-                        it.name = support.toIDMultiple("compliance", nameArray.get(0),
+                        it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2))
-                                nameArray.get(2))
                        it.fofRole = "axiom"
                        it.fofFormula = createVLSUniversalQuantifier => [
                                for (v : relVar2VLS) {
                                        it.variables += support.duplicate(v)
                                }
                                it.operand = createVLSImplies => [
-                                        it.left = createVLSFunction => [
+                                        val rel = createVLSFunction => [
-                                                it.constant = support.toIDMultiple("rel", r.name)
+                                                it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2))
+                                                for (v : relVar2VLS) {
-                                                for (i : 0 ..< r.parameters.length) {
+                                                        it.terms += support.duplicate(v)
-                                                        val v = createVLSVariable => [
-                                                                it.name = relVar2VLS.get(i).name
-                                                        ]
-                                                        it.terms += v
                                                }
                                        ]
+                                        trace.rel2Predicate.put(r, rel)
+                                        it.left = support.duplicate(rel)
                                        it.right = support.unfoldAnd(relVar2TypeDecComply)
                                ]
                        ]
                ]
-                // trace.relationDefinition2Predicate.put(r,res)
                trace.specification.formulas += comply
        }
@@ -100,9 +91,8 @@ class Logic2VampireLanguageMapper_RelationMapper {
                        relationVar2TypeDecComply.put(variable, varTypeComply)
                        relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
                }
+                val nameArray = reldef.name.split(" ")
                val comply = createVLSFofFormula => [
-                        val nameArray = reldef.name.split(" ")
                        it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
                                nameArray.get(nameArray.length - 1))
                        it.fofRole = "axiom"
@@ -127,7 +117,8 @@ class Logic2VampireLanguageMapper_RelationMapper {
                ]
                val res = createVLSFofFormula => [
-                        it.name = support.toIDMultiple("relation", reldef.name)
+                        it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
+                                nameArray.get(nameArray.length - 1))
                        it.fofRole = "axiom"
                        it.fofFormula = createVLSUniversalQuantifier => [
                                for (variable : reldef.variables) {
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index 090cf916..d3595a73 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -17,6 +17,8 @@ import java.util.List
 import java.util.Map
 import org.eclipse.emf.common.util.EList
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 class Logic2VampireLanguageMapper_Support {
        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -29,28 +31,27 @@ class Logic2VampireLanguageMapper_Support {
                ids.split("\\s+").join("_")
        }
-        //Term Handling
+        // Term Handling
-        //TODO Make more general
+        // TODO Make more general
        def protected VLSVariable duplicate(VLSVariable term) {
                return createVLSVariable => [it.name = term.name]
        }
-        
        def protected VLSFunction duplicate(VLSFunction term) {
                return createVLSFunction => [
                        it.constant = term.constant
-                        for ( v : term.terms){
+                        for (v : term.terms) {
                                it.terms += duplicate(v as VLSVariable)
                        }
-                        ]
+                ]
        }
-        
        def protected VLSFunction duplicate(VLSFunction term, VLSVariable v) {
                return createVLSFunction => [
                        it.constant = term.constant
                        it.terms += duplicate(v)
-                        ]
+                ]
        }
-        
        def protected VLSFunction topLevelTypeFunc() {
                return createVLSFunction => [
@@ -60,24 +61,22 @@ class Logic2VampireLanguageMapper_Support {
                        ]
                ]
        }
-        
-        //TODO Make more general
+        // TODO Make more general
        def establishUniqueness(List<VLSConstant> terms) {
                val List<VLSInequality> eqs = newArrayList
-                for (t1 : terms.subList(1, terms.length)){
+                for (t1 : terms.subList(1, terms.length)) {
-                        for (t2 : terms.subList(0, terms.indexOf(t1))){
+                        for (t2 : terms.subList(0, terms.indexOf(t1))) {
                                val eq = createVLSInequality => [
-                                        //TEMP
+                                        // TEMP
                                        it.left = createVLSConstant => [it.name = t2.name]
                                        it.right = createVLSConstant => [it.name = t1.name]
-                                        //TEMP
+                                // TEMP
                                ]
                                eqs.add(eq)
-                        }                       
+                        }
                }
-                
                return unfoldAnd(eqs)
-                
        }
        // Support Functions
@@ -108,6 +107,7 @@ class Logic2VampireLanguageMapper_Support {
                        throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP
        }
+        // can delete below
        def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands,
                Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
                if (operands.size == 1) {
@@ -143,58 +143,36 @@ class Logic2VampireLanguageMapper_Support {
         * }
         */
        // QUANTIFIERS + VARIABLES
-        def protected VLSTerm createUniversallyQuantifiedExpression(Logic2VampireLanguageMapper mapper,
+        def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper,
-                QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+                QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables, boolean isUniversal) {
                val variableMap = expression.quantifiedVariables.toInvertedMap [ v |
-                        createVLSVariable => [it.name = toIDMultiple("Var", v.name)]
+                        createVLSVariable => [it.name = toIDMultiple("V", v.name)]
                ]
                val typedefs = new ArrayList<VLSTerm>
                for (variable : expression.quantifiedVariables) {
-                        val eq = createVLSFunction => [
+                        val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), variable.lookup(variableMap))
-                                it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
-                                it.terms += createVLSVariable => [
-                                        it.name = toIDMultiple("Var", variable.name)
-                                ]
-                        ]
                        typedefs.add(eq)
                }
+                if (isUniversal) {
-                createVLSUniversalQuantifier => [
+                        createVLSUniversalQuantifier => [
-                        it.variables += variableMap.values
+                                it.variables += variableMap.values
-                        it.operand = createVLSImplies => [
+                                it.operand = createVLSImplies => [
-                                it.left = unfoldAnd(typedefs)
+                                        it.left = unfoldAnd(typedefs)
-                                it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))
+                                        it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))
+                                ]
                        ]
-                ]
+                } else {
-        }
+                        typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)))
+                        createVLSExistentialQuantifier => [
+                                it.variables += variableMap.values
+                                it.operand = unfoldAnd(typedefs)
-        def protected VLSTerm createExistentiallyQuantifiedExpression(Logic2VampireLanguageMapper mapper,
-                QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
-                val variableMap = expression.quantifiedVariables.toInvertedMap [ v |
-                        createVLSVariable => [it.name = toIDMultiple("Var", v.name)]
-                ]
-                val typedefs = new ArrayList<VLSTerm>
-                for (variable : expression.quantifiedVariables) {
-                        val eq = createVLSFunction => [
-                                it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
-                                it.terms += createVLSVariable => [
-                                        it.name = toIDMultiple("Var", variable.name)
-                                ]
                        ]
-                        typedefs.add(eq)
                }
-                typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)))
-                createVLSExistentialQuantifier => [
-                        it.variables += variableMap.values
-                        it.operand = unfoldAnd(typedefs)
-                ]
        }
-        
        def protected boolean dfsSupertypeCheck(Type type, Type type2) {
                // There is surely a better way to do this
                if (type.supertypes.isEmpty)
@@ -213,7 +191,5 @@ class Logic2VampireLanguageMapper_Support {
        def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) {
                new HashMap(map1) => [putAll(map2)]
        }
-        
-        
 }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index bda7463e..4828107b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index a062fcec..64061f82 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index 5fc0da27..f0cd1c7c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
index 562b9bbf..7d15db96 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index dd7bdf86..8fed8f56 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 496d27b3..a40e27e4 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index 4a03f2ce..4b6b4a1e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index 511f4a1f..c3035658 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index 37e9480c..2e21736e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
index f473c4bc..e870dabc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
index e53791d6..ed198ef6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index 1b112c56..83697125 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index c8284658..063650c5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
index 89d4c657..e36d2270 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
index 3c98bd64..5e5be153 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index 6643576f..dc2cd5ec 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -50,6 +50,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration;
 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.TypeReference;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
@@ -262,18 +263,18 @@ public class Logic2VampireLanguageMapper {
  }
  
  protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
-    return this.support.createUniversallyQuantifiedExpression(this, forall, trace, variables);
+    return this.support.createQuantifiedExpression(this, forall, trace, variables, true);
  }
  
  protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
-    return this.support.createExistentiallyQuantifiedExpression(this, exists, trace, variables);
+    return this.support.createQuantifiedExpression(this, exists, trace, variables, false);
  }
  
  protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
      TypeReference _range = instanceOf.getRange();
-      it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));
+      it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate).getConstant());
      EList<VLSTerm> _terms = it.getTerms();
      VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables);
      _terms.add(_transformTerm);
@@ -303,12 +304,7 @@ public class Logic2VampireLanguageMapper {
  }
  
  protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
-    VLSVariable _createVLSVariable = this.factory.createVLSVariable();
+    return this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables));
-    final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
-      it.setName(this.support.toID(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables).getName()));
-    };
-    final VLSVariable res = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
-    return res;
  }
  
  protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
@@ -359,7 +355,7 @@ public class Logic2VampireLanguageMapper {
  protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
-      it.setConstant(this.support.toIDMultiple("rel", relation.getName()));
+      it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant());
      EList<VLSTerm> _terms = it.getTerms();
      final Function1<Term, VLSTerm> _function_1 = (Term p) -> {
        return this.transformTerm(p, trace, variables);
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
index 4f5c6acc..d5745333 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
@@ -48,7 +48,6 @@ public class Logic2VampireLanguageMapper_RelationMapper {
  public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) {
    final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>();
    final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>();
-    final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();
    int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
    ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true);
    for (final Integer i : _doubleDotLessThan) {
@@ -68,8 +67,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
    final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
      final String[] nameArray = r.getName().split(" ");
-      it.setName(this.support.toIDMultiple("compliance", nameArray[0], 
+      it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2]));
-        nameArray[2]));
      it.setFofRole("axiom");
      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
      final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
@@ -82,23 +80,16 @@ public class Logic2VampireLanguageMapper_RelationMapper {
        final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {
          VLSFunction _createVLSFunction = this.factory.createVLSFunction();
          final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {
-            it_3.setConstant(this.support.toIDMultiple("rel", r.getName()));
+            it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2]));
-            int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
+            for (final VLSVariable v_1 : relVar2VLS) {
-            ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true);
+              EList<VLSTerm> _terms = it_3.getTerms();
-            for (final Integer i_1 : _doubleDotLessThan_1) {
+              VLSVariable _duplicate_1 = this.support.duplicate(v_1);
-              {
+              _terms.add(_duplicate_1);
-                VLSVariable _createVLSVariable = this.factory.createVLSVariable();
-                final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> {
-                  it_4.setName(relVar2VLS.get((i_1).intValue()).getName());
-                };
-                final VLSVariable v_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4);
-                EList<VLSTerm> _terms = it_3.getTerms();
-                _terms.add(v_1);
-              }
            }
          };
-          VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);
+          final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);
-          it_2.setLeft(_doubleArrow);
+          trace.rel2Predicate.put(r, rel);
+          it_2.setLeft(this.support.duplicate(rel));
          it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply));
        };
        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
@@ -139,9 +130,9 @@ public class Logic2VampireLanguageMapper_RelationMapper {
        relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply));
      }
    }
+    final String[] nameArray = reldef.getName().split(" ");
    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
    final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
-      final String[] nameArray = reldef.getName().split(" ");
      int _length = nameArray.length;
      int _minus = (_length - 2);
      int _length_1 = nameArray.length;
@@ -190,7 +181,12 @@ public class Logic2VampireLanguageMapper_RelationMapper {
    final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
    VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
    final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
-      it.setName(this.support.toIDMultiple("relation", reldef.getName()));
+      int _length = nameArray.length;
+      int _minus = (_length - 2);
+      int _length_1 = nameArray.length;
+      int _minus_1 = (_length_1 - 1);
+      it.setName(this.support.toIDMultiple("relation", nameArray[_minus], 
+        nameArray[_minus_1]));
      it.setFofRole("axiom");
      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
      final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
index 35497eab..72ca44e9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
@@ -20,6 +20,7 @@ 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.TypeReference;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
+import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.HashMap;
@@ -220,13 +221,13 @@ public class Logic2VampireLanguageMapper_Support {
   *    ids.map[it.split("\\s+").join("'")].join("'")
   * }
   */
-  protected VLSTerm createUniversallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
+  protected VLSTerm createQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables, final boolean isUniversal) {
-    VLSUniversalQuantifier _xblockexpression = null;
+    VLSTerm _xblockexpression = null;
    {
      final Function1<Variable, VLSVariable> _function = (Variable v) -> {
        VLSVariable _createVLSVariable = this.factory.createVLSVariable();
        final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> {
-          it.setName(this.toIDMultiple("Var", v.getName()));
+          it.setName(this.toIDMultiple("V", v.getName()));
        };
        return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1);
      };
@@ -235,80 +236,43 @@ public class Logic2VampireLanguageMapper_Support {
      EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables();
      for (final Variable variable : _quantifiedVariables) {
        {
-          VLSFunction _createVLSFunction = this.factory.createVLSFunction();
+          TypeReference _range = variable.getRange();
-          final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
+          final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap));
-            TypeReference _range = variable.getRange();
-            it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));
-            EList<VLSTerm> _terms = it.getTerms();
-            VLSVariable _createVLSVariable = this.factory.createVLSVariable();
-            final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> {
-              it_1.setName(this.toIDMultiple("Var", variable.getName()));
-            };
-            VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2);
-            _terms.add(_doubleArrow);
-          };
-          final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
          typedefs.add(eq);
        }
      }
-      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
+      VLSTerm _xifexpression = null;
-      final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> {
+      if (isUniversal) {
-        EList<VLSVariable> _variables = it.getVariables();
+        VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
-        Collection<VLSVariable> _values = variableMap.values();
+        final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> {
-        Iterables.<VLSVariable>addAll(_variables, _values);
+          EList<VLSVariable> _variables = it.getVariables();
-        VLSImplies _createVLSImplies = this.factory.createVLSImplies();
+          Collection<VLSVariable> _values = variableMap.values();
-        final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> {
+          Iterables.<VLSVariable>addAll(_variables, _values);
-          it_1.setLeft(this.unfoldAnd(typedefs));
+          VLSImplies _createVLSImplies = this.factory.createVLSImplies();
-          it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));
+          final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> {
-        };
+            it_1.setLeft(this.unfoldAnd(typedefs));
-        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
+            it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));
-        it.setOperand(_doubleArrow);
+          };
-      };
+          VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
-      _xblockexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
+          it.setOperand(_doubleArrow);
-    }
-    return _xblockexpression;
-  }
-  
-  protected VLSTerm createExistentiallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
-    VLSExistentialQuantifier _xblockexpression = null;
-    {
-      final Function1<Variable, VLSVariable> _function = (Variable v) -> {
-        VLSVariable _createVLSVariable = this.factory.createVLSVariable();
-        final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> {
-          it.setName(this.toIDMultiple("Var", v.getName()));
        };
-        return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1);
+        _xifexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
-      };
+      } else {
-      final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function);
+        VLSExistentialQuantifier _xblockexpression_1 = null;
-      final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();
-      EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables();
-      for (final Variable variable : _quantifiedVariables) {
        {
-          VLSFunction _createVLSFunction = this.factory.createVLSFunction();
+          typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));
-          final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
+          VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();
-            TypeReference _range = variable.getRange();
+          final Procedure1<VLSExistentialQuantifier> _function_2 = (VLSExistentialQuantifier it) -> {
-            it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));
+            EList<VLSVariable> _variables = it.getVariables();
-            EList<VLSTerm> _terms = it.getTerms();
+            Collection<VLSVariable> _values = variableMap.values();
-            VLSVariable _createVLSVariable = this.factory.createVLSVariable();
+            Iterables.<VLSVariable>addAll(_variables, _values);
-            final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> {
+            it.setOperand(this.unfoldAnd(typedefs));
-              it_1.setName(this.toIDMultiple("Var", variable.getName()));
-            };
-            VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2);
-            _terms.add(_doubleArrow);
          };
-          final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
+          _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2);
-          typedefs.add(eq);
        }
+        _xifexpression = _xblockexpression_1;
      }
-      typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));
+      _xblockexpression = _xifexpression;
-      VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();
-      final Procedure1<VLSExistentialQuantifier> _function_1 = (VLSExistentialQuantifier it) -> {
-        EList<VLSVariable> _variables = it.getVariables();
-        Collection<VLSVariable> _values = variableMap.values();
-        Iterables.<VLSVariable>addAll(_variables, _values);
-        it.setOperand(this.unfoldAnd(typedefs));
-      };
-      _xblockexpression = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_1);
    }
    return _xblockexpression;
  }
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
index a0b5d6ea..85e09a0a 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="ASCII"?>
-<language:LogicProblem xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/ecore2logicannotation" xmlns:language="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" xmlns:language_1="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" xmlns:viatra2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/viatra2logicannotation">
+<language:LogicProblem xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/ecore2logicannotation" xmlns:language="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" xmlns:language_1="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language">
  <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/>
  <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class"/>
  <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/>
@@ -494,22 +494,6 @@
      </expression>
    </value>
  </assertions>
-  <assertions name="errorpattern ca mcgill ecse dslreasoner vampire queries terminatorAndInformation" annotations="//@annotations.20">
-    <value xsi:type="language_1:Forall">
-      <quantifiedVariables name="p0">
-        <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/>
-      </quantifiedVariables>
-      <quantifiedVariables name="p1">
-        <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/>
-      </quantifiedVariables>
-      <expression xsi:type="language_1:Not">
-        <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15">
-          <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.0"/>
-          <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.1"/>
-        </operand>
-      </expression>
-    </value>
-  </assertions>
  <relations xsi:type="language_1:RelationDeclaration" name="interface reference FunctionalElement">
    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/>
    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.5"/>
@@ -570,48 +554,6 @@
    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>
    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/>
  </relations>
-  <relations xsi:type="language_1:RelationDefinition" name="pattern ca mcgill ecse dslreasoner vampire queries terminatorAndInformation" annotations="//@annotations.19">
-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/>
-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/>
-    <variables name="parameter T">
-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/>
-    </variables>
-    <variables name="parameter I">
-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/>
-    </variables>
-    <value xsi:type="language_1:Or">
-      <operands xsi:type="language_1:Exists">
-        <quantifiedVariables name="variable Out">
-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.7"/>
-        </quantifiedVariables>
-        <expression xsi:type="language_1:And">
-          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.11">
-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/>
-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/>
-          </operands>
-          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12">
-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/>
-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/>
-          </operands>
-        </expression>
-      </operands>
-      <operands xsi:type="language_1:Exists">
-        <quantifiedVariables name="variable In">
-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.6"/>
-        </quantifiedVariables>
-        <expression xsi:type="language_1:And">
-          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.7">
-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/>
-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/>
-          </operands>
-          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12">
-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/>
-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/>
-          </operands>
-        </expression>
-      </operands>
-    </value>
-  </relations>
  <elements name="Root literal FunctionType" definedInType="//@types.9"/>
  <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/>
  <elements name="Leaf literal FunctionType" definedInType="//@types.9"/>
@@ -635,6 +577,4 @@
  <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/>
  <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/>
  <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/>
-  <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.15" patternFullyQualifiedName="ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"/>
-  <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.19"/>
 </language:LogicProblem>
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
index 865b3155..4bc4628b 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
@@ -1,42 +1,39 @@
 % This is an initial Test Comment
 fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) .
-fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalData ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
+fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalData ( A ) & t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
 fof ( typeScope , axiom , ! [ A ] : ( object ( A ) <=> ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) .
 fof ( typeUniqueness , axiom , o1 != o2 & ( o1 != o3 & ( o2 != o3 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) .
-fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_interface_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
+fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
-fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_model_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) .
+fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) .
-fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_parent_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) .
+fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) .
-fof ( compliance_rootElements_FunctionalArchitectureModel , axiom , ! [ V_0 , V_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( V_0 , V_1 ) => ( t_FunctionalArchitectureModel ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
+fof ( compliance_rootElements_FunctionalArchitectureModel , axiom , ! [ V_0 , V_1 ] : ( r_rootElements_FunctionalArchitectureModel ( V_0 , V_1 ) => ( t_FunctionalArchitectureModel ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
-fof ( compliance_subElements_Function , axiom , ! [ V_0 , V_1 ] : ( rel_subElements_reference_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
+fof ( compliance_subElements_Function , axiom , ! [ V_0 , V_1 ] : ( r_subElements_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
-fof ( compliance_data_FAMTerminator , axiom , ! [ V_0 , V_1 ] : ( rel_data_reference_FAMTerminator ( V_0 , V_1 ) => ( t_FAMTerminator ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) .
+fof ( compliance_data_FAMTerminator , axiom , ! [ V_0 , V_1 ] : ( r_data_FAMTerminator ( V_0 , V_1 ) => ( t_FAMTerminator ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) .
-fof ( compliance_from_InformationLink , axiom , ! [ V_0 , V_1 ] : ( rel_from_reference_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalOutput ( V_1 ) ) ) ) .
+fof ( compliance_from_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_from_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalOutput ( V_1 ) ) ) ) .
-fof ( compliance_to_InformationLink , axiom , ! [ V_0 , V_1 ] : ( rel_to_reference_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalInput ( V_1 ) ) ) ) .
+fof ( compliance_to_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_to_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalInput ( V_1 ) ) ) ) .
-fof ( compliance_data_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( rel_data_reference_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) .
+fof ( compliance_data_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_data_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) .
-fof ( compliance_element_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( rel_element_reference_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
+fof ( compliance_element_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_element_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
-fof ( compliance_IncomingLinks_FunctionalInput , axiom , ! [ V_0 , V_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( V_0 , V_1 ) => ( t_FunctionalInput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) .
+fof ( compliance_IncomingLinks_FunctionalInput , axiom , ! [ V_0 , V_1 ] : ( r_IncomingLinks_FunctionalInput ( V_0 , V_1 ) => ( t_FunctionalInput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) .
-fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( V_0 , V_1 ) => ( t_FunctionalOutput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) .
+fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( r_outgoingLinks_FunctionalOutput ( V_0 , V_1 ) => ( t_FunctionalOutput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) .
-fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( rel_terminator_reference_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) .
+fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_terminator_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) .
-fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( rel_interface_reference_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
+fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
-fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( rel_type_attribute_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) .
+fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( r_type_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) .
-fof ( compliance_queries_terminatorAndInformation , axiom , ! [ V_parameter_T , V_parameter_I ] : ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( V_parameter_T , V_parameter_I ) => ( t_FAMTerminator_class ( V_parameter_T ) & t_InformationLink_class ( V_parameter_I ) ) ) ) .
+fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalElement ( V_src , V_trg_1 ) & r_interface_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
-fof ( relation_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ V_parameter_T , V_parameter_I ] : ( ( t_FAMTerminator_class ( V_parameter_T ) & t_InformationLink_class ( V_parameter_I ) ) => ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( V_parameter_T , V_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( t_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , V_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , V_parameter_T ) ) ) | ? [ Var_variable_In ] : ( t_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( V_parameter_I , Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , V_parameter_T ) ) ) ) ) ) ) .
+fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ V_src ] : ( t_FunctionalElement ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalArchitectureModel ( V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_1 ) ) ) ) .
-fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
+fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalArchitectureModel ( V_trg_1 ) & t_FunctionalArchitectureModel ( V_trg_2 ) ) ) => ( ( r_model_FunctionalElement ( V_src , V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
-fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( t_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) .
+fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_Function ( V_trg_1 ) & t_Function ( V_trg_2 ) ) ) => ( ( r_parent_FunctionalElement ( V_src , V_trg_1 ) & r_parent_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
-fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & t_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
+fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FAMTerminator ( V_src ) & ( t_FunctionalData ( V_trg_1 ) & t_FunctionalData ( V_trg_2 ) ) ) => ( ( r_data_FAMTerminator ( V_src , V_trg_1 ) & r_data_FAMTerminator ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
-fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_Function_class ( Var_trg_1 ) & t_Function_class ( Var_trg_2 ) ) ) => ( ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_parent_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
+fof ( upperMultiplicity_from_InformationLink , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_InformationLink ( V_src ) & ( t_FunctionalOutput ( V_trg_1 ) & t_FunctionalOutput ( V_trg_2 ) ) ) => ( ( r_from_InformationLink ( V_src , V_trg_1 ) & r_from_InformationLink ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
-fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FAMTerminator_class ( Var_src ) & ( t_FunctionalData_class ( Var_trg_1 ) & t_FunctionalData_class ( Var_trg_2 ) ) ) => ( ( rel_data_reference_FAMTerminator ( Var_src , Var_trg_1 ) & rel_data_reference_FAMTerminator ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
+fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ V_src ] : ( t_InformationLink ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalInput ( V_trg_1 ) & r_to_InformationLink ( V_src , V_trg_1 ) ) ) ) .
-fof ( upperMultiplicity_from_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalOutput_class ( Var_trg_1 ) & t_FunctionalOutput_class ( Var_trg_2 ) ) ) => ( ( rel_from_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_from_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
+fof ( upperMultiplicity_to_InformationLink , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_InformationLink ( V_src ) & ( t_FunctionalInput ( V_trg_1 ) & t_FunctionalInput ( V_trg_2 ) ) ) => ( ( r_to_InformationLink ( V_src , V_trg_1 ) & r_to_InformationLink ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
-fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ Var_src ] : ( t_InformationLink_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalInput_class ( Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) ) ) ) .
+fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalInterface ( V_src ) & ( t_FunctionalElement ( V_trg_1 ) & t_FunctionalElement ( V_trg_2 ) ) ) => ( ( r_element_FunctionalInterface ( V_src , V_trg_1 ) & r_element_FunctionalInterface ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
-fof ( upperMultiplicity_to_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalInput_class ( Var_trg_1 ) & t_FunctionalInput_class ( Var_trg_2 ) ) ) => ( ( rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
+fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalData ( V_src ) & ( t_FAMTerminator ( V_trg_1 ) & t_FAMTerminator ( V_trg_2 ) ) ) => ( ( r_terminator_FunctionalData ( V_src , V_trg_1 ) & r_terminator_FunctionalData ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
-fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalInterface_class ( Var_src ) & ( t_FunctionalElement_class ( Var_trg_1 ) & t_FunctionalElement_class ( Var_trg_2 ) ) ) => ( ( rel_element_reference_FunctionalInterface ( Var_src , Var_trg_1 ) & rel_element_reference_FunctionalInterface ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
+fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalData ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalData ( V_src , V_trg_1 ) & r_interface_FunctionalData ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
-fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FAMTerminator_class ( Var_trg_1 ) & t_FAMTerminator_class ( Var_trg_2 ) ) ) => ( ( rel_terminator_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_terminator_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
+fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalElement ( V_src ) & t_FunctionalInterface ( V_trg ) ) => ( r_interface_FunctionalElement ( V_src , V_trg ) <=> r_element_FunctionalInterface ( V_trg , V_src ) ) ) ) .
-fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
+fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalElement ( V_src ) & t_Function ( V_trg ) ) => ( r_parent_FunctionalElement ( V_src , V_trg ) <=> r_subElements_Function ( V_trg , V_src ) ) ) ) .
-fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_FunctionalInterface_class ( Var_trg ) ) => ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_element_reference_FunctionalInterface ( Var_trg , Var_src ) ) ) ) .
+fof ( oppositeReference_data_FAMTerminator , axiom , ! [ V_src , V_trg ] : ( ( t_FAMTerminator ( V_src ) & t_FunctionalData ( V_trg ) ) => ( r_data_FAMTerminator ( V_src , V_trg ) <=> r_terminator_FunctionalData ( V_trg , V_src ) ) ) ) .
-fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_Function_class ( Var_trg ) ) => ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_subElements_reference_Function ( Var_trg , Var_src ) ) ) ) .
+fof ( oppositeReference_from_InformationLink , axiom , ! [ V_src , V_trg ] : ( ( t_InformationLink ( V_src ) & t_FunctionalOutput ( V_trg ) ) => ( r_from_InformationLink ( V_src , V_trg ) <=> r_outgoingLinks_FunctionalOutput ( V_trg , V_src ) ) ) ) .
-fof ( oppositeReference_data_FAMTerminator , axiom , ! [ Var_src , Var_trg ] : ( ( t_FAMTerminator_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FAMTerminator ( Var_src , Var_trg ) <=> rel_terminator_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .
+fof ( oppositeReference_to_InformationLink , axiom , ! [ V_src , V_trg ] : ( ( t_InformationLink ( V_src ) & t_FunctionalInput ( V_trg ) ) => ( r_to_InformationLink ( V_src , V_trg ) <=> r_IncomingLinks_FunctionalInput ( V_trg , V_src ) ) ) ) .
-fof ( oppositeReference_from_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalOutput_class ( Var_trg ) ) => ( rel_from_reference_InformationLink ( Var_src , Var_trg ) <=> rel_outgoingLinks_reference_FunctionalOutput ( Var_trg , Var_src ) ) ) ) .
+fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalInterface ( V_src ) & t_FunctionalData ( V_trg ) ) => ( r_data_FunctionalInterface ( V_src , V_trg ) <=> r_interface_FunctionalData ( V_trg , V_src ) ) ) ) .
-fof ( oppositeReference_to_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalInput_class ( Var_trg ) ) => ( rel_to_reference_InformationLink ( Var_src , Var_trg ) <=> rel_IncomingLinks_reference_FunctionalInput ( Var_trg , Var_src ) ) ) ) .
+fof ( lowerMultiplicity_type_Function , axiom , ! [ V_src ] : ( t_Function ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionType ( V_trg_1 ) & r_type_Function ( V_src , V_trg_1 ) ) ) ) .
-fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalInterface_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FunctionalInterface ( Var_src , Var_trg ) <=> rel_interface_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .
+fof ( upperMultiplicity_type_Function , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_Function ( V_src ) & ( t_FunctionType ( V_trg_1 ) & t_FunctionType ( V_trg_2 ) ) ) => ( ( r_type_Function ( V_src , V_trg_1 ) & r_type_Function ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
-fof ( lowerMultiplicity_type_Function , axiom , ! [ Var_src ] : ( t_Function_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionType_enum ( Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_1 ) ) ) ) .
-fof ( upperMultiplicity_type_Function , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_Function_class ( Var_src ) & ( t_FunctionType_enum ( Var_trg_1 ) & t_FunctionType_enum ( Var_trg_2 ) ) ) => ( ( rel_type_attribute_Function ( Var_src , Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
-fof ( errorpattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_p0 , Var_p1 ] : ( ( t_FAMTerminator_class ( Var_p0 ) & t_InformationLink_class ( Var_p1 ) ) => ~ rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_p0 , Var_p1 ) ) ) .
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
index 8a60f486..20ad6119 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
@@ -39,8 +39,9 @@ class GeneralTest {
                val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
                val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
-                var problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
+                var problem = modelGenerationProblem.output
-                problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
+//              problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
+//              problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
                workspace.writeModel(problem, "Fam.logicproblem")
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
index 2cd47088..6d33db67 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
index b4d3bda8..9f3d423f 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
index 2401e710..5e4df399 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
@@ -15,7 +15,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
 import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore;
 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;
-import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration;
 import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor;
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic;
 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
@@ -59,9 +58,7 @@ public class GeneralTest {
        final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();
        Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
        final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
-        LogicProblem problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput();
+        LogicProblem problem = modelGenerationProblem.getOutput();
-        Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration();
-        problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, _viatra2LogicConfiguration).getOutput();
        workspace.writeModel(problem, "Fam.logicproblem");
        InputOutput.<String>println("Problem created");
        LogicResult solution = null;
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
index ece511d9..4212d100 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
index a7cea425..d00afe64 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
Binary files differ
author	ArenBabikian <aren.babikian@mail.mcgill.ca>	2019-03-06 02:59:19 -0500
committer	ArenBabikian <aren.babikian@mail.mcgill.ca>	2019-03-06 02:59:19 -0500
commit	edfd98b8fca74489ae338077f43521b6c5e6606f (patch)
tree	68f6236435ea01471b37a8a6d55f8b2d49ff8190
parent	Partially improve coding style (leaving for soccer) (diff)
download	VIATRA-Generator-edfd98b8fca74489ae338077f43521b6c5e6606f.tar.gz VIATRA-Generator-edfd98b8fca74489ae338077f43521b6c5e6606f.tar.zst VIATRA-Generator-edfd98b8fca74489ae338077f43521b6c5e6606f.zip