diff options
author | 2019-04-04 20:08:30 -0400 | |
---|---|---|
committer | 2019-04-04 20:08:30 -0400 | |
commit | e8ec04bff69e414b0f1b67c060d235a844c0018b (patch) | |
tree | c49d4969e9a024045361a4eb1034dc6c43c8725f /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen | |
parent | Facilitate #31, close #36 (diff) | |
download | VIATRA-Generator-e8ec04bff69e414b0f1b67c060d235a844c0018b.tar.gz VIATRA-Generator-e8ec04bff69e414b0f1b67c060d235a844c0018b.tar.zst VIATRA-Generator-e8ec04bff69e414b0f1b67c060d235a844c0018b.zip |
Add small detail to #36
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen')
2 files changed, 34 insertions, 13 deletions
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 1108945f..f6006175 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_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 24b46e3e..cd3b1d13 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 | |||
@@ -18,6 +18,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | |||
18 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 18 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
19 | import java.util.ArrayList; | 19 | import java.util.ArrayList; |
20 | import java.util.HashMap; | 20 | import java.util.HashMap; |
21 | import java.util.List; | ||
21 | import java.util.Map; | 22 | import java.util.Map; |
22 | import java.util.Set; | 23 | import java.util.Set; |
23 | import org.eclipse.emf.common.util.EList; | 24 | import org.eclipse.emf.common.util.EList; |
@@ -104,22 +105,42 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
104 | } | 105 | } |
105 | } | 106 | } |
106 | } | 107 | } |
108 | final boolean DUPLICATES = true; | ||
107 | final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; | 109 | final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; |
108 | int ind = 1; | 110 | int ind = 1; |
109 | if ((numInst != 0)) { | 111 | if ((numInst != 0)) { |
110 | for (final VLSConstant e : trace.uniqueInstances) { | 112 | if (DUPLICATES) { |
111 | { | 113 | for (final VLSConstant e : trace.uniqueInstances) { |
112 | final int x = ind; | 114 | { |
113 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 115 | final int x = ind; |
114 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 116 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
115 | it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); | 117 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
116 | it.setFofRole("axiom"); | 118 | it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); |
117 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); | 119 | it.setFofRole("axiom"); |
118 | }; | 120 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); |
119 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 121 | }; |
120 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 122 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); |
121 | _formulas.add(uniqueness); | 123 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
122 | ind++; | 124 | _formulas.add(uniqueness); |
125 | ind++; | ||
126 | } | ||
127 | } | ||
128 | } else { | ||
129 | List<VLSConstant> _subList = trace.uniqueInstances.subList(0, (numInst - 1)); | ||
130 | for (final VLSConstant e_1 : _subList) { | ||
131 | { | ||
132 | final int x = ind; | ||
133 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
134 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
135 | it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName())); | ||
136 | it.setFofRole("axiom"); | ||
137 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1)); | ||
138 | }; | ||
139 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
140 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
141 | _formulas.add(uniqueness); | ||
142 | ind++; | ||
143 | } | ||
123 | } | 144 | } |
124 | } | 145 | } |
125 | } | 146 | } |