diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra')
2 files changed, 9 insertions, 4 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index a2b11632..d4c76bb4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend | |||
@@ -203,6 +203,11 @@ class PatternGenerator { | |||
203 | find mayExist(problem,interpretation,b); | 203 | find mayExist(problem,interpretation,b); |
204 | a == b; | 204 | a == b; |
205 | } | 205 | } |
206 | pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { | ||
207 | find mustExist(problem,interpretation,a); | ||
208 | find mustExist(problem,interpretation,b); | ||
209 | a == b; | ||
210 | } | ||
206 | 211 | ||
207 | //////////////////////// | 212 | //////////////////////// |
208 | // 0.3 Required Patterns by TypeIndexer | 213 | // 0.3 Required Patterns by TypeIndexer |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend index 329d3658..9723373f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend | |||
@@ -179,7 +179,7 @@ class RelationDefinitionIndexer { | |||
179 | } | 179 | } |
180 | 180 | ||
181 | private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { | 181 | private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { |
182 | if(modality.isMustOrCurrent) '''«a.canonizeName» == «b.canonizeName»;''' | 182 | if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' |
183 | else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | 183 | else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' |
184 | } | 184 | } |
185 | 185 | ||
@@ -187,11 +187,11 @@ class RelationDefinitionIndexer { | |||
187 | val a = inequality.who | 187 | val a = inequality.who |
188 | val b = inequality.withWhom | 188 | val b = inequality.withWhom |
189 | if(modality.isCurrent) { | 189 | if(modality.isCurrent) { |
190 | return '''«a.canonizeName» != «b.canonizeName»;''' | 190 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' |
191 | } else if(modality.isMust) { | 191 | } else if(modality.isMust) { |
192 | return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | 192 | return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' |
193 | } else { | 193 | } else { // modality.isMay |
194 | return '''«a.canonizeName» != «b.canonizeName»;''' | 194 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' |
195 | } | 195 | } |
196 | } | 196 | } |
197 | 197 | ||