From 54431d1418fd4133a49605b804c10dd523c4c30d Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 6 Mar 2019 02:59:19 -0500 Subject: Continue improving code style (need sleep) --- .../builder/Logic2VampireLanguageMapper.xtend | 16 ++-- ...ogic2VampireLanguageMapper_RelationMapper.xtend | 31 +++----- .../Logic2VampireLanguageMapper_Support.xtend | 92 ++++++++-------------- 3 files changed, 51 insertions(+), 88 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index 54c44c72..81af24e5 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend @@ -40,6 +40,7 @@ import java.util.Map import org.eclipse.xtend.lib.annotations.Accessors import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration class Logic2VampireLanguageMapper { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -227,18 +228,18 @@ class Logic2VampireLanguageMapper { // def dispatch protected VLSTerm transformTerm(Forall forall, Logic2VampireLanguageMapperTrace trace, Map variables) { - support.createUniversallyQuantifiedExpression(this, forall, trace, variables) + support.createQuantifiedExpression(this, forall, trace, variables, true) } def dispatch protected VLSTerm transformTerm(Exists exists, Logic2VampireLanguageMapperTrace trace, Map variables) { - support.createExistentiallyQuantifiedExpression(this, exists, trace, variables) + support.createQuantifiedExpression(this, exists, trace, variables, false) } def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map variables) { return createVLSFunction => [ - it.constant = support.toIDMultiple("t", (instanceOf.range as ComplexTypeReference).referred.name) + it.constant = (instanceOf.range as ComplexTypeReference).referred.lookup(trace.type2Predicate).constant it.terms += instanceOf.value.transformTerm(trace, variables) ] } @@ -292,13 +293,8 @@ class Logic2VampireLanguageMapper { Logic2VampireLanguageMapperTrace trace, Map variables) { // cannot treat variable as function (constant) because of name ID not being the same - // below does not work - val res = createVLSVariable => [ -// it.name = support.toIDMultiple("Var", variable.lookup(variables).name) - it.name = support.toID(variable.lookup(variables).name) - ] // no need for potprocessing cuz booleans are supported - return res + return support.duplicate(variable.lookup(variables)) } // TODO @@ -383,7 +379,7 @@ class Logic2VampireLanguageMapper { // it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] // ] return createVLSFunction => [ - it.constant = support.toIDMultiple("rel", relation.name) + it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] ] } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend index 23b57701..deb24778 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend @@ -30,15 +30,13 @@ class Logic2VampireLanguageMapper_RelationMapper { // 1.1 if variable has type, creating list of type declarations val List relVar2VLS = new ArrayList val List relVar2TypeDecComply = new ArrayList - val typedefs = new ArrayList - for (i : 0 ..< r.parameters.length) { val v = createVLSVariable => [ it.name = support.toIDMultiple("V", i.toString) ] relVar2VLS.add(v) - + val relType = (r.parameters.get(i) as ComplexTypeReference).referred val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v) relVar2TypeDecComply.add(varTypeComply) @@ -47,33 +45,26 @@ class Logic2VampireLanguageMapper_RelationMapper { val comply = createVLSFofFormula => [ val nameArray = r.name.split(" ") - it.name = support.toIDMultiple("compliance", nameArray.get(0), - nameArray.get(2)) + it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2)) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ - for (v : relVar2VLS) { it.variables += support.duplicate(v) } - it.operand = createVLSImplies => [ - it.left = createVLSFunction => [ - it.constant = support.toIDMultiple("rel", r.name) - - for (i : 0 ..< r.parameters.length) { - val v = createVLSVariable => [ - it.name = relVar2VLS.get(i).name - ] - it.terms += v + val rel = createVLSFunction => [ + it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2)) + for (v : relVar2VLS) { + it.terms += support.duplicate(v) } - ] + trace.rel2Predicate.put(r, rel) + it.left = support.duplicate(rel) it.right = support.unfoldAnd(relVar2TypeDecComply) ] ] ] - // trace.relationDefinition2Predicate.put(r,res) trace.specification.formulas += comply } @@ -100,9 +91,8 @@ class Logic2VampireLanguageMapper_RelationMapper { relationVar2TypeDecComply.put(variable, varTypeComply) relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) } - + val nameArray = reldef.name.split(" ") val comply = createVLSFofFormula => [ - val nameArray = reldef.name.split(" ") it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), nameArray.get(nameArray.length - 1)) it.fofRole = "axiom" @@ -127,7 +117,8 @@ class Logic2VampireLanguageMapper_RelationMapper { ] val res = createVLSFofFormula => [ - it.name = support.toIDMultiple("relation", reldef.name) + it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2), + nameArray.get(nameArray.length - 1)) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ for (variable : reldef.variables) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index 090cf916..d3595a73 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend @@ -17,6 +17,8 @@ import java.util.List import java.util.Map import org.eclipse.emf.common.util.EList +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + class Logic2VampireLanguageMapper_Support { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -29,28 +31,27 @@ class Logic2VampireLanguageMapper_Support { ids.split("\\s+").join("_") } - //Term Handling - //TODO Make more general + // Term Handling + // TODO Make more general def protected VLSVariable duplicate(VLSVariable term) { return createVLSVariable => [it.name = term.name] } - + def protected VLSFunction duplicate(VLSFunction term) { return createVLSFunction => [ it.constant = term.constant - for ( v : term.terms){ + for (v : term.terms) { it.terms += duplicate(v as VLSVariable) } - ] + ] } - + def protected VLSFunction duplicate(VLSFunction term, VLSVariable v) { return createVLSFunction => [ it.constant = term.constant it.terms += duplicate(v) - ] + ] } - def protected VLSFunction topLevelTypeFunc() { return createVLSFunction => [ @@ -60,24 +61,22 @@ class Logic2VampireLanguageMapper_Support { ] ] } - - //TODO Make more general + + // TODO Make more general def establishUniqueness(List terms) { val List eqs = newArrayList - for (t1 : terms.subList(1, terms.length)){ - for (t2 : terms.subList(0, terms.indexOf(t1))){ + for (t1 : terms.subList(1, terms.length)) { + for (t2 : terms.subList(0, terms.indexOf(t1))) { val eq = createVLSInequality => [ - //TEMP + // TEMP it.left = createVLSConstant => [it.name = t2.name] it.right = createVLSConstant => [it.name = t1.name] - //TEMP + // TEMP ] eqs.add(eq) - } + } } - return unfoldAnd(eqs) - } // Support Functions @@ -108,6 +107,7 @@ class Logic2VampireLanguageMapper_Support { throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP } + // can delete below def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList operands, Logic2VampireLanguageMapperTrace trace, Map variables) { if (operands.size == 1) { @@ -143,58 +143,36 @@ class Logic2VampireLanguageMapper_Support { * } */ // QUANTIFIERS + VARIABLES - def protected VLSTerm createUniversallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, - QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables) { + def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, + QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables, boolean isUniversal) { val variableMap = expression.quantifiedVariables.toInvertedMap [ v | - createVLSVariable => [it.name = toIDMultiple("Var", v.name)] + createVLSVariable => [it.name = toIDMultiple("V", v.name)] ] val typedefs = new ArrayList for (variable : expression.quantifiedVariables) { - val eq = createVLSFunction => [ - it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) - it.terms += createVLSVariable => [ - it.name = toIDMultiple("Var", variable.name) - ] - - ] + val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), variable.lookup(variableMap)) typedefs.add(eq) } - - createVLSUniversalQuantifier => [ - it.variables += variableMap.values - it.operand = createVLSImplies => [ - it.left = unfoldAnd(typedefs) - it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)) + if (isUniversal) { + createVLSUniversalQuantifier => [ + it.variables += variableMap.values + it.operand = createVLSImplies => [ + it.left = unfoldAnd(typedefs) + it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)) + ] ] - ] - } + } else { + typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))) + createVLSExistentialQuantifier => [ + it.variables += variableMap.values + it.operand = unfoldAnd(typedefs) - def protected VLSTerm createExistentiallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, - QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables) { - val variableMap = expression.quantifiedVariables.toInvertedMap [ v | - createVLSVariable => [it.name = toIDMultiple("Var", v.name)] - ] - - val typedefs = new ArrayList - for (variable : expression.quantifiedVariables) { - val eq = createVLSFunction => [ - it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) - it.terms += createVLSVariable => [ - it.name = toIDMultiple("Var", variable.name) - ] ] - typedefs.add(eq) } - typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))) - createVLSExistentialQuantifier => [ - it.variables += variableMap.values - it.operand = unfoldAnd(typedefs) - - ] } - + def protected boolean dfsSupertypeCheck(Type type, Type type2) { // There is surely a better way to do this if (type.supertypes.isEmpty) @@ -213,7 +191,5 @@ class Logic2VampireLanguageMapper_Support { def protected withAddition(Map map1, Map map2) { new HashMap(map1) => [putAll(map2)] } - - } -- cgit v1.2.3-54-g00ecf