From d7730cb0d684d6324622021a310d9b4a53e7531c Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 14 Mar 2019 03:45:46 -0400 Subject: Implement Containment mapping (partially) and revisit enum mapping --- .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 17817 -> 18129 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 0 -> 7649 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8209 -> 8210 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 8916 -> 9263 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 11900 -> 12311 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 9688 -> 10377 bytes .../vampire/reasoner/builder/.gitignore | 2 + .../builder/Logic2VampireLanguageMapper.java | 12 +- ...ic2VampireLanguageMapper_ContainmentMapper.java | 180 +++++++++++++++++++++ .../Logic2VampireLanguageMapper_ScopeMapper.java | 78 +++++---- .../Logic2VampireLanguageMapper_Support.java | 27 +++- .../Logic2VampireLanguageMapper_TypeMapper.java | 99 ++++++++---- 14 files changed, 334 insertions(+), 64 deletions(-) create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java (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/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index 052e0175..8e50f399 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 1296bf9e..99ba52b8 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/.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 fd625384..7b01a284 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 new file mode 100644 index 00000000..9f455fdd Binary files /dev/null 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 978571d2..0b91349d 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 b98f0332..07e249ce 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 8238a89e..115249ba 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 f64a218b..2e86d0c7 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/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore index ec8107e8..8a9aa4bb 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore @@ -38,3 +38,5 @@ /.VampireSolutionModel.java._trace /.VampireCallerWithTimeout.java._trace /.Logic2VampireLanguageMapper_ScopeMapper.java._trace +/.Logic2VampireLanguageMapper_Containment.java._trace +/.Logic2VampireLanguageMapper_ContainmentMapper.java._trace diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index afe77bbe..36a727b2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java @@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ContainmentMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; @@ -82,6 +83,9 @@ public class Logic2VampireLanguageMapper { @Accessors(AccessorType.PUBLIC_GETTER) private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); + @Accessors(AccessorType.PUBLIC_GETTER) + private final Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(this); + @Accessors(AccessorType.PUBLIC_GETTER) private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); @@ -114,12 +118,13 @@ public class Logic2VampireLanguageMapper { this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); } this.scopeMapper.transformScope(config, trace); - trace.constantDefinitions = this.collectConstantDefinitions(problem); trace.relationDefinitions = this.collectRelationDefinitions(problem); final Consumer _function_3 = (Relation it) -> { this.relationMapper.transformRelation(it, trace); }; problem.getRelations().forEach(_function_3); + this.containmentMapper.transformContainment(problem.getContainmentHierarchies(), trace); + trace.constantDefinitions = this.collectConstantDefinitions(problem); final Consumer _function_4 = (ConstantDefinition it) -> { this.constantMapper.transformConstantDefinitionSpecification(it, trace); }; @@ -427,6 +432,11 @@ public class Logic2VampireLanguageMapper { return this.constantMapper; } + @Pure + public Logic2VampireLanguageMapper_ContainmentMapper getContainmentMapper() { + return this.containmentMapper; + } + @Pure public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { return this.relationMapper; 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 new file mode 100644 index 00000000..da0e5615 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java @@ -0,0 +1,180 @@ +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.VLSAnd; +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.VLSExistentialQuantifier; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; +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.logiclanguage.ComplexTypeReference; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; +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.logicproblem.ContainmentHierarchy; +import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; +import java.util.ArrayList; +import java.util.List; +import org.eclipse.emf.common.util.EList; +import org.eclipse.xtext.xbase.lib.CollectionLiterals; +import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; + +@SuppressWarnings("all") +public class Logic2VampireLanguageMapper_ContainmentMapper { + @Extension + private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; + + private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); + + private final Logic2VampireLanguageMapper base; + + private final VLSVariable variable = ObjectExtensions.operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1) (VLSVariable it) -> { + it.setName("A"); + })); + + public Logic2VampireLanguageMapper_ContainmentMapper(final Logic2VampireLanguageMapper base) { + this.base = base; + } + + public void transformContainment(final List hierarchies, final Logic2VampireLanguageMapperTrace trace) { + final ContainmentHierarchy hierarchy = hierarchies.get(0); + final EList containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); + final EList relationsList = hierarchy.getContainmentRelations(); + for (final Relation l : relationsList) { + { + TypeReference _get = l.getParameters().get(1); + Type _referred = ((ComplexTypeReference) _get).getReferred(); + Type pointingTo = ((Type) _referred); + containmentListCopy.remove(pointingTo); + EList _subtypes = pointingTo.getSubtypes(); + for (final Type c : _subtypes) { + 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(); + final Procedure1 _function = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("containment_topLevel", topName)); + 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); + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function_2 = (VLSEquivalent it_2) -> { + it_2.setLeft(topTerm); + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function_3 = (VLSEquality it_3) -> { + it_3.setLeft(this.support.duplicate(this.variable)); + VLSConstant _createVLSConstant = this.factory.createVLSConstant(); + final Procedure1 _function_4 = (VLSConstant it_4) -> { + it_4.setName("o1"); + }; + VLSConstant _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function_4); + it_3.setRight(_doubleArrow); + }; + VLSEquality _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_3); + it_2.setRight(_doubleArrow); + }; + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_2); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula contTop = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(contTop); + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_1 = (VLSVariable it) -> { + it.setName("A"); + }; + final VLSVariable varA = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_1); + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_2 = (VLSVariable it) -> { + it.setName("B"); + }; + final VLSVariable varB = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_2); + final ArrayList varList = CollectionLiterals.newArrayList(varB, varA); + for (final Relation l_1 : relationsList) { + { + final String relName = CollectionsUtil.lookup(((RelationDeclaration) l_1), trace.rel2Predicate).getConstant().toString(); + TypeReference _get = l_1.getParameters().get(0); + Type _referred = ((ComplexTypeReference) _get).getReferred(); + final Type fromType = ((Type) _referred); + TypeReference _get_1 = l_1.getParameters().get(1); + Type _referred_1 = ((ComplexTypeReference) _get_1).getReferred(); + final Type toType = ((Type) _referred_1); + VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); + final Procedure1 _function_3 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("containment", relName)); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_4 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(varA); + _variables.add(_duplicate); + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_5 = (VLSImplies it_2) -> { + it_2.setLeft(this.support.duplicate(CollectionsUtil.lookup(toType, trace.type2Predicate), varA)); + VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); + final Procedure1 _function_6 = (VLSExistentialQuantifier it_3) -> { + EList _variables_1 = it_3.getVariables(); + VLSVariable _duplicate_1 = this.support.duplicate(varB); + _variables_1.add(_duplicate_1); + VLSAnd _createVLSAnd = this.factory.createVLSAnd(); + final Procedure1 _function_7 = (VLSAnd it_4) -> { + it_4.setLeft(this.support.duplicate(CollectionsUtil.lookup(fromType, trace.type2Predicate), varB)); + it_4.setRight(this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList)); + }; + VLSAnd _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function_7); + it_3.setOperand(_doubleArrow); + }; + VLSExistentialQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_6); + it_2.setRight(_doubleArrow); + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function_7 = (VLSEquality it_3) -> { + it_3.setLeft(this.support.duplicate(this.variable)); + VLSConstant _createVLSConstant = this.factory.createVLSConstant(); + final Procedure1 _function_8 = (VLSConstant it_4) -> { + it_4.setName("o1"); + }; + VLSConstant _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function_8); + it_3.setRight(_doubleArrow_1); + }; + ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_7); + }; + VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_5); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula relFormula = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_3); + EList _formulas_1 = trace.specification.getFormulas(); + _formulas_1.add(relFormula); + TypeReference _get_2 = l_1.getParameters().get(1); + Type _referred_2 = ((ComplexTypeReference) _get_2).getReferred(); + Type pointingTo = ((Type) _referred_2); + containmentListCopy.remove(pointingTo); + EList _subtypes = pointingTo.getSubtypes(); + for (final Type c : _subtypes) { + containmentListCopy.remove(c); + } + } + } + } +} 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 1950cad0..d2a6bff2 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 @@ -3,6 +3,7 @@ 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.VLSAnd; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; @@ -48,16 +49,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper { public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { final int GLOBAL_MIN = config.typeScopes.minNewElements; final int GLOBAL_MAX = config.typeScopes.maxNewElements; - final ArrayList localInstances = CollectionLiterals.newArrayList(); + final ArrayList localInstances = CollectionLiterals.newArrayList(); if ((GLOBAL_MIN != 0)) { this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); + for (final VLSConstant i : trace.uniqueInstances) { + localInstances.add(this.support.duplicate(i)); + } this.makeFofFormula(localInstances, trace, true, null); } if ((GLOBAL_MAX != 0)) { this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); - this.makeFofFormula(localInstances, trace, false, null); + this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); } - int i = 0; + int i_1 = 1; int minNum = (-1); Map startPoints = new HashMap(); Set _keySet = config.typeScopes.minNewElementsByType.keySet(); @@ -65,10 +69,10 @@ public class Logic2VampireLanguageMapper_ScopeMapper { { minNum = (CollectionsUtil.lookup(t, config.typeScopes.minNewElementsByType)).intValue(); if ((minNum != 0)) { - this.getInstanceConstants((i + minNum), i, localInstances, trace, true, false); - startPoints.put(t, Integer.valueOf(i)); - int _i = i; - i = (_i + minNum); + this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); + startPoints.put(t, Integer.valueOf(i_1)); + int _i = i_1; + i_1 = (_i + minNum); this.makeFofFormula(localInstances, trace, true, t); } } @@ -83,8 +87,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper { this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); } if (((maxNum).intValue() != minNum)) { - int instEndInd = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum)); - this.getInstanceConstants(instEndInd, i, localInstances, trace, false, false); + int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); + this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); this.makeFofFormula(localInstances, trace, false, t_1); } } @@ -126,18 +130,24 @@ public class Logic2VampireLanguageMapper_ScopeMapper { protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { String nm = ""; - VLSFunction tm = null; + VLSTerm tm = null; if ((type == null)) { nm = "object"; tm = this.support.topLevelTypeFunc(); } else { nm = CollectionsUtil.lookup(type, trace.type2Predicate).getConstant().toString(); - tm = this.support.duplicate(CollectionsUtil.lookup(type, trace.type2Predicate)); + VLSAnd _createVLSAnd = this.factory.createVLSAnd(); + final Procedure1 _function = (VLSAnd it) -> { + it.setLeft(this.support.duplicate(CollectionsUtil.lookup(type, trace.type2Predicate))); + it.setRight(this.support.topLevelTypeFunc()); + }; + VLSAnd _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function); + tm = _doubleArrow; } final String name = nm; - final VLSFunction term = tm; + final VLSTerm term = tm; VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { + final Procedure1 _function_1 = (VLSFofFormula it) -> { String _xifexpression = null; if (minimum) { _xifexpression = "min"; @@ -147,53 +157,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper { it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { + final Procedure1 _function_2 = (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) -> { + final Procedure1 _function_3 = (VLSImplies it_2) -> { if (minimum) { - final Function1 _function_3 = (VLSTerm i) -> { + final Function1 _function_4 = (VLSTerm i) -> { VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_4 = (VLSEquality it_3) -> { + final Procedure1 _function_5 = (VLSEquality it_3) -> { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_5 = (VLSVariable it_4) -> { + final Procedure1 _function_6 = (VLSVariable it_4) -> { it_4.setName(this.variable.getName()); }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_5); - it_3.setLeft(_doubleArrow); + VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); + it_3.setLeft(_doubleArrow_1); it_3.setRight(i); }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_4); + return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); }; - it_2.setLeft(this.support.unfoldOr(ListExtensions.map(list, _function_3))); + it_2.setLeft(this.support.unfoldOr(ListExtensions.map(list, _function_4))); it_2.setRight(term); } else { it_2.setLeft(term); - final Function1 _function_4 = (VLSTerm i) -> { + final Function1 _function_5 = (VLSTerm i) -> { VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_5 = (VLSEquality it_3) -> { + final Procedure1 _function_6 = (VLSEquality it_3) -> { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_6 = (VLSVariable it_4) -> { + final Procedure1 _function_7 = (VLSVariable it_4) -> { it_4.setName(this.variable.getName()); }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); - it_3.setLeft(_doubleArrow); + VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_7); + it_3.setLeft(_doubleArrow_1); it_3.setRight(i); }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); + return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_6); }; - it_2.setRight(this.support.unfoldOr(ListExtensions.map(list, _function_4))); + it_2.setRight(this.support.unfoldOr(ListExtensions.map(list, _function_5))); } }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); - it_1.setOperand(_doubleArrow); + VLSImplies _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); + it_1.setOperand(_doubleArrow_1); }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); - it.setFofFormula(_doubleArrow); + VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); + it.setFofFormula(_doubleArrow_1); }; - final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); EList _formulas = trace.specification.getFormulas(); _formulas.add(cstDec); } 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 e2ff7a0e..119d01f1 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 @@ -104,6 +104,19 @@ public class Logic2VampireLanguageMapper_Support { return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); } + protected VLSFunction duplicate(final VLSFunction term, final List vars) { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + it.setConstant(term.getConstant()); + for (final VLSVariable v : vars) { + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.duplicate(v); + _terms.add(_duplicate); + } + }; + 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) -> { @@ -138,6 +151,17 @@ public class Logic2VampireLanguageMapper_Support { return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); } + protected VLSFunction topLevelTypeFunc(final VLSVariable v) { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + it.setConstant("object"); + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.duplicate(v); + _terms.add(_duplicate); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); + } + protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function = (VLSFunction it) -> { @@ -284,7 +308,8 @@ public class Logic2VampireLanguageMapper_Support { for (final Variable variable : _quantifiedVariables) { { TypeReference _range = variable.getRange(); - final VLSFunction eq = this.duplicate(CollectionsUtil.lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), CollectionsUtil.lookup(variable, variableMap)); + final VLSFunction eq = this.duplicate(CollectionsUtil.lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), + CollectionsUtil.lookup(variable, variableMap)); typedefs.add(eq); } } 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 b8d74f36..ec759ebf 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,8 +3,10 @@ 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.VLSAnd; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; +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.VLSFunction; @@ -18,7 +20,6 @@ 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; @@ -56,6 +57,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setName("A"); }; final VLSVariable variable = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + int globalCounter = 0; for (final Type type : types) { { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); @@ -92,7 +94,31 @@ public class Logic2VampireLanguageMapper_TypeMapper { }; final VLSFunction enumElemPred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); trace.element2Predicate.put(e, enumElemPred); - orElems.add(enumElemPred); + } + } + final List possibleNots = CollectionLiterals.newArrayList(); + final List typeDefs = CollectionLiterals.newArrayList(); + EList _elements_1 = type_1.getElements(); + for (final DefinedElement t1 : _elements_1) { + { + EList _elements_2 = type_1.getElements(); + for (final DefinedElement t2 : _elements_2) { + boolean _equals = Objects.equal(t1, t2); + if (_equals) { + final VLSFunction fct = this.support.duplicate(CollectionsUtil.lookup(t2, trace.element2Predicate), variable); + possibleNots.add(fct); + } else { + final VLSFunction op = this.support.duplicate(CollectionsUtil.lookup(t2, trace.element2Predicate), variable); + VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); + final Procedure1 _function_1 = (VLSUnaryNegation it) -> { + it.setOperand(op); + }; + final VLSUnaryNegation negFct = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_1); + possibleNots.add(negFct); + } + } + typeDefs.add(this.support.unfoldAnd(possibleNots)); + possibleNots.clear(); } } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); @@ -107,7 +133,13 @@ public class Logic2VampireLanguageMapper_TypeMapper { VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); final Procedure1 _function_3 = (VLSEquivalent it_2) -> { it_2.setLeft(CollectionsUtil.lookup(type_1, trace.type2Predicate)); - it_2.setRight(this.support.unfoldOr(orElems)); + VLSAnd _createVLSAnd = this.factory.createVLSAnd(); + final Procedure1 _function_4 = (VLSAnd it_3) -> { + it_3.setLeft(this.support.topLevelTypeFunc(variable)); + it_3.setRight(this.support.unfoldOr(typeDefs)); + }; + VLSAnd _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function_4); + it_2.setRight(_doubleArrow); }; VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); it_1.setOperand(_doubleArrow); @@ -118,8 +150,7 @@ 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++) { + for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { { final int num = (i + 1); VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); @@ -129,38 +160,50 @@ 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 VLSFunction fct = this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); - enumScopeElems.add(fct); - for (int j = 0; (j < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); j++) { - if ((j != i)) { - final VLSFunction op = this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(j), trace.element2Predicate), cstTerm); - VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_3 = (VLSUnaryNegation it) -> { - it.setOperand(op); + final int index = i; + VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); + final Procedure1 _function_3 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], + type_1.getElements().get(index).getName().split(" ")[0])); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_4 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(variable); + _variables.add(_duplicate); + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function_5 = (VLSEquivalent it_2) -> { + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function_6 = (VLSEquality it_3) -> { + it_3.setLeft(this.support.duplicate(variable)); + it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); + }; + VLSEquality _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_6); + it_2.setLeft(_doubleArrow); + it_2.setRight(this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); }; - final VLSUnaryNegation negFct = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); - enumScopeElems.add(negFct); - } - } + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_5); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula enumScope = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_3); + EList _formulas_1 = trace.specification.getFormulas(); + _formulas_1.add(enumScope); } } - 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); + int _globalCounter = globalCounter; + int _size = type_1.getElements().size(); + globalCounter = (_globalCounter + _size); } } final Function1 _function_1 = (Type it) -> { boolean _isIsAbstract = it.isIsAbstract(); return Boolean.valueOf((!_isIsAbstract)); }; - Iterable _filter_1 = Iterables.filter(IterableExtensions.filter(types, _function_1), TypeDeclaration.class); - for (final TypeDeclaration t1 : _filter_1) { + Iterable _filter_1 = IterableExtensions.filter(types, _function_1); + for (final Type t1 : _filter_1) { { for (final Type t2 : types) { if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { -- cgit v1.2.3-54-g00ecf