1 files changed, 25 insertions, 46 deletions
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 88e1e23a..ea72940e 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
@@ -22,21 +22,20 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                LogicproblemPackage.eINSTANCE.class
        }
-        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements,
+        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
-                Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
+                
-                val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
+//              val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
-                trace.typeMapperTrace = typeTrace
+//              trace.typeMapperTrace = typeTrace
-                // The variable
                val VLSVariable variable = createVLSVariable => [it.name = "A"]
                // 1. Each type (class) is a predicate with a single variable as input
                for (type : types) {
                        val typePred = createVLSFunction => [
-                                it.constant = support.toIDMultiple("t", type.name)
+                                it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
                                it.terms += support.duplicate(variable)
                        ]
-                        typeTrace.type2Predicate.put(type, typePred)
+//                      typeTrace.type2Predicate.put(type, typePred)
+                        trace.type2Predicate.put(type, typePred)
                }
                // 2. Map each ENUM type definition to fof formula
@@ -44,15 +43,16 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                        val List<VLSFunction> orElems = newArrayList
                        for (e : type.elements) {
                                val enumElemPred = createVLSFunction => [
-                                        it.constant = support.toIDMultiple("e", e.name, type.name)
+                                        it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2))
                                        it.terms += support.duplicate(variable)
                                ]
-                                typeTrace.element2Predicate.put(e, enumElemPred)
+//                              typeTrace.element2Predicate.put(e, enumElemPred)
+                                trace.element2Predicate.put(e, enumElemPred)
                                orElems.add(enumElemPred)
                        }
                        val res = createVLSFofFormula => [
-                                it.name = support.toIDMultiple("typeDef", type.name)
+                                it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
                                // below is temporary solution
                                it.fofRole = "axiom"
                                it.fofFormula = createVLSUniversalQuantifier => [
@@ -62,7 +62,8 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
 //                                                      it.constant = type.lookup(typeTrace.type2Predicate).constant
 //                                                      it.terms += createVLSVariable => [it.name = "A"]
 //                                              ]
-                                                it.left = type.lookup(typeTrace.type2Predicate)
+//                                              it.left = type.lookup(typeTrace.type2Predicate)
+                                                it.left = type.lookup(trace.type2Predicate)
                                                it.right = support.unfoldOr(orElems)
@@ -92,31 +93,23 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                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 (t1 == t2 || dfsSupertypeCheck(t1, t2)) {
+                                if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
-                                        typeTrace.type2PossibleNot.put(t2, createVLSFunction => [
+//                                      typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate)))
-                                                it.constant = t2.lookup(typeTrace.type2Predicate).constant
+                                        trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
-                                                it.terms += support.duplicate(variable)
-                                        ])
                                } else {
-                                        typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
+//                                      typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
-                                                it.operand = createVLSFunction => [
+                                        trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
-                                                        it.constant = t2.lookup(typeTrace.type2Predicate).constant
+                                                it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
-                                                        it.terms += support.duplicate(variable)
-                                                ]
                                        ])
                                }
-//                              typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate))
                        }
-                        typeTrace.type2And.put(t1, 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
-                        typeTrace.type2PossibleNot.clear
+                        trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values)))
+                        trace.type2PossibleNot.clear
                }
                // 5. create fof function that is an or with all the elements in map
-                
-                
-                
-                
                val hierarch = createVLSFofFormula => [
                        it.name = "hierarchyHandler"
                        it.fofRole = "axiom"
@@ -124,7 +117,8 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                                it.variables += support.duplicate(variable)
                                it.operand = createVLSEquivalent => [
                                        it.left = support.topLevelTypeFunc
-                                        it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
+//                                      it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
+                                        it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values))
                                ]
                        ]
                ]
@@ -133,21 +127,6 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
        }
-        def boolean dfsSupertypeCheck(Type type, Type type2) {
-                // There is surely a better way to do this
-                if (type.supertypes.isEmpty)
-                        return false
-                else {
-                        if (type.supertypes.contains(type2))
-                                return true
-                        else {
-                                for (supertype : type.supertypes) {
-                                        if(dfsSupertypeCheck(supertype, type2)) return true
-                                }
-                        }
-                }
-        }
        override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
                Logic2VampireLanguageMapperTrace trace) {
                throw new UnsupportedOperationException("TODO: auto-generated method stub")

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 88e1e23a..ea72940e 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
@@ -22,21 +22,20 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
22	LogicproblemPackage.eINSTANCE.class	22	LogicproblemPackage.eINSTANCE.class
23	}	23	}
24		24
25	override transformTypes(Collection<Type> types, Collection<DefinedElement> elements,	25	override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
26	Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {	26
27	val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes	27	// val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
28	trace.typeMapperTrace = typeTrace	28	// trace.typeMapperTrace = typeTrace
29
30	// The variable
31	val VLSVariable variable = createVLSVariable => [it.name = "A"]	29	val VLSVariable variable = createVLSVariable => [it.name = "A"]
32		30
33	// 1. Each type (class) is a predicate with a single variable as input	31	// 1. Each type (class) is a predicate with a single variable as input
34	for (type : types) {	32	for (type : types) {
35	val typePred = createVLSFunction => [	33	val typePred = createVLSFunction => [
36	it.constant = support.toIDMultiple("t", type.name)	34	it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
37	it.terms += support.duplicate(variable)	35	it.terms += support.duplicate(variable)
38	]	36	]
39	typeTrace.type2Predicate.put(type, typePred)	37	// typeTrace.type2Predicate.put(type, typePred)
		38	trace.type2Predicate.put(type, typePred)
40	}	39	}
41		40
42	// 2. Map each ENUM type definition to fof formula	41	// 2. Map each ENUM type definition to fof formula
@@ -44,15 +43,16 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
44	val List<VLSFunction> orElems = newArrayList	43	val List<VLSFunction> orElems = newArrayList
45	for (e : type.elements) {	44	for (e : type.elements) {
46	val enumElemPred = createVLSFunction => [	45	val enumElemPred = createVLSFunction => [
47	it.constant = support.toIDMultiple("e", e.name, type.name)	46	it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2))
48	it.terms += support.duplicate(variable)	47	it.terms += support.duplicate(variable)
49	]	48	]
50	typeTrace.element2Predicate.put(e, enumElemPred)	49	// typeTrace.element2Predicate.put(e, enumElemPred)
		50	trace.element2Predicate.put(e, enumElemPred)
51	orElems.add(enumElemPred)	51	orElems.add(enumElemPred)
52	}	52	}
53		53
54	val res = createVLSFofFormula => [	54	val res = createVLSFofFormula => [
55	it.name = support.toIDMultiple("typeDef", type.name)	55	it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
56	// below is temporary solution	56	// below is temporary solution
57	it.fofRole = "axiom"	57	it.fofRole = "axiom"
58	it.fofFormula = createVLSUniversalQuantifier => [	58	it.fofFormula = createVLSUniversalQuantifier => [
@@ -62,7 +62,8 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
62	// it.constant = type.lookup(typeTrace.type2Predicate).constant	62	// it.constant = type.lookup(typeTrace.type2Predicate).constant
63	// it.terms += createVLSVariable => [it.name = "A"]	63	// it.terms += createVLSVariable => [it.name = "A"]
64	// ]	64	// ]
65	it.left = type.lookup(typeTrace.type2Predicate)	65	// it.left = type.lookup(typeTrace.type2Predicate)
		66	it.left = type.lookup(trace.type2Predicate)
66		67
67	it.right = support.unfoldOr(orElems)	68	it.right = support.unfoldOr(orElems)
68		69
@@ -92,31 +93,23 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
92	for (t1 : types.filter[!isIsAbstract]) {	93	for (t1 : types.filter[!isIsAbstract]) {
93	for (t2 : types) {	94	for (t2 : types) {
94	// possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes	95	// possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
95	if (t1 == t2 \|\| dfsSupertypeCheck(t1, t2)) {	96	if (t1 == t2 \|\| support.dfsSupertypeCheck(t1, t2)) {
96	typeTrace.type2PossibleNot.put(t2, createVLSFunction => [	97	// typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate)))
97	it.constant = t2.lookup(typeTrace.type2Predicate).constant	98	trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
98	it.terms += support.duplicate(variable)
99	])
100	} else {	99	} else {
101	typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [	100	// typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
102	it.operand = createVLSFunction => [	101	trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
103	it.constant = t2.lookup(typeTrace.type2Predicate).constant	102	it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
104	it.terms += support.duplicate(variable)
105	]
106	])	103	])
107	}	104	}
108	// typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate))
109	}	105	}
110	typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))	106	// typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
111	// typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) )	107	// typeTrace.type2PossibleNot.clear
112	typeTrace.type2PossibleNot.clear	108	trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values)))
		109	trace.type2PossibleNot.clear
113	}	110	}
114		111
115	// 5. create fof function that is an or with all the elements in map	112	// 5. create fof function that is an or with all the elements in map
116
117
118
119
120	val hierarch = createVLSFofFormula => [	113	val hierarch = createVLSFofFormula => [
121	it.name = "hierarchyHandler"	114	it.name = "hierarchyHandler"
122	it.fofRole = "axiom"	115	it.fofRole = "axiom"
@@ -124,7 +117,8 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
124	it.variables += support.duplicate(variable)	117	it.variables += support.duplicate(variable)
125	it.operand = createVLSEquivalent => [	118	it.operand = createVLSEquivalent => [
126	it.left = support.topLevelTypeFunc	119	it.left = support.topLevelTypeFunc
127	it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))	120	// it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
		121	it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values))
128	]	122	]
129	]	123	]
130	]	124	]
@@ -133,21 +127,6 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
133		127
134	}	128	}
135		129
136	def boolean dfsSupertypeCheck(Type type, Type type2) {
137	// There is surely a better way to do this
138	if (type.supertypes.isEmpty)
139	return false
140	else {
141	if (type.supertypes.contains(type2))
142	return true
143	else {
144	for (supertype : type.supertypes) {
145	if(dfsSupertypeCheck(supertype, type2)) return true
146	}
147	}
148	}
149	}
150
151	override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,	130	override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
152	Logic2VampireLanguageMapperTrace trace) {	131	Logic2VampireLanguageMapperTrace trace) {
153	throw new UnsupportedOperationException("TODO: auto-generated method stub")	132	throw new UnsupportedOperationException("TODO: auto-generated method stub")