diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-15 00:06:29 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-15 00:06:29 -0400 |
commit | 2f8149678539a94f2f4ca2e7ff5640ff5d7087cc (patch) | |
tree | 87355cdeb19a987a6ffc2dd215460e2bc34f1683 /Solvers | |
parent | VAMPIRE: #39 Reorganise tests, working yakindu test, need debugging (diff) | |
download | VIATRA-Generator-2f8149678539a94f2f4ca2e7ff5640ff5d7087cc.tar.gz VIATRA-Generator-2f8149678539a94f2f4ca2e7ff5640ff5d7087cc.tar.zst VIATRA-Generator-2f8149678539a94f2f4ca2e7ff5640ff5d7087cc.zip |
Diffstat (limited to 'Solvers')
37 files changed, 169 insertions, 279 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 024dcab9..10495630 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 7e128ad1..295d9ec2 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 0bf8ccc6..83b00f77 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 58a18bbb..f8a7a2f3 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 205afcc4..544f5811 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 b388bd43..62aac4ca 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 3092be97..31d4543e 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 8b23f34d..7b230b65 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 84682c47..a24c2795 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 e3f67a0c..b35605ae 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 bf354098..5e9cd3bd 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 da62f4c1..0001d80f 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 482b884e..b189414a 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 81c1f803..b4eec95c 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 395b4305..8e0e0b11 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 | |||
@@ -39,7 +39,15 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
39 | for (l : relationsList) { | 39 | for (l : relationsList) { |
40 | var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type | 40 | var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type |
41 | containmentListCopy.remove(pointingTo) | 41 | containmentListCopy.remove(pointingTo) |
42 | for (c : pointingTo.subtypes) { | 42 | var List<Type> allSubtypes = newArrayList |
43 | support.listSubtypes(pointingTo, allSubtypes) | ||
44 | for (c : allSubtypes) { | ||
45 | containmentListCopy.remove(c) | ||
46 | } | ||
47 | } | ||
48 | |||
49 | for (c : containmentListCopy) { | ||
50 | if(c.isIsAbstract) { | ||
43 | containmentListCopy.remove(c) | 51 | containmentListCopy.remove(c) |
44 | } | 52 | } |
45 | } | 53 | } |
@@ -135,7 +143,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
135 | // STEP 2 CONT'D | 143 | // STEP 2 CONT'D |
136 | for (e : type2cont.entrySet) { | 144 | for (e : type2cont.entrySet) { |
137 | val relFormula = createVLSFofFormula => [ | 145 | val relFormula = createVLSFofFormula => [ |
138 | it.name = support.toIDMultiple("containment", e.key.constant.toString) | 146 | it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) |
139 | it.fofRole = "axiom" | 147 | it.fofRole = "axiom" |
140 | 148 | ||
141 | it.fofFormula = createVLSUniversalQuantifier => [ | 149 | it.fofFormula = createVLSUniversalQuantifier => [ |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend index 0ae06bc3..2dec281d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend | |||
@@ -44,9 +44,20 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
44 | 44 | ||
45 | } | 45 | } |
46 | 46 | ||
47 | //deciding name of relation | ||
48 | val nameArray = r.name.split(" ") | ||
49 | var relNameVar = "" | ||
50 | if (nameArray.length == 3) { | ||
51 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) | ||
52 | } | ||
53 | else { | ||
54 | relNameVar = r.name | ||
55 | } | ||
56 | val relName = relNameVar | ||
57 | |||
47 | val comply = createVLSFofFormula=> [ | 58 | val comply = createVLSFofFormula=> [ |
48 | val nameArray = r.name.split(" ") | 59 | |
49 | it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2)) | 60 | it.name = support.toIDMultiple("compliance", relName) |
50 | it.fofRole = "axiom" | 61 | it.fofRole = "axiom" |
51 | it.fofFormula = createVLSUniversalQuantifier => [ | 62 | it.fofFormula = createVLSUniversalQuantifier => [ |
52 | for (v : relVar2VLS) { | 63 | for (v : relVar2VLS) { |
@@ -54,7 +65,7 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
54 | } | 65 | } |
55 | it.operand = createVLSImplies => [ | 66 | it.operand = createVLSImplies => [ |
56 | val rel = createVLSFunction => [ | 67 | val rel = createVLSFunction => [ |
57 | it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2)) | 68 | it.constant = support.toIDMultiple("r", relName) |
58 | for (v : relVar2VLS) { | 69 | for (v : relVar2VLS) { |
59 | it.terms += support.duplicate(v) | 70 | it.terms += support.duplicate(v) |
60 | } | 71 | } |
@@ -71,89 +82,89 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
71 | 82 | ||
72 | def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) { | 83 | def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) { |
73 | 84 | ||
74 | // 1. store all variables in support wrt their name | 85 | // // 1. store all variables in support wrt their name |
75 | // 1.1 if variable has type, creating list of type declarations | 86 | // // 1.1 if variable has type, creating list of type declarations |
76 | // val VLSVariable variable = createVLSVariable => [it.name = "A"] | 87 | //// val VLSVariable variable = createVLSVariable => [it.name = "A"] |
77 | val Map<Variable, VLSVariable> relationVar2VLS = new HashMap | 88 | // val Map<Variable, VLSVariable> relationVar2VLS = new HashMap |
78 | val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap | 89 | // val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap |
79 | val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap | 90 | // val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap |
80 | val typedefs = new ArrayList<VLSTerm> | 91 | // val typedefs = new ArrayList<VLSTerm> |
81 | 92 | // | |
82 | for (variable : reldef.variables) { | 93 | // for (variable : reldef.variables) { |
83 | val v = createVLSVariable => [ | 94 | // val v = createVLSVariable => [ |
84 | it.name = support.toIDMultiple("V", variable.name) | 95 | // it.name = support.toIDMultiple("V", variable.name) |
85 | ] | 96 | // ] |
86 | relationVar2VLS.put(variable, v) | 97 | // relationVar2VLS.put(variable, v) |
87 | 98 | // | |
88 | val varTypeComply = createVLSFunction => [ | 99 | // val varTypeComply = createVLSFunction => [ |
89 | it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) | 100 | // it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) |
90 | it.terms += support.duplicate(v) | 101 | // it.terms += support.duplicate(v) |
91 | ] | 102 | // ] |
92 | relationVar2TypeDecComply.put(variable, varTypeComply) | 103 | // relationVar2TypeDecComply.put(variable, varTypeComply) |
93 | relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) | 104 | // relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) |
94 | } | 105 | // } |
95 | val nameArray = reldef.name.split(" ") | 106 | // val nameArray = reldef.name.split(" ") |
96 | val comply = createVLSFofFormula => [ | 107 | // val comply = createVLSFofFormula => [ |
97 | it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), | 108 | // it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), |
98 | nameArray.get(nameArray.length - 1)) | 109 | // nameArray.get(nameArray.length - 1)) |
99 | it.fofRole = "axiom" | 110 | // it.fofRole = "axiom" |
100 | it.fofFormula = createVLSUniversalQuantifier => [ | 111 | // it.fofFormula = createVLSUniversalQuantifier => [ |
101 | for (variable : reldef.variables) { | 112 | // for (variable : reldef.variables) { |
102 | it.variables += support.duplicate(variable.lookup(relationVar2VLS)) | 113 | // it.variables += support.duplicate(variable.lookup(relationVar2VLS)) |
103 | 114 | // | |
104 | } | 115 | // } |
105 | it.operand = createVLSImplies => [ | 116 | // it.operand = createVLSImplies => [ |
106 | it.left = createVLSFunction => [ | 117 | // it.left = createVLSFunction => [ |
107 | it.constant = support.toIDMultiple("rel", reldef.name) | 118 | // it.constant = support.toIDMultiple("rel", reldef.name) |
108 | for (variable : reldef.variables) { | 119 | // for (variable : reldef.variables) { |
109 | val v = createVLSVariable => [ | 120 | // val v = createVLSVariable => [ |
110 | it.name = variable.lookup(relationVar2VLS).name | 121 | // it.name = variable.lookup(relationVar2VLS).name |
111 | ] | 122 | // ] |
112 | it.terms += v | 123 | // it.terms += v |
113 | } | 124 | // } |
114 | ] | 125 | // ] |
115 | it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values)) | 126 | // it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values)) |
116 | ] | 127 | // ] |
117 | ] | 128 | // ] |
118 | ] | 129 | // ] |
119 | 130 | // | |
120 | val res = createVLSFofFormula => [ | 131 | // val res = createVLSFofFormula => [ |
121 | it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2), | 132 | // it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2), |
122 | nameArray.get(nameArray.length - 1)) | 133 | // nameArray.get(nameArray.length - 1)) |
123 | it.fofRole = "axiom" | 134 | // it.fofRole = "axiom" |
124 | it.fofFormula = createVLSUniversalQuantifier => [ | 135 | // it.fofFormula = createVLSUniversalQuantifier => [ |
125 | for (variable : reldef.variables) { | 136 | // for (variable : reldef.variables) { |
126 | val v = createVLSVariable => [ | 137 | // val v = createVLSVariable => [ |
127 | it.name = variable.lookup(relationVar2VLS).name | 138 | // it.name = variable.lookup(relationVar2VLS).name |
128 | ] | 139 | // ] |
129 | it.variables += v | 140 | // it.variables += v |
130 | 141 | // | |
131 | } | 142 | // } |
132 | it.operand = createVLSImplies => [ | 143 | // it.operand = createVLSImplies => [ |
133 | it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values)) | 144 | // it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values)) |
134 | it.right = createVLSEquivalent => [ | 145 | // it.right = createVLSEquivalent => [ |
135 | it.left = createVLSFunction => [ | 146 | // it.left = createVLSFunction => [ |
136 | it.constant = support.toIDMultiple("rel", reldef.name) | 147 | // it.constant = support.toIDMultiple("rel", reldef.name) |
137 | for (variable : reldef.variables) { | 148 | // for (variable : reldef.variables) { |
138 | val v = createVLSVariable => [ | 149 | // val v = createVLSVariable => [ |
139 | it.name = variable.lookup(relationVar2VLS).name | 150 | // it.name = variable.lookup(relationVar2VLS).name |
140 | ] | 151 | // ] |
141 | it.terms += v | 152 | // it.terms += v |
142 | 153 | // | |
143 | } | 154 | // } |
144 | ] | 155 | // ] |
145 | it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) | 156 | // it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) |
146 | ] | 157 | // ] |
147 | 158 | // | |
148 | ] | 159 | // ] |
149 | 160 | // | |
150 | ] | 161 | // ] |
151 | 162 | // | |
152 | ] | 163 | // ] |
153 | 164 | // | |
154 | // trace.relationDefinition2Predicate.put(r,res) | 165 | // // trace.relationDefinition2Predicate.put(r,res) |
155 | trace.specification.formulas += comply; | 166 | // trace.specification.formulas += comply; |
156 | trace.specification.formulas += res; | 167 | // trace.specification.formulas += res; |
157 | 168 | ||
158 | } | 169 | } |
159 | 170 | ||
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 0a8812e4..4a8d2827 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 | |||
@@ -29,6 +29,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
29 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS | 29 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS |
30 | // TODO HANDLE | 30 | // TODO HANDLE |
31 | // 1. make a list of constants equaling the min number of specified objects | 31 | // 1. make a list of constants equaling the min number of specified objects |
32 | //These numbers do not include enums or initial model elements | ||
32 | val GLOBAL_MIN = config.typeScopes.minNewElements | 33 | val GLOBAL_MIN = config.typeScopes.minNewElements |
33 | val GLOBAL_MAX = config.typeScopes.maxNewElements | 34 | val GLOBAL_MAX = config.typeScopes.maxNewElements |
34 | 35 | ||
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 195b89bb..680213ab 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 | |||
@@ -273,15 +273,11 @@ class Logic2VampireLanguageMapper_Support { | |||
273 | } | 273 | } |
274 | } | 274 | } |
275 | 275 | ||
276 | def protected List<Type> listSubtypes(Type t) { | 276 | def protected void listSubtypes(Type t, List<Type> allSubtypes) { |
277 | var List<Type> allSubtypes = newArrayList | 277 | for (subt : t.subtypes) { |
278 | if (!t.subtypes.isEmpty) { | 278 | allSubtypes.add(subt) |
279 | for (subt : t.subtypes) { | 279 | listSubtypes(subt, allSubtypes) |
280 | allSubtypes.add(subt) | ||
281 | allSubtypes = listSubtypes(subt) | ||
282 | } | ||
283 | } | 280 | } |
284 | return allSubtypes | ||
285 | } | 281 | } |
286 | 282 | ||
287 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { | 283 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { |
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 3bc945df..2f3af593 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 | |||
@@ -44,14 +44,19 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
44 | 44 | ||
45 | // Create a VLSFunction for each Enum Element | 45 | // Create a VLSFunction for each Enum Element |
46 | val List<VLSFunction> orElems = newArrayList | 46 | val List<VLSFunction> orElems = newArrayList |
47 | |||
47 | for (e : type.elements) { | 48 | for (e : type.elements) { |
49 | val nameArray = e.name.split(" ") | ||
50 | var relNameVar = "" | ||
51 | if (nameArray.length == 3) { | ||
52 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) | ||
53 | } else { | ||
54 | relNameVar = e.name | ||
55 | } | ||
56 | val relName = relNameVar | ||
57 | |||
48 | val enumElemPred = createVLSFunction => [ | 58 | val enumElemPred = createVLSFunction => [ |
49 | val splitName = e.name.split(" ") | 59 | it.constant = support.toIDMultiple("e", relName) |
50 | if (splitName.length > 2) { | ||
51 | it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) | ||
52 | } else { | ||
53 | it.constant = support.toIDMultiple("e", splitName.get(0)) | ||
54 | } | ||
55 | it.terms += support.duplicate(variable) | 60 | it.terms += support.duplicate(variable) |
56 | ] | 61 | ] |
57 | trace.element2Predicate.put(e, enumElemPred) | 62 | trace.element2Predicate.put(e, enumElemPred) |
@@ -80,7 +85,7 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
80 | 85 | ||
81 | // Implement Enum Inheritence Hierarchy | 86 | // Implement Enum Inheritence Hierarchy |
82 | val res = createVLSFofFormula => [ | 87 | val res = createVLSFofFormula => [ |
83 | it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) | 88 | it.name = support.toIDMultiple("typeDef", type.lookup(trace.type2Predicate).constant.toString) |
84 | it.fofRole = "axiom" | 89 | it.fofRole = "axiom" |
85 | it.fofFormula = createVLSUniversalQuantifier => [ | 90 | it.fofFormula = createVLSUniversalQuantifier => [ |
86 | it.variables += support.duplicate(variable) | 91 | it.variables += support.duplicate(variable) |
@@ -105,9 +110,9 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
105 | val cst = support.toConstant(cstTerm) | 110 | val cst = support.toConstant(cstTerm) |
106 | trace.uniqueInstances.add(cst) | 111 | trace.uniqueInstances.add(cst) |
107 | 112 | ||
108 | val index = i | 113 | val index = i-globalCounter |
109 | val enumScope = createVLSFofFormula => [ | 114 | val enumScope = createVLSFofFormula => [ |
110 | it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0), | 115 | it.name = support.toIDMultiple("enumScope", type.lookup(trace.type2Predicate).constant.toString, |
111 | type.elements.get(index).name.split(" ").get(0)) | 116 | type.elements.get(index).name.split(" ").get(0)) |
112 | it.fofRole = "axiom" | 117 | it.fofRole = "axiom" |
113 | it.fofFormula = createVLSUniversalQuantifier => [ | 118 | it.fofFormula = createVLSUniversalQuantifier => [ |
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 43e1e477..1ea7e30a 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 4e6f6ca0..ee06cb39 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 707a6089..648d9600 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 3171324f..a02821a5 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 301df7fa..b01f92a6 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 5e53ea26..7634af4b 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 b378ed09..4906adfc 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 605ac88c..e2c945e3 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 0c289e29..f465506c 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 cb72fd90..e046604a 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 cfe1e8cd..aff62dca 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 c2079147..7212cce7 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 3c70bc14..d23bacad 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 9ef20b23..be78cace 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 4cdc7e6a..9deab87f 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 | |||
@@ -64,12 +64,19 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
64 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | 64 | Type _referred = ((ComplexTypeReference) _get).getReferred(); |
65 | Type pointingTo = ((Type) _referred); | 65 | Type pointingTo = ((Type) _referred); |
66 | containmentListCopy.remove(pointingTo); | 66 | containmentListCopy.remove(pointingTo); |
67 | EList<Type> _subtypes = pointingTo.getSubtypes(); | 67 | List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList(); |
68 | for (final Type c : _subtypes) { | 68 | this.support.listSubtypes(pointingTo, allSubtypes); |
69 | for (final Type c : allSubtypes) { | ||
69 | containmentListCopy.remove(c); | 70 | containmentListCopy.remove(c); |
70 | } | 71 | } |
71 | } | 72 | } |
72 | } | 73 | } |
74 | for (final Type c : containmentListCopy) { | ||
75 | boolean _isIsAbstract = c.isIsAbstract(); | ||
76 | if (_isIsAbstract) { | ||
77 | containmentListCopy.remove(c); | ||
78 | } | ||
79 | } | ||
73 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); | 80 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); |
74 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate)); | 81 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate)); |
75 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 82 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
@@ -132,7 +139,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
132 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); | 139 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); |
133 | this.addToMap(type2cont, toFunc, rel); | 140 | this.addToMap(type2cont, toFunc, rel); |
134 | EList<Type> _subtypes = toType.getSubtypes(); | 141 | EList<Type> _subtypes = toType.getSubtypes(); |
135 | for (final Type c : _subtypes) { | 142 | for (final Type c_1 : _subtypes) { |
136 | this.addToMap(type2cont, toFunc, rel); | 143 | this.addToMap(type2cont, toFunc, rel); |
137 | } | 144 | } |
138 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 145 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
@@ -184,7 +191,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
184 | { | 191 | { |
185 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 192 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
186 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | 193 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
187 | it.setName(this.support.toIDMultiple("containment", e.getKey().getConstant().toString())); | 194 | it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); |
188 | it.setFofRole("axiom"); | 195 | it.setFofRole("axiom"); |
189 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 196 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
190 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { | 197 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java index d5745333..c6565f6a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java | |||
@@ -3,7 +3,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | |||
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.Logic2VampireLanguageMapper_Support; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
@@ -17,14 +16,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | |||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
21 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 19 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
22 | import java.util.ArrayList; | 20 | import java.util.ArrayList; |
23 | import java.util.Arrays; | 21 | import java.util.Arrays; |
24 | import java.util.Collection; | ||
25 | import java.util.HashMap; | ||
26 | import java.util.List; | 22 | import java.util.List; |
27 | import java.util.Map; | ||
28 | import org.eclipse.emf.common.util.EList; | 23 | import org.eclipse.emf.common.util.EList; |
29 | import org.eclipse.xtext.xbase.lib.Conversions; | 24 | import org.eclipse.xtext.xbase.lib.Conversions; |
30 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | 25 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; |
@@ -64,10 +59,19 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
64 | relVar2TypeDecComply.add(varTypeComply); | 59 | relVar2TypeDecComply.add(varTypeComply); |
65 | } | 60 | } |
66 | } | 61 | } |
62 | final String[] nameArray = r.getName().split(" "); | ||
63 | String relNameVar = ""; | ||
64 | int _length_1 = nameArray.length; | ||
65 | boolean _equals = (_length_1 == 3); | ||
66 | if (_equals) { | ||
67 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | ||
68 | } else { | ||
69 | relNameVar = r.getName(); | ||
70 | } | ||
71 | final String relName = relNameVar; | ||
67 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 72 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
68 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 73 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
69 | final String[] nameArray = r.getName().split(" "); | 74 | it.setName(this.support.toIDMultiple("compliance", relName)); |
70 | it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2])); | ||
71 | it.setFofRole("axiom"); | 75 | it.setFofRole("axiom"); |
72 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 76 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
73 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | 77 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { |
@@ -80,7 +84,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
80 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | 84 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { |
81 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 85 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
82 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | 86 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { |
83 | it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2])); | 87 | it_3.setConstant(this.support.toIDMultiple("r", relName)); |
84 | for (final VLSVariable v_1 : relVar2VLS) { | 88 | for (final VLSVariable v_1 : relVar2VLS) { |
85 | EList<VLSTerm> _terms = it_3.getTerms(); | 89 | EList<VLSTerm> _terms = it_3.getTerms(); |
86 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); | 90 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); |
@@ -104,145 +108,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
104 | } | 108 | } |
105 | 109 | ||
106 | public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { | 110 | public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { |
107 | final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
108 | final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>(); | ||
109 | final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>(); | ||
110 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
111 | EList<Variable> _variables = reldef.getVariables(); | ||
112 | for (final Variable variable : _variables) { | ||
113 | { | ||
114 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
115 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
116 | it.setName(this.support.toIDMultiple("V", variable.getName())); | ||
117 | }; | ||
118 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
119 | relationVar2VLS.put(variable, v); | ||
120 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
121 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
122 | TypeReference _range = variable.getRange(); | ||
123 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | ||
124 | EList<VLSTerm> _terms = it.getTerms(); | ||
125 | VLSVariable _duplicate = this.support.duplicate(v); | ||
126 | _terms.add(_duplicate); | ||
127 | }; | ||
128 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
129 | relationVar2TypeDecComply.put(variable, varTypeComply); | ||
130 | relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); | ||
131 | } | ||
132 | } | ||
133 | final String[] nameArray = reldef.getName().split(" "); | ||
134 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
135 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
136 | int _length = nameArray.length; | ||
137 | int _minus = (_length - 2); | ||
138 | int _length_1 = nameArray.length; | ||
139 | int _minus_1 = (_length_1 - 1); | ||
140 | it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], | ||
141 | nameArray[_minus_1])); | ||
142 | it.setFofRole("axiom"); | ||
143 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
144 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
145 | EList<Variable> _variables_1 = reldef.getVariables(); | ||
146 | for (final Variable variable_1 : _variables_1) { | ||
147 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
148 | VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS)); | ||
149 | _variables_2.add(_duplicate); | ||
150 | } | ||
151 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
152 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
153 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
154 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
155 | it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName())); | ||
156 | EList<Variable> _variables_3 = reldef.getVariables(); | ||
157 | for (final Variable variable_2 : _variables_3) { | ||
158 | { | ||
159 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
160 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
161 | it_4.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
162 | }; | ||
163 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
164 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
165 | _terms.add(v); | ||
166 | } | ||
167 | } | ||
168 | }; | ||
169 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
170 | it_2.setLeft(_doubleArrow); | ||
171 | Collection<VLSFunction> _values = relationVar2TypeDecComply.values(); | ||
172 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
173 | it_2.setRight(this.support.unfoldAnd(_arrayList)); | ||
174 | }; | ||
175 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
176 | it_1.setOperand(_doubleArrow); | ||
177 | }; | ||
178 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
179 | it.setFofFormula(_doubleArrow); | ||
180 | }; | ||
181 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
182 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
183 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
184 | int _length = nameArray.length; | ||
185 | int _minus = (_length - 2); | ||
186 | int _length_1 = nameArray.length; | ||
187 | int _minus_1 = (_length_1 - 1); | ||
188 | it.setName(this.support.toIDMultiple("relation", nameArray[_minus], | ||
189 | nameArray[_minus_1])); | ||
190 | it.setFofRole("axiom"); | ||
191 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
192 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
193 | EList<Variable> _variables_1 = reldef.getVariables(); | ||
194 | for (final Variable variable_1 : _variables_1) { | ||
195 | { | ||
196 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
197 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> { | ||
198 | it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName()); | ||
199 | }; | ||
200 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_3); | ||
201 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
202 | _variables_2.add(v); | ||
203 | } | ||
204 | } | ||
205 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
206 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | ||
207 | Collection<VLSFunction> _values = relationVar2TypeDecRes.values(); | ||
208 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
209 | it_2.setLeft(this.support.unfoldAnd(_arrayList)); | ||
210 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
211 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> { | ||
212 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
213 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> { | ||
214 | it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName())); | ||
215 | EList<Variable> _variables_2 = reldef.getVariables(); | ||
216 | for (final Variable variable_2 : _variables_2) { | ||
217 | { | ||
218 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
219 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_5) -> { | ||
220 | it_5.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
221 | }; | ||
222 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); | ||
223 | EList<VLSTerm> _terms = it_4.getTerms(); | ||
224 | _terms.add(v); | ||
225 | } | ||
226 | } | ||
227 | }; | ||
228 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); | ||
229 | it_3.setLeft(_doubleArrow); | ||
230 | it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS)); | ||
231 | }; | ||
232 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
233 | it_2.setRight(_doubleArrow); | ||
234 | }; | ||
235 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
236 | it_1.setOperand(_doubleArrow); | ||
237 | }; | ||
238 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
239 | it.setFofFormula(_doubleArrow); | ||
240 | }; | ||
241 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_1); | ||
242 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
243 | _formulas.add(comply); | ||
244 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
245 | _formulas_1.add(res); | ||
246 | } | 111 | } |
247 | 112 | ||
248 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { | 113 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { |
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 89633ca1..f1d73bec 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 | |||
@@ -403,20 +403,14 @@ public class Logic2VampireLanguageMapper_Support { | |||
403 | return _xifexpression; | 403 | return _xifexpression; |
404 | } | 404 | } |
405 | 405 | ||
406 | protected List<Type> listSubtypes(final Type t) { | 406 | protected void listSubtypes(final Type t, final List<Type> allSubtypes) { |
407 | List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList(); | 407 | EList<Type> _subtypes = t.getSubtypes(); |
408 | boolean _isEmpty = t.getSubtypes().isEmpty(); | 408 | for (final Type subt : _subtypes) { |
409 | boolean _not = (!_isEmpty); | 409 | { |
410 | if (_not) { | 410 | allSubtypes.add(subt); |
411 | EList<Type> _subtypes = t.getSubtypes(); | 411 | this.listSubtypes(subt, allSubtypes); |
412 | for (final Type subt : _subtypes) { | ||
413 | { | ||
414 | allSubtypes.add(subt); | ||
415 | allSubtypes = this.listSubtypes(subt); | ||
416 | } | ||
417 | } | 412 | } |
418 | } | 413 | } |
419 | return allSubtypes; | ||
420 | } | 414 | } |
421 | 415 | ||
422 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { | 416 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { |
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 9b8f049d..b9c1d28d 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 | |||
@@ -78,16 +78,19 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
78 | EList<DefinedElement> _elements = type_1.getElements(); | 78 | EList<DefinedElement> _elements = type_1.getElements(); |
79 | for (final DefinedElement e : _elements) { | 79 | for (final DefinedElement e : _elements) { |
80 | { | 80 | { |
81 | final String[] nameArray = e.getName().split(" "); | ||
82 | String relNameVar = ""; | ||
83 | int _length = nameArray.length; | ||
84 | boolean _equals = (_length == 3); | ||
85 | if (_equals) { | ||
86 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | ||
87 | } else { | ||
88 | relNameVar = e.getName(); | ||
89 | } | ||
90 | final String relName = relNameVar; | ||
81 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 91 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
82 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 92 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
83 | final String[] splitName = e.getName().split(" "); | 93 | it.setConstant(this.support.toIDMultiple("e", relName)); |
84 | int _length = splitName.length; | ||
85 | boolean _greaterThan = (_length > 2); | ||
86 | if (_greaterThan) { | ||
87 | it.setConstant(this.support.toIDMultiple("e", splitName[0], splitName[2])); | ||
88 | } else { | ||
89 | it.setConstant(this.support.toIDMultiple("e", splitName[0])); | ||
90 | } | ||
91 | EList<VLSTerm> _terms = it.getTerms(); | 94 | EList<VLSTerm> _terms = it.getTerms(); |
92 | VLSVariable _duplicate = this.support.duplicate(variable); | 95 | VLSVariable _duplicate = this.support.duplicate(variable); |
93 | _terms.add(_duplicate); | 96 | _terms.add(_duplicate); |
@@ -123,7 +126,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
123 | } | 126 | } |
124 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 127 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
125 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 128 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { |
126 | it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); | 129 | it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString())); |
127 | it.setFofRole("axiom"); | 130 | it.setFofRole("axiom"); |
128 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 131 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
129 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 132 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
@@ -160,10 +163,10 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
160 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); | 163 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); |
161 | final VLSConstant cst = this.support.toConstant(cstTerm); | 164 | final VLSConstant cst = this.support.toConstant(cstTerm); |
162 | trace.uniqueInstances.add(cst); | 165 | trace.uniqueInstances.add(cst); |
163 | final int index = i; | 166 | final int index = (i - globalCounter); |
164 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 167 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
165 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | 168 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { |
166 | it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], | 169 | it.setName(this.support.toIDMultiple("enumScope", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), |
167 | type_1.getElements().get(index).getName().split(" ")[0])); | 170 | type_1.getElements().get(index).getName().split(" ")[0])); |
168 | it.setFofRole("axiom"); | 171 | it.setFofRole("axiom"); |
169 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 172 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |