From 56df1f808fa2289c3e97d45d84bce8acc8937280 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 --- ...ic2VampireLanguageMapper_ContainmentMapper.java | 180 +++++++++++++++++++++ 1 file changed, 180 insertions(+) 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/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java') 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); + } + } + } + } +} -- cgit v1.2.3-70-g09d2