aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszkar.semerath@gmail.com>2018-03-07 12:48:01 -0500
committerLibravatar OszkarSemerath <oszkar.semerath@gmail.com>2018-03-07 12:48:01 -0500
commit5ac36bba74bcf71224d4895cccdae253b07ccbc9 (patch)
tree85a15ac3d720c24021c9126dc6e00e653135a9b5
parentremoved unnecessary println (diff)
downloadVIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.tar.gz
VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.tar.zst
VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.zip
Rebooting Z3 solver Containment vs Inheritance still has a bug
Diffstat
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend2
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend315
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend129
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_44
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend3
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend8
6 files changed, 437 insertions, 64 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
index 44708f44..e7f35626 100644
--- 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
@@ -23,7 +23,7 @@ class Logic2SMT_TypeMapperInterpretation {
23 } 23 }
24 24
25 public def getElements(Type type) { 25 public def getElements(Type type) {
26 return type2Elements.get(type) 26 return type.lookup(this.type2Elements)
27 } 27 }
28 28
29 public def ValueType logicElement2Smt(DefinedElement element) { 29 public def ValueType logicElement2Smt(DefinedElement element) {
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
index aad43716..ec1502e5 100644
--- 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
@@ -1,5 +1,6 @@
1package hu.bme.mit.inf.dslreasoner.smt.reasoner 1package hu.bme.mit.inf.dslreasoner.smt.reasoner
2 2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput 4import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
4import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes 5import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
@@ -42,13 +43,17 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
42import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition 43import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
43import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue 44import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
44import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term 45import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
46import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
45import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable 47import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
48import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
46import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 49import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
47import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd 50import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd
48import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion 51import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion
49import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference 52import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference
50import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference 53import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
51import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument 54import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
55import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
56import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
52import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput 57import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
53import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference 58import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference
54import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr 59import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr
@@ -60,6 +65,7 @@ import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
60import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm 65import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
61import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType 66import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType
62import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory 67import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
68import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil
63import java.util.ArrayList 69import java.util.ArrayList
64import java.util.HashMap 70import java.util.HashMap
65import java.util.LinkedHashMap 71import java.util.LinkedHashMap
@@ -72,18 +78,14 @@ import org.eclipse.xtend.lib.annotations.Accessors
72import org.eclipse.xtext.xbase.lib.Functions.Function0 78import org.eclipse.xtext.xbase.lib.Functions.Function0
73import org.eclipse.xtext.xbase.lib.Functions.Function1 79import org.eclipse.xtext.xbase.lib.Functions.Function1
74import org.eclipse.xtext.xbase.lib.Functions.Function2 80import org.eclipse.xtext.xbase.lib.Functions.Function2
81
75import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 82import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
76import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
77import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
78import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
79 83
80class Logic2SmtMapper{ 84class Logic2SmtMapper{
81 val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE 85 val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
82 val Logic2SmtMapper_UnfoldingSupport unfolder = new Logic2SmtMapper_UnfoldingSupport 86 val Logic2SmtMapper_UnfoldingSupport unfolder = new Logic2SmtMapper_UnfoldingSupport
83 @Accessors val Logic2Smt_TypeMapper typeMapper; 87 @Accessors val Logic2Smt_TypeMapper typeMapper;
84 88
85 LogicProblemBuilder b
86
87 new(Logic2Smt_TypeMapper typeMapper) { 89 new(Logic2Smt_TypeMapper typeMapper) {
88 this.typeMapper = typeMapper 90 this.typeMapper = typeMapper
89 } 91 }
@@ -109,11 +111,16 @@ class Logic2SmtMapper{
109 111
110 problem.relations.filter(RelationDefinition).forEach[it.transformRelationDefinition_definition(documentInput,trace)] 112 problem.relations.filter(RelationDefinition).forEach[it.transformRelationDefinition_definition(documentInput,trace)]
111 documentInput.assertions += problem.assertions.map[transformAssertion(trace)] 113 documentInput.assertions += problem.assertions.map[transformAssertion(trace)]
114
115 if(!problem.containmentHierarchies.empty) {
116 transformContainmentV1(documentInput,problem.containmentHierarchies.head,trace)
117 }
112 // End trafo 118 // End trafo
113 119
114 document.input.assertions.forEach[it.value.nameAllUnnamedVariable] 120 document.input.assertions.forEach[it.value.nameAllUnnamedVariable]
115 document.input.functionDefinition.forEach[it.value.nameAllUnnamedVariable] 121 document.input.functionDefinition.forEach[it.value.nameAllUnnamedVariable]
116 document.cleanDocument 122 document.cleanDocument
123 document.orderDefinitions
117 return new TracedOutput(document,trace) 124 return new TracedOutput(document,trace)
118 } 125 }
119 126
@@ -1000,15 +1007,269 @@ class Logic2SmtMapper{
1000 1007
1001 /////////// 1008 ///////////
1002 1009
1003 /*def transformContainment(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) { 1010 def transformContainmentV1(SMTInput document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) {
1004 val containmentRelation_oo = createSMTFunctionDefinition=>[ 1011 val extension builder = new LogicProblemBuilder
1005 it.name="containment!oo" 1012 val types = h.typesOrderedInHierarchy
1006 it.range=createSMTBoolTypeReference 1013
1007 val child = createSMTSortedVariable => [ 1014 val rootRelations = new HashMap<Type,Relation>
1008 it.name = 1015 for(type: types) {
1016 val rootRelation = RelationDeclaration('''Root «type.name»''',type)
1017 rootRelations.put(type,rootRelation)
1018 this.transformRelationDeclaration(rootRelation,document,trace)
1019 }
1020 val possibleParentRelations = types.toInvertedMap[type|
1021 h.containmentRelations.filter[it.parameters.get(1) === type]
1022 //TODO inheritance
1023 ]
1024
1025 // root is true only for at most one element in every root type
1026 for(root: rootRelations.entrySet) {
1027 val a1 = Assertion(Forall[
1028 val r1 = addVar(root.key)
1029 val r2 = addVar(root.key)
1030 (root.value.call(r1) && root.value.call(r2)) => (r1 == r2)
1031 ])
1032 document.assertions+=this.transformAssertion(a1,trace)
1033 }
1034 // only one of the root entries is true
1035// val a2 = Assertion(
1036// rootRelations.entrySet.map[selected|
1037// rootRelations.entrySet.map[other|
1038// if(selected == other) {
1039// Exists[
1040// val r = addVar(other.key)
1041// other.value.call(r)
1042// ]
1043// } else {
1044// Forall[
1045// val r = addVar(other.key)
1046// !other.value.call(r)
1047// ]
1048// }
1049// ].And
1050// ].Or
1051// )
1052// document.assertions+=this.transformAssertion(a2,trace)
1053// // the root has no parent
1054// for(root : rootRelations.entrySet) {
1055// val parentRelations = root.key.lookup(possibleParentRelations)
1056// val a3 = Assertion(Forall[
1057// val r = addVar(root.key)
1058// root.value.call(r) => parentRelations.map[containment |
1059// Forall[
1060// val container = addVar(containment.parameters.get(0))
1061// !containment.call(container,r)
1062// ]
1063// ].And
1064// ])
1065// document.assertions+=this.transformAssertion(a3,trace)
1066// }
1067// // no element has two parents
1068// for(root : rootRelations.entrySet) {
1069// val parentRelations = root.key.lookup(possibleParentRelations)
1070// val a4 = Assertion(Forall[
1071// val element = addVar(root.key)
1072// parentRelations.map[selected |
1073// Forall[
1074// val container = addVar(selected.parameters.get(0))
1075// selected.call(container,element) => (
1076// Forall[
1077// val other = addVar(selected.parameters.get(0))
1078// (!selected.call(other,element)) || (other == element)
1079// ] &&
1080// parentRelations.filter[it !==selected].map[otherContainment |
1081// Forall[
1082// val other = addVar(otherContainment.parameters.get(0))
1083// otherContainment.call(other,element)
1084// ]
1085// ].And)
1086//
1087// ]
1088// ].And
1089// ])
1090// document.assertions+=this.transformAssertion(a4,trace)
1091// }
1092
1093 // an element is not root, then it has a container
1094 for(root : rootRelations.entrySet) {
1095 val parentRelations = root.key.lookup(possibleParentRelations)
1096 val a5 = Assertion(Forall[
1097 val element = addVar(root.key)
1098 !root.value.call(element) =>
1099 parentRelations.map[selected |
1100 Exists[
1101 val container = addVar(selected.parameters.get(0))
1102 selected.call(container,element)
1103 ]
1104 ].Or
1105 ])
1106 document.assertions+=this.transformAssertion(a5,trace)
1107 }
1108//
1109// // no circle in containment
1110// for(length : 1..5) {
1111// val paths = h.containmentRelations.paths(length)
1112// val loopPaths = paths.filter[path|
1113// val first = (path.head.parameters.get(0) as ComplexTypeReference).referred
1114// val last = (path.last.parameters.get(1) as ComplexTypeReference).referred
1115// hasCommonElement(first,last)
1116// ]
1117// for(loopPath : loopPaths) {
1118// val variableIndexes = 0..<length
1119// val a6 = Assertion(!Exists[e|
1120// val variables = new ArrayList
1121// for(variableIndex : variableIndexes) {
1122// variables += e.addVar('''c«variableIndex»''',(loopPath.get(variableIndex).parameters.get(0) as ComplexTypeReference).referred)
1123// }
1124// val pathElements = new ArrayList
1125// for(variableIndex : variableIndexes) {
1126// val from = variableIndex
1127// val to = variableIndex+1
1128// if(variableIndexes.contains(to)) {
1129// pathElements += loopPath.get(variableIndex).call(variables.get(from),variables.get(to))
1130// }
1131// }
1132// pathElements += loopPath.last.call(variables.last,variables.head)
1133//
1134// pathElements.And
1135// ])
1136// document.assertions+=this.transformAssertion(a6,trace)
1137// }
1138// }
1139// }
1140//
1141// def private Iterable<List<Relation>> paths(Iterable<Relation> relations, int length) {
1142// if(length == 0) {
1143// return #[]
1144// } else if(length == 1) {
1145// return relations.map[#[it]]
1146// } else {
1147// val previous = paths(relations,length-1)
1148// val List<List<Relation>> res = new ArrayList(previous.size*relations.size)
1149// for(p:previous) {
1150// for(r:relations) {
1151// val lastType = (p.last.parameters.get(1) as ComplexTypeReference).referred
1152// val firstType = (r.parameters.get(0) as ComplexTypeReference).referred
1153// val hasCommonElement = hasCommonElement(lastType, firstType)
1154// if(hasCommonElement) {
1155// res.add(new ArrayList(p) => [add(r)])
1156// }
1157// }
1158// }
1159// return res
1160// }
1161 }
1162
1163 protected def boolean hasCommonElement(Type lastType, Type firstType) {
1164 val a = lastType.transitiveClosureStar[subtypes]
1165 val b = firstType.transitiveClosureStar[subtypes]
1166 return a.exists[b.contains(it)]
1167 }
1168
1169 def transformContainmentV2(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) {
1170 val typeConstraintsOfTypesInContainment = h.typesOrderedInHierarchy
1171 .map[typeMapper.transformTypeReference(it,trace)].flatten
1172 val relationsOfTypeConstraints = h.containmentRelations.map[it]
1173 val typesOfTypeConstraints = typeConstraintsOfTypesInContainment
1174 .map[(it.type as SMTComplexTypeReference).referred]
1175 .toSet
1176
1177 // Root declaration
1178 val rootRelations = new HashMap<SMTType,SMTFunctionDeclaration>
1179 for(t : typesOfTypeConstraints) {
1180 val rootRelation = createSMTFunctionDeclaration => [
1181 it.name = toID('''root «t.name»''')
1182 it.range = createSMTBoolTypeReference
1183 it.parameters += createSMTComplexTypeReference => [
1184 it.referred = t
1185 ]
1186 ]
1187 document.input.functionDeclarations += rootRelation
1188 rootRelations.put(t,rootRelation)
1189 }
1190 // root is true only for one element in every root type
1191 for(entry : rootRelations.entrySet) {
1192 document.input.assertions += createSMTAssertion => [
1193 it.value = createSMTForall => [
1194 val r1 = createSMTSortedVariable => [
1195 it.name = "r1"
1196 it.range = createSMTComplexTypeReference => [it.referred = entry.key]
1197 ]
1198 val r2 = createSMTSortedVariable => [
1199 it.name = "r2"
1200 it.range = createSMTComplexTypeReference => [it.referred = entry.key]
1201 ]
1202
1203 it.quantifiedVariables += r1
1204 it.quantifiedVariables += r2
1205
1206 it.expression = createSMTImpl => [
1207 it.leftOperand = createSMTAnd => [
1208 it.operands += createSMTSymbolicValue => [
1209 it.symbolicReference = entry.value
1210 it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r1]
1211 ]
1212 it.operands += createSMTSymbolicValue => [
1213 it.symbolicReference = entry.value
1214 it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r2]
1215 ]
1216 ]
1217 it.rightOperand = createSMTEquals => [
1218 it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = r1]
1219 it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = r2]
1220 ]
1221 ]
1222 ]
1223 ]
1224 }
1225 // only one of the root entries is true
1226 document.input.assertions += createSMTAssertion => [
1227 it.value = createSMTOr =>[or |
1228 for(selectedCombination : rootRelations.entrySet) {
1229 or.operands += createSMTAnd => [and |
1230 for(otherCombination : rootRelations.entrySet) {
1231 if(selectedCombination == otherCombination) {
1232 and.operands += createSMTExists => [
1233 val r = createSMTSortedVariable => [
1234 it.name = "r"
1235 it.range = createSMTComplexTypeReference => [it.referred = otherCombination.key]
1236 ]
1237 it.quantifiedVariables += r
1238 it.expression = createSMTSymbolicValue => [
1239 it.symbolicReference = otherCombination.value
1240 it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r]
1241 ]
1242 ]
1243 } else {
1244 and.operands += createSMTForall => [
1245 val r = createSMTSortedVariable => [
1246 it.name = "r"
1247 it.range = createSMTComplexTypeReference => [it.referred = otherCombination.key]
1248 ]
1249 it.quantifiedVariables += r
1250 it.expression = createSMTNot=> [
1251 it.operand = createSMTSymbolicValue => [
1252 it.symbolicReference = otherCombination.value
1253 it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r]
1254 ]
1255 ]
1256 ]
1257 }
1258 }
1259 ]
1260 }
1009 ] 1261 ]
1010 ] 1262 ]
1011 }*/ 1263
1264 // the root has no parent
1265 throw new UnsupportedOperationException('''Unfinished version''')
1266
1267 // no element has two parents
1268
1269 // an element is either root or has parent
1270
1271 // no circle in containment
1272 }
1012 1273
1013 /////////// 1274 ///////////
1014 1275
@@ -1052,4 +1313,34 @@ class Logic2SmtMapper{
1052 def private dispatch replaceWith(EObject object) { 1313 def private dispatch replaceWith(EObject object) {
1053 null 1314 null
1054 } 1315 }
1316
1317 def orderDefinitions(SMTDocument document) {
1318 val definitionsInDocument = document.input.functionDefinition
1319 val List<SMTFunctionDefinition> definitionsInOrder = new ArrayList(definitionsInDocument.size)
1320 while(!definitionsInDocument.empty) {
1321 val selection = definitionsInDocument.selectOneUnreferenced
1322 definitionsInOrder.add(selection)
1323 definitionsInDocument.remove(selection)
1324 }
1325 document.input.functionDefinition.addAll(definitionsInOrder)
1326 }
1327
1328 def referencedDefinitions(SMTFunctionDefinition definition) {
1329 definition
1330 .eAllContents
1331 .filter(SMTSymbolicValue)
1332 .map[it.symbolicReference]
1333 .filter(SMTFunctionDefinition)
1334 .toList
1335 }
1336
1337 def selectOneUnreferenced(List<SMTFunctionDefinition> definitions) {
1338 for(definition : definitions) {
1339 val references = definition.referencedDefinitions
1340 if(references.forall[!definitions.contains(it)]) {
1341 return definition
1342 }
1343 }
1344 throw new AssertionError('''Recursion in function definitions! definitions: «definitions.map[name].toList»''')
1345 }
1055} \ No newline at end of file 1346} \ 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
index c9bafa6c..2796e077 100644
--- 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
@@ -27,8 +27,10 @@ import java.util.HashMap
27import java.util.LinkedList 27import java.util.LinkedList
28import java.util.List 28import java.util.List
29import java.util.Map 29import java.util.Map
30import org.eclipse.emf.ecore.EObject
30import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine 31import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
31import org.eclipse.viatra.query.runtime.emf.EMFScope 32import org.eclipse.viatra.query.runtime.emf.EMFScope
33import org.eclipse.xtext.EcoreUtil2
32import org.eclipse.xtext.xbase.lib.Functions.Function0 34import org.eclipse.xtext.xbase.lib.Functions.Function0
33import org.eclipse.xtext.xbase.lib.Functions.Function1 35import org.eclipse.xtext.xbase.lib.Functions.Function1
34 36
@@ -63,32 +65,77 @@ class Logic2Smt_TypeMapperTrace_FilteredTypes implements Logic2Smt_TypeMapperTra
63 val a = this 65 val a = this
64 val b = new Logic2Smt_TypeMapperTrace_FilteredTypes 66 val b = new Logic2Smt_TypeMapperTrace_FilteredTypes
65 67
66 b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name]) 68 b.independentClasses = copyMap(a.independentClasses,newModel.typeDeclarations,[name])
67 69 b.independentClasses.values.validate(newModel)
68 b.newObjects = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head 70 b.newObjects = newModel.typeDeclarations.copyValue(a.newObjects,[name])
69 b.oldObjects = newModel.typeDeclarations.filter[it.name == a.oldObjects.name].head as SMTEnumeratedTypeDeclaration 71 b.newObjects.validate(newModel)
70 b.elementMap = a.elementMap.copyMap(b.oldObjects.elements,[name]) 72 b.oldObjects = newModel.typeDeclarations.copyValue(a.oldObjects,[name]) as SMTEnumeratedTypeDeclaration
73 b.oldObjects.validate(newModel)
74 b.elementMap = a.elementMap.copyMap(
75 newModel.typeDeclarations
76 .filter(SMTEnumeratedTypeDeclaration)
77 .map[it.elements]
78 .flatten,
79 [name]
80 )
81 b.elementMap.values.validate(newModel)
71 82
72 b.oldObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head as SMTEnumeratedTypeDeclaration 83 b.oldObjectTypes = newModel.typeDeclarations.copyValue(a.newObjects,[name]) as SMTEnumeratedTypeDeclaration
84 b.oldObjectTypes.validate(newModel)
73 b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name]) 85 b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name])
74 b.oldObjectTypeFunction = newModel.functionDefinition.filter[it.name == a.oldObjectTypeFunction.name].head 86 b.oldObjectTypeMap.values.validate(newModel)
87 b.oldObjectTypeFunction = newModel.functionDefinition.copyValue(a.oldObjectTypeFunction,[name])
88 b.oldObjectTypeFunction.validate(newModel)
75 b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) 89 b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name])
90 b.oldObjectTypePredicates.values.validate(newModel)
76 91
77 b.newObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjectTypes.name].head as SMTEnumeratedTypeDeclaration 92 b.newObjectTypes = newModel.typeDeclarations.copyValue(a.newObjectTypes,[name]) as SMTEnumeratedTypeDeclaration
93 b.newObjectTypes.validate(newModel)
78 b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name]) 94 b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name])
79 b.newObjectTypeFunction = newModel.functionDeclarations.filter[it.name == a.newObjectTypeFunction.name].head 95 b.newObjectTypeMap.values.validate(newModel)
96 b.newObjectTypeFunction = newModel.functionDeclarations.copyValue(a.newObjectTypeFunction,[name])
97 b.newObjectTypeFunction.validate(newModel)
80 b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) 98 b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name])
81 99 b.newObjectTypePredicates.values.validate(newModel)
82 return b 100 return b
83 } 101 }
102
103 def public static <Type, ValueType> copyValue(Iterable<? extends Type> collection, Type target, Function1<Type,ValueType> extractor) {
104 if(target===null) {
105 return null
106 } else {
107 val targetValue = extractor.apply(target)
108 val res = collection.filter[extractor.apply(it)==targetValue].head
109 return res
110 }
111 }
112
113 def validate(EObject element, EObject other) {
114 if(element != null) {
115 val headOfElement = EcoreUtil2.getContainerOfType(element,SMTDocument)
116 val expectedHeadOfElement = EcoreUtil2.getContainerOfType(other,SMTDocument)
117 if(headOfElement !== expectedHeadOfElement) {
118 throw new AssertionError('''
119 Element in different resource: «element»
120 Expected root: «expectedHeadOfElement»
121 Found root: «headOfElement»''')
122 }
123 }
124 }
125 def validate(Iterable<? extends EObject> iterable, EObject root) {
126 if(iterable !== null)
127 for(element : iterable) {
128 element.validate(root)
129 }
130 }
84} 131}
85 132
86class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { 133class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
87 val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE 134 val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
88 val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE 135 val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE
89 136
90 private def toID(List<String> names) {names.join("!") } 137 private def String toID(List<String> names) { names.map[split("\\s+").join("!")].join("!") }
91 private def toID(String name) {name.split("\\s+").toID} 138 private def String toID(String name) { name.split("\\s+").join("!")}
92 139
93 override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { 140 override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) {
94 val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes 141 val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes
@@ -105,7 +152,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
105 val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty 152 val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty
106 153
107 // 0. map the simple types 154 // 0. map the simple types
108 this.transformIndependentTypes(independentTypes,trace) 155 this.transformIndependentTypes(independentTypes,trace,document)
109 156
110 // 1. Has old elements => create supertype for it 157 // 1. Has old elements => create supertype for it
111 if(hasOldElements) { 158 if(hasOldElements) {
@@ -135,7 +182,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
135 return types.size == 1 && types.head.isIndependentType 182 return types.size == 1 && types.head.isIndependentType
136 } 183 }
137 184
138 protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace) { 185 protected def transformIndependentTypes(Iterable<TypeDefinition> types,Logic2SmtMapperTrace trace, SMTInput document) {
139 for(type: types) { 186 for(type: types) {
140 val independentSMTType = createSMTEnumeratedTypeDeclaration => [ 187 val independentSMTType = createSMTEnumeratedTypeDeclaration => [
141 name = toID(#["oldType",type.name]) 188 name = toID(#["oldType",type.name])
@@ -146,6 +193,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
146 independentSMTType.elements += enumLiteral 193 independentSMTType.elements += enumLiteral
147 trace.typeTrace.elementMap.put(element,enumLiteral) 194 trace.typeTrace.elementMap.put(element,enumLiteral)
148 } 195 }
196 document.typeDeclarations += independentSMTType
149 } 197 }
150 } 198 }
151 199
@@ -474,26 +522,45 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper {
474 val engine = ViatraQueryEngine.on(new EMFScope(problem)) 522 val engine = ViatraQueryEngine.on(new EMFScope(problem))
475 val supertypeStarMatcher = SupertypeStarMatcher.on(engine) 523 val supertypeStarMatcher = SupertypeStarMatcher.on(engine)
476 524
477 val type2Elements = (trace.typeTrace.oldObjectTypeMap.keySet + 525 val Map<Type,List<DefinedElement>> type2Elements = new HashMap
478 trace.typeTrace.newObjectTypeMap.keySet) 526 for(key : problem.types) {
479 .toInvertedMap[new LinkedList<DefinedElement>] 527 type2Elements.put(key,new LinkedList<DefinedElement>)
528 }
480 529
481 val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse 530 if(trace.typeTrace.independentClasses != null) {
482 for(oldElement: trace.typeTrace.elementMap.values) { 531 for(type : trace.typeTrace.independentClasses.keySet) {
483 val type = interpretation.queryEngine.resolveFunctionDefinition( 532 if(type instanceof TypeDefinition) {
484 trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral 533 type.lookup(type2Elements).addAll(type.elements)
485 val dynamicType = type.lookup(inverseOldTypeMap) 534 } else {
486 val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) 535 throw new AssertionError('''Independent classes are type definitions, but got: "«type»"''')
487 supertypes.forEach[type2Elements.get(it) += oldElement.lookup(smt2logic)] 536 }
537 }
488 } 538 }
489 539
490 val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse 540 if(trace.typeTrace.oldObjectTypeFunction != null) {
491 for(newElement: newElements.map[value as SMTSymbolicDeclaration]) { 541 val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse
492 val type = interpretation.queryEngine.resolveFunctionDeclaration( 542 for(oldElement: trace.typeTrace.elementMap.values) {
493 trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral 543 val type = interpretation.queryEngine.resolveFunctionDefinition(
494 val dynamicType = type.lookup(inverseNewTypeMap) 544 trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral
495 val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) 545 val dynamicType = type.lookup(inverseOldTypeMap)
496 supertypes.forEach[type2Elements.get(it) += newElement.lookup(smt2logic)] 546 val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)
547 for(superType : supertypes) {
548 superType.lookup(type2Elements) += oldElement.lookup(smt2logic)
549 }
550 }
551 }
552
553 if(trace.typeTrace.newObjectTypeFunction !== null) {
554 val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse
555 for(newElement: newElements.map[value as SMTSymbolicDeclaration]) {
556 val type = interpretation.queryEngine.resolveFunctionDeclaration(
557 trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral
558 val dynamicType = type.lookup(inverseNewTypeMap)
559 val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType)
560 for(superType : supertypes) {
561 superType.lookup(type2Elements) += newElement.lookup(smt2logic)
562 }
563 }
497 } 564 }
498 565
499 return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic) 566 return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic)
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_
index 79fc38e6..ceb7cc06 100644
--- 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_
@@ -1,24 +1,38 @@
1package hu.bme.mit.inf.dslreasoner.smt.reasoner 1package hu.bme.mit.inf.dslreasoner.smt.reasoner
2 2
3import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType 3import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
5import java.util.HashMap
6import java.util.Map
7import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
8import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
9import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral
10import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement 4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
12import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
13import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 9import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
14import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes 10import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher
11import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher
12import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
15import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument 13import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
14import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral
15import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration
16import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
17import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
18import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
19import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult
20import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSetTypeDeclaration
21import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration
22import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
23import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType
16import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory 24import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory 25import java.util.ArrayList
26import java.util.HashMap
27import java.util.LinkedList
18import java.util.List 28import java.util.List
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition 29import java.util.Map
20import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine 30import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
21import org.eclipse.viatra.query.runtime.emf.EMFScope 31import org.eclipse.viatra.query.runtime.emf.EMFScope
32import org.eclipse.xtext.xbase.lib.Functions.Function0
33import org.eclipse.xtext.xbase.lib.Functions.Function1
34
35import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
22 36
23class Logic2Smt_TypeMapperTrace_FilteredTypesSimple implements Logic2Smt_TypeMapperTrace{ 37class Logic2Smt_TypeMapperTrace_FilteredTypesSimple implements Logic2Smt_TypeMapperTrace{
24 public var Map<Type, SMTType> independentClasses = new HashMap 38 public var Map<Type, SMTType> independentClasses = new HashMap
@@ -58,8 +72,8 @@ class Logic2Smt_TypeMapper_FilteredTypesSimple implements Logic2Smt_TypeMapper{
58 val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE 72 val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
59 val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE 73 val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE
60 74
61 private def toID(List<String> names) {names.join("!") } 75 private def String toID(List<String> names) { names.map[split("\\s+").join("!")].join("!") }
62 private def toID(String name) {name.split("\\s+").toID} 76 private def String toID(String name) { name.split("\\s+").join("!")}
63 77
64 override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { 78 override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) {
65 val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes 79 val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes
@@ -80,7 +94,7 @@ class Logic2Smt_TypeMapper_FilteredTypesSimple implements Logic2Smt_TypeMapper{
80 this.transformUndefinedElements(scopes,trace,document) 94 this.transformUndefinedElements(scopes,trace,document)
81 95
82 96
83 this.transforTypes(connectedTypes, connectedElements, trace, document, engine) 97 this.transformType(connectedTypes, connectedElements, trace, document, engine)
84 // 3.2: Type definition to new elements 98 // 3.2: Type definition to new elements
85 if(hasNewElements) { 99 if(hasNewElements) {
86 this.transformNewTypes(connectedTypesWithoutDefintypesWithoutDefinedSupertype,trace,document,engine); 100 this.transformNewTypes(connectedTypesWithoutDefintypesWithoutDefinedSupertype,trace,document,engine);
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
index 4e2e1890..76b1ddbd 100644
--- 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
@@ -35,8 +35,7 @@ class SMTSolver extends LogicReasoner{
35 handler.callSolver(input,configuration) 35 handler.callSolver(input,configuration)
36 val solverTime = System.currentTimeMillis - solverTimeStart 36 val solverTime = System.currentTimeMillis - solverTimeStart
37 val outputModel = workspace.reloadModel(typeof(SMTDocument), "problem.smt2") 37 val outputModel = workspace.reloadModel(typeof(SMTDocument), "problem.smt2")
38 EcoreUtil.resolveAll(outputModel) 38 EcoreUtil.resolveAll(outputModel.eResource)
39 workspace.deactivateModel("problem.smt2")
40 return backMapper.transformOutput(problem,outputModel.output,trace, transformationTime, solverTime) 39 return backMapper.transformOutput(problem,outputModel.output,trace, transformationTime, solverTime)
41 } else throw new IllegalArgumentException('''The configuration have to be an «SmtSolverConfiguration.simpleName»!''') 40 } else throw new IllegalArgumentException('''The configuration have to be an «SmtSolverConfiguration.simpleName»!''')
42 } 41 }
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
index 38ae1dae..d2c54aaf 100644
--- 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
@@ -17,9 +17,12 @@ class SmtSolverException extends Exception{
17 17
18class SmtSolverHandler { 18class SmtSolverHandler {
19 public def callSolver(URI resourceURI, SmtSolverConfiguration configuration) { 19 public def callSolver(URI resourceURI, SmtSolverConfiguration configuration) {
20
20 val URI smtUri = CommonPlugin.resolve(resourceURI) 21 val URI smtUri = CommonPlugin.resolve(resourceURI)
21 val File smtFile = new File(smtUri.toFileString()) 22 val File smtFile = new File(smtUri.toFileString())
22 23
24 val path = configuration.solverPath
25 if(path===null) {throw new IllegalArgumentException('''Path to solver is not specified!''')}
23 val params = 26 val params =
24 '''/smt2 /st« 27 '''/smt2 /st«
25 IF configuration.runtimeLimit != SmtSolverConfiguration::Unlimited» /T:«configuration.runtimeLimit»«ENDIF»« 28 IF configuration.runtimeLimit != SmtSolverConfiguration::Unlimited» /T:«configuration.runtimeLimit»«ENDIF»«
@@ -28,9 +31,9 @@ class SmtSolverHandler {
28 » «smtFile.path»''' 31 » «smtFile.path»'''
29 32
30 val Runtime runTime = Runtime.getRuntime() 33 val Runtime runTime = Runtime.getRuntime()
31 34
32 try { 35 try {
33 val process = runTime.exec(configuration.solverPath + " " + params) 36 val process = runTime.exec(path + " " + params)
34 37
35 val FileWriter writer = new FileWriter(smtFile,true) 38 val FileWriter writer = new FileWriter(smtFile,true)
36 writer.append("\n--------------\n") 39 writer.append("\n--------------\n")
@@ -44,7 +47,6 @@ class SmtSolverHandler {
44 47
45 return resourceURI 48 return resourceURI
46 } 49 }
47
48 def private void printStream(InputStream inputStream) throws IOException { 50 def private void printStream(InputStream inputStream) throws IOException {
49 val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream)) 51 val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream))
50 var int line = -1 52 var int line = -1
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-05 06:03:22 +0000