diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-06-10 19:05:05 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-06-10 19:05:05 +0200 |
commit | 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch) | |
tree | 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend | |
parent | Initial commit, migrating from SVN (diff) | |
download | VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip |
Migrating Additional projects
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend | 167 |
1 files changed, 167 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend new file mode 100644 index 00000000..fb0739ab --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend | |||
@@ -0,0 +1,167 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
11 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.builder.SmtModelQueryEngine | ||
12 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
13 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
14 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration | ||
15 | import org.eclipse.xtend.lib.annotations.Accessors | ||
16 | import org.eclipse.xtend.lib.annotations.Data | ||
17 | |||
18 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
19 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration | ||
20 | |||
21 | @Data | ||
22 | class ValueType { | ||
23 | TypeDescriptor descriptor | ||
24 | Object value | ||
25 | } | ||
26 | |||
27 | class SmtModelInterpretation implements LogicModelInterpretation { | ||
28 | //val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
29 | @Accessors(PUBLIC_GETTER) val SmtModelQueryEngine queryEngine; | ||
30 | |||
31 | // Trace info | ||
32 | val Logic2SmtMapperTrace newTrace; | ||
33 | val Logic2SMT_TypeMapperInterpretation typeInterpretation | ||
34 | |||
35 | /** | ||
36 | * Creates a model builder which queries a logic structure. | ||
37 | * @param document The whole SMT2 document. | ||
38 | * @param trace The trace of the [Logic problem -> SMT problem] mapping | ||
39 | */ | ||
40 | new(LogicProblem problem, SMTDocument document, Logic2SmtMapper forwardMapper, Logic2SmtMapperTrace forwardTrace) { | ||
41 | //document.input.typeDeclarations.forEach[typeNames.put(it.name,it)] | ||
42 | |||
43 | this.queryEngine = new SmtModelQueryEngine(document) | ||
44 | this.newTrace = initialiseNewTrace(document,forwardTrace) | ||
45 | this.typeInterpretation = forwardMapper.typeMapper.getTypeInterpretation(problem,document,this,newTrace) | ||
46 | } | ||
47 | |||
48 | /** | ||
49 | * Creates a new trace from the logic model to the new smt file by using the old trace. | ||
50 | */ | ||
51 | def protected Logic2SmtMapperTrace initialiseNewTrace(SMTDocument document, Logic2SmtMapperTrace oldTrace) { | ||
52 | val i = document.input | ||
53 | |||
54 | val res = new Logic2SmtMapperTrace => [ typeMapperTrace = oldTrace.typeMapperTrace.copy(i) ] | ||
55 | |||
56 | for(entry : oldTrace.relationUnfolding.entrySet) { | ||
57 | val rel = entry.key | ||
58 | val descriptors = entry.value.map[old | | ||
59 | new Descriptor<Relation>( | ||
60 | old.parameterTypes.map[copyTypeDescriptor(i)], | ||
61 | old.relation) | ||
62 | ] | ||
63 | res.relationUnfolding.put(rel,descriptors) | ||
64 | } | ||
65 | |||
66 | for(entry : oldTrace.relationMap.entrySet) { | ||
67 | val desc = new Descriptor<Relation>( | ||
68 | entry.key.parameterTypes.map[copyTypeDescriptor(i)], | ||
69 | entry.key.relation) | ||
70 | val fun = i.functionDeclarations.filter[it.name == entry.value.name].head | ||
71 | res.relationMap.put(desc,fun) | ||
72 | } | ||
73 | |||
74 | return res | ||
75 | } | ||
76 | |||
77 | def private copyTypeDescriptor(TypeDescriptor original, SMTInput i) { | ||
78 | if(original.complexType == null) return original | ||
79 | else { | ||
80 | val newType = i.typeDeclarations.filter[it.name == original.complexType.name].head | ||
81 | new TypeDescriptor(newType) | ||
82 | } | ||
83 | } | ||
84 | |||
85 | /*def protected initialiseTypes(SMTDocument document) { | ||
86 | val model = document.output.getModelResult as SMTModelResult | ||
87 | val smtUndefinedType2LogicType = this.newTrace.typeDeclarationMap.bijectiveInverse | ||
88 | |||
89 | for(cardinalityConstraint : model.typeDefinitions) { | ||
90 | val targetType = (cardinalityConstraint.type as SMTComplexTypeReference).referred as SMTSetTypeDeclaration | ||
91 | val List<DefinedElement> elementCollection = new LinkedList | ||
92 | for(element : cardinalityConstraint.elements.map[symbolicReference]) { | ||
93 | if(element instanceof SMTFunctionDeclaration) { | ||
94 | val definedElementRepresentation = createDefinedElement => [name += element.name.split("!")] | ||
95 | newElement2Constants.put(definedElementRepresentation,element) | ||
96 | newConstants2Elements.put(element,definedElementRepresentation) | ||
97 | } else{ | ||
98 | throw new UnsupportedOperationException( | ||
99 | "Unresolvable reference in cardinality constraint: " + element.class.name + ": " + element.name) | ||
100 | } | ||
101 | } | ||
102 | undefinedTypeDefinitions.put(targetType.lookup(smtUndefinedType2LogicType),elementCollection); | ||
103 | } | ||
104 | }*/ | ||
105 | |||
106 | def private dispatch ValueType logicLiteral2SmtLiteral(Integer literal) { | ||
107 | new ValueType(TypeDescriptor::numericTypeDescriptor_Instance, literal) | ||
108 | } | ||
109 | def private dispatch ValueType logicLiteral2SmtLiteral(Boolean literal) { | ||
110 | new ValueType(TypeDescriptor::logicTypeDescriptor_Instance, literal) | ||
111 | } | ||
112 | def private dispatch ValueType logicLiteral2SmtLiteral(DefinedElement literal) { | ||
113 | this.typeInterpretation.logicElement2Smt(literal) | ||
114 | } | ||
115 | |||
116 | // def private dispatch Object smt2Literal2LogicLiteral(Integer literal) { literal } | ||
117 | // def private dispatch Object smt2Literal2LogicLiteral(Boolean literal) { literal } | ||
118 | // def private dispatch Object smt2Literal2LogicLiteral(SMTSymbolicDeclaration literal) { | ||
119 | // this.typeInterpretation.smtElement2Logic(literal) | ||
120 | // } | ||
121 | |||
122 | override getElements(Type type) { | ||
123 | return this.typeInterpretation.getElements(type) | ||
124 | } | ||
125 | |||
126 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | ||
127 | /*queryEngine.resolveFunctionDeclaration( | ||
128 | function.lookup(newTrace.functionDeclarationMap), | ||
129 | parameterSubstitution.map[logicLiteral2SmtLiteral] | ||
130 | ).smt2Literal2LogicLiteral*/ | ||
131 | throw new UnsupportedOperationException | ||
132 | } | ||
133 | |||
134 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | ||
135 | val transformedParameters = parameterSubstitution.map[logicLiteral2SmtLiteral] | ||
136 | |||
137 | val smtFunction = new Descriptor<Relation>( | ||
138 | transformedParameters.map[descriptor], | ||
139 | relation) | ||
140 | .lookup(newTrace.relationMap) | ||
141 | |||
142 | val result = queryEngine.resolveFunctionDeclaration( | ||
143 | smtFunction as SMTFunctionDeclaration, | ||
144 | transformedParameters.map[value] | ||
145 | ) as Boolean | ||
146 | |||
147 | return result | ||
148 | } | ||
149 | |||
150 | override getInterpretation(ConstantDeclaration constant) { | ||
151 | /*queryEngine.resolveFunctionDeclaration( | ||
152 | constant.lookup(newTrace.constantDeclarationMap), | ||
153 | Collections.EMPTY_LIST | ||
154 | ).smt2Literal2LogicLiteral*/ | ||
155 | throw new UnsupportedOperationException | ||
156 | } | ||
157 | |||
158 | override getMaximalInteger() { | ||
159 | 100 | ||
160 | //throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
161 | } | ||
162 | |||
163 | override getMinimalInteger() { | ||
164 | -100 | ||
165 | //throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
166 | } | ||
167 | } \ No newline at end of file | ||