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/src/ca/mcgill | |
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/src/ca/mcgill')
5 files changed, 194 insertions, 163 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 | ||