1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
|
package hu.bme.mit.inf.dslreasoner.smt.reasoner
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.smt.reasoner.builder.SmtModelQueryEngine
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration
import org.eclipse.xtend.lib.annotations.Accessors
import org.eclipse.xtend.lib.annotations.Data
import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral
import java.util.TreeSet
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealLiteral
@Data
class ValueType {
TypeDescriptor descriptor
Object value
}
class SmtModelInterpretation implements LogicModelInterpretation {
//val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
@Accessors(PUBLIC_GETTER) val SmtModelQueryEngine queryEngine;
// Trace info
val SMTDocument document
val Logic2SmtMapperTrace newTrace;
val Logic2SMT_TypeMapperInterpretation typeInterpretation
/**
* Creates a model builder which queries a logic structure.
* @param document The whole SMT2 document.
* @param trace The trace of the [Logic problem -> SMT problem] mapping
*/
new(LogicProblem problem, SMTDocument document, Logic2SmtMapper forwardMapper, Logic2SmtMapperTrace forwardTrace) {
//document.input.typeDeclarations.forEach[typeNames.put(it.name,it)]
this.document = document
this.queryEngine = new SmtModelQueryEngine(document)
this.newTrace = initialiseNewTrace(document,forwardTrace)
this.typeInterpretation = forwardMapper.typeMapper.getTypeInterpretation(problem,document,this,newTrace)
}
/**
* Creates a new trace from the logic model to the new smt file by using the old trace.
*/
def protected Logic2SmtMapperTrace initialiseNewTrace(SMTDocument document, Logic2SmtMapperTrace oldTrace) {
val i = document.input
val res = new Logic2SmtMapperTrace => [ typeMapperTrace = oldTrace.typeMapperTrace.copy(i) ]
for(entry : oldTrace.relationUnfolding.entrySet) {
val rel = entry.key
val descriptors = entry.value.map[old |
new Descriptor<Relation>(
old.parameterTypes.map[copyTypeDescriptor(i)],
old.relation)
]
res.relationUnfolding.put(rel,descriptors)
}
for(entry : oldTrace.relationMap.entrySet) {
val desc = new Descriptor<Relation>(
entry.key.parameterTypes.map[copyTypeDescriptor(i)],
entry.key.relation)
val fun = i.functionDeclarations.filter[it.name == entry.value.name].head
res.relationMap.put(desc,fun)
}
return res
}
def private copyTypeDescriptor(TypeDescriptor original, SMTInput i) {
if(original.complexType == null) return original
else {
val newType = i.typeDeclarations.filter[it.name == original.complexType.name].head
new TypeDescriptor(newType)
}
}
/*def protected initialiseTypes(SMTDocument document) {
val model = document.output.getModelResult as SMTModelResult
val smtUndefinedType2LogicType = this.newTrace.typeDeclarationMap.bijectiveInverse
for(cardinalityConstraint : model.typeDefinitions) {
val targetType = (cardinalityConstraint.type as SMTComplexTypeReference).referred as SMTSetTypeDeclaration
val List<DefinedElement> elementCollection = new LinkedList
for(element : cardinalityConstraint.elements.map[symbolicReference]) {
if(element instanceof SMTFunctionDeclaration) {
val definedElementRepresentation = createDefinedElement => [name += element.name.split("!")]
newElement2Constants.put(definedElementRepresentation,element)
newConstants2Elements.put(element,definedElementRepresentation)
} else{
throw new UnsupportedOperationException(
"Unresolvable reference in cardinality constraint: " + element.class.name + ": " + element.name)
}
}
undefinedTypeDefinitions.put(targetType.lookup(smtUndefinedType2LogicType),elementCollection);
}
}*/
def private dispatch ValueType logicLiteral2SmtLiteral(Integer literal) {
new ValueType(TypeDescriptor::numericTypeDescriptor_Instance, literal)
}
def private dispatch ValueType logicLiteral2SmtLiteral(Boolean literal) {
new ValueType(TypeDescriptor::logicTypeDescriptor_Instance, literal)
}
def private dispatch ValueType logicLiteral2SmtLiteral(DefinedElement literal) {
this.typeInterpretation.logicElement2Smt(literal)
}
// def private dispatch Object smt2Literal2LogicLiteral(Integer literal) { literal }
// def private dispatch Object smt2Literal2LogicLiteral(Boolean literal) { literal }
// def private dispatch Object smt2Literal2LogicLiteral(SMTSymbolicDeclaration literal) {
// this.typeInterpretation.smtElement2Logic(literal)
// }
override getElements(Type type) {
return this.typeInterpretation.getElements(type)
}
override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
/*queryEngine.resolveFunctionDeclaration(
function.lookup(newTrace.functionDeclarationMap),
parameterSubstitution.map[logicLiteral2SmtLiteral]
).smt2Literal2LogicLiteral*/
throw new UnsupportedOperationException
}
override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
val transformedParameters = parameterSubstitution.map[logicLiteral2SmtLiteral]
val smtFunction = new Descriptor<Relation>(
transformedParameters.map[descriptor],
relation)
.lookup(newTrace.relationMap)
val result = queryEngine.resolveFunctionDeclaration(
smtFunction as SMTFunctionDeclaration,
transformedParameters.map[value]
) as Boolean
return result
}
override getInterpretation(ConstantDeclaration constant) {
/*queryEngine.resolveFunctionDeclaration(
constant.lookup(newTrace.constantDeclarationMap),
Collections.EMPTY_LIST
).smt2Literal2LogicLiteral*/
throw new UnsupportedOperationException
}
override getAllIntegersInStructure() {
val res = new TreeSet
for(literal : document.eAllContents.filter(SMTIntLiteral).toIterable) {
res += literal.value
res += -literal.value
}
res
}
override getAllRealsInStructure() {
val res = new TreeSet
for(literal : document.eAllContents.filter(SMTRealLiteral).toIterable) {
res += literal.value
res += -literal.value
}
res
}
override getAllStringsInStructure() {
new TreeSet
}
}
|
