diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder')
4 files changed, 157 insertions, 145 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend index 135b3f07..3c672f4b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend | |||
@@ -1,15 +1,17 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula | 3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
13 | import java.util.HashMap | 15 | import java.util.HashMap |
14 | import java.util.Map | 16 | import java.util.Map |
15 | 17 | ||
@@ -22,17 +24,29 @@ class Logic2VampireLanguageMapperTrace { | |||
22 | public var VampireModel specification | 24 | public var VampireModel specification |
23 | public var VLSFofFormula logicLanguageBody | 25 | public var VLSFofFormula logicLanguageBody |
24 | public var VLSTerm formula | 26 | public var VLSTerm formula |
25 | //NOT NEEDED //public var VLSFunction constantDec | ||
26 | 27 | ||
28 | //Necessary containers | ||
27 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace | 29 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace |
28 | 30 | ||
31 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; | ||
32 | public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap | ||
33 | public val Map<Type, VLSTerm> type2PossibleNot = new HashMap | ||
34 | public val Map<Type, VLSTerm> type2And = new HashMap | ||
35 | |||
36 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | ||
37 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | ||
38 | public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap | ||
39 | |||
40 | |||
41 | //NOT NEEDED //public var VLSFunction constantDec | ||
42 | |||
43 | |||
44 | |||
29 | 45 | ||
30 | //NOT NEEDED //public val Map<ConstantDeclaration, VLSFunctionDeclaration> constantDeclaration2LanguageField = new HashMap | 46 | //NOT NEEDED //public val Map<ConstantDeclaration, VLSFunctionDeclaration> constantDeclaration2LanguageField = new HashMap |
31 | //public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap | 47 | //public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap |
32 | 48 | ||
33 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | ||
34 | 49 | ||
35 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | ||
36 | public val Map<Variable, VLSVariable> relationVar2VLS = new HashMap | 50 | public val Map<Variable, VLSVariable> relationVar2VLS = new HashMap |
37 | public val Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap | 51 | public val Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap |
38 | 52 | ||
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 6f3b13ef..23b57701 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 | |||
@@ -24,52 +24,97 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
24 | this.base = base | 24 | this.base = base |
25 | } | 25 | } |
26 | 26 | ||
27 | def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace) { | 27 | def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) { |
28 | 28 | ||
29 | // 1. store all variables in support wrt their name | 29 | // 1. store all variables in support wrt their name |
30 | // 1.1 if variable has type, creating list of type declarations | 30 | // 1.1 if variable has type, creating list of type declarations |
31 | val List<VLSVariable> relVar2VLS = new ArrayList | ||
32 | val List<VLSFunction> relVar2TypeDecComply = new ArrayList | ||
33 | val typedefs = new ArrayList<VLSTerm> | ||
34 | |||
35 | for (i : 0 ..< r.parameters.length) { | ||
36 | |||
37 | val v = createVLSVariable => [ | ||
38 | it.name = support.toIDMultiple("V", i.toString) | ||
39 | ] | ||
40 | relVar2VLS.add(v) | ||
41 | |||
42 | val relType = (r.parameters.get(i) as ComplexTypeReference).referred | ||
43 | val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v) | ||
44 | relVar2TypeDecComply.add(varTypeComply) | ||
45 | |||
46 | } | ||
47 | |||
48 | val comply = createVLSFofFormula => [ | ||
49 | val nameArray = r.name.split(" ") | ||
50 | it.name = support.toIDMultiple("compliance", nameArray.get(0), | ||
51 | nameArray.get(2)) | ||
52 | it.fofRole = "axiom" | ||
53 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
54 | |||
55 | for (v : relVar2VLS) { | ||
56 | it.variables += support.duplicate(v) | ||
57 | } | ||
58 | |||
59 | it.operand = createVLSImplies => [ | ||
60 | it.left = createVLSFunction => [ | ||
61 | it.constant = support.toIDMultiple("rel", r.name) | ||
62 | |||
63 | for (i : 0 ..< r.parameters.length) { | ||
64 | val v = createVLSVariable => [ | ||
65 | it.name = relVar2VLS.get(i).name | ||
66 | ] | ||
67 | it.terms += v | ||
68 | } | ||
69 | |||
70 | ] | ||
71 | it.right = support.unfoldAnd(relVar2TypeDecComply) | ||
72 | ] | ||
73 | ] | ||
74 | ] | ||
75 | |||
76 | // trace.relationDefinition2Predicate.put(r,res) | ||
77 | trace.specification.formulas += comply | ||
78 | } | ||
79 | |||
80 | def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) { | ||
81 | |||
82 | // 1. store all variables in support wrt their name | ||
83 | // 1.1 if variable has type, creating list of type declarations | ||
84 | // val VLSVariable variable = createVLSVariable => [it.name = "A"] | ||
31 | val Map<Variable, VLSVariable> relationVar2VLS = new HashMap | 85 | val Map<Variable, VLSVariable> relationVar2VLS = new HashMap |
32 | val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap | 86 | val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap |
33 | val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap | 87 | val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap |
34 | val typedefs = new ArrayList<VLSTerm> | 88 | val typedefs = new ArrayList<VLSTerm> |
35 | for (variable : r.variables) { | 89 | |
90 | for (variable : reldef.variables) { | ||
36 | val v = createVLSVariable => [ | 91 | val v = createVLSVariable => [ |
37 | it.name = support.toIDMultiple("Var", variable.name) | 92 | it.name = support.toIDMultiple("V", variable.name) |
38 | ] | 93 | ] |
39 | relationVar2VLS.put(variable, v) | 94 | relationVar2VLS.put(variable, v) |
40 | 95 | ||
41 | val varTypeComply = createVLSFunction => [ | 96 | val varTypeComply = createVLSFunction => [ |
42 | it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) | 97 | it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) |
43 | it.terms += createVLSVariable => [ | 98 | it.terms += support.duplicate(v) |
44 | it.name = support.toIDMultiple("Var", variable.name) | ||
45 | ] | ||
46 | ] | 99 | ] |
47 | relationVar2TypeDecComply.put(variable, varTypeComply) | 100 | relationVar2TypeDecComply.put(variable, varTypeComply) |
48 | 101 | relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) | |
49 | val varTypeRes = createVLSFunction => [ | ||
50 | it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) | ||
51 | it.terms += createVLSVariable => [ | ||
52 | it.name = support.toIDMultiple("Var", variable.name) | ||
53 | ] | ||
54 | ] | ||
55 | relationVar2TypeDecRes.put(variable, varTypeRes) | ||
56 | } | 102 | } |
57 | 103 | ||
58 | val comply = createVLSFofFormula => [ | 104 | val comply = createVLSFofFormula => [ |
59 | it.name = support.toIDMultiple("compliance", r.name) | 105 | val nameArray = reldef.name.split(" ") |
106 | it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), | ||
107 | nameArray.get(nameArray.length - 1)) | ||
60 | it.fofRole = "axiom" | 108 | it.fofRole = "axiom" |
61 | it.fofFormula = createVLSUniversalQuantifier => [ | 109 | it.fofFormula = createVLSUniversalQuantifier => [ |
62 | for (variable : r.variables) { | 110 | for (variable : reldef.variables) { |
63 | val v = createVLSVariable => [ | 111 | it.variables += support.duplicate(variable.lookup(relationVar2VLS)) |
64 | it.name = variable.lookup(relationVar2VLS).name | ||
65 | ] | ||
66 | it.variables += v | ||
67 | 112 | ||
68 | } | 113 | } |
69 | it.operand = createVLSImplies => [ | 114 | it.operand = createVLSImplies => [ |
70 | it.left = createVLSFunction => [ | 115 | it.left = createVLSFunction => [ |
71 | it.constant = support.toIDMultiple("rel", r.name) | 116 | it.constant = support.toIDMultiple("rel", reldef.name) |
72 | for (variable : r.variables) { | 117 | for (variable : reldef.variables) { |
73 | val v = createVLSVariable => [ | 118 | val v = createVLSVariable => [ |
74 | it.name = variable.lookup(relationVar2VLS).name | 119 | it.name = variable.lookup(relationVar2VLS).name |
75 | ] | 120 | ] |
@@ -82,10 +127,10 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
82 | ] | 127 | ] |
83 | 128 | ||
84 | val res = createVLSFofFormula => [ | 129 | val res = createVLSFofFormula => [ |
85 | it.name = support.toIDMultiple("relation", r.name) | 130 | it.name = support.toIDMultiple("relation", reldef.name) |
86 | it.fofRole = "axiom" | 131 | it.fofRole = "axiom" |
87 | it.fofFormula = createVLSUniversalQuantifier => [ | 132 | it.fofFormula = createVLSUniversalQuantifier => [ |
88 | for (variable : r.variables) { | 133 | for (variable : reldef.variables) { |
89 | val v = createVLSVariable => [ | 134 | val v = createVLSVariable => [ |
90 | it.name = variable.lookup(relationVar2VLS).name | 135 | it.name = variable.lookup(relationVar2VLS).name |
91 | ] | 136 | ] |
@@ -96,8 +141,8 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
96 | it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values)) | 141 | it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values)) |
97 | it.right = createVLSEquivalent => [ | 142 | it.right = createVLSEquivalent => [ |
98 | it.left = createVLSFunction => [ | 143 | it.left = createVLSFunction => [ |
99 | it.constant = support.toIDMultiple("rel", r.name) | 144 | it.constant = support.toIDMultiple("rel", reldef.name) |
100 | for (variable : r.variables) { | 145 | for (variable : reldef.variables) { |
101 | val v = createVLSVariable => [ | 146 | val v = createVLSVariable => [ |
102 | it.name = variable.lookup(relationVar2VLS).name | 147 | it.name = variable.lookup(relationVar2VLS).name |
103 | ] | 148 | ] |
@@ -105,7 +150,7 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
105 | 150 | ||
106 | } | 151 | } |
107 | ] | 152 | ] |
108 | it.right = base.transformTerm(r.value, trace, relationVar2VLS) | 153 | it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) |
109 | ] | 154 | ] |
110 | 155 | ||
111 | ] | 156 | ] |
@@ -119,65 +164,5 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
119 | trace.specification.formulas += res; | 164 | trace.specification.formulas += res; |
120 | 165 | ||
121 | } | 166 | } |
122 | |||
123 | def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) { | ||
124 | |||
125 | // 1. store all variables in support wrt their name | ||
126 | // 1.1 if variable has type, creating list of type declarations | ||
127 | val List<VLSVariable> relationVar2VLS = new ArrayList | ||
128 | val List<VLSFunction> relationVar2TypeDecComply = new ArrayList | ||
129 | val typedefs = new ArrayList<VLSTerm> | ||
130 | |||
131 | for (i : 0..<r.parameters.length) { | ||
132 | |||
133 | val v = createVLSVariable => [ | ||
134 | it.name = support.toIDMultiple("Var", i.toString) | ||
135 | ] | ||
136 | relationVar2VLS.add(v) | ||
137 | |||
138 | val varTypeComply = createVLSFunction => [ | ||
139 | it.constant = support.toIDMultiple("t", (r.parameters.get(i) as ComplexTypeReference).referred.name) | ||
140 | it.terms += createVLSVariable => [ | ||
141 | it.name = support.toIDMultiple("Var", i.toString) | ||
142 | ] | ||
143 | ] | ||
144 | relationVar2TypeDecComply.add(varTypeComply) | ||
145 | |||
146 | } | ||
147 | |||
148 | |||
149 | val comply = createVLSFofFormula => [ | ||
150 | it.name = support.toIDMultiple("compliance", r.name) | ||
151 | it.fofRole = "axiom" | ||
152 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
153 | |||
154 | for (i : 0..<r.parameters.length) { | ||
155 | val v = createVLSVariable => [ | ||
156 | it.name = relationVar2VLS.get(i).name | ||
157 | ] | ||
158 | it.variables += v | ||
159 | |||
160 | } | ||
161 | |||
162 | it.operand = createVLSImplies => [ | ||
163 | it.left = createVLSFunction => [ | ||
164 | it.constant = support.toIDMultiple("rel", r.name) | ||
165 | |||
166 | for (i : 0..<r.parameters.length) { | ||
167 | val v = createVLSVariable => [ | ||
168 | it.name = relationVar2VLS.get(i).name | ||
169 | ] | ||
170 | it.terms += v | ||
171 | } | ||
172 | |||
173 | ] | ||
174 | it.right = support.unfoldAnd(relationVar2TypeDecComply) | ||
175 | ] | ||
176 | ] | ||
177 | ] | ||
178 | |||
179 | // trace.relationDefinition2Predicate.put(r,res) | ||
180 | trace.specification.formulas += comply | ||
181 | } | ||
182 | 167 | ||
183 | } | 168 | } |
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 06ec585c..090cf916 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 | |||
@@ -1,20 +1,21 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable |
11 | import java.util.ArrayList | 14 | import java.util.ArrayList |
12 | import java.util.HashMap | 15 | import java.util.HashMap |
13 | import java.util.List | 16 | import java.util.List |
14 | import java.util.Map | 17 | import java.util.Map |
15 | import org.eclipse.emf.common.util.EList | 18 | import org.eclipse.emf.common.util.EList |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality | ||
18 | 19 | ||
19 | class Logic2VampireLanguageMapper_Support { | 20 | class Logic2VampireLanguageMapper_Support { |
20 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 21 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -28,10 +29,28 @@ class Logic2VampireLanguageMapper_Support { | |||
28 | ids.split("\\s+").join("_") | 29 | ids.split("\\s+").join("_") |
29 | } | 30 | } |
30 | 31 | ||
32 | //Term Handling | ||
31 | //TODO Make more general | 33 | //TODO Make more general |
32 | def protected VLSVariable duplicate(VLSVariable vrbl) { | 34 | def protected VLSVariable duplicate(VLSVariable term) { |
33 | return createVLSVariable => [it.name = vrbl.name] | 35 | return createVLSVariable => [it.name = term.name] |
36 | } | ||
37 | |||
38 | def protected VLSFunction duplicate(VLSFunction term) { | ||
39 | return createVLSFunction => [ | ||
40 | it.constant = term.constant | ||
41 | for ( v : term.terms){ | ||
42 | it.terms += duplicate(v as VLSVariable) | ||
43 | } | ||
44 | ] | ||
34 | } | 45 | } |
46 | |||
47 | def protected VLSFunction duplicate(VLSFunction term, VLSVariable v) { | ||
48 | return createVLSFunction => [ | ||
49 | it.constant = term.constant | ||
50 | it.terms += duplicate(v) | ||
51 | ] | ||
52 | } | ||
53 | |||
35 | 54 | ||
36 | def protected VLSFunction topLevelTypeFunc() { | 55 | def protected VLSFunction topLevelTypeFunc() { |
37 | return createVLSFunction => [ | 56 | return createVLSFunction => [ |
@@ -175,6 +194,21 @@ class Logic2VampireLanguageMapper_Support { | |||
175 | 194 | ||
176 | ] | 195 | ] |
177 | } | 196 | } |
197 | |||
198 | def protected boolean dfsSupertypeCheck(Type type, Type type2) { | ||
199 | // There is surely a better way to do this | ||
200 | if (type.supertypes.isEmpty) | ||
201 | return false | ||
202 | else { | ||
203 | if (type.supertypes.contains(type2)) | ||
204 | return true | ||
205 | else { | ||
206 | for (supertype : type.supertypes) { | ||
207 | if(dfsSupertypeCheck(supertype, type2)) return true | ||
208 | } | ||
209 | } | ||
210 | } | ||
211 | } | ||
178 | 212 | ||
179 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { | 213 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { |
180 | new HashMap(map1) => [putAll(map2)] | 214 | 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 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") |