diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner')
3 files changed, 61 insertions, 34 deletions
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 5e8819a6..741389bb 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 | |||
@@ -93,30 +93,36 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
93 | } | 93 | } |
94 | 94 | ||
95 | // 3. Specify uniqueness of elements | 95 | // 3. Specify uniqueness of elements |
96 | // TEMP | ||
97 | val DUPLICATES = true | ||
98 | |||
96 | val numInst = trace.uniqueInstances.length | 99 | val numInst = trace.uniqueInstances.length |
97 | var ind = 1 | 100 | var ind = 1 |
98 | if (numInst != 0) { | 101 | if (numInst != 0) { |
99 | /* | 102 | if (DUPLICATES) { |
100 | * // SHORTER | 103 | // W/ DUPLICATES |
101 | * for (e : trace.uniqueInstances.subList(0, numInst-1)) { | 104 | for (e : trace.uniqueInstances) { |
102 | /*/ | 105 | val x = ind |
103 | // LONGER | 106 | val uniqueness = createVLSFofFormula => [ |
104 | for (e : trace.uniqueInstances) { | 107 | it.name = support.toIDMultiple("t_uniqueness", e.name) |
105 | // */ | 108 | it.fofRole = "axiom" |
106 | val x = ind | 109 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e) |
107 | val uniqueness = createVLSFofFormula => [ | 110 | ] |
108 | it.name = support.toIDMultiple("t_uniqueness", e.name) | 111 | trace.specification.formulas += uniqueness |
109 | it.fofRole = "axiom" | 112 | ind++ |
110 | /* | 113 | } |
111 | * // SHORTER | 114 | } else { |
112 | * it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e) | 115 | // W/O DUPLICATES |
113 | /*/ | 116 | for (e : trace.uniqueInstances.subList(0, numInst - 1)) { |
114 | // LONGER | 117 | val x = ind |
115 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e) | 118 | val uniqueness = createVLSFofFormula => [ |
116 | // */ | 119 | it.name = support.toIDMultiple("t_uniqueness", e.name) |
117 | ] | 120 | it.fofRole = "axiom" |
118 | trace.specification.formulas += uniqueness | 121 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e) |
119 | ind++ | 122 | ] |
123 | trace.specification.formulas += uniqueness | ||
124 | ind++ | ||
125 | } | ||
120 | } | 126 | } |
121 | } | 127 | } |
122 | } | 128 | } |
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 | } |