From 35ac37963fc3e3f3fb142aaf1fdffd26e05e473a Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 2 Sep 2019 03:47:21 -0400 Subject: VAMPIRE: implement Vampire Model Interpreter, 2/3 done --- .../builder/Logic2VampireLanguageMapperTrace.xtend | 1 + .../Logic2VampireLanguageMapper_TypeMapper.xtend | 1 + .../builder/VampireModelInterpretation.xtend | 167 ++++++++++++++++++--- .../vampire/reasoner/.VampireSolver.xtendbin | Bin 6957 -> 6957 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 17754 -> 17726 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 4692 -> 4773 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3165 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 11835 -> 11807 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 6497 -> 6467 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 10701 -> 10676 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13083 -> 13060 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11170 -> 11170 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 3858 -> 3858 bytes .../builder/Logic2VampireLanguageMapperTrace.java | 2 + ...ic2VampireLanguageMapper_ContainmentMapper.java | 20 +-- ...Logic2VampireLanguageMapper_RelationMapper.java | 4 +- .../Logic2VampireLanguageMapper_ScopeMapper.java | 4 +- .../Logic2VampireLanguageMapper_Support.java | 10 +- .../Logic2VampireLanguageMapper_TypeMapper.java | 11 +- 19 files changed, 179 insertions(+), 41 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend index e94584ae..7ab15fba 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend @@ -35,6 +35,7 @@ class Logic2VampireLanguageMapperTrace { public var topLevelType = null public val Map type2Predicate = new HashMap; + public val Map predicate2Type = new HashMap; public val Map element2Predicate = new HashMap public val Map type2PossibleNot = new HashMap public val Map type2And = new HashMap diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend index 1b30393f..d2a01e0e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend @@ -42,6 +42,7 @@ class Logic2VampireLanguageMapper_TypeMapper { it.terms += support.duplicate(variable) ] trace.type2Predicate.put(type, typePred) + trace.predicate2Type.put(typePred, type) } // 2. Map each ENUM/InitialModelElement type definition to fof formula diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend index c2cffa6b..0c93e3fe 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend @@ -1,49 +1,182 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder +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.VLSFunction +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel +import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAndImpl +import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSOrImpl +import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSUnaryNegationImpl import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory 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.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl +import java.util.HashMap +import java.util.List +import java.util.Map + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* class VampireModelInterpretation implements LogicModelInterpretation { protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE - + protected val Logic2VampireLanguageMapperTrace forwardTrace; - - + + private val Map name2DefinedElement = new HashMap + private val Map> type2DefinedElement = new HashMap + + var num = -1 + public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) { this.forwardTrace = trace + + // 1. look at "finite_domain" formula (there should only be one) + // IN REALITY THE DEFINED ELEMENTS ARE DEFINED AS :$i + // SPECIFICALLY, THESE ARE "TYPE" FORMULAS + val finDomFormula = model.tfformulas.filter[name == "finite_domain"].get(0) as VLSTffFormula + val univQuant = finDomFormula.fofFormula as VLSUniversalQuantifier + var orFormulaTerm = univQuant.operand + + var end = false + while (!end) { + if (orFormulaTerm.class == VLSOrImpl) { + val orFormula = orFormulaTerm as VLSOr + val orRight = orFormula.right as VLSEquality + add2ConstDefMap(orRight) + orFormulaTerm = orFormula.left + } else { + val firstTerm = orFormulaTerm as VLSEquality + add2ConstDefMap(firstTerm) + end = true + } + + } + + // 2. associate each type to defined elements +// println(trace.type2Predicate.keySet) +// println(trace.type2Predicate.keySet.length) +// println(trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl]) +// println(trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl].length) +// println() +// println(trace.type2Predicate) + // Fill keys of map + val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl] + val allTypeFunctions = trace.predicate2Type + + for (type : allTypeDecls) { + type2DefinedElement.put(type as TypeDeclaration, newArrayList) + } + + // USE THE DECLARE_ FORMULAS TO SEE WHAT THE TYPES ARE + val typeFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_t_"] + // ^this way, we ignore the "object" type + //TODO potentially need to handle the enums in this case as well + for (formula : typeFormulas) { + // get associated type + val associatedTypeName = (formula as VLSTffFormula).name.substring(10) + val associatedFunction = allTypeFunctions.keySet.filter[constant == associatedTypeName]. + get(0) as VLSFunction + val associatedTypeAll = associatedFunction.lookup(allTypeFunctions) +// val associatedTypeDeclFormula = model.tfformulas.filter[name == ("declare_t_" + associatedTypeName)].get(0) as VLSTffFormula +// val associatedTypeDefn = associatedTypeDeclFormula.fofFormula as VLSOtherDeclaration +// val associatedTypeFct = associatedTypeDefn.name as VLSConstant + if (associatedTypeAll.class == TypeDeclarationImpl) { + val associatedType = associatedTypeAll as TypeDeclaration + + // get definedElements + var andFormulaTerm = formula.fofFormula + end = false + val List instances = newArrayList + while (!end) { + if (andFormulaTerm.class == VLSAndImpl) { + val andFormula = andFormulaTerm as VLSAnd + val andRight = andFormula.right + addIfNotNeg(andRight, instances) + andFormulaTerm = andFormula.left + } else { + addIfNotNeg(andFormulaTerm as VLSTerm, instances) + end = true + } + + } + for (elem : instances) { + associatedType.lookup(type2DefinedElement).add(elem) + } + } + } + + printMap() + } - - override getElements(Type type) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + + def printMap() { + for (key : type2DefinedElement.keySet) { + println(key.name + "==>") + for (elem : key.lookup(type2DefinedElement)) { + print(elem.name + ", ") + } + println() + + } + println() } - + + def private addIfNotNeg(VLSTerm term, List list) { + if (term.class != VLSUnaryNegationImpl) { + val nodeName = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor + val defnElem = nodeName.lookup(name2DefinedElement) + list.add(defnElem) + } + } + + def private add2ConstDefMap(VLSEquality eq) { + val defElemConst = (eq.right as VLSConstant) + val definedElement = createDefinedElement => [name = defElemConst.name] + this.name2DefinedElement.put(defElemConst.name, definedElement) + } + + override getElements(Type type) { getElementsDispatch(type) } + + def private dispatch getElementsDispatch(TypeDeclaration declaration) { + return declaration.lookup(this.type2DefinedElement) + } + + def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements } + override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { throw new UnsupportedOperationException("TODO: auto-generated method stub") } - + override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { throw new UnsupportedOperationException("TODO: auto-generated method stub") } - + override getInterpretation(ConstantDeclaration constant) { throw new UnsupportedOperationException("TODO: auto-generated method stub") } - + override getAllIntegersInStructure() { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + return null } - + override getAllRealsInStructure() { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + return null } - + override getAllStringsInStructure() { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + return null } - -} \ No newline at end of file + +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index 298a6c08..0fafa9e9 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 863b572e..7174bfba 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index 410f2550..af66dabc 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index b1b39a4f..b9301875 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index 3710e753..88c3e932 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index 9dc7abaf..e3437e53 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index 7029d196..1a884261 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 03aead59..7e2aba1c 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index 62960704..187a0447 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index 56a10b3c..ee115b16 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index c2ae099e..4537240e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java @@ -37,6 +37,8 @@ public class Logic2VampireLanguageMapperTrace { public final Map type2Predicate = new HashMap(); + public final Map predicate2Type = new HashMap(); + public final Map element2Predicate = new HashMap(); public final Map type2PossibleNot = new HashMap(); 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 index 7daf1b2f..2100b92f 100644 --- 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 @@ -12,10 +12,10 @@ 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.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; 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.VLSVariableDeclaration; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import com.google.common.base.Objects; import com.google.common.collect.Iterables; @@ -123,7 +123,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(this.variable); _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); @@ -193,10 +193,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { it.setFofRole("axiom"); VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_5 = (VLSExistentialQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(varA); _variables.add(_duplicate); - EList _variables_1 = it_1.getVariables(); + EList _variables_1 = it_1.getVariables(); VLSVariable _duplicate_1 = this.support.duplicate(varB); _variables_1.add(_duplicate_1); VLSImplies _createVLSImplies = this.factory.createVLSImplies(); @@ -206,10 +206,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { final Procedure1 _function_7 = (VLSUnaryNegation it_3) -> { VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_8 = (VLSExistentialQuantifier it_4) -> { - EList _variables_2 = it_4.getVariables(); + EList _variables_2 = it_4.getVariables(); VLSVariable _duplicate_2 = this.support.duplicate(varC); _variables_2.add(_duplicate_2); - EList _variables_3 = it_4.getVariables(); + EList _variables_3 = it_4.getVariables(); VLSVariable _duplicate_3 = this.support.duplicate(varB); _variables_3.add(_duplicate_3); it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.newArrayList(varC, varB))); @@ -240,7 +240,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(varA); _variables.add(_duplicate); VLSImplies _createVLSImplies = this.factory.createVLSImplies(); @@ -248,7 +248,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { it_2.setLeft(this.support.duplicate(e.getKey(), varA)); VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_7 = (VLSExistentialQuantifier it_3) -> { - EList _variables_1 = it_3.getVariables(); + EList _variables_1 = it_3.getVariables(); VLSVariable _duplicate_1 = this.support.duplicate(varB); _variables_1.add(_duplicate_1); int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; @@ -308,9 +308,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { final Procedure1 _function_6 = (VLSUnaryNegation it_1) -> { VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_7 = (VLSExistentialQuantifier it_2) -> { - EList _variables = it_2.getVariables(); + EList _variables = it_2.getVariables(); List _duplicate = this.support.duplicate(variables); - Iterables.addAll(_variables, _duplicate); + Iterables.addAll(_variables, _duplicate); it_2.setOperand(this.support.unfoldAnd(conjunctionList)); }; VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); 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 657c3292..8d36952b 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 @@ -7,9 +7,9 @@ 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.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; 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; @@ -77,7 +77,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { for (final VLSVariable v : relVar2VLS) { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(v); _variables.add(_duplicate); } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index 6d4767a7..6da75271 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java @@ -11,9 +11,9 @@ 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.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import com.google.common.base.Objects; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; @@ -245,7 +245,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(this.variable); _variables.add(_duplicate); VLSImplies _createVLSImplies = this.factory.createVLSImplies(); diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index 6cd53fae..dae0df6e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java @@ -11,9 +11,9 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import com.google.common.base.Objects; import com.google.common.collect.Iterables; @@ -324,9 +324,9 @@ public class Logic2VampireLanguageMapper_Support { if (isUniversal) { VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_1 = (VLSUniversalQuantifier it) -> { - EList _variables = it.getVariables(); + EList _variables = it.getVariables(); Collection _values = variableMap.values(); - Iterables.addAll(_variables, _values); + Iterables.addAll(_variables, _values); VLSImplies _createVLSImplies = this.factory.createVLSImplies(); final Procedure1 _function_2 = (VLSImplies it_1) -> { it_1.setLeft(this.unfoldAnd(typedefs)); @@ -342,9 +342,9 @@ public class Logic2VampireLanguageMapper_Support { typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_2 = (VLSExistentialQuantifier it) -> { - EList _variables = it.getVariables(); + EList _variables = it.getVariables(); Collection _values = variableMap.values(); - Iterables.addAll(_variables, _values); + Iterables.addAll(_variables, _values); it.setOperand(this.unfoldAnd(typedefs)); }; _xblockexpression_1 = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_2); 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 7921f204..c8888eb0 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 @@ -12,10 +12,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; 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.VLSVariableDeclaration; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import com.google.common.base.Objects; import com.google.common.collect.Iterables; @@ -76,6 +76,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { }; final VLSFunction typePred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); trace.type2Predicate.put(type, typePred); + trace.predicate2Type.put(typePred, type); } } final Function1 _function_1 = (TypeDefinition it) -> { @@ -144,7 +145,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_3 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(variable); _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); @@ -194,7 +195,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(variable); _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); @@ -264,7 +265,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(variable); _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); @@ -292,7 +293,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_6 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(variable); _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); -- cgit v1.2.3-54-g00ecf