diff options
| author |  OszkarSemerath <oszkar.semerath@gmail.com> | 2018-05-05 17:51:10 +0200 |
|---|---|---|
| committer | OszkarSemerath <oszkar.semerath@gmail.com> | 2018-05-05 17:51:10 +0200 |
| commit | d33b37e90d55dfa526cd8aebcf8057b693344f31 (patch) | |
| tree | ed932823e2200730685320e6e86c5e081f0210e8 | |
| parent | Removed unused projects (diff) | |
| download | VIATRA-Generator-d33b37e90d55dfa526cd8aebcf8057b693344f31.tar.gz VIATRA-Generator-d33b37e90d55dfa526cd8aebcf8057b693344f31.tar.zst VIATRA-Generator-d33b37e90d55dfa526cd8aebcf8057b693344f31.zip | |
containment mapping fix
| -rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend | 123 |
1 files changed, 65 insertions, 58 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 ec1502e5..6f20b956 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 | |||
| @@ -1027,68 +1027,75 @@ class Logic2SmtMapper{ | |||
| 1027 | val a1 = Assertion(Forall[ | 1027 | val a1 = Assertion(Forall[ |
| 1028 | val r1 = addVar(root.key) | 1028 | val r1 = addVar(root.key) |
| 1029 | val r2 = addVar(root.key) | 1029 | val r2 = addVar(root.key) |
| 1030 | (root.value.call(r1) && root.value.call(r2)) => (r1 == r2) | 1030 | return (root.value.call(r1) && root.value.call(r2)) => (r1 == r2) |
| 1031 | ]) | 1031 | ]) |
| 1032 | document.assertions+=this.transformAssertion(a1,trace) | 1032 | document.assertions+=this.transformAssertion(a1,trace) |
| 1033 | } | 1033 | } |
| 1034 | |||
| 1034 | // only one of the root entries is true | 1035 | // only one of the root entries is true |
| 1035 | // val a2 = Assertion( | 1036 | val a2 = Assertion( |
| 1036 | // rootRelations.entrySet.map[selected| | 1037 | Or(rootRelations.entrySet.map[selected| |
| 1037 | // rootRelations.entrySet.map[other| | 1038 | And(rootRelations.entrySet.map[other| |
| 1038 | // if(selected == other) { | 1039 | val isSupertype = selected.key.transitiveClosurePlus[return supertypes].contains(other) |
| 1039 | // Exists[ | 1040 | val type = other.key |
| 1040 | // val r = addVar(other.key) | 1041 | val relation = other.value |
| 1041 | // other.value.call(r) | 1042 | if(selected == other) { |
| 1042 | // ] | 1043 | return Exists[ |
| 1043 | // } else { | 1044 | val r = addVar(type) |
| 1044 | // Forall[ | 1045 | val x = addVar(LogicInt) |
| 1045 | // val r = addVar(other.key) | 1046 | return relation.call(r) |
| 1046 | // !other.value.call(r) | 1047 | ] |
| 1047 | // ] | 1048 | }else if(isSupertype) { |
| 1048 | // } | 1049 | return true.asTerm |
| 1049 | // ].And | 1050 | }else { |
| 1050 | // ].Or | 1051 | return Forall[ |
| 1051 | // ) | 1052 | val r = addVar(other.key) |
| 1052 | // document.assertions+=this.transformAssertion(a2,trace) | 1053 | !other.value.call(r) |
| 1053 | // // the root has no parent | 1054 | ] |
| 1054 | // for(root : rootRelations.entrySet) { | 1055 | } |
| 1055 | // val parentRelations = root.key.lookup(possibleParentRelations) | 1056 | ]) |
| 1056 | // val a3 = Assertion(Forall[ | 1057 | ]) |
| 1057 | // val r = addVar(root.key) | 1058 | ) |
| 1058 | // root.value.call(r) => parentRelations.map[containment | | 1059 | document.assertions+=this.transformAssertion(a2,trace) |
| 1059 | // Forall[ | 1060 | // the root has no parent |
| 1060 | // val container = addVar(containment.parameters.get(0)) | 1061 | for(root : rootRelations.entrySet) { |
| 1061 | // !containment.call(container,r) | 1062 | val parentRelations = root.key.lookup(possibleParentRelations) |
| 1062 | // ] | 1063 | val a3 = Assertion(Forall[ |
| 1063 | // ].And | 1064 | val r = addVar(root.key) |
| 1064 | // ]) | 1065 | root.value.call(r) => parentRelations.map[containment | |
| 1065 | // document.assertions+=this.transformAssertion(a3,trace) | 1066 | Forall[ |
| 1066 | // } | 1067 | val container = addVar(containment.parameters.get(0)) |
| 1067 | // // no element has two parents | 1068 | !containment.call(container,r) |
| 1068 | // for(root : rootRelations.entrySet) { | 1069 | ] |
| 1069 | // val parentRelations = root.key.lookup(possibleParentRelations) | 1070 | ].And |
| 1070 | // val a4 = Assertion(Forall[ | 1071 | ]) |
| 1071 | // val element = addVar(root.key) | 1072 | document.assertions+=this.transformAssertion(a3,trace) |
| 1072 | // parentRelations.map[selected | | 1073 | } |
| 1073 | // Forall[ | 1074 | // no element has two parents |
| 1074 | // val container = addVar(selected.parameters.get(0)) | 1075 | for(root : rootRelations.entrySet) { |
| 1075 | // selected.call(container,element) => ( | 1076 | val parentRelations = root.key.lookup(possibleParentRelations) |
| 1076 | // Forall[ | 1077 | val a4 = Assertion(Forall[ |
| 1077 | // val other = addVar(selected.parameters.get(0)) | 1078 | val element = addVar(root.key) |
| 1078 | // (!selected.call(other,element)) || (other == element) | 1079 | parentRelations.map[selected | |
| 1079 | // ] && | 1080 | Forall[ |
| 1080 | // parentRelations.filter[it !==selected].map[otherContainment | | 1081 | val container = addVar(selected.parameters.get(0)) |
| 1081 | // Forall[ | 1082 | selected.call(container,element) => ( |
| 1082 | // val other = addVar(otherContainment.parameters.get(0)) | 1083 | Forall[ |
| 1083 | // otherContainment.call(other,element) | 1084 | val other = addVar(selected.parameters.get(0)) |
| 1084 | // ] | 1085 | (!selected.call(other,element)) || (other == element) |
| 1085 | // ].And) | 1086 | ] && |
| 1086 | // | 1087 | parentRelations.filter[it !==selected].map[otherContainment | |
| 1087 | // ] | 1088 | Forall[ |
| 1088 | // ].And | 1089 | val other = addVar(otherContainment.parameters.get(0)) |
| 1089 | // ]) | 1090 | otherContainment.call(other,element) |
| 1090 | // document.assertions+=this.transformAssertion(a4,trace) | 1091 | ] |
| 1091 | // } | 1092 | ].And) |
| 1093 | |||
| 1094 | ] | ||
| 1095 | ].And | ||
| 1096 | ]) | ||
| 1097 | document.assertions+=this.transformAssertion(a4,trace) | ||
| 1098 | } | ||
| 1092 | 1099 | ||
| 1093 | // an element is not root, then it has a container | 1100 | // an element is not root, then it has a container |
| 1094 | for(root : rootRelations.entrySet) { | 1101 | for(root : rootRelations.entrySet) { |