From 96e6ef62e818ee3b5c15d107ad49a448abfd4cd1 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 6 Mar 2019 14:18:35 -0500 Subject: Restructure Vampire Reasoner project --- .../Logic2VampireLanguageMapper_TypeMapper.java | 183 ++++++++++++++++++++- 1 file changed, 175 insertions(+), 8 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java') 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 c55e2421..d3dddcfc 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 @@ -2,24 +2,191 @@ 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.VampireModelInterpretation_TypeInterpretation; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +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.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; +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.TypeDefinition; +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; +import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; +import java.util.ArrayList; 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.Extension; +import org.eclipse.xtext.xbase.lib.Functions.Function1; +import org.eclipse.xtext.xbase.lib.IterableExtensions; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @SuppressWarnings("all") -public interface Logic2VampireLanguageMapper_TypeMapper { - public abstract void transformTypes(final Collection types, final Collection elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); +public class Logic2VampireLanguageMapper_TypeMapper { + @Extension + private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; - public abstract List transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); + private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); - public abstract VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace); + private final Logic2VampireLanguageMapper base; - public abstract int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace); + public Logic2VampireLanguageMapper_TypeMapper(final Logic2VampireLanguageMapper base) { + LogicproblemPackage.eINSTANCE.getClass(); + this.base = base; + } - public abstract VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace); + protected boolean transformTypes(final Collection types, final Collection elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { + boolean _xblockexpression = false; + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function = (VLSVariable it) -> { + it.setName("A"); + }; + final VLSVariable variable = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + for (final Type type : types) { + { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_1 = (VLSFunction it) -> { + it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.support.duplicate(variable); + _terms.add(_duplicate); + }; + final VLSFunction typePred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + trace.type2Predicate.put(type, typePred); + } + } + Iterable _filter = Iterables.filter(types, TypeDefinition.class); + for (final TypeDefinition type_1 : _filter) { + { + final List orElems = CollectionLiterals.newArrayList(); + EList _elements = type_1.getElements(); + for (final DefinedElement e : _elements) { + { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_1 = (VLSFunction it) -> { + it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2])); + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.support.duplicate(variable); + _terms.add(_duplicate); + }; + final VLSFunction enumElemPred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + trace.element2Predicate.put(e, enumElemPred); + orElems.add(enumElemPred); + } + } + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function_1 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(variable); + _variables.add(_duplicate); + 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)); + }; + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(res); + } + } + 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) { + { + for (final Type t2 : types) { + if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { + trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); + } else { + VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); + final Procedure1 _function_2 = (VLSUnaryNegation it) -> { + it.setOperand(this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); + }; + VLSUnaryNegation _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_2); + trace.type2PossibleNot.put(t2, _doubleArrow); + } + } + Collection _values = trace.type2PossibleNot.values(); + ArrayList _arrayList = new ArrayList(_values); + trace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); + trace.type2PossibleNot.clear(); + } + } + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function_2 = (VLSFofFormula it) -> { + it.setName("hierarchyHandler"); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_3 = (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_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)); + }; + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula hierarch = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_2); + EList _formulas = trace.specification.getFormulas(); + _xblockexpression = _formulas.add(hierarch); + } + return _xblockexpression; + } - public abstract VampireModelInterpretation_TypeInterpretation getTypeInterpreter(); + protected void transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } + + protected void getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } + + protected void getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } + + protected VLSDoubleQuote transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { + VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); + final Procedure1 _function = (VLSDoubleQuote it) -> { + String _name = referred.getName(); + String _plus = ("\"a" + _name); + String _plus_1 = (_plus + "\""); + it.setValue(_plus_1); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSDoubleQuote, _function); + } + + protected void getTypeInterpreter() { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } } -- cgit v1.2.3-70-g09d2