aboutsummaryrefslogtreecommitdiffstats
path: root/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicModelInterpretation.xtend
blob: cdcbb48a336a8310b88efe346b0282d6c6f08cd6 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
package hu.bme.mit.inf.dslreasoner.logic.model.builder

import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
import java.math.BigDecimal
import java.util.List
import java.util.Map
import java.util.SortedSet
import java.util.TreeSet

import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

interface LogicModelInterpretation {

	/**
	 * Returns the elements of a type.
	 */
	def List<DefinedElement> getElements(Type type)

	/**
	 * Returns the interpretation of a function. The parameters and the return values are encoded to primitive java objects defined by the following table:
	 * <p><table>
	 * <tr><th>Term type</th><th>Java object type</th></tr>
	 * <tr><td>Element of a type </td><td>DefinedElement </td></tr>
	 * <tr><td>Boolean literal </td><td>Boolean </td></tr>
	 * <tr><td>Integer literal </td><td>Integer </td></tr>
	 * <tr><td>Real literal </td><td>BigDecimal </td></tr>
	 * <tr><td>String literal </td><td>String </td></tr>
	 * </table></p>
	 * @param function The target function to be interpreted.
	 * @param parameterSubstitution The array of the substituted parameters encoded as defined in the table.
	 * @return The result of the function call encoded as defined in the table.
	 */
	def Object getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution)

	/**
	 * Returns the interpretation of a relation. The parameters are encoded to primitive java objects defined by the following table:
	 * <p><table>
	 * <tr><th>Term type</th><th>Java object type</th></tr>
	 * <tr><td>Element of a type </td><td>DefinedElement </td></tr>
	 * <tr><td>Boolean literal </td><td>Boolean </td></tr>
	 * <tr><td>Integer literal </td><td>Integer </td></tr>
	 * <tr><td>Real literal </td><td>BigDecimal </td></tr>
	 * <tr><td>String literal </td><td>String </td></tr>
	 * </table></p>
	 * @param relation The target relation to be interpreted.
	 * @param parameterSubstitution The array of the substituted parameters encoded as defined in the table.
	 * @return If the parameter tuple is in the relation.
	 */
	def boolean getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution)

	/**
	 * Returns the interpretation of a constant. The value is encoded to primitive java objects defined by the following table:
	 * <p><table>
	 * <tr><th>Term type</th><th>Java object type</th></tr>
	 * <tr><td>Element of a type </td><td>DefinedElement </td></tr>
	 * <tr><td>Boolean literal </td><td>Boolean </td></tr>
	 * <tr><td>Integer literal </td><td>Integer </td></tr>
	 * <tr><td>Real literal </td><td>BigDecimal </td></tr>
	 * <tr><td>String literal </td><td>String </td></tr>
	 * </table></p>
	 * @param constant The target constant to be interpreted.
	 * @return The value of the constant encoded as specified in the table.
	 */
	def Object getInterpretation(ConstantDeclaration constant)

	/**
	 * Returns all integers relevant to the logic structure. Not all integer is necessarily used.
	 */
	def SortedSet<Integer> getAllIntegersInStructure()

	def Map<TermDescription, Integer> getAllIntegersWithInterpretation() {
		allIntegersInStructure.toMap [ integer |
			(LogiclanguageFactory.eINSTANCE.createIntLiteral => [value = integer]) as TermDescription
		]
	}

	/**
	 * Returns all real numbers relevant to the logic structure. Not all integer is necessarily used.
	 */
	def SortedSet<BigDecimal> getAllRealsInStructure()

	def Map<TermDescription, BigDecimal> getAllRealsWithInterpretation() {
		allRealsInStructure.toMap [ real |
			(LogiclanguageFactory.eINSTANCE.createRealLiteral => [value = real]) as TermDescription
		]
	}

	/**
	 * Returns all string values relevant to the logic structure. Not all integer is necessarily used.
	 */
	def SortedSet<String> getAllStringsInStructure()
	
	def Map<TermDescription, String> getAllStringsWithInterpretation() {
		allStringsInStructure.toMap [ string |
			(LogiclanguageFactory.eINSTANCE.createStringLiteral => [value = string]) as TermDescription
		]
	}
	
	def SortedSet<Boolean> getAllBooleansInStructure() {
		new TreeSet(#{true, false})
	}
	
	def Map<TermDescription, Boolean> getAllBooleansWithInterpretation() {
		allBooleansInStructure.toMap [ bool |
			(LogiclanguageFactory.eINSTANCE.createBoolLiteral => [value = bool]) as TermDescription
		]
	}
}

class Uninterpreted implements LogicModelInterpretation {
	/*private val static unknownBecauseUninterpreted = LogiclanguageFactory.eINSTANCE.createUnknownBecauseUninterpreted
	 public def static getUnknownBecauseUninterpreted() {return Uninterpreted.unknownBecauseUninterpreted}*/
	override getElements(Type type) {
		throw new UnsupportedOperationException("The interpteration is unknown.")
	}

	def getKnownElements(Type type) {
		val allSubtypes = type.transitiveClosureStar[it.subtypes]
		return allSubtypes.filter(TypeDefinition).map[elements].flatten.toList
	}

	def allElementsAreInterpreted(Type type) {
		val allSubtypes = type.transitiveClosureStar[it.subtypes]
		return allSubtypes.exists[it instanceof TypeDeclaration]
	}

	override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
		throw new UnsupportedOperationException("The interpteration is unknown.")
	}

	override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
		throw new UnsupportedOperationException("The interpteration is unknown.")
	}

	override getInterpretation(ConstantDeclaration constant) {
		throw new UnsupportedOperationException("The interpteration is unknown.")
	}

	override getAllIntegersInStructure() {
		throw new UnsupportedOperationException("The interpteration is unknown.")
	}

	override getAllRealsInStructure() {
		throw new UnsupportedOperationException("The interpteration is unknown.")
	}

	override getAllStringsInStructure() {
		throw new UnsupportedOperationException("The interpteration is unknown.")
	}
}