aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend')
-rw-r--r--Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend249
1 files changed, 0 insertions, 249 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
deleted file mode 100644
index dcb4bb32..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
+++ /dev/null
@@ -1,249 +0,0 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2
3import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
4import edu.mit.csail.sdg.alloy4compiler.ast.Sig
5import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field
6import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
7import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
16import java.util.Arrays
17import java.util.HashMap
18import java.util.LinkedList
19import java.util.List
20import java.util.Map
21import java.util.Set
22import java.util.SortedSet
23import java.util.TreeSet
24
25import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
26
27class AlloyModelInterpretation implements LogicModelInterpretation{
28
29 protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
30 protected val AlloyModelInterpretation_TypeInterpretation typeInterpretator
31
32 protected val Logic2AlloyLanguageMapper forwardMapper
33 protected val Logic2AlloyLanguageMapperTrace forwardTrace;
34
35 private var ExprVar logicLanguage;
36
37 private var String logicBooleanTrue;
38 private var String logicBooleanFalse;
39 private SortedSet<Integer> integerAtoms = new TreeSet
40 private SortedSet<String> stringAtoms = new TreeSet
41
42 private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap
43 private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap
44
45 private val Map<ConstantDeclaration, Object> constant2Value
46 private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value
47 private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value
48
49 //private val int minInt
50 //private val int maxInt
51
52 public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) {
53 this.typeInterpretator = typeInterpretator
54 this.forwardMapper = forwardMapper
55 this.forwardTrace = trace
56
57 // Maps to trace language elements to the parsed problem.
58 val Map<String, Sig> name2AlloySig = new HashMap
59 val Map<String, Field> name2AlloyField = new HashMap
60 // exploring signatures
61 for(sig:solution.allReachableSigs) {
62 name2AlloySig.put(sig.label,sig)
63 for(field : sig.fields) {
64 name2AlloyField.put(field.label,field)
65 }
66 }
67 val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution)
68 this.typeInterpretator.resolveUnknownAtoms(
69 unknownAtoms,
70 solution,
71 forwardTrace,
72 name2AlloySig,
73 name2AlloyField,
74 alloyAtom2LogicElement,
75 interpretationOfUndefinedType)
76
77 // eval consants
78 constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[
79 solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term
80 ]
81 // eval functions
82 val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function |
83 newHashMap(
84 solution.eval(function.name.lookup(name2AlloyField))
85 .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])]
86
87 val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function |
88 val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField)
89 val paramIndexes = 1..(function.parameters.size)
90 return newHashMap(
91 solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t |
92 new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term])
93 ->
94 t.atom(function.parameters.size + 1).atomLabel2Term
95 ])]
96 this.function2Value = Union(hostedfunction2Value,globalfunction2Value)
97 // eval relations
98 val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation |
99 solution.eval(relation.name.lookup(name2AlloyField)).map[ t |
100 new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet]
101 val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation |
102 solution.eval(relation.name.lookup(name2AlloyField)).map[ t |
103 new ParameterSubstitution((1..<t.arity).map[int a|t.atom(a).atomLabel2Term])].toSet]
104 this.relation2Value = Union(hostedRelation2Value,globalRelation2Value)
105
106 //Int limits
107 //this.minInt = solution.min
108 //this.maxInt = solution.max
109
110 //print(trace)
111 }
112
113 def List<ExprVar> collectUnknownAndResolveKnownAtoms(A4Solution solution) {
114 val Iterable<ExprVar> allAtoms = solution.allAtoms
115 val List<ExprVar> unknownAtoms = new LinkedList
116
117 for(atom: allAtoms) {
118 val typeName = getName(atom.type)
119 val atomName = atom.name
120 println(atom.toString + " < - " + typeName)
121 if(typeName == forwardTrace.logicLanguage.name) {
122 this.logicLanguage = atom
123 } else if(typeName == "Int" || typeName == "seq/Int") {
124 val value = Integer.parseInt(atomName.join)
125 this.integerAtoms.add(value)
126 } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) {
127 if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label }
128 else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label}
129 else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''')
130 } else if(typeName == "String") {
131 val value = parseString(atomName.join)
132 this.stringAtoms.add(value)
133 } else {
134 unknownAtoms += atom
135 }
136 }
137 val integerSignature = solution.allReachableSigs.filter[it.label=="Int"].head
138 for(i : solution.eval(integerSignature)) {
139 val value = Integer.parseInt(i.atom(0))
140 this.integerAtoms.add(value)
141 }
142 val stringSignature = solution.allReachableSigs.filter[it.label=="String"].head
143 for(i : solution.eval(stringSignature)) {
144 val value = parseString(i.atom(0))
145 this.stringAtoms.add(value)
146 }
147 return unknownAtoms
148 }
149
150 def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) {
151 val name = type.toString
152 if(name.startsWith("{this/") && name.endsWith("}")) {
153 return type.toString.replaceFirst("\\{this\\/","").replace("}","")
154 }
155 else throw new IllegalArgumentException('''Unknown type format: "«name»"!''')
156 }
157 def private getName(ExprVar atom) { atom.toString.split("\\$") }
158
159 def print(Logic2AlloyLanguageMapperTrace trace) {
160 println('''Undefined-----''')
161 interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v.map[name]»''')]
162 //println('''Defined-----''')
163 //trace.type2ALSType.keySet.filter(TypeDefinition).forEach[println('''«it.name» -> «it.elements.map[name.join]»''')]
164
165 println('''Constants-----''')
166 constant2Value.forEach[k, v|println('''«k.name» : «v»''')]
167 println('''Functions-----''')
168 function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]]
169 println('''Relations-----''')
170 relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]]
171 }
172
173 override getElements(Type type) { getElementsDispatch(type) }
174 def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) }
175 def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements }
176
177 override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
178 val transformedParams = new ParameterSubstitution(parameterSubstitution)
179 return transformedParams.lookup(
180 function.lookup(this.function2Value)
181 )
182 }
183
184 override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
185 relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution))
186 }
187
188 override getInterpretation(ConstantDeclaration constant) {
189 constant.lookup(this.constant2Value)
190 }
191
192 // Alloy term -> logic term
193 def private atomLabel2Term(String label) {
194 if(label.number) return Integer.parseInt(label)
195 else if(label == this.logicBooleanTrue) return true
196 else if(label == this.logicBooleanFalse) return false
197 else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement)
198 else if(label.isString) return parseString(label)
199 else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''')
200 }
201 def private isNumber(String s) {
202 try{
203 Integer.parseInt(s)
204 return true
205 }catch(NumberFormatException e) {
206 return false
207 }
208 }
209 def private isString(String label) {
210 label.startsWith("\"") && label.endsWith("\"")
211 }
212 def private parseString(String label) {
213 label.substring(1,label.length-1)
214 }
215
216 override getAllIntegersInStructure() {
217 this.integerAtoms
218 }
219
220 override getAllRealsInStructure() {
221 new TreeSet
222 }
223
224 override getAllStringsInStructure() {
225 this.stringAtoms
226 }
227}
228
229/**
230 * Helper class for efficiently matching parameter substitutions for functions and relations.
231 */
232class ParameterSubstitution{
233 val Object[] data;
234
235 new(Object[] data) { this.data = data }
236
237 override equals(Object obj) {
238 if(obj === this) return true
239 else if(obj == null) return false
240 if(obj instanceof ParameterSubstitution) {
241 return Arrays.equals(this.data,obj.data)
242 }
243 return false
244 }
245
246 override hashCode() {
247 Arrays.hashCode(data)
248 }
249} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-18 21:48:05 +0000