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/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend | |
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/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend | 315 |
1 files changed, 303 insertions, 12 deletions
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 |