Implement type scope handling

5 files changed, 70 insertions, 59 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 e2c15b75..54c44c72 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
@@ -238,7 +238,7 @@ class Logic2VampireLanguageMapper {
         def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> variables) {
                 return createVLSFunction => [
-                        it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name)
+                        it.constant = support.toIDMultiple("t", (instanceOf.range as ComplexTypeReference).referred.name)
                         it.terms += instanceOf.value.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 60653a42..6f3b13ef 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
@@ -39,7 +39,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                         relationVar2VLS.put(variable, v)
 
                         val varTypeComply = createVLSFunction => [
-                                it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = support.toIDMultiple("Var", variable.name)
                                 ]
@@ -47,7 +47,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                         relationVar2TypeDecComply.put(variable, varTypeComply)
                         
                         val varTypeRes = createVLSFunction => [
-                                it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = support.toIDMultiple("Var", variable.name)
                                 ]
@@ -136,7 +136,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                         relationVar2VLS.add(v)
 
                         val varTypeComply = createVLSFunction => [
-                                it.constant = support.toIDMultiple("type", (r.parameters.get(i) as ComplexTypeReference).referred.name)
+                                it.constant = support.toIDMultiple("t", (r.parameters.get(i) as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = support.toIDMultiple("Var", i.toString)
                                 ]
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
index 84aa521d..4b7ea3d0 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -18,7 +18,6 @@ class Logic2VampireLanguageMapper_ScopeMapper {
         def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {

                 val VLSVariable variable = createVLSVariable => [it.name = "A"]

 

-                

                 // 1. make a list of constants equaling the min number of specified objects

                 val List<VLSConstant> instances = newArrayList

                 for (var i = 0; i < config.typeScopes.minNewElements; i++) {

@@ -28,47 +27,37 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                         ]

                         instances.add(cst)

                 }

-                

-                

-                // TODO: specify for the max

-

 

-                // 2. Create initial fof formula to specify the number of elems

-                val cstDec = createVLSFofFormula => [

-                        it.name = "typeScope"

-                        it.fofRole = "axiom"

-                        it.fofFormula = createVLSUniversalQuantifier => [

-                                it.variables += support.duplicate(variable)

-                                // check below

-                                it.operand = createVLSEquivalent => [

-                                        it.left = support.topLevelTypeFunc

-                                        it.right = support.unfoldOr(instances.map [ i |

-                                                createVLSEquality => [

-                                                        it.left = createVLSVariable => [it.name = variable.name]

-                                                        it.right = i

-                                                ]

-                                        ])

+                // TODO: specify for the max

+                if (config.typeScopes.minNewElements != 0) {

+                        // 2. Create initial fof formula to specify the number of elems

+                        val cstDec = createVLSFofFormula => [

+                                it.name = "typeScope"

+                                it.fofRole = "axiom"

+                                it.fofFormula = createVLSUniversalQuantifier => [

+                                        it.variables += support.duplicate(variable)

+                                        // check below

+                                        it.operand = createVLSEquivalent => [

+                                                it.left = support.topLevelTypeFunc

+                                                it.right = support.unfoldOr(instances.map [ i |

+                                                        createVLSEquality => [

+                                                                it.left = createVLSVariable => [it.name = variable.name]

+                                                                it.right = i

+                                                        ]

+                                                ])

+                                        ]

                                 ]

                         ]

-                ]

-                trace.specification.formulas += cstDec

-

-

-                // TODO: specify for scope per type

-

-

-

-                // 3. Specify uniqueness of elements

-                val uniqueness = createVLSFofFormula => [

-                        it.name = "typeUniqueness"

-                        it.fofRole = "axiom"

-                        it.fofFormula = support.unfoldOr(instances.map [ i |

-                                createVLSEquality => [

-                                        it.left = createVLSVariable => [it.name = variable.name]

-                                        it.right = i

-                                ]

-                        ])

-                ]

-                trace.specification.formulas += cstDec

+                        trace.specification.formulas += cstDec

+

+                        // TODO: specify for scope per type

+                        // 3. Specify uniqueness of elements

+                        val uniqueness = createVLSFofFormula => [

+                                it.name = "typeUniqueness"

+                                it.fofRole = "axiom"

+                                it.fofFormula = support.establishUniqueness(instances)

+                        ]

+                        trace.specification.formulas += uniqueness

+                }

         }

 }

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 e69f0d51..06ec585c 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
@@ -13,6 +13,8 @@ import java.util.HashMap
 import java.util.List
 import java.util.Map
 import org.eclipse.emf.common.util.EList
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality
 
 class Logic2VampireLanguageMapper_Support {
         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -26,6 +28,7 @@ class Logic2VampireLanguageMapper_Support {
                 ids.split("\\s+").join("_")
         }
 
+        //TODO Make more general
         def protected VLSVariable duplicate(VLSVariable vrbl) {
                 return createVLSVariable => [it.name = vrbl.name]
         }
@@ -38,6 +41,25 @@ class Logic2VampireLanguageMapper_Support {
                         ]
                 ]
         }
+        
+        //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))){
+                                val eq = createVLSInequality => [
+                                        //TEMP
+                                        it.left = createVLSConstant => [it.name = t2.name]
+                                        it.right = createVLSConstant => [it.name = t1.name]
+                                        //TEMP
+                                ]
+                                eqs.add(eq)
+                        }                       
+                }
+                
+                return unfoldAnd(eqs)
+                
+        }
 
         // Support Functions
         // booleans
@@ -111,7 +133,7 @@ class Logic2VampireLanguageMapper_Support {
                 val typedefs = new ArrayList<VLSTerm>
                 for (variable : expression.quantifiedVariables) {
                         val eq = createVLSFunction => [
-                                it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = toIDMultiple("Var", variable.name)
                                 ]
@@ -138,7 +160,7 @@ class Logic2VampireLanguageMapper_Support {
                 val typedefs = new ArrayList<VLSTerm>
                 for (variable : expression.quantifiedVariables) {
                         val eq = createVLSFunction => [
-                                it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = toIDMultiple("Var", variable.name)
                                 ]
@@ -157,5 +179,7 @@ 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/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
index eed10656..88e1e23a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -89,27 +89,25 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                 
                 // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
                 // and store in a map
-//              val List<VLSTerm> type2PossibleNot = new ArrayList
-//              val List<VLSTerm> type2And = new ArrayList
-                for (type : types.filter[!isIsAbstract]) {
-                        for (type2 : types) {
+                for (t1 : types.filter[!isIsAbstract]) {
+                        for (t2 : types) {
                                 // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
-                                if (type == type2 || dfsSupertypeCheck(type, type2)) {
-                                        typeTrace.type2PossibleNot.put(type2, createVLSFunction => [
-                                                it.constant = type2.lookup(typeTrace.type2Predicate).constant
-                                                it.terms += createVLSVariable => [it.name = "A"]
+                                if (t1 == t2 || dfsSupertypeCheck(t1, t2)) {
+                                        typeTrace.type2PossibleNot.put(t2, createVLSFunction => [
+                                                it.constant = t2.lookup(typeTrace.type2Predicate).constant
+                                                it.terms += support.duplicate(variable)
                                         ])
                                 } else {
-                                        typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [
+                                        typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
                                                 it.operand = createVLSFunction => [
-                                                        it.constant = type2.lookup(typeTrace.type2Predicate).constant
-                                                        it.terms += createVLSVariable => [it.name = "A"]
+                                                        it.constant = t2.lookup(typeTrace.type2Predicate).constant
+                                                        it.terms += support.duplicate(variable)
                                                 ]
                                         ])
                                 }
 //                              typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate))
                         }
-                        typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
+                        typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
 //                      typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) )
                         typeTrace.type2PossibleNot.clear
                 }
@@ -123,7 +121,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                         it.name = "hierarchyHandler"
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
-                                it.variables += createVLSVariable => [it.name = "A"]
+                                it.variables += support.duplicate(variable)
                                 it.operand = createVLSEquivalent => [
                                         it.left = support.topLevelTypeFunc
                                         it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))