diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-08 03:00:08 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:10 -0400 |
commit | d0e4ffcc9dfc85367ccc73bf070404416081a477 (patch) | |
tree | 0db0134207f473f6a12d7c362512b008bd6449eb /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend | |
parent | VAMPIRE: Implement Vampire measurement code (diff) | |
download | VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.tar.gz VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.tar.zst VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.zip |
VAMPIRE: fix bug in transformation, further implement measurement code
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend | 49 |
1 files changed, 22 insertions, 27 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend index 181c59ca..efedf6dc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend | |||
@@ -23,7 +23,8 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
23 | this.base = base | 23 | this.base = base |
24 | } | 24 | } |
25 | 25 | ||
26 | def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) { | 26 | def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace, |
27 | Logic2VampireLanguageMapper mapper) { | ||
27 | 28 | ||
28 | // 1. store all variables in support wrt their name | 29 | // 1. store all variables in support wrt their name |
29 | // 1.1 if variable has type, creating list of type declarations | 30 | // 1.1 if variable has type, creating list of type declarations |
@@ -42,19 +43,18 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
42 | 43 | ||
43 | } | 44 | } |
44 | 45 | ||
45 | //deciding name of relation | 46 | // deciding name of relation |
46 | val nameArray = r.name.split(" ") | 47 | val nameArray = r.name.split(" ") |
47 | var relNameVar = "" | 48 | var relNameVar = "" |
48 | if (nameArray.length == 3) { | 49 | if (nameArray.length == 3) { |
49 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) | 50 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) |
50 | } | 51 | } else { |
51 | else { | ||
52 | relNameVar = r.name | 52 | relNameVar = r.name |
53 | } | 53 | } |
54 | val relName = relNameVar | 54 | val relName = relNameVar |
55 | 55 | ||
56 | val comply = createVLSFofFormula=> [ | 56 | val comply = createVLSFofFormula => [ |
57 | 57 | ||
58 | it.name = support.toIDMultiple("compliance", relName) | 58 | it.name = support.toIDMultiple("compliance", relName) |
59 | it.fofRole = "axiom" | 59 | it.fofRole = "axiom" |
60 | it.fofFormula = createVLSUniversalQuantifier => [ | 60 | it.fofFormula = createVLSUniversalQuantifier => [ |
@@ -79,10 +79,10 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
79 | trace.specification.formulas += comply | 79 | trace.specification.formulas += comply |
80 | } | 80 | } |
81 | 81 | ||
82 | def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) { | 82 | def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace, |
83 | 83 | Logic2VampireLanguageMapper mapper) { | |
84 | // println("XXXXXXXXXXXXXXXXX") | ||
85 | 84 | ||
85 | // println("XXXXXXXXXXXXXXXXX") | ||
86 | // 1. store all variables in support wrt their name | 86 | // 1. store all variables in support wrt their name |
87 | // 1.1 if variable has type, creating list of type declarations | 87 | // 1.1 if variable has type, creating list of type declarations |
88 | val Map<Variable, VLSVariable> relVar2VLS = new HashMap | 88 | val Map<Variable, VLSVariable> relVar2VLS = new HashMap |
@@ -102,34 +102,30 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
102 | 102 | ||
103 | } | 103 | } |
104 | 104 | ||
105 | //deciding name of relation | 105 | // deciding name of relation |
106 | val nameArray = r.name.split(" ") | 106 | val nameArray = r.name.split(" ") |
107 | var relNameVar = "" | 107 | var relNameVar = "" |
108 | if (nameArray.length == 3) { | 108 | if (nameArray.length == 3) { |
109 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) | 109 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) |
110 | } | 110 | } else { |
111 | else { | ||
112 | relNameVar = r.name | 111 | relNameVar = r.name |
113 | } | 112 | } |
114 | val relName = relNameVar | 113 | val relName = relNameVar |
115 | 114 | ||
116 | //define logic for pattern | 115 | // define logic for pattern |
117 | // val map = new HashMap | 116 | // val map = new HashMap |
118 | // map.put(r.variables.get(0), createVLSVariable) | 117 | // map.put(r.variables.get(0), createVLSVariable) |
119 | val definition = mapper.transformTerm(r.value, trace, relVar2VLS) | 118 | val definition = mapper.transformTerm(r.value, trace, relVar2VLS) |
120 | 119 | ||
121 | 120 | // get entire contents of and | |
122 | |||
123 | |||
124 | //get entire contents of and | ||
125 | val compliance = support.unfoldAnd(relVar2TypeDecComply) | 121 | val compliance = support.unfoldAnd(relVar2TypeDecComply) |
126 | val compDefn = createVLSAnd=> [ | 122 | val compDefn = createVLSAnd => [ |
127 | it.left = compliance | 123 | it.left = compliance |
128 | it.right = definition | 124 | it.right = definition |
129 | ] | 125 | ] |
130 | 126 | ||
131 | val relDef = createVLSFofFormula=> [ | 127 | val relDef = createVLSFofFormula => [ |
132 | 128 | ||
133 | it.name = support.toID(relName) | 129 | it.name = support.toID(relName) |
134 | it.fofRole = "axiom" | 130 | it.fofRole = "axiom" |
135 | it.fofFormula = createVLSUniversalQuantifier => [ | 131 | it.fofFormula = createVLSUniversalQuantifier => [ |
@@ -143,14 +139,13 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
143 | it.terms += support.duplicate(v) | 139 | it.terms += support.duplicate(v) |
144 | } | 140 | } |
145 | ] | 141 | ] |
146 | trace.relDef2Predicate.put(r, rel) | 142 | // trace.relDef2Predicate.put(r, rel) |
147 | trace.predicate2RelDef.put(rel, r) | 143 | // trace.predicate2RelDef.put(rel, r) |
148 | it.left = support.duplicate(rel) | 144 | it.left = support.duplicate(rel) |
149 | it.right = compDefn | 145 | it.right = compDefn |
150 | ] | 146 | ] |
151 | ] | 147 | ] |
152 | ] | 148 | ] |
153 | |||
154 | trace.specification.formulas += relDef | 149 | trace.specification.formulas += relDef |
155 | 150 | ||
156 | } | 151 | } |