diff options
author | 2018-05-05 17:51:10 +0200 | |
---|---|---|
committer | 2018-05-05 17:51:10 +0200 | |
commit | d33b37e90d55dfa526cd8aebcf8057b693344f31 (patch) | |
tree | ed932823e2200730685320e6e86c5e081f0210e8 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src | |
parent | Removed unused projects (diff) | |
download | VIATRA-Generator-d33b37e90d55dfa526cd8aebcf8057b693344f31.tar.gz VIATRA-Generator-d33b37e90d55dfa526cd8aebcf8057b693344f31.tar.zst VIATRA-Generator-d33b37e90d55dfa526cd8aebcf8057b693344f31.zip |
containment mapping fix
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src')
-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) { |