diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder')
2 files changed, 378 insertions, 0 deletions
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 | ||