diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner')
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 { | |||
238 | def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, | 238 | def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, |
239 | Map<Variable, VLSVariable> variables) { | 239 | Map<Variable, VLSVariable> variables) { |
240 | return createVLSFunction => [ | 240 | return createVLSFunction => [ |
241 | it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name) | 241 | it.constant = support.toIDMultiple("t", (instanceOf.range as ComplexTypeReference).referred.name) |
242 | it.terms += instanceOf.value.transformTerm(trace, variables) | 242 | it.terms += instanceOf.value.transformTerm(trace, variables) |
243 | ] | 243 | ] |
244 | } | 244 | } |
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 { | |||
39 | relationVar2VLS.put(variable, v) | 39 | relationVar2VLS.put(variable, v) |
40 | 40 | ||
41 | val varTypeComply = createVLSFunction => [ | 41 | val varTypeComply = createVLSFunction => [ |
42 | it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | 42 | it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) |
43 | it.terms += createVLSVariable => [ | 43 | it.terms += createVLSVariable => [ |
44 | it.name = support.toIDMultiple("Var", variable.name) | 44 | it.name = support.toIDMultiple("Var", variable.name) |
45 | ] | 45 | ] |
@@ -47,7 +47,7 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
47 | relationVar2TypeDecComply.put(variable, varTypeComply) | 47 | relationVar2TypeDecComply.put(variable, varTypeComply) |
48 | 48 | ||
49 | val varTypeRes = createVLSFunction => [ | 49 | val varTypeRes = createVLSFunction => [ |
50 | it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | 50 | it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) |
51 | it.terms += createVLSVariable => [ | 51 | it.terms += createVLSVariable => [ |
52 | it.name = support.toIDMultiple("Var", variable.name) | 52 | it.name = support.toIDMultiple("Var", variable.name) |
53 | ] | 53 | ] |
@@ -136,7 +136,7 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
136 | relationVar2VLS.add(v) | 136 | relationVar2VLS.add(v) |
137 | 137 | ||
138 | val varTypeComply = createVLSFunction => [ | 138 | val varTypeComply = createVLSFunction => [ |
139 | it.constant = support.toIDMultiple("type", (r.parameters.get(i) as ComplexTypeReference).referred.name) | 139 | it.constant = support.toIDMultiple("t", (r.parameters.get(i) as ComplexTypeReference).referred.name) |
140 | it.terms += createVLSVariable => [ | 140 | it.terms += createVLSVariable => [ |
141 | it.name = support.toIDMultiple("Var", i.toString) | 141 | it.name = support.toIDMultiple("Var", i.toString) |
142 | ] | 142 | ] |
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 { | |||
18 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { | 18 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { |
19 | val VLSVariable variable = createVLSVariable => [it.name = "A"] | 19 | val VLSVariable variable = createVLSVariable => [it.name = "A"] |
20 | 20 | ||
21 | |||
22 | // 1. make a list of constants equaling the min number of specified objects | 21 | // 1. make a list of constants equaling the min number of specified objects |
23 | val List<VLSConstant> instances = newArrayList | 22 | val List<VLSConstant> instances = newArrayList |
24 | for (var i = 0; i < config.typeScopes.minNewElements; i++) { | 23 | for (var i = 0; i < config.typeScopes.minNewElements; i++) { |
@@ -28,47 +27,37 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
28 | ] | 27 | ] |
29 | instances.add(cst) | 28 | instances.add(cst) |
30 | } | 29 | } |
31 | |||
32 | |||
33 | // TODO: specify for the max | ||
34 | |||
35 | 30 | ||
36 | // 2. Create initial fof formula to specify the number of elems | 31 | // TODO: specify for the max |
37 | val cstDec = createVLSFofFormula => [ | 32 | if (config.typeScopes.minNewElements != 0) { |
38 | it.name = "typeScope" | 33 | // 2. Create initial fof formula to specify the number of elems |
39 | it.fofRole = "axiom" | 34 | val cstDec = createVLSFofFormula => [ |
40 | it.fofFormula = createVLSUniversalQuantifier => [ | 35 | it.name = "typeScope" |
41 | it.variables += support.duplicate(variable) | 36 | it.fofRole = "axiom" |
42 | // check below | 37 | it.fofFormula = createVLSUniversalQuantifier => [ |
43 | it.operand = createVLSEquivalent => [ | 38 | it.variables += support.duplicate(variable) |
44 | it.left = support.topLevelTypeFunc | 39 | // check below |
45 | it.right = support.unfoldOr(instances.map [ i | | 40 | it.operand = createVLSEquivalent => [ |
46 | createVLSEquality => [ | 41 | it.left = support.topLevelTypeFunc |
47 | it.left = createVLSVariable => [it.name = variable.name] | 42 | it.right = support.unfoldOr(instances.map [ i | |
48 | it.right = i | 43 | createVLSEquality => [ |
49 | ] | 44 | it.left = createVLSVariable => [it.name = variable.name] |
50 | ]) | 45 | it.right = i |
46 | ] | ||
47 | ]) | ||
48 | ] | ||
51 | ] | 49 | ] |
52 | ] | 50 | ] |
53 | ] | 51 | trace.specification.formulas += cstDec |
54 | trace.specification.formulas += cstDec | 52 | |
55 | 53 | // TODO: specify for scope per type | |
56 | 54 | // 3. Specify uniqueness of elements | |
57 | // TODO: specify for scope per type | 55 | val uniqueness = createVLSFofFormula => [ |
58 | 56 | it.name = "typeUniqueness" | |
59 | 57 | it.fofRole = "axiom" | |
60 | 58 | it.fofFormula = support.establishUniqueness(instances) | |
61 | // 3. Specify uniqueness of elements | 59 | ] |
62 | val uniqueness = createVLSFofFormula => [ | 60 | trace.specification.formulas += uniqueness |
63 | it.name = "typeUniqueness" | 61 | } |
64 | it.fofRole = "axiom" | ||
65 | it.fofFormula = support.unfoldOr(instances.map [ i | | ||
66 | createVLSEquality => [ | ||
67 | it.left = createVLSVariable => [it.name = variable.name] | ||
68 | it.right = i | ||
69 | ] | ||
70 | ]) | ||
71 | ] | ||
72 | trace.specification.formulas += cstDec | ||
73 | } | 62 | } |
74 | } | 63 | } |
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 | |||
13 | import java.util.List | 13 | import java.util.List |
14 | import java.util.Map | 14 | import java.util.Map |
15 | import org.eclipse.emf.common.util.EList | 15 | import org.eclipse.emf.common.util.EList |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality | ||
16 | 18 | ||
17 | class Logic2VampireLanguageMapper_Support { | 19 | class Logic2VampireLanguageMapper_Support { |
18 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 20 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -26,6 +28,7 @@ class Logic2VampireLanguageMapper_Support { | |||
26 | ids.split("\\s+").join("_") | 28 | ids.split("\\s+").join("_") |
27 | } | 29 | } |
28 | 30 | ||
31 | //TODO Make more general | ||
29 | def protected VLSVariable duplicate(VLSVariable vrbl) { | 32 | def protected VLSVariable duplicate(VLSVariable vrbl) { |
30 | return createVLSVariable => [it.name = vrbl.name] | 33 | return createVLSVariable => [it.name = vrbl.name] |
31 | } | 34 | } |
@@ -38,6 +41,25 @@ class Logic2VampireLanguageMapper_Support { | |||
38 | ] | 41 | ] |
39 | ] | 42 | ] |
40 | } | 43 | } |
44 | |||
45 | //TODO Make more general | ||
46 | def establishUniqueness(List<VLSConstant> terms) { | ||
47 | val List<VLSInequality> eqs = newArrayList | ||
48 | for (t1 : terms.subList(1, terms.length)){ | ||
49 | for (t2 : terms.subList(0, terms.indexOf(t1))){ | ||
50 | val eq = createVLSInequality => [ | ||
51 | //TEMP | ||
52 | it.left = createVLSConstant => [it.name = t2.name] | ||
53 | it.right = createVLSConstant => [it.name = t1.name] | ||
54 | //TEMP | ||
55 | ] | ||
56 | eqs.add(eq) | ||
57 | } | ||
58 | } | ||
59 | |||
60 | return unfoldAnd(eqs) | ||
61 | |||
62 | } | ||
41 | 63 | ||
42 | // Support Functions | 64 | // Support Functions |
43 | // booleans | 65 | // booleans |
@@ -111,7 +133,7 @@ class Logic2VampireLanguageMapper_Support { | |||
111 | val typedefs = new ArrayList<VLSTerm> | 133 | val typedefs = new ArrayList<VLSTerm> |
112 | for (variable : expression.quantifiedVariables) { | 134 | for (variable : expression.quantifiedVariables) { |
113 | val eq = createVLSFunction => [ | 135 | val eq = createVLSFunction => [ |
114 | it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | 136 | it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) |
115 | it.terms += createVLSVariable => [ | 137 | it.terms += createVLSVariable => [ |
116 | it.name = toIDMultiple("Var", variable.name) | 138 | it.name = toIDMultiple("Var", variable.name) |
117 | ] | 139 | ] |
@@ -138,7 +160,7 @@ class Logic2VampireLanguageMapper_Support { | |||
138 | val typedefs = new ArrayList<VLSTerm> | 160 | val typedefs = new ArrayList<VLSTerm> |
139 | for (variable : expression.quantifiedVariables) { | 161 | for (variable : expression.quantifiedVariables) { |
140 | val eq = createVLSFunction => [ | 162 | val eq = createVLSFunction => [ |
141 | it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | 163 | it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) |
142 | it.terms += createVLSVariable => [ | 164 | it.terms += createVLSVariable => [ |
143 | it.name = toIDMultiple("Var", variable.name) | 165 | it.name = toIDMultiple("Var", variable.name) |
144 | ] | 166 | ] |
@@ -157,5 +179,7 @@ class Logic2VampireLanguageMapper_Support { | |||
157 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { | 179 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { |
158 | new HashMap(map1) => [putAll(map2)] | 180 | new HashMap(map1) => [putAll(map2)] |
159 | } | 181 | } |
182 | |||
183 | |||
160 | 184 | ||
161 | } | 185 | } |
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 | |||
89 | 89 | ||
90 | // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates | 90 | // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates |
91 | // and store in a map | 91 | // and store in a map |
92 | // val List<VLSTerm> type2PossibleNot = new ArrayList | 92 | for (t1 : types.filter[!isIsAbstract]) { |
93 | // val List<VLSTerm> type2And = new ArrayList | 93 | for (t2 : types) { |
94 | for (type : types.filter[!isIsAbstract]) { | ||
95 | for (type2 : types) { | ||
96 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes | 94 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes |
97 | if (type == type2 || dfsSupertypeCheck(type, type2)) { | 95 | if (t1 == t2 || dfsSupertypeCheck(t1, t2)) { |
98 | typeTrace.type2PossibleNot.put(type2, createVLSFunction => [ | 96 | typeTrace.type2PossibleNot.put(t2, createVLSFunction => [ |
99 | it.constant = type2.lookup(typeTrace.type2Predicate).constant | 97 | it.constant = t2.lookup(typeTrace.type2Predicate).constant |
100 | it.terms += createVLSVariable => [it.name = "A"] | 98 | it.terms += support.duplicate(variable) |
101 | ]) | 99 | ]) |
102 | } else { | 100 | } else { |
103 | typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [ | 101 | typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ |
104 | it.operand = createVLSFunction => [ | 102 | it.operand = createVLSFunction => [ |
105 | it.constant = type2.lookup(typeTrace.type2Predicate).constant | 103 | it.constant = t2.lookup(typeTrace.type2Predicate).constant |
106 | it.terms += createVLSVariable => [it.name = "A"] | 104 | it.terms += support.duplicate(variable) |
107 | ] | 105 | ] |
108 | ]) | 106 | ]) |
109 | } | 107 | } |
110 | // typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate)) | 108 | // typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate)) |
111 | } | 109 | } |
112 | typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values))) | 110 | typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values))) |
113 | // typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) ) | 111 | // typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) ) |
114 | typeTrace.type2PossibleNot.clear | 112 | typeTrace.type2PossibleNot.clear |
115 | } | 113 | } |
@@ -123,7 +121,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp | |||
123 | it.name = "hierarchyHandler" | 121 | it.name = "hierarchyHandler" |
124 | it.fofRole = "axiom" | 122 | it.fofRole = "axiom" |
125 | it.fofFormula = createVLSUniversalQuantifier => [ | 123 | it.fofFormula = createVLSUniversalQuantifier => [ |
126 | it.variables += createVLSVariable => [it.name = "A"] | 124 | it.variables += support.duplicate(variable) |
127 | it.operand = createVLSEquivalent => [ | 125 | it.operand = createVLSEquivalent => [ |
128 | it.left = support.topLevelTypeFunc | 126 | it.left = support.topLevelTypeFunc |
129 | it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values)) | 127 | it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values)) |