From 6cac004e4935f4cdbfaf1004c74ba7604f990ddc Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 6 Mar 2019 17:26:43 -0500 Subject: Implement Enum handling and study hierarchy handling --- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2399 -> 2399 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 17812 -> 17814 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 3708 -> 4215 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8207 -> 8212 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 6096 -> 6157 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 10926 -> 11900 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 8576 -> 9388 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 .../builder/Logic2VampireLanguageMapperTrace.java | 5 +++ .../Logic2VampireLanguageMapper_ScopeMapper.java | 24 ++++++----- .../Logic2VampireLanguageMapper_Support.java | 47 +++++++++++++++++++++ .../Logic2VampireLanguageMapper_TypeMapper.java | 36 ++++++++++++++-- 17 files changed, 97 insertions(+), 15 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 e0766c08..3f204913 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 c38c96ad..10983f27 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 2c091b47..00ebca4b 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 b05fd2c1..9641858d 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 7f6519eb..2b51fe5d 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 d30eebe5..75482abc 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 921b79bd..c394f878 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 6b8d1dc0..1ec5da80 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 83e57283..e85b5240 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 5a0087bc..c000d128 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 7d090297..5eb63977 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 c8ab54c2..501dbfb4 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 3306fa73..621c888a 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/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index 2b491209..24df5fcd 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java @@ -1,6 +1,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; @@ -14,7 +15,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; import java.util.HashMap; +import java.util.List; import java.util.Map; +import org.eclipse.xtext.xbase.lib.CollectionLiterals; @SuppressWarnings("all") public class Logic2VampireLanguageMapperTrace { @@ -34,6 +37,8 @@ public class Logic2VampireLanguageMapperTrace { public final Map type2And = new HashMap(); + public final List uniqueInstances = CollectionLiterals.newArrayList(); + public Map constantDefinitions; public Map relationDefinitions; 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 8967839d..15ba78c9 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 @@ -5,13 +5,14 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; 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 java.util.List; +import java.util.ArrayList; import org.eclipse.emf.common.util.EList; import org.eclipse.xtext.xbase.lib.CollectionLiterals; import org.eclipse.xtext.xbase.lib.Extension; @@ -39,7 +40,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { it.setName("A"); }; final VLSVariable variable = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - final List instances = CollectionLiterals.newArrayList(); + final ArrayList localInstances = CollectionLiterals.newArrayList(); for (int i = 0; (i < config.typeScopes.minNewElements); i++) { { final int num = (i + 1); @@ -48,7 +49,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper { it.setName(("o" + Integer.valueOf(num))); }; final VLSConstant cst = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function_1); - instances.add(cst); + trace.uniqueInstances.add(cst); + localInstances.add(cst); } } if ((config.typeScopes.minNewElements != 0)) { @@ -61,10 +63,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper { EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(variable); _variables.add(_duplicate); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_3 = (VLSEquivalent it_2) -> { - it_2.setLeft(this.support.topLevelTypeFunc()); - final Function1 _function_4 = (VLSConstant i) -> { + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_3 = (VLSImplies it_2) -> { + final Function1 _function_4 = (VLSTerm i) -> { VLSEquality _createVLSEquality = this.factory.createVLSEquality(); final Procedure1 _function_5 = (VLSEquality it_3) -> { VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); @@ -77,9 +78,10 @@ public class Logic2VampireLanguageMapper_ScopeMapper { }; return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); }; - it_2.setRight(this.support.unfoldOr(ListExtensions.map(instances, _function_4))); + it_2.setLeft(this.support.unfoldOr(ListExtensions.map(localInstances, _function_4))); + it_2.setRight(this.support.topLevelTypeFunc()); }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); + VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); it_1.setOperand(_doubleArrow); }; VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); @@ -92,7 +94,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { final Procedure1 _function_2 = (VLSFofFormula it) -> { it.setName("typeUniqueness"); it.setFofRole("axiom"); - it.setFofFormula(this.support.establishUniqueness(instances)); + it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances)); }; final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_2); EList _formulas_1 = trace.specification.getFormulas(); diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index 72ca44e9..e2ff7a0e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java @@ -6,6 +6,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; @@ -62,6 +63,22 @@ public class Logic2VampireLanguageMapper_Support { return ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); } + protected VLSFunctionAsTerm duplicate(final VLSFunctionAsTerm term) { + VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); + final Procedure1 _function = (VLSFunctionAsTerm it) -> { + it.setFunctor(term.getFunctor()); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function); + } + + protected VLSConstant duplicate(final VLSConstant term) { + VLSConstant _createVLSConstant = this.factory.createVLSConstant(); + final Procedure1 _function = (VLSConstant it) -> { + it.setName(term.getName()); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); + } + protected VLSFunction duplicate(final VLSFunction term) { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function = (VLSFunction it) -> { @@ -87,6 +104,25 @@ public class Logic2VampireLanguageMapper_Support { return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); } + protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + it.setConstant(term.getConstant()); + EList _terms = it.getTerms(); + VLSFunctionAsTerm _duplicate = this.duplicate(v); + _terms.add(_duplicate); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); + } + + protected VLSConstant toConstant(final VLSFunctionAsTerm term) { + VLSConstant _createVLSConstant = this.factory.createVLSConstant(); + final Procedure1 _function = (VLSConstant it) -> { + it.setName(term.getFunctor()); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); + } + protected VLSFunction topLevelTypeFunc() { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function = (VLSFunction it) -> { @@ -102,6 +138,17 @@ public class Logic2VampireLanguageMapper_Support { return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); } + protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + it.setConstant("object"); + EList _terms = it.getTerms(); + VLSFunctionAsTerm _duplicate = this.duplicate(v); + _terms.add(_duplicate); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); + } + public VLSTerm establishUniqueness(final List terms) { final List eqs = CollectionLiterals.newArrayList(); List _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); 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 d3dddcfc..f776371b 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 @@ -3,10 +3,12 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; @@ -16,6 +18,7 @@ import com.google.common.base.Objects; import com.google.common.collect.Iterables; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; @@ -24,6 +27,7 @@ import java.util.Collection; import java.util.List; 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.IterableExtensions; @@ -107,14 +111,38 @@ public class Logic2VampireLanguageMapper_TypeMapper { final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); EList _formulas = trace.specification.getFormulas(); _formulas.add(res); + final List enumScopeElems = CollectionLiterals.newArrayList(); + for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) { + { + final int num = (i + 1); + VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); + final Procedure1 _function_2 = (VLSFunctionAsTerm it) -> { + it.setFunctor(("eo" + Integer.valueOf(num))); + }; + final VLSFunctionAsTerm cstTerm = ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); + final VLSConstant cst = this.support.toConstant(cstTerm); + trace.uniqueInstances.add(cst); + final VLSFunction fct = this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); + enumScopeElems.add(fct); + } + } + VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); + final Procedure1 _function_2 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0])); + it.setFofRole("axiom"); + it.setFofFormula(this.support.unfoldAnd(enumScopeElems)); + }; + final VLSFofFormula enumScope = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_2); + EList _formulas_1 = trace.specification.getFormulas(); + _formulas_1.add(enumScope); } } final Function1 _function_1 = (Type it) -> { boolean _isIsAbstract = it.isIsAbstract(); return Boolean.valueOf((!_isIsAbstract)); }; - Iterable _filter_1 = IterableExtensions.filter(types, _function_1); - for (final Type t1 : _filter_1) { + Iterable _filter_1 = Iterables.filter(IterableExtensions.filter(types, _function_1), TypeDeclaration.class); + for (final TypeDeclaration t1 : _filter_1) { { for (final Type t2 : types) { if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { @@ -147,8 +175,8 @@ public class Logic2VampireLanguageMapper_TypeMapper { final Procedure1 _function_4 = (VLSEquivalent it_2) -> { it_2.setLeft(this.support.topLevelTypeFunc()); Collection _values = trace.type2And.values(); - ArrayList _arrayList = new ArrayList(_values); - it_2.setRight(this.support.unfoldOr(_arrayList)); + final ArrayList reversedList = new ArrayList(_values); + it_2.setRight(this.support.unfoldOr(reversedList)); }; VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); it_1.setOperand(_doubleArrow); -- cgit v1.2.3-54-g00ecf