aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend5
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend10
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend162
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend153
4 files changed, 155 insertions, 175 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
index ee802a99..1d56892e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -3,7 +3,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner
3import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup 3import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
4import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated 4import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper 5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes
7import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper 6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper
8import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler 7import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage 8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
@@ -14,6 +13,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
14import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 13import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
15import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult 14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
16import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 15import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
16import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper
17 17
18class VampireSolver extends LogicReasoner { 18class VampireSolver extends LogicReasoner {
19 19
@@ -23,8 +23,7 @@ class VampireSolver extends LogicReasoner {
23 VampireLanguageStandaloneSetup::doSetup() 23 VampireLanguageStandaloneSetup::doSetup()
24 } 24 }
25 25
26 val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper( 26 val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper
27 new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)
28 val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper 27 val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
29 val VampireHandler handler = new VampireHandler 28 val VampireHandler handler = new VampireHandler
30 29
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index 81af24e5..1dbc0055 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -51,11 +51,8 @@ class Logic2VampireLanguageMapper {
51 this) 51 this)
52 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper( 52 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(
53 this) 53 this)
54 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper 54 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper(
55 55 this)
56 public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) {
57 this.typeMapper = typeMapper
58 }
59 56
60 public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem, 57 public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem,
61 VampireSolverConfiguration config) { 58 VampireSolverConfiguration config) {
@@ -82,8 +79,7 @@ class Logic2VampireLanguageMapper {
82 79
83 // SCOPE MAPPER 80 // SCOPE MAPPER
84 scopeMapper.transformScope(config, trace) 81 scopeMapper.transformScope(config, trace)
85 82
86
87 trace.constantDefinitions = problem.collectConstantDefinitions 83 trace.constantDefinitions = problem.collectConstantDefinitions
88 trace.relationDefinitions = problem.collectRelationDefinitions 84 trace.relationDefinitions = problem.collectRelationDefinitions
89 85
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
index 1f071635..bc0b3e23 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
@@ -1,19 +1,157 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder 1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
2 2
3import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
4import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
11import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
12import java.util.ArrayList
5import java.util.Collection 13import java.util.Collection
6import java.util.List 14import java.util.List
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
8 15
9interface Logic2VampireLanguageMapper_TypeMapper { 16import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
10 def void transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace); 17
11 //samples below 2 lines 18class Logic2VampireLanguageMapper_TypeMapper {
12 def List<VLSTerm> transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) 19 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
13 def VLSTerm getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) 20 private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
14 21 val Logic2VampireLanguageMapper base
15 def int getUndefinedSupertypeScope(int undefinedScope,Logic2VampireLanguageMapperTrace trace) 22
16 def VLSTerm transformReference(DefinedElement referred,Logic2VampireLanguageMapperTrace trace) 23 new(Logic2VampireLanguageMapper base) {
17 24 LogicproblemPackage.eINSTANCE.class
18 def VampireModelInterpretation_TypeInterpretation getTypeInterpreter() 25 this.base = base
19} \ No newline at end of file 26 }
27
28 def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
29
30// val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
31// trace.typeMapperTrace = typeTrace
32 val VLSVariable variable = createVLSVariable => [it.name = "A"]
33
34 // 1. Each type (class) is a predicate with a single variable as input
35 for (type : types) {
36 val typePred = createVLSFunction => [
37 it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
38 it.terms += support.duplicate(variable)
39 ]
40// typeTrace.type2Predicate.put(type, typePred)
41 trace.type2Predicate.put(type, typePred)
42 }
43
44 // 2. Map each ENUM type definition to fof formula
45 for (type : types.filter(TypeDefinition)) {
46 val List<VLSFunction> orElems = newArrayList
47 for (e : type.elements) {
48 val enumElemPred = createVLSFunction => [
49 it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2))
50 it.terms += support.duplicate(variable)
51 ]
52// typeTrace.element2Predicate.put(e, enumElemPred)
53 trace.element2Predicate.put(e, enumElemPred)
54 orElems.add(enumElemPred)
55 }
56
57 val res = createVLSFofFormula => [
58 it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
59 // below is temporary solution
60 it.fofRole = "axiom"
61 it.fofFormula = createVLSUniversalQuantifier => [
62 it.variables += support.duplicate(variable)
63 it.operand = createVLSEquivalent => [
64// it.left = createVLSFunction => [
65// it.constant = type.lookup(typeTrace.type2Predicate).constant
66// it.terms += createVLSVariable => [it.name = "A"]
67// ]
68// it.left = type.lookup(typeTrace.type2Predicate)
69 it.left = type.lookup(trace.type2Predicate)
70
71 it.right = support.unfoldOr(orElems)
72
73 // TEMPPPPPPP
74// it.right = support.unfoldOr(type.elements.map [e |
75//
76// createVLSEquality => [
77// it.left = support.duplicate(variable)
78// it.right = createVLSDoubleQuote => [
79// it.value = "\"a" + e.name + "\""
80// ]
81// ]
82// ])
83 // END TEMPPPPP
84 ]
85 ]
86
87 ]
88 trace.specification.formulas += res
89 }
90
91 //HIERARCHY HANDLER
92
93
94 // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
95 // and store in a map
96 for (t1 : types.filter[!isIsAbstract]) {
97 for (t2 : types) {
98 // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
99 if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
100// typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate)))
101 trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
102 } else {
103// typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
104 trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
105 it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
106 ])
107 }
108 }
109// typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
110// typeTrace.type2PossibleNot.clear
111 trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values)))
112 trace.type2PossibleNot.clear
113 }
114
115 // 5. create fof function that is an or with all the elements in map
116 val hierarch = createVLSFofFormula => [
117 it.name = "hierarchyHandler"
118 it.fofRole = "axiom"
119 it.fofFormula = createVLSUniversalQuantifier => [
120 it.variables += support.duplicate(variable)
121 it.operand = createVLSEquivalent => [
122 it.left = support.topLevelTypeFunc
123// it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
124 it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values))
125 ]
126 ]
127 ]
128
129 trace.specification.formulas += hierarch
130
131 }
132
133 //below are from previous interface
134 def protected transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
135 Logic2VampireLanguageMapperTrace trace) {
136 throw new UnsupportedOperationException("TODO: auto-generated method stub")
137 }
138
139 def protected getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) {
140 throw new UnsupportedOperationException("TODO: auto-generated method stub")
141 }
142
143 def protected getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) {
144 throw new UnsupportedOperationException("TODO: auto-generated method stub")
145 }
146
147 def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) {
148 createVLSDoubleQuote => [
149 it.value = "\"a" + referred.name + "\""
150 ]
151 }
152
153 def protected getTypeInterpreter() {
154 throw new UnsupportedOperationException("TODO: auto-generated method stub")
155 }
156
157}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
deleted file mode 100644
index ea72940e..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ /dev/null
@@ -1,153 +0,0 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
6import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
10import java.util.ArrayList
11import java.util.Collection
12
13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
14import java.util.List
15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
16
17class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {
18 private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
19 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
20
21 new() {
22 LogicproblemPackage.eINSTANCE.class
23 }
24
25 override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
26
27// val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
28// trace.typeMapperTrace = typeTrace
29 val VLSVariable variable = createVLSVariable => [it.name = "A"]
30
31 // 1. Each type (class) is a predicate with a single variable as input
32 for (type : types) {
33 val typePred = createVLSFunction => [
34 it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
35 it.terms += support.duplicate(variable)
36 ]
37// typeTrace.type2Predicate.put(type, typePred)
38 trace.type2Predicate.put(type, typePred)
39 }
40
41 // 2. Map each ENUM type definition to fof formula
42 for (type : types.filter(TypeDefinition)) {
43 val List<VLSFunction> orElems = newArrayList
44 for (e : type.elements) {
45 val enumElemPred = createVLSFunction => [
46 it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2))
47 it.terms += support.duplicate(variable)
48 ]
49// typeTrace.element2Predicate.put(e, enumElemPred)
50 trace.element2Predicate.put(e, enumElemPred)
51 orElems.add(enumElemPred)
52 }
53
54 val res = createVLSFofFormula => [
55 it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
56 // below is temporary solution
57 it.fofRole = "axiom"
58 it.fofFormula = createVLSUniversalQuantifier => [
59 it.variables += support.duplicate(variable)
60 it.operand = createVLSEquivalent => [
61// it.left = createVLSFunction => [
62// it.constant = type.lookup(typeTrace.type2Predicate).constant
63// it.terms += createVLSVariable => [it.name = "A"]
64// ]
65// it.left = type.lookup(typeTrace.type2Predicate)
66 it.left = type.lookup(trace.type2Predicate)
67
68 it.right = support.unfoldOr(orElems)
69
70 // TEMPPPPPPP
71// it.right = support.unfoldOr(type.elements.map [e |
72//
73// createVLSEquality => [
74// it.left = support.duplicate(variable)
75// it.right = createVLSDoubleQuote => [
76// it.value = "\"a" + e.name + "\""
77// ]
78// ]
79// ])
80 // END TEMPPPPP
81 ]
82 ]
83
84 ]
85 trace.specification.formulas += res
86 }
87
88 //HIERARCHY HANDLER
89
90
91 // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
92 // and store in a map
93 for (t1 : types.filter[!isIsAbstract]) {
94 for (t2 : types) {
95 // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
96 if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
97// typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate)))
98 trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
99 } else {
100// typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
101 trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
102 it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
103 ])
104 }
105 }
106// typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
107// typeTrace.type2PossibleNot.clear
108 trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values)))
109 trace.type2PossibleNot.clear
110 }
111
112 // 5. create fof function that is an or with all the elements in map
113 val hierarch = createVLSFofFormula => [
114 it.name = "hierarchyHandler"
115 it.fofRole = "axiom"
116 it.fofFormula = createVLSUniversalQuantifier => [
117 it.variables += support.duplicate(variable)
118 it.operand = createVLSEquivalent => [
119 it.left = support.topLevelTypeFunc
120// it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
121 it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values))
122 ]
123 ]
124 ]
125
126 trace.specification.formulas += hierarch
127
128 }
129
130 override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
131 Logic2VampireLanguageMapperTrace trace) {
132 throw new UnsupportedOperationException("TODO: auto-generated method stub")
133 }
134
135 override getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) {
136 throw new UnsupportedOperationException("TODO: auto-generated method stub")
137 }
138
139 override getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) {
140 throw new UnsupportedOperationException("TODO: auto-generated method stub")
141 }
142
143 override transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) {
144 createVLSDoubleQuote => [
145 it.value = "\"a" + referred.name + "\""
146 ]
147 }
148
149 override getTypeInterpreter() {
150 throw new UnsupportedOperationException("TODO: auto-generated method stub")
151 }
152
153}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-26 13:41:43 +0000