From 1cdcfeeda9f2d35655ffec9fca9f64f92101ce53 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 6 Mar 2019 17:46:15 -0500 Subject: Fix Enum handling for Paradox Integration --- .../Logic2VampireLanguageMapper_TypeMapper.xtend | 14 +++++++++++++- .../.Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 9388 -> 9592 bytes .../Logic2VampireLanguageMapper_TypeMapper.java | 13 ++++++++++++- .../output/FAMTest/vampireProblem.tptp | 2 +- 4 files changed, 26 insertions(+), 3 deletions(-) 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 f2a7b3f2..ee6365dd 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 @@ -90,7 +90,7 @@ class Logic2VampireLanguageMapper_TypeMapper { trace.specification.formulas += res // Create objects for the enum elements - val List enumScopeElems = newArrayList + val List enumScopeElems = newArrayList for (var i = 0; i < type.elements.length; i++) { val num = i + 1 val cstTerm = createVLSFunctionAsTerm => [ @@ -100,6 +100,18 @@ class Logic2VampireLanguageMapper_TypeMapper { trace.uniqueInstances.add(cst) val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm) enumScopeElems.add(fct) + + //For paradox Only + for (var j = 0; j < type.elements.length; j++) { + if(j != i) { + val op = support.duplicate(type.elements.get(j).lookup(trace.element2Predicate), cstTerm) + val negFct = createVLSUnaryNegation => [ + it.operand = op + ] + enumScopeElems.add(negFct) + } + } + //End Paradox // enumScopeElems.add(support.topLevelTypeFunc(cstTerm)) } 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 e85b5240..8a6f30f9 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/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 f776371b..c101aa4c 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 @@ -111,7 +111,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); EList _formulas = trace.specification.getFormulas(); _formulas.add(res); - final List enumScopeElems = CollectionLiterals.newArrayList(); + final List enumScopeElems = CollectionLiterals.newArrayList(); for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) { { final int num = (i + 1); @@ -124,6 +124,17 @@ public class Logic2VampireLanguageMapper_TypeMapper { trace.uniqueInstances.add(cst); final VLSFunction fct = this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); enumScopeElems.add(fct); + for (int j = 0; (j < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); j++) { + if ((j != i)) { + final VLSFunction op = this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(j), trace.element2Predicate), cstTerm); + VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); + final Procedure1 _function_3 = (VLSUnaryNegation it) -> { + it.setOperand(op); + }; + final VLSUnaryNegation negFct = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); + enumScopeElems.add(negFct); + } + } } } VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp index c492b66d..a3b9c865 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp @@ -1,6 +1,6 @@ % This is an initial Test Comment fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) . -fof ( enumScope_FunctionType , axiom , e_Root_FunctionType ( eo1 ) & ( e_Intermediate_FunctionType ( eo2 ) & e_Leaf_FunctionType ( eo3 ) ) ) . +fof ( enumScope_FunctionType , axiom , e_Root_FunctionType ( eo1 ) & ( ~ e_Intermediate_FunctionType ( eo1 ) & ( ~ e_Leaf_FunctionType ( eo1 ) & ( e_Intermediate_FunctionType ( eo2 ) & ( ~ e_Root_FunctionType ( eo2 ) & ( ~ e_Leaf_FunctionType ( eo2 ) & ( e_Leaf_FunctionType ( eo3 ) & ( ~ e_Root_FunctionType ( eo3 ) & ~ e_Intermediate_FunctionType ( eo3 ) ) ) ) ) ) ) ) ) . fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FunctionalData ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & t_Function ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . fof ( typeScope , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) => object ( A ) ) ) . fof ( typeUniqueness , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo2 != eo3 & ( eo1 != o1 & ( eo2 != o1 & ( eo3 != o1 & ( eo1 != o2 & ( eo2 != o2 & ( eo3 != o2 & ( o1 != o2 & ( eo1 != o3 & ( eo2 != o3 & ( eo3 != o3 & ( o1 != o3 & ( o2 != o3 & ( eo1 != o4 & ( eo2 != o4 & ( eo3 != o4 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( eo1 != o5 & ( eo2 != o5 & ( eo3 != o5 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . -- cgit v1.2.3-54-g00ecf