From 5d1165ceef23e20c4bbe46fe6f88e95f317234b5 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 7 Oct 2019 00:35:42 -0400 Subject: VAMPIRE: Implement Vampire measurement code --- .../builder/VampireModelInterpretation.xtend | 28 ++++++++++++---------- 1 file changed, 16 insertions(+), 12 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend') 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 9eb47f41..063dcf2a 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 @@ -33,6 +33,7 @@ import java.util.Map import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition import java.util.concurrent.TimeUnit +import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTermImpl class VampireModelInterpretation implements LogicModelInterpretation { protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE @@ -79,10 +80,10 @@ class VampireModelInterpretation implements LogicModelInterpretation { // println() // println(trace.type2Predicate) // Fill keys of map - println(trace.type2Predicate.keySet) +// println(trace.type2Predicate.keySet) val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl] val allTypeFunctions = trace.predicate2Type - println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl]) +// println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl]) for (type : allTypeDecls) { type2DefinedElement.put(type as TypeDeclaration, newArrayList) @@ -97,7 +98,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { for (formula : typeFormulas) { // get associated type val associatedTypeName = (formula as VLSTffFormula).name.substring(10) - print(associatedTypeName) +// print(associatedTypeName) val associatedFunctions = allTypeFunctions.keySet.filter[constant == associatedTypeName] if (associatedFunctions.length > 0) { val associatedFunction = associatedFunctions.get(0) as VLSFunction @@ -132,7 +133,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { } - printMap() +// printMap() // 3. get relations // Fill keys of map @@ -153,6 +154,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { val relFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_r_"] for (formula : relFormulas) { +// println(formula) // get associated type val associatedRelName = (formula as VLSTffFormula).name.substring(10) @@ -169,7 +171,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { end = false val List instances = newArrayList while (!end) { - if (andFormulaTerm.class == VLSAndImpl) { + if (andFormulaTerm.class != null && andFormulaTerm.class == VLSAndImpl) { val andFormula = andFormulaTerm as VLSAnd val andRight = andFormula.right addRelIfNotNeg(andRight, instances) @@ -202,6 +204,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { } println() + println("--------END ELEMENTS MAP----------") } def printMap2() { @@ -226,7 +229,8 @@ class VampireModelInterpretation implements LogicModelInterpretation { } def private addRelIfNotNeg(VLSTerm term, List list) { - if (term.class != VLSUnaryNegationImpl) { +// println("xxx " + term.class) + if (term.class != VLSUnaryNegationImpl && term.class != VLSTermImpl) { val nodeName1 = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor val nodeName2 = ((term as VLSFunction).terms.get(1) as VLSFunctionAsTerm).functor val strArr = newArrayList(nodeName1, nodeName2) @@ -247,9 +251,9 @@ class VampireModelInterpretation implements LogicModelInterpretation { } def private dispatch getElementsDispatch(TypeDefinition declaration) { - println("~~" + declaration) - println(declaration.elements) - println() +// println("~~" + declaration) +// println(declaration.elements) +// println() return declaration.elements } @@ -258,18 +262,18 @@ class VampireModelInterpretation implements LogicModelInterpretation { } override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { - print("-- " + relation.name) +// print("-- " + relation.name) val node1 = (parameterSubstitution.get(0) as DefinedElement).name val node2 = (parameterSubstitution.get(1) as DefinedElement).name val realRelations = relation.lookup(relDec2Inst) for (real : realRelations) { if (real.contains(node1) && real.contains(node2)) { - println(" true") +// println(" true") TimeUnit.MILLISECONDS.sleep(10) return true } } - println(" false") +// println(" false") TimeUnit.MILLISECONDS.sleep(10) return false } -- cgit v1.2.3-54-g00ecf