From b42fb7517302ff158a61920a63d8682c31565619 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 20 Mar 2019 20:39:28 -0400 Subject: Add gitignore, commit everything --- ...Logic2VampireLanguageMapper_ContainmentMapper.xtend | 14 +++++++++----- ...eLanguageMapper_TypeMapperTrace_FilteredTypes.xtend | 18 ------------------ 2 files changed, 9 insertions(+), 23 deletions(-) delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner') 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 { val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type + val listForAnd = newArrayList +// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) + listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)) +// listForAnd.add(createVLSInequality => [ +// it.left = support.duplicate(varA) +// it.right = support.duplicate(varB) +// ]) + val relFormula = createVLSFofFormula => [ it.name = support.toIDMultiple("containment", relName) it.fofRole = "axiom" @@ -91,11 +99,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA) it.right = createVLSExistentialQuantifier => [ it.variables += support.duplicate(varB) - it.operand = createVLSAnd => [ - it.left = support.duplicate(fromType.lookup(trace.type2Predicate), varB) - it.right = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), - varList) - ] + it.operand = support.unfoldAnd(listForAnd) ] 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 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder - -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type -import java.util.HashMap -import java.util.Map - -class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace{ - -// public var VLSFofFormula objectSuperClass - public val Map type2Predicate = new HashMap; - public val Map element2Predicate = new HashMap - public val Map type2PossibleNot = new HashMap - public val Map type2And = new HashMap - -} \ No newline at end of file -- cgit v1.2.3-54-g00ecf