From 0380611be40f8f92256455e117f2f3c04b7dd216 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 7 Mar 2019 17:29:18 -0500 Subject: Improve TypeScope handling --- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2399 -> 2399 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 17814 -> 17817 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 4215 -> 4215 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8212 -> 8209 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 6157 -> 8357 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 11900 -> 11900 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 9592 -> 9688 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 1720 -> 1720 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 4908 -> 4908 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes .../Logic2VampireLanguageMapper_ScopeMapper.java | 166 +++++++++++++++------ .../Logic2VampireLanguageMapper_TypeMapper.java | 11 +- 15 files changed, 129 insertions(+), 48 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 3f204913..5c634ba0 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin differ 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 10983f27..19d48790 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin 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 00ebca4b..2db39cf0 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index 9641858d..1fba7ac4 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin 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 2b51fe5d..9ef3a39c 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin 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 75482abc..687f4889 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.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.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index c394f878..d59b2e98 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_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 1ec5da80..eb12e24a 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin 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 8a6f30f9..70eb3434 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index c000d128..0077e151 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 5eb63977..62de24fc 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index 501dbfb4..d00ac8ca 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index 621c888a..b86330dc 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.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 15ba78c9..a412241a 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 @@ -12,9 +12,13 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; +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.Set; import org.eclipse.emf.common.util.EList; import org.eclipse.xtext.xbase.lib.CollectionLiterals; +import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.Extension; import org.eclipse.xtext.xbase.lib.Functions.Function1; import org.eclipse.xtext.xbase.lib.ListExtensions; @@ -30,76 +34,146 @@ public class Logic2VampireLanguageMapper_ScopeMapper { private final Logic2VampireLanguageMapper base; + private final VLSVariable variable = ObjectExtensions.operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1) (VLSVariable it) -> { + it.setName("A"); + })); + public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) { this.base = base; } public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName("A"); - }; - final VLSVariable variable = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - final ArrayList localInstances = CollectionLiterals.newArrayList(); - for (int i = 0; (i < config.typeScopes.minNewElements); i++) { + final int GLOBAL_MIN = config.typeScopes.minNewElements; + final int GLOBAL_MAX = config.typeScopes.maxNewElements; + final ArrayList localInstances = CollectionLiterals.newArrayList(); + if ((GLOBAL_MIN != 0)) { + this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false); + this.makeFofFormula(localInstances, trace, true, "object"); + } + if ((GLOBAL_MAX != 0)) { + this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true); + this.makeFofFormula(localInstances, trace, false, "object"); + } + int i = 0; + int minNum = (-1); + Set _keySet = config.typeScopes.minNewElementsByType.keySet(); + for (final Type t : _keySet) { + { + minNum = (CollectionsUtil.lookup(t, config.typeScopes.minNewElementsByType)).intValue(); + if ((minNum != 0)) { + this.getInstanceConstants((i + minNum), i, localInstances, trace, false); + int _i = i; + i = (_i + minNum); + this.makeFofFormula(localInstances, trace, true, t.toString()); + } + } + } + Set _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); + for (final Type t_1 : _keySet_1) { + { + Integer maxNum = CollectionsUtil.lookup(t_1, config.typeScopes.maxNewElementsByType); + minNum = (CollectionsUtil.lookup(t_1, config.typeScopes.minNewElementsByType)).intValue(); + if (((maxNum).intValue() != 0)) { + int forLimit = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum)); + this.getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false); + this.makeFofFormula(localInstances, trace, false, t_1.toString()); + } + } + } + int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; + boolean _notEquals = (_length != 0); + if (_notEquals) { + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function = (VLSFofFormula it) -> { + it.setName("typeUniqueness"); + it.setFofRole("axiom"); + it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances)); + }; + final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(uniqueness); + } + } + + protected void getInstanceConstants(final int numElems, final int init, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean addToTrace) { + list.clear(); + for (int i = init; (i < numElems); i++) { { final int num = (i + 1); VLSConstant _createVLSConstant = this.factory.createVLSConstant(); - final Procedure1 _function_1 = (VLSConstant it) -> { + final Procedure1 _function = (VLSConstant it) -> { it.setName(("o" + Integer.valueOf(num))); }; - final VLSConstant cst = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function_1); - trace.uniqueInstances.add(cst); - localInstances.add(cst); + final VLSConstant cst = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); + if (addToTrace) { + trace.uniqueInstances.add(cst); + } + list.add(cst); } } - if ((config.typeScopes.minNewElements != 0)) { - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_1 = (VLSFofFormula it) -> { - it.setName("typeScope"); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(variable); - _variables.add(_duplicate); - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_3 = (VLSImplies it_2) -> { + } + + protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final String name) { + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function = (VLSFofFormula it) -> { + String _xifexpression = null; + if (minimum) { + _xifexpression = "min"; + } else { + _xifexpression = "max"; + } + it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(this.variable); + _variables.add(_duplicate); + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_2 = (VLSImplies it_2) -> { + if (minimum) { + final Function1 _function_3 = (VLSTerm i) -> { + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function_4 = (VLSEquality it_3) -> { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_5 = (VLSVariable it_4) -> { + it_4.setName(this.variable.getName()); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_5); + it_3.setLeft(_doubleArrow); + it_3.setRight(i); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_4); + }; + it_2.setLeft(this.support.unfoldOr(ListExtensions.map(list, _function_3))); + it_2.setRight(this.support.topLevelTypeFunc()); + } else { final Function1 _function_4 = (VLSTerm i) -> { VLSEquality _createVLSEquality = this.factory.createVLSEquality(); final Procedure1 _function_5 = (VLSEquality it_3) -> { - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); final Procedure1 _function_6 = (VLSVariable it_4) -> { - it_4.setName(variable.getName()); + it_4.setName(this.variable.getName()); }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_6); + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); it_3.setLeft(_doubleArrow); it_3.setRight(i); }; return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); }; - it_2.setLeft(this.support.unfoldOr(ListExtensions.map(localInstances, _function_4))); - it_2.setRight(this.support.topLevelTypeFunc()); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); - it_1.setOperand(_doubleArrow); + it_2.setRight(this.support.unfoldOr(ListExtensions.map(list, _function_4))); + it_2.setLeft(this.support.topLevelTypeFunc()); + } }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); - it.setFofFormula(_doubleArrow); + VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); + it_1.setOperand(_doubleArrow); }; - final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(cstDec); - VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_2 = (VLSFofFormula it) -> { - it.setName("typeUniqueness"); - it.setFofRole("axiom"); - it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances)); - }; - final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_2); - EList _formulas_1 = trace.specification.getFormulas(); - _formulas_1.add(uniqueness); - } + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(cstDec); } public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { 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 c101aa4c..b8d74f36 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 @@ -78,7 +78,14 @@ public class Logic2VampireLanguageMapper_TypeMapper { { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { - it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2])); + final String[] splitName = e.getName().split(" "); + int _length = splitName.length; + boolean _greaterThan = (_length > 2); + if (_greaterThan) { + it.setConstant(this.support.toIDMultiple("e", splitName[0], splitName[2])); + } else { + it.setConstant(this.support.toIDMultiple("e", splitName[0])); + } EList _terms = it.getTerms(); VLSVariable _duplicate = this.support.duplicate(variable); _terms.add(_duplicate); @@ -175,7 +182,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function_2 = (VLSFofFormula it) -> { - it.setName("hierarchyHandler"); + it.setName("inheritanceHierarchyHandler"); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_3 = (VLSUniversalQuantifier it_1) -> { -- cgit v1.2.3-54-g00ecf