From 9643b7b7a735afc408ca6a172e2719653553627a Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 4 Mar 2019 17:31:16 -0500 Subject: Begin handing of scope and fix type definitions. --- .../Logic2VampireLanguageMapper_Support.xtend | 45 ++++++++++++++-------- 1 file changed, 29 insertions(+), 16 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend') 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 ab92b42f..e69f0d51 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 @@ -1,17 +1,18 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm 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.QuantifiedExpression +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable import java.util.ArrayList import java.util.HashMap import java.util.List import java.util.Map -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference import org.eclipse.emf.common.util.EList -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term class Logic2VampireLanguageMapper_Support { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -25,6 +26,19 @@ class Logic2VampireLanguageMapper_Support { ids.split("\\s+").join("_") } + def protected VLSVariable duplicate(VLSVariable vrbl) { + return createVLSVariable => [it.name = vrbl.name] + } + + def protected VLSFunction topLevelTypeFunc() { + return createVLSFunction => [ + it.constant = "object" + it.terms += createVLSVariable => [ + it.name = "A" + ] + ] + } + // Support Functions // booleans // AND and OR @@ -41,7 +55,6 @@ class Logic2VampireLanguageMapper_Support { } def protected VLSTerm unfoldOr(List operands) { - // if(operands.size == 0) {basically return true} /*else*/ if (operands.size == 1) { return operands.head @@ -56,20 +69,21 @@ class Logic2VampireLanguageMapper_Support { def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList operands, Logic2VampireLanguageMapperTrace trace, Map variables) { - if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) } - else if(operands.size > 1) { - val notEquals = new ArrayList(operands.size*operands.size/2) - for(i:0..[ - it.left= m.transformTerm(operands.get(i),trace,variables) - it.right = m.transformTerm(operands.get(j),trace,variables) + if (operands.size == 1) { + return m.transformTerm(operands.head, trace, variables) + } else if (operands.size > 1) { + val notEquals = new ArrayList(operands.size * operands.size / 2) + for (i : 0 ..< operands.size) { + for (j : i + 1 ..< operands.size) { + notEquals += createVLSInequality => [ + it.left = m.transformTerm(operands.get(i), trace, variables) + it.right = m.transformTerm(operands.get(j), trace, variables) ] } } return notEquals.unfoldAnd - } - else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') + } else + throw new UnsupportedOperationException('''Logic operator with 0 operands!''') } // Symbolic @@ -105,7 +119,6 @@ class Logic2VampireLanguageMapper_Support { ] typedefs.add(eq) } - createVLSUniversalQuantifier => [ it.variables += variableMap.values -- cgit v1.2.3-54-g00ecf