From 4aee5bcc86b9e6b515fbbdac030df42147be7dc1 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Sun, 8 Sep 2019 16:12:55 -0400 Subject: VAMPIRE: Implement wf constraint handling --- ...Logic2VampireLanguageMapper_RelationMapper.java | 92 ++++++++++++++++++++-- 1 file changed, 86 insertions(+), 6 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java') 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 143d3db5..c175c72a 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,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.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; @@ -17,11 +18,15 @@ 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.HashMap; import java.util.List; +import java.util.Map; import org.eclipse.emf.common.util.EList; +import org.eclipse.xtext.xbase.lib.CollectionLiterals; import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.ExclusiveRange; import org.eclipse.xtext.xbase.lib.Extension; @@ -41,7 +46,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { this.base = base; } - public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { + public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { final List relVar2VLS = new ArrayList(); final List relVar2TypeDecComply = new ArrayList(); int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; @@ -109,19 +114,94 @@ public class Logic2VampireLanguageMapper_RelationMapper { _formulas.add(comply); } - public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { + public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { + final Map relVar2VLS = new HashMap(); + final List vars = CollectionLiterals.newArrayList(); + final List relVar2TypeDecComply = new ArrayList(); + int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; + ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); + for (final Integer i : _doubleDotLessThan) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function = (VLSVariable it) -> { + it.setName(this.support.toIDMultiple("V", i.toString())); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + relVar2VLS.put(r.getVariables().get((i).intValue()), v); + vars.add(v); + TypeReference _get = r.getParameters().get((i).intValue()); + final Type relType = ((ComplexTypeReference) _get).getReferred(); + final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.lookup(relType, trace.type2Predicate), v); + 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; + final VLSTerm definition = mapper.transformTerm(r.getValue(), trace, relVar2VLS); + final VLSTerm compliance = this.support.unfoldAnd(relVar2TypeDecComply); + VLSAnd _createVLSAnd = this.factory.createVLSAnd(); + final Procedure1 _function = (VLSAnd it) -> { + it.setLeft(compliance); + it.setRight(definition); + }; + final VLSAnd compDefn = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function); + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function_1 = (VLSFofFormula it) -> { + it.setName(this.support.toID(relName)); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { + for (final VLSVariable v : vars) { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(v); + _variables.add(_duplicate); + } + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_3 = (VLSImplies it_2) -> { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_4 = (VLSFunction it_3) -> { + it_3.setConstant(this.support.toIDMultiple("r", relName)); + for (final VLSVariable v_1 : vars) { + EList _terms = it_3.getTerms(); + VLSVariable _duplicate_1 = this.support.duplicate(v_1); + _terms.add(_duplicate_1); + } + }; + final VLSFunction rel = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_4); + trace.relDef2Predicate.put(r, rel); + trace.predicate2RelDef.put(rel, r); + it_2.setLeft(this.support.duplicate(rel)); + it_2.setRight(compDefn); + }; + 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 relDef = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(relDef); } - public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { + public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { if (r instanceof RelationDeclaration) { - _transformRelation((RelationDeclaration)r, trace); + _transformRelation((RelationDeclaration)r, trace, mapper); return; } else if (r instanceof RelationDefinition) { - _transformRelation((RelationDefinition)r, trace); + _transformRelation((RelationDefinition)r, trace, mapper); return; } else { throw new IllegalArgumentException("Unhandled parameter types: " + - Arrays.asList(r, trace).toString()); + Arrays.asList(r, trace, mapper).toString()); } } } -- cgit v1.2.3-54-g00ecf