diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-06 14:18:35 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-06 14:18:35 -0500 |
commit | 96e6ef62e818ee3b5c15d107ad49a448abfd4cd1 (patch) | |
tree | 1e27e5b1054ba647fbe88a4a01567358aeddeedf /Solvers/Vampire-Solver | |
parent | Continue improving code style (need sleep) (diff) | |
download | VIATRA-Generator-96e6ef62e818ee3b5c15d107ad49a448abfd4cd1.tar.gz VIATRA-Generator-96e6ef62e818ee3b5c15d107ad49a448abfd4cd1.tar.zst VIATRA-Generator-96e6ef62e818ee3b5c15d107ad49a448abfd4cd1.zip |
Restructure Vampire Reasoner project
Diffstat (limited to 'Solvers/Vampire-Solver')
35 files changed, 332 insertions, 384 deletions
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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 | |||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | 3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup |
4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated | 4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler | 7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage |
@@ -14,6 +13,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | |||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
16 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 15 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
16 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper | ||
17 | 17 | ||
18 | class VampireSolver extends LogicReasoner { | 18 | class VampireSolver extends LogicReasoner { |
19 | 19 | ||
@@ -23,8 +23,7 @@ class VampireSolver extends LogicReasoner { | |||
23 | VampireLanguageStandaloneSetup::doSetup() | 23 | VampireLanguageStandaloneSetup::doSetup() |
24 | } | 24 | } |
25 | 25 | ||
26 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper( | 26 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper |
27 | new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes) | ||
28 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper | 27 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper |
29 | val VampireHandler handler = new VampireHandler | 28 | val VampireHandler handler = new VampireHandler |
30 | 29 | ||
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 { | |||
51 | this) | 51 | this) |
52 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper( | 52 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper( |
53 | this) | 53 | this) |
54 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper | 54 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper( |
55 | 55 | this) | |
56 | public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) { | ||
57 | this.typeMapper = typeMapper | ||
58 | } | ||
59 | 56 | ||
60 | public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem, | 57 | public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem, |
61 | VampireSolverConfiguration config) { | 58 | VampireSolverConfiguration config) { |
@@ -82,8 +79,7 @@ class Logic2VampireLanguageMapper { | |||
82 | 79 | ||
83 | // SCOPE MAPPER | 80 | // SCOPE MAPPER |
84 | scopeMapper.transformScope(config, trace) | 81 | scopeMapper.transformScope(config, trace) |
85 | 82 | ||
86 | |||
87 | trace.constantDefinitions = problem.collectConstantDefinitions | 83 | trace.constantDefinitions = problem.collectConstantDefinitions |
88 | trace.relationDefinitions = problem.collectRelationDefinitions | 84 | trace.relationDefinitions = problem.collectRelationDefinitions |
89 | 85 | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
12 | import java.util.ArrayList | ||
5 | import java.util.Collection | 13 | import java.util.Collection |
6 | import java.util.List | 14 | import java.util.List |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
8 | 15 | ||
9 | interface Logic2VampireLanguageMapper_TypeMapper { | 16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
10 | def void transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace); | 17 | |
11 | //samples below 2 lines | 18 | class Logic2VampireLanguageMapper_TypeMapper { |
12 | def List<VLSTerm> transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) | 19 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
13 | def VLSTerm getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) | 20 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support |
14 | 21 | val Logic2VampireLanguageMapper base | |
15 | def int getUndefinedSupertypeScope(int undefinedScope,Logic2VampireLanguageMapperTrace trace) | 22 | |
16 | def VLSTerm transformReference(DefinedElement referred,Logic2VampireLanguageMapperTrace trace) | 23 | new(Logic2VampireLanguageMapper base) { |
17 | 24 | LogicproblemPackage.eINSTANCE.class | |
18 | def VampireModelInterpretation_TypeInterpretation getTypeInterpreter() | 25 | this.base = base |
19 | } \ No newline at end of file | 26 | } |
27 | |||
28 | def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { | ||
29 | |||
30 | // val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes | ||
31 | // trace.typeMapperTrace = typeTrace | ||
32 | val VLSVariable variable = createVLSVariable => [it.name = "A"] | ||
33 | |||
34 | // 1. Each type (class) is a predicate with a single variable as input | ||
35 | for (type : types) { | ||
36 | val typePred = createVLSFunction => [ | ||
37 | it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) | ||
38 | it.terms += support.duplicate(variable) | ||
39 | ] | ||
40 | // typeTrace.type2Predicate.put(type, typePred) | ||
41 | trace.type2Predicate.put(type, typePred) | ||
42 | } | ||
43 | |||
44 | // 2. Map each ENUM type definition to fof formula | ||
45 | for (type : types.filter(TypeDefinition)) { | ||
46 | val List<VLSFunction> orElems = newArrayList | ||
47 | for (e : type.elements) { | ||
48 | val enumElemPred = createVLSFunction => [ | ||
49 | it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2)) | ||
50 | it.terms += support.duplicate(variable) | ||
51 | ] | ||
52 | // typeTrace.element2Predicate.put(e, enumElemPred) | ||
53 | trace.element2Predicate.put(e, enumElemPred) | ||
54 | orElems.add(enumElemPred) | ||
55 | } | ||
56 | |||
57 | val res = createVLSFofFormula => [ | ||
58 | it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) | ||
59 | // below is temporary solution | ||
60 | it.fofRole = "axiom" | ||
61 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
62 | it.variables += support.duplicate(variable) | ||
63 | it.operand = createVLSEquivalent => [ | ||
64 | // it.left = createVLSFunction => [ | ||
65 | // it.constant = type.lookup(typeTrace.type2Predicate).constant | ||
66 | // it.terms += createVLSVariable => [it.name = "A"] | ||
67 | // ] | ||
68 | // it.left = type.lookup(typeTrace.type2Predicate) | ||
69 | it.left = type.lookup(trace.type2Predicate) | ||
70 | |||
71 | it.right = support.unfoldOr(orElems) | ||
72 | |||
73 | // TEMPPPPPPP | ||
74 | // it.right = support.unfoldOr(type.elements.map [e | | ||
75 | // | ||
76 | // createVLSEquality => [ | ||
77 | // it.left = support.duplicate(variable) | ||
78 | // it.right = createVLSDoubleQuote => [ | ||
79 | // it.value = "\"a" + e.name + "\"" | ||
80 | // ] | ||
81 | // ] | ||
82 | // ]) | ||
83 | // END TEMPPPPP | ||
84 | ] | ||
85 | ] | ||
86 | |||
87 | ] | ||
88 | trace.specification.formulas += res | ||
89 | } | ||
90 | |||
91 | //HIERARCHY HANDLER | ||
92 | |||
93 | |||
94 | // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates | ||
95 | // and store in a map | ||
96 | for (t1 : types.filter[!isIsAbstract]) { | ||
97 | for (t2 : types) { | ||
98 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes | ||
99 | if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { | ||
100 | // typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate))) | ||
101 | trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) | ||
102 | } else { | ||
103 | // typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ | ||
104 | trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ | ||
105 | it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) | ||
106 | ]) | ||
107 | } | ||
108 | } | ||
109 | // typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values))) | ||
110 | // typeTrace.type2PossibleNot.clear | ||
111 | trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values))) | ||
112 | trace.type2PossibleNot.clear | ||
113 | } | ||
114 | |||
115 | // 5. create fof function that is an or with all the elements in map | ||
116 | val hierarch = createVLSFofFormula => [ | ||
117 | it.name = "hierarchyHandler" | ||
118 | it.fofRole = "axiom" | ||
119 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
120 | it.variables += support.duplicate(variable) | ||
121 | it.operand = createVLSEquivalent => [ | ||
122 | it.left = support.topLevelTypeFunc | ||
123 | // it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values)) | ||
124 | it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values)) | ||
125 | ] | ||
126 | ] | ||
127 | ] | ||
128 | |||
129 | trace.specification.formulas += hierarch | ||
130 | |||
131 | } | ||
132 | |||
133 | //below are from previous interface | ||
134 | def protected transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, | ||
135 | Logic2VampireLanguageMapperTrace trace) { | ||
136 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
137 | } | ||
138 | |||
139 | def protected getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) { | ||
140 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
141 | } | ||
142 | |||
143 | def protected getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) { | ||
144 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
145 | } | ||
146 | |||
147 | def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { | ||
148 | createVLSDoubleQuote => [ | ||
149 | it.value = "\"a" + referred.name + "\"" | ||
150 | ] | ||
151 | } | ||
152 | |||
153 | def protected getTypeInterpreter() { | ||
154 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
155 | } | ||
156 | |||
157 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
10 | import java.util.ArrayList | ||
11 | import java.util.Collection | ||
12 | |||
13 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
14 | import java.util.List | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
16 | |||
17 | class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { | ||
18 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | ||
19 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
20 | |||
21 | new() { | ||
22 | LogicproblemPackage.eINSTANCE.class | ||
23 | } | ||
24 | |||
25 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { | ||
26 | |||
27 | // val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes | ||
28 | // trace.typeMapperTrace = typeTrace | ||
29 | val VLSVariable variable = createVLSVariable => [it.name = "A"] | ||
30 | |||
31 | // 1. Each type (class) is a predicate with a single variable as input | ||
32 | for (type : types) { | ||
33 | val typePred = createVLSFunction => [ | ||
34 | it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) | ||
35 | it.terms += support.duplicate(variable) | ||
36 | ] | ||
37 | // typeTrace.type2Predicate.put(type, typePred) | ||
38 | trace.type2Predicate.put(type, typePred) | ||
39 | } | ||
40 | |||
41 | // 2. Map each ENUM type definition to fof formula | ||
42 | for (type : types.filter(TypeDefinition)) { | ||
43 | val List<VLSFunction> orElems = newArrayList | ||
44 | for (e : type.elements) { | ||
45 | val enumElemPred = createVLSFunction => [ | ||
46 | it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2)) | ||
47 | it.terms += support.duplicate(variable) | ||
48 | ] | ||
49 | // typeTrace.element2Predicate.put(e, enumElemPred) | ||
50 | trace.element2Predicate.put(e, enumElemPred) | ||
51 | orElems.add(enumElemPred) | ||
52 | } | ||
53 | |||
54 | val res = createVLSFofFormula => [ | ||
55 | it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) | ||
56 | // below is temporary solution | ||
57 | it.fofRole = "axiom" | ||
58 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
59 | it.variables += support.duplicate(variable) | ||
60 | it.operand = createVLSEquivalent => [ | ||
61 | // it.left = createVLSFunction => [ | ||
62 | // it.constant = type.lookup(typeTrace.type2Predicate).constant | ||
63 | // it.terms += createVLSVariable => [it.name = "A"] | ||
64 | // ] | ||
65 | // it.left = type.lookup(typeTrace.type2Predicate) | ||
66 | it.left = type.lookup(trace.type2Predicate) | ||
67 | |||
68 | it.right = support.unfoldOr(orElems) | ||
69 | |||
70 | // TEMPPPPPPP | ||
71 | // it.right = support.unfoldOr(type.elements.map [e | | ||
72 | // | ||
73 | // createVLSEquality => [ | ||
74 | // it.left = support.duplicate(variable) | ||
75 | // it.right = createVLSDoubleQuote => [ | ||
76 | // it.value = "\"a" + e.name + "\"" | ||
77 | // ] | ||
78 | // ] | ||
79 | // ]) | ||
80 | // END TEMPPPPP | ||
81 | ] | ||
82 | ] | ||
83 | |||
84 | ] | ||
85 | trace.specification.formulas += res | ||
86 | } | ||
87 | |||
88 | //HIERARCHY HANDLER | ||
89 | |||
90 | |||
91 | // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates | ||
92 | // and store in a map | ||
93 | for (t1 : types.filter[!isIsAbstract]) { | ||
94 | for (t2 : types) { | ||
95 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes | ||
96 | if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { | ||
97 | // typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate))) | ||
98 | trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) | ||
99 | } else { | ||
100 | // typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ | ||
101 | trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ | ||
102 | it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) | ||
103 | ]) | ||
104 | } | ||
105 | } | ||
106 | // typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values))) | ||
107 | // typeTrace.type2PossibleNot.clear | ||
108 | trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values))) | ||
109 | trace.type2PossibleNot.clear | ||
110 | } | ||
111 | |||
112 | // 5. create fof function that is an or with all the elements in map | ||
113 | val hierarch = createVLSFofFormula => [ | ||
114 | it.name = "hierarchyHandler" | ||
115 | it.fofRole = "axiom" | ||
116 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
117 | it.variables += support.duplicate(variable) | ||
118 | it.operand = createVLSEquivalent => [ | ||
119 | it.left = support.topLevelTypeFunc | ||
120 | // it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values)) | ||
121 | it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values)) | ||
122 | ] | ||
123 | ] | ||
124 | ] | ||
125 | |||
126 | trace.specification.formulas += hierarch | ||
127 | |||
128 | } | ||
129 | |||
130 | override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, | ||
131 | Logic2VampireLanguageMapperTrace trace) { | ||
132 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
133 | } | ||
134 | |||
135 | override getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) { | ||
136 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
137 | } | ||
138 | |||
139 | override getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) { | ||
140 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
141 | } | ||
142 | |||
143 | override transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { | ||
144 | createVLSDoubleQuote => [ | ||
145 | it.value = "\"a" + referred.name + "\"" | ||
146 | ] | ||
147 | } | ||
148 | |||
149 | override getTypeInterpreter() { | ||
150 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
151 | } | ||
152 | |||
153 | } | ||
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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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; | |||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; | 8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; |
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | 9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
@@ -31,8 +30,7 @@ public class VampireSolver extends LogicReasoner { | |||
31 | VampireLanguageStandaloneSetup.doSetup(); | 30 | VampireLanguageStandaloneSetup.doSetup(); |
32 | } | 31 | } |
33 | 32 | ||
34 | private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper( | 33 | private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(); |
35 | new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes()); | ||
36 | 34 | ||
37 | private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper(); | 35 | private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper(); |
38 | 36 | ||
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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 { | |||
89 | private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this); | 89 | private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this); |
90 | 90 | ||
91 | @Accessors(AccessorType.PUBLIC_GETTER) | 91 | @Accessors(AccessorType.PUBLIC_GETTER) |
92 | private final Logic2VampireLanguageMapper_TypeMapper typeMapper; | 92 | private final Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper(this); |
93 | |||
94 | public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) { | ||
95 | this.typeMapper = typeMapper; | ||
96 | } | ||
97 | 93 | ||
98 | public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) { | 94 | public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) { |
99 | VLSComment _createVLSComment = this.factory.createVLSComment(); | 95 | 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; | |||
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
15 | import com.google.common.base.Objects; | ||
16 | import com.google.common.collect.Iterables; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; | ||
21 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
22 | import java.util.ArrayList; | ||
9 | import java.util.Collection; | 23 | import java.util.Collection; |
10 | import java.util.List; | 24 | import java.util.List; |
25 | import org.eclipse.emf.common.util.EList; | ||
26 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
27 | import org.eclipse.xtext.xbase.lib.Extension; | ||
28 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
29 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
30 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
31 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
11 | 32 | ||
12 | @SuppressWarnings("all") | 33 | @SuppressWarnings("all") |
13 | public interface Logic2VampireLanguageMapper_TypeMapper { | 34 | public class Logic2VampireLanguageMapper_TypeMapper { |
14 | public abstract void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); | 35 | @Extension |
36 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
15 | 37 | ||
16 | public abstract List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); | 38 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); |
17 | 39 | ||
18 | public abstract VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace); | 40 | private final Logic2VampireLanguageMapper base; |
19 | 41 | ||
20 | public abstract int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace); | 42 | public Logic2VampireLanguageMapper_TypeMapper(final Logic2VampireLanguageMapper base) { |
43 | LogicproblemPackage.eINSTANCE.getClass(); | ||
44 | this.base = base; | ||
45 | } | ||
21 | 46 | ||
22 | public abstract VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace); | 47 | protected boolean transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { |
48 | boolean _xblockexpression = false; | ||
49 | { | ||
50 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
51 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
52 | it.setName("A"); | ||
53 | }; | ||
54 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
55 | for (final Type type : types) { | ||
56 | { | ||
57 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
58 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
59 | it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); | ||
60 | EList<VLSTerm> _terms = it.getTerms(); | ||
61 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
62 | _terms.add(_duplicate); | ||
63 | }; | ||
64 | final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
65 | trace.type2Predicate.put(type, typePred); | ||
66 | } | ||
67 | } | ||
68 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); | ||
69 | for (final TypeDefinition type_1 : _filter) { | ||
70 | { | ||
71 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); | ||
72 | EList<DefinedElement> _elements = type_1.getElements(); | ||
73 | for (final DefinedElement e : _elements) { | ||
74 | { | ||
75 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
76 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
77 | it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2])); | ||
78 | EList<VLSTerm> _terms = it.getTerms(); | ||
79 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
80 | _terms.add(_duplicate); | ||
81 | }; | ||
82 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
83 | trace.element2Predicate.put(e, enumElemPred); | ||
84 | orElems.add(enumElemPred); | ||
85 | } | ||
86 | } | ||
87 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
88 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
89 | it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); | ||
90 | it.setFofRole("axiom"); | ||
91 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
92 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
93 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
94 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
95 | _variables.add(_duplicate); | ||
96 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
97 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { | ||
98 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); | ||
99 | it_2.setRight(this.support.unfoldOr(orElems)); | ||
100 | }; | ||
101 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); | ||
102 | it_1.setOperand(_doubleArrow); | ||
103 | }; | ||
104 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
105 | it.setFofFormula(_doubleArrow); | ||
106 | }; | ||
107 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | ||
108 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
109 | _formulas.add(res); | ||
110 | } | ||
111 | } | ||
112 | final Function1<Type, Boolean> _function_1 = (Type it) -> { | ||
113 | boolean _isIsAbstract = it.isIsAbstract(); | ||
114 | return Boolean.valueOf((!_isIsAbstract)); | ||
115 | }; | ||
116 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); | ||
117 | for (final Type t1 : _filter_1) { | ||
118 | { | ||
119 | for (final Type t2 : types) { | ||
120 | if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { | ||
121 | trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | ||
122 | } else { | ||
123 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
124 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { | ||
125 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | ||
126 | }; | ||
127 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); | ||
128 | trace.type2PossibleNot.put(t2, _doubleArrow); | ||
129 | } | ||
130 | } | ||
131 | Collection<VLSTerm> _values = trace.type2PossibleNot.values(); | ||
132 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
133 | trace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); | ||
134 | trace.type2PossibleNot.clear(); | ||
135 | } | ||
136 | } | ||
137 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
138 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | ||
139 | it.setName("hierarchyHandler"); | ||
140 | it.setFofRole("axiom"); | ||
141 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
142 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | ||
143 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
144 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
145 | _variables.add(_duplicate); | ||
146 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
147 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | ||
148 | it_2.setLeft(this.support.topLevelTypeFunc()); | ||
149 | Collection<VLSTerm> _values = trace.type2And.values(); | ||
150 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
151 | it_2.setRight(this.support.unfoldOr(_arrayList)); | ||
152 | }; | ||
153 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
154 | it_1.setOperand(_doubleArrow); | ||
155 | }; | ||
156 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); | ||
157 | it.setFofFormula(_doubleArrow); | ||
158 | }; | ||
159 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); | ||
160 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
161 | _xblockexpression = _formulas.add(hierarch); | ||
162 | } | ||
163 | return _xblockexpression; | ||
164 | } | ||
23 | 165 | ||
24 | public abstract VampireModelInterpretation_TypeInterpretation getTypeInterpreter(); | 166 | protected void transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { |
167 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
168 | } | ||
169 | |||
170 | protected void getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) { | ||
171 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
172 | } | ||
173 | |||
174 | protected void getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) { | ||
175 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
176 | } | ||
177 | |||
178 | protected VLSDoubleQuote transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { | ||
179 | VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); | ||
180 | final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> { | ||
181 | String _name = referred.getName(); | ||
182 | String _plus = ("\"a" + _name); | ||
183 | String _plus_1 = (_plus + "\""); | ||
184 | it.setValue(_plus_1); | ||
185 | }; | ||
186 | return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function); | ||
187 | } | ||
188 | |||
189 | protected void getTypeInterpreter() { | ||
190 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
191 | } | ||
25 | } | 192 | } |
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
17 | import com.google.common.base.Objects; | ||
18 | import com.google.common.collect.Iterables; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; | ||
23 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
24 | import java.util.ArrayList; | ||
25 | import java.util.Collection; | ||
26 | import java.util.List; | ||
27 | import org.eclipse.emf.common.util.EList; | ||
28 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
29 | import org.eclipse.xtext.xbase.lib.Extension; | ||
30 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
31 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
32 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
33 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
34 | |||
35 | @SuppressWarnings("all") | ||
36 | public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { | ||
37 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
38 | |||
39 | @Extension | ||
40 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
41 | |||
42 | public Logic2VampireLanguageMapper_TypeMapper_FilteredTypes() { | ||
43 | LogicproblemPackage.eINSTANCE.getClass(); | ||
44 | } | ||
45 | |||
46 | @Override | ||
47 | public void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | ||
48 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
49 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
50 | it.setName("A"); | ||
51 | }; | ||
52 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
53 | for (final Type type : types) { | ||
54 | { | ||
55 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
56 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
57 | it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); | ||
58 | EList<VLSTerm> _terms = it.getTerms(); | ||
59 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
60 | _terms.add(_duplicate); | ||
61 | }; | ||
62 | final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
63 | trace.type2Predicate.put(type, typePred); | ||
64 | } | ||
65 | } | ||
66 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); | ||
67 | for (final TypeDefinition type_1 : _filter) { | ||
68 | { | ||
69 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); | ||
70 | EList<DefinedElement> _elements = type_1.getElements(); | ||
71 | for (final DefinedElement e : _elements) { | ||
72 | { | ||
73 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
74 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
75 | it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2])); | ||
76 | EList<VLSTerm> _terms = it.getTerms(); | ||
77 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
78 | _terms.add(_duplicate); | ||
79 | }; | ||
80 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
81 | trace.element2Predicate.put(e, enumElemPred); | ||
82 | orElems.add(enumElemPred); | ||
83 | } | ||
84 | } | ||
85 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
86 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
87 | it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); | ||
88 | it.setFofRole("axiom"); | ||
89 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
90 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
91 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
92 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
93 | _variables.add(_duplicate); | ||
94 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
95 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { | ||
96 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); | ||
97 | it_2.setRight(this.support.unfoldOr(orElems)); | ||
98 | }; | ||
99 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); | ||
100 | it_1.setOperand(_doubleArrow); | ||
101 | }; | ||
102 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
103 | it.setFofFormula(_doubleArrow); | ||
104 | }; | ||
105 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | ||
106 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
107 | _formulas.add(res); | ||
108 | } | ||
109 | } | ||
110 | final Function1<Type, Boolean> _function_1 = (Type it) -> { | ||
111 | boolean _isIsAbstract = it.isIsAbstract(); | ||
112 | return Boolean.valueOf((!_isIsAbstract)); | ||
113 | }; | ||
114 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); | ||
115 | for (final Type t1 : _filter_1) { | ||
116 | { | ||
117 | for (final Type t2 : types) { | ||
118 | if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { | ||
119 | trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | ||
120 | } else { | ||
121 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
122 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { | ||
123 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | ||
124 | }; | ||
125 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); | ||
126 | trace.type2PossibleNot.put(t2, _doubleArrow); | ||
127 | } | ||
128 | } | ||
129 | Collection<VLSTerm> _values = trace.type2PossibleNot.values(); | ||
130 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
131 | trace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); | ||
132 | trace.type2PossibleNot.clear(); | ||
133 | } | ||
134 | } | ||
135 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
136 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | ||
137 | it.setName("hierarchyHandler"); | ||
138 | it.setFofRole("axiom"); | ||
139 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
140 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | ||
141 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
142 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
143 | _variables.add(_duplicate); | ||
144 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
145 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | ||
146 | it_2.setLeft(this.support.topLevelTypeFunc()); | ||
147 | Collection<VLSTerm> _values = trace.type2And.values(); | ||
148 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
149 | it_2.setRight(this.support.unfoldOr(_arrayList)); | ||
150 | }; | ||
151 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
152 | it_1.setOperand(_doubleArrow); | ||
153 | }; | ||
154 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); | ||
155 | it.setFofFormula(_doubleArrow); | ||
156 | }; | ||
157 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); | ||
158 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
159 | _formulas.add(hierarch); | ||
160 | } | ||
161 | |||
162 | @Override | ||
163 | public List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | ||
164 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
165 | } | ||
166 | |||
167 | @Override | ||
168 | public VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) { | ||
169 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
170 | } | ||
171 | |||
172 | @Override | ||
173 | public int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) { | ||
174 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
175 | } | ||
176 | |||
177 | @Override | ||
178 | public VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { | ||
179 | VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); | ||
180 | final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> { | ||
181 | String _name = referred.getName(); | ||
182 | String _plus = ("\"a" + _name); | ||
183 | String _plus_1 = (_plus + "\""); | ||
184 | it.setValue(_plus_1); | ||
185 | }; | ||
186 | return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function); | ||
187 | } | ||
188 | |||
189 | @Override | ||
190 | public VampireModelInterpretation_TypeInterpretation getTypeInterpreter() { | ||
191 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
192 | } | ||
193 | } | ||