From 96e6ef62e818ee3b5c15d107ad49a448abfd4cd1 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 6 Mar 2019 14:18:35 -0500 Subject: Restructure Vampire Reasoner project --- .../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 .../vampire/reasoner/VampireSolver.xtend | 5 +- .../builder/Logic2VampireLanguageMapper.xtend | 10 +- .../Logic2VampireLanguageMapper_TypeMapper.xtend | 162 +++++++++++++++-- ...reLanguageMapper_TypeMapper_FilteredTypes.xtend | 153 ---------------- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2399 -> 2399 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5941 -> 5892 bytes .../vampire/reasoner/VampireSolver.java | 4 +- .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 17847 -> 17812 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 3708 -> 3708 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8207 -> 8207 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 6096 -> 6096 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 10926 -> 10926 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 3223 -> 8576 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 .../builder/Logic2VampireLanguageMapper.java | 6 +- .../Logic2VampireLanguageMapper_TypeMapper.java | 183 ++++++++++++++++++- ...ireLanguageMapper_TypeMapper_FilteredTypes.java | 193 --------------------- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 6358 -> 6358 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 4155 -> 4155 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 4115 -> 4115 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 7580 -> 7580 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 4054 -> 4054 bytes .../vampire/test/.MedicalSystem.xtendbin | Bin 4997 -> 4997 bytes .../dslreasoner/vampire/test/.SimpleRun.xtendbin | Bin 687 -> 687 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 6500 -> 6500 bytes 43 files changed, 332 insertions(+), 384 deletions(-) delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java 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 fef8d621..89a95266 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 3c37bd02..362c1696 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 76127556..67fbde4f 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 467395cb..2f2eaa65 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 601c5a4c..4ff50857 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 c60c4d59..bce7ab42 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 030267ff..b6c23926 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 ef7ffcdf..19d1d4f6 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 219fec58..503b9b33 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 47712412..279b2fbb 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 831f0df4..bcff04c1 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 696d67c0..66b7827f 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 9bef3ff9..5bac2912 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 dd65afb4..7cafc3c7 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/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend index ee802a99..1d56892e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend @@ -3,7 +3,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage @@ -14,6 +13,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper class VampireSolver extends LogicReasoner { @@ -23,8 +23,7 @@ class VampireSolver extends LogicReasoner { VampireLanguageStandaloneSetup::doSetup() } - val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper( - new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes) + val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper val VampireHandler handler = new VampireHandler diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index 81af24e5..1dbc0055 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend @@ -51,11 +51,8 @@ class Logic2VampireLanguageMapper { this) @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper( this) - @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper - - public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) { - this.typeMapper = typeMapper - } + @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper( + this) public def TracedOutput transformProblem(LogicProblem problem, VampireSolverConfiguration config) { @@ -82,8 +79,7 @@ class Logic2VampireLanguageMapper { // SCOPE MAPPER scopeMapper.transformScope(config, trace) - - + trace.constantDefinitions = problem.collectConstantDefinitions trace.relationDefinitions = problem.collectRelationDefinitions 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 1f071635..bc0b3e23 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 @@ -1,19 +1,157 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +import java.util.ArrayList import java.util.Collection import java.util.List -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm -interface Logic2VampireLanguageMapper_TypeMapper { - def void transformTypes(Collection types, Collection elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace); - //samples below 2 lines - def List transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) - def VLSTerm getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) - - def int getUndefinedSupertypeScope(int undefinedScope,Logic2VampireLanguageMapperTrace trace) - def VLSTerm transformReference(DefinedElement referred,Logic2VampireLanguageMapperTrace trace) - - def VampireModelInterpretation_TypeInterpretation getTypeInterpreter() -} \ No newline at end of file +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2VampireLanguageMapper_TypeMapper { + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support + val Logic2VampireLanguageMapper base + + new(Logic2VampireLanguageMapper base) { + LogicproblemPackage.eINSTANCE.class + this.base = base + } + + def protected transformTypes(Collection types, Collection elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { + +// val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes +// trace.typeMapperTrace = typeTrace + val VLSVariable variable = createVLSVariable => [it.name = "A"] + + // 1. Each type (class) is a predicate with a single variable as input + for (type : types) { + val typePred = createVLSFunction => [ + it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) + it.terms += support.duplicate(variable) + ] +// typeTrace.type2Predicate.put(type, typePred) + trace.type2Predicate.put(type, typePred) + } + + // 2. Map each ENUM type definition to fof formula + for (type : types.filter(TypeDefinition)) { + val List orElems = newArrayList + for (e : type.elements) { + val enumElemPred = createVLSFunction => [ + it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2)) + it.terms += support.duplicate(variable) + ] +// typeTrace.element2Predicate.put(e, enumElemPred) + trace.element2Predicate.put(e, enumElemPred) + orElems.add(enumElemPred) + } + + val res = createVLSFofFormula => [ + it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) + // below is temporary solution + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += support.duplicate(variable) + it.operand = createVLSEquivalent => [ +// it.left = createVLSFunction => [ +// it.constant = type.lookup(typeTrace.type2Predicate).constant +// it.terms += createVLSVariable => [it.name = "A"] +// ] +// it.left = type.lookup(typeTrace.type2Predicate) + it.left = type.lookup(trace.type2Predicate) + + it.right = support.unfoldOr(orElems) + + // TEMPPPPPPP +// it.right = support.unfoldOr(type.elements.map [e | +// +// createVLSEquality => [ +// it.left = support.duplicate(variable) +// it.right = createVLSDoubleQuote => [ +// it.value = "\"a" + e.name + "\"" +// ] +// ] +// ]) + // END TEMPPPPP + ] + ] + + ] + trace.specification.formulas += res + } + + //HIERARCHY HANDLER + + + // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates + // and store in a map + for (t1 : types.filter[!isIsAbstract]) { + for (t2 : types) { + // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes + if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { +// typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate))) + trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) + } else { +// typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ + trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ + it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) + ]) + } + } +// typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList(typeTrace.type2PossibleNot.values))) +// typeTrace.type2PossibleNot.clear + trace.type2And.put(t1, support.unfoldAnd(new ArrayList(trace.type2PossibleNot.values))) + trace.type2PossibleNot.clear + } + + // 5. create fof function that is an or with all the elements in map + val hierarch = createVLSFofFormula => [ + it.name = "hierarchyHandler" + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += support.duplicate(variable) + it.operand = createVLSEquivalent => [ + it.left = support.topLevelTypeFunc +// it.right = support.unfoldOr(new ArrayList(typeTrace.type2And.values)) + it.right = support.unfoldOr(new ArrayList(trace.type2And.values)) + ] + ] + ] + + trace.specification.formulas += hierarch + + } + + //below are from previous interface + def protected transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, + Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + def protected getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + def protected getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { + createVLSDoubleQuote => [ + it.value = "\"a" + referred.name + "\"" + ] + } + + def protected getTypeInterpreter() { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend deleted file mode 100644 index ea72940e..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend +++ /dev/null @@ -1,153 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder - -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition -import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory -import java.util.ArrayList -import java.util.Collection - -import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import java.util.List -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction - -class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { - private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support - private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE - - new() { - LogicproblemPackage.eINSTANCE.class - } - - override transformTypes(Collection types, Collection elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { - -// val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes -// trace.typeMapperTrace = typeTrace - val VLSVariable variable = createVLSVariable => [it.name = "A"] - - // 1. Each type (class) is a predicate with a single variable as input - for (type : types) { - val typePred = createVLSFunction => [ - it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) - it.terms += support.duplicate(variable) - ] -// typeTrace.type2Predicate.put(type, typePred) - trace.type2Predicate.put(type, typePred) - } - - // 2. Map each ENUM type definition to fof formula - for (type : types.filter(TypeDefinition)) { - val List orElems = newArrayList - for (e : type.elements) { - val enumElemPred = createVLSFunction => [ - it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2)) - it.terms += support.duplicate(variable) - ] -// typeTrace.element2Predicate.put(e, enumElemPred) - trace.element2Predicate.put(e, enumElemPred) - orElems.add(enumElemPred) - } - - val res = createVLSFofFormula => [ - it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) - // below is temporary solution - it.fofRole = "axiom" - it.fofFormula = createVLSUniversalQuantifier => [ - it.variables += support.duplicate(variable) - it.operand = createVLSEquivalent => [ -// it.left = createVLSFunction => [ -// it.constant = type.lookup(typeTrace.type2Predicate).constant -// it.terms += createVLSVariable => [it.name = "A"] -// ] -// it.left = type.lookup(typeTrace.type2Predicate) - it.left = type.lookup(trace.type2Predicate) - - it.right = support.unfoldOr(orElems) - - // TEMPPPPPPP -// it.right = support.unfoldOr(type.elements.map [e | -// -// createVLSEquality => [ -// it.left = support.duplicate(variable) -// it.right = createVLSDoubleQuote => [ -// it.value = "\"a" + e.name + "\"" -// ] -// ] -// ]) - // END TEMPPPPP - ] - ] - - ] - trace.specification.formulas += res - } - - //HIERARCHY HANDLER - - - // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates - // and store in a map - for (t1 : types.filter[!isIsAbstract]) { - for (t2 : types) { - // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes - if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { -// typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate))) - trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) - } else { -// typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ - trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ - it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) - ]) - } - } -// typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList(typeTrace.type2PossibleNot.values))) -// typeTrace.type2PossibleNot.clear - trace.type2And.put(t1, support.unfoldAnd(new ArrayList(trace.type2PossibleNot.values))) - trace.type2PossibleNot.clear - } - - // 5. create fof function that is an or with all the elements in map - val hierarch = createVLSFofFormula => [ - it.name = "hierarchyHandler" - it.fofRole = "axiom" - it.fofFormula = createVLSUniversalQuantifier => [ - it.variables += support.duplicate(variable) - it.operand = createVLSEquivalent => [ - it.left = support.topLevelTypeFunc -// it.right = support.unfoldOr(new ArrayList(typeTrace.type2And.values)) - it.right = support.unfoldOr(new ArrayList(trace.type2And.values)) - ] - ] - ] - - trace.specification.formulas += hierarch - - } - - override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, - Logic2VampireLanguageMapperTrace trace) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") - } - - override getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") - } - - override getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") - } - - override transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { - createVLSDoubleQuote => [ - it.value = "\"a" + referred.name + "\"" - ] - } - - override getTypeInterpreter() { - throw new UnsupportedOperationException("TODO: auto-generated method stub") - } - -} 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 4828107b..e0766c08 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 64061f82..c38c96ad 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/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java index 1846ba2e..d9d75887 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java @@ -5,7 +5,6 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; 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_TypeMapper_FilteredTypes; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; @@ -31,8 +30,7 @@ public class VampireSolver extends LogicReasoner { VampireLanguageStandaloneSetup.doSetup(); } - private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper( - new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes()); + private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(); private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper(); 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 f0cd1c7c..2c091b47 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 7d15db96..b05fd2c1 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 8fed8f56..7f6519eb 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_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 a40e27e4..d30eebe5 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 4b6b4a1e..921b79bd 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 c3035658..6b8d1dc0 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 2e21736e..83e57283 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 83697125..5a0087bc 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 063650c5..7d090297 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 e36d2270..c8ab54c2 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 5e5be153..3306fa73 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.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index dc2cd5ec..afe77bbe 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java @@ -89,11 +89,7 @@ public class Logic2VampireLanguageMapper { private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this); @Accessors(AccessorType.PUBLIC_GETTER) - private final Logic2VampireLanguageMapper_TypeMapper typeMapper; - - public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) { - this.typeMapper = typeMapper; - } + private final Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper(this); public TracedOutput transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) { VLSComment _createVLSComment = this.factory.createVLSComment(); 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 c55e2421..d3dddcfc 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 @@ -2,24 +2,191 @@ 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.VampireModelInterpretation_TypeInterpretation; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; +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.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; +import com.google.common.base.Objects; +import com.google.common.collect.Iterables; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; +import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; +import java.util.ArrayList; import java.util.Collection; import java.util.List; +import org.eclipse.emf.common.util.EList; +import org.eclipse.xtext.xbase.lib.CollectionLiterals; +import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.Functions.Function1; +import org.eclipse.xtext.xbase.lib.IterableExtensions; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @SuppressWarnings("all") -public interface Logic2VampireLanguageMapper_TypeMapper { - public abstract void transformTypes(final Collection types, final Collection elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); +public class Logic2VampireLanguageMapper_TypeMapper { + @Extension + private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; - public abstract List transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); + private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); - public abstract VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace); + private final Logic2VampireLanguageMapper base; - public abstract int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace); + public Logic2VampireLanguageMapper_TypeMapper(final Logic2VampireLanguageMapper base) { + LogicproblemPackage.eINSTANCE.getClass(); + this.base = base; + } - public abstract VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace); + protected boolean transformTypes(final Collection types, final Collection elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { + boolean _xblockexpression = false; + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function = (VLSVariable it) -> { + it.setName("A"); + }; + final VLSVariable variable = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + for (final Type type : types) { + { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_1 = (VLSFunction it) -> { + it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.support.duplicate(variable); + _terms.add(_duplicate); + }; + final VLSFunction typePred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + trace.type2Predicate.put(type, typePred); + } + } + Iterable _filter = Iterables.filter(types, TypeDefinition.class); + for (final TypeDefinition type_1 : _filter) { + { + final List orElems = CollectionLiterals.newArrayList(); + EList _elements = type_1.getElements(); + for (final DefinedElement e : _elements) { + { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_1 = (VLSFunction it) -> { + it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2])); + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.support.duplicate(variable); + _terms.add(_duplicate); + }; + final VLSFunction enumElemPred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + trace.element2Predicate.put(e, enumElemPred); + orElems.add(enumElemPred); + } + } + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function_1 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(variable); + _variables.add(_duplicate); + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function_3 = (VLSEquivalent it_2) -> { + it_2.setLeft(CollectionsUtil.lookup(type_1, trace.type2Predicate)); + it_2.setRight(this.support.unfoldOr(orElems)); + }; + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(res); + } + } + final Function1 _function_1 = (Type it) -> { + boolean _isIsAbstract = it.isIsAbstract(); + return Boolean.valueOf((!_isIsAbstract)); + }; + Iterable _filter_1 = IterableExtensions.filter(types, _function_1); + for (final Type t1 : _filter_1) { + { + for (final Type t2 : types) { + if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { + trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); + } else { + VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); + final Procedure1 _function_2 = (VLSUnaryNegation it) -> { + it.setOperand(this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); + }; + VLSUnaryNegation _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_2); + trace.type2PossibleNot.put(t2, _doubleArrow); + } + } + Collection _values = trace.type2PossibleNot.values(); + ArrayList _arrayList = new ArrayList(_values); + trace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); + trace.type2PossibleNot.clear(); + } + } + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function_2 = (VLSFofFormula it) -> { + it.setName("hierarchyHandler"); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_3 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(variable); + _variables.add(_duplicate); + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function_4 = (VLSEquivalent it_2) -> { + it_2.setLeft(this.support.topLevelTypeFunc()); + Collection _values = trace.type2And.values(); + ArrayList _arrayList = new ArrayList(_values); + it_2.setRight(this.support.unfoldOr(_arrayList)); + }; + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula hierarch = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_2); + EList _formulas = trace.specification.getFormulas(); + _xblockexpression = _formulas.add(hierarch); + } + return _xblockexpression; + } - public abstract VampireModelInterpretation_TypeInterpretation getTypeInterpreter(); + protected void transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } + + protected void getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } + + protected void getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } + + protected VLSDoubleQuote transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { + VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); + final Procedure1 _function = (VLSDoubleQuote it) -> { + String _name = referred.getName(); + String _plus = ("\"a" + _name); + String _plus_1 = (_plus + "\""); + it.setValue(_plus_1); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSDoubleQuote, _function); + } + + protected void getTypeInterpreter() { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java deleted file mode 100644 index b582fb96..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java +++ /dev/null @@ -1,193 +0,0 @@ -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.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; -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.VLSTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; -import com.google.common.base.Objects; -import com.google.common.collect.Iterables; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; -import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; -import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; -import java.util.ArrayList; -import java.util.Collection; -import java.util.List; -import org.eclipse.emf.common.util.EList; -import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Extension; -import org.eclipse.xtext.xbase.lib.Functions.Function1; -import org.eclipse.xtext.xbase.lib.IterableExtensions; -import org.eclipse.xtext.xbase.lib.ObjectExtensions; -import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; - -@SuppressWarnings("all") -public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { - private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); - - @Extension - private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; - - public Logic2VampireLanguageMapper_TypeMapper_FilteredTypes() { - LogicproblemPackage.eINSTANCE.getClass(); - } - - @Override - public void transformTypes(final Collection types, final Collection elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName("A"); - }; - final VLSVariable variable = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - for (final Type type : types) { - { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_1 = (VLSFunction it) -> { - it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.support.duplicate(variable); - _terms.add(_duplicate); - }; - final VLSFunction typePred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); - trace.type2Predicate.put(type, typePred); - } - } - Iterable _filter = Iterables.filter(types, TypeDefinition.class); - for (final TypeDefinition type_1 : _filter) { - { - final List orElems = CollectionLiterals.newArrayList(); - EList _elements = type_1.getElements(); - for (final DefinedElement e : _elements) { - { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_1 = (VLSFunction it) -> { - it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2])); - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.support.duplicate(variable); - _terms.add(_duplicate); - }; - final VLSFunction enumElemPred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); - trace.element2Predicate.put(e, enumElemPred); - orElems.add(enumElemPred); - } - } - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_1 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(variable); - _variables.add(_duplicate); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_3 = (VLSEquivalent it_2) -> { - it_2.setLeft(CollectionsUtil.lookup(type_1, trace.type2Predicate)); - it_2.setRight(this.support.unfoldOr(orElems)); - }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(res); - } - } - final Function1 _function_1 = (Type it) -> { - boolean _isIsAbstract = it.isIsAbstract(); - return Boolean.valueOf((!_isIsAbstract)); - }; - Iterable _filter_1 = IterableExtensions.filter(types, _function_1); - for (final Type t1 : _filter_1) { - { - for (final Type t2 : types) { - if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { - trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); - } else { - VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_2 = (VLSUnaryNegation it) -> { - it.setOperand(this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); - }; - VLSUnaryNegation _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_2); - trace.type2PossibleNot.put(t2, _doubleArrow); - } - } - Collection _values = trace.type2PossibleNot.values(); - ArrayList _arrayList = new ArrayList(_values); - trace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); - trace.type2PossibleNot.clear(); - } - } - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_2 = (VLSFofFormula it) -> { - it.setName("hierarchyHandler"); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_3 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(variable); - _variables.add(_duplicate); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_4 = (VLSEquivalent it_2) -> { - it_2.setLeft(this.support.topLevelTypeFunc()); - Collection _values = trace.type2And.values(); - ArrayList _arrayList = new ArrayList(_values); - it_2.setRight(this.support.unfoldOr(_arrayList)); - }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula hierarch = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_2); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(hierarch); - } - - @Override - public List transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { - throw new UnsupportedOperationException("TODO: auto-generated method stub"); - } - - @Override - public VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) { - throw new UnsupportedOperationException("TODO: auto-generated method stub"); - } - - @Override - public int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) { - throw new UnsupportedOperationException("TODO: auto-generated method stub"); - } - - @Override - public VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { - VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); - final Procedure1 _function = (VLSDoubleQuote it) -> { - String _name = referred.getName(); - String _plus = ("\"a" + _name); - String _plus_1 = (_plus + "\""); - it.setValue(_plus_1); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSDoubleQuote, _function); - } - - @Override - public VampireModelInterpretation_TypeInterpretation getTypeInterpreter() { - throw new UnsupportedOperationException("TODO: auto-generated method stub"); - } -} diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin index 6d33db67..446cfded 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin index 1406c597..9ded2f72 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin index 20397ff3..2c84c402 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin index 9f3d423f..867fe276 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin index 8fc60bab..8364a369 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin index 4212d100..fa2a2fc1 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin index 78d32090..a6a6e1b8 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin index d00afe64..26cbd485 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin differ -- cgit v1.2.3-54-g00ecf