From 85e6d0b8590f5aa22cd7065cb850b0f460da25dd 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 --- ...c2VampireLanguageMapper_ContainmentMapper.xtend | 12 +- ...ogic2VampireLanguageMapper_RelationMapper.xtend | 183 +++++++++++---------- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 1 + .../Logic2VampireLanguageMapper_Support.xtend | 12 +- .../Logic2VampireLanguageMapper_TypeMapper.xtend | 23 ++- 5 files changed, 126 insertions(+), 105 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill') 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 => [ -- cgit v1.2.3-54-g00ecf