diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend | 183 |
1 files changed, 183 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend new file mode 100644 index 00000000..48952288 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend | |||
@@ -0,0 +1,183 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable | ||
4 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue | ||
5 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm | ||
6 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory | ||
7 | import java.util.ArrayList | ||
8 | import java.util.List | ||
9 | import java.util.Map | ||
10 | import org.eclipse.emf.ecore.EObject | ||
11 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
12 | import org.eclipse.xtend.lib.annotations.Data | ||
13 | import java.util.HashMap | ||
14 | import java.util.LinkedList | ||
15 | |||
16 | abstract class TransformedSubterm { | ||
17 | val static extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE | ||
18 | def LogicSubterm expectLogic() | ||
19 | def NumericSubterm expectNumber() | ||
20 | |||
21 | def List<SubtermOption> getPossibleValues() | ||
22 | |||
23 | public static def List<List<SubtermOption>> allCombinations(List<SubtermOption>... possibleValues) { | ||
24 | return allCombinations(possibleValues.toList) | ||
25 | } | ||
26 | public static def List<List<SubtermOption>> allCombinations(Iterable<List<SubtermOption>> possibleValues) { | ||
27 | if(possibleValues.size == 1) { | ||
28 | return possibleValues.head.map[x|#[x.copy]] | ||
29 | } else { | ||
30 | val head = possibleValues.head | ||
31 | val tails = possibleValues.tail.allCombinations | ||
32 | val res = new ArrayList(tails.size * head.size) | ||
33 | for(headElement : head) { | ||
34 | for(tail : tails) { | ||
35 | val combination = new ArrayList(tail.size+1) | ||
36 | combination.add(headElement) | ||
37 | combination.addAll(tail.map[copy]) | ||
38 | res.add(combination) | ||
39 | } | ||
40 | } | ||
41 | return res | ||
42 | } | ||
43 | } | ||
44 | |||
45 | public static def resolveToLogic(List<SubtermOption> subterms, SMTTerm value) { | ||
46 | val allDefinitions = subterms.map[it.variables].flatten | ||
47 | val allPreconditions = subterms.map[it.preconditions].flatten | ||
48 | val preconditionedExpression = if(allPreconditions.empty) { | ||
49 | value | ||
50 | } else { | ||
51 | createSMTAnd => [it.operands += allPreconditions it.operands += value] | ||
52 | } | ||
53 | val quantifiedExpression = if(allDefinitions.empty) { | ||
54 | preconditionedExpression | ||
55 | } else { | ||
56 | createSMTForall => [ | ||
57 | it.quantifiedVariables += allDefinitions | ||
58 | it.expression = preconditionedExpression] | ||
59 | } | ||
60 | return quantifiedExpression | ||
61 | } | ||
62 | } | ||
63 | |||
64 | @Data class SubtermOption { | ||
65 | List<SMTSortedVariable> variables | ||
66 | List<SMTTerm> preconditions | ||
67 | SMTTerm expression | ||
68 | TypeDescriptor type | ||
69 | |||
70 | public new( | ||
71 | List<SMTSortedVariable> variables, | ||
72 | List<SMTTerm> preconditions, | ||
73 | SMTTerm expression, | ||
74 | TypeDescriptor type) | ||
75 | { | ||
76 | this.variables = variables | ||
77 | this.preconditions = preconditions | ||
78 | this.expression = expression | ||
79 | this.type = type | ||
80 | } | ||
81 | |||
82 | public new( | ||
83 | List<SubtermOption> previousSubterms, | ||
84 | List<SMTSortedVariable> newVariables, | ||
85 | List<SMTTerm> newPreconditions, | ||
86 | SMTTerm newExpression, | ||
87 | TypeDescriptor newType) | ||
88 | { | ||
89 | val old2New = new HashMap | ||
90 | variables = new LinkedList | ||
91 | for(variable : previousSubterms.map[getVariables].flatten) { | ||
92 | val newVariable = EcoreUtil.copy(variable) | ||
93 | old2New.put(variable,newVariable) | ||
94 | variables+=newVariable | ||
95 | } | ||
96 | |||
97 | preconditions = new LinkedList | ||
98 | preconditions += previousSubterms.map[getPreconditions].flatten.map[x|EcoreUtil.copy(x)] | ||
99 | preconditions += newPreconditions.map[x|EcoreUtil.copy(x)] | ||
100 | preconditions.forEach[relinkAllVariableReference(old2New)] | ||
101 | |||
102 | expression = EcoreUtil.copy(newExpression) | ||
103 | relinkAllVariableReference(expression,old2New) | ||
104 | |||
105 | type = newType | ||
106 | } | ||
107 | |||
108 | public def copy() { | ||
109 | val old2New = variables.toInvertedMap[EcoreUtil.copy(it)] | ||
110 | val newPreconditions = preconditions.map[EcoreUtil.copy(it)] | ||
111 | newPreconditions.forEach[it.relinkAllVariableReference(old2New)] | ||
112 | val newExpression = EcoreUtil.copy(expression) | ||
113 | return new SubtermOption(variables.map[old2New.get(it)],newPreconditions,newExpression,type) | ||
114 | } | ||
115 | |||
116 | def private relinkAllVariableReference(EObject root,Map<SMTSortedVariable, SMTSortedVariable> map) { | ||
117 | if(root instanceof SMTSymbolicValue) root.relinkVariableReference(map) | ||
118 | root.eAllContents().filter(SMTSymbolicValue).forEach[relinkVariableReference(map)] | ||
119 | } | ||
120 | def private relinkVariableReference(SMTSymbolicValue target,Map<SMTSortedVariable, SMTSortedVariable> map) { | ||
121 | if(map.containsKey(target.symbolicReference)) { | ||
122 | target.symbolicReference = map.get(target.symbolicReference) | ||
123 | } | ||
124 | } | ||
125 | } | ||
126 | |||
127 | @Data | ||
128 | class LogicSubterm extends TransformedSubterm{ | ||
129 | |||
130 | SMTTerm value | ||
131 | override expectLogic() {return this} | ||
132 | override expectNumber() { throw new AssertionError("A term is not a number") } | ||
133 | |||
134 | public new(SMTTerm expression) | ||
135 | { | ||
136 | this.value = expression | ||
137 | } | ||
138 | override getPossibleValues() { | ||
139 | #[new SubtermOption(#[],#[],value,TypeDescriptor::logicTypeDescriptor_Instance)] | ||
140 | } | ||
141 | } | ||
142 | |||
143 | @Data | ||
144 | class NumericSubterm extends TransformedSubterm { | ||
145 | List<SubtermOption> values | ||
146 | |||
147 | public new( | ||
148 | List<SMTSortedVariable> variables, | ||
149 | List<SMTTerm> preconditions, | ||
150 | SMTTerm expression) { | ||
151 | this.values = #[new SubtermOption(variables,preconditions,expression,TypeDescriptor.numericTypeDescriptor_Instance)] | ||
152 | } | ||
153 | public new(List<SubtermOption> values) { | ||
154 | this.values = values | ||
155 | } | ||
156 | |||
157 | override expectLogic() { throw new AssertionError("A term is not a logic value") } | ||
158 | override expectNumber() { return this } | ||
159 | |||
160 | override getPossibleValues() { | ||
161 | values | ||
162 | } | ||
163 | } | ||
164 | |||
165 | @Data | ||
166 | class ComplexSubterm extends TransformedSubterm { | ||
167 | List<SubtermOption> options | ||
168 | override expectLogic() { throw new AssertionError("A term is not a logic value") } | ||
169 | override expectNumber() { throw new AssertionError("A term is not a number") } | ||
170 | public new(List<SMTSortedVariable> variables, | ||
171 | List<SMTTerm> preconditions, | ||
172 | SMTTerm expression, | ||
173 | TypeDescriptor type) | ||
174 | { | ||
175 | this.options = #[new SubtermOption(variables,preconditions,expression,type)] | ||
176 | } | ||
177 | public new(List<SubtermOption> subterms) { | ||
178 | this.options = subterms | ||
179 | } | ||
180 | override getPossibleValues() { | ||
181 | this.options | ||
182 | } | ||
183 | } | ||