From 2f8149678539a94f2f4ca2e7ff5640ff5d7087cc Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 15 Apr 2019 00:06:29 -0400 Subject: VAMPIRE: close #22, improve test structure for #39, .vql file trouble --- .../ide/.VampireLanguageIdeModule.xtendbin | Bin 1685 -> 1685 bytes .../ide/.VampireLanguageIdeSetup.xtendbin | Bin 2500 -> 2500 bytes .../ui/.VampireLanguageUiModule.xtendbin | Bin 2342 -> 2342 bytes .../.VampireLanguageProposalProvider.xtendbin | Bin 1792 -> 1792 bytes ...ampireLanguageDescriptionLabelProvider.xtendbin | Bin 1965 -> 1965 bytes .../.VampireLanguageLabelProvider.xtendbin | Bin 2405 -> 2405 bytes .../.VampireLanguageOutlineTreeProvider.xtendbin | Bin 1819 -> 1819 bytes .../.VampireLanguageQuickfixProvider.xtendbin | Bin 1786 -> 1786 bytes .../.VampireLanguageRuntimeModule.xtendbin | Bin 1706 -> 1706 bytes .../.VampireLanguageStandaloneSetup.xtendbin | Bin 1980 -> 1980 bytes .../formatting2/.VampireLanguageFormatter.xtendbin | Bin 4130 -> 4130 bytes .../generator/.VampireLanguageGenerator.xtendbin | Bin 2338 -> 2338 bytes .../scoping/.VampireLanguageScopeProvider.xtendbin | Bin 1751 -> 1751 bytes .../validation/.VampireLanguageValidator.xtendbin | Bin 1736 -> 1736 bytes ...c2VampireLanguageMapper_ContainmentMapper.xtend | 12 +- ...ogic2VampireLanguageMapper_RelationMapper.xtend | 183 +++++++++++---------- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 1 + .../Logic2VampireLanguageMapper_Support.xtend | 12 +- .../Logic2VampireLanguageMapper_TypeMapper.xtend | 23 ++- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2691 -> 2691 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18156 -> 18156 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 4215 -> 4215 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 10551 -> 10674 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8209 -> 6457 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 9839 -> 9839 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13093 -> 13046 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 10705 -> 10792 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 1720 -> 1720 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 4908 -> 4908 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes ...ic2VampireLanguageMapper_ContainmentMapper.java | 15 +- ...Logic2VampireLanguageMapper_RelationMapper.java | 159 ++---------------- .../Logic2VampireLanguageMapper_Support.java | 18 +- .../Logic2VampireLanguageMapper_TypeMapper.java | 25 +-- 37 files changed, 169 insertions(+), 279 deletions(-) (limited to 'Solvers/Vampire-Solver') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin index 024dcab9..10495630 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin index 7e128ad1..295d9ec2 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin index 0bf8ccc6..83b00f77 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin index 58a18bbb..f8a7a2f3 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin index 205afcc4..544f5811 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin index b388bd43..62aac4ca 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin index 3092be97..31d4543e 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin index 8b23f34d..7b230b65 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin index 84682c47..a24c2795 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin index e3f67a0c..b35605ae 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin index bf354098..5e9cd3bd 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin index da62f4c1..0001d80f 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin index 482b884e..b189414a 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin index 81c1f803..b4eec95c 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index 395b4305..8e0e0b11 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend @@ -39,7 +39,15 @@ class Logic2VampireLanguageMapper_ContainmentMapper { for (l : relationsList) { var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type containmentListCopy.remove(pointingTo) - for (c : pointingTo.subtypes) { + var List allSubtypes = newArrayList + support.listSubtypes(pointingTo, allSubtypes) + for (c : allSubtypes) { + containmentListCopy.remove(c) + } + } + + for (c : containmentListCopy) { + if(c.isIsAbstract) { containmentListCopy.remove(c) } } @@ -135,7 +143,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { // STEP 2 CONT'D for (e : type2cont.entrySet) { val relFormula = createVLSFofFormula => [ - it.name = support.toIDMultiple("containment", e.key.constant.toString) + it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ 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 0ae06bc3..2dec281d 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 @@ -44,9 +44,20 @@ class Logic2VampireLanguageMapper_RelationMapper { } + //deciding name of relation + val nameArray = r.name.split(" ") + var relNameVar = "" + if (nameArray.length == 3) { + relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) + } + else { + relNameVar = r.name + } + val relName = relNameVar + val comply = createVLSFofFormula=> [ - val nameArray = r.name.split(" ") - it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2)) + + it.name = support.toIDMultiple("compliance", relName) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ for (v : relVar2VLS) { @@ -54,7 +65,7 @@ class Logic2VampireLanguageMapper_RelationMapper { } it.operand = createVLSImplies => [ val rel = createVLSFunction => [ - it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2)) + it.constant = support.toIDMultiple("r", relName) for (v : relVar2VLS) { it.terms += support.duplicate(v) } @@ -71,89 +82,89 @@ class Logic2VampireLanguageMapper_RelationMapper { def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) { - // 1. store all variables in support wrt their name - // 1.1 if variable has type, creating list of type declarations -// val VLSVariable variable = createVLSVariable => [it.name = "A"] - val Map relationVar2VLS = new HashMap - val Map relationVar2TypeDecComply = new HashMap - val Map relationVar2TypeDecRes = new HashMap - val typedefs = new ArrayList - - for (variable : reldef.variables) { - val v = createVLSVariable => [ - it.name = support.toIDMultiple("V", variable.name) - ] - relationVar2VLS.put(variable, v) - - val varTypeComply = createVLSFunction => [ - it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) - it.terms += support.duplicate(v) - ] - relationVar2TypeDecComply.put(variable, varTypeComply) - relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) - } - val nameArray = reldef.name.split(" ") - val comply = createVLSFofFormula => [ - it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), - nameArray.get(nameArray.length - 1)) - it.fofRole = "axiom" - it.fofFormula = createVLSUniversalQuantifier => [ - for (variable : reldef.variables) { - it.variables += support.duplicate(variable.lookup(relationVar2VLS)) - - } - it.operand = createVLSImplies => [ - it.left = createVLSFunction => [ - it.constant = support.toIDMultiple("rel", reldef.name) - for (variable : reldef.variables) { - val v = createVLSVariable => [ - it.name = variable.lookup(relationVar2VLS).name - ] - it.terms += v - } - ] - it.right = support.unfoldAnd(new ArrayList(relationVar2TypeDecComply.values)) - ] - ] - ] - - val res = createVLSFofFormula => [ - 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) { - val v = createVLSVariable => [ - it.name = variable.lookup(relationVar2VLS).name - ] - it.variables += v - - } - it.operand = createVLSImplies => [ - it.left = support.unfoldAnd(new ArrayList(relationVar2TypeDecRes.values)) - it.right = createVLSEquivalent => [ - it.left = createVLSFunction => [ - it.constant = support.toIDMultiple("rel", reldef.name) - for (variable : reldef.variables) { - val v = createVLSVariable => [ - it.name = variable.lookup(relationVar2VLS).name - ] - it.terms += v - - } - ] - it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) - ] - - ] - - ] - - ] - - // trace.relationDefinition2Predicate.put(r,res) - trace.specification.formulas += comply; - trace.specification.formulas += res; +// // 1. store all variables in support wrt their name +// // 1.1 if variable has type, creating list of type declarations +//// val VLSVariable variable = createVLSVariable => [it.name = "A"] +// val Map relationVar2VLS = new HashMap +// val Map relationVar2TypeDecComply = new HashMap +// val Map relationVar2TypeDecRes = new HashMap +// val typedefs = new ArrayList +// +// for (variable : reldef.variables) { +// val v = createVLSVariable => [ +// it.name = support.toIDMultiple("V", variable.name) +// ] +// relationVar2VLS.put(variable, v) +// +// val varTypeComply = createVLSFunction => [ +// it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) +// it.terms += support.duplicate(v) +// ] +// relationVar2TypeDecComply.put(variable, varTypeComply) +// relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) +// } +// val nameArray = reldef.name.split(" ") +// val comply = createVLSFofFormula => [ +// it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), +// nameArray.get(nameArray.length - 1)) +// it.fofRole = "axiom" +// it.fofFormula = createVLSUniversalQuantifier => [ +// for (variable : reldef.variables) { +// it.variables += support.duplicate(variable.lookup(relationVar2VLS)) +// +// } +// it.operand = createVLSImplies => [ +// it.left = createVLSFunction => [ +// it.constant = support.toIDMultiple("rel", reldef.name) +// for (variable : reldef.variables) { +// val v = createVLSVariable => [ +// it.name = variable.lookup(relationVar2VLS).name +// ] +// it.terms += v +// } +// ] +// it.right = support.unfoldAnd(new ArrayList(relationVar2TypeDecComply.values)) +// ] +// ] +// ] +// +// val res = createVLSFofFormula => [ +// 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) { +// val v = createVLSVariable => [ +// it.name = variable.lookup(relationVar2VLS).name +// ] +// it.variables += v +// +// } +// it.operand = createVLSImplies => [ +// it.left = support.unfoldAnd(new ArrayList(relationVar2TypeDecRes.values)) +// it.right = createVLSEquivalent => [ +// it.left = createVLSFunction => [ +// it.constant = support.toIDMultiple("rel", reldef.name) +// for (variable : reldef.variables) { +// val v = createVLSVariable => [ +// it.name = variable.lookup(relationVar2VLS).name +// ] +// it.terms += v +// +// } +// ] +// it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) +// ] +// +// ] +// +// ] +// +// ] +// +// // trace.relationDefinition2Predicate.put(r,res) +// trace.specification.formulas += comply; +// trace.specification.formulas += res; } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index 0a8812e4..4a8d2827 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend @@ -29,6 +29,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS // TODO HANDLE // 1. make a list of constants equaling the min number of specified objects + //These numbers do not include enums or initial model elements val GLOBAL_MIN = config.typeScopes.minNewElements val GLOBAL_MAX = config.typeScopes.maxNewElements 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 195b89bb..680213ab 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 @@ -273,15 +273,11 @@ class Logic2VampireLanguageMapper_Support { } } - def protected List listSubtypes(Type t) { - var List allSubtypes = newArrayList - if (!t.subtypes.isEmpty) { - for (subt : t.subtypes) { - allSubtypes.add(subt) - allSubtypes = listSubtypes(subt) - } + def protected void listSubtypes(Type t, List allSubtypes) { + for (subt : t.subtypes) { + allSubtypes.add(subt) + listSubtypes(subt, allSubtypes) } - return allSubtypes } def protected withAddition(Map map1, Map map2) { 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 3bc945df..2f3af593 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 @@ -44,14 +44,19 @@ class Logic2VampireLanguageMapper_TypeMapper { // Create a VLSFunction for each Enum Element val List orElems = newArrayList + for (e : type.elements) { + val nameArray = e.name.split(" ") + var relNameVar = "" + if (nameArray.length == 3) { + relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) + } else { + relNameVar = e.name + } + val relName = relNameVar + val enumElemPred = createVLSFunction => [ - val splitName = e.name.split(" ") - if (splitName.length > 2) { - it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) - } else { - it.constant = support.toIDMultiple("e", splitName.get(0)) - } + it.constant = support.toIDMultiple("e", relName) it.terms += support.duplicate(variable) ] trace.element2Predicate.put(e, enumElemPred) @@ -80,7 +85,7 @@ class Logic2VampireLanguageMapper_TypeMapper { // Implement Enum Inheritence Hierarchy val res = createVLSFofFormula => [ - it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) + it.name = support.toIDMultiple("typeDef", type.lookup(trace.type2Predicate).constant.toString) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ it.variables += support.duplicate(variable) @@ -105,9 +110,9 @@ class Logic2VampireLanguageMapper_TypeMapper { val cst = support.toConstant(cstTerm) trace.uniqueInstances.add(cst) - val index = i + val index = i-globalCounter val enumScope = createVLSFofFormula => [ - it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0), + it.name = support.toIDMultiple("enumScope", type.lookup(trace.type2Predicate).constant.toString, type.elements.get(index).name.split(" ").get(0)) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 43e1e477..1ea7e30a 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin differ 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 4e6f6ca0..ee06cb39 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 707a6089..648d9600 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 3171324f..a02821a5 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 301df7fa..b01f92a6 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 5e53ea26..7634af4b 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 b378ed09..4906adfc 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 605ac88c..e2c945e3 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 0c289e29..f465506c 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 cb72fd90..e046604a 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 cfe1e8cd..aff62dca 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/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index c2079147..7212cce7 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index 3c70bc14..d23bacad 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index 9ef20b23..be78cace 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.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.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index 4cdc7e6a..9deab87f 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 @@ -64,12 +64,19 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { Type _referred = ((ComplexTypeReference) _get).getReferred(); Type pointingTo = ((Type) _referred); containmentListCopy.remove(pointingTo); - EList _subtypes = pointingTo.getSubtypes(); - for (final Type c : _subtypes) { + List allSubtypes = CollectionLiterals.newArrayList(); + this.support.listSubtypes(pointingTo, allSubtypes); + for (final Type c : allSubtypes) { containmentListCopy.remove(c); } } } + for (final Type c : containmentListCopy) { + boolean _isIsAbstract = c.isIsAbstract(); + if (_isIsAbstract) { + containmentListCopy.remove(c); + } + } final String topName = CollectionsUtil.lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.lookup(containmentListCopy.get(0), trace.type2Predicate)); VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); @@ -132,7 +139,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { final VLSFunction toFunc = CollectionsUtil.lookup(toType, trace.type2Predicate); this.addToMap(type2cont, toFunc, rel); EList _subtypes = toType.getSubtypes(); - for (final Type c : _subtypes) { + for (final Type c_1 : _subtypes) { this.addToMap(type2cont, toFunc, rel); } VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); @@ -184,7 +191,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { { VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_4 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("containment", e.getKey().getConstant().toString())); + it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { 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 d5745333..c6565f6a 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 @@ -3,7 +3,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; @@ -17,14 +16,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.ArrayList; import java.util.Arrays; -import java.util.Collection; -import java.util.HashMap; import java.util.List; -import java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.ExclusiveRange; @@ -64,10 +59,19 @@ public class Logic2VampireLanguageMapper_RelationMapper { relVar2TypeDecComply.add(varTypeComply); } } + final String[] nameArray = r.getName().split(" "); + String relNameVar = ""; + int _length_1 = nameArray.length; + boolean _equals = (_length_1 == 3); + if (_equals) { + relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); + } else { + relNameVar = r.getName(); + } + final String relName = relNameVar; VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function = (VLSFofFormula it) -> { - final String[] nameArray = r.getName().split(" "); - it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2])); + it.setName(this.support.toIDMultiple("compliance", relName)); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { @@ -80,7 +84,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { final Procedure1 _function_2 = (VLSImplies it_2) -> { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_3 = (VLSFunction it_3) -> { - it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2])); + it_3.setConstant(this.support.toIDMultiple("r", relName)); for (final VLSVariable v_1 : relVar2VLS) { EList _terms = it_3.getTerms(); VLSVariable _duplicate_1 = this.support.duplicate(v_1); @@ -104,145 +108,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { } public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { - final Map relationVar2VLS = new HashMap(); - final Map relationVar2TypeDecComply = new HashMap(); - final Map relationVar2TypeDecRes = new HashMap(); - final ArrayList typedefs = new ArrayList(); - EList _variables = reldef.getVariables(); - for (final Variable variable : _variables) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName(this.support.toIDMultiple("V", variable.getName())); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - relationVar2VLS.put(variable, v); - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_1 = (VLSFunction it) -> { - TypeReference _range = variable.getRange(); - it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.support.duplicate(v); - _terms.add(_duplicate); - }; - final VLSFunction varTypeComply = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); - relationVar2TypeDecComply.put(variable, varTypeComply); - relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); - } - } - final String[] nameArray = reldef.getName().split(" "); - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { - int _length = nameArray.length; - int _minus = (_length - 2); - int _length_1 = nameArray.length; - int _minus_1 = (_length_1 - 1); - it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], - nameArray[_minus_1])); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { - EList _variables_1 = reldef.getVariables(); - for (final Variable variable_1 : _variables_1) { - EList _variables_2 = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.lookup(variable_1, relationVar2VLS)); - _variables_2.add(_duplicate); - } - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_2 = (VLSImplies it_2) -> { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_3 = (VLSFunction it_3) -> { - it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName())); - EList _variables_3 = reldef.getVariables(); - for (final Variable variable_2 : _variables_3) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_4 = (VLSVariable it_4) -> { - it_4.setName(CollectionsUtil.lookup(variable_2, relationVar2VLS).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_4); - EList _terms = it_3.getTerms(); - _terms.add(v); - } - } - }; - VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_3); - it_2.setLeft(_doubleArrow); - Collection _values = relationVar2TypeDecComply.values(); - ArrayList _arrayList = new ArrayList(_values); - it_2.setRight(this.support.unfoldAnd(_arrayList)); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula comply = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); - VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_1 = (VLSFofFormula it) -> { - int _length = nameArray.length; - int _minus = (_length - 2); - int _length_1 = nameArray.length; - int _minus_1 = (_length_1 - 1); - it.setName(this.support.toIDMultiple("relation", nameArray[_minus], - nameArray[_minus_1])); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - EList _variables_1 = reldef.getVariables(); - for (final Variable variable_1 : _variables_1) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_3 = (VLSVariable it_2) -> { - it_2.setName(CollectionsUtil.lookup(variable_1, relationVar2VLS).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_3); - EList _variables_2 = it_1.getVariables(); - _variables_2.add(v); - } - } - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_3 = (VLSImplies it_2) -> { - Collection _values = relationVar2TypeDecRes.values(); - ArrayList _arrayList = new ArrayList(_values); - it_2.setLeft(this.support.unfoldAnd(_arrayList)); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_4 = (VLSEquivalent it_3) -> { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_5 = (VLSFunction it_4) -> { - it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName())); - EList _variables_2 = reldef.getVariables(); - for (final Variable variable_2 : _variables_2) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_6 = (VLSVariable it_5) -> { - it_5.setName(CollectionsUtil.lookup(variable_2, relationVar2VLS).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); - EList _terms = it_4.getTerms(); - _terms.add(v); - } - } - }; - VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_5); - it_3.setLeft(_doubleArrow); - it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS)); - }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); - it_2.setRight(_doubleArrow); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_1); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(comply); - EList _formulas_1 = trace.specification.getFormulas(); - _formulas_1.add(res); } public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { 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 89633ca1..f1d73bec 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 @@ -403,20 +403,14 @@ public class Logic2VampireLanguageMapper_Support { return _xifexpression; } - protected List listSubtypes(final Type t) { - List allSubtypes = CollectionLiterals.newArrayList(); - boolean _isEmpty = t.getSubtypes().isEmpty(); - boolean _not = (!_isEmpty); - if (_not) { - EList _subtypes = t.getSubtypes(); - for (final Type subt : _subtypes) { - { - allSubtypes.add(subt); - allSubtypes = this.listSubtypes(subt); - } + protected void listSubtypes(final Type t, final List allSubtypes) { + EList _subtypes = t.getSubtypes(); + for (final Type subt : _subtypes) { + { + allSubtypes.add(subt); + this.listSubtypes(subt, allSubtypes); } } - return allSubtypes; } protected HashMap withAddition(final Map map1, final Map map2) { 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 9b8f049d..b9c1d28d 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 @@ -78,16 +78,19 @@ public class Logic2VampireLanguageMapper_TypeMapper { EList _elements = type_1.getElements(); for (final DefinedElement e : _elements) { { + final String[] nameArray = e.getName().split(" "); + String relNameVar = ""; + int _length = nameArray.length; + boolean _equals = (_length == 3); + if (_equals) { + relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); + } else { + relNameVar = e.getName(); + } + final String relName = relNameVar; VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { - final String[] splitName = e.getName().split(" "); - int _length = splitName.length; - boolean _greaterThan = (_length > 2); - if (_greaterThan) { - it.setConstant(this.support.toIDMultiple("e", splitName[0], splitName[2])); - } else { - it.setConstant(this.support.toIDMultiple("e", splitName[0])); - } + it.setConstant(this.support.toIDMultiple("e", relName)); EList _terms = it.getTerms(); VLSVariable _duplicate = this.support.duplicate(variable); _terms.add(_duplicate); @@ -123,7 +126,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function_1 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); + it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.lookup(type_1, trace.type2Predicate).getConstant().toString())); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { @@ -160,10 +163,10 @@ public class Logic2VampireLanguageMapper_TypeMapper { final VLSFunctionAsTerm cstTerm = ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); final VLSConstant cst = this.support.toConstant(cstTerm); trace.uniqueInstances.add(cst); - final int index = i; + final int index = (i - globalCounter); VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_3 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], + it.setName(this.support.toIDMultiple("enumScope", CollectionsUtil.lookup(type_1, trace.type2Predicate).getConstant().toString(), type_1.getElements().get(index).getName().split(" ")[0])); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); -- cgit v1.2.3-54-g00ecf