diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-14 03:45:46 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-14 03:45:46 -0400 |
commit | 56df1f808fa2289c3e97d45d84bce8acc8937280 (patch) | |
tree | 8956a784e9bc76f5f05411e891da86776c10629d /Solvers | |
parent | Implement type scope for specific types (diff) | |
download | VIATRA-Generator-56df1f808fa2289c3e97d45d84bce8acc8937280.tar.gz VIATRA-Generator-56df1f808fa2289c3e97d45d84bce8acc8937280.tar.zst VIATRA-Generator-56df1f808fa2289c3e97d45d84bce8acc8937280.zip |
Implement Containment mapping (partially) and revisit enum mapping
Diffstat (limited to 'Solvers')
19 files changed, 567 insertions, 129 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 | ]) |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index 052e0175..8e50f399 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 1296bf9e..99ba52b8 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index fd625384..7b01a284 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin new file mode 100644 index 00000000..9f455fdd --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index 978571d2..0b91349d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index b98f0332..07e249ce 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 8238a89e..115249ba 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index f64a218b..2e86d0c7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore index ec8107e8..8a9aa4bb 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore | |||
@@ -38,3 +38,5 @@ | |||
38 | /.VampireSolutionModel.java._trace | 38 | /.VampireSolutionModel.java._trace |
39 | /.VampireCallerWithTimeout.java._trace | 39 | /.VampireCallerWithTimeout.java._trace |
40 | /.Logic2VampireLanguageMapper_ScopeMapper.java._trace | 40 | /.Logic2VampireLanguageMapper_ScopeMapper.java._trace |
41 | /.Logic2VampireLanguageMapper_Containment.java._trace | ||
42 | /.Logic2VampireLanguageMapper_ContainmentMapper.java._trace | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index afe77bbe..36a727b2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java | |||
@@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ContainmentMapper; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; | 7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper; | 8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper; |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
@@ -83,6 +84,9 @@ public class Logic2VampireLanguageMapper { | |||
83 | private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); | 84 | private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); |
84 | 85 | ||
85 | @Accessors(AccessorType.PUBLIC_GETTER) | 86 | @Accessors(AccessorType.PUBLIC_GETTER) |
87 | private final Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(this); | ||
88 | |||
89 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
86 | private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); | 90 | private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); |
87 | 91 | ||
88 | @Accessors(AccessorType.PUBLIC_GETTER) | 92 | @Accessors(AccessorType.PUBLIC_GETTER) |
@@ -114,12 +118,13 @@ public class Logic2VampireLanguageMapper { | |||
114 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); | 118 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); |
115 | } | 119 | } |
116 | this.scopeMapper.transformScope(config, trace); | 120 | this.scopeMapper.transformScope(config, trace); |
117 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | ||
118 | trace.relationDefinitions = this.collectRelationDefinitions(problem); | 121 | trace.relationDefinitions = this.collectRelationDefinitions(problem); |
119 | final Consumer<Relation> _function_3 = (Relation it) -> { | 122 | final Consumer<Relation> _function_3 = (Relation it) -> { |
120 | this.relationMapper.transformRelation(it, trace); | 123 | this.relationMapper.transformRelation(it, trace); |
121 | }; | 124 | }; |
122 | problem.getRelations().forEach(_function_3); | 125 | problem.getRelations().forEach(_function_3); |
126 | this.containmentMapper.transformContainment(problem.getContainmentHierarchies(), trace); | ||
127 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | ||
123 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { | 128 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { |
124 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); | 129 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); |
125 | }; | 130 | }; |
@@ -428,6 +433,11 @@ public class Logic2VampireLanguageMapper { | |||
428 | } | 433 | } |
429 | 434 | ||
430 | @Pure | 435 | @Pure |
436 | public Logic2VampireLanguageMapper_ContainmentMapper getContainmentMapper() { | ||
437 | return this.containmentMapper; | ||
438 | } | ||
439 | |||
440 | @Pure | ||
431 | public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { | 441 | public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { |
432 | return this.relationMapper; | 442 | return this.relationMapper; |
433 | } | 443 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java new file mode 100644 index 00000000..da0e5615 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | |||
@@ -0,0 +1,180 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; | ||
23 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
24 | import java.util.ArrayList; | ||
25 | import java.util.List; | ||
26 | import org.eclipse.emf.common.util.EList; | ||
27 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
28 | import org.eclipse.xtext.xbase.lib.Extension; | ||
29 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
30 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
31 | |||
32 | @SuppressWarnings("all") | ||
33 | public class Logic2VampireLanguageMapper_ContainmentMapper { | ||
34 | @Extension | ||
35 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
36 | |||
37 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
38 | |||
39 | private final Logic2VampireLanguageMapper base; | ||
40 | |||
41 | private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> { | ||
42 | it.setName("A"); | ||
43 | })); | ||
44 | |||
45 | public Logic2VampireLanguageMapper_ContainmentMapper(final Logic2VampireLanguageMapper base) { | ||
46 | this.base = base; | ||
47 | } | ||
48 | |||
49 | public void transformContainment(final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) { | ||
50 | final ContainmentHierarchy hierarchy = hierarchies.get(0); | ||
51 | final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); | ||
52 | final EList<Relation> relationsList = hierarchy.getContainmentRelations(); | ||
53 | for (final Relation l : relationsList) { | ||
54 | { | ||
55 | TypeReference _get = l.getParameters().get(1); | ||
56 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
57 | Type pointingTo = ((Type) _referred); | ||
58 | containmentListCopy.remove(pointingTo); | ||
59 | EList<Type> _subtypes = pointingTo.getSubtypes(); | ||
60 | for (final Type c : _subtypes) { | ||
61 | containmentListCopy.remove(c); | ||
62 | } | ||
63 | } | ||
64 | } | ||
65 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); | ||
66 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate)); | ||
67 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
68 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
69 | it.setName(this.support.toIDMultiple("containment_topLevel", topName)); | ||
70 | it.setFofRole("axiom"); | ||
71 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
72 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
73 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
74 | VLSVariable _duplicate = this.support.duplicate(this.variable); | ||
75 | _variables.add(_duplicate); | ||
76 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
77 | final Procedure1<VLSEquivalent> _function_2 = (VLSEquivalent it_2) -> { | ||
78 | it_2.setLeft(topTerm); | ||
79 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
80 | final Procedure1<VLSEquality> _function_3 = (VLSEquality it_3) -> { | ||
81 | it_3.setLeft(this.support.duplicate(this.variable)); | ||
82 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
83 | final Procedure1<VLSConstant> _function_4 = (VLSConstant it_4) -> { | ||
84 | it_4.setName("o1"); | ||
85 | }; | ||
86 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_4); | ||
87 | it_3.setRight(_doubleArrow); | ||
88 | }; | ||
89 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_3); | ||
90 | it_2.setRight(_doubleArrow); | ||
91 | }; | ||
92 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_2); | ||
93 | it_1.setOperand(_doubleArrow); | ||
94 | }; | ||
95 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
96 | it.setFofFormula(_doubleArrow); | ||
97 | }; | ||
98 | final VLSFofFormula contTop = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
99 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
100 | _formulas.add(contTop); | ||
101 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
102 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
103 | it.setName("A"); | ||
104 | }; | ||
105 | final VLSVariable varA = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
106 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
107 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it) -> { | ||
108 | it.setName("B"); | ||
109 | }; | ||
110 | final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
111 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); | ||
112 | for (final Relation l_1 : relationsList) { | ||
113 | { | ||
114 | final String relName = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate).getConstant().toString(); | ||
115 | TypeReference _get = l_1.getParameters().get(0); | ||
116 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
117 | final Type fromType = ((Type) _referred); | ||
118 | TypeReference _get_1 = l_1.getParameters().get(1); | ||
119 | Type _referred_1 = ((ComplexTypeReference) _get_1).getReferred(); | ||
120 | final Type toType = ((Type) _referred_1); | ||
121 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
122 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | ||
123 | it.setName(this.support.toIDMultiple("containment", relName)); | ||
124 | it.setFofRole("axiom"); | ||
125 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
126 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | ||
127 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
128 | VLSVariable _duplicate = this.support.duplicate(varA); | ||
129 | _variables.add(_duplicate); | ||
130 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
131 | final Procedure1<VLSImplies> _function_5 = (VLSImplies it_2) -> { | ||
132 | it_2.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate), varA)); | ||
133 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
134 | final Procedure1<VLSExistentialQuantifier> _function_6 = (VLSExistentialQuantifier it_3) -> { | ||
135 | EList<VLSVariable> _variables_1 = it_3.getVariables(); | ||
136 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | ||
137 | _variables_1.add(_duplicate_1); | ||
138 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
139 | final Procedure1<VLSAnd> _function_7 = (VLSAnd it_4) -> { | ||
140 | it_4.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(fromType, trace.type2Predicate), varB)); | ||
141 | it_4.setRight(this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList)); | ||
142 | }; | ||
143 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_7); | ||
144 | it_3.setOperand(_doubleArrow); | ||
145 | }; | ||
146 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_6); | ||
147 | it_2.setRight(_doubleArrow); | ||
148 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
149 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { | ||
150 | it_3.setLeft(this.support.duplicate(this.variable)); | ||
151 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
152 | final Procedure1<VLSConstant> _function_8 = (VLSConstant it_4) -> { | ||
153 | it_4.setName("o1"); | ||
154 | }; | ||
155 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_8); | ||
156 | it_3.setRight(_doubleArrow_1); | ||
157 | }; | ||
158 | ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); | ||
159 | }; | ||
160 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_5); | ||
161 | it_1.setOperand(_doubleArrow); | ||
162 | }; | ||
163 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | ||
164 | it.setFofFormula(_doubleArrow); | ||
165 | }; | ||
166 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); | ||
167 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
168 | _formulas_1.add(relFormula); | ||
169 | TypeReference _get_2 = l_1.getParameters().get(1); | ||
170 | Type _referred_2 = ((ComplexTypeReference) _get_2).getReferred(); | ||
171 | Type pointingTo = ((Type) _referred_2); | ||
172 | containmentListCopy.remove(pointingTo); | ||
173 | EList<Type> _subtypes = pointingTo.getSubtypes(); | ||
174 | for (final Type c : _subtypes) { | ||
175 | containmentListCopy.remove(c); | ||
176 | } | ||
177 | } | ||
178 | } | ||
179 | } | ||
180 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index 1950cad0..d2a6bff2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |||
@@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
@@ -48,16 +49,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
48 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 49 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
49 | final int GLOBAL_MIN = config.typeScopes.minNewElements; | 50 | final int GLOBAL_MIN = config.typeScopes.minNewElements; |
50 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; | 51 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; |
51 | final ArrayList<Object> localInstances = CollectionLiterals.<Object>newArrayList(); | 52 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); |
52 | if ((GLOBAL_MIN != 0)) { | 53 | if ((GLOBAL_MIN != 0)) { |
53 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); | 54 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); |
55 | for (final VLSConstant i : trace.uniqueInstances) { | ||
56 | localInstances.add(this.support.duplicate(i)); | ||
57 | } | ||
54 | this.makeFofFormula(localInstances, trace, true, null); | 58 | this.makeFofFormula(localInstances, trace, true, null); |
55 | } | 59 | } |
56 | if ((GLOBAL_MAX != 0)) { | 60 | if ((GLOBAL_MAX != 0)) { |
57 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); | 61 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); |
58 | this.makeFofFormula(localInstances, trace, false, null); | 62 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); |
59 | } | 63 | } |
60 | int i = 0; | 64 | int i_1 = 1; |
61 | int minNum = (-1); | 65 | int minNum = (-1); |
62 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); | 66 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); |
63 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); | 67 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); |
@@ -65,10 +69,10 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
65 | { | 69 | { |
66 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); | 70 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); |
67 | if ((minNum != 0)) { | 71 | if ((minNum != 0)) { |
68 | this.getInstanceConstants((i + minNum), i, localInstances, trace, true, false); | 72 | this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); |
69 | startPoints.put(t, Integer.valueOf(i)); | 73 | startPoints.put(t, Integer.valueOf(i_1)); |
70 | int _i = i; | 74 | int _i = i_1; |
71 | i = (_i + minNum); | 75 | i_1 = (_i + minNum); |
72 | this.makeFofFormula(localInstances, trace, true, t); | 76 | this.makeFofFormula(localInstances, trace, true, t); |
73 | } | 77 | } |
74 | } | 78 | } |
@@ -83,8 +87,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
83 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); | 87 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); |
84 | } | 88 | } |
85 | if (((maxNum).intValue() != minNum)) { | 89 | if (((maxNum).intValue() != minNum)) { |
86 | int instEndInd = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum)); | 90 | int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); |
87 | this.getInstanceConstants(instEndInd, i, localInstances, trace, false, false); | 91 | this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); |
88 | this.makeFofFormula(localInstances, trace, false, t_1); | 92 | this.makeFofFormula(localInstances, trace, false, t_1); |
89 | } | 93 | } |
90 | } | 94 | } |
@@ -126,18 +130,24 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
126 | 130 | ||
127 | protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { | 131 | protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { |
128 | String nm = ""; | 132 | String nm = ""; |
129 | VLSFunction tm = null; | 133 | VLSTerm tm = null; |
130 | if ((type == null)) { | 134 | if ((type == null)) { |
131 | nm = "object"; | 135 | nm = "object"; |
132 | tm = this.support.topLevelTypeFunc(); | 136 | tm = this.support.topLevelTypeFunc(); |
133 | } else { | 137 | } else { |
134 | nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString(); | 138 | nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString(); |
135 | tm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate)); | 139 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); |
140 | final Procedure1<VLSAnd> _function = (VLSAnd it) -> { | ||
141 | it.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate))); | ||
142 | it.setRight(this.support.topLevelTypeFunc()); | ||
143 | }; | ||
144 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function); | ||
145 | tm = _doubleArrow; | ||
136 | } | 146 | } |
137 | final String name = nm; | 147 | final String name = nm; |
138 | final VLSFunction term = tm; | 148 | final VLSTerm term = tm; |
139 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 149 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
140 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 150 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { |
141 | String _xifexpression = null; | 151 | String _xifexpression = null; |
142 | if (minimum) { | 152 | if (minimum) { |
143 | _xifexpression = "min"; | 153 | _xifexpression = "min"; |
@@ -147,53 +157,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
147 | it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); | 157 | it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); |
148 | it.setFofRole("axiom"); | 158 | it.setFofRole("axiom"); |
149 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 159 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
150 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | 160 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
151 | EList<VLSVariable> _variables = it_1.getVariables(); | 161 | EList<VLSVariable> _variables = it_1.getVariables(); |
152 | VLSVariable _duplicate = this.support.duplicate(this.variable); | 162 | VLSVariable _duplicate = this.support.duplicate(this.variable); |
153 | _variables.add(_duplicate); | 163 | _variables.add(_duplicate); |
154 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 164 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
155 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | 165 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { |
156 | if (minimum) { | 166 | if (minimum) { |
157 | final Function1<VLSTerm, VLSEquality> _function_3 = (VLSTerm i) -> { | 167 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { |
158 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | 168 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); |
159 | final Procedure1<VLSEquality> _function_4 = (VLSEquality it_3) -> { | 169 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { |
160 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 170 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
161 | final Procedure1<VLSVariable> _function_5 = (VLSVariable it_4) -> { | 171 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { |
162 | it_4.setName(this.variable.getName()); | 172 | it_4.setName(this.variable.getName()); |
163 | }; | 173 | }; |
164 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_5); | 174 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); |
165 | it_3.setLeft(_doubleArrow); | 175 | it_3.setLeft(_doubleArrow_1); |
166 | it_3.setRight(i); | 176 | it_3.setRight(i); |
167 | }; | 177 | }; |
168 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_4); | 178 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); |
169 | }; | 179 | }; |
170 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_3))); | 180 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4))); |
171 | it_2.setRight(term); | 181 | it_2.setRight(term); |
172 | } else { | 182 | } else { |
173 | it_2.setLeft(term); | 183 | it_2.setLeft(term); |
174 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { | 184 | final Function1<VLSTerm, VLSEquality> _function_5 = (VLSTerm i) -> { |
175 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | 185 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); |
176 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { | 186 | final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> { |
177 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 187 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
178 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { | 188 | final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> { |
179 | it_4.setName(this.variable.getName()); | 189 | it_4.setName(this.variable.getName()); |
180 | }; | 190 | }; |
181 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); | 191 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_7); |
182 | it_3.setLeft(_doubleArrow); | 192 | it_3.setLeft(_doubleArrow_1); |
183 | it_3.setRight(i); | 193 | it_3.setRight(i); |
184 | }; | 194 | }; |
185 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); | 195 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6); |
186 | }; | 196 | }; |
187 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4))); | 197 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_5))); |
188 | } | 198 | } |
189 | }; | 199 | }; |
190 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | 200 | VLSImplies _doubleArrow_1 = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); |
191 | it_1.setOperand(_doubleArrow); | 201 | it_1.setOperand(_doubleArrow_1); |
192 | }; | 202 | }; |
193 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | 203 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); |
194 | it.setFofFormula(_doubleArrow); | 204 | it.setFofFormula(_doubleArrow_1); |
195 | }; | 205 | }; |
196 | final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 206 | final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); |
197 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 207 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
198 | _formulas.add(cstDec); | 208 | _formulas.add(cstDec); |
199 | } | 209 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index e2ff7a0e..119d01f1 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | |||
@@ -104,6 +104,19 @@ public class Logic2VampireLanguageMapper_Support { | |||
104 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 104 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
105 | } | 105 | } |
106 | 106 | ||
107 | protected VLSFunction duplicate(final VLSFunction term, final List<VLSVariable> vars) { | ||
108 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
109 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
110 | it.setConstant(term.getConstant()); | ||
111 | for (final VLSVariable v : vars) { | ||
112 | EList<VLSTerm> _terms = it.getTerms(); | ||
113 | VLSVariable _duplicate = this.duplicate(v); | ||
114 | _terms.add(_duplicate); | ||
115 | } | ||
116 | }; | ||
117 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
118 | } | ||
119 | |||
107 | protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) { | 120 | protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) { |
108 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 121 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
109 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 122 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
@@ -138,6 +151,17 @@ public class Logic2VampireLanguageMapper_Support { | |||
138 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 151 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
139 | } | 152 | } |
140 | 153 | ||
154 | protected VLSFunction topLevelTypeFunc(final VLSVariable v) { | ||
155 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
156 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
157 | it.setConstant("object"); | ||
158 | EList<VLSTerm> _terms = it.getTerms(); | ||
159 | VLSVariable _duplicate = this.duplicate(v); | ||
160 | _terms.add(_duplicate); | ||
161 | }; | ||
162 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
163 | } | ||
164 | |||
141 | protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { | 165 | protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { |
142 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 166 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
143 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 167 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
@@ -284,7 +308,8 @@ public class Logic2VampireLanguageMapper_Support { | |||
284 | for (final Variable variable : _quantifiedVariables) { | 308 | for (final Variable variable : _quantifiedVariables) { |
285 | { | 309 | { |
286 | TypeReference _range = variable.getRange(); | 310 | TypeReference _range = variable.getRange(); |
287 | final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap)); | 311 | final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), |
312 | CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap)); | ||
288 | typedefs.add(eq); | 313 | typedefs.add(eq); |
289 | } | 314 | } |
290 | } | 315 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java index b8d74f36..ec759ebf 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java | |||
@@ -3,8 +3,10 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
@@ -18,7 +20,6 @@ import com.google.common.base.Objects; | |||
18 | import com.google.common.collect.Iterables; | 20 | import com.google.common.collect.Iterables; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | 23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; |
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; | 24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; |
24 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 25 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
@@ -56,6 +57,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
56 | it.setName("A"); | 57 | it.setName("A"); |
57 | }; | 58 | }; |
58 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | 59 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); |
60 | int globalCounter = 0; | ||
59 | for (final Type type : types) { | 61 | for (final Type type : types) { |
60 | { | 62 | { |
61 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 63 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
@@ -92,7 +94,31 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
92 | }; | 94 | }; |
93 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | 95 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); |
94 | trace.element2Predicate.put(e, enumElemPred); | 96 | trace.element2Predicate.put(e, enumElemPred); |
95 | orElems.add(enumElemPred); | 97 | } |
98 | } | ||
99 | final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList(); | ||
100 | final List<VLSTerm> typeDefs = CollectionLiterals.<VLSTerm>newArrayList(); | ||
101 | EList<DefinedElement> _elements_1 = type_1.getElements(); | ||
102 | for (final DefinedElement t1 : _elements_1) { | ||
103 | { | ||
104 | EList<DefinedElement> _elements_2 = type_1.getElements(); | ||
105 | for (final DefinedElement t2 : _elements_2) { | ||
106 | boolean _equals = Objects.equal(t1, t2); | ||
107 | if (_equals) { | ||
108 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | ||
109 | possibleNots.add(fct); | ||
110 | } else { | ||
111 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | ||
112 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
113 | final Procedure1<VLSUnaryNegation> _function_1 = (VLSUnaryNegation it) -> { | ||
114 | it.setOperand(op); | ||
115 | }; | ||
116 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_1); | ||
117 | possibleNots.add(negFct); | ||
118 | } | ||
119 | } | ||
120 | typeDefs.add(this.support.unfoldAnd(possibleNots)); | ||
121 | possibleNots.clear(); | ||
96 | } | 122 | } |
97 | } | 123 | } |
98 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 124 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
@@ -107,7 +133,13 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
107 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 133 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
108 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { | 134 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { |
109 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); | 135 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); |
110 | it_2.setRight(this.support.unfoldOr(orElems)); | 136 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); |
137 | final Procedure1<VLSAnd> _function_4 = (VLSAnd it_3) -> { | ||
138 | it_3.setLeft(this.support.topLevelTypeFunc(variable)); | ||
139 | it_3.setRight(this.support.unfoldOr(typeDefs)); | ||
140 | }; | ||
141 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_4); | ||
142 | it_2.setRight(_doubleArrow); | ||
111 | }; | 143 | }; |
112 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); | 144 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); |
113 | it_1.setOperand(_doubleArrow); | 145 | it_1.setOperand(_doubleArrow); |
@@ -118,8 +150,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
118 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | 150 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); |
119 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 151 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
120 | _formulas.add(res); | 152 | _formulas.add(res); |
121 | final List<VLSTerm> enumScopeElems = CollectionLiterals.<VLSTerm>newArrayList(); | 153 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { |
122 | for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) { | ||
123 | { | 154 | { |
124 | final int num = (i + 1); | 155 | final int num = (i + 1); |
125 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | 156 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); |
@@ -129,38 +160,50 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
129 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); | 160 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); |
130 | final VLSConstant cst = this.support.toConstant(cstTerm); | 161 | final VLSConstant cst = this.support.toConstant(cstTerm); |
131 | trace.uniqueInstances.add(cst); | 162 | trace.uniqueInstances.add(cst); |
132 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); | 163 | final int index = i; |
133 | enumScopeElems.add(fct); | 164 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
134 | for (int j = 0; (j < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); j++) { | 165 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { |
135 | if ((j != i)) { | 166 | it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], |
136 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(j), trace.element2Predicate), cstTerm); | 167 | type_1.getElements().get(index).getName().split(" ")[0])); |
137 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | 168 | it.setFofRole("axiom"); |
138 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { | 169 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
139 | it.setOperand(op); | 170 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { |
171 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
172 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
173 | _variables.add(_duplicate); | ||
174 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
175 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | ||
176 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
177 | final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> { | ||
178 | it_3.setLeft(this.support.duplicate(variable)); | ||
179 | it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); | ||
180 | }; | ||
181 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6); | ||
182 | it_2.setLeft(_doubleArrow); | ||
183 | it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); | ||
140 | }; | 184 | }; |
141 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); | 185 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); |
142 | enumScopeElems.add(negFct); | 186 | it_1.setOperand(_doubleArrow); |
143 | } | 187 | }; |
144 | } | 188 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); |
189 | it.setFofFormula(_doubleArrow); | ||
190 | }; | ||
191 | final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); | ||
192 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
193 | _formulas_1.add(enumScope); | ||
145 | } | 194 | } |
146 | } | 195 | } |
147 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 196 | int _globalCounter = globalCounter; |
148 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | 197 | int _size = type_1.getElements().size(); |
149 | it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0])); | 198 | globalCounter = (_globalCounter + _size); |
150 | it.setFofRole("axiom"); | ||
151 | it.setFofFormula(this.support.unfoldAnd(enumScopeElems)); | ||
152 | }; | ||
153 | final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2); | ||
154 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
155 | _formulas_1.add(enumScope); | ||
156 | } | 199 | } |
157 | } | 200 | } |
158 | final Function1<Type, Boolean> _function_1 = (Type it) -> { | 201 | final Function1<Type, Boolean> _function_1 = (Type it) -> { |
159 | boolean _isIsAbstract = it.isIsAbstract(); | 202 | boolean _isIsAbstract = it.isIsAbstract(); |
160 | return Boolean.valueOf((!_isIsAbstract)); | 203 | return Boolean.valueOf((!_isIsAbstract)); |
161 | }; | 204 | }; |
162 | Iterable<TypeDeclaration> _filter_1 = Iterables.<TypeDeclaration>filter(IterableExtensions.<Type>filter(types, _function_1), TypeDeclaration.class); | 205 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); |
163 | for (final TypeDeclaration t1 : _filter_1) { | 206 | for (final Type t1 : _filter_1) { |
164 | { | 207 | { |
165 | for (final Type t2 : types) { | 208 | for (final Type t2 : types) { |
166 | if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { | 209 | if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { |