diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-09-08 16:12:55 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:42:29 -0400 |
commit | 4aee5bcc86b9e6b515fbbdac030df42147be7dc1 (patch) | |
tree | ce9f8aa1cf0ab33d4304b9ce3a0abf4beb7b757a /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner | |
parent | VAMPIRE: complete first version of VampireModelInterpretation (diff) | |
download | VIATRA-Generator-4aee5bcc86b9e6b515fbbdac030df42147be7dc1.tar.gz VIATRA-Generator-4aee5bcc86b9e6b515fbbdac030df42147be7dc1.tar.zst VIATRA-Generator-4aee5bcc86b9e6b515fbbdac030df42147be7dc1.zip |
VAMPIRE: Implement wf constraint handling
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner')
22 files changed, 298 insertions, 172 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index a2449fc0..14926280 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend | |||
@@ -1,5 +1,10 @@ | |||
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.vampire.reasoner.VampireSolverConfiguration | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion |
@@ -21,18 +26,14 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf | |||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | 26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral |
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | 27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not |
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | 28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or |
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | 29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation |
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | 31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition |
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | 32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue |
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | 33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term |
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | 34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable |
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 36 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
31 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
32 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
33 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
34 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
35 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
36 | import java.util.Collections | 37 | import java.util.Collections |
37 | import java.util.HashMap | 38 | import java.util.HashMap |
38 | import java.util.List | 39 | import java.util.List |
@@ -40,7 +41,7 @@ import java.util.Map | |||
40 | import org.eclipse.xtend.lib.annotations.Accessors | 41 | import org.eclipse.xtend.lib.annotations.Accessors |
41 | 42 | ||
42 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 43 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl |
44 | 45 | ||
45 | class Logic2VampireLanguageMapper { | 46 | class Logic2VampireLanguageMapper { |
46 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 47 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -81,7 +82,8 @@ class Logic2VampireLanguageMapper { | |||
81 | 82 | ||
82 | // RELATION MAPPER | 83 | // RELATION MAPPER |
83 | trace.relationDefinitions = problem.collectRelationDefinitions | 84 | trace.relationDefinitions = problem.collectRelationDefinitions |
84 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] | 85 | // println(problem.relations.filter[class == RelationDefinitionImpl]) |
86 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace, new Logic2VampireLanguageMapper)] | ||
85 | 87 | ||
86 | // CONTAINMENT MAPPER | 88 | // CONTAINMENT MAPPER |
87 | containmentMapper.transformContainment(config,problem.containmentHierarchies, trace) | 89 | containmentMapper.transformContainment(config,problem.containmentHierarchies, trace) |
@@ -140,7 +142,7 @@ class Logic2VampireLanguageMapper { | |||
140 | // //////////// | 142 | // //////////// |
141 | def protected transformAssertion(Assertion assertion, Logic2VampireLanguageMapperTrace trace) { | 143 | def protected transformAssertion(Assertion assertion, Logic2VampireLanguageMapperTrace trace) { |
142 | val res = createVLSFofFormula => [ | 144 | val res = createVLSFofFormula => [ |
143 | it.name = support.toID(assertion.name) | 145 | it.name = support.toID("assertion_" + assertion.name) |
144 | // below is temporary solution | 146 | // below is temporary solution |
145 | it.fofRole = "axiom" | 147 | it.fofRole = "axiom" |
146 | it.fofFormula = assertion.value.transformTerm(trace, Collections.EMPTY_MAP) | 148 | it.fofFormula = assertion.value.transformTerm(trace, Collections.EMPTY_MAP) |
@@ -378,8 +380,18 @@ class Logic2VampireLanguageMapper { | |||
378 | // it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) | 380 | // it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) |
379 | // it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] | 381 | // it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] |
380 | // ] | 382 | // ] |
383 | // println(relation.name) | ||
384 | // if(relation.class == RelationDefinitionImpl) { | ||
385 | // println("(" + (relation as RelationDefinition).getDefines + ")") | ||
386 | // } | ||
381 | return createVLSFunction => [ | 387 | return createVLSFunction => [ |
382 | it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant | 388 | if (relation.class == RelationDeclarationImpl) { |
389 | it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant | ||
390 | } | ||
391 | else { | ||
392 | it.constant = (relation as RelationDefinition).lookup(trace.relDef2Predicate).constant | ||
393 | } | ||
394 | |||
383 | it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] | 395 | it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] |
384 | ] | 396 | ] |
385 | } | 397 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend index 6b383b12..13778dee 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend | |||
@@ -47,6 +47,8 @@ class Logic2VampireLanguageMapperTrace { | |||
47 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | 47 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions |
48 | public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap | 48 | public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap |
49 | public var Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap | 49 | public var Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap |
50 | public var Map<RelationDefinition, VLSFunction> relDef2Predicate = new HashMap | ||
51 | public var Map<VLSFunction, RelationDefinition> predicate2RelDef = new HashMap | ||
50 | 52 | ||
51 | 53 | ||
52 | //NOT NEEDED //public var VLSFunction constantDec | 54 | //NOT NEEDED //public var VLSFunction constantDec |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend new file mode 100644 index 00000000..cf218270 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend | |||
@@ -0,0 +1,5 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | class Logic2VampireLanguageMapper_AssertionMapper { | ||
4 | |||
5 | } \ No newline at end of file | ||
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 18e97020..181c59ca 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 | |||
@@ -1,14 +1,12 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
12 | import java.util.ArrayList | 10 | import java.util.ArrayList |
13 | import java.util.HashMap | 11 | import java.util.HashMap |
14 | import java.util.List | 12 | import java.util.List |
@@ -25,7 +23,7 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
25 | this.base = base | 23 | this.base = base |
26 | } | 24 | } |
27 | 25 | ||
28 | def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) { | 26 | def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) { |
29 | 27 | ||
30 | // 1. store all variables in support wrt their name | 28 | // 1. store all variables in support wrt their name |
31 | // 1.1 if variable has type, creating list of type declarations | 29 | // 1.1 if variable has type, creating list of type declarations |
@@ -81,91 +79,79 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
81 | trace.specification.formulas += comply | 79 | trace.specification.formulas += comply |
82 | } | 80 | } |
83 | 81 | ||
84 | def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) { | 82 | def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) { |
85 | 83 | ||
86 | // // 1. store all variables in support wrt their name | 84 | // println("XXXXXXXXXXXXXXXXX") |
87 | // // 1.1 if variable has type, creating list of type declarations | 85 | |
88 | //// val VLSVariable variable = createVLSVariable => [it.name = "A"] | 86 | // 1. store all variables in support wrt their name |
89 | // val Map<Variable, VLSVariable> relationVar2VLS = new HashMap | 87 | // 1.1 if variable has type, creating list of type declarations |
90 | // val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap | 88 | val Map<Variable, VLSVariable> relVar2VLS = new HashMap |
91 | // val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap | 89 | val List<VLSVariable> vars = newArrayList |
92 | // val typedefs = new ArrayList<VLSTerm> | 90 | val List<VLSFunction> relVar2TypeDecComply = new ArrayList |
93 | // | 91 | for (i : 0 ..< r.parameters.length) { |
94 | // for (variable : reldef.variables) { | 92 | |
95 | // val v = createVLSVariable => [ | 93 | val v = createVLSVariable => [ |
96 | // it.name = support.toIDMultiple("V", variable.name) | 94 | it.name = support.toIDMultiple("V", i.toString) |
97 | // ] | 95 | ] |
98 | // relationVar2VLS.put(variable, v) | 96 | relVar2VLS.put(r.variables.get(i), v) |
99 | // | 97 | vars.add(v) |
100 | // val varTypeComply = createVLSFunction => [ | 98 | |
101 | // it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) | 99 | val relType = (r.parameters.get(i) as ComplexTypeReference).referred |
102 | // it.terms += support.duplicate(v) | 100 | val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v) |
103 | // ] | 101 | relVar2TypeDecComply.add(varTypeComply) |
104 | // relationVar2TypeDecComply.put(variable, varTypeComply) | 102 | |
105 | // relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) | 103 | } |
106 | // } | 104 | |
107 | // val nameArray = reldef.name.split(" ") | 105 | //deciding name of relation |
108 | // val comply = createVLSFofFormula => [ | 106 | val nameArray = r.name.split(" ") |
109 | // it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), | 107 | var relNameVar = "" |
110 | // nameArray.get(nameArray.length - 1)) | 108 | if (nameArray.length == 3) { |
111 | // it.fofRole = "axiom" | 109 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) |
112 | // it.fofFormula = createVLSUniversalQuantifier => [ | 110 | } |
113 | // for (variable : reldef.variables) { | 111 | else { |
114 | // it.variables += support.duplicate(variable.lookup(relationVar2VLS)) | 112 | relNameVar = r.name |
115 | // | 113 | } |
116 | // } | 114 | val relName = relNameVar |
117 | // it.operand = createVLSImplies => [ | 115 | |
118 | // it.left = createVLSFunction => [ | 116 | //define logic for pattern |
119 | // it.constant = support.toIDMultiple("rel", reldef.name) | 117 | // val map = new HashMap |
120 | // for (variable : reldef.variables) { | 118 | // map.put(r.variables.get(0), createVLSVariable) |
121 | // val v = createVLSVariable => [ | 119 | val definition = mapper.transformTerm(r.value, trace, relVar2VLS) |
122 | // it.name = variable.lookup(relationVar2VLS).name | 120 | |
123 | // ] | 121 | |
124 | // it.terms += v | 122 | |
125 | // } | 123 | |
126 | // ] | 124 | //get entire contents of and |
127 | // it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values)) | 125 | val compliance = support.unfoldAnd(relVar2TypeDecComply) |
128 | // ] | 126 | val compDefn = createVLSAnd=> [ |
129 | // ] | 127 | it.left = compliance |
130 | // ] | 128 | it.right = definition |
131 | // | 129 | ] |
132 | // val res = createVLSFofFormula => [ | 130 | |
133 | // it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2), | 131 | val relDef = createVLSFofFormula=> [ |
134 | // nameArray.get(nameArray.length - 1)) | 132 | |
135 | // it.fofRole = "axiom" | 133 | it.name = support.toID(relName) |
136 | // it.fofFormula = createVLSUniversalQuantifier => [ | 134 | it.fofRole = "axiom" |
137 | // for (variable : reldef.variables) { | 135 | it.fofFormula = createVLSUniversalQuantifier => [ |
138 | // val v = createVLSVariable => [ | 136 | for (v : vars) { |
139 | // it.name = variable.lookup(relationVar2VLS).name | 137 | it.variables += support.duplicate(v) |
140 | // ] | 138 | } |
141 | // it.variables += v | 139 | it.operand = createVLSImplies => [ |
142 | // | 140 | val rel = createVLSFunction => [ |
143 | // } | 141 | it.constant = support.toIDMultiple("r", relName) |
144 | // it.operand = createVLSImplies => [ | 142 | for (v : vars) { |
145 | // it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values)) | 143 | it.terms += support.duplicate(v) |
146 | // it.right = createVLSEquivalent => [ | 144 | } |
147 | // it.left = createVLSFunction => [ | 145 | ] |
148 | // it.constant = support.toIDMultiple("rel", reldef.name) | 146 | trace.relDef2Predicate.put(r, rel) |
149 | // for (variable : reldef.variables) { | 147 | trace.predicate2RelDef.put(rel, r) |
150 | // val v = createVLSVariable => [ | 148 | it.left = support.duplicate(rel) |
151 | // it.name = variable.lookup(relationVar2VLS).name | 149 | it.right = compDefn |
152 | // ] | 150 | ] |
153 | // it.terms += v | 151 | ] |
154 | // | 152 | ] |
155 | // } | 153 | |
156 | // ] | 154 | trace.specification.formulas += relDef |
157 | // it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) | ||
158 | // ] | ||
159 | // | ||
160 | // ] | ||
161 | // | ||
162 | // ] | ||
163 | // | ||
164 | // ] | ||
165 | // | ||
166 | // // trace.relationDefinition2Predicate.put(r,res) | ||
167 | // trace.specification.formulas += comply; | ||
168 | // trace.specification.formulas += res; | ||
169 | 155 | ||
170 | } | 156 | } |
171 | 157 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend index 5df47bbc..ef77b6ca 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend | |||
@@ -24,26 +24,28 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | |||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl | 25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl |
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl | 26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl |
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl | ||
27 | import java.util.Arrays | 28 | import java.util.Arrays |
28 | import java.util.HashMap | 29 | import java.util.HashMap |
29 | import java.util.List | 30 | import java.util.List |
30 | import java.util.Map | 31 | import java.util.Map |
31 | import java.util.Set | ||
32 | 32 | ||
33 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 33 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl | 34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition |
35 | import java.util.concurrent.TimeUnit | ||
35 | 36 | ||
36 | class VampireModelInterpretation implements LogicModelInterpretation { | 37 | class VampireModelInterpretation implements LogicModelInterpretation { |
37 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | 38 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE |
38 | 39 | ||
39 | protected val Logic2VampireLanguageMapperTrace forwardTrace; | 40 | protected val Logic2VampireLanguageMapperTrace forwardTrace; |
40 | 41 | ||
41 | //These three maps capture all the information found in the Vampire output | 42 | // These three maps capture all the information found in the Vampire output |
42 | private val Map<String, DefinedElement> name2DefinedElement = new HashMap | 43 | private val Map<String, DefinedElement> name2DefinedElement = new HashMap |
43 | private val Map<TypeDeclaration, List<DefinedElement>> type2DefinedElement = new HashMap | 44 | private val Map<TypeDeclaration, List<DefinedElement>> type2DefinedElement = new HashMap |
44 | private val Map<RelationDeclaration, List<String[]>> rel2Inst = new HashMap | 45 | private val Map<RelationDeclaration, List<String[]>> relDec2Inst = new HashMap |
45 | //end | 46 | private val Map<RelationDefinition, List<String[]>> relDef2Inst = new HashMap |
46 | 47 | ||
48 | // end | ||
47 | public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) { | 49 | public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) { |
48 | this.forwardTrace = trace | 50 | this.forwardTrace = trace |
49 | 51 | ||
@@ -77,6 +79,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
77 | // println() | 79 | // println() |
78 | // println(trace.type2Predicate) | 80 | // println(trace.type2Predicate) |
79 | // Fill keys of map | 81 | // Fill keys of map |
82 | println(trace.type2Predicate.keySet) | ||
80 | val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl] | 83 | val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl] |
81 | val allTypeFunctions = trace.predicate2Type | 84 | val allTypeFunctions = trace.predicate2Type |
82 | println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl]) | 85 | println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl]) |
@@ -86,52 +89,64 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
86 | } | 89 | } |
87 | 90 | ||
88 | // USE THE DECLARE_<TYPE_NAME> FORMULAS TO SEE WHAT THE TYPES ARE | 91 | // USE THE DECLARE_<TYPE_NAME> FORMULAS TO SEE WHAT THE TYPES ARE |
89 | val typeFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_t_"] | 92 | val typeFormulas = model.tfformulas.filter [ |
93 | name.length > 12 && (name.substring(0, 12) == "predicate_t_" || name.substring(0, 12) == "predicate_e_") | ||
94 | ] | ||
90 | // ^this way, we ignore the "object" type | 95 | // ^this way, we ignore the "object" type |
91 | //TODO potentially need to handle the enums in this case as well | 96 | // TODO potentially need to handle the enums in this case as well |
92 | for (formula : typeFormulas) { | 97 | for (formula : typeFormulas) { |
93 | // get associated type | 98 | // get associated type |
94 | val associatedTypeName = (formula as VLSTffFormula).name.substring(10) | 99 | val associatedTypeName = (formula as VLSTffFormula).name.substring(10) |
95 | val associatedFunction = allTypeFunctions.keySet.filter[constant == associatedTypeName]. | 100 | print(associatedTypeName) |
96 | get(0) as VLSFunction | 101 | val associatedFunctions = allTypeFunctions.keySet.filter[constant == associatedTypeName] |
97 | val associatedTypeAll = associatedFunction.lookup(allTypeFunctions) | 102 | if (associatedFunctions.length > 0) { |
103 | val associatedFunction = associatedFunctions.get(0) as VLSFunction | ||
104 | val associatedTypeAll = associatedFunction.lookup(allTypeFunctions) | ||
98 | // val associatedTypeDeclFormula = model.tfformulas.filter[name == ("declare_t_" + associatedTypeName)].get(0) as VLSTffFormula | 105 | // val associatedTypeDeclFormula = model.tfformulas.filter[name == ("declare_t_" + associatedTypeName)].get(0) as VLSTffFormula |
99 | // val associatedTypeDefn = associatedTypeDeclFormula.fofFormula as VLSOtherDeclaration | 106 | // val associatedTypeDefn = associatedTypeDeclFormula.fofFormula as VLSOtherDeclaration |
100 | // val associatedTypeFct = associatedTypeDefn.name as VLSConstant | 107 | // val associatedTypeFct = associatedTypeDefn.name as VLSConstant |
101 | if (associatedTypeAll.class == TypeDeclarationImpl) { | 108 | if (associatedTypeAll.class == TypeDeclarationImpl) { |
102 | val associatedType = associatedTypeAll as TypeDeclaration | 109 | val associatedType = associatedTypeAll as TypeDeclaration |
110 | |||
111 | // get definedElements | ||
112 | var andFormulaTerm = formula.fofFormula | ||
113 | end = false | ||
114 | val List<DefinedElement> instances = newArrayList | ||
115 | while (!end) { | ||
116 | if (andFormulaTerm.class == VLSAndImpl) { | ||
117 | val andFormula = andFormulaTerm as VLSAnd | ||
118 | val andRight = andFormula.right | ||
119 | addIfNotNeg(andRight, instances) | ||
120 | andFormulaTerm = andFormula.left | ||
121 | } else { | ||
122 | addIfNotNeg(andFormulaTerm as VLSTerm, instances) | ||
123 | end = true | ||
124 | } | ||
103 | 125 | ||
104 | // get definedElements | ||
105 | var andFormulaTerm = formula.fofFormula | ||
106 | end = false | ||
107 | val List<DefinedElement> instances = newArrayList | ||
108 | while (!end) { | ||
109 | if (andFormulaTerm.class == VLSAndImpl) { | ||
110 | val andFormula = andFormulaTerm as VLSAnd | ||
111 | val andRight = andFormula.right | ||
112 | addIfNotNeg(andRight, instances) | ||
113 | andFormulaTerm = andFormula.left | ||
114 | } else { | ||
115 | addIfNotNeg(andFormulaTerm as VLSTerm, instances) | ||
116 | end = true | ||
117 | } | 126 | } |
118 | 127 | for (elem : instances) { | |
119 | } | 128 | associatedType.lookup(type2DefinedElement).add(elem) |
120 | for (elem : instances) { | 129 | } |
121 | associatedType.lookup(type2DefinedElement).add(elem) | ||
122 | } | 130 | } |
123 | } | 131 | } |
132 | |||
124 | } | 133 | } |
125 | 134 | ||
126 | printMap() | 135 | printMap() |
127 | 136 | ||
128 | // 3. get relations | 137 | // 3. get relations |
129 | // Fill keys of map | 138 | // Fill keys of map |
130 | val allRelDecls = trace.rel2Predicate.keySet.filter[class == RelationDeclarationImpl] | 139 | val allRelDecls = trace.rel2Predicate.keySet |
131 | val allRelFunctions = trace.predicate2Relation | 140 | val allRelDefns = trace.relDef2Predicate.keySet |
141 | val allRelDeclFunctions = trace.predicate2Relation | ||
142 | val allRelDefnFunctions = trace.predicate2RelDef | ||
132 | 143 | ||
133 | for (rel : allRelDecls) { | 144 | for (rel : allRelDecls) { |
134 | rel2Inst.put(rel as RelationDeclaration, newArrayList) | 145 | relDec2Inst.put(rel as RelationDeclaration, newArrayList) |
146 | } | ||
147 | |||
148 | for (rel : allRelDefns) { | ||
149 | relDef2Inst.put(rel as RelationDefinition, newArrayList) | ||
135 | } | 150 | } |
136 | 151 | ||
137 | // USE THE DECLARE_<RELATION_NAME> FORMULAS TO SEE WHAT THE RELATIONS ARE | 152 | // USE THE DECLARE_<RELATION_NAME> FORMULAS TO SEE WHAT THE RELATIONS ARE |
@@ -140,34 +155,40 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
140 | for (formula : relFormulas) { | 155 | for (formula : relFormulas) { |
141 | // get associated type | 156 | // get associated type |
142 | val associatedRelName = (formula as VLSTffFormula).name.substring(10) | 157 | val associatedRelName = (formula as VLSTffFormula).name.substring(10) |
143 | val associatedRelFunction = allRelFunctions.keySet.filter[constant == associatedRelName]. | 158 | |
144 | get(0) as VLSFunction | 159 | // TRY FOR DECLARATION |
145 | val associatedRel = associatedRelFunction.lookup(allRelFunctions) as RelationDeclaration | 160 | val associatedRelFunctionList = allRelDeclFunctions.keySet.filter[constant == associatedRelName] |
146 | 161 | if (associatedRelFunctionList.isEmpty) { | |
147 | // get definedElements | 162 | // THEN IT IS NOT A DECLARATION |
148 | var andFormulaTerm = formula.fofFormula | 163 | } else { |
149 | end = false | 164 | val associatedRelFunction = associatedRelFunctionList.get(0) as VLSFunction // ASSUMING ONLY 1 SATISFIES QUERY |
150 | val List<String[]> instances = newArrayList | 165 | val associatedRel = associatedRelFunction.lookup(allRelDeclFunctions) as RelationDeclaration |
151 | while (!end) { | 166 | |
152 | if (andFormulaTerm.class == VLSAndImpl) { | 167 | // get definedElements |
153 | val andFormula = andFormulaTerm as VLSAnd | 168 | var andFormulaTerm = formula.fofFormula |
154 | val andRight = andFormula.right | 169 | end = false |
155 | addRelIfNotNeg(andRight, instances) | 170 | val List<String[]> instances = newArrayList |
156 | andFormulaTerm = andFormula.left | 171 | while (!end) { |
157 | } else { | 172 | if (andFormulaTerm.class == VLSAndImpl) { |
158 | addRelIfNotNeg(andFormulaTerm as VLSTerm, instances) | 173 | val andFormula = andFormulaTerm as VLSAnd |
159 | end = true | 174 | val andRight = andFormula.right |
175 | addRelIfNotNeg(andRight, instances) | ||
176 | andFormulaTerm = andFormula.left | ||
177 | } else { | ||
178 | addRelIfNotNeg(andFormulaTerm as VLSTerm, instances) | ||
179 | end = true | ||
180 | } | ||
181 | |||
182 | } | ||
183 | for (elem : instances) { | ||
184 | associatedRel.lookup(relDec2Inst).add(elem) | ||
160 | } | 185 | } |
161 | 186 | ||
162 | } | 187 | } |
163 | for (elem : instances) { | ||
164 | associatedRel.lookup(rel2Inst).add(elem) | ||
165 | } | ||
166 | 188 | ||
167 | } | 189 | } |
168 | 190 | ||
169 | // printMap2() | 191 | // printMap2() |
170 | |||
171 | } | 192 | } |
172 | 193 | ||
173 | def printMap() { | 194 | def printMap() { |
@@ -182,12 +203,12 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
182 | } | 203 | } |
183 | println() | 204 | println() |
184 | } | 205 | } |
185 | 206 | ||
186 | def printMap2() { | 207 | def printMap2() { |
187 | println("------------------") | 208 | println("------------------") |
188 | for (key : rel2Inst.keySet) { | 209 | for (key : relDec2Inst.keySet) { |
189 | println(key.name + "==>") | 210 | println(key.name + "==>") |
190 | for (elem : key.lookup(rel2Inst)) { | 211 | for (elem : key.lookup(relDec2Inst)) { |
191 | print("[" + elem.get(0) + "-" + elem.get(1) + "], ") | 212 | print("[" + elem.get(0) + "-" + elem.get(1) + "], ") |
192 | } | 213 | } |
193 | println() | 214 | println() |
@@ -203,7 +224,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
203 | list.add(defnElem) | 224 | list.add(defnElem) |
204 | } | 225 | } |
205 | } | 226 | } |
206 | 227 | ||
207 | def private addRelIfNotNeg(VLSTerm term, List<String[]> list) { | 228 | def private addRelIfNotNeg(VLSTerm term, List<String[]> list) { |
208 | if (term.class != VLSUnaryNegationImpl) { | 229 | if (term.class != VLSUnaryNegationImpl) { |
209 | val nodeName1 = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor | 230 | val nodeName1 = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor |
@@ -232,14 +253,19 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
232 | } | 253 | } |
233 | 254 | ||
234 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | 255 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { |
256 | print("-- " + relation.name) | ||
235 | val node1 = (parameterSubstitution.get(0) as DefinedElement).name | 257 | val node1 = (parameterSubstitution.get(0) as DefinedElement).name |
236 | val node2 = (parameterSubstitution.get(1) as DefinedElement).name | 258 | val node2 = (parameterSubstitution.get(1) as DefinedElement).name |
237 | val realRelations = relation.lookup(rel2Inst) | 259 | val realRelations = relation.lookup(relDec2Inst) |
238 | for (real : realRelations){ | 260 | for (real : realRelations) { |
239 | if(real.contains(node1) && real.contains(node2)){ | 261 | if (real.contains(node1) && real.contains(node2)) { |
262 | println(" true") | ||
263 | TimeUnit.SECONDS.sleep(1) | ||
240 | return true | 264 | return true |
241 | } | 265 | } |
242 | } | 266 | } |
267 | println(" false") | ||
268 | TimeUnit.SECONDS.sleep(1) | ||
243 | return false | 269 | return false |
244 | } | 270 | } |
245 | 271 | ||
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 a1d6f783..972af7b4 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 6ac0457b..071db3ce 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 f5991439..b1e3b95d 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 0d6c8b61..31cc2f43 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 659d4637..552bcd6c 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 927327e1..680bcfe1 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 d8fc0296..9cc64d7c 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 bc3caa3b..803b5fed 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 299c4e0c..0083e90f 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 da8c1d26..7e8b1703 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 adc3fff4..081757ca 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 2ab5b32f..3471f95b 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 41af19ec..1c707ca6 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 2b46d5c2..d8e3808c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index 58da7ccd..f8a65187 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java | |||
@@ -21,6 +21,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | |||
21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
23 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 23 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
24 | import com.google.common.base.Objects; | ||
24 | import com.google.common.collect.Iterables; | 25 | import com.google.common.collect.Iterables; |
25 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | 26 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; |
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; | 27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; |
@@ -52,6 +53,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | |||
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | 55 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; |
56 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl; | ||
55 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 57 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
56 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 58 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
57 | import java.util.Arrays; | 59 | import java.util.Arrays; |
@@ -117,7 +119,8 @@ public class Logic2VampireLanguageMapper { | |||
117 | } | 119 | } |
118 | trace.relationDefinitions = this.collectRelationDefinitions(problem); | 120 | trace.relationDefinitions = this.collectRelationDefinitions(problem); |
119 | final Consumer<Relation> _function_3 = (Relation it) -> { | 121 | final Consumer<Relation> _function_3 = (Relation it) -> { |
120 | this.relationMapper.transformRelation(it, trace); | 122 | Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper(); |
123 | this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper); | ||
121 | }; | 124 | }; |
122 | problem.getRelations().forEach(_function_3); | 125 | problem.getRelations().forEach(_function_3); |
123 | this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); | 126 | this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); |
@@ -169,7 +172,9 @@ public class Logic2VampireLanguageMapper { | |||
169 | { | 172 | { |
170 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 173 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
171 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 174 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
172 | it.setName(this.support.toID(assertion.getName())); | 175 | String _name = assertion.getName(); |
176 | String _plus = ("assertion_" + _name); | ||
177 | it.setName(this.support.toID(_plus)); | ||
173 | it.setFofRole("axiom"); | 178 | it.setFofRole("axiom"); |
174 | it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP)); | 179 | it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP)); |
175 | }; | 180 | }; |
@@ -346,7 +351,13 @@ public class Logic2VampireLanguageMapper { | |||
346 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 351 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
347 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 352 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
348 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 353 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
349 | it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); | 354 | Class<? extends Relation> _class = relation.getClass(); |
355 | boolean _equals = Objects.equal(_class, RelationDeclarationImpl.class); | ||
356 | if (_equals) { | ||
357 | it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); | ||
358 | } else { | ||
359 | it.setConstant(CollectionsUtil.<RelationDefinition, VLSFunction>lookup(((RelationDefinition) relation), trace.relDef2Predicate).getConstant()); | ||
360 | } | ||
350 | EList<VLSTerm> _terms = it.getTerms(); | 361 | EList<VLSTerm> _terms = it.getTerms(); |
351 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { | 362 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { |
352 | return this.transformTerm(p, trace, variables); | 363 | return this.transformTerm(p, trace, variables); |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index 4e77d45d..22df456b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java | |||
@@ -55,6 +55,10 @@ public class Logic2VampireLanguageMapperTrace { | |||
55 | 55 | ||
56 | public Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap<VLSFunction, RelationDeclaration>(); | 56 | public Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap<VLSFunction, RelationDeclaration>(); |
57 | 57 | ||
58 | public Map<RelationDefinition, VLSFunction> relDef2Predicate = new HashMap<RelationDefinition, VLSFunction>(); | ||
59 | |||
60 | public Map<VLSFunction, RelationDefinition> predicate2RelDef = new HashMap<VLSFunction, RelationDefinition>(); | ||
61 | |||
58 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | 62 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); |
59 | 63 | ||
60 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); | 64 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); |
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 143d3db5..c175c72a 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,6 +3,7 @@ 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.VLSAnd; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
@@ -17,11 +18,15 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | |||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
20 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 22 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
21 | import java.util.ArrayList; | 23 | import java.util.ArrayList; |
22 | import java.util.Arrays; | 24 | import java.util.Arrays; |
25 | import java.util.HashMap; | ||
23 | import java.util.List; | 26 | import java.util.List; |
27 | import java.util.Map; | ||
24 | import org.eclipse.emf.common.util.EList; | 28 | import org.eclipse.emf.common.util.EList; |
29 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
25 | import org.eclipse.xtext.xbase.lib.Conversions; | 30 | import org.eclipse.xtext.xbase.lib.Conversions; |
26 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | 31 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; |
27 | import org.eclipse.xtext.xbase.lib.Extension; | 32 | import org.eclipse.xtext.xbase.lib.Extension; |
@@ -41,7 +46,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
41 | this.base = base; | 46 | this.base = base; |
42 | } | 47 | } |
43 | 48 | ||
44 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { | 49 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { |
45 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); | 50 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); |
46 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | 51 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); |
47 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | 52 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; |
@@ -109,19 +114,94 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
109 | _formulas.add(comply); | 114 | _formulas.add(comply); |
110 | } | 115 | } |
111 | 116 | ||
112 | public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { | 117 | public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { |
118 | final Map<Variable, VLSVariable> relVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
119 | final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList(); | ||
120 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
121 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
122 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
123 | for (final Integer i : _doubleDotLessThan) { | ||
124 | { | ||
125 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
126 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
127 | it.setName(this.support.toIDMultiple("V", i.toString())); | ||
128 | }; | ||
129 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
130 | relVar2VLS.put(r.getVariables().get((i).intValue()), v); | ||
131 | vars.add(v); | ||
132 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
133 | final Type relType = ((ComplexTypeReference) _get).getReferred(); | ||
134 | final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v); | ||
135 | relVar2TypeDecComply.add(varTypeComply); | ||
136 | } | ||
137 | } | ||
138 | final String[] nameArray = r.getName().split(" "); | ||
139 | String relNameVar = ""; | ||
140 | int _length_1 = nameArray.length; | ||
141 | boolean _equals = (_length_1 == 3); | ||
142 | if (_equals) { | ||
143 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | ||
144 | } else { | ||
145 | relNameVar = r.getName(); | ||
146 | } | ||
147 | final String relName = relNameVar; | ||
148 | final VLSTerm definition = mapper.transformTerm(r.getValue(), trace, relVar2VLS); | ||
149 | final VLSTerm compliance = this.support.unfoldAnd(relVar2TypeDecComply); | ||
150 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
151 | final Procedure1<VLSAnd> _function = (VLSAnd it) -> { | ||
152 | it.setLeft(compliance); | ||
153 | it.setRight(definition); | ||
154 | }; | ||
155 | final VLSAnd compDefn = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function); | ||
156 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
157 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
158 | it.setName(this.support.toID(relName)); | ||
159 | it.setFofRole("axiom"); | ||
160 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
161 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
162 | for (final VLSVariable v : vars) { | ||
163 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
164 | VLSVariable _duplicate = this.support.duplicate(v); | ||
165 | _variables.add(_duplicate); | ||
166 | } | ||
167 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
168 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | ||
169 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
170 | final Procedure1<VLSFunction> _function_4 = (VLSFunction it_3) -> { | ||
171 | it_3.setConstant(this.support.toIDMultiple("r", relName)); | ||
172 | for (final VLSVariable v_1 : vars) { | ||
173 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
174 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); | ||
175 | _terms.add(_duplicate_1); | ||
176 | } | ||
177 | }; | ||
178 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_4); | ||
179 | trace.relDef2Predicate.put(r, rel); | ||
180 | trace.predicate2RelDef.put(rel, r); | ||
181 | it_2.setLeft(this.support.duplicate(rel)); | ||
182 | it_2.setRight(compDefn); | ||
183 | }; | ||
184 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
185 | it_1.setOperand(_doubleArrow); | ||
186 | }; | ||
187 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
188 | it.setFofFormula(_doubleArrow); | ||
189 | }; | ||
190 | final VLSFofFormula relDef = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | ||
191 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
192 | _formulas.add(relDef); | ||
113 | } | 193 | } |
114 | 194 | ||
115 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { | 195 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { |
116 | if (r instanceof RelationDeclaration) { | 196 | if (r instanceof RelationDeclaration) { |
117 | _transformRelation((RelationDeclaration)r, trace); | 197 | _transformRelation((RelationDeclaration)r, trace, mapper); |
118 | return; | 198 | return; |
119 | } else if (r instanceof RelationDefinition) { | 199 | } else if (r instanceof RelationDefinition) { |
120 | _transformRelation((RelationDefinition)r, trace); | 200 | _transformRelation((RelationDefinition)r, trace, mapper); |
121 | return; | 201 | return; |
122 | } else { | 202 | } else { |
123 | throw new IllegalArgumentException("Unhandled parameter types: " + | 203 | throw new IllegalArgumentException("Unhandled parameter types: " + |
124 | Arrays.<Object>asList(r, trace).toString()); | 204 | Arrays.<Object>asList(r, trace, mapper).toString()); |
125 | } | 205 | } |
126 | } | 206 | } |
127 | } | 207 | } |