diff options
author | OszkarSemerath <oszkar.semerath@gmail.com> | 2018-03-07 12:48:01 -0500 |
---|---|---|
committer | OszkarSemerath <oszkar.semerath@gmail.com> | 2018-03-07 12:48:01 -0500 |
commit | 5ac36bba74bcf71224d4895cccdae253b07ccbc9 (patch) | |
tree | 85a15ac3d720c24021c9126dc6e00e653135a9b5 /Solvers | |
parent | removed unnecessary println (diff) | |
download | VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.tar.gz VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.tar.zst VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.zip |
Rebooting Z3 solver Containment vs Inheritance still has a bug
Diffstat (limited to 'Solvers')
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | 1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | 4 | 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.builder.TypeScopes |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And |
@@ -42,13 +43,17 @@ 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.RelationDefinition |
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | 44 | 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.Term |
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | 47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable |
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 49 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
47 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd | 50 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd |
48 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion | 51 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion |
49 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference | 52 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference |
50 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference | 53 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference |
51 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | 54 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument |
55 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration | ||
56 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition | ||
52 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | 57 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput |
53 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference | 58 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference |
54 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr | 59 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr |
@@ -60,6 +65,7 @@ import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue | |||
60 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm | 65 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm |
61 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType | 66 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType |
62 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | 67 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory |
68 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil | ||
63 | import java.util.ArrayList | 69 | import java.util.ArrayList |
64 | import java.util.HashMap | 70 | import java.util.HashMap |
65 | import java.util.LinkedHashMap | 71 | import java.util.LinkedHashMap |
@@ -72,18 +78,14 @@ import org.eclipse.xtend.lib.annotations.Accessors | |||
72 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | 78 | import org.eclipse.xtext.xbase.lib.Functions.Function0 |
73 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 79 | import org.eclipse.xtext.xbase.lib.Functions.Function1 |
74 | import org.eclipse.xtext.xbase.lib.Functions.Function2 | 80 | import org.eclipse.xtext.xbase.lib.Functions.Function2 |
81 | |||
75 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 82 | 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 | 83 | ||
80 | class Logic2SmtMapper{ | 84 | class 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 | |||
27 | import java.util.LinkedList | 27 | import java.util.LinkedList |
28 | import java.util.List | 28 | import java.util.List |
29 | import java.util.Map | 29 | import java.util.Map |
30 | import org.eclipse.emf.ecore.EObject | ||
30 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 31 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
31 | import org.eclipse.viatra.query.runtime.emf.EMFScope | 32 | import org.eclipse.viatra.query.runtime.emf.EMFScope |
33 | import org.eclipse.xtext.EcoreUtil2 | ||
32 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | 34 | import org.eclipse.xtext.xbase.lib.Functions.Function0 |
33 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 35 | import 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 | ||
86 | class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { | 133 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | 1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes |
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 | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
12 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 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 | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | 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 | ||
15 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | 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 | ||
16 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | 24 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | 25 | import java.util.ArrayList |
26 | import java.util.HashMap | ||
27 | import java.util.LinkedList | ||
18 | import java.util.List | 28 | import java.util.List |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 29 | import java.util.Map |
20 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 30 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
21 | import org.eclipse.viatra.query.runtime.emf.EMFScope | 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.* | ||
22 | 36 | ||
23 | class Logic2Smt_TypeMapperTrace_FilteredTypesSimple implements Logic2Smt_TypeMapperTrace{ | 37 | class 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 | ||
18 | class SmtSolverHandler { | 18 | class 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 |