Continue improving code style (need sleep)

3 files changed, 51 insertions, 88 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),
-                                nameArray.get(2))
+                        it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2))
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
-
                                 for (v : relVar2VLS) {
                                         it.variables += support.duplicate(v)
                                 }
-
                                 it.operand = createVLSImplies => [
-                                        it.left = createVLSFunction => [
-                                                it.constant = support.toIDMultiple("rel", r.name)
-
-                                                for (i : 0 ..< r.parameters.length) {
-                                                        val v = createVLSVariable => [
-                                                                it.name = relVar2VLS.get(i).name
-                                                        ]
-                                                        it.terms += v
+                                        val rel = createVLSFunction => [
+                                                it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2))
+                                                for (v : relVar2VLS) {
+                                                        it.terms += support.duplicate(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
-        //TODO Make more general
+        // Term Handling
+        // 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 (t2 : terms.subList(0, terms.indexOf(t1))){
+                for (t1 : terms.subList(1, terms.length)) {
+                        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,
-                QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+        def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper,
+                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 => [
-                                it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
-                                it.terms += createVLSVariable => [
-                                        it.name = toIDMultiple("Var", variable.name)
-                                ]
-
-                        ]
+                        val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), variable.lookup(variableMap))
                         typedefs.add(eq)
                 }
-
-                createVLSUniversalQuantifier => [
-                        it.variables += variableMap.values
-                        it.operand = createVLSImplies => [
-                                it.left = unfoldAnd(typedefs)
-                                it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))
+                if (isUniversal) {
+                        createVLSUniversalQuantifier => [
+                                it.variables += variableMap.values
+                                it.operand = createVLSImplies => [
+                                        it.left = unfoldAnd(typedefs)
+                                        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)]
         }
-        
-        
 
 }