diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-20 20:39:28 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-20 20:39:28 -0400 |
commit | b42fb7517302ff158a61920a63d8682c31565619 (patch) | |
tree | d0649992bf0ee4f01fac40ec5404a6c92da0448a /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca | |
parent | Merge remote-tracking branch 'origin/master' into Vampire-New (diff) | |
download | VIATRA-Generator-b42fb7517302ff158a61920a63d8682c31565619.tar.gz VIATRA-Generator-b42fb7517302ff158a61920a63d8682c31565619.tar.zst VIATRA-Generator-b42fb7517302ff158a61920a63d8682c31565619.zip |
Add gitignore, commit everything
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca')
2 files changed, 9 insertions, 23 deletions
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 0820f47d..ff5a192e 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 | |||
@@ -81,6 +81,14 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
81 | val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type | 81 | val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type |
82 | val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type | 82 | val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type |
83 | 83 | ||
84 | val listForAnd = newArrayList | ||
85 | // listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) | ||
86 | listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)) | ||
87 | // listForAnd.add(createVLSInequality => [ | ||
88 | // it.left = support.duplicate(varA) | ||
89 | // it.right = support.duplicate(varB) | ||
90 | // ]) | ||
91 | |||
84 | val relFormula = createVLSFofFormula => [ | 92 | val relFormula = createVLSFofFormula => [ |
85 | it.name = support.toIDMultiple("containment", relName) | 93 | it.name = support.toIDMultiple("containment", relName) |
86 | it.fofRole = "axiom" | 94 | it.fofRole = "axiom" |
@@ -91,11 +99,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
91 | it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA) | 99 | it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA) |
92 | it.right = createVLSExistentialQuantifier => [ | 100 | it.right = createVLSExistentialQuantifier => [ |
93 | it.variables += support.duplicate(varB) | 101 | it.variables += support.duplicate(varB) |
94 | it.operand = createVLSAnd => [ | 102 | it.operand = support.unfoldAnd(listForAnd) |
95 | it.left = support.duplicate(fromType.lookup(trace.type2Predicate), varB) | ||
96 | it.right = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), | ||
97 | varList) | ||
98 | ] | ||
99 | ] | 103 | ] |
100 | 104 | ||
101 | createVLSEquality => [ | 105 | createVLSEquality => [ |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend deleted file mode 100644 index aba47edb..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend +++ /dev/null | |||
@@ -1,18 +0,0 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
7 | import java.util.HashMap | ||
8 | import java.util.Map | ||
9 | |||
10 | class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace{ | ||
11 | |||
12 | // public var VLSFofFormula objectSuperClass | ||
13 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; | ||
14 | public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap | ||
15 | public val Map<Type, VLSTerm> type2PossibleNot = new HashMap | ||
16 | public val Map<Type, VLSTerm> type2And = new HashMap | ||
17 | |||
18 | } \ No newline at end of file | ||