From e8ec04bff69e414b0f1b67c060d235a844c0018b Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 4 Apr 2019 20:08:30 -0400 Subject: Add small detail to #36 --- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 48 ++++++++++++--------- ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 9570 -> 9829 bytes .../Logic2VampireLanguageMapper_ScopeMapper.java | 47 ++++++++++++++------ 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 { } // 3. Specify uniqueness of elements + // TEMP + val DUPLICATES = true + val numInst = trace.uniqueInstances.length var ind = 1 if (numInst != 0) { - /* - * // SHORTER - * for (e : trace.uniqueInstances.subList(0, numInst-1)) { - /*/ - // LONGER - for (e : trace.uniqueInstances) { - // */ - val x = ind - val uniqueness = createVLSFofFormula => [ - it.name = support.toIDMultiple("t_uniqueness", e.name) - it.fofRole = "axiom" - /* - * // SHORTER - * it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e) - /*/ - // LONGER - it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e) - // */ - ] - trace.specification.formulas += uniqueness - ind++ + if (DUPLICATES) { + // W/ DUPLICATES + for (e : trace.uniqueInstances) { + val x = ind + val uniqueness = createVLSFofFormula => [ + it.name = support.toIDMultiple("t_uniqueness", e.name) + it.fofRole = "axiom" + it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e) + ] + trace.specification.formulas += uniqueness + ind++ + } + } else { + // W/O DUPLICATES + for (e : trace.uniqueInstances.subList(0, numInst - 1)) { + val x = ind + val uniqueness = createVLSFofFormula => [ + it.name = support.toIDMultiple("t_uniqueness", e.name) + it.fofRole = "axiom" + it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e) + ] + trace.specification.formulas += uniqueness + ind++ + } } } } 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin 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; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.ArrayList; import java.util.HashMap; +import java.util.List; import java.util.Map; import java.util.Set; import org.eclipse.emf.common.util.EList; @@ -104,22 +105,42 @@ public class Logic2VampireLanguageMapper_ScopeMapper { } } } + final boolean DUPLICATES = true; final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; int ind = 1; if ((numInst != 0)) { - for (final VLSConstant e : trace.uniqueInstances) { - { - final int x = ind; - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); - it.setFofRole("axiom"); - it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); - }; - final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(uniqueness); - ind++; + if (DUPLICATES) { + for (final VLSConstant e : trace.uniqueInstances) { + { + final int x = ind; + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); + it.setFofRole("axiom"); + it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); + }; + final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(uniqueness); + ind++; + } + } + } else { + List _subList = trace.uniqueInstances.subList(0, (numInst - 1)); + for (final VLSConstant e_1 : _subList) { + { + final int x = ind; + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName())); + it.setFofRole("axiom"); + it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1)); + }; + final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(uniqueness); + ind++; + } } } } -- cgit v1.2.3-54-g00ecf