diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf')
16 files changed, 3113 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend new file mode 100644 index 00000000..44708f44 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend | |||
@@ -0,0 +1,36 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration | ||
6 | import java.util.List | ||
7 | import java.util.Map | ||
8 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
9 | |||
10 | class Logic2SMT_TypeMapperInterpretation { | ||
11 | |||
12 | val Map<Type, ? extends List<DefinedElement>> type2Elements | ||
13 | val Map<DefinedElement, ValueType> logic2smt | ||
14 | val Map<SMTSymbolicDeclaration, DefinedElement> smt2logic | ||
15 | |||
16 | public new( | ||
17 | Map<Type, ? extends List<DefinedElement>> type2Elements, | ||
18 | Map<DefinedElement, ValueType> logic2smt, | ||
19 | Map<SMTSymbolicDeclaration, DefinedElement> smt2logic) { | ||
20 | this.type2Elements = type2Elements | ||
21 | this.logic2smt = logic2smt | ||
22 | this.smt2logic = smt2logic | ||
23 | } | ||
24 | |||
25 | public def getElements(Type type) { | ||
26 | return type2Elements.get(type) | ||
27 | } | ||
28 | |||
29 | public def ValueType logicElement2Smt(DefinedElement element) { | ||
30 | return element.lookup(this.logic2smt) | ||
31 | } | ||
32 | |||
33 | public def smtElement2Logic(SMTSymbolicDeclaration element) { | ||
34 | return element.lookup(this.smt2logic) | ||
35 | } | ||
36 | } | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend new file mode 100644 index 00000000..aad43716 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend | |||
@@ -0,0 +1,1055 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
47 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd | ||
48 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion | ||
49 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference | ||
50 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference | ||
51 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
52 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
53 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference | ||
54 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr | ||
55 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression | ||
56 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealTypeReference | ||
57 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTReasoningTactic | ||
58 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable | ||
59 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue | ||
60 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm | ||
61 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType | ||
62 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | ||
63 | import java.util.ArrayList | ||
64 | import java.util.HashMap | ||
65 | import java.util.LinkedHashMap | ||
66 | import java.util.LinkedList | ||
67 | import java.util.List | ||
68 | import java.util.Map | ||
69 | import org.eclipse.emf.ecore.EObject | ||
70 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
71 | import org.eclipse.xtend.lib.annotations.Accessors | ||
72 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | ||
73 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
74 | import org.eclipse.xtext.xbase.lib.Functions.Function2 | ||
75 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
76 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition | ||
77 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy | ||
78 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | ||
79 | |||
80 | class Logic2SmtMapper{ | ||
81 | val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE | ||
82 | val Logic2SmtMapper_UnfoldingSupport unfolder = new Logic2SmtMapper_UnfoldingSupport | ||
83 | @Accessors val Logic2Smt_TypeMapper typeMapper; | ||
84 | |||
85 | LogicProblemBuilder b | ||
86 | |||
87 | new(Logic2Smt_TypeMapper typeMapper) { | ||
88 | this.typeMapper = typeMapper | ||
89 | } | ||
90 | |||
91 | public def TracedOutput<SMTDocument, Logic2SmtMapperTrace> transformProblem(LogicProblem problem, TypeScopes scope, SMTReasoningTactic strategy) { | ||
92 | val documentInput = createSMTInput => [getModelCommand = createSMTGetModelCommand] | ||
93 | if(strategy == null) documentInput.satCommand = createSMTSimpleSatCommand | ||
94 | else documentInput.satCommand = createSMTComplexSatCommand => [it.method = EcoreUtil.copy(strategy)] | ||
95 | |||
96 | val document = createSMTDocument => [input = documentInput] | ||
97 | val trace = new Logic2SmtMapperTrace => [ | ||
98 | it.forwardMapper = this | ||
99 | it.problem = problem | ||
100 | ] | ||
101 | // Trafo | ||
102 | this.typeMapper.transformTypes(documentInput,problem,trace, scope) | ||
103 | problem.functions.filter(FunctionDeclaration).forEach[it.transformFunctionDeclaration(documentInput,trace)] | ||
104 | problem.functions.filter(FunctionDefinition) .forEach[it.transformFunctionDefinition(documentInput,trace)] | ||
105 | problem.relations.filter(RelationDeclaration).forEach[it.transformRelationDeclaration(documentInput,trace)] | ||
106 | problem.relations.filter(RelationDefinition) .forEach[it.transformRelationDefinition(documentInput,trace)] | ||
107 | problem.constants.filter(ConstantDeclaration).forEach[it.transformConstantDeclaration(documentInput,trace)] | ||
108 | problem.constants.filter(ConstantDefinition) .forEach[it.transformConstantDefinition(documentInput,trace)] | ||
109 | |||
110 | problem.relations.filter(RelationDefinition).forEach[it.transformRelationDefinition_definition(documentInput,trace)] | ||
111 | documentInput.assertions += problem.assertions.map[transformAssertion(trace)] | ||
112 | // End trafo | ||
113 | |||
114 | document.input.assertions.forEach[it.value.nameAllUnnamedVariable] | ||
115 | document.input.functionDefinition.forEach[it.value.nameAllUnnamedVariable] | ||
116 | document.cleanDocument | ||
117 | return new TracedOutput(document,trace) | ||
118 | } | ||
119 | |||
120 | private def toID(String name) {name.split("\\s+").join("!") } | ||
121 | |||
122 | private def nameAllUnnamedVariable(SMTTerm root) { | ||
123 | var index = 1 | ||
124 | val unnamedVariables = root.eAllContents.filter(SMTSortedVariable).filter[it.name == null].toList | ||
125 | for(unnamedVariable : unnamedVariables) { | ||
126 | unnamedVariable.name = '''var«index++»''' | ||
127 | } | ||
128 | } | ||
129 | |||
130 | // def protected maxIntegerRageDefiniton(SMTInput documentInput) { | ||
131 | // val upperlimit = createSMTFunctionDeclaration | ||
132 | // } | ||
133 | |||
134 | def dispatch protected List<TypeConstraint> transformTypeReference(BoolTypeReference boolTypeReference, Logic2SmtMapperTrace trace) { | ||
135 | return #[new TypeConstraint(createSMTBoolTypeReference,null)] | ||
136 | } | ||
137 | def dispatch protected List<TypeConstraint> transformTypeReference(IntTypeReference intTypeReference, Logic2SmtMapperTrace trace) { | ||
138 | return #[new TypeConstraint(createSMTIntTypeReference,null)] | ||
139 | } | ||
140 | def dispatch protected List<TypeConstraint> transformTypeReference(RealTypeReference realTypeReference, Logic2SmtMapperTrace trace) { | ||
141 | return #[new TypeConstraint(createSMTRealTypeReference,null)] | ||
142 | } | ||
143 | def dispatch protected List<TypeConstraint> transformTypeReference(ComplexTypeReference complexTypeReference, Logic2SmtMapperTrace trace) { | ||
144 | return typeMapper.transformTypeReference(complexTypeReference.referred,trace) | ||
145 | } | ||
146 | |||
147 | /////////////////////////////////////////////////////// | ||
148 | // Definitions | ||
149 | /////////////////////////////////////////////////////// | ||
150 | |||
151 | def transformFunctionDeclaration(FunctionDeclaration function, SMTInput input, Logic2SmtMapperTrace trace) { | ||
152 | val parameterTypeCombinations = unfolder.getPermutations(function.parameters.map[x|transformTypeReference(x,trace)]) | ||
153 | val rangeTypeCombinations = function.range.transformTypeReference(trace) | ||
154 | |||
155 | if(rangeTypeCombinations.size == 1) { | ||
156 | val rangeType = rangeTypeCombinations.head | ||
157 | // Map it as function | ||
158 | var index = 1 | ||
159 | for(combination : parameterTypeCombinations) { | ||
160 | val nameWithIndex = if (parameterTypeCombinations.size > 1) | ||
161 | toID('''function «function.name.toID» «index++»''') | ||
162 | else | ||
163 | toID('''function «function.name.toID»''') | ||
164 | |||
165 | createFunctionDeclaration(function,nameWithIndex,combination,rangeType,true, input,trace) | ||
166 | } | ||
167 | } else { | ||
168 | // Map it as a relation | ||
169 | var index = 1 | ||
170 | for(combination : parameterTypeCombinations) { | ||
171 | val type2function = new HashMap | ||
172 | for(rangeType : rangeTypeCombinations) { | ||
173 | val nameWithIndex = toID('''function «function.name.toID» «index++»''') | ||
174 | val f = createFunctionDeclaration(function,nameWithIndex,combination,rangeType,false,input,trace) | ||
175 | type2function.put(rangeType,f) | ||
176 | } | ||
177 | // for all rangeTypes, there is | ||
178 | // 1. at least one range type that satisfies the relation | ||
179 | input.assertions+=createSMTAssertion => [ | ||
180 | it.value = createSMTForall => [f| | ||
181 | var paramIndex = 1 | ||
182 | for(param : combination) { | ||
183 | val paramName = '''p«paramIndex++»''' | ||
184 | val variable = createSMTSortedVariable => [ | ||
185 | it.name = paramName | ||
186 | it.range = param.type | ||
187 | ] | ||
188 | f.quantifiedVariables += variable | ||
189 | } | ||
190 | f.expression = createSMTOr => [ | ||
191 | operands+=rangeTypeCombinations.map[t| | ||
192 | createSMTExists => [ | ||
193 | val v = createSMTSortedVariable => [ | ||
194 | it.name = "r" | ||
195 | it.range = EcoreUtil.copy(t.type) | ||
196 | ] | ||
197 | it.quantifiedVariables += v | ||
198 | it.expression = createSMTSymbolicValue => [ | ||
199 | it.symbolicReference = type2function.get(t) | ||
200 | it.parameterSubstitutions += f.quantifiedVariables.map[fv| | ||
201 | createSMTSymbolicValue => [it.symbolicReference = fv] | ||
202 | ] | ||
203 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = v] | ||
204 | ] | ||
205 | ] | ||
206 | ] | ||
207 | ] | ||
208 | ] | ||
209 | ] | ||
210 | // 2. at most one range type that satisfies the relation | ||
211 | // TODO a | ||
212 | } | ||
213 | } | ||
214 | } | ||
215 | |||
216 | private def createFunctionDeclaration( | ||
217 | Function function, | ||
218 | String nameWithIndex, | ||
219 | List<TypeConstraint> combination, | ||
220 | TypeConstraint rangeType, | ||
221 | boolean useFunction, | ||
222 | SMTInput input, | ||
223 | Logic2SmtMapperTrace trace | ||
224 | ) { | ||
225 | val smtFunction = if(useFunction) { | ||
226 | createSMTFunctionDeclaration => [ | ||
227 | it.name = nameWithIndex | ||
228 | it.parameters += combination.map[it.type] | ||
229 | it.range = rangeType.type | ||
230 | ] | ||
231 | } else { | ||
232 | createSMTFunctionDeclaration => [ | ||
233 | it.name = nameWithIndex | ||
234 | it.parameters += combination.map[it.type] | ||
235 | it.parameters += rangeType.type | ||
236 | it.range = createSMTBoolTypeReference | ||
237 | ] | ||
238 | } | ||
239 | |||
240 | val descriptor = new Descriptor<Function>((combination+#[rangeType]).toList.map[ | ||
241 | TypeDescriptor.createFromTypeReference(it.type)],function) | ||
242 | trace.functionMap.put(descriptor,smtFunction) | ||
243 | input.functionDeclarations += smtFunction | ||
244 | trace.functionUnfolding.put(function,#[descriptor]) | ||
245 | |||
246 | if(!useFunction) { | ||
247 | input.assertions += createSMTAssertion => [ | ||
248 | it.value = createSMTForall => [f| | ||
249 | var pi = 0 | ||
250 | for(param : combination) { | ||
251 | val variable = createSMTSortedVariable | ||
252 | variable.name = "p"+pi.toString | ||
253 | variable.range = EcoreUtil.copy(combination.get(pi).type) | ||
254 | f.quantifiedVariables+=variable | ||
255 | pi++ | ||
256 | } | ||
257 | val resultParam1 = createSMTSortedVariable => [ | ||
258 | it.name = "res1" | ||
259 | it.range = EcoreUtil.copy(rangeType.type) | ||
260 | ] | ||
261 | f.quantifiedVariables+=resultParam1 | ||
262 | val resultParam2 = createSMTSortedVariable => [ | ||
263 | it.name = "res2" | ||
264 | it.range = EcoreUtil.copy(rangeType.type) | ||
265 | ] | ||
266 | f.quantifiedVariables+=resultParam2 | ||
267 | f.expression = createSMTImpl => [ | ||
268 | it.leftOperand = createSMTAnd => [ | ||
269 | it.operands += createSMTSymbolicValue => [ | ||
270 | it.symbolicReference = smtFunction | ||
271 | it.parameterSubstitutions += (0..<combination.size).map[x| | ||
272 | createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]] | ||
273 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam1] | ||
274 | ] | ||
275 | it.operands += createSMTSymbolicValue => [ | ||
276 | it.symbolicReference = smtFunction | ||
277 | it.parameterSubstitutions += (0..<combination.size).map[x| | ||
278 | createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]] | ||
279 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam2] | ||
280 | ] | ||
281 | ] | ||
282 | it.rightOperand = createSMTEquals => [ | ||
283 | it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam1] | ||
284 | it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam2] | ||
285 | ] | ||
286 | ] | ||
287 | ] | ||
288 | ] | ||
289 | } | ||
290 | |||
291 | if(rangeType.constraint != null) { | ||
292 | input.assertions += createSMTAssertion => [ | ||
293 | it.value = createSMTForall => [f| | ||
294 | var pi = 0 | ||
295 | for(param : combination) { | ||
296 | val variable = createSMTSortedVariable | ||
297 | variable.name = "p"+pi.toString | ||
298 | variable.range = EcoreUtil.copy(combination.get(pi).type) | ||
299 | f.quantifiedVariables+=variable | ||
300 | pi++ | ||
301 | } | ||
302 | val resultParam = createSMTSortedVariable => [ | ||
303 | it.name = "res" | ||
304 | it.range = EcoreUtil.copy(rangeType.type) | ||
305 | ] | ||
306 | f.quantifiedVariables += resultParam | ||
307 | f.expression = createSMTImpl => [ | ||
308 | it.leftOperand = if(useFunction) | ||
309 | { | ||
310 | createSMTEquals => [ | ||
311 | leftOperand = createSMTSymbolicValue => [ | ||
312 | it.symbolicReference = smtFunction | ||
313 | it.parameterSubstitutions += (0..<combination.size).map[x| | ||
314 | createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)] | ||
315 | ] | ||
316 | ] | ||
317 | rightOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam] | ||
318 | ] | ||
319 | } else { | ||
320 | createSMTSymbolicValue => [ | ||
321 | it.symbolicReference = smtFunction | ||
322 | it.parameterSubstitutions += (0..<combination.size).map[x| | ||
323 | createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]] | ||
324 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam] | ||
325 | ] | ||
326 | } | ||
327 | it.rightOperand = rangeType.constraint.apply(resultParam) | ||
328 | ] | ||
329 | ] | ||
330 | ] | ||
331 | } | ||
332 | return smtFunction | ||
333 | } | ||
334 | |||
335 | def transformFunctionDefinition(FunctionDefinition function, SMTInput input, Logic2SmtMapperTrace trace) { | ||
336 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
337 | } | ||
338 | |||
339 | def protected transformRelationDeclaration(RelationDeclaration relation, SMTInput input, Logic2SmtMapperTrace trace) { | ||
340 | val parameterTypeCombinations = unfolder.getPermutations(relation.parameters.map[x|transformTypeReference(x,trace)]) | ||
341 | var relationIndex = 1 | ||
342 | val unfolding = new ArrayList(parameterTypeCombinations.size) | ||
343 | for(parameterTypeCombination : parameterTypeCombinations) { | ||
344 | /// Create a name for the relation | ||
345 | val nameWithIndex = if (parameterTypeCombinations.size > 1) | ||
346 | toID('''relation «relation.name.toID» «relationIndex++»''') | ||
347 | else | ||
348 | toID('''relation «relation.name.toID»''') | ||
349 | |||
350 | // Adding an unfolded relation | ||
351 | val smtRelation = createSMTFunctionDeclaration => [ | ||
352 | name = nameWithIndex | ||
353 | parameters+= parameterTypeCombination.map[typeConstraint | EcoreUtil.copy(typeConstraint.type)] | ||
354 | range = createSMTBoolTypeReference | ||
355 | ] | ||
356 | val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[ | ||
357 | TypeDescriptor.createFromTypeReference(it.type)],relation) | ||
358 | trace.relationMap.put(descriptor,smtRelation) | ||
359 | input.functionDeclarations += smtRelation | ||
360 | unfolding += descriptor | ||
361 | |||
362 | // If there is a type constraint | ||
363 | if(parameterTypeCombination.exists[it.constraint != null]) { | ||
364 | // create a constraint that specifies that the relation contains elemenents with the required properties | ||
365 | val and = createSMTAnd | ||
366 | val rel = createSMTSymbolicValue => [it.symbolicReference = smtRelation] | ||
367 | val forall = createSMTForall => [ | ||
368 | it.expression = createSMTImpl => [ | ||
369 | it.leftOperand = rel | ||
370 | it.rightOperand = and | ||
371 | ] | ||
372 | ] | ||
373 | var paramIndex = 0 | ||
374 | for(param : parameterTypeCombination) { | ||
375 | val paramName = '''p«paramIndex++»''' | ||
376 | val variable = createSMTSortedVariable => [ | ||
377 | it.name = paramName | ||
378 | it.range = param.type | ||
379 | ] | ||
380 | forall.quantifiedVariables += variable | ||
381 | rel.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = variable] | ||
382 | if(param.constraint != null) { | ||
383 | and.operands+=param.constraint.apply(variable) | ||
384 | } | ||
385 | } | ||
386 | input.assertions += createSMTAssertion => [ | ||
387 | it.value = forall | ||
388 | ] | ||
389 | } | ||
390 | } | ||
391 | trace.relationUnfolding.put(relation,unfolding) | ||
392 | } | ||
393 | def protected transformRelationDefinition(RelationDefinition relation, SMTInput input, Logic2SmtMapperTrace trace) { | ||
394 | val parameterTypeCombinations = unfolder.getPermutations(relation.variables.map[x|transformTypeReference(x.range,trace)]).toList | ||
395 | var relationIndex = 1 | ||
396 | val unfolding = new ArrayList(parameterTypeCombinations.size) | ||
397 | for(parameterTypeCombination : parameterTypeCombinations) { | ||
398 | /// Create a name for the relation | ||
399 | val nameWithIndex = if (parameterTypeCombinations.size > 1) | ||
400 | toID('''relation «relation.name.toID» «relationIndex++»''') | ||
401 | else | ||
402 | toID('''relation «relation.name.toID»''') | ||
403 | |||
404 | // creating an unfolded relation | ||
405 | val smtRelation = createSMTFunctionDefinition => [ | ||
406 | name = nameWithIndex | ||
407 | range = createSMTBoolTypeReference | ||
408 | ] | ||
409 | /* | ||
410 | // adding variables as parameters | ||
411 | val Map<Variable, SMTSortedVariable> variables = new HashMap | ||
412 | var paramIndex = 0 | ||
413 | val constraintList = new LinkedList | ||
414 | for(param : parameterTypeCombination) { | ||
415 | val paramName = relation.variables.get(paramIndex).name.toID | ||
416 | val variable = createSMTSortedVariable => [ | ||
417 | it.name = paramName | ||
418 | it.range = param.type | ||
419 | ] | ||
420 | |||
421 | smtRelation.parameters+=variable | ||
422 | variables.put(relation.variables.get(paramIndex),variable) | ||
423 | if(param.constraint != null) { | ||
424 | constraintList+=param.constraint.apply(variable) | ||
425 | } | ||
426 | paramIndex++ | ||
427 | } | ||
428 | val definition = transformTerm(relation.value,trace,variables) | ||
429 | if(constraintList.empty) { | ||
430 | smtRelation.value = definition.expectLogic.value | ||
431 | } else if(constraintList.size == 1) { | ||
432 | smtRelation.value = createSMTAnd => [ | ||
433 | it.operands += constraintList.head | ||
434 | it.operands += definition.expectLogic.value | ||
435 | ] | ||
436 | } else { | ||
437 | smtRelation.value = createSMTAnd => [ | ||
438 | it.operands += createSMTAnd => [operands += constraintList] | ||
439 | it.operands += definition.expectLogic.value | ||
440 | ] | ||
441 | } | ||
442 | */ | ||
443 | // | ||
444 | val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[ | ||
445 | TypeDescriptor.createFromTypeReference(it.type)],relation) | ||
446 | trace.relationMap.put(descriptor,smtRelation) | ||
447 | input.functionDefinition += smtRelation | ||
448 | unfolding += descriptor | ||
449 | } | ||
450 | trace.relationUnfolding.put(relation,unfolding) | ||
451 | } | ||
452 | def transformRelationDefinition_definition(RelationDefinition relation, SMTInput input, Logic2SmtMapperTrace trace) { | ||
453 | val parameterTypeCombinations = unfolder.getPermutations(relation.variables.map[x|transformTypeReference(x.range,trace)]).toList | ||
454 | for(parameterTypeCombination : parameterTypeCombinations) { | ||
455 | val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[ | ||
456 | TypeDescriptor.createFromTypeReference(it.type)],relation) | ||
457 | val smtRelation = descriptor.lookup(trace.relationMap) as SMTFunctionDefinition | ||
458 | |||
459 | // adding variables as parameters | ||
460 | val Map<Variable, SMTSortedVariable> variables = new HashMap | ||
461 | var paramIndex = 0 | ||
462 | val constraintList = new LinkedList | ||
463 | for(param : parameterTypeCombination) { | ||
464 | val paramName = relation.variables.get(paramIndex).name.toID | ||
465 | val variable = createSMTSortedVariable => [ | ||
466 | it.name = paramName | ||
467 | it.range = param.type | ||
468 | ] | ||
469 | |||
470 | smtRelation.parameters+=variable | ||
471 | variables.put(relation.variables.get(paramIndex),variable) | ||
472 | if(param.constraint != null) { | ||
473 | constraintList+=param.constraint.apply(variable) | ||
474 | } | ||
475 | paramIndex++ | ||
476 | } | ||
477 | val definition = transformTerm(relation.value,trace,variables) | ||
478 | if(constraintList.empty) { | ||
479 | smtRelation.value = definition.expectLogic.value | ||
480 | } else if(constraintList.size == 1) { | ||
481 | smtRelation.value = createSMTAnd => [ | ||
482 | it.operands += constraintList.head | ||
483 | it.operands += definition.expectLogic.value | ||
484 | ] | ||
485 | } else { | ||
486 | smtRelation.value = createSMTAnd => [ | ||
487 | it.operands += createSMTAnd => [operands += constraintList] | ||
488 | it.operands += definition.expectLogic.value | ||
489 | ] | ||
490 | } | ||
491 | } | ||
492 | } | ||
493 | |||
494 | def transformConstantDeclaration(ConstantDeclaration constant,SMTInput input, Logic2SmtMapperTrace trace) { | ||
495 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
496 | } | ||
497 | |||
498 | def transformConstantDefinition(ConstantDefinition constant, SMTInput input, Logic2SmtMapperTrace trace) { | ||
499 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
500 | } | ||
501 | |||
502 | |||
503 | def protected SMTAssertion transformAssertion(Assertion assertion, Logic2SmtMapperTrace trace) { | ||
504 | val a = assertion.value.transformTerm(trace,emptyMap) | ||
505 | createSMTAssertion => [value = a.expectLogic.value] | ||
506 | } | ||
507 | |||
508 | /////////////////////////////////////////////////////// | ||
509 | // Logic -> Logic value transformation | ||
510 | /////////////////////////////////////////////////////// | ||
511 | |||
512 | /////////////////////////////////////////////////////// | ||
513 | // Literals | ||
514 | /////////////////////////////////////////////////////// | ||
515 | def dispatch protected TransformedSubterm transformTerm(BoolLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
516 | new LogicSubterm(createSMTBoolLiteral => [value = literal.value]) } | ||
517 | def dispatch protected TransformedSubterm transformTerm(IntLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
518 | if(literal.value>=0) { new NumericSubterm(#[],#[],createSMTIntLiteral => [value = literal.value])} | ||
519 | else {new NumericSubterm(#[],#[],createSMTMinus => [ leftOperand = (createSMTIntLiteral => [value = - (literal.value) ] ) ]) } } | ||
520 | def dispatch protected TransformedSubterm transformTerm(RealLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
521 | new NumericSubterm(#[],#[],createSMTRealLiteral => [value = literal.value]) } | ||
522 | |||
523 | /////////////////////////////////////////////////////// | ||
524 | // NumericOperators | ||
525 | /////////////////////////////////////////////////////// | ||
526 | def dispatch protected TransformedSubterm transformTerm(Plus plus, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
527 | return transformBinaryNumericOperator( | ||
528 | plus.leftOperand,plus.rightOperand, | ||
529 | [l,r|createSMTPlus => [ leftOperand = l rightOperand = r ]], | ||
530 | trace,variables) | ||
531 | } | ||
532 | def dispatch protected TransformedSubterm transformTerm(Minus minus, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
533 | return transformBinaryNumericOperator( | ||
534 | minus.leftOperand,minus.rightOperand, | ||
535 | [l,r|createSMTMinus => [ leftOperand = l rightOperand = r ]], | ||
536 | trace,variables) | ||
537 | } | ||
538 | def dispatch protected TransformedSubterm transformTerm(Multiply multiply, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
539 | return transformBinaryNumericOperator( | ||
540 | multiply.leftOperand,multiply.rightOperand, | ||
541 | [l,r|createSMTMultiply => [ leftOperand = l rightOperand = r ]], | ||
542 | trace,variables) | ||
543 | } | ||
544 | def dispatch protected TransformedSubterm transformTerm(Divison div, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
545 | return transformBinaryNumericOperator( | ||
546 | div.leftOperand,div.rightOperand, | ||
547 | [l,r|createSMTDiv => [ leftOperand = l rightOperand = r ]], | ||
548 | trace,variables) | ||
549 | } | ||
550 | def dispatch protected TransformedSubterm transformTerm(Mod mod, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
551 | return transformBinaryNumericOperator( | ||
552 | mod.leftOperand,mod.rightOperand, | ||
553 | [l,r|createSMTMod => [ leftOperand = l rightOperand = r ]], | ||
554 | trace,variables) | ||
555 | } | ||
556 | |||
557 | def protected TransformedSubterm transformBinaryNumericOperator( | ||
558 | Term leftOperand, | ||
559 | Term rightOperand, | ||
560 | Function2<SMTTerm,SMTTerm,SMTTerm> combinator, | ||
561 | Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) | ||
562 | { | ||
563 | val left = leftOperand. transformTerm(trace,variables).expectNumber.getPossibleValues | ||
564 | val right = rightOperand.transformTerm(trace,variables).expectNumber.getPossibleValues | ||
565 | val values = new ArrayList(left.size * right.size) | ||
566 | for(combination : TransformedSubterm.allCombinations(left,right)) { | ||
567 | val l = combination.get(0) | ||
568 | val r = combination.get(1) | ||
569 | values += new SubtermOption( | ||
570 | #[l,r],#[],#[], | ||
571 | combinator.apply(l.expression, r.expression), | ||
572 | TypeDescriptor.numericTypeDescriptor_Instance | ||
573 | ) | ||
574 | } | ||
575 | return new NumericSubterm(values) | ||
576 | } | ||
577 | |||
578 | /////////////////////////////////////////////////////// | ||
579 | // LogicOperators | ||
580 | /////////////////////////////////////////////////////// | ||
581 | def dispatch protected TransformedSubterm transformTerm(Not not, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
582 | val operand = not.operand.transformTerm(trace,variables).expectLogic | ||
583 | new LogicSubterm(createSMTNot => [operand = operand.value]) } | ||
584 | def dispatch protected TransformedSubterm transformTerm(And and, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
585 | transformBinaryLogicOperator2(and.operands,[x|createSMTAnd => [operands += x]],trace,variables) } | ||
586 | def dispatch protected TransformedSubterm transformTerm(Or or, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
587 | transformBinaryLogicOperator2(or.operands,[x|createSMTOr => [operands += x]],trace,variables) } | ||
588 | def dispatch protected TransformedSubterm transformTerm(Impl impl, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
589 | transformBinaryLogicOperator1(impl.leftOperand,impl.rightOperand,[l,r|createSMTImpl =>[leftOperand = l rightOperand = r]],trace,variables) } | ||
590 | def dispatch protected TransformedSubterm transformTerm(Iff iff, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
591 | transformBinaryLogicOperator1(iff.leftOperand,iff.rightOperand,[l,r|createSMTIff => [leftOperand = l rightOperand = r]],trace,variables)} | ||
592 | |||
593 | /** | ||
594 | * Logic combinator with two values | ||
595 | */ | ||
596 | def protected transformBinaryLogicOperator1( | ||
597 | Term leftOperand, Term rightOperand, | ||
598 | Function2<SMTTerm,SMTTerm,SMTTerm> combinator, | ||
599 | Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
600 | val left = leftOperand.transformTerm(trace,variables).expectLogic | ||
601 | val right = rightOperand.transformTerm(trace,variables).expectLogic | ||
602 | return new LogicSubterm(combinator.apply(left.value, right.value)) | ||
603 | } | ||
604 | /** | ||
605 | * Logic combinator with multiple values | ||
606 | */ | ||
607 | def protected transformBinaryLogicOperator2( | ||
608 | Iterable<? extends Term> operands, | ||
609 | Function1<Iterable<? extends SMTTerm>,SMTTerm> combinator, | ||
610 | Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
611 | val smtOperands = operands.map[transformTerm(trace,variables).expectLogic.value] | ||
612 | return new LogicSubterm(combinator.apply(smtOperands)) | ||
613 | } | ||
614 | |||
615 | /////////////////////////////////////////////////////// | ||
616 | // Numeric -> Logic | ||
617 | /////////////////////////////////////////////////////// | ||
618 | def dispatch protected TransformedSubterm transformTerm(MoreThan moreThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
619 | transformNumericComparison(moreThan.leftOperand,moreThan.rightOperand, [l,r|createSMTMT => [ leftOperand = l rightOperand = r ]],trace,variables)} | ||
620 | def dispatch protected TransformedSubterm transformTerm(LessThan lessThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
621 | transformNumericComparison(lessThan.leftOperand,lessThan.rightOperand, [l,r|createSMTLT => [ leftOperand = l rightOperand = r ]],trace,variables)} | ||
622 | def dispatch protected TransformedSubterm transformTerm(MoreOrEqualThan moreThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
623 | transformNumericComparison(moreThan.leftOperand,moreThan.rightOperand, [l,r|createSMTMEQ => [ leftOperand = l rightOperand = r ]],trace,variables)} | ||
624 | def dispatch protected TransformedSubterm transformTerm(LessOrEqualThan lessThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
625 | transformNumericComparison(lessThan.leftOperand,lessThan.rightOperand, [l,r|createSMTLEQ => [ leftOperand = l rightOperand = r ]],trace,variables)} | ||
626 | |||
627 | def protected transformNumericComparison(Term leftOperand, Term rightOperand, Function2<SMTTerm,SMTTerm,SMTTerm> combinator, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables){ | ||
628 | val left = leftOperand.transformTerm(trace,variables).getPossibleValues | ||
629 | val right = rightOperand.transformTerm(trace,variables).getPossibleValues | ||
630 | val values = new ArrayList(left.size * right.size) | ||
631 | for(combination : TransformedSubterm.allCombinations(left,right)) { | ||
632 | val l = combination.get(0) | ||
633 | val r = combination.get(1) | ||
634 | values += LogicSubterm::resolveToLogic(#[l,r],combinator.apply(l.expression, r.expression)) | ||
635 | } | ||
636 | val res = createSMTOr =>[operands += values] | ||
637 | return new LogicSubterm(res) | ||
638 | } | ||
639 | |||
640 | /////////////////////////////////////////////////////// | ||
641 | // Equals and Distinct | ||
642 | /////////////////////////////////////////////////////// | ||
643 | |||
644 | def dispatch protected TransformedSubterm transformTerm(Equals equals, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
645 | val left = equals.leftOperand.transformTerm(trace,variables) | ||
646 | val rightX = equals.rightOperand.transformTerm(trace,variables) | ||
647 | if(left instanceof LogicSubterm) { | ||
648 | val right = rightX.expectLogic | ||
649 | new LogicSubterm(createSMTEquals => [ | ||
650 | leftOperand = left.value | ||
651 | rightOperand = right.value ]) | ||
652 | } else if(left instanceof NumericSubterm) { | ||
653 | val right = rightX.expectNumber | ||
654 | val leftOperands = left.possibleValues | ||
655 | val rightOperands = right.possibleValues | ||
656 | val values = new ArrayList(leftOperands.size * rightOperands.size) | ||
657 | for(combination : TransformedSubterm.allCombinations(left.possibleValues,right.possibleValues)) { | ||
658 | val l = combination.get(0) | ||
659 | val r = combination.get(1) | ||
660 | values += TransformedSubterm.resolveToLogic(#[l,r], | ||
661 | createSMTEquals => [ | ||
662 | leftOperand = combination.get(0).expression | ||
663 | rightOperand = combination.get(1).expression]) | ||
664 | } | ||
665 | return new LogicSubterm(createSMTOr =>[operands += values]) | ||
666 | } else if(left instanceof ComplexSubterm){ | ||
667 | val right = rightX as ComplexSubterm | ||
668 | |||
669 | val values = new LinkedList | ||
670 | for(combination : TransformedSubterm.allCombinations(left.possibleValues,right.possibleValues)) { | ||
671 | val l = combination.get(0) | ||
672 | val r = combination.get(1) | ||
673 | if(l.type.complexType == r.type.complexType) { | ||
674 | values += TransformedSubterm.resolveToLogic(#[l,r],createSMTEquals => [ | ||
675 | leftOperand = l.expression | ||
676 | rightOperand = r.expression ]) | ||
677 | } /*else dont add*/ | ||
678 | } | ||
679 | |||
680 | if(values.size == 0) { | ||
681 | return new LogicSubterm(createSMTBoolLiteral => [it.value = false]) | ||
682 | } else if(values.size == 1) { | ||
683 | return new LogicSubterm(values.head) | ||
684 | } else { | ||
685 | return new LogicSubterm(createSMTOr => [operands += values]) | ||
686 | } | ||
687 | } | ||
688 | } | ||
689 | |||
690 | def dispatch protected TransformedSubterm transformTerm(Distinct distinct, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
691 | val o = distinct.operands.map[transformTerm(trace,variables)] | ||
692 | if(o.empty) { | ||
693 | throw new IllegalArgumentException('''empty distinct''') | ||
694 | } else if(o.size == 1) { | ||
695 | // 1 element is always distinct | ||
696 | new LogicSubterm(createSMTBoolLiteral => [it.value = true]) | ||
697 | } else { | ||
698 | val head = o.head | ||
699 | if(head instanceof LogicSubterm) { | ||
700 | return new LogicSubterm(createSMTDistinct => [ | ||
701 | it.operands += o.map[expectLogic.value]]) | ||
702 | } else if(head instanceof NumericSubterm) { | ||
703 | val numbers = o.map[expectNumber.possibleValues] | ||
704 | val distincts = new LinkedList | ||
705 | for(combination : TransformedSubterm.allCombinations(numbers)) { | ||
706 | distincts += LogicSubterm::resolveToLogic(combination,createSMTDistinct => [operands += combination.map[it.expression]]) | ||
707 | } | ||
708 | new LogicSubterm(createSMTOr => [it.operands += distincts]) | ||
709 | } else { | ||
710 | val objects = o.map[possibleValues] | ||
711 | val distincts = new LinkedList | ||
712 | for(combination : TransformedSubterm.allCombinations(objects)) { | ||
713 | val Map<SMTType,LinkedList<SubtermOption>> type2Terms = new LinkedHashMap; | ||
714 | for(param:combination) { | ||
715 | val type = param.type.complexType | ||
716 | val value = param | ||
717 | var LinkedList<SubtermOption> list; | ||
718 | if(type2Terms.containsKey(type)) { | ||
719 | list = type2Terms.get(type) | ||
720 | } else { | ||
721 | list = new LinkedList | ||
722 | type2Terms.put(type,list) | ||
723 | } | ||
724 | list+=value | ||
725 | } | ||
726 | |||
727 | val groups = type2Terms.values.map[elementList| | ||
728 | if(elementList.size == 1) return null | ||
729 | else return LogicSubterm.resolveToLogic(elementList,createSMTDistinct => [it.operands += elementList.map[expression]]) | ||
730 | ].filterNull | ||
731 | if(groups.empty) { | ||
732 | // One of the group is trivially satisfied | ||
733 | return new LogicSubterm(createSMTBoolLiteral => [it.value = true]) | ||
734 | } else { | ||
735 | val and = createSMTAnd => [operands += groups] | ||
736 | distincts.add(and) | ||
737 | } | ||
738 | } | ||
739 | if(distincts.size == 1) { | ||
740 | return new LogicSubterm(distincts.head) | ||
741 | } else { | ||
742 | return new LogicSubterm(createSMTOr => [it.operands += distincts]) | ||
743 | } | ||
744 | } | ||
745 | } | ||
746 | } | ||
747 | |||
748 | /////////////////////////////////////////////////////// | ||
749 | // Quantifiers | ||
750 | /////////////////////////////////////////////////////// | ||
751 | |||
752 | def dispatch protected TransformedSubterm transformTerm(Forall forall, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
753 | new LogicSubterm(transformQuantifiedExpression(forall,trace,variables, | ||
754 | [createSMTForall], | ||
755 | [q|createSMTAnd=>[operands+=q]], | ||
756 | [precondition,expression|createSMTImpl=>[leftOperand=precondition rightOperand=expression]])) | ||
757 | } | ||
758 | def dispatch protected TransformedSubterm transformTerm(Exists exists, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
759 | new LogicSubterm(transformQuantifiedExpression(exists,trace,variables, | ||
760 | [createSMTExists], | ||
761 | [q|createSMTOr=>[operands+=q]], | ||
762 | [precondition,expression|createSMTAnd=>[operands+=precondition operands+=expression]])) | ||
763 | } | ||
764 | |||
765 | def protected SMTTerm transformQuantifiedExpression( | ||
766 | QuantifiedExpression q, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables, | ||
767 | Function0<SMTQuantifiedExpression> constructor, | ||
768 | Function1<Iterable<SMTQuantifiedExpression>,SMTTerm> combinator, | ||
769 | Function2<SMTTerm,SMTTerm,SMTTerm> preconditionCombinator | ||
770 | ) { | ||
771 | val permutations = unfolder.getPermutations(q.quantifiedVariables.map[it.range.transformTypeReference(trace)]) | ||
772 | val ArrayList<SMTQuantifiedExpression> unfoldedQuantification = new ArrayList(permutations.size) | ||
773 | |||
774 | for(permutation : permutations) { | ||
775 | val allVariables = new HashMap(variables) | ||
776 | val newSMTVariables = new ArrayList(q.quantifiedVariables.size) | ||
777 | val typePrecondition = new ArrayList<SMTTerm>(q.quantifiedVariables.size) | ||
778 | |||
779 | for(variableIndex: 0..<q.quantifiedVariables.size) { | ||
780 | val logicVariable = q.quantifiedVariables.get(variableIndex) | ||
781 | val elementInPermutation = permutation.get(variableIndex) | ||
782 | |||
783 | val newSMTVariable = createSMTSortedVariable => [ | ||
784 | name = logicVariable.name.toID | ||
785 | range = elementInPermutation.type | ||
786 | ] | ||
787 | allVariables.put(logicVariable, newSMTVariable) | ||
788 | newSMTVariables+=newSMTVariable | ||
789 | if(elementInPermutation.constraint != null) { | ||
790 | typePrecondition += elementInPermutation.constraint.apply(newSMTVariable) | ||
791 | } | ||
792 | } | ||
793 | |||
794 | val expressionOfQuantifiedFormula = | ||
795 | if(typePrecondition.isEmpty) | ||
796 | q.expression.transformTerm(trace,allVariables).expectLogic.value | ||
797 | else if(typePrecondition.size == 1) | ||
798 | preconditionCombinator.apply( | ||
799 | typePrecondition.head, | ||
800 | q.expression.transformTerm(trace,allVariables).expectLogic.value) | ||
801 | else | ||
802 | preconditionCombinator.apply( | ||
803 | createSMTAnd => [it.operands += typePrecondition], | ||
804 | q.expression.transformTerm(trace,allVariables).expectLogic.value) | ||
805 | |||
806 | unfoldedQuantification += constructor.apply => [ | ||
807 | quantifiedVariables += newSMTVariables | ||
808 | expression = expressionOfQuantifiedFormula | ||
809 | ] | ||
810 | |||
811 | // if(newSMTVariables.exists[it.range == null]) { | ||
812 | // println(newSMTVariables.filter[it.range == null].map[name]) | ||
813 | // } | ||
814 | } | ||
815 | |||
816 | if(permutations.size == 1) return unfoldedQuantification.head | ||
817 | else return combinator.apply(unfoldedQuantification) | ||
818 | } | ||
819 | |||
820 | /////////////////////////////////////////////////////// | ||
821 | // If - Then - Else | ||
822 | /////////////////////////////////////////////////////// | ||
823 | def dispatch protected TransformedSubterm transformTerm(IfThenElse ite, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
824 | val condition = ite.condition.transformTerm(trace,variables).expectLogic.value | ||
825 | val positiveTerm = ite.ifTrue.transformTerm(trace,variables) | ||
826 | val positives = positiveTerm.possibleValues | ||
827 | val negativeTerm = ite.ifFalse.transformTerm(trace,variables) | ||
828 | val negatives = negativeTerm.possibleValues | ||
829 | // Simple ITE | ||
830 | if(positives.size == 1 && negatives.size == 1 && positives.head.type == negatives.head.type) { | ||
831 | val t = positives.head.type | ||
832 | if(t.isLogic) { | ||
833 | return new LogicSubterm(createSMTITE => [ | ||
834 | it.condition = condition | ||
835 | it.^if = positives.head.expression | ||
836 | it.^else = negatives.head.expression]) | ||
837 | } else if(t.isNumeric) { | ||
838 | return new NumericSubterm( | ||
839 | (positives.head.variables + negatives.head.variables).toList, | ||
840 | (positives.head.preconditions + negatives.head.preconditions).toList, | ||
841 | createSMTITE => [ | ||
842 | it.condition = condition | ||
843 | it.^if = positives.head.expression | ||
844 | it.^else = negatives.head.expression | ||
845 | ]) | ||
846 | } else { | ||
847 | return new ComplexSubterm( | ||
848 | (positives.head.variables + negatives.head.variables).toList, | ||
849 | (positives.head.preconditions + negatives.head.preconditions).toList, | ||
850 | createSMTITE => [ | ||
851 | it.condition = condition | ||
852 | it.^if = positives.head.expression | ||
853 | it.^else = negatives.head.expression], | ||
854 | t | ||
855 | ) | ||
856 | } | ||
857 | // else the ite need to be unfolded | ||
858 | } else { | ||
859 | if(positiveTerm instanceof LogicSubterm) { | ||
860 | throw new AssertionError('''If the subterm has logic value it should be transformed as "Simple ITE""''') | ||
861 | } else if (positiveTerm instanceof NumericSubterm){ | ||
862 | return new NumericSubterm(unfoldIte(positives, condition, negatives)) | ||
863 | } else { | ||
864 | return new ComplexSubterm(unfoldIte(positives, condition, negatives)) | ||
865 | } | ||
866 | } | ||
867 | } | ||
868 | |||
869 | private def List<SubtermOption> unfoldIte(List<SubtermOption> positives, SMTTerm condition, List<SubtermOption> negatives) { | ||
870 | (positives.map[ | ||
871 | new SubtermOption(#[it],#[],#[condition],it.expression,it.type) | ||
872 | ] + | ||
873 | negatives.map[ | ||
874 | new SubtermOption(#[it],#[],#[createSMTNot => [it.operand = condition]],it.expression,it.type) | ||
875 | ]).toList | ||
876 | } | ||
877 | |||
878 | /////////////////////////////////////////////////////// | ||
879 | // instanceof | ||
880 | /////////////////////////////////////////////////////// | ||
881 | |||
882 | def dispatch protected TransformedSubterm transformTerm(InstanceOf i, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
883 | val value = i.value.transformTerm(trace,variables) | ||
884 | val range = i.range | ||
885 | if(range instanceof BoolTypeReference) { | ||
886 | return new LogicSubterm(createSMTBoolLiteral=>[it.value = (value instanceof LogicSubterm)]) | ||
887 | } else if(range instanceof IntTypeReference || range instanceof RealTypeReference) { | ||
888 | return new LogicSubterm(createSMTBoolLiteral=>[it.value = (value instanceof NumericSubterm)]) | ||
889 | } else { | ||
890 | val requestedTypes = this.typeMapper.transformTypeReference((range as ComplexTypeReference).referred,trace) | ||
891 | val possileValues = value.possibleValues | ||
892 | val options = new ArrayList(requestedTypes.size) | ||
893 | for(typeConstraint : requestedTypes) { | ||
894 | val possibleValue = possileValues.filter[it.type.complexType == (typeConstraint.type as SMTComplexTypeReference).referred].head | ||
895 | if(possibleValue != null) { | ||
896 | val x = if(typeConstraint.constraint != null ) { | ||
897 | if(possibleValue.expression instanceof SMTSymbolicValue && (possibleValue.expression as SMTSymbolicValue).symbolicReference instanceof SMTSortedVariable) { | ||
898 | val referred = (possibleValue.expression as SMTSymbolicValue).symbolicReference as SMTSortedVariable | ||
899 | typeConstraint.constraint.apply(referred) | ||
900 | } else { | ||
901 | createSMTForall => [ | ||
902 | val v = createSMTSortedVariable => [it.range = EcoreUtil.copy(typeConstraint.type)] | ||
903 | it.quantifiedVariables += v | ||
904 | it.expression = createSMTImpl => [ | ||
905 | leftOperand = createSMTEquals => [ | ||
906 | it.leftOperand = possibleValue.expression | ||
907 | it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = v] | ||
908 | ] | ||
909 | rightOperand = typeConstraint.constraint.apply(v) | ||
910 | ] | ||
911 | ] | ||
912 | } | ||
913 | } else if(typeConstraint.constraint == null) { | ||
914 | createSMTBoolLiteral => [it.value = true] | ||
915 | } | ||
916 | options += LogicSubterm::resolveToLogic(#[possibleValue],x) | ||
917 | } | ||
918 | } | ||
919 | |||
920 | if(options.size == 0) { | ||
921 | return new LogicSubterm(createSMTBoolLiteral=>[it.value = false]) | ||
922 | } else if(options.size == 1) { | ||
923 | return new LogicSubterm(options.head) | ||
924 | } else { | ||
925 | return new LogicSubterm(createSMTOr => [it.operands += options]) | ||
926 | } | ||
927 | } | ||
928 | |||
929 | } | ||
930 | |||
931 | /////////////////////////////////////////////////////// | ||
932 | // SymbolicReference | ||
933 | /////////////////////////////////////////////////////// | ||
934 | |||
935 | def dispatch protected TransformedSubterm transformTerm(SymbolicValue symbolicValue, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
936 | val referred = symbolicValue.symbolicReference | ||
937 | val params = symbolicValue.parameterSubstitutions | ||
938 | return transformSymbolicReference(referred,params,trace,variables) | ||
939 | } | ||
940 | |||
941 | def dispatch protected TransformedSubterm transformSymbolicReference(Relation referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
942 | val parameters = parameterSubstitution.map[transformTerm(it,trace,variables)] | ||
943 | val list = new LinkedList | ||
944 | for(combination : TransformedSubterm.allCombinations(parameters.map[it.possibleValues])) { | ||
945 | val descriptor = new Descriptor(combination.map[it.type],referred) | ||
946 | val targetRelation = descriptor.lookup(trace.relationMap) | ||
947 | if(targetRelation == null) { | ||
948 | throw new AssertionError('''target relation should not be null (yet)''') | ||
949 | |||
950 | } else { | ||
951 | list += TransformedSubterm.resolveToLogic(combination,createSMTSymbolicValue => [ | ||
952 | it.symbolicReference = targetRelation | ||
953 | it.parameterSubstitutions += combination.map[it.expression] | ||
954 | ]) | ||
955 | } | ||
956 | } | ||
957 | |||
958 | if(list.size == 1) { | ||
959 | return new LogicSubterm(list.head) | ||
960 | } else { | ||
961 | return new LogicSubterm(createSMTOr => [ operands += list ]) | ||
962 | } | ||
963 | } | ||
964 | |||
965 | |||
966 | def dispatch protected TransformedSubterm transformSymbolicReference(Function referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
967 | throw new UnsupportedOperationException | ||
968 | } | ||
969 | |||
970 | def dispatch protected TransformedSubterm transformSymbolicReference(Variable referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
971 | if(!variables.containsKey(referred)) { | ||
972 | val container = referred.eContainer | ||
973 | println("X" + container) | ||
974 | for(v : variables.keySet) { | ||
975 | println(v) | ||
976 | println("in " +v.eContainer) | ||
977 | } | ||
978 | return null | ||
979 | } | ||
980 | val v = referred.lookup(variables) | ||
981 | |||
982 | val expression = createSMTSymbolicValue => [it.symbolicReference = v] | ||
983 | if(v.range instanceof SMTBoolTypeReference) { | ||
984 | return new LogicSubterm(expression) | ||
985 | } else if(v.range instanceof SMTIntTypeReference || v.range instanceof SMTRealTypeReference) { | ||
986 | return new NumericSubterm(#[],#[],expression) | ||
987 | } else { | ||
988 | return new ComplexSubterm(#[],#[],expression, | ||
989 | new TypeDescriptor((v.range as SMTComplexTypeReference).referred)); | ||
990 | } | ||
991 | } | ||
992 | |||
993 | def dispatch protected TransformedSubterm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
994 | this.typeMapper.transformSymbolicReference(referred,trace) | ||
995 | } | ||
996 | |||
997 | def dispatch protected TransformedSubterm transformSymbolicReference(Void referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
998 | throw new NullPointerException('''unfilled symbolic reference!''') | ||
999 | } | ||
1000 | |||
1001 | /////////// | ||
1002 | |||
1003 | /*def transformContainment(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) { | ||
1004 | val containmentRelation_oo = createSMTFunctionDefinition=>[ | ||
1005 | it.name="containment!oo" | ||
1006 | it.range=createSMTBoolTypeReference | ||
1007 | val child = createSMTSortedVariable => [ | ||
1008 | it.name = | ||
1009 | ] | ||
1010 | ] | ||
1011 | }*/ | ||
1012 | |||
1013 | /////////// | ||
1014 | |||
1015 | def cleanDocument(SMTDocument document) { | ||
1016 | val content = document.eAllContents.toList | ||
1017 | for(object:content) { | ||
1018 | for(containmentReference : object.eClass.EAllReferences.filter[containment]) { | ||
1019 | val child = object.eGet(containmentReference) { | ||
1020 | if(child!=null) { | ||
1021 | if(containmentReference.isMany) { | ||
1022 | val list = child as List<EObject> | ||
1023 | for(index : 0..<list.size) { | ||
1024 | val single = list.get(index) | ||
1025 | val newSingle = replaceWith(single) | ||
1026 | if(newSingle!=null) { | ||
1027 | list.set(index,newSingle) | ||
1028 | } | ||
1029 | } | ||
1030 | } else { | ||
1031 | val single = child as EObject | ||
1032 | val newSingle = replaceWith(single) | ||
1033 | if(newSingle!=null) { | ||
1034 | object.eSet(containmentReference,newSingle) | ||
1035 | } | ||
1036 | } | ||
1037 | } | ||
1038 | } | ||
1039 | } | ||
1040 | } | ||
1041 | } | ||
1042 | def private dispatch replaceWith(SMTOr or) { | ||
1043 | if(or.operands.empty) { | ||
1044 | return createSMTBoolLiteral => [it.value = false] | ||
1045 | } else return null | ||
1046 | } | ||
1047 | def private dispatch replaceWith(SMTAnd and) { | ||
1048 | if(and.operands.empty) { | ||
1049 | return createSMTBoolLiteral => [it.value = true] | ||
1050 | } else return null | ||
1051 | } | ||
1052 | def private dispatch replaceWith(EObject object) { | ||
1053 | null | ||
1054 | } | ||
1055 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapperTrace.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapperTrace.xtend new file mode 100644 index 00000000..69111a11 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapperTrace.xtend | |||
@@ -0,0 +1,23 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
7 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration | ||
8 | import java.util.HashMap | ||
9 | import java.util.List | ||
10 | import java.util.Map | ||
11 | |||
12 | class Logic2SmtMapperTrace { | ||
13 | public var LogicProblem problem | ||
14 | public var Logic2SmtMapper forwardMapper | ||
15 | public var Logic2Smt_TypeMapperTrace typeMapperTrace | ||
16 | |||
17 | public val Map<Relation,List<Descriptor<Relation>>> relationUnfolding = new HashMap | ||
18 | public val Map<Descriptor<Relation>,SMTSymbolicDeclaration> relationMap = new HashMap | ||
19 | public val Map<Function,List<Descriptor<Function>>> functionUnfolding = new HashMap | ||
20 | public val Map<Descriptor<Function>,SMTSymbolicDeclaration> functionMap = new HashMap | ||
21 | public val Map<Function,List<Descriptor<Constant>>> constantUnfolding = new HashMap | ||
22 | public val Map<Descriptor<Constant>,SMTSymbolicDeclaration> constantMap = new HashMap | ||
23 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper_UnfoldingSupport.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper_UnfoldingSupport.xtend new file mode 100644 index 00000000..8c2d5dad --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper_UnfoldingSupport.xtend | |||
@@ -0,0 +1,33 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | //import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | ||
4 | import java.util.ArrayList | ||
5 | import java.util.List | ||
6 | |||
7 | class Logic2SmtMapper_UnfoldingSupport { | ||
8 | //val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE | ||
9 | |||
10 | def List<List<TypeConstraint>> getPermutations(List<List<TypeConstraint>> lists) { | ||
11 | if(lists.size == 1) { | ||
12 | val elements = lists.head | ||
13 | val result = new ArrayList(elements.size) | ||
14 | for(element: elements){ | ||
15 | result.add(#[element.copy]) | ||
16 | } | ||
17 | return result | ||
18 | } else { | ||
19 | val permuteThis = lists.head | ||
20 | val withThat = getPermutations(lists.tail.toList) | ||
21 | val result = new ArrayList(permuteThis.size*withThat.size) | ||
22 | for(h:permuteThis) { | ||
23 | for(t:withThat) { | ||
24 | val l = new ArrayList(withThat.size+1) | ||
25 | l+=h.copy | ||
26 | l.addAll(t.map[copy]) | ||
27 | result.add(l) | ||
28 | } | ||
29 | } | ||
30 | return result | ||
31 | } | ||
32 | } | ||
33 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend new file mode 100644 index 00000000..71cfd0e0 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend | |||
@@ -0,0 +1,38 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
7 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
8 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
9 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable | ||
10 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm | ||
11 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTypeReference | ||
12 | import java.util.List | ||
13 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
14 | import org.eclipse.xtend.lib.annotations.Data | ||
15 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
16 | |||
17 | interface Logic2Smt_TypeMapper { | ||
18 | def void transformTypes( | ||
19 | SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) | ||
20 | |||
21 | def List<TypeConstraint> transformTypeReference(Type type, Logic2SmtMapperTrace trace) | ||
22 | def TransformedSubterm transformSymbolicReference(DefinedElement referred, Logic2SmtMapperTrace trace) | ||
23 | def Logic2SMT_TypeMapperInterpretation getTypeInterpretation(LogicProblem problem,SMTDocument document,SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) | ||
24 | } | ||
25 | |||
26 | @Data | ||
27 | class TypeConstraint { | ||
28 | SMTTypeReference type | ||
29 | Function1<SMTSortedVariable,SMTTerm> constraint | ||
30 | |||
31 | def public copy() { | ||
32 | return new TypeConstraint(EcoreUtil.copy(this.type),this.constraint) | ||
33 | } | ||
34 | } | ||
35 | |||
36 | interface Logic2Smt_TypeMapperTrace{ | ||
37 | def Logic2Smt_TypeMapperTrace copy(SMTInput newModel) | ||
38 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend new file mode 100644 index 00000000..c9bafa6c --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend | |||
@@ -0,0 +1,501 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher | ||
12 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference | ||
13 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
14 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral | ||
15 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration | ||
16 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration | ||
17 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition | ||
18 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
19 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult | ||
20 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSetTypeDeclaration | ||
21 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration | ||
22 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm | ||
23 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType | ||
24 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | ||
25 | import java.util.ArrayList | ||
26 | import java.util.HashMap | ||
27 | import java.util.LinkedList | ||
28 | import java.util.List | ||
29 | import java.util.Map | ||
30 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
31 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
32 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | ||
33 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
34 | |||
35 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
36 | |||
37 | class Logic2Smt_TypeMapperTrace_FilteredTypes implements Logic2Smt_TypeMapperTrace{ | ||
38 | public var Map<Type, SMTType> independentClasses = new HashMap | ||
39 | /** | ||
40 | * SMT type for the new objects | ||
41 | */ | ||
42 | public var SMTType newObjects | ||
43 | /** | ||
44 | * SMT type for the existing objects | ||
45 | */ | ||
46 | public var SMTEnumeratedTypeDeclaration oldObjects | ||
47 | /** | ||
48 | * existing element -> SMT literal map | ||
49 | */ | ||
50 | public var Map<DefinedElement, SMTEnumLiteral> elementMap = new HashMap | ||
51 | |||
52 | public var SMTEnumeratedTypeDeclaration oldObjectTypes | ||
53 | public var Map<Type, SMTEnumLiteral> oldObjectTypeMap = new HashMap | ||
54 | public var SMTFunctionDefinition oldObjectTypeFunction | ||
55 | public var Map<Type, SMTFunctionDefinition> oldObjectTypePredicates = new HashMap | ||
56 | |||
57 | public var SMTEnumeratedTypeDeclaration newObjectTypes | ||
58 | public var Map<Type, SMTEnumLiteral> newObjectTypeMap = new HashMap | ||
59 | public var SMTFunctionDeclaration newObjectTypeFunction | ||
60 | public var Map<Type, SMTFunctionDefinition> newObjectTypePredicates = new HashMap | ||
61 | |||
62 | override copy(SMTInput newModel) { | ||
63 | val a = this | ||
64 | val b = new Logic2Smt_TypeMapperTrace_FilteredTypes | ||
65 | |||
66 | b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name]) | ||
67 | |||
68 | b.newObjects = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head | ||
69 | b.oldObjects = newModel.typeDeclarations.filter[it.name == a.oldObjects.name].head as SMTEnumeratedTypeDeclaration | ||
70 | b.elementMap = a.elementMap.copyMap(b.oldObjects.elements,[name]) | ||
71 | |||
72 | b.oldObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head as SMTEnumeratedTypeDeclaration | ||
73 | b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name]) | ||
74 | b.oldObjectTypeFunction = newModel.functionDefinition.filter[it.name == a.oldObjectTypeFunction.name].head | ||
75 | b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) | ||
76 | |||
77 | b.newObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjectTypes.name].head as SMTEnumeratedTypeDeclaration | ||
78 | b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name]) | ||
79 | b.newObjectTypeFunction = newModel.functionDeclarations.filter[it.name == a.newObjectTypeFunction.name].head | ||
80 | b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) | ||
81 | |||
82 | return b | ||
83 | } | ||
84 | } | ||
85 | |||
86 | class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | ||
87 | val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE | ||
88 | val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE | ||
89 | |||
90 | private def toID(List<String> names) {names.join("!") } | ||
91 | private def toID(String name) {name.split("\\s+").toID} | ||
92 | |||
93 | override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { | ||
94 | val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes | ||
95 | trace.typeMapperTrace = typeTrace | ||
96 | val engine = ViatraQueryEngine.on(new EMFScope(problem)) | ||
97 | |||
98 | val independentTypes = problem.types.filter(TypeDefinition).filter[isIndependentType] | ||
99 | |||
100 | val connectedTypes = problem.types.filter[!isIndependentType] | ||
101 | val connectedElements = problem.elements.filter[!isIndependentElement] | ||
102 | |||
103 | val connectedTypesWithoutDefintypesWithoutDefinedSupertype = connectedTypes.filter(TypeDeclaration).filter[!hasDefinedSupertype].toList | ||
104 | val hasOldElements = !connectedElements.empty | ||
105 | val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty | ||
106 | |||
107 | // 0. map the simple types | ||
108 | this.transformIndependentTypes(independentTypes,trace) | ||
109 | |||
110 | // 1. Has old elements => create supertype for it | ||
111 | if(hasOldElements) { | ||
112 | this.transformDefinedElements(connectedElements, trace,document) | ||
113 | } | ||
114 | // 2. Has new types => create a supertype for it | ||
115 | if(hasNewElements) { | ||
116 | this.transformUndefinedElements(scopes,trace,document) | ||
117 | } | ||
118 | // 3. Adding type definitions of the types | ||
119 | // 3.1: Type definition to old elements | ||
120 | if(hasOldElements) { | ||
121 | this.transformOldTypes(connectedTypes, connectedElements, trace, document, engine) | ||
122 | } | ||
123 | // 3.2: Type definition to new elements | ||
124 | if(hasNewElements) { | ||
125 | this.transformNewTypes(connectedTypesWithoutDefintypesWithoutDefinedSupertype,trace,document,engine); | ||
126 | } | ||
127 | } | ||
128 | |||
129 | private def isIndependentType(Type t) { | ||
130 | val res = (t instanceof TypeDefinition) && t.supertypes.empty && t.subtypes.empty | ||
131 | return res | ||
132 | } | ||
133 | private def isIndependentElement(DefinedElement e) { | ||
134 | val types = e.definedInType | ||
135 | return types.size == 1 && types.head.isIndependentType | ||
136 | } | ||
137 | |||
138 | protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace) { | ||
139 | for(type: types) { | ||
140 | val independentSMTType = createSMTEnumeratedTypeDeclaration => [ | ||
141 | name = toID(#["oldType",type.name]) | ||
142 | ] | ||
143 | trace.typeTrace.independentClasses.put(type,independentSMTType) | ||
144 | for(element : type.elements) { | ||
145 | val enumLiteral = createSMTEnumLiteral => [it.name = toID(#["oldElement",element.name])] | ||
146 | independentSMTType.elements += enumLiteral | ||
147 | trace.typeTrace.elementMap.put(element,enumLiteral) | ||
148 | } | ||
149 | } | ||
150 | } | ||
151 | |||
152 | protected def transformDefinedElements(Iterable<DefinedElement> oldElements, Logic2SmtMapperTrace trace, SMTInput document) { | ||
153 | val List<SMTEnumLiteral> literals = new ArrayList(oldElements.size) | ||
154 | for(element : oldElements) { | ||
155 | val elementName ='''oldElement «element.name»''' | ||
156 | val literal = createSMTEnumLiteral => [name = elementName.toID] | ||
157 | literals += literal | ||
158 | trace.typeTrace.elementMap.put(element,literal) | ||
159 | } | ||
160 | trace.typeTrace.oldObjects = createSMTEnumeratedTypeDeclaration => | ||
161 | [name = "oldObjects" it.elements += literals] | ||
162 | document.typeDeclarations += trace.typeTrace.oldObjects | ||
163 | } | ||
164 | |||
165 | protected def transformUndefinedElements(TypeScopes scopes, Logic2SmtMapperTrace trace, SMTInput document) { | ||
166 | var SMTType newObjects | ||
167 | if(scopes.maxNewElements == -1) { | ||
168 | newObjects = createSMTSetTypeDeclaration => [ | ||
169 | name = "newObjects" | ||
170 | ] | ||
171 | } else { | ||
172 | val newElements = new ArrayList(scopes.maxNewElements) | ||
173 | for(index : (1..<scopes.maxNewElements+1)) { | ||
174 | val literal = createSMTEnumLiteral => [ | ||
175 | name = #["newElement",index.toString].toID | ||
176 | ] | ||
177 | newElements += literal | ||
178 | } | ||
179 | newObjects = createSMTEnumeratedTypeDeclaration => [ | ||
180 | name = "newObjects" | ||
181 | it.elements += newElements | ||
182 | ] | ||
183 | } | ||
184 | trace.typeTrace.newObjects = newObjects | ||
185 | document.typeDeclarations += newObjects | ||
186 | } | ||
187 | |||
188 | protected def transformOldTypes(Iterable<Type> oldTypes,Iterable<DefinedElement> oldElements, Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) { | ||
189 | val possibleTypeMatcher = PossibleDynamicTypeMatcher.on(engine) | ||
190 | val supertypeStarMatcher = SupertypeStarMatcher.on(engine) | ||
191 | // val possibleTypes = new LinkedList | ||
192 | // if(hasDefinedElement) possibleTypes += typesWithDefinedSupertype | ||
193 | // if(hasUndefinedElement) possibleTypes += typesWithoutDefinedSupertype | ||
194 | // val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract] | ||
195 | // val possibleConcreteTypes = possibleTypeMatcher.allValuesOfdynamic | ||
196 | |||
197 | // 3.1.1. cretate a type for old types | ||
198 | val possibleConcreteTypeLiterals = new ArrayList() | ||
199 | for(possibleConcreteType: oldTypes.filter[!isIsAbstract]) { | ||
200 | val typeName = '''oldType «possibleConcreteType.name»''' | ||
201 | val literal = createSMTEnumLiteral => [name = typeName.toID] | ||
202 | trace.typeTrace.oldObjectTypeMap.put(possibleConcreteType,literal) | ||
203 | possibleConcreteTypeLiterals+=literal | ||
204 | } | ||
205 | val oldObjectTypes = createSMTEnumeratedTypeDeclaration => [ | ||
206 | it.name = "oldTypes" | ||
207 | it.elements += possibleConcreteTypeLiterals | ||
208 | ] | ||
209 | trace.typeTrace.oldObjectTypes = oldObjectTypes | ||
210 | document.typeDeclarations += oldObjectTypes | ||
211 | |||
212 | // 3.1.2 for each object, create a constant for its possible dynamic type | ||
213 | val Map<DefinedElement,SMTFunctionDeclaration> possibleTypesOfElement = new HashMap | ||
214 | val Map<DefinedElement,Type> onlyPossibleType = new HashMap | ||
215 | for(object: oldElements) { | ||
216 | val types = possibleTypeMatcher.getAllValuesOfdynamic(null,object) | ||
217 | if(types.size == 1) { | ||
218 | onlyPossibleType.put(object,types.head) | ||
219 | } else { // including 0 or more than 1 | ||
220 | // create a constant declaration | ||
221 | val typeOfObjectConstant = createSMTFunctionDeclaration => [ | ||
222 | it.name = toID(#["typeDecisions",toID(object.name)]) | ||
223 | it.range = createSMTComplexTypeReference => [ | ||
224 | it.referred = trace.typeTrace.oldObjectTypes | ||
225 | ] | ||
226 | ] | ||
227 | document.functionDeclarations += typeOfObjectConstant | ||
228 | possibleTypesOfElement.put(object,typeOfObjectConstant) | ||
229 | // add assertions to the constant to select valid values | ||
230 | document.assertions += createSMTAssertion => [ | ||
231 | val options = types.map[type | createSMTEquals => [ | ||
232 | it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = typeOfObjectConstant] | ||
233 | it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = type.lookup(trace.typeTrace.oldObjectTypeMap)] | ||
234 | ]] | ||
235 | it.value = if(options.empty) { | ||
236 | createSMTBoolLiteral => [it.value = false] | ||
237 | } else { | ||
238 | createSMTOr=>[operands += options] | ||
239 | } | ||
240 | ] | ||
241 | } | ||
242 | } | ||
243 | |||
244 | // 3.1.2 create a function: old elements -> old types | ||
245 | val oldTypeFunction = createSMTFunctionDefinition => [ | ||
246 | it.name = "oldTypeFunction" | ||
247 | val o = createSMTSortedVariable => [ | ||
248 | it.name = "o" | ||
249 | it.range= createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects] | ||
250 | ] | ||
251 | it.parameters += o | ||
252 | it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjectTypes] | ||
253 | it.value = unfoldITE(oldElements, | ||
254 | [createSMTSymbolicValue => [it.symbolicReference = o]], | ||
255 | [DefinedElement e | createSMTSymbolicValue => [it.symbolicReference = e.lookup(trace.typeTrace.elementMap)]], | ||
256 | [DefinedElement e | | ||
257 | if(onlyPossibleType.containsKey(e)) { | ||
258 | return createSMTSymbolicValue => [ | ||
259 | symbolicReference = e.lookup(onlyPossibleType).lookup(trace.typeTrace.oldObjectTypeMap) ] | ||
260 | } else { | ||
261 | return createSMTSymbolicValue => [ | ||
262 | symbolicReference = e.lookup(possibleTypesOfElement) | ||
263 | ] | ||
264 | } | ||
265 | ] | ||
266 | ) | ||
267 | ] | ||
268 | trace.typeTrace.oldObjectTypeFunction = oldTypeFunction | ||
269 | document.functionDefinition += oldTypeFunction | ||
270 | |||
271 | // 3.1.3 create a predicate for each type: old object -> {true, false} | ||
272 | for(oldType: oldTypes) { | ||
273 | val oldTypePredicate = createSMTFunctionDefinition | ||
274 | oldTypePredicate.name = toID(#["oldTypePredicate",oldType.name.toID]) | ||
275 | val param = createSMTSortedVariable => [ | ||
276 | name = "o" | ||
277 | range = createSMTComplexTypeReference => [referred = trace.typeTrace.oldObjects] | ||
278 | ] | ||
279 | oldTypePredicate.parameters += param | ||
280 | oldTypePredicate.range = createSMTBoolTypeReference | ||
281 | val values = new LinkedList | ||
282 | for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(oldType).filter[!isIsAbstract]) { | ||
283 | val typeOfO = createSMTSymbolicValue => [ | ||
284 | it.symbolicReference = oldTypeFunction | ||
285 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param] | ||
286 | ] | ||
287 | val valueOfConcreteSupbtype = createSMTSymbolicValue => [ | ||
288 | it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.oldObjectTypeMap) | ||
289 | ] | ||
290 | values += createSMTEquals => [ | ||
291 | it.leftOperand = typeOfO | ||
292 | it.rightOperand = valueOfConcreteSupbtype | ||
293 | ] | ||
294 | } | ||
295 | oldTypePredicate.value = createSMTOr=>[it.operands +=values] | ||
296 | |||
297 | document.functionDefinition += oldTypePredicate | ||
298 | trace.typeTrace.oldObjectTypePredicates.put(oldType,oldTypePredicate) | ||
299 | } | ||
300 | } | ||
301 | |||
302 | protected def transformNewTypes( | ||
303 | Iterable<TypeDeclaration> typesWithoutDefinedSupertype, | ||
304 | Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) | ||
305 | { | ||
306 | val supertypeStarMatcher = SupertypeStarMatcher.on(engine) | ||
307 | val possibleTypes = typesWithoutDefinedSupertype | ||
308 | val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract].toList | ||
309 | |||
310 | // 3.2.1. cretate a type for new types | ||
311 | val possibleConcreteTypeLiterals = new ArrayList() | ||
312 | for(possibleConcreteType: possibleConcreteTypes) { | ||
313 | val typeName = '''newType «possibleConcreteType.name»''' | ||
314 | val literal = createSMTEnumLiteral => [name = typeName.toID] | ||
315 | trace.typeTrace.newObjectTypeMap.put(possibleConcreteType,literal) | ||
316 | possibleConcreteTypeLiterals+=literal | ||
317 | } | ||
318 | val newObjectTypes = createSMTEnumeratedTypeDeclaration => [ | ||
319 | it.name = "newTypes" | ||
320 | it.elements += possibleConcreteTypeLiterals | ||
321 | ] | ||
322 | trace.typeTrace.newObjectTypes = newObjectTypes | ||
323 | document.typeDeclarations += newObjectTypes | ||
324 | |||
325 | // 3.2.2 create a function: new elements -> new types | ||
326 | val newTypeFunction = createSMTFunctionDeclaration => [ | ||
327 | it.name = "newTypeFunction" | ||
328 | it.parameters += createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects] | ||
329 | it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjectTypes] | ||
330 | ] | ||
331 | trace.typeTrace.newObjectTypeFunction = newTypeFunction | ||
332 | document.functionDeclarations += newTypeFunction | ||
333 | |||
334 | // 3.1.3 create a predicate for each type: new type -> {true, false} | ||
335 | for(newType: possibleTypes) { | ||
336 | val newTypePredicate = createSMTFunctionDefinition | ||
337 | newTypePredicate.name = toID(#["newTypePredicate",newType.name.toID]) | ||
338 | val param = createSMTSortedVariable => [ | ||
339 | name = "o" | ||
340 | range = createSMTComplexTypeReference => [referred = trace.typeTrace.newObjects] | ||
341 | ] | ||
342 | newTypePredicate.parameters += param | ||
343 | newTypePredicate.range = createSMTBoolTypeReference | ||
344 | val values = new LinkedList | ||
345 | for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(newType).filter[!isIsAbstract]) { | ||
346 | if(possibleConcreteTypes.contains(concreteSupbtype)) { | ||
347 | val typeOfO = createSMTSymbolicValue => [ | ||
348 | it.symbolicReference = newTypeFunction | ||
349 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param] | ||
350 | ] | ||
351 | if(!trace.typeTrace.newObjectTypeMap.containsKey(concreteSupbtype)) { | ||
352 | println("gebasz") | ||
353 | } | ||
354 | val valueOfConcreteSupbtype = createSMTSymbolicValue => [ | ||
355 | it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.newObjectTypeMap) | ||
356 | ] | ||
357 | values+= createSMTEquals => [ | ||
358 | it.leftOperand = typeOfO | ||
359 | it.rightOperand = valueOfConcreteSupbtype | ||
360 | ] | ||
361 | } | ||
362 | } | ||
363 | newTypePredicate.value = createSMTOr=>[it.operands +=values] | ||
364 | |||
365 | document.functionDefinition += newTypePredicate | ||
366 | trace.typeTrace.newObjectTypePredicates.put(newType,newTypePredicate) | ||
367 | } | ||
368 | } | ||
369 | |||
370 | private def Logic2Smt_TypeMapperTrace_FilteredTypes getTypeTrace(Logic2SmtMapperTrace trace) { | ||
371 | val typeTrace = trace.typeMapperTrace | ||
372 | if(typeTrace instanceof Logic2Smt_TypeMapperTrace_FilteredTypes) { | ||
373 | return typeTrace | ||
374 | } else { | ||
375 | throw new IllegalArgumentException('''Unknown trace type: «typeTrace.class.name»''') | ||
376 | } | ||
377 | } | ||
378 | |||
379 | private def boolean hasDefinedSupertype(Type type) { | ||
380 | if(type instanceof TypeDefinition) { | ||
381 | return true | ||
382 | } else { | ||
383 | if(type.supertypes.empty) return false | ||
384 | else return type.supertypes.exists[it.hasDefinedSupertype] | ||
385 | } | ||
386 | } | ||
387 | |||
388 | def private <T> SMTTerm unfoldITE(Iterable<T> options, Function0<SMTTerm> input, Function1<T,SMTTerm> conditionOfOption, Function1<T,SMTTerm> outputForOption) { | ||
389 | if(options.size == 1) { | ||
390 | return outputForOption.apply(options.head) | ||
391 | } else { | ||
392 | return createSMTITE => [ | ||
393 | it.condition = createSMTEquals => [ | ||
394 | leftOperand = input.apply | ||
395 | rightOperand = conditionOfOption.apply(options.head) | ||
396 | ] | ||
397 | it.^if = outputForOption.apply(options.head) | ||
398 | it.^else = unfoldITE(options.tail,input,conditionOfOption,outputForOption) | ||
399 | ] | ||
400 | } | ||
401 | } | ||
402 | |||
403 | override transformSymbolicReference(DefinedElement referred,Logic2SmtMapperTrace trace) { | ||
404 | val x = referred.lookup(trace.typeTrace.elementMap) | ||
405 | new ComplexSubterm(#[],#[], | ||
406 | createSMTSymbolicValue => [it.symbolicReference = x], | ||
407 | new TypeDescriptor(x.eContainer as SMTEnumeratedTypeDeclaration) | ||
408 | ) | ||
409 | } | ||
410 | |||
411 | override transformTypeReference(Type type, Logic2SmtMapperTrace trace) { | ||
412 | val list = new ArrayList | ||
413 | |||
414 | if(trace.typeTrace.oldObjectTypePredicates.containsKey(type)) { | ||
415 | list += new TypeConstraint( | ||
416 | createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects], | ||
417 | [x|createSMTSymbolicValue => [ | ||
418 | it.symbolicReference = trace.typeTrace.oldObjectTypePredicates.get(type) | ||
419 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]] | ||
420 | ) | ||
421 | } | ||
422 | if(trace.typeTrace.newObjectTypePredicates.containsKey(type)) { | ||
423 | list += new TypeConstraint( | ||
424 | createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects], | ||
425 | [x|createSMTSymbolicValue => [ | ||
426 | it.symbolicReference = trace.typeTrace.newObjectTypePredicates.get(type) | ||
427 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]] | ||
428 | ) | ||
429 | } | ||
430 | if(trace.typeTrace.independentClasses.containsKey(type)) { | ||
431 | list += new TypeConstraint( | ||
432 | createSMTComplexTypeReference => [it.referred = type.lookup(trace.typeTrace.independentClasses)], | ||
433 | null | ||
434 | ) | ||
435 | } | ||
436 | |||
437 | if(list.empty) throw new AssertionError('''Typereference to type is «type.name» empty''') | ||
438 | if(list.exists[it.type == null]){ | ||
439 | throw new AssertionError('''Typereference to null!''') | ||
440 | } | ||
441 | return list | ||
442 | } | ||
443 | |||
444 | override getTypeInterpretation(LogicProblem problem, SMTDocument document, SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) { | ||
445 | val model = document.output.getModelResult as SMTModelResult | ||
446 | val newTypeDec = trace.typeTrace.newObjects | ||
447 | var List<ValueType> newElements = null | ||
448 | |||
449 | if(newTypeDec instanceof SMTSetTypeDeclaration) { | ||
450 | val newElementType = model.typeDefinitions.filter[ | ||
451 | (it.type as SMTComplexTypeReference).referred == newTypeDec | ||
452 | ].head | ||
453 | newElements = newElementType.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it.symbolicReference)] | ||
454 | } else if(newTypeDec instanceof SMTEnumeratedTypeDeclaration) { | ||
455 | newElements = newTypeDec.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it)] | ||
456 | } else throw new IllegalArgumentException('''Unknown type : «newTypeDec.class.name»''') | ||
457 | |||
458 | val Map<DefinedElement, ValueType> logic2smt = new HashMap<DefinedElement,ValueType> | ||
459 | val Map<SMTSymbolicDeclaration, DefinedElement> smt2logic = new HashMap<SMTSymbolicDeclaration,DefinedElement> | ||
460 | |||
461 | var index = 1; | ||
462 | for(newElement : newElements) { | ||
463 | val n = '''new «index++»''' | ||
464 | val logic = factory2.createDefinedElement => [it.name = n] | ||
465 | logic2smt.put(logic,newElement) | ||
466 | smt2logic.put(newElement.value as SMTSymbolicDeclaration,logic) | ||
467 | } | ||
468 | for(oldElement : problem.elements) { | ||
469 | val declaration = trace.typeTrace.oldObjectTypeMap.get(oldElement) | ||
470 | logic2smt.put(oldElement,new ValueType(new TypeDescriptor(trace.typeTrace.oldObjects),declaration)) | ||
471 | smt2logic.put(declaration,oldElement) | ||
472 | } | ||
473 | |||
474 | val engine = ViatraQueryEngine.on(new EMFScope(problem)) | ||
475 | val supertypeStarMatcher = SupertypeStarMatcher.on(engine) | ||
476 | |||
477 | val type2Elements = (trace.typeTrace.oldObjectTypeMap.keySet + | ||
478 | trace.typeTrace.newObjectTypeMap.keySet) | ||
479 | .toInvertedMap[new LinkedList<DefinedElement>] | ||
480 | |||
481 | val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse | ||
482 | for(oldElement: trace.typeTrace.elementMap.values) { | ||
483 | val type = interpretation.queryEngine.resolveFunctionDefinition( | ||
484 | trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral | ||
485 | val dynamicType = type.lookup(inverseOldTypeMap) | ||
486 | val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) | ||
487 | supertypes.forEach[type2Elements.get(it) += oldElement.lookup(smt2logic)] | ||
488 | } | ||
489 | |||
490 | val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse | ||
491 | for(newElement: newElements.map[value as SMTSymbolicDeclaration]) { | ||
492 | val type = interpretation.queryEngine.resolveFunctionDeclaration( | ||
493 | trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral | ||
494 | val dynamicType = type.lookup(inverseNewTypeMap) | ||
495 | val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) | ||
496 | supertypes.forEach[type2Elements.get(it) += newElement.lookup(smt2logic)] | ||
497 | } | ||
498 | |||
499 | return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic) | ||
500 | } | ||
501 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ new file mode 100644 index 00000000..79fc38e6 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ | |||
@@ -0,0 +1,463 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import java.util.HashMap | ||
6 | import java.util.Map | ||
7 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
8 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition | ||
9 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral | ||
10 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
12 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | ||
15 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
16 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
18 | import java.util.List | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
20 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
21 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
22 | |||
23 | class Logic2Smt_TypeMapperTrace_FilteredTypesSimple implements Logic2Smt_TypeMapperTrace{ | ||
24 | public var Map<Type, SMTType> independentClasses = new HashMap | ||
25 | /** | ||
26 | * SMT type for the new objects | ||
27 | */ | ||
28 | public var SMTEnumeratedTypeDeclaration objects | ||
29 | /** | ||
30 | * existing element -> SMT literal map | ||
31 | */ | ||
32 | public var Map<DefinedElement, SMTEnumLiteral> elementMap = new HashMap | ||
33 | |||
34 | public var SMTEnumeratedTypeDeclaration objectTypes | ||
35 | public var Map<Type, SMTEnumLiteral> objectTypeMap = new HashMap | ||
36 | public var SMTFunctionDefinition objectTypeFunction | ||
37 | public var Map<Type, SMTFunctionDefinition> objectTypePredicates = new HashMap | ||
38 | |||
39 | override copy(SMTInput newModel) { | ||
40 | val a = this | ||
41 | val b = new Logic2Smt_TypeMapperTrace_FilteredTypesSimple | ||
42 | |||
43 | b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name]) | ||
44 | |||
45 | b.objects = newModel.typeDeclarations.filter[it.name == a.objects.name].head as SMTEnumeratedTypeDeclaration | ||
46 | b.elementMap = a.elementMap.copyMap(b.objects.elements,[name]) | ||
47 | |||
48 | b.objectTypes = newModel.typeDeclarations.filter[it.name == a.objects.name].head as SMTEnumeratedTypeDeclaration | ||
49 | b.objectTypeMap = a.objectTypeMap.copyMap(b.objectTypes.elements,[name]) | ||
50 | b.objectTypeFunction = newModel.functionDefinition.filter[it.name == a.objectTypeFunction.name].head | ||
51 | b.objectTypePredicates = a.objectTypePredicates.copyMap(newModel.functionDefinition,[name]) | ||
52 | |||
53 | return b | ||
54 | } | ||
55 | } | ||
56 | |||
57 | class Logic2Smt_TypeMapper_FilteredTypesSimple implements Logic2Smt_TypeMapper{ | ||
58 | val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE | ||
59 | val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE | ||
60 | |||
61 | private def toID(List<String> names) {names.join("!") } | ||
62 | private def toID(String name) {name.split("\\s+").toID} | ||
63 | |||
64 | override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { | ||
65 | val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes | ||
66 | trace.typeMapperTrace = typeTrace | ||
67 | val engine = ViatraQueryEngine.on(new EMFScope(problem)) | ||
68 | |||
69 | val independentTypes = problem.types.filter(TypeDefinition).filter[isIndependentType] | ||
70 | |||
71 | val connectedTypes = problem.types.filter[!isIndependentType] | ||
72 | val connectedElements = problem.elements.filter[!isIndependentElement] | ||
73 | |||
74 | // 0. map the simple types | ||
75 | this.transformIndependentTypes(independentTypes,trace) | ||
76 | |||
77 | // 1. Has old elements => create supertype for it | ||
78 | |||
79 | this.transformDefinedElements(connectedElements, trace,document) | ||
80 | this.transformUndefinedElements(scopes,trace,document) | ||
81 | |||
82 | |||
83 | this.transforTypes(connectedTypes, connectedElements, trace, document, engine) | ||
84 | // 3.2: Type definition to new elements | ||
85 | if(hasNewElements) { | ||
86 | this.transformNewTypes(connectedTypesWithoutDefintypesWithoutDefinedSupertype,trace,document,engine); | ||
87 | } | ||
88 | } | ||
89 | |||
90 | private def isIndependentType(Type t) { | ||
91 | val res = (t instanceof TypeDefinition) && t.supertypes.empty && t.subtypes.empty | ||
92 | return res | ||
93 | } | ||
94 | private def isIndependentElement(DefinedElement e) { | ||
95 | val types = e.definedInType | ||
96 | return types.size == 1 && types.head.isIndependentType | ||
97 | } | ||
98 | |||
99 | protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace) { | ||
100 | for(type: types) { | ||
101 | val independentSMTType = createSMTEnumeratedTypeDeclaration => [ | ||
102 | name = toID(#["oldType",type.name]) | ||
103 | ] | ||
104 | trace.typeTrace.independentClasses.put(type,independentSMTType) | ||
105 | for(element : type.elements) { | ||
106 | val enumLiteral = createSMTEnumLiteral => [it.name = toID(#["oldElement",element.name])] | ||
107 | independentSMTType.elements += enumLiteral | ||
108 | trace.typeTrace.elementMap.put(element,enumLiteral) | ||
109 | } | ||
110 | } | ||
111 | } | ||
112 | |||
113 | protected def transformDefinedElements(Iterable<DefinedElement> oldElements, Logic2SmtMapperTrace trace, SMTInput document) { | ||
114 | val List<SMTEnumLiteral> literals = new ArrayList(oldElements.size) | ||
115 | for(element : oldElements) { | ||
116 | val elementName ='''oldElement «element.name»''' | ||
117 | val literal = createSMTEnumLiteral => [name = elementName.toID] | ||
118 | literals += literal | ||
119 | trace.typeTrace.elementMap.put(element,literal) | ||
120 | } | ||
121 | trace.typeTrace.oldObjects = createSMTEnumeratedTypeDeclaration => | ||
122 | [name = "oldObjects" it.elements += literals] | ||
123 | document.typeDeclarations += trace.typeTrace.oldObjects | ||
124 | } | ||
125 | |||
126 | protected def transformUndefinedElements(TypeScopes scopes, Logic2SmtMapperTrace trace, SMTInput document) { | ||
127 | var SMTType newObjects | ||
128 | if(scopes.maxNewElements == -1) { | ||
129 | newObjects = createSMTSetTypeDeclaration => [ | ||
130 | name = "newObjects" | ||
131 | ] | ||
132 | } else { | ||
133 | val newElements = new ArrayList(scopes.maxNewElements) | ||
134 | for(index : (1..<scopes.maxNewElements+1)) { | ||
135 | val literal = createSMTEnumLiteral => [ | ||
136 | name = #["newElement",index.toString].toID | ||
137 | ] | ||
138 | newElements += literal | ||
139 | } | ||
140 | newObjects = createSMTEnumeratedTypeDeclaration => [ | ||
141 | name = "newObjects" | ||
142 | it.elements += newElements | ||
143 | ] | ||
144 | } | ||
145 | trace.typeTrace.newObjects = newObjects | ||
146 | document.typeDeclarations += newObjects | ||
147 | } | ||
148 | |||
149 | protected def transformOldTypes(Iterable<Type> oldTypes,Iterable<DefinedElement> oldElements, Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) { | ||
150 | val possibleTypeMatcher = PossibleDynamicTypeMatcher.on(engine) | ||
151 | val supertypeStarMatcher = SupertypeStarMatcher.on(engine) | ||
152 | // val possibleTypes = new LinkedList | ||
153 | // if(hasDefinedElement) possibleTypes += typesWithDefinedSupertype | ||
154 | // if(hasUndefinedElement) possibleTypes += typesWithoutDefinedSupertype | ||
155 | // val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract] | ||
156 | // val possibleConcreteTypes = possibleTypeMatcher.allValuesOfdynamic | ||
157 | |||
158 | // 3.1.1. cretate a type for old types | ||
159 | val possibleConcreteTypeLiterals = new ArrayList() | ||
160 | for(possibleConcreteType: oldTypes.filter[!isIsAbstract]) { | ||
161 | val typeName = '''oldType «possibleConcreteType.name»''' | ||
162 | val literal = createSMTEnumLiteral => [name = typeName.toID] | ||
163 | trace.typeTrace.oldObjectTypeMap.put(possibleConcreteType,literal) | ||
164 | possibleConcreteTypeLiterals+=literal | ||
165 | } | ||
166 | val oldObjectTypes = createSMTEnumeratedTypeDeclaration => [ | ||
167 | it.name = "oldTypes" | ||
168 | it.elements += possibleConcreteTypeLiterals | ||
169 | ] | ||
170 | trace.typeTrace.oldObjectTypes = oldObjectTypes | ||
171 | document.typeDeclarations += oldObjectTypes | ||
172 | |||
173 | // 3.1.2 for each object, create a constant for its possible dynamic type | ||
174 | val Map<DefinedElement,SMTFunctionDeclaration> possibleTypesOfElement = new HashMap | ||
175 | val Map<DefinedElement,Type> onlyPossibleType = new HashMap | ||
176 | for(object: oldElements) { | ||
177 | val types = possibleTypeMatcher.getAllValuesOfdynamic(null,object) | ||
178 | if(types.size == 1) { | ||
179 | onlyPossibleType.put(object,types.head) | ||
180 | } else { // including 0 or more than 1 | ||
181 | // create a constant declaration | ||
182 | val typeOfObjectConstant = createSMTFunctionDeclaration => [ | ||
183 | it.name = toID(#["typeDecisions",toID(object.name)]) | ||
184 | it.range = createSMTComplexTypeReference => [ | ||
185 | it.referred = trace.typeTrace.oldObjectTypes | ||
186 | ] | ||
187 | ] | ||
188 | document.functionDeclarations += typeOfObjectConstant | ||
189 | possibleTypesOfElement.put(object,typeOfObjectConstant) | ||
190 | // add assertions to the constant to select valid values | ||
191 | document.assertions += createSMTAssertion => [ | ||
192 | val options = types.map[type | createSMTEquals => [ | ||
193 | it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = typeOfObjectConstant] | ||
194 | it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = type.lookup(trace.typeTrace.oldObjectTypeMap)] | ||
195 | ]] | ||
196 | it.value = if(options.empty) { | ||
197 | createSMTBoolLiteral => [it.value = false] | ||
198 | } else { | ||
199 | createSMTOr=>[operands += options] | ||
200 | } | ||
201 | ] | ||
202 | } | ||
203 | } | ||
204 | |||
205 | // 3.1.2 create a function: old elements -> old types | ||
206 | val oldTypeFunction = createSMTFunctionDefinition => [ | ||
207 | it.name = "oldTypeFunction" | ||
208 | val o = createSMTSortedVariable => [ | ||
209 | it.name = "o" | ||
210 | it.range= createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects] | ||
211 | ] | ||
212 | it.parameters += o | ||
213 | it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjectTypes] | ||
214 | it.value = unfoldITE(oldElements, | ||
215 | [createSMTSymbolicValue => [it.symbolicReference = o]], | ||
216 | [DefinedElement e | createSMTSymbolicValue => [it.symbolicReference = e.lookup(trace.typeTrace.elementMap)]], | ||
217 | [DefinedElement e | | ||
218 | if(onlyPossibleType.containsKey(e)) { | ||
219 | return createSMTSymbolicValue => [ | ||
220 | symbolicReference = e.lookup(onlyPossibleType).lookup(trace.typeTrace.oldObjectTypeMap) ] | ||
221 | } else { | ||
222 | return createSMTSymbolicValue => [ | ||
223 | symbolicReference = e.lookup(possibleTypesOfElement) | ||
224 | ] | ||
225 | } | ||
226 | ] | ||
227 | ) | ||
228 | ] | ||
229 | trace.typeTrace.oldObjectTypeFunction = oldTypeFunction | ||
230 | document.functionDefinition += oldTypeFunction | ||
231 | |||
232 | // 3.1.3 create a predicate for each type: old object -> {true, false} | ||
233 | for(oldType: oldTypes) { | ||
234 | val oldTypePredicate = createSMTFunctionDefinition | ||
235 | oldTypePredicate.name = toID(#["oldTypePredicate",oldType.name.toID]) | ||
236 | val param = createSMTSortedVariable => [ | ||
237 | name = "o" | ||
238 | range = createSMTComplexTypeReference => [referred = trace.typeTrace.oldObjects] | ||
239 | ] | ||
240 | oldTypePredicate.parameters += param | ||
241 | oldTypePredicate.range = createSMTBoolTypeReference | ||
242 | val values = new LinkedList | ||
243 | for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(oldType).filter[!isIsAbstract]) { | ||
244 | val typeOfO = createSMTSymbolicValue => [ | ||
245 | it.symbolicReference = oldTypeFunction | ||
246 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param] | ||
247 | ] | ||
248 | val valueOfConcreteSupbtype = createSMTSymbolicValue => [ | ||
249 | it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.oldObjectTypeMap) | ||
250 | ] | ||
251 | values += createSMTEquals => [ | ||
252 | it.leftOperand = typeOfO | ||
253 | it.rightOperand = valueOfConcreteSupbtype | ||
254 | ] | ||
255 | } | ||
256 | oldTypePredicate.value = createSMTOr=>[it.operands +=values] | ||
257 | |||
258 | document.functionDefinition += oldTypePredicate | ||
259 | trace.typeTrace.oldObjectTypePredicates.put(oldType,oldTypePredicate) | ||
260 | } | ||
261 | } | ||
262 | |||
263 | protected def transformNewTypes( | ||
264 | Iterable<TypeDeclaration> typesWithoutDefinedSupertype, | ||
265 | Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) | ||
266 | { | ||
267 | val supertypeStarMatcher = SupertypeStarMatcher.on(engine) | ||
268 | val possibleTypes = typesWithoutDefinedSupertype | ||
269 | val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract].toList | ||
270 | |||
271 | // 3.2.1. cretate a type for new types | ||
272 | val possibleConcreteTypeLiterals = new ArrayList() | ||
273 | for(possibleConcreteType: possibleConcreteTypes) { | ||
274 | val typeName = '''newType «possibleConcreteType.name»''' | ||
275 | val literal = createSMTEnumLiteral => [name = typeName.toID] | ||
276 | trace.typeTrace.newObjectTypeMap.put(possibleConcreteType,literal) | ||
277 | possibleConcreteTypeLiterals+=literal | ||
278 | } | ||
279 | val newObjectTypes = createSMTEnumeratedTypeDeclaration => [ | ||
280 | it.name = "newTypes" | ||
281 | it.elements += possibleConcreteTypeLiterals | ||
282 | ] | ||
283 | trace.typeTrace.newObjectTypes = newObjectTypes | ||
284 | document.typeDeclarations += newObjectTypes | ||
285 | |||
286 | // 3.2.2 create a function: new elements -> new types | ||
287 | val newTypeFunction = createSMTFunctionDeclaration => [ | ||
288 | it.name = "newTypeFunction" | ||
289 | it.parameters += createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects] | ||
290 | it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjectTypes] | ||
291 | ] | ||
292 | trace.typeTrace.newObjectTypeFunction = newTypeFunction | ||
293 | document.functionDeclarations += newTypeFunction | ||
294 | |||
295 | // 3.1.3 create a predicate for each type: new type -> {true, false} | ||
296 | for(newType: possibleTypes) { | ||
297 | val newTypePredicate = createSMTFunctionDefinition | ||
298 | newTypePredicate.name = toID(#["newTypePredicate",newType.name.toID]) | ||
299 | val param = createSMTSortedVariable => [ | ||
300 | name = "o" | ||
301 | range = createSMTComplexTypeReference => [referred = trace.typeTrace.newObjects] | ||
302 | ] | ||
303 | newTypePredicate.parameters += param | ||
304 | newTypePredicate.range = createSMTBoolTypeReference | ||
305 | val values = new LinkedList | ||
306 | for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(newType).filter[!isIsAbstract]) { | ||
307 | if(possibleConcreteTypes.contains(concreteSupbtype)) { | ||
308 | val typeOfO = createSMTSymbolicValue => [ | ||
309 | it.symbolicReference = newTypeFunction | ||
310 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param] | ||
311 | ] | ||
312 | if(!trace.typeTrace.newObjectTypeMap.containsKey(concreteSupbtype)) { | ||
313 | println("gebasz") | ||
314 | } | ||
315 | val valueOfConcreteSupbtype = createSMTSymbolicValue => [ | ||
316 | it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.newObjectTypeMap) | ||
317 | ] | ||
318 | values+= createSMTEquals => [ | ||
319 | it.leftOperand = typeOfO | ||
320 | it.rightOperand = valueOfConcreteSupbtype | ||
321 | ] | ||
322 | } | ||
323 | } | ||
324 | newTypePredicate.value = createSMTOr=>[it.operands +=values] | ||
325 | |||
326 | document.functionDefinition += newTypePredicate | ||
327 | trace.typeTrace.newObjectTypePredicates.put(newType,newTypePredicate) | ||
328 | } | ||
329 | } | ||
330 | |||
331 | private def Logic2Smt_TypeMapperTrace_FilteredTypes getTypeTrace(Logic2SmtMapperTrace trace) { | ||
332 | val typeTrace = trace.typeMapperTrace | ||
333 | if(typeTrace instanceof Logic2Smt_TypeMapperTrace_FilteredTypes) { | ||
334 | return typeTrace | ||
335 | } else { | ||
336 | throw new IllegalArgumentException('''Unknown trace type: «typeTrace.class.name»''') | ||
337 | } | ||
338 | } | ||
339 | |||
340 | private def boolean hasDefinedSupertype(Type type) { | ||
341 | if(type instanceof TypeDefinition) { | ||
342 | return true | ||
343 | } else { | ||
344 | if(type.supertypes.empty) return false | ||
345 | else return type.supertypes.exists[it.hasDefinedSupertype] | ||
346 | } | ||
347 | } | ||
348 | |||
349 | def private <T> SMTTerm unfoldITE(Iterable<T> options, Function0<SMTTerm> input, Function1<T,SMTTerm> conditionOfOption, Function1<T,SMTTerm> outputForOption) { | ||
350 | if(options.size == 1) { | ||
351 | return outputForOption.apply(options.head) | ||
352 | } else { | ||
353 | return createSMTITE => [ | ||
354 | it.condition = createSMTEquals => [ | ||
355 | leftOperand = input.apply | ||
356 | rightOperand = conditionOfOption.apply(options.head) | ||
357 | ] | ||
358 | it.^if = outputForOption.apply(options.head) | ||
359 | it.^else = unfoldITE(options.tail,input,conditionOfOption,outputForOption) | ||
360 | ] | ||
361 | } | ||
362 | } | ||
363 | |||
364 | override transformSymbolicReference(DefinedElement referred,Logic2SmtMapperTrace trace) { | ||
365 | val x = referred.lookup(trace.typeTrace.elementMap) | ||
366 | new ComplexSubterm(#[],#[], | ||
367 | createSMTSymbolicValue => [it.symbolicReference = x], | ||
368 | new TypeDescriptor(x.eContainer as SMTEnumeratedTypeDeclaration) | ||
369 | ) | ||
370 | } | ||
371 | |||
372 | override transformTypeReference(Type type, Logic2SmtMapperTrace trace) { | ||
373 | val list = new ArrayList | ||
374 | |||
375 | if(trace.typeTrace.oldObjectTypePredicates.containsKey(type)) { | ||
376 | list += new TypeConstraint( | ||
377 | createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects], | ||
378 | [x|createSMTSymbolicValue => [ | ||
379 | it.symbolicReference = trace.typeTrace.oldObjectTypePredicates.get(type) | ||
380 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]] | ||
381 | ) | ||
382 | } | ||
383 | if(trace.typeTrace.newObjectTypePredicates.containsKey(type)) { | ||
384 | list += new TypeConstraint( | ||
385 | createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects], | ||
386 | [x|createSMTSymbolicValue => [ | ||
387 | it.symbolicReference = trace.typeTrace.newObjectTypePredicates.get(type) | ||
388 | it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]] | ||
389 | ) | ||
390 | } | ||
391 | if(trace.typeTrace.independentClasses.containsKey(type)) { | ||
392 | list += new TypeConstraint( | ||
393 | createSMTComplexTypeReference => [it.referred = type.lookup(trace.typeTrace.independentClasses)], | ||
394 | null | ||
395 | ) | ||
396 | } | ||
397 | |||
398 | if(list.empty) throw new AssertionError('''Typereference to type is «type.name» empty''') | ||
399 | if(list.exists[it.type == null]){ | ||
400 | throw new AssertionError('''Typereference to null!''') | ||
401 | } | ||
402 | return list | ||
403 | } | ||
404 | |||
405 | override getTypeInterpretation(LogicProblem problem, SMTDocument document, SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) { | ||
406 | val model = document.output.getModelResult as SMTModelResult | ||
407 | val newTypeDec = trace.typeTrace.newObjects | ||
408 | var List<ValueType> newElements = null | ||
409 | |||
410 | if(newTypeDec instanceof SMTSetTypeDeclaration) { | ||
411 | val newElementType = model.typeDefinitions.filter[ | ||
412 | (it.type as SMTComplexTypeReference).referred == newTypeDec | ||
413 | ].head | ||
414 | newElements = newElementType.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it.symbolicReference)] | ||
415 | } else if(newTypeDec instanceof SMTEnumeratedTypeDeclaration) { | ||
416 | newElements = newTypeDec.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it)] | ||
417 | } else throw new IllegalArgumentException('''Unknown type : «newTypeDec.class.name»''') | ||
418 | |||
419 | val Map<DefinedElement, ValueType> logic2smt = new HashMap<DefinedElement,ValueType> | ||
420 | val Map<SMTSymbolicDeclaration, DefinedElement> smt2logic = new HashMap<SMTSymbolicDeclaration,DefinedElement> | ||
421 | |||
422 | var index = 1; | ||
423 | for(newElement : newElements) { | ||
424 | val n = '''new «index++»''' | ||
425 | val logic = factory2.createDefinedElement => [it.name = n] | ||
426 | logic2smt.put(logic,newElement) | ||
427 | smt2logic.put(newElement.value as SMTSymbolicDeclaration,logic) | ||
428 | } | ||
429 | for(oldElement : problem.elements) { | ||
430 | val declaration = trace.typeTrace.oldObjectTypeMap.get(oldElement) | ||
431 | logic2smt.put(oldElement,new ValueType(new TypeDescriptor(trace.typeTrace.oldObjects),declaration)) | ||
432 | smt2logic.put(declaration,oldElement) | ||
433 | } | ||
434 | |||
435 | val engine = ViatraQueryEngine.on(new EMFScope(problem)) | ||
436 | val supertypeStarMatcher = SupertypeStarMatcher.on(engine) | ||
437 | |||
438 | val type2Elements = (trace.typeTrace.oldObjectTypeMap.keySet + | ||
439 | trace.typeTrace.newObjectTypeMap.keySet) | ||
440 | .toInvertedMap[new LinkedList<DefinedElement>] | ||
441 | |||
442 | val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse | ||
443 | for(oldElement: trace.typeTrace.elementMap.values) { | ||
444 | val type = interpretation.queryEngine.resolveFunctionDefinition( | ||
445 | trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral | ||
446 | val dynamicType = type.lookup(inverseOldTypeMap) | ||
447 | val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) | ||
448 | supertypes.forEach[type2Elements.get(it) += oldElement.lookup(smt2logic)] | ||
449 | } | ||
450 | |||
451 | val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse | ||
452 | for(newElement: newElements.map[value as SMTSymbolicDeclaration]) { | ||
453 | val type = interpretation.queryEngine.resolveFunctionDeclaration( | ||
454 | trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral | ||
455 | val dynamicType = type.lookup(inverseNewTypeMap) | ||
456 | val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) | ||
457 | supertypes.forEach[type2Elements.get(it) += newElement.lookup(smt2logic)] | ||
458 | } | ||
459 | |||
460 | return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic) | ||
461 | } | ||
462 | |||
463 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_Horizontal.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_Horizontal.xtend new file mode 100644 index 00000000..a5abbb44 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_Horizontal.xtend | |||
@@ -0,0 +1,63 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
8 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
9 | import java.util.List | ||
10 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
12 | |||
13 | class Logic2Smt_TypeMapperTrace_Horizontal implements Logic2Smt_TypeMapperTrace{ | ||
14 | |||
15 | override copy(SMTInput newModel) { | ||
16 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
17 | } | ||
18 | } | ||
19 | |||
20 | class Logic2Smt_TypeMapper_Horizontal implements Logic2Smt_TypeMapper { | ||
21 | val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE | ||
22 | |||
23 | private def toID(List<String> names) {names.join("!") } | ||
24 | |||
25 | override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { | ||
26 | val typeTrace = new Logic2Smt_TypeMapperTrace_Horizontal | ||
27 | trace.typeMapperTrace = typeTrace | ||
28 | |||
29 | // mapping of known elements | ||
30 | |||
31 | } | ||
32 | |||
33 | private def Logic2Smt_TypeMapperTrace_Horizontal getTypeTrace(Logic2SmtMapperTrace trace) { | ||
34 | val typeTrace = trace.typeMapperTrace | ||
35 | if(typeTrace instanceof Logic2Smt_TypeMapperTrace_Horizontal) { | ||
36 | return typeTrace | ||
37 | } else { | ||
38 | throw new IllegalArgumentException('''Unknown trace type: «typeTrace.class.name»''') | ||
39 | } | ||
40 | } | ||
41 | |||
42 | private def boolean hasDefinedSupertype(Type type) { | ||
43 | if(type instanceof TypeDefinition) { | ||
44 | return true | ||
45 | } else { | ||
46 | if(type.supertypes.empty) return false | ||
47 | else return type.supertypes.exists[it.hasDefinedSupertype] | ||
48 | } | ||
49 | } | ||
50 | |||
51 | override transformTypeReference(Type type, Logic2SmtMapperTrace trace) { | ||
52 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
53 | } | ||
54 | |||
55 | override transformSymbolicReference(DefinedElement referred, Logic2SmtMapperTrace trace) { | ||
56 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
57 | } | ||
58 | |||
59 | override getTypeInterpretation(LogicProblem problem, SMTDocument document, SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) { | ||
60 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
61 | } | ||
62 | |||
63 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend new file mode 100644 index 00000000..d371b89e --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend | |||
@@ -0,0 +1,49 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.SmtLanguageStandaloneSetupGenerated | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
8 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.builder.SmtSolverHandler | ||
9 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
10 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguagePackage | ||
11 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
12 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
13 | |||
14 | class SMTSolver extends LogicReasoner{ | ||
15 | |||
16 | public new() { | ||
17 | SmtLanguagePackage.eINSTANCE.eClass | ||
18 | val x = new SmtLanguageStandaloneSetupGenerated | ||
19 | x.createInjectorAndDoEMFRegistration | ||
20 | } | ||
21 | |||
22 | val forwardMapper = new Logic2SmtMapper(new Logic2Smt_TypeMapper_FilteredTypes); | ||
23 | val backMapper = new Smt2LogicMapper; | ||
24 | val handler = new SmtSolverHandler | ||
25 | |||
26 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) { | ||
27 | if(configuration instanceof SmtSolverConfiguration) { | ||
28 | val transformationStart = System.currentTimeMillis | ||
29 | val transformationResult = forwardMapper.transformProblem(problem,configuration.typeScopes,configuration.strategy) | ||
30 | val SMTDocument inputModel= transformationResult.output | ||
31 | val trace = transformationResult.trace | ||
32 | val input = workspace.writeModel(inputModel,"problem.smt2") | ||
33 | val transformationTime = System.currentTimeMillis-transformationStart | ||
34 | val solverTimeStart = System.currentTimeMillis | ||
35 | handler.callSolver(input,configuration) | ||
36 | val solverTime = System.currentTimeMillis - solverTimeStart | ||
37 | val outputModel = workspace.reloadModel(typeof(SMTDocument), "problem.smt2") | ||
38 | EcoreUtil.resolveAll(outputModel) | ||
39 | workspace.deactivateModel("problem.smt2") | ||
40 | return backMapper.transformOutput(problem,outputModel.output,trace, transformationTime, solverTime) | ||
41 | } else throw new IllegalArgumentException('''The configuration have to be an «SmtSolverConfiguration.simpleName»!''') | ||
42 | } | ||
43 | |||
44 | override getInterpretation(ModelResult modelResult) { | ||
45 | val representation = modelResult.representation as SMTDocument | ||
46 | val trace = modelResult.trace as Logic2SmtMapperTrace | ||
47 | return new SmtModelInterpretation(trace.problem,representation,trace.forwardMapper,trace) | ||
48 | } | ||
49 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend new file mode 100644 index 00000000..cbabc7b0 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend | |||
@@ -0,0 +1,71 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput | ||
4 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticsSection | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticIntValue | ||
7 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticDoubleValue | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
9 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTErrorResult | ||
10 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSatResult | ||
11 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTUnsupportedResult | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | ||
14 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticValue | ||
15 | import java.math.BigDecimal | ||
16 | |||
17 | class Smt2LogicMapper { | ||
18 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | ||
19 | |||
20 | public def transformOutput(LogicProblem problem, SMTOutput output, Logic2SmtMapperTrace trace, long transformationTime, long solverTime) { | ||
21 | val satResult = output.satResult | ||
22 | if(satResult === null) { // Timeout | ||
23 | return createInsuficientResourcesResult => [ init(problem,output,transformationTime,solverTime) it.resourceName = "time"] | ||
24 | } else { | ||
25 | if(satResult instanceof SMTErrorResult) { | ||
26 | return createErrorResult => [init(problem,output,transformationTime,solverTime) message = satResult.message] | ||
27 | } else if(satResult instanceof SMTUnsupportedResult) { | ||
28 | return createUndecidableResult => [init(problem,output,transformationTime,solverTime)] | ||
29 | } else if(satResult instanceof SMTSatResult) { | ||
30 | if(satResult.sat) { | ||
31 | return createModelResult => [ | ||
32 | init(problem,output,transformationTime,solverTime) | ||
33 | representation += output.eContainer | ||
34 | it.trace = trace | ||
35 | ] | ||
36 | } else if(satResult.unsat) { | ||
37 | return createInconsistencyResult => [init(problem,output,transformationTime,solverTime)] | ||
38 | } else if(satResult.unknown) { | ||
39 | return createUndecidableResult => [init(problem,output,transformationTime,solverTime)] | ||
40 | } | ||
41 | } else throw new LogicReasonerException("The solver resulted with unknown result.") | ||
42 | } | ||
43 | } | ||
44 | |||
45 | private def init(LogicResult result,LogicProblem problem, SMTOutput output, long transformationTime, long solverTime) { | ||
46 | result.problem = problem | ||
47 | result.statistics = output.statistics.transformStatistics(transformationTime,solverTime) | ||
48 | } | ||
49 | |||
50 | protected def transformStatistics(SMTStatisticsSection section, long transformationTime, long solverTime) { | ||
51 | createStatistics => [ | ||
52 | it.transformationTime = transformationTime.intValue | ||
53 | it.solverTime = solverTime.intValue | ||
54 | |||
55 | val memorySection = section.values.filter[it.name==":memory"].head | ||
56 | if(memorySection != null) { | ||
57 | it.solverMemory = ((memorySection as SMTStatisticDoubleValue).value.add(BigDecimal.valueOf(0.5))).intValue | ||
58 | } | ||
59 | entries += section.values.map[transformEntry] | ||
60 | ] | ||
61 | } | ||
62 | |||
63 | protected def dispatch transformEntry(SMTStatisticIntValue entry) { | ||
64 | createIntStatisticEntry => [name = entry.exportName value = entry.value] } | ||
65 | protected def dispatch transformEntry(SMTStatisticDoubleValue entry) { | ||
66 | createRealStatisticEntry => [name = entry.exportName value = entry.value.doubleValue] } | ||
67 | |||
68 | private def exportName(SMTStatisticValue value) { | ||
69 | return value.name.replaceFirst(":","") | ||
70 | } | ||
71 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend new file mode 100644 index 00000000..fb0739ab --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend | |||
@@ -0,0 +1,167 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
11 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.builder.SmtModelQueryEngine | ||
12 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
13 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
14 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration | ||
15 | import org.eclipse.xtend.lib.annotations.Accessors | ||
16 | import org.eclipse.xtend.lib.annotations.Data | ||
17 | |||
18 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
19 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration | ||
20 | |||
21 | @Data | ||
22 | class ValueType { | ||
23 | TypeDescriptor descriptor | ||
24 | Object value | ||
25 | } | ||
26 | |||
27 | class SmtModelInterpretation implements LogicModelInterpretation { | ||
28 | //val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
29 | @Accessors(PUBLIC_GETTER) val SmtModelQueryEngine queryEngine; | ||
30 | |||
31 | // Trace info | ||
32 | val Logic2SmtMapperTrace newTrace; | ||
33 | val Logic2SMT_TypeMapperInterpretation typeInterpretation | ||
34 | |||
35 | /** | ||
36 | * Creates a model builder which queries a logic structure. | ||
37 | * @param document The whole SMT2 document. | ||
38 | * @param trace The trace of the [Logic problem -> SMT problem] mapping | ||
39 | */ | ||
40 | new(LogicProblem problem, SMTDocument document, Logic2SmtMapper forwardMapper, Logic2SmtMapperTrace forwardTrace) { | ||
41 | //document.input.typeDeclarations.forEach[typeNames.put(it.name,it)] | ||
42 | |||
43 | this.queryEngine = new SmtModelQueryEngine(document) | ||
44 | this.newTrace = initialiseNewTrace(document,forwardTrace) | ||
45 | this.typeInterpretation = forwardMapper.typeMapper.getTypeInterpretation(problem,document,this,newTrace) | ||
46 | } | ||
47 | |||
48 | /** | ||
49 | * Creates a new trace from the logic model to the new smt file by using the old trace. | ||
50 | */ | ||
51 | def protected Logic2SmtMapperTrace initialiseNewTrace(SMTDocument document, Logic2SmtMapperTrace oldTrace) { | ||
52 | val i = document.input | ||
53 | |||
54 | val res = new Logic2SmtMapperTrace => [ typeMapperTrace = oldTrace.typeMapperTrace.copy(i) ] | ||
55 | |||
56 | for(entry : oldTrace.relationUnfolding.entrySet) { | ||
57 | val rel = entry.key | ||
58 | val descriptors = entry.value.map[old | | ||
59 | new Descriptor<Relation>( | ||
60 | old.parameterTypes.map[copyTypeDescriptor(i)], | ||
61 | old.relation) | ||
62 | ] | ||
63 | res.relationUnfolding.put(rel,descriptors) | ||
64 | } | ||
65 | |||
66 | for(entry : oldTrace.relationMap.entrySet) { | ||
67 | val desc = new Descriptor<Relation>( | ||
68 | entry.key.parameterTypes.map[copyTypeDescriptor(i)], | ||
69 | entry.key.relation) | ||
70 | val fun = i.functionDeclarations.filter[it.name == entry.value.name].head | ||
71 | res.relationMap.put(desc,fun) | ||
72 | } | ||
73 | |||
74 | return res | ||
75 | } | ||
76 | |||
77 | def private copyTypeDescriptor(TypeDescriptor original, SMTInput i) { | ||
78 | if(original.complexType == null) return original | ||
79 | else { | ||
80 | val newType = i.typeDeclarations.filter[it.name == original.complexType.name].head | ||
81 | new TypeDescriptor(newType) | ||
82 | } | ||
83 | } | ||
84 | |||
85 | /*def protected initialiseTypes(SMTDocument document) { | ||
86 | val model = document.output.getModelResult as SMTModelResult | ||
87 | val smtUndefinedType2LogicType = this.newTrace.typeDeclarationMap.bijectiveInverse | ||
88 | |||
89 | for(cardinalityConstraint : model.typeDefinitions) { | ||
90 | val targetType = (cardinalityConstraint.type as SMTComplexTypeReference).referred as SMTSetTypeDeclaration | ||
91 | val List<DefinedElement> elementCollection = new LinkedList | ||
92 | for(element : cardinalityConstraint.elements.map[symbolicReference]) { | ||
93 | if(element instanceof SMTFunctionDeclaration) { | ||
94 | val definedElementRepresentation = createDefinedElement => [name += element.name.split("!")] | ||
95 | newElement2Constants.put(definedElementRepresentation,element) | ||
96 | newConstants2Elements.put(element,definedElementRepresentation) | ||
97 | } else{ | ||
98 | throw new UnsupportedOperationException( | ||
99 | "Unresolvable reference in cardinality constraint: " + element.class.name + ": " + element.name) | ||
100 | } | ||
101 | } | ||
102 | undefinedTypeDefinitions.put(targetType.lookup(smtUndefinedType2LogicType),elementCollection); | ||
103 | } | ||
104 | }*/ | ||
105 | |||
106 | def private dispatch ValueType logicLiteral2SmtLiteral(Integer literal) { | ||
107 | new ValueType(TypeDescriptor::numericTypeDescriptor_Instance, literal) | ||
108 | } | ||
109 | def private dispatch ValueType logicLiteral2SmtLiteral(Boolean literal) { | ||
110 | new ValueType(TypeDescriptor::logicTypeDescriptor_Instance, literal) | ||
111 | } | ||
112 | def private dispatch ValueType logicLiteral2SmtLiteral(DefinedElement literal) { | ||
113 | this.typeInterpretation.logicElement2Smt(literal) | ||
114 | } | ||
115 | |||
116 | // def private dispatch Object smt2Literal2LogicLiteral(Integer literal) { literal } | ||
117 | // def private dispatch Object smt2Literal2LogicLiteral(Boolean literal) { literal } | ||
118 | // def private dispatch Object smt2Literal2LogicLiteral(SMTSymbolicDeclaration literal) { | ||
119 | // this.typeInterpretation.smtElement2Logic(literal) | ||
120 | // } | ||
121 | |||
122 | override getElements(Type type) { | ||
123 | return this.typeInterpretation.getElements(type) | ||
124 | } | ||
125 | |||
126 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | ||
127 | /*queryEngine.resolveFunctionDeclaration( | ||
128 | function.lookup(newTrace.functionDeclarationMap), | ||
129 | parameterSubstitution.map[logicLiteral2SmtLiteral] | ||
130 | ).smt2Literal2LogicLiteral*/ | ||
131 | throw new UnsupportedOperationException | ||
132 | } | ||
133 | |||
134 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | ||
135 | val transformedParameters = parameterSubstitution.map[logicLiteral2SmtLiteral] | ||
136 | |||
137 | val smtFunction = new Descriptor<Relation>( | ||
138 | transformedParameters.map[descriptor], | ||
139 | relation) | ||
140 | .lookup(newTrace.relationMap) | ||
141 | |||
142 | val result = queryEngine.resolveFunctionDeclaration( | ||
143 | smtFunction as SMTFunctionDeclaration, | ||
144 | transformedParameters.map[value] | ||
145 | ) as Boolean | ||
146 | |||
147 | return result | ||
148 | } | ||
149 | |||
150 | override getInterpretation(ConstantDeclaration constant) { | ||
151 | /*queryEngine.resolveFunctionDeclaration( | ||
152 | constant.lookup(newTrace.constantDeclarationMap), | ||
153 | Collections.EMPTY_LIST | ||
154 | ).smt2Literal2LogicLiteral*/ | ||
155 | throw new UnsupportedOperationException | ||
156 | } | ||
157 | |||
158 | override getMaximalInteger() { | ||
159 | 100 | ||
160 | //throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
161 | } | ||
162 | |||
163 | override getMinimalInteger() { | ||
164 | -100 | ||
165 | //throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
166 | } | ||
167 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtSolverConfiguration.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtSolverConfiguration.xtend new file mode 100644 index 00000000..2a926cb6 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtSolverConfiguration.xtend | |||
@@ -0,0 +1,9 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
4 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTReasoningTactic | ||
5 | |||
6 | class SmtSolverConfiguration extends LogicSolverConfiguration{ | ||
7 | public boolean fixRandomSeed = false | ||
8 | public SMTReasoningTactic strategy = null | ||
9 | } | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend new file mode 100644 index 00000000..48952288 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend | |||
@@ -0,0 +1,183 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable | ||
4 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue | ||
5 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm | ||
6 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | ||
7 | import java.util.ArrayList | ||
8 | import java.util.List | ||
9 | import java.util.Map | ||
10 | import org.eclipse.emf.ecore.EObject | ||
11 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
12 | import org.eclipse.xtend.lib.annotations.Data | ||
13 | import java.util.HashMap | ||
14 | import java.util.LinkedList | ||
15 | |||
16 | abstract class TransformedSubterm { | ||
17 | val static extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE | ||
18 | def LogicSubterm expectLogic() | ||
19 | def NumericSubterm expectNumber() | ||
20 | |||
21 | def List<SubtermOption> getPossibleValues() | ||
22 | |||
23 | public static def List<List<SubtermOption>> allCombinations(List<SubtermOption>... possibleValues) { | ||
24 | return allCombinations(possibleValues.toList) | ||
25 | } | ||
26 | public static def List<List<SubtermOption>> allCombinations(Iterable<List<SubtermOption>> possibleValues) { | ||
27 | if(possibleValues.size == 1) { | ||
28 | return possibleValues.head.map[x|#[x.copy]] | ||
29 | } else { | ||
30 | val head = possibleValues.head | ||
31 | val tails = possibleValues.tail.allCombinations | ||
32 | val res = new ArrayList(tails.size * head.size) | ||
33 | for(headElement : head) { | ||
34 | for(tail : tails) { | ||
35 | val combination = new ArrayList(tail.size+1) | ||
36 | combination.add(headElement) | ||
37 | combination.addAll(tail.map[copy]) | ||
38 | res.add(combination) | ||
39 | } | ||
40 | } | ||
41 | return res | ||
42 | } | ||
43 | } | ||
44 | |||
45 | public static def resolveToLogic(List<SubtermOption> subterms, SMTTerm value) { | ||
46 | val allDefinitions = subterms.map[it.variables].flatten | ||
47 | val allPreconditions = subterms.map[it.preconditions].flatten | ||
48 | val preconditionedExpression = if(allPreconditions.empty) { | ||
49 | value | ||
50 | } else { | ||
51 | createSMTAnd => [it.operands += allPreconditions it.operands += value] | ||
52 | } | ||
53 | val quantifiedExpression = if(allDefinitions.empty) { | ||
54 | preconditionedExpression | ||
55 | } else { | ||
56 | createSMTForall => [ | ||
57 | it.quantifiedVariables += allDefinitions | ||
58 | it.expression = preconditionedExpression] | ||
59 | } | ||
60 | return quantifiedExpression | ||
61 | } | ||
62 | } | ||
63 | |||
64 | @Data class SubtermOption { | ||
65 | List<SMTSortedVariable> variables | ||
66 | List<SMTTerm> preconditions | ||
67 | SMTTerm expression | ||
68 | TypeDescriptor type | ||
69 | |||
70 | public new( | ||
71 | List<SMTSortedVariable> variables, | ||
72 | List<SMTTerm> preconditions, | ||
73 | SMTTerm expression, | ||
74 | TypeDescriptor type) | ||
75 | { | ||
76 | this.variables = variables | ||
77 | this.preconditions = preconditions | ||
78 | this.expression = expression | ||
79 | this.type = type | ||
80 | } | ||
81 | |||
82 | public new( | ||
83 | List<SubtermOption> previousSubterms, | ||
84 | List<SMTSortedVariable> newVariables, | ||
85 | List<SMTTerm> newPreconditions, | ||
86 | SMTTerm newExpression, | ||
87 | TypeDescriptor newType) | ||
88 | { | ||
89 | val old2New = new HashMap | ||
90 | variables = new LinkedList | ||
91 | for(variable : previousSubterms.map[getVariables].flatten) { | ||
92 | val newVariable = EcoreUtil.copy(variable) | ||
93 | old2New.put(variable,newVariable) | ||
94 | variables+=newVariable | ||
95 | } | ||
96 | |||
97 | preconditions = new LinkedList | ||
98 | preconditions += previousSubterms.map[getPreconditions].flatten.map[x|EcoreUtil.copy(x)] | ||
99 | preconditions += newPreconditions.map[x|EcoreUtil.copy(x)] | ||
100 | preconditions.forEach[relinkAllVariableReference(old2New)] | ||
101 | |||
102 | expression = EcoreUtil.copy(newExpression) | ||
103 | relinkAllVariableReference(expression,old2New) | ||
104 | |||
105 | type = newType | ||
106 | } | ||
107 | |||
108 | public def copy() { | ||
109 | val old2New = variables.toInvertedMap[EcoreUtil.copy(it)] | ||
110 | val newPreconditions = preconditions.map[EcoreUtil.copy(it)] | ||
111 | newPreconditions.forEach[it.relinkAllVariableReference(old2New)] | ||
112 | val newExpression = EcoreUtil.copy(expression) | ||
113 | return new SubtermOption(variables.map[old2New.get(it)],newPreconditions,newExpression,type) | ||
114 | } | ||
115 | |||
116 | def private relinkAllVariableReference(EObject root,Map<SMTSortedVariable, SMTSortedVariable> map) { | ||
117 | if(root instanceof SMTSymbolicValue) root.relinkVariableReference(map) | ||
118 | root.eAllContents().filter(SMTSymbolicValue).forEach[relinkVariableReference(map)] | ||
119 | } | ||
120 | def private relinkVariableReference(SMTSymbolicValue target,Map<SMTSortedVariable, SMTSortedVariable> map) { | ||
121 | if(map.containsKey(target.symbolicReference)) { | ||
122 | target.symbolicReference = map.get(target.symbolicReference) | ||
123 | } | ||
124 | } | ||
125 | } | ||
126 | |||
127 | @Data | ||
128 | class LogicSubterm extends TransformedSubterm{ | ||
129 | |||
130 | SMTTerm value | ||
131 | override expectLogic() {return this} | ||
132 | override expectNumber() { throw new AssertionError("A term is not a number") } | ||
133 | |||
134 | public new(SMTTerm expression) | ||
135 | { | ||
136 | this.value = expression | ||
137 | } | ||
138 | override getPossibleValues() { | ||
139 | #[new SubtermOption(#[],#[],value,TypeDescriptor::logicTypeDescriptor_Instance)] | ||
140 | } | ||
141 | } | ||
142 | |||
143 | @Data | ||
144 | class NumericSubterm extends TransformedSubterm { | ||
145 | List<SubtermOption> values | ||
146 | |||
147 | public new( | ||
148 | List<SMTSortedVariable> variables, | ||
149 | List<SMTTerm> preconditions, | ||
150 | SMTTerm expression) { | ||
151 | this.values = #[new SubtermOption(variables,preconditions,expression,TypeDescriptor.numericTypeDescriptor_Instance)] | ||
152 | } | ||
153 | public new(List<SubtermOption> values) { | ||
154 | this.values = values | ||
155 | } | ||
156 | |||
157 | override expectLogic() { throw new AssertionError("A term is not a logic value") } | ||
158 | override expectNumber() { return this } | ||
159 | |||
160 | override getPossibleValues() { | ||
161 | values | ||
162 | } | ||
163 | } | ||
164 | |||
165 | @Data | ||
166 | class ComplexSubterm extends TransformedSubterm { | ||
167 | List<SubtermOption> options | ||
168 | override expectLogic() { throw new AssertionError("A term is not a logic value") } | ||
169 | override expectNumber() { throw new AssertionError("A term is not a number") } | ||
170 | public new(List<SMTSortedVariable> variables, | ||
171 | List<SMTTerm> preconditions, | ||
172 | SMTTerm expression, | ||
173 | TypeDescriptor type) | ||
174 | { | ||
175 | this.options = #[new SubtermOption(variables,preconditions,expression,type)] | ||
176 | } | ||
177 | public new(List<SubtermOption> subterms) { | ||
178 | this.options = subterms | ||
179 | } | ||
180 | override getPossibleValues() { | ||
181 | this.options | ||
182 | } | ||
183 | } | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TypeDescriptor.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TypeDescriptor.xtend new file mode 100644 index 00000000..1aa5cf04 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TypeDescriptor.xtend | |||
@@ -0,0 +1,44 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference | ||
4 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference | ||
5 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference | ||
6 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealTypeReference | ||
7 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType | ||
8 | import java.util.List | ||
9 | import org.eclipse.xtend.lib.annotations.Accessors | ||
10 | import org.eclipse.xtend.lib.annotations.Data | ||
11 | |||
12 | @Data | ||
13 | class Descriptor<T> { | ||
14 | List<TypeDescriptor> parameterTypes | ||
15 | T relation | ||
16 | } | ||
17 | |||
18 | @Data | ||
19 | class TypeDescriptor { | ||
20 | val boolean logic | ||
21 | val boolean numeric | ||
22 | val SMTType complexType | ||
23 | |||
24 | @Accessors(PUBLIC_GETTER) | ||
25 | static val LogicTypeDescriptor_Instance = new TypeDescriptor(true,false,null) | ||
26 | @Accessors(PUBLIC_GETTER) | ||
27 | static val NumericTypeDescriptor_Instance = new TypeDescriptor(false,true,null) | ||
28 | |||
29 | private new(boolean logic, boolean numeric, SMTType complexType) { | ||
30 | this.logic = logic | ||
31 | this.numeric = numeric | ||
32 | this.complexType = complexType | ||
33 | } | ||
34 | public new(SMTType complexType) { | ||
35 | this.logic = false | ||
36 | this.numeric = false | ||
37 | this.complexType = complexType | ||
38 | } | ||
39 | |||
40 | def static dispatch createFromTypeReference(SMTBoolTypeReference ref) { return TypeDescriptor::LogicTypeDescriptor_Instance} | ||
41 | def static dispatch createFromTypeReference(SMTIntTypeReference ref) { return TypeDescriptor::NumericTypeDescriptor_Instance} | ||
42 | def static dispatch createFromTypeReference(SMTRealTypeReference ref) { return TypeDescriptor::NumericTypeDescriptor_Instance} | ||
43 | def static dispatch createFromTypeReference(SMTComplexTypeReference ref) { return new TypeDescriptor(false,false,ref.referred)} | ||
44 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend new file mode 100644 index 00000000..a259d103 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend | |||
@@ -0,0 +1,314 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd | ||
4 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolLiteral | ||
5 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference | ||
6 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference | ||
7 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
8 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral | ||
9 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration | ||
10 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEquals | ||
11 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration | ||
12 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition | ||
13 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTITE | ||
14 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
15 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral | ||
16 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference | ||
17 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMinus | ||
18 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult | ||
19 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput | ||
20 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable | ||
21 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue | ||
22 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm | ||
23 | import java.util.HashMap | ||
24 | import java.util.List | ||
25 | import java.util.Map | ||
26 | |||
27 | class SmtModelQueryEngine { | ||
28 | private Map<SMTFunctionDeclaration, SMTFunctionDefinition> functionDeclarationToDefinitions = | ||
29 | new HashMap<SMTFunctionDeclaration, SMTFunctionDefinition> | ||
30 | |||
31 | private val SMTInput input; | ||
32 | private val SMTOutput output | ||
33 | |||
34 | new(SMTDocument model) { | ||
35 | val nameToFunctionDefiniton = new HashMap<String, SMTFunctionDefinition> | ||
36 | input = model.input | ||
37 | var SMTModelResult modelResult = null | ||
38 | |||
39 | output = model.output | ||
40 | if(output!=null) { | ||
41 | val result = output.getModelResult | ||
42 | if(result instanceof SMTModelResult) { | ||
43 | modelResult = result as SMTModelResult | ||
44 | } | ||
45 | } | ||
46 | |||
47 | input.functionDefinition. | ||
48 | forEach[x|nameToFunctionDefiniton.put(x.name,x)] | ||
49 | if(modelResult!=null) | ||
50 | modelResult.newFunctionDefinitions. | ||
51 | forEach[x|nameToFunctionDefiniton.put(x.name,x)] | ||
52 | |||
53 | input.functionDeclarations. | ||
54 | forEach[x|functionDeclarationToDefinitions.put(x,x.name.lookup(nameToFunctionDefiniton))] | ||
55 | if(modelResult!=null) | ||
56 | modelResult.newFunctionDeclarations. | ||
57 | forEach[x|functionDeclarationToDefinitions.put(x,x.name.lookup(nameToFunctionDefiniton))] | ||
58 | } | ||
59 | |||
60 | def protected <KEY_TYPE,VALUE_TYPE> VALUE_TYPE lookup(KEY_TYPE key, Map<? extends KEY_TYPE,? extends VALUE_TYPE> map) { | ||
61 | return map.get(key) | ||
62 | } | ||
63 | |||
64 | def protected dispatch getDefaultValue(SMTIntTypeReference reference) { 0 } | ||
65 | def protected dispatch getDefaultValue(SMTBoolTypeReference reference) { false } | ||
66 | def protected dispatch getDefaultValue(SMTComplexTypeReference reference) { | ||
67 | val type = reference.referred | ||
68 | if(type instanceof SMTEnumeratedTypeDeclaration) return type.elements.head | ||
69 | else { | ||
70 | val definition = (output.getModelResult as SMTModelResult).typeDefinitions.filter[it.type == type].head | ||
71 | return definition.elements.head | ||
72 | } | ||
73 | } | ||
74 | |||
75 | def protected isTerminal( | ||
76 | SMTTerm term, | ||
77 | Map<SMTSortedVariable,Object> substitution) | ||
78 | { | ||
79 | /* | ||
80 | * An undefined function is a terminal. | ||
81 | */ | ||
82 | if(term instanceof SMTSymbolicValue) { | ||
83 | val symbolicValue = term as SMTSymbolicValue | ||
84 | |||
85 | if(symbolicValue.symbolicReference instanceof SMTFunctionDeclaration) | ||
86 | { | ||
87 | val function = symbolicValue.symbolicReference as SMTFunctionDeclaration; | ||
88 | val hasDefinition = functionDeclarationToDefinitions.get(function) != null | ||
89 | return ! hasDefinition | ||
90 | } | ||
91 | else return false | ||
92 | } | ||
93 | /* | ||
94 | * A finite element is a terminal. | ||
95 | */ | ||
96 | else if(term instanceof SMTEnumLiteral) | ||
97 | return true | ||
98 | else return false | ||
99 | } | ||
100 | def protected resolveTerminal( | ||
101 | SMTTerm terminal, | ||
102 | Map<SMTSortedVariable,Object> substitution) | ||
103 | { | ||
104 | if(terminal instanceof SMTEnumLiteral) { | ||
105 | return terminal; | ||
106 | } | ||
107 | else if(terminal instanceof SMTSymbolicValue) { | ||
108 | val symbolicValue = terminal as SMTSymbolicValue | ||
109 | if(symbolicValue.symbolicReference instanceof SMTFunctionDeclaration) | ||
110 | { | ||
111 | val function = symbolicValue.symbolicReference as SMTFunctionDeclaration; | ||
112 | return function | ||
113 | } | ||
114 | } | ||
115 | } | ||
116 | |||
117 | def public Object resolveFunctionDeclaration( | ||
118 | SMTFunctionDeclaration declaration, | ||
119 | List<Object> params) | ||
120 | { | ||
121 | |||
122 | val definition = declaration.lookup(functionDeclarationToDefinitions) | ||
123 | if(definition == null) return declaration.range.defaultValue | ||
124 | else return definition.resolveFunctionDefinition(params) | ||
125 | } | ||
126 | def public Object resolveFunctionDefinition( | ||
127 | SMTFunctionDefinition definition, | ||
128 | List<Object> params) | ||
129 | { | ||
130 | if(params.nullOrEmpty && definition.parameters.nullOrEmpty) { | ||
131 | return definition.resolveFunctionDefinition(emptyMap) | ||
132 | } | ||
133 | else if(params.size!=definition.parameters.size) | ||
134 | throw new IllegalArgumentException( | ||
135 | "Incorrect number of parameters!") | ||
136 | else { | ||
137 | val substitution = new HashMap<SMTSortedVariable,Object> | ||
138 | if(! definition.parameters.nullOrEmpty) { | ||
139 | for(i : 0..definition.parameters.size-1) { | ||
140 | substitution.put( | ||
141 | definition.parameters.get(i), | ||
142 | params.get(i)) | ||
143 | } | ||
144 | } | ||
145 | val result=definition.resolveFunctionDefinition(substitution) | ||
146 | //System::out.println(definition.name+"("+params.map[toString] + ") = " + result) | ||
147 | return result | ||
148 | } | ||
149 | } | ||
150 | def protected Object resolveFunctionDefinition( | ||
151 | SMTFunctionDefinition definition, | ||
152 | Map<SMTSortedVariable,Object> substitution) | ||
153 | { | ||
154 | definition.value.resolveValue(substitution) | ||
155 | } | ||
156 | |||
157 | def protected isBoolLiteral(SMTTerm term, Map<SMTSortedVariable,Object> substitution) { | ||
158 | term instanceof SMTBoolLiteral | ||
159 | } | ||
160 | def protected resolveBoolLiteral(SMTTerm boolValue, Map<SMTSortedVariable,Object> substitution) { | ||
161 | return (boolValue as SMTBoolLiteral).^value | ||
162 | } | ||
163 | |||
164 | def protected isIntLiteral(SMTTerm term, Map<SMTSortedVariable,Object> substitution) { | ||
165 | term instanceof SMTIntLiteral || | ||
166 | (term instanceof SMTMinus && (term as SMTMinus).rightOperand==null) | ||
167 | } | ||
168 | def protected resolveIntLiteral(SMTTerm intValue, Map<SMTSortedVariable,Object> substitution) { | ||
169 | if(intValue instanceof SMTIntLiteral) return (intValue as SMTIntLiteral).^value | ||
170 | else return -((intValue as SMTMinus).leftOperand as SMTIntLiteral).value | ||
171 | } | ||
172 | |||
173 | def protected isParameterValue( | ||
174 | SMTTerm term, | ||
175 | Map<SMTSortedVariable,Object> substitution) | ||
176 | { | ||
177 | if(term instanceof SMTSymbolicValue) { | ||
178 | return substitution.containsKey((term as SMTSymbolicValue).symbolicReference) | ||
179 | } | ||
180 | else return false | ||
181 | } | ||
182 | def protected Object resolveParameterValue( | ||
183 | SMTTerm term, | ||
184 | Map<SMTSortedVariable,Object> substitution) | ||
185 | { | ||
186 | return substitution.get((term as SMTSymbolicValue).symbolicReference); | ||
187 | } | ||
188 | |||
189 | def protected isITE( | ||
190 | SMTTerm term, | ||
191 | Map<SMTSortedVariable,Object> substitution) | ||
192 | { | ||
193 | return term instanceof SMTITE; | ||
194 | } | ||
195 | def protected resolveITE( | ||
196 | SMTTerm term, | ||
197 | Map<SMTSortedVariable,Object> substitution) | ||
198 | { | ||
199 | val ite = term as SMTITE | ||
200 | val condition = ite.condition.resolveValue(substitution) as Boolean | ||
201 | |||
202 | if(condition){ | ||
203 | return resolveValue(ite.^if,substitution) | ||
204 | }else{ | ||
205 | return resolveValue(ite.^else,substitution) | ||
206 | } | ||
207 | } | ||
208 | |||
209 | def protected isAnd(SMTTerm term, Map<SMTSortedVariable,Object> substitution) { | ||
210 | term instanceof SMTAnd | ||
211 | } | ||
212 | def protected resolveAnd(SMTTerm term, Map<SMTSortedVariable,Object> substitution) { | ||
213 | val and = term as SMTAnd | ||
214 | for(operand : and.operands) { | ||
215 | val operandValue = operand.resolveValue(substitution) as Boolean | ||
216 | if(!operandValue) return false | ||
217 | } | ||
218 | return true | ||
219 | } | ||
220 | |||
221 | def protected isEquals( | ||
222 | SMTTerm operand, | ||
223 | Map<SMTSortedVariable,Object> substitution) | ||
224 | { | ||
225 | return operand instanceof SMTEquals | ||
226 | } | ||
227 | def protected resolveEquals(SMTTerm term, Map<SMTSortedVariable,Object> substitution){ | ||
228 | val equals = term as SMTEquals | ||
229 | val left = equals.leftOperand.resolveValue(substitution) | ||
230 | val right = equals.rightOperand.resolveValue(substitution) | ||
231 | val res = left.equals(right) | ||
232 | return res | ||
233 | } | ||
234 | |||
235 | def protected isFiniteElementReference(SMTTerm term, Map<SMTSortedVariable,Object> substitution) { | ||
236 | if(term instanceof SMTSymbolicValue) { | ||
237 | if((term as SMTSymbolicValue).symbolicReference instanceof SMTEnumLiteral) { | ||
238 | return true | ||
239 | } | ||
240 | } | ||
241 | return false; | ||
242 | } | ||
243 | def protected resolveFiniteElementReference(SMTTerm term, Map<SMTSortedVariable,Object> substitution) { | ||
244 | (term as SMTSymbolicValue).symbolicReference | ||
245 | } | ||
246 | |||
247 | def protected isFunctionCall(SMTTerm term, Map<SMTSortedVariable,Object> substitution) { | ||
248 | if(term instanceof SMTSymbolicValue) { | ||
249 | val functionCall = (term as SMTSymbolicValue).symbolicReference | ||
250 | return functionCall instanceof SMTFunctionDeclaration || functionCall instanceof SMTFunctionDefinition | ||
251 | } | ||
252 | return false; | ||
253 | } | ||
254 | def protected resolveFunctionCall(SMTTerm term, Map<SMTSortedVariable,Object> substitution) { | ||
255 | if(term.isTerminal(substitution)) | ||
256 | { | ||
257 | return term.resolveTerminal(substitution); | ||
258 | } | ||
259 | else{ | ||
260 | val functionCall = term as SMTSymbolicValue | ||
261 | var SMTFunctionDefinition calledFunction; | ||
262 | var SMTFunctionDeclaration calledDeclaration; | ||
263 | if(functionCall.symbolicReference instanceof SMTFunctionDeclaration) { | ||
264 | calledDeclaration = functionCall.symbolicReference as SMTFunctionDeclaration | ||
265 | calledFunction = functionCall.symbolicReference.lookup(functionDeclarationToDefinitions)} | ||
266 | else { | ||
267 | calledDeclaration = null; | ||
268 | calledFunction = functionCall.symbolicReference as SMTFunctionDefinition | ||
269 | } | ||
270 | |||
271 | val newSubstitution = new HashMap<SMTSortedVariable,Object> | ||
272 | if(! calledFunction.parameters.nullOrEmpty) { | ||
273 | for(i : 0..calledFunction.parameters.size-1) { | ||
274 | newSubstitution.put( | ||
275 | calledFunction.parameters.get(i), | ||
276 | functionCall.parameterSubstitutions.get(i).resolveValue(substitution) | ||
277 | ) | ||
278 | } | ||
279 | } | ||
280 | return calledFunction.resolveFunctionDefinition(newSubstitution) | ||
281 | } | ||
282 | } | ||
283 | |||
284 | def protected Object resolveValue( | ||
285 | SMTTerm value, | ||
286 | Map<SMTSortedVariable,Object> substitution) | ||
287 | { | ||
288 | if(value instanceof SMTSymbolicValue){ | ||
289 | (value as SMTSymbolicValue).symbolicReference | ||
290 | } | ||
291 | |||
292 | if(value.isTerminal(substitution)) { | ||
293 | return value.resolveTerminal(substitution) | ||
294 | }else if(value.isBoolLiteral(substitution)){ | ||
295 | return resolveBoolLiteral(value, substitution) | ||
296 | }else if(value.isIntLiteral(substitution)){ | ||
297 | return resolveIntLiteral(value, substitution) | ||
298 | }else if(value.isParameterValue(substitution)) { | ||
299 | return resolveParameterValue(value,substitution) | ||
300 | }else if(value.isITE(substitution)){ | ||
301 | return resolveITE(value, substitution) | ||
302 | }else if(value.isAnd(substitution)) { | ||
303 | return resolveAnd(value,substitution) | ||
304 | }else if(value.isEquals(substitution)) { | ||
305 | return resolveEquals(value,substitution) | ||
306 | }else if(value.isFiniteElementReference(substitution)) { | ||
307 | return resolveFiniteElementReference(value,substitution) | ||
308 | }else if(value.isFunctionCall(substitution)) { | ||
309 | return resolveFunctionCall(value,substitution) | ||
310 | }else{ | ||
311 | throw new IllegalArgumentException("Can not resolve this term: " + value) | ||
312 | } | ||
313 | } | ||
314 | } \ No newline at end of file | ||
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend new file mode 100644 index 00000000..38ae1dae --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend | |||
@@ -0,0 +1,64 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner.builder | ||
2 | |||
3 | import org.eclipse.emf.common.util.URI | ||
4 | import java.io.InputStream | ||
5 | import java.io.IOException | ||
6 | import java.io.FileWriter | ||
7 | import java.io.File | ||
8 | import java.io.BufferedReader | ||
9 | import java.io.InputStreamReader | ||
10 | import org.eclipse.emf.common.CommonPlugin | ||
11 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration | ||
12 | |||
13 | class SmtSolverException extends Exception{ | ||
14 | new(String s) { super(s) } | ||
15 | new(String s, Exception e) { super(s,e) } | ||
16 | } | ||
17 | |||
18 | class SmtSolverHandler { | ||
19 | public def callSolver(URI resourceURI, SmtSolverConfiguration configuration) { | ||
20 | val URI smtUri = CommonPlugin.resolve(resourceURI) | ||
21 | val File smtFile = new File(smtUri.toFileString()) | ||
22 | |||
23 | val params = | ||
24 | '''/smt2 /st« | ||
25 | IF configuration.runtimeLimit != SmtSolverConfiguration::Unlimited» /T:«configuration.runtimeLimit»«ENDIF»« | ||
26 | IF configuration.memoryLimit != SmtSolverConfiguration::Unlimited» /memory:«configuration.memoryLimit»«ENDIF»« | ||
27 | IF configuration.fixRandomSeed» /rs:0«ENDIF | ||
28 | » «smtFile.path»''' | ||
29 | |||
30 | val Runtime runTime = Runtime.getRuntime() | ||
31 | |||
32 | try { | ||
33 | val process = runTime.exec(configuration.solverPath + " " + params) | ||
34 | |||
35 | val FileWriter writer = new FileWriter(smtFile,true) | ||
36 | writer.append("\n--------------\n") | ||
37 | appendStream(writer, process.getInputStream()) | ||
38 | printStream(process.getErrorStream()) | ||
39 | writer.close | ||
40 | } catch (IOException e) { | ||
41 | throw new SmtSolverException( | ||
42 | "Error during the input/output handling of the reasoner.", e) | ||
43 | } | ||
44 | |||
45 | return resourceURI | ||
46 | } | ||
47 | |||
48 | def private void printStream(InputStream inputStream) throws IOException { | ||
49 | val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream)) | ||
50 | var int line = -1 | ||
51 | while ((line = input.read()) != -1) { | ||
52 | System.out.print(line as char) | ||
53 | } | ||
54 | input.close() | ||
55 | } | ||
56 | |||
57 | def private appendStream(FileWriter writer, InputStream inputStream) throws IOException { | ||
58 | val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream)) | ||
59 | var int line = -1 | ||
60 | while ((line = input.read()) != -1) { | ||
61 | writer.append(line as char) | ||
62 | } | ||
63 | } | ||
64 | } \ No newline at end of file | ||