From 2f8149678539a94f2f4ca2e7ff5640ff5d7087cc Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 15 Apr 2019 00:06:29 -0400 Subject: VAMPIRE: close #22, improve test structure for #39, .vql file trouble --- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2691 -> 2691 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18156 -> 18156 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 4215 -> 4215 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 10551 -> 10674 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8209 -> 6457 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 9839 -> 9839 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13093 -> 13046 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 10705 -> 10792 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 ...ic2VampireLanguageMapper_ContainmentMapper.java | 15 +- ...Logic2VampireLanguageMapper_RelationMapper.java | 159 ++------------------- .../Logic2VampireLanguageMapper_Support.java | 18 +-- .../Logic2VampireLanguageMapper_TypeMapper.java | 25 ++-- 18 files changed, 43 insertions(+), 174 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire') 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 43e1e477..1ea7e30a 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 4e6f6ca0..ee06cb39 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 707a6089..648d9600 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 3171324f..a02821a5 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 301df7fa..b01f92a6 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_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index 5e53ea26..7634af4b 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.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 b378ed09..4906adfc 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 605ac88c..e2c945e3 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 0c289e29..f465506c 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 cb72fd90..e046604a 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 cfe1e8cd..aff62dca 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 c2079147..7212cce7 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 3c70bc14..d23bacad 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 9ef20b23..be78cace 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_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index 4cdc7e6a..9deab87f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java @@ -64,12 +64,19 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { Type _referred = ((ComplexTypeReference) _get).getReferred(); Type pointingTo = ((Type) _referred); containmentListCopy.remove(pointingTo); - EList _subtypes = pointingTo.getSubtypes(); - for (final Type c : _subtypes) { + List allSubtypes = CollectionLiterals.newArrayList(); + this.support.listSubtypes(pointingTo, allSubtypes); + for (final Type c : allSubtypes) { containmentListCopy.remove(c); } } } + for (final Type c : containmentListCopy) { + boolean _isIsAbstract = c.isIsAbstract(); + if (_isIsAbstract) { + containmentListCopy.remove(c); + } + } final String topName = CollectionsUtil.lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.lookup(containmentListCopy.get(0), trace.type2Predicate)); VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); @@ -132,7 +139,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { final VLSFunction toFunc = CollectionsUtil.lookup(toType, trace.type2Predicate); this.addToMap(type2cont, toFunc, rel); EList _subtypes = toType.getSubtypes(); - for (final Type c : _subtypes) { + for (final Type c_1 : _subtypes) { this.addToMap(type2cont, toFunc, rel); } VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); @@ -184,7 +191,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { { VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_4 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("containment", e.getKey().getConstant().toString())); + it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java index d5745333..c6565f6a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java @@ -3,7 +3,6 @@ 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.VLSEquivalent; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; @@ -17,14 +16,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; 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.TypeReference; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.ArrayList; import java.util.Arrays; -import java.util.Collection; -import java.util.HashMap; import java.util.List; -import java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.ExclusiveRange; @@ -64,10 +59,19 @@ public class Logic2VampireLanguageMapper_RelationMapper { relVar2TypeDecComply.add(varTypeComply); } } + final String[] nameArray = r.getName().split(" "); + String relNameVar = ""; + int _length_1 = nameArray.length; + boolean _equals = (_length_1 == 3); + if (_equals) { + relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); + } else { + relNameVar = r.getName(); + } + final String relName = relNameVar; VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function = (VLSFofFormula it) -> { - final String[] nameArray = r.getName().split(" "); - it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2])); + it.setName(this.support.toIDMultiple("compliance", relName)); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { @@ -80,7 +84,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { final Procedure1 _function_2 = (VLSImplies it_2) -> { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_3 = (VLSFunction it_3) -> { - it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2])); + it_3.setConstant(this.support.toIDMultiple("r", relName)); for (final VLSVariable v_1 : relVar2VLS) { EList _terms = it_3.getTerms(); VLSVariable _duplicate_1 = this.support.duplicate(v_1); @@ -104,145 +108,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { } public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { - final Map relationVar2VLS = new HashMap(); - final Map relationVar2TypeDecComply = new HashMap(); - final Map relationVar2TypeDecRes = new HashMap(); - final ArrayList typedefs = new ArrayList(); - EList _variables = reldef.getVariables(); - for (final Variable variable : _variables) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName(this.support.toIDMultiple("V", variable.getName())); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - relationVar2VLS.put(variable, v); - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_1 = (VLSFunction it) -> { - TypeReference _range = variable.getRange(); - it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.support.duplicate(v); - _terms.add(_duplicate); - }; - final VLSFunction varTypeComply = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); - relationVar2TypeDecComply.put(variable, varTypeComply); - relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); - } - } - final String[] nameArray = reldef.getName().split(" "); - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { - int _length = nameArray.length; - int _minus = (_length - 2); - int _length_1 = nameArray.length; - int _minus_1 = (_length_1 - 1); - it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], - nameArray[_minus_1])); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { - EList _variables_1 = reldef.getVariables(); - for (final Variable variable_1 : _variables_1) { - EList _variables_2 = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.lookup(variable_1, relationVar2VLS)); - _variables_2.add(_duplicate); - } - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_2 = (VLSImplies it_2) -> { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_3 = (VLSFunction it_3) -> { - it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName())); - EList _variables_3 = reldef.getVariables(); - for (final Variable variable_2 : _variables_3) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_4 = (VLSVariable it_4) -> { - it_4.setName(CollectionsUtil.lookup(variable_2, relationVar2VLS).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_4); - EList _terms = it_3.getTerms(); - _terms.add(v); - } - } - }; - VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_3); - it_2.setLeft(_doubleArrow); - Collection _values = relationVar2TypeDecComply.values(); - ArrayList _arrayList = new ArrayList(_values); - it_2.setRight(this.support.unfoldAnd(_arrayList)); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula comply = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); - VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_1 = (VLSFofFormula it) -> { - int _length = nameArray.length; - int _minus = (_length - 2); - int _length_1 = nameArray.length; - int _minus_1 = (_length_1 - 1); - it.setName(this.support.toIDMultiple("relation", nameArray[_minus], - nameArray[_minus_1])); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - EList _variables_1 = reldef.getVariables(); - for (final Variable variable_1 : _variables_1) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_3 = (VLSVariable it_2) -> { - it_2.setName(CollectionsUtil.lookup(variable_1, relationVar2VLS).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_3); - EList _variables_2 = it_1.getVariables(); - _variables_2.add(v); - } - } - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_3 = (VLSImplies it_2) -> { - Collection _values = relationVar2TypeDecRes.values(); - ArrayList _arrayList = new ArrayList(_values); - it_2.setLeft(this.support.unfoldAnd(_arrayList)); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_4 = (VLSEquivalent it_3) -> { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_5 = (VLSFunction it_4) -> { - it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName())); - EList _variables_2 = reldef.getVariables(); - for (final Variable variable_2 : _variables_2) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_6 = (VLSVariable it_5) -> { - it_5.setName(CollectionsUtil.lookup(variable_2, relationVar2VLS).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); - EList _terms = it_4.getTerms(); - _terms.add(v); - } - } - }; - VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_5); - it_3.setLeft(_doubleArrow); - it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS)); - }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); - it_2.setRight(_doubleArrow); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_1); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(comply); - EList _formulas_1 = trace.specification.getFormulas(); - _formulas_1.add(res); } public void transformRelation(final Relation r, 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_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 89633ca1..f1d73bec 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 @@ -403,20 +403,14 @@ public class Logic2VampireLanguageMapper_Support { return _xifexpression; } - protected List listSubtypes(final Type t) { - List allSubtypes = CollectionLiterals.newArrayList(); - boolean _isEmpty = t.getSubtypes().isEmpty(); - boolean _not = (!_isEmpty); - if (_not) { - EList _subtypes = t.getSubtypes(); - for (final Type subt : _subtypes) { - { - allSubtypes.add(subt); - allSubtypes = this.listSubtypes(subt); - } + protected void listSubtypes(final Type t, final List allSubtypes) { + EList _subtypes = t.getSubtypes(); + for (final Type subt : _subtypes) { + { + allSubtypes.add(subt); + this.listSubtypes(subt, allSubtypes); } } - return allSubtypes; } protected HashMap withAddition(final Map map1, final Map map2) { 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 9b8f049d..b9c1d28d 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,16 +78,19 @@ public class Logic2VampireLanguageMapper_TypeMapper { EList _elements = type_1.getElements(); for (final DefinedElement e : _elements) { { + final String[] nameArray = e.getName().split(" "); + String relNameVar = ""; + int _length = nameArray.length; + boolean _equals = (_length == 3); + if (_equals) { + relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); + } else { + relNameVar = e.getName(); + } + final String relName = relNameVar; VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { - 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])); - } + it.setConstant(this.support.toIDMultiple("e", relName)); EList _terms = it.getTerms(); VLSVariable _duplicate = this.support.duplicate(variable); _terms.add(_duplicate); @@ -123,7 +126,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function_1 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); + it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.lookup(type_1, trace.type2Predicate).getConstant().toString())); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { @@ -160,10 +163,10 @@ public class Logic2VampireLanguageMapper_TypeMapper { final VLSFunctionAsTerm cstTerm = ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); final VLSConstant cst = this.support.toConstant(cstTerm); trace.uniqueInstances.add(cst); - final int index = i; + final int index = (i - globalCounter); VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_3 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], + it.setName(this.support.toIDMultiple("enumScope", CollectionsUtil.lookup(type_1, trace.type2Predicate).getConstant().toString(), type_1.getElements().get(index).getName().split(" ")[0])); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); -- cgit v1.2.3-54-g00ecf