diff options
Diffstat (limited to 'Solvers')
42 files changed, 391 insertions, 142 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF index 23e3ad13..acaf466f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF | |||
@@ -4,23 +4,23 @@ Bundle-Name: Logic2viatra | |||
4 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;singleton:=true | 4 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;singleton:=true |
5 | Bundle-Version: 1.0.0.qualifier | 5 | Bundle-Version: 1.0.0.qualifier |
6 | Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra, | 6 | Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra, |
7 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, | 7 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, |
8 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries | 8 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries |
9 | Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | 9 | Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", |
10 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", | 10 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", |
11 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", | 11 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", |
12 | hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", | 12 | hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", |
13 | com.google.guava, | 13 | com.google.guava, |
14 | org.eclipse.xtext.xbase.lib, | 14 | org.eclipse.xtext.xbase.lib, |
15 | org.eclipse.xtend.lib, | 15 | org.eclipse.xtend.lib, |
16 | org.eclipse.xtend.lib.macro, | 16 | org.eclipse.xtend.lib.macro, |
17 | org.eclipse.viatra.query.runtime;bundle-version="1.5.0", | 17 | org.eclipse.viatra.query.runtime;bundle-version="1.5.0", |
18 | org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.5.0", | 18 | org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.5.0", |
19 | org.eclipse.viatra.query.patternlanguage.emf;bundle-version="1.5.0", | 19 | org.eclipse.viatra.query.patternlanguage.emf;bundle-version="1.5.0", |
20 | com.google.inject;bundle-version="3.0.0", | 20 | com.google.inject;bundle-version="3.0.0", |
21 | org.eclipse.xtext;bundle-version="2.10.0", | 21 | org.eclipse.xtext;bundle-version="2.10.0", |
22 | org.eclipse.viatra.transformation.runtime.emf;bundle-version="1.5.0", | 22 | org.eclipse.viatra.transformation.runtime.emf;bundle-version="1.5.0", |
23 | org.eclipse.xtext.xbase;bundle-version="2.10.0" | 23 | org.eclipse.xtext.xbase;bundle-version="2.10.0" |
24 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 | 24 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 |
25 | Import-Package: org.apache.log4j | 25 | Import-Package: org.apache.log4j |
26 | Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery | 26 | Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/.gitignore index ae3c1726..53edc85a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/.gitignore +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/.gitignore | |||
@@ -1 +1,3 @@ | |||
1 | /bin/ | 1 | /bin/ |
2 | /src-gen/ | ||
3 | /xtend-gen/ \ No newline at end of file | ||
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 416a4ced..31f46622 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 4c3a5366..cc4fa425 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.tests/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.gitignore index ae3c1726..8d2cfe73 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.gitignore +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.gitignore | |||
@@ -1 +1,3 @@ | |||
1 | /bin/ | 1 | /bin/ |
2 | /src-gen/ | ||
3 | /xtend-gen/ | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui.tests/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui.tests/.gitignore index ae3c1726..8d2cfe73 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui.tests/.gitignore +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui.tests/.gitignore | |||
@@ -1 +1,3 @@ | |||
1 | /bin/ | 1 | /bin/ |
2 | /src-gen/ | ||
3 | /xtend-gen/ | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/.gitignore index ae3c1726..8d2cfe73 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/.gitignore +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/.gitignore | |||
@@ -1 +1,3 @@ | |||
1 | /bin/ | 1 | /bin/ |
2 | /src-gen/ | ||
3 | /xtend-gen/ | ||
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 b9e07a68..23c27b9f 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 f51dce03..c0b6798a 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 23bdd607..f8684dcf 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 438765b1..34cde9c6 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 fb05770c..794a6799 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 1626ed6c..fca8ea98 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/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/.gitignore index ae3c1726..9dd5f2f6 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/.gitignore +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/.gitignore | |||
@@ -1 +1,3 @@ | |||
1 | /bin/ | 1 | /bin/ |
2 | /src-egn/ | ||
3 | /xtend-gen/ \ No newline at end of file | ||
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 c38505ea..690743f8 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 3ab52ff6..ac507dd4 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 e845ff1e..b9d659a5 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 d45af918..0f24f135 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 cc9d50ce..46e4ff65 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 0418e131..feb807fe 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/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index ff5a192e..820d0db2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend | |||
@@ -1,16 +1,19 @@ | |||
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.VLSAnd | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy | ||
7 | import java.util.List | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy | ||
12 | import java.util.HashMap | ||
13 | import java.util.List | ||
14 | import java.util.Map | ||
10 | 15 | ||
11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
14 | 17 | ||
15 | class Logic2VampireLanguageMapper_ContainmentMapper { | 18 | class Logic2VampireLanguageMapper_ContainmentMapper { |
16 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 19 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -74,54 +77,121 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
74 | // for each edge, if the pointedTo element exists,the edge must exist also | 77 | // for each edge, if the pointedTo element exists,the edge must exist also |
75 | val varA = createVLSVariable => [it.name = "A"] | 78 | val varA = createVLSVariable => [it.name = "A"] |
76 | val varB = createVLSVariable => [it.name = "B"] | 79 | val varB = createVLSVariable => [it.name = "B"] |
80 | val varC = createVLSVariable => [it.name = "C"] | ||
77 | val varList = newArrayList(varB, varA) | 81 | val varList = newArrayList(varB, varA) |
78 | 82 | val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap | |
79 | for (l : relationsList) { | 83 | for (l : relationsList) { |
80 | val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString | 84 | val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList) |
81 | val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type | 85 | // val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type |
82 | val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type | 86 | val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type) |
87 | val toFunc = toType.lookup(trace.type2Predicate) | ||
88 | |||
89 | addToMap(type2cont, toFunc, rel) | ||
83 | 90 | ||
84 | val listForAnd = newArrayList | 91 | for (c : toType.subtypes) { |
85 | // listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) | 92 | addToMap(type2cont, toFunc, rel) |
86 | listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)) | 93 | } |
94 | |||
95 | // val listForAnd = newArrayList | ||
96 | //// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) | ||
97 | // listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)) | ||
87 | // listForAnd.add(createVLSInequality => [ | 98 | // listForAnd.add(createVLSInequality => [ |
88 | // it.left = support.duplicate(varA) | 99 | // it.left = support.duplicate(varA) |
89 | // it.right = support.duplicate(varB) | 100 | // it.right = support.duplicate(varB) |
90 | // ]) | 101 | // ]) |
102 | // remove subtypes of elements being pointed to | ||
103 | // var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type | ||
104 | // containmentListCopy.remove(pointingTo) | ||
105 | // for (c : pointingTo.subtypes) { | ||
106 | // containmentListCopy.remove(c) | ||
107 | // } | ||
108 | // STEP 3 | ||
109 | // Ensure that an objct only has 1 parent | ||
110 | val relFormula = createVLSFofFormula => [ | ||
111 | it.name = support.toIDMultiple("noDupCont", rel.constant.toString) | ||
112 | it.fofRole = "axiom" | ||
113 | it.fofFormula = createVLSExistentialQuantifier => [ | ||
114 | it.variables += support.duplicate(varA) | ||
115 | it.variables += support.duplicate(varB) | ||
116 | it.operand = createVLSImplies => [ | ||
117 | it.left = support.duplicate(rel, newArrayList(varA, varB)) | ||
118 | it.right = createVLSUnaryNegation => [ | ||
119 | it.operand = createVLSExistentialQuantifier => [ | ||
120 | it.variables += support.duplicate(varC) | ||
121 | it.variables += support.duplicate(varB) | ||
122 | it.operand = support.duplicate(rel, newArrayList(varC, varB)) | ||
123 | |||
124 | ] | ||
125 | ] | ||
126 | ] | ||
127 | ] | ||
128 | ] | ||
129 | trace.specification.formulas += relFormula | ||
91 | 130 | ||
131 | } | ||
132 | |||
133 | // STEP CONT'D | ||
134 | for (e : type2cont.entrySet) { | ||
92 | val relFormula = createVLSFofFormula => [ | 135 | val relFormula = createVLSFofFormula => [ |
93 | it.name = support.toIDMultiple("containment", relName) | 136 | it.name = support.toIDMultiple("containment", e.key.constant.toString) |
94 | it.fofRole = "axiom" | 137 | it.fofRole = "axiom" |
95 | 138 | ||
96 | it.fofFormula = createVLSUniversalQuantifier => [ | 139 | it.fofFormula = createVLSUniversalQuantifier => [ |
97 | it.variables += support.duplicate(varA) | 140 | it.variables += support.duplicate(varA) |
98 | it.operand = createVLSImplies => [ | 141 | it.operand = createVLSImplies => [ |
99 | it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA) | 142 | it.left = support.duplicate(e.key, varA) |
100 | it.right = createVLSExistentialQuantifier => [ | 143 | it.right = createVLSExistentialQuantifier => [ |
101 | it.variables += support.duplicate(varB) | 144 | it.variables += support.duplicate(varB) |
102 | it.operand = support.unfoldAnd(listForAnd) | 145 | if (e.value.length > 1) { |
103 | ] | 146 | it.operand = makeUnique(e.value) |
147 | } else { | ||
148 | it.operand = e.value.get(0) | ||
149 | } | ||
104 | 150 | ||
105 | createVLSEquality => [ | ||
106 | it.left = support.duplicate(variable) | ||
107 | it.right = createVLSConstant => [ | ||
108 | it.name = "o1" | ||
109 | ] | ||
110 | ] | 151 | ] |
111 | ] | 152 | ] |
112 | ] | 153 | ] |
113 | ] | 154 | ] |
114 | trace.specification.formulas += relFormula | 155 | trace.specification.formulas += relFormula |
115 | var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type | 156 | |
116 | containmentListCopy.remove(pointingTo) | ||
117 | for (c : pointingTo.subtypes) { | ||
118 | containmentListCopy.remove(c) | ||
119 | } | ||
120 | } | 157 | } |
121 | 158 | ||
122 | // STEP 3 | ||
123 | // Ensure that an objct only has 1 parent | ||
124 | // STEP 4 | 159 | // STEP 4 |
125 | // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) | 160 | // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) |
126 | } | 161 | } |
162 | |||
163 | protected def VLSTerm makeUnique(List<VLSFunction> list) { | ||
164 | val List<VLSTerm> possibleNots = newArrayList | ||
165 | val List<VLSTerm> uniqueRels = newArrayList | ||
166 | |||
167 | for (t1 : list) { | ||
168 | for (t2 : list) { | ||
169 | if (t1 == t2) { | ||
170 | val fct = support.duplicate(t2) | ||
171 | possibleNots.add(fct) | ||
172 | } else { | ||
173 | val op = support.duplicate(t2) | ||
174 | val negFct = createVLSUnaryNegation => [ | ||
175 | it.operand = op | ||
176 | ] | ||
177 | possibleNots.add(negFct) | ||
178 | } | ||
179 | } | ||
180 | uniqueRels.add(support.unfoldAnd(possibleNots)) | ||
181 | possibleNots.clear | ||
182 | } | ||
183 | return support.unfoldOr(uniqueRels) | ||
184 | } | ||
185 | |||
186 | protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) { | ||
187 | if (!type2cont.containsKey(toFunc)) { | ||
188 | type2cont.put(toFunc, newArrayList(rel)) | ||
189 | } else { | ||
190 | if (!type2cont.get(toFunc).contains(rel)) { | ||
191 | type2cont.get(toFunc).add(rel) | ||
192 | // type2cont.replace(toFunc, newArrayList(firstRel)) | ||
193 | } | ||
194 | |||
195 | } | ||
196 | } | ||
127 | } | 197 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index 548deda4..bc87d3b7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend | |||
@@ -38,10 +38,10 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
38 | // Handling Minimum_General | 38 | // Handling Minimum_General |
39 | if (GLOBAL_MIN != 0) { | 39 | if (GLOBAL_MIN != 0) { |
40 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) | 40 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) |
41 | for(i : trace.uniqueInstances){ | 41 | for (i : trace.uniqueInstances) { |
42 | localInstances.add(support.duplicate(i)) | 42 | localInstances.add(support.duplicate(i)) |
43 | } | 43 | } |
44 | 44 | ||
45 | makeFofFormula(localInstances, trace, true, null) | 45 | makeFofFormula(localInstances, trace, true, null) |
46 | } | 46 | } |
47 | 47 | ||
@@ -83,14 +83,15 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
83 | 83 | ||
84 | // 3. Specify uniqueness of elements | 84 | // 3. Specify uniqueness of elements |
85 | if (trace.uniqueInstances.length != 0) { | 85 | if (trace.uniqueInstances.length != 0) { |
86 | val uniqueness = createVLSFofFormula => [ | 86 | for (e : trace.uniqueInstances) { |
87 | it.name = "typeUniqueness" | 87 | val uniqueness = createVLSFofFormula => [ |
88 | it.fofRole = "axiom" | 88 | it.name = support.toIDMultiple("t_uniqueness", e.name) |
89 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances) | 89 | it.fofRole = "axiom" |
90 | ] | 90 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e) |
91 | trace.specification.formulas += uniqueness | 91 | ] |
92 | trace.specification.formulas += uniqueness | ||
93 | } | ||
92 | } | 94 | } |
93 | |||
94 | } | 95 | } |
95 | 96 | ||
96 | def protected void getInstanceConstants(int endInd, int startInd, ArrayList list, | 97 | def protected void getInstanceConstants(int endInd, int startInd, ArrayList list, |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index 8d00d3e7..d1ea2a15 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend | |||
@@ -92,7 +92,7 @@ class Logic2VampireLanguageMapper_Support { | |||
92 | ] | 92 | ] |
93 | ] | 93 | ] |
94 | } | 94 | } |
95 | 95 | ||
96 | def protected VLSFunction topLevelTypeFunc(VLSVariable v) { | 96 | def protected VLSFunction topLevelTypeFunc(VLSVariable v) { |
97 | return createVLSFunction => [ | 97 | return createVLSFunction => [ |
98 | it.constant = "object" | 98 | it.constant = "object" |
@@ -108,15 +108,26 @@ class Logic2VampireLanguageMapper_Support { | |||
108 | } | 108 | } |
109 | 109 | ||
110 | // TODO Make more general | 110 | // TODO Make more general |
111 | def establishUniqueness(List<VLSConstant> terms) { | 111 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { |
112 | // val List<VLSInequality> eqs = newArrayList | ||
113 | // for (t1 : terms.subList(1, terms.length)) { | ||
114 | // for (t2 : terms.subList(0, terms.indexOf(t1))) { | ||
115 | // val eq = createVLSInequality => [ | ||
116 | // // TEMP | ||
117 | // it.left = createVLSConstant => [it.name = t2.name] | ||
118 | // it.right = createVLSConstant => [it.name = t1.name] | ||
119 | // // TEMP | ||
120 | // ] | ||
121 | // eqs.add(eq) | ||
122 | // } | ||
123 | // } | ||
124 | // return unfoldAnd(eqs) | ||
112 | val List<VLSInequality> eqs = newArrayList | 125 | val List<VLSInequality> eqs = newArrayList |
113 | for (t1 : terms.subList(1, terms.length)) { | 126 | for (t1 : terms) { |
114 | for (t2 : terms.subList(0, terms.indexOf(t1))) { | 127 | if (t1 != t2) { |
115 | val eq = createVLSInequality => [ | 128 | val eq = createVLSInequality => [ |
116 | // TEMP | ||
117 | it.left = createVLSConstant => [it.name = t2.name] | 129 | it.left = createVLSConstant => [it.name = t2.name] |
118 | it.right = createVLSConstant => [it.name = t1.name] | 130 | it.right = createVLSConstant => [it.name = t1.name] |
119 | // TEMP | ||
120 | ] | 131 | ] |
121 | eqs.add(eq) | 132 | eqs.add(eq) |
122 | } | 133 | } |
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 4c4247ce..1719bbcc 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 | |||
@@ -91,13 +91,12 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
91 | it.right = support.unfoldOr(typeDefs) | 91 | it.right = support.unfoldOr(typeDefs) |
92 | ] | 92 | ] |
93 | // it.right = support.unfoldOr((typeDefs)) | 93 | // it.right = support.unfoldOr((typeDefs)) |
94 | |||
95 | ] | 94 | ] |
96 | ] | 95 | ] |
97 | ] | 96 | ] |
98 | trace.specification.formulas += res | 97 | trace.specification.formulas += res |
99 | 98 | ||
100 | for (var i = globalCounter; i < globalCounter+type.elements.length; i++) { | 99 | for (var i = globalCounter; i < globalCounter + type.elements.length; i++) { |
101 | // Create objects for the enum elements | 100 | // Create objects for the enum elements |
102 | val num = i + 1 | 101 | val num = i + 1 |
103 | val cstTerm = createVLSFunctionAsTerm => [ | 102 | val cstTerm = createVLSFunctionAsTerm => [ |
@@ -127,7 +126,7 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
127 | trace.specification.formulas += enumScope | 126 | trace.specification.formulas += enumScope |
128 | 127 | ||
129 | } | 128 | } |
130 | globalCounter+=type.elements.size | 129 | globalCounter += type.elements.size |
131 | } | 130 | } |
132 | 131 | ||
133 | // HIERARCHY HANDLER | 132 | // HIERARCHY HANDLER |
@@ -148,9 +147,35 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
148 | // typeTrace.type2PossibleNot.clear | 147 | // typeTrace.type2PossibleNot.clear |
149 | trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values))) | 148 | trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values))) |
150 | trace.type2PossibleNot.clear | 149 | trace.type2PossibleNot.clear |
150 | |||
151 | } | ||
152 | |||
153 | // 4. case where an object is not an object | ||
154 | val List<VLSTerm> type2Not = newArrayList | ||
155 | |||
156 | for(t : types) { | ||
157 | type2Not.add(createVLSUnaryNegation => [ | ||
158 | it.operand = support.duplicate(t.lookup(trace.type2Predicate)) | ||
159 | ]) | ||
151 | } | 160 | } |
152 | 161 | ||
153 | // 5. create fof function that is an or with all the elements in map | 162 | val notObj = createVLSFofFormula => [ |
163 | it.name = "notObjectHandler" | ||
164 | it.fofRole = "axiom" | ||
165 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
166 | it.variables += support.duplicate(variable) | ||
167 | it.operand = createVLSEquivalent => [ | ||
168 | it.left = createVLSUnaryNegation => [ | ||
169 | it.operand = support.topLevelTypeFunc | ||
170 | ] | ||
171 | it.right = support.unfoldAnd(type2Not) | ||
172 | ] | ||
173 | ] | ||
174 | ] | ||
175 | |||
176 | trace.specification.formulas += notObj | ||
177 | |||
178 | // 4. create fof function that is an or with all the elements in map | ||
154 | val hierarch = createVLSFofFormula => [ | 179 | val hierarch = createVLSFofFormula => [ |
155 | it.name = "inheritanceHierarchyHandler" | 180 | it.name = "inheritanceHierarchyHandler" |
156 | it.fofRole = "axiom" | 181 | it.fofRole = "axiom" |
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 be554f99..b2e83781 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 0ee9b884..ec4554da 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/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 8e96ba14..85d288b2 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 ee720e29..f43d3267 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 528da797..a49422be 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_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index a1204329..e9060301 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.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 3413fc3f..ca19d1c9 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 a53a998a..bd348286 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 f265f6a3..274a1261 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 efde8350..2e16b79c 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 2cabecc8..b363474f 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 57844580..82ee023c 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 24898f59..e378eda2 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 a9589e7e..427ec9c1 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_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index 8c0ae38d..7bc70e9d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | |||
@@ -10,9 +10,12 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | |||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
18 | import com.google.common.base.Objects; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; |
@@ -21,9 +24,13 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | |||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; | 24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; |
22 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 25 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
23 | import java.util.ArrayList; | 26 | import java.util.ArrayList; |
27 | import java.util.HashMap; | ||
24 | import java.util.List; | 28 | import java.util.List; |
29 | import java.util.Map; | ||
30 | import java.util.Set; | ||
25 | import org.eclipse.emf.common.util.EList; | 31 | import org.eclipse.emf.common.util.EList; |
26 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 32 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
33 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
27 | import org.eclipse.xtext.xbase.lib.Extension; | 34 | import org.eclipse.xtext.xbase.lib.Extension; |
28 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 35 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
29 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 36 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
@@ -107,69 +114,155 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
107 | it.setName("B"); | 114 | it.setName("B"); |
108 | }; | 115 | }; |
109 | final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | 116 | final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); |
117 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
118 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it) -> { | ||
119 | it.setName("C"); | ||
120 | }; | ||
121 | final VLSVariable varC = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_3); | ||
110 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); | 122 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); |
123 | final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); | ||
111 | for (final Relation l_1 : relationsList) { | 124 | for (final Relation l_1 : relationsList) { |
112 | { | 125 | { |
113 | final String relName = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate).getConstant().toString(); | 126 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList); |
114 | TypeReference _get = l_1.getParameters().get(0); | 127 | TypeReference _get = l_1.getParameters().get(1); |
115 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | 128 | Type _referred = ((ComplexTypeReference) _get).getReferred(); |
116 | final Type fromType = ((Type) _referred); | 129 | final Type toType = ((Type) _referred); |
117 | TypeReference _get_1 = l_1.getParameters().get(1); | 130 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); |
118 | Type _referred_1 = ((ComplexTypeReference) _get_1).getReferred(); | 131 | this.addToMap(type2cont, toFunc, rel); |
119 | final Type toType = ((Type) _referred_1); | 132 | EList<Type> _subtypes = toType.getSubtypes(); |
120 | final ArrayList<VLSFunction> listForAnd = CollectionLiterals.<VLSFunction>newArrayList(); | 133 | for (final Type c : _subtypes) { |
121 | listForAnd.add(this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList)); | 134 | this.addToMap(type2cont, toFunc, rel); |
135 | } | ||
136 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
137 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
138 | it.setName(this.support.toIDMultiple("noDupCont", rel.getConstant().toString())); | ||
139 | it.setFofRole("axiom"); | ||
140 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
141 | final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> { | ||
142 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
143 | VLSVariable _duplicate = this.support.duplicate(varA); | ||
144 | _variables.add(_duplicate); | ||
145 | EList<VLSVariable> _variables_1 = it_1.getVariables(); | ||
146 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | ||
147 | _variables_1.add(_duplicate_1); | ||
148 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
149 | final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> { | ||
150 | it_2.setLeft(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varA, varB))); | ||
151 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
152 | final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> { | ||
153 | VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier(); | ||
154 | final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> { | ||
155 | EList<VLSVariable> _variables_2 = it_4.getVariables(); | ||
156 | VLSVariable _duplicate_2 = this.support.duplicate(varC); | ||
157 | _variables_2.add(_duplicate_2); | ||
158 | EList<VLSVariable> _variables_3 = it_4.getVariables(); | ||
159 | VLSVariable _duplicate_3 = this.support.duplicate(varB); | ||
160 | _variables_3.add(_duplicate_3); | ||
161 | it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB))); | ||
162 | }; | ||
163 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier_1, _function_8); | ||
164 | it_3.setOperand(_doubleArrow); | ||
165 | }; | ||
166 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_7); | ||
167 | it_2.setRight(_doubleArrow); | ||
168 | }; | ||
169 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6); | ||
170 | it_1.setOperand(_doubleArrow); | ||
171 | }; | ||
172 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_5); | ||
173 | it.setFofFormula(_doubleArrow); | ||
174 | }; | ||
175 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); | ||
176 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
177 | _formulas_1.add(relFormula); | ||
178 | } | ||
179 | } | ||
180 | Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); | ||
181 | for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { | ||
182 | { | ||
122 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 183 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
123 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | 184 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
124 | it.setName(this.support.toIDMultiple("containment", relName)); | 185 | it.setName(this.support.toIDMultiple("containment", e.getKey().getConstant().toString())); |
125 | it.setFofRole("axiom"); | 186 | it.setFofRole("axiom"); |
126 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 187 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
127 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | 188 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
128 | EList<VLSVariable> _variables = it_1.getVariables(); | 189 | EList<VLSVariable> _variables = it_1.getVariables(); |
129 | VLSVariable _duplicate = this.support.duplicate(varA); | 190 | VLSVariable _duplicate = this.support.duplicate(varA); |
130 | _variables.add(_duplicate); | 191 | _variables.add(_duplicate); |
131 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 192 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
132 | final Procedure1<VLSImplies> _function_5 = (VLSImplies it_2) -> { | 193 | final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> { |
133 | it_2.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate), varA)); | 194 | it_2.setLeft(this.support.duplicate(e.getKey(), varA)); |
134 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | 195 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); |
135 | final Procedure1<VLSExistentialQuantifier> _function_6 = (VLSExistentialQuantifier it_3) -> { | 196 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> { |
136 | EList<VLSVariable> _variables_1 = it_3.getVariables(); | 197 | EList<VLSVariable> _variables_1 = it_3.getVariables(); |
137 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | 198 | VLSVariable _duplicate_1 = this.support.duplicate(varB); |
138 | _variables_1.add(_duplicate_1); | 199 | _variables_1.add(_duplicate_1); |
139 | it_3.setOperand(this.support.unfoldAnd(listForAnd)); | 200 | int _length = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; |
201 | boolean _greaterThan = (_length > 1); | ||
202 | if (_greaterThan) { | ||
203 | it_3.setOperand(this.makeUnique(e.getValue())); | ||
204 | } else { | ||
205 | it_3.setOperand(e.getValue().get(0)); | ||
206 | } | ||
140 | }; | 207 | }; |
141 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_6); | 208 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); |
142 | it_2.setRight(_doubleArrow); | 209 | it_2.setRight(_doubleArrow); |
143 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
144 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { | ||
145 | it_3.setLeft(this.support.duplicate(this.variable)); | ||
146 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
147 | final Procedure1<VLSConstant> _function_8 = (VLSConstant it_4) -> { | ||
148 | it_4.setName("o1"); | ||
149 | }; | ||
150 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_8); | ||
151 | it_3.setRight(_doubleArrow_1); | ||
152 | }; | ||
153 | ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); | ||
154 | }; | 210 | }; |
155 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_5); | 211 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6); |
156 | it_1.setOperand(_doubleArrow); | 212 | it_1.setOperand(_doubleArrow); |
157 | }; | 213 | }; |
158 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | 214 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); |
159 | it.setFofFormula(_doubleArrow); | 215 | it.setFofFormula(_doubleArrow); |
160 | }; | 216 | }; |
161 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); | 217 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); |
162 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | 218 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); |
163 | _formulas_1.add(relFormula); | 219 | _formulas_1.add(relFormula); |
164 | TypeReference _get_2 = l_1.getParameters().get(1); | 220 | } |
165 | Type _referred_2 = ((ComplexTypeReference) _get_2).getReferred(); | 221 | } |
166 | Type pointingTo = ((Type) _referred_2); | 222 | } |
167 | containmentListCopy.remove(pointingTo); | 223 | |
168 | EList<Type> _subtypes = pointingTo.getSubtypes(); | 224 | protected VLSTerm makeUnique(final List<VLSFunction> list) { |
169 | for (final Type c : _subtypes) { | 225 | final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList(); |
170 | containmentListCopy.remove(c); | 226 | final List<VLSTerm> uniqueRels = CollectionLiterals.<VLSTerm>newArrayList(); |
227 | for (final VLSFunction t1 : list) { | ||
228 | { | ||
229 | for (final VLSFunction t2 : list) { | ||
230 | boolean _equals = Objects.equal(t1, t2); | ||
231 | if (_equals) { | ||
232 | final VLSFunction fct = this.support.duplicate(t2); | ||
233 | possibleNots.add(fct); | ||
234 | } else { | ||
235 | final VLSFunction op = this.support.duplicate(t2); | ||
236 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
237 | final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> { | ||
238 | it.setOperand(op); | ||
239 | }; | ||
240 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function); | ||
241 | possibleNots.add(negFct); | ||
242 | } | ||
171 | } | 243 | } |
244 | uniqueRels.add(this.support.unfoldAnd(possibleNots)); | ||
245 | possibleNots.clear(); | ||
246 | } | ||
247 | } | ||
248 | return this.support.unfoldOr(uniqueRels); | ||
249 | } | ||
250 | |||
251 | protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) { | ||
252 | Object _xifexpression = null; | ||
253 | boolean _containsKey = type2cont.containsKey(toFunc); | ||
254 | boolean _not = (!_containsKey); | ||
255 | if (_not) { | ||
256 | _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel)); | ||
257 | } else { | ||
258 | boolean _xifexpression_1 = false; | ||
259 | boolean _contains = type2cont.get(toFunc).contains(rel); | ||
260 | boolean _not_1 = (!_contains); | ||
261 | if (_not_1) { | ||
262 | _xifexpression_1 = type2cont.get(toFunc).add(rel); | ||
172 | } | 263 | } |
264 | _xifexpression = Boolean.valueOf(_xifexpression_1); | ||
173 | } | 265 | } |
266 | return _xifexpression; | ||
174 | } | 267 | } |
175 | } | 268 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index d2a6bff2..7aca7633 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |||
@@ -96,15 +96,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
96 | int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; | 96 | int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; |
97 | boolean _notEquals = (_length != 0); | 97 | boolean _notEquals = (_length != 0); |
98 | if (_notEquals) { | 98 | if (_notEquals) { |
99 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 99 | for (final VLSConstant e : trace.uniqueInstances) { |
100 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 100 | { |
101 | it.setName("typeUniqueness"); | 101 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
102 | it.setFofRole("axiom"); | 102 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
103 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances)); | 103 | it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); |
104 | }; | 104 | it.setFofRole("axiom"); |
105 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 105 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); |
106 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 106 | }; |
107 | _formulas.add(uniqueness); | 107 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); |
108 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
109 | _formulas.add(uniqueness); | ||
110 | } | ||
111 | } | ||
108 | } | 112 | } |
109 | } | 113 | } |
110 | 114 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index 119d01f1..64129bf3 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | |||
@@ -14,6 +14,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | |||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
17 | import com.google.common.base.Objects; | ||
17 | import com.google.common.collect.Iterables; | 18 | import com.google.common.collect.Iterables; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; |
@@ -173,31 +174,28 @@ public class Logic2VampireLanguageMapper_Support { | |||
173 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 174 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
174 | } | 175 | } |
175 | 176 | ||
176 | public VLSTerm establishUniqueness(final List<VLSConstant> terms) { | 177 | public VLSTerm establishUniqueness(final List<VLSConstant> terms, final VLSConstant t2) { |
177 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); | 178 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); |
178 | List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); | 179 | for (final VLSConstant t1 : terms) { |
179 | for (final VLSConstant t1 : _subList) { | 180 | boolean _notEquals = (!Objects.equal(t1, t2)); |
180 | List<VLSConstant> _subList_1 = terms.subList(0, terms.indexOf(t1)); | 181 | if (_notEquals) { |
181 | for (final VLSConstant t2 : _subList_1) { | 182 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); |
182 | { | 183 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { |
183 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); | 184 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); |
184 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { | 185 | final Procedure1<VLSConstant> _function_1 = (VLSConstant it_1) -> { |
185 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | 186 | it_1.setName(t2.getName()); |
186 | final Procedure1<VLSConstant> _function_1 = (VLSConstant it_1) -> { | ||
187 | it_1.setName(t2.getName()); | ||
188 | }; | ||
189 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); | ||
190 | it.setLeft(_doubleArrow); | ||
191 | VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant(); | ||
192 | final Procedure1<VLSConstant> _function_2 = (VLSConstant it_1) -> { | ||
193 | it_1.setName(t1.getName()); | ||
194 | }; | ||
195 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2); | ||
196 | it.setRight(_doubleArrow_1); | ||
197 | }; | 187 | }; |
198 | final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | 188 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); |
199 | eqs.add(eq); | 189 | it.setLeft(_doubleArrow); |
200 | } | 190 | VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant(); |
191 | final Procedure1<VLSConstant> _function_2 = (VLSConstant it_1) -> { | ||
192 | it_1.setName(t1.getName()); | ||
193 | }; | ||
194 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2); | ||
195 | it.setRight(_doubleArrow_1); | ||
196 | }; | ||
197 | final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | ||
198 | eqs.add(eq); | ||
201 | } | 199 | } |
202 | } | 200 | } |
203 | return this.unfoldAnd(eqs); | 201 | return this.unfoldAnd(eqs); |
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 ec759ebf..9b8f049d 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 | |||
@@ -223,31 +223,68 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
223 | trace.type2PossibleNot.clear(); | 223 | trace.type2PossibleNot.clear(); |
224 | } | 224 | } |
225 | } | 225 | } |
226 | final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList(); | ||
227 | for (final Type t : types) { | ||
228 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
229 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { | ||
230 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate))); | ||
231 | }; | ||
232 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); | ||
233 | type2Not.add(_doubleArrow); | ||
234 | } | ||
226 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 235 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
227 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | 236 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { |
237 | it.setName("notObjectHandler"); | ||
238 | it.setFofRole("axiom"); | ||
239 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
240 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | ||
241 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
242 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
243 | _variables.add(_duplicate); | ||
244 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
245 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | ||
246 | VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation(); | ||
247 | final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_3) -> { | ||
248 | it_3.setOperand(this.support.topLevelTypeFunc()); | ||
249 | }; | ||
250 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_6); | ||
251 | it_2.setLeft(_doubleArrow_1); | ||
252 | it_2.setRight(this.support.unfoldAnd(type2Not)); | ||
253 | }; | ||
254 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); | ||
255 | it_1.setOperand(_doubleArrow_1); | ||
256 | }; | ||
257 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | ||
258 | it.setFofFormula(_doubleArrow_1); | ||
259 | }; | ||
260 | final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_3); | ||
261 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
262 | _formulas.add(notObj); | ||
263 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
264 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
228 | it.setName("inheritanceHierarchyHandler"); | 265 | it.setName("inheritanceHierarchyHandler"); |
229 | it.setFofRole("axiom"); | 266 | it.setFofRole("axiom"); |
230 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 267 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
231 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | 268 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
232 | EList<VLSVariable> _variables = it_1.getVariables(); | 269 | EList<VLSVariable> _variables = it_1.getVariables(); |
233 | VLSVariable _duplicate = this.support.duplicate(variable); | 270 | VLSVariable _duplicate = this.support.duplicate(variable); |
234 | _variables.add(_duplicate); | 271 | _variables.add(_duplicate); |
235 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 272 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
236 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | 273 | final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { |
237 | it_2.setLeft(this.support.topLevelTypeFunc()); | 274 | it_2.setLeft(this.support.topLevelTypeFunc()); |
238 | Collection<VLSTerm> _values = trace.type2And.values(); | 275 | Collection<VLSTerm> _values = trace.type2And.values(); |
239 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); | 276 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); |
240 | it_2.setRight(this.support.unfoldOr(reversedList)); | 277 | it_2.setRight(this.support.unfoldOr(reversedList)); |
241 | }; | 278 | }; |
242 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | 279 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); |
243 | it_1.setOperand(_doubleArrow); | 280 | it_1.setOperand(_doubleArrow_1); |
244 | }; | 281 | }; |
245 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); | 282 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); |
246 | it.setFofFormula(_doubleArrow); | 283 | it.setFofFormula(_doubleArrow_1); |
247 | }; | 284 | }; |
248 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); | 285 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); |
249 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 286 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); |
250 | _xblockexpression = _formulas.add(hierarch); | 287 | _xblockexpression = _formulas_1.add(hierarch); |
251 | } | 288 | } |
252 | return _xblockexpression; | 289 | return _xblockexpression; |
253 | } | 290 | } |