diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-14 03:45:46 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:22:51 -0400 |
commit | d7730cb0d684d6324622021a310d9b4a53e7531c (patch) | |
tree | b631b8c666448b948bdf670fbf5ad7c2277496dd /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder | |
parent | Implement type scope for specific types (diff) | |
download | VIATRA-Generator-d7730cb0d684d6324622021a310d9b4a53e7531c.tar.gz VIATRA-Generator-d7730cb0d684d6324622021a310d9b4a53e7531c.tar.zst VIATRA-Generator-d7730cb0d684d6324622021a310d9b4a53e7531c.zip |
Implement Containment mapping (partially) and revisit enum mapping
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder')
5 files changed, 233 insertions, 65 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 1dbc0055..b7ad8f3d 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 | |||
@@ -47,6 +47,8 @@ class Logic2VampireLanguageMapper { | |||
47 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support; | 47 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support; |
48 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper( | 48 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper( |
49 | this) | 49 | this) |
50 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper( | ||
51 | this) | ||
50 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( | 52 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( |
51 | this) | 53 | this) |
52 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper( | 54 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper( |
@@ -80,24 +82,26 @@ class Logic2VampireLanguageMapper { | |||
80 | // SCOPE MAPPER | 82 | // SCOPE MAPPER |
81 | scopeMapper.transformScope(config, trace) | 83 | scopeMapper.transformScope(config, trace) |
82 | 84 | ||
83 | trace.constantDefinitions = problem.collectConstantDefinitions | 85 | // RELATION MAPPER |
84 | trace.relationDefinitions = problem.collectRelationDefinitions | 86 | trace.relationDefinitions = problem.collectRelationDefinitions |
85 | |||
86 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] | 87 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] |
88 | |||
89 | // CONTAINMENT MAPPER | ||
90 | containmentMapper.transformContainment(problem.containmentHierarchies, trace) | ||
87 | 91 | ||
92 | // CONSTANT MAPPER | ||
88 | // only transforms definitions | 93 | // only transforms definitions |
94 | trace.constantDefinitions = problem.collectConstantDefinitions | ||
89 | // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)] | 95 | // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)] |
90 | problem.constants.filter(ConstantDefinition).forEach [ | 96 | problem.constants.filter(ConstantDefinition).forEach [ |
91 | this.constantMapper.transformConstantDefinitionSpecification(it, trace) | 97 | this.constantMapper.transformConstantDefinitionSpecification(it, trace) |
92 | ] | 98 | ] |
93 | 99 | ||
94 | // ////////////////// | 100 | // ASSERTION MAPPER |
95 | // Transform Assertions | ||
96 | // ////////////////// | ||
97 | for (assertion : problem.assertions) { | 101 | for (assertion : problem.assertions) { |
98 | transformAssertion(assertion, trace) | 102 | transformAssertion(assertion, trace) |
99 | } | 103 | } |
100 | 104 | // OUTPUT | |
101 | return new TracedOutput(specification, trace) | 105 | return new TracedOutput(specification, trace) |
102 | } | 106 | } |
103 | 107 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend new file mode 100644 index 00000000..0820f47d --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend | |||
@@ -0,0 +1,123 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy | ||
7 | import java.util.List | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
10 | |||
11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
14 | |||
15 | class Logic2VampireLanguageMapper_ContainmentMapper { | ||
16 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
17 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | ||
18 | val Logic2VampireLanguageMapper base | ||
19 | private val VLSVariable variable = createVLSVariable => [it.name = "A"] | ||
20 | |||
21 | public new(Logic2VampireLanguageMapper base) { | ||
22 | this.base = base | ||
23 | } | ||
24 | |||
25 | def public void transformContainment(List<ContainmentHierarchy> hierarchies, | ||
26 | Logic2VampireLanguageMapperTrace trace) { | ||
27 | |||
28 | // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST | ||
29 | // TEMP | ||
30 | val hierarchy = hierarchies.get(0) | ||
31 | |||
32 | val containmentListCopy = hierarchy.typesOrderedInHierarchy | ||
33 | val relationsList = hierarchy.containmentRelations | ||
34 | // STEP 1 | ||
35 | // Find root element | ||
36 | for (l : relationsList) { | ||
37 | var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type | ||
38 | containmentListCopy.remove(pointingTo) | ||
39 | for (c : pointingTo.subtypes) { | ||
40 | containmentListCopy.remove(c) | ||
41 | } | ||
42 | } | ||
43 | |||
44 | // State that there must exist 1 and only 1 root element | ||
45 | val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString | ||
46 | val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) | ||
47 | |||
48 | val contTop = createVLSFofFormula => [ | ||
49 | it.name = support.toIDMultiple("containment_topLevel", topName) | ||
50 | it.fofRole = "axiom" | ||
51 | |||
52 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
53 | it.variables += support.duplicate(variable) | ||
54 | it.operand = createVLSEquivalent => [ | ||
55 | it.left = topTerm | ||
56 | it.right = createVLSEquality => [ | ||
57 | it.left = support.duplicate(variable) | ||
58 | it.right = createVLSConstant => [ | ||
59 | it.name = "o1" | ||
60 | ] | ||
61 | ] | ||
62 | ] | ||
63 | ] | ||
64 | // it.fofFormula = support.duplicate( | ||
65 | // topTerm, | ||
66 | // createVLSFunctionAsTerm => [ | ||
67 | // it.functor = "o1" | ||
68 | // ] | ||
69 | // ) | ||
70 | ] | ||
71 | trace.specification.formulas += contTop | ||
72 | |||
73 | // STEP 2 | ||
74 | // for each edge, if the pointedTo element exists,the edge must exist also | ||
75 | val varA = createVLSVariable => [it.name = "A"] | ||
76 | val varB = createVLSVariable => [it.name = "B"] | ||
77 | val varList = newArrayList(varB, varA) | ||
78 | |||
79 | for (l : relationsList) { | ||
80 | val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString | ||
81 | val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type | ||
82 | val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type | ||
83 | |||
84 | val relFormula = createVLSFofFormula => [ | ||
85 | it.name = support.toIDMultiple("containment", relName) | ||
86 | it.fofRole = "axiom" | ||
87 | |||
88 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
89 | it.variables += support.duplicate(varA) | ||
90 | it.operand = createVLSImplies => [ | ||
91 | it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA) | ||
92 | it.right = createVLSExistentialQuantifier => [ | ||
93 | it.variables += support.duplicate(varB) | ||
94 | it.operand = createVLSAnd => [ | ||
95 | it.left = support.duplicate(fromType.lookup(trace.type2Predicate), varB) | ||
96 | it.right = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), | ||
97 | varList) | ||
98 | ] | ||
99 | ] | ||
100 | |||
101 | createVLSEquality => [ | ||
102 | it.left = support.duplicate(variable) | ||
103 | it.right = createVLSConstant => [ | ||
104 | it.name = "o1" | ||
105 | ] | ||
106 | ] | ||
107 | ] | ||
108 | ] | ||
109 | ] | ||
110 | trace.specification.formulas += relFormula | ||
111 | var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type | ||
112 | containmentListCopy.remove(pointingTo) | ||
113 | for (c : pointingTo.subtypes) { | ||
114 | containmentListCopy.remove(c) | ||
115 | } | ||
116 | } | ||
117 | |||
118 | // STEP 3 | ||
119 | // Ensure that an objct only has 1 parent | ||
120 | // STEP 4 | ||
121 | // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) | ||
122 | } | ||
123 | } | ||
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 5c5eaff3..548deda4 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 | |||
@@ -10,6 +10,8 @@ import java.util.Map | |||
10 | 10 | ||
11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
12 | import java.util.HashMap | 12 | import java.util.HashMap |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
14 | import java.util.List | ||
13 | 15 | ||
14 | class Logic2VampireLanguageMapper_ScopeMapper { | 16 | class Logic2VampireLanguageMapper_ScopeMapper { |
15 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 17 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -24,7 +26,8 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
24 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { | 26 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { |
25 | 27 | ||
26 | // TODO HANDLE ERRORS RELATED TO MAX > MIN | 28 | // TODO HANDLE ERRORS RELATED TO MAX > MIN |
27 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS | 29 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS |
30 | // TODO HANDLE | ||
28 | // TODO NOT SPECIFIED MEANS =0 ? | 31 | // TODO NOT SPECIFIED MEANS =0 ? |
29 | // 1. make a list of constants equaling the min number of specified objects | 32 | // 1. make a list of constants equaling the min number of specified objects |
30 | val GLOBAL_MIN = config.typeScopes.minNewElements | 33 | val GLOBAL_MIN = config.typeScopes.minNewElements |
@@ -34,18 +37,22 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
34 | 37 | ||
35 | // Handling Minimum_General | 38 | // Handling Minimum_General |
36 | if (GLOBAL_MIN != 0) { | 39 | if (GLOBAL_MIN != 0) { |
37 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) // fix last param | 40 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) |
41 | for(i : trace.uniqueInstances){ | ||
42 | localInstances.add(support.duplicate(i)) | ||
43 | } | ||
44 | |||
38 | makeFofFormula(localInstances, trace, true, null) | 45 | makeFofFormula(localInstances, trace, true, null) |
39 | } | 46 | } |
40 | 47 | ||
41 | // Handling Maximum_General | 48 | // Handling Maximum_General |
42 | if (GLOBAL_MAX != 0) { | 49 | if (GLOBAL_MAX != 0) { |
43 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) // fix last param | 50 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) |
44 | makeFofFormula(localInstances, trace, false, null) | 51 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) |
45 | } | 52 | } |
46 | 53 | ||
47 | // Handling Minimum_Specific | 54 | // Handling Minimum_Specific |
48 | var i = 0 | 55 | var i = 1 |
49 | var minNum = -1 | 56 | var minNum = -1 |
50 | var Map<Type, Integer> startPoints = new HashMap | 57 | var Map<Type, Integer> startPoints = new HashMap |
51 | for (t : config.typeScopes.minNewElementsByType.keySet) { | 58 | for (t : config.typeScopes.minNewElementsByType.keySet) { |
@@ -106,13 +113,17 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
106 | def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, | 113 | def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, |
107 | Type type) { | 114 | Type type) { |
108 | var nm = "" | 115 | var nm = "" |
109 | var VLSFunction tm = null | 116 | var VLSTerm tm = null |
110 | if (type === null) { | 117 | if (type === null) { |
111 | nm = "object" | 118 | nm = "object" |
112 | tm = support.topLevelTypeFunc | 119 | tm = support.topLevelTypeFunc |
113 | } else { | 120 | } else { |
114 | nm = type.lookup(trace.type2Predicate).constant.toString | 121 | nm = type.lookup(trace.type2Predicate).constant.toString |
115 | tm = support.duplicate(type.lookup(trace.type2Predicate)) | 122 | tm = createVLSAnd => [ |
123 | it.left = support.duplicate(type.lookup(trace.type2Predicate)) | ||
124 | it.right = support.topLevelTypeFunc | ||
125 | ] | ||
126 | // tm = support.duplicate(type.lookup(trace.type2Predicate)) | ||
116 | } | 127 | } |
117 | val name = nm | 128 | val name = nm |
118 | val term = tm | 129 | val term = tm |
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 021cb0ea..8d00d3e7 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 | |||
@@ -37,11 +37,11 @@ class Logic2VampireLanguageMapper_Support { | |||
37 | def protected VLSVariable duplicate(VLSVariable term) { | 37 | def protected VLSVariable duplicate(VLSVariable term) { |
38 | return createVLSVariable => [it.name = term.name] | 38 | return createVLSVariable => [it.name = term.name] |
39 | } | 39 | } |
40 | 40 | ||
41 | def protected VLSFunctionAsTerm duplicate(VLSFunctionAsTerm term) { | 41 | def protected VLSFunctionAsTerm duplicate(VLSFunctionAsTerm term) { |
42 | return createVLSFunctionAsTerm => [it.functor = term.functor] | 42 | return createVLSFunctionAsTerm => [it.functor = term.functor] |
43 | } | 43 | } |
44 | 44 | ||
45 | def protected VLSConstant duplicate(VLSConstant term) { | 45 | def protected VLSConstant duplicate(VLSConstant term) { |
46 | return createVLSConstant => [it.name = term.name] | 46 | return createVLSConstant => [it.name = term.name] |
47 | } | 47 | } |
@@ -61,14 +61,23 @@ class Logic2VampireLanguageMapper_Support { | |||
61 | it.terms += duplicate(v) | 61 | it.terms += duplicate(v) |
62 | ] | 62 | ] |
63 | } | 63 | } |
64 | 64 | ||
65 | def protected VLSFunction duplicate(VLSFunction term, List<VLSVariable> vars) { | ||
66 | return createVLSFunction => [ | ||
67 | it.constant = term.constant | ||
68 | for (v : vars) { | ||
69 | it.terms += duplicate(v) | ||
70 | } | ||
71 | ] | ||
72 | } | ||
73 | |||
65 | def protected VLSFunction duplicate(VLSFunction term, VLSFunctionAsTerm v) { | 74 | def protected VLSFunction duplicate(VLSFunction term, VLSFunctionAsTerm v) { |
66 | return createVLSFunction => [ | 75 | return createVLSFunction => [ |
67 | it.constant = term.constant | 76 | it.constant = term.constant |
68 | it.terms += duplicate(v) | 77 | it.terms += duplicate(v) |
69 | ] | 78 | ] |
70 | } | 79 | } |
71 | 80 | ||
72 | def protected VLSConstant toConstant(VLSFunctionAsTerm term) { | 81 | def protected VLSConstant toConstant(VLSFunctionAsTerm term) { |
73 | return createVLSConstant => [ | 82 | return createVLSConstant => [ |
74 | it.name = term.functor | 83 | it.name = term.functor |
@@ -84,6 +93,13 @@ class Logic2VampireLanguageMapper_Support { | |||
84 | ] | 93 | ] |
85 | } | 94 | } |
86 | 95 | ||
96 | def protected VLSFunction topLevelTypeFunc(VLSVariable v) { | ||
97 | return createVLSFunction => [ | ||
98 | it.constant = "object" | ||
99 | it.terms += duplicate(v) | ||
100 | ] | ||
101 | } | ||
102 | |||
87 | def protected VLSFunction topLevelTypeFunc(VLSFunctionAsTerm v) { | 103 | def protected VLSFunction topLevelTypeFunc(VLSFunctionAsTerm v) { |
88 | return createVLSFunction => [ | 104 | return createVLSFunction => [ |
89 | it.constant = "object" | 105 | it.constant = "object" |
@@ -173,14 +189,16 @@ class Logic2VampireLanguageMapper_Support { | |||
173 | */ | 189 | */ |
174 | // QUANTIFIERS + VARIABLES | 190 | // QUANTIFIERS + VARIABLES |
175 | def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, | 191 | def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, |
176 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables, boolean isUniversal) { | 192 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables, |
193 | boolean isUniversal) { | ||
177 | val variableMap = expression.quantifiedVariables.toInvertedMap [ v | | 194 | val variableMap = expression.quantifiedVariables.toInvertedMap [ v | |
178 | createVLSVariable => [it.name = toIDMultiple("V", v.name)] | 195 | createVLSVariable => [it.name = toIDMultiple("V", v.name)] |
179 | ] | 196 | ] |
180 | 197 | ||
181 | val typedefs = new ArrayList<VLSTerm> | 198 | val typedefs = new ArrayList<VLSTerm> |
182 | for (variable : expression.quantifiedVariables) { | 199 | for (variable : expression.quantifiedVariables) { |
183 | val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), variable.lookup(variableMap)) | 200 | val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), |
201 | variable.lookup(variableMap)) | ||
184 | typedefs.add(eq) | 202 | typedefs.add(eq) |
185 | } | 203 | } |
186 | if (isUniversal) { | 204 | if (isUniversal) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend index e12180fa..4c4247ce 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend | |||
@@ -1,12 +1,12 @@ | |||
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.VLSAnd | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage |
12 | import java.util.ArrayList | 12 | import java.util.ArrayList |
@@ -14,7 +14,6 @@ import java.util.Collection | |||
14 | import java.util.List | 14 | import java.util.List |
15 | 15 | ||
16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
17 | import java.util.Collections | ||
18 | 17 | ||
19 | class Logic2VampireLanguageMapper_TypeMapper { | 18 | class Logic2VampireLanguageMapper_TypeMapper { |
20 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 19 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -28,10 +27,8 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
28 | 27 | ||
29 | def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements, | 28 | def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements, |
30 | Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { | 29 | Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { |
31 | |||
32 | // val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes | ||
33 | // trace.typeMapperTrace = typeTrace | ||
34 | val VLSVariable variable = createVLSVariable => [it.name = "A"] | 30 | val VLSVariable variable = createVLSVariable => [it.name = "A"] |
31 | var globalCounter = 0 | ||
35 | 32 | ||
36 | // 1. Each type (class) is a predicate with a single variable as input | 33 | // 1. Each type (class) is a predicate with a single variable as input |
37 | for (type : types) { | 34 | for (type : types) { |
@@ -39,94 +36,109 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
39 | it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) | 36 | it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) |
40 | it.terms += support.duplicate(variable) | 37 | it.terms += support.duplicate(variable) |
41 | ] | 38 | ] |
42 | // typeTrace.type2Predicate.put(type, typePred) | ||
43 | trace.type2Predicate.put(type, typePred) | 39 | trace.type2Predicate.put(type, typePred) |
44 | } | 40 | } |
45 | 41 | ||
46 | // 2. Map each ENUM type definition to fof formula | 42 | // 2. Map each ENUM type definition to fof formula |
47 | for (type : types.filter(TypeDefinition)) { | 43 | for (type : types.filter(TypeDefinition)) { |
44 | |||
45 | // Create a VLSFunction for each Enum Element | ||
48 | val List<VLSFunction> orElems = newArrayList | 46 | val List<VLSFunction> orElems = newArrayList |
49 | for (e : type.elements) { | 47 | for (e : type.elements) { |
50 | val enumElemPred = createVLSFunction => [ | 48 | val enumElemPred = createVLSFunction => [ |
51 | val splitName = e.name.split(" ") | 49 | val splitName = e.name.split(" ") |
52 | if( splitName.length > 2) { | 50 | if (splitName.length > 2) { |
53 | it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) | 51 | it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) |
54 | } | 52 | } else { |
55 | else { | ||
56 | it.constant = support.toIDMultiple("e", splitName.get(0)) | 53 | it.constant = support.toIDMultiple("e", splitName.get(0)) |
57 | } | 54 | } |
58 | it.terms += support.duplicate(variable) | 55 | it.terms += support.duplicate(variable) |
59 | ] | 56 | ] |
60 | // typeTrace.element2Predicate.put(e, enumElemPred) | ||
61 | trace.element2Predicate.put(e, enumElemPred) | 57 | trace.element2Predicate.put(e, enumElemPred) |
62 | orElems.add(enumElemPred) | ||
63 | } | 58 | } |
64 | 59 | ||
60 | // Similar to InheritanceHierarchy for the Enum | ||
61 | val List<VLSTerm> possibleNots = newArrayList | ||
62 | val List<VLSTerm> typeDefs = newArrayList | ||
63 | |||
64 | for (t1 : type.elements) { | ||
65 | for (t2 : type.elements) { | ||
66 | if (t1 == t2) { | ||
67 | val fct = support.duplicate(t2.lookup(trace.element2Predicate), variable) | ||
68 | possibleNots.add(fct) | ||
69 | } else { | ||
70 | val op = support.duplicate(t2.lookup(trace.element2Predicate), variable) | ||
71 | val negFct = createVLSUnaryNegation => [ | ||
72 | it.operand = op | ||
73 | ] | ||
74 | possibleNots.add(negFct) | ||
75 | } | ||
76 | } | ||
77 | typeDefs.add(support.unfoldAnd(possibleNots)) | ||
78 | possibleNots.clear | ||
79 | } | ||
80 | |||
81 | // Implement Enum Inheritence Hierarchy | ||
65 | val res = createVLSFofFormula => [ | 82 | val res = createVLSFofFormula => [ |
66 | it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) | 83 | it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) |
67 | // below is temporary solution | ||
68 | it.fofRole = "axiom" | 84 | it.fofRole = "axiom" |
69 | it.fofFormula = createVLSUniversalQuantifier => [ | 85 | it.fofFormula = createVLSUniversalQuantifier => [ |
70 | it.variables += support.duplicate(variable) | 86 | it.variables += support.duplicate(variable) |
71 | it.operand = createVLSEquivalent => [ | 87 | it.operand = createVLSEquivalent => [ |
72 | it.left = type.lookup(trace.type2Predicate) | 88 | it.left = type.lookup(trace.type2Predicate) |
73 | it.right = support.unfoldOr(orElems) | 89 | it.right = createVLSAnd => [ |
90 | it.left = support.topLevelTypeFunc(variable) | ||
91 | it.right = support.unfoldOr(typeDefs) | ||
92 | ] | ||
93 | // it.right = support.unfoldOr((typeDefs)) | ||
94 | |||
74 | ] | 95 | ] |
75 | ] | 96 | ] |
76 | |||
77 | ] | 97 | ] |
78 | trace.specification.formulas += res | 98 | trace.specification.formulas += res |
79 | 99 | ||
80 | // Create objects for the enum elements | 100 | for (var i = globalCounter; i < globalCounter+type.elements.length; i++) { |
81 | val List<VLSTerm> enumScopeElems = newArrayList | 101 | // Create objects for the enum elements |
82 | for (var i = 0; i < type.elements.length; i++) { | ||
83 | val num = i + 1 | 102 | val num = i + 1 |
84 | val cstTerm = createVLSFunctionAsTerm => [ | 103 | val cstTerm = createVLSFunctionAsTerm => [ |
85 | it.functor = "eo" + num | 104 | it.functor = "eo" + num |
86 | ] | 105 | ] |
87 | val cst = support.toConstant(cstTerm) | 106 | val cst = support.toConstant(cstTerm) |
88 | trace.uniqueInstances.add(cst) | 107 | trace.uniqueInstances.add(cst) |
89 | val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm) | 108 | |
90 | enumScopeElems.add(fct) | 109 | val index = i |
91 | 110 | val enumScope = createVLSFofFormula => [ | |
92 | //For paradox Only | 111 | it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0), |
93 | for (var j = 0; j < type.elements.length; j++) { | 112 | type.elements.get(index).name.split(" ").get(0)) |
94 | if(j != i) { | 113 | it.fofRole = "axiom" |
95 | val op = support.duplicate(type.elements.get(j).lookup(trace.element2Predicate), cstTerm) | 114 | it.fofFormula = createVLSUniversalQuantifier => [ |
96 | val negFct = createVLSUnaryNegation => [ | 115 | it.variables += support.duplicate(variable) |
97 | it.operand = op | 116 | it.operand = createVLSEquivalent => [ |
117 | it.left = createVLSEquality => [ | ||
118 | it.left = support.duplicate(variable) | ||
119 | it.right = support.duplicate(support.toConstant(cstTerm)) | ||
120 | ] | ||
121 | it.right = support.duplicate(type.elements.get(index).lookup(trace.element2Predicate), | ||
122 | variable) | ||
98 | ] | 123 | ] |
99 | enumScopeElems.add(negFct) | 124 | ] |
100 | } | 125 | ] |
101 | } | 126 | |
102 | //End Paradox | 127 | trace.specification.formulas += enumScope |
103 | // enumScopeElems.add(support.topLevelTypeFunc(cstTerm)) | 128 | |
104 | } | 129 | } |
105 | 130 | globalCounter+=type.elements.size | |
106 | |||
107 | |||
108 | val enumScope = createVLSFofFormula => [ | ||
109 | it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0)) | ||
110 | // below is temporary solution | ||
111 | it.fofRole = "axiom" | ||
112 | it.fofFormula = support.unfoldAnd(enumScopeElems) | ||
113 | ] | ||
114 | |||
115 | trace.specification.formulas += enumScope | ||
116 | } | 131 | } |
117 | 132 | ||
118 | // HIERARCHY HANDLER | 133 | // HIERARCHY HANDLER |
119 | // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates | 134 | // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates |
120 | // and store in a map | 135 | // and store in a map |
121 | // println(types.filter[!isIsAbstract]) | 136 | for (t1 : types.filter[!isIsAbstract]) { |
122 | for (t1 : types.filter[!isIsAbstract].filter(TypeDeclaration)) { | ||
123 | for (t2 : types) { | 137 | for (t2 : types) { |
124 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes | 138 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes |
125 | if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { | 139 | if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { |
126 | // typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate))) | ||
127 | trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) | 140 | trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) |
128 | } else { | 141 | } else { |
129 | // typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ | ||
130 | trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ | 142 | trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ |
131 | it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) | 143 | it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) |
132 | ]) | 144 | ]) |