1 files changed, 314 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend
new file mode 100644
index 00000000..a259d103
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend
@@ -0,0 +1,314 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolLiteral
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEquals
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTITE
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMinus
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+class SmtModelQueryEngine {
+        private Map<SMTFunctionDeclaration, SMTFunctionDefinition> functionDeclarationToDefinitions =
+                new HashMap<SMTFunctionDeclaration, SMTFunctionDefinition>
+        
+        private val SMTInput input;
+        private val SMTOutput output
+        
+        new(SMTDocument model) {
+                val nameToFunctionDefiniton = new HashMap<String, SMTFunctionDefinition>
+                input = model.input
+                var SMTModelResult modelResult = null
+                
+                output = model.output
+                if(output!=null) {
+                        val result = output.getModelResult
+                        if(result instanceof SMTModelResult) {
+                                modelResult = result as SMTModelResult
+                        }
+                }
+                
+                input.functionDefinition.
+                        forEach[x|nameToFunctionDefiniton.put(x.name,x)]
+                if(modelResult!=null)
+                        modelResult.newFunctionDefinitions.
+                                forEach[x|nameToFunctionDefiniton.put(x.name,x)]
+                
+                input.functionDeclarations.
+                        forEach[x|functionDeclarationToDefinitions.put(x,x.name.lookup(nameToFunctionDefiniton))]
+                if(modelResult!=null)
+                        modelResult.newFunctionDeclarations.
+                                forEach[x|functionDeclarationToDefinitions.put(x,x.name.lookup(nameToFunctionDefiniton))]
+        }
+        
+        def protected <KEY_TYPE,VALUE_TYPE> VALUE_TYPE lookup(KEY_TYPE key, Map<? extends KEY_TYPE,? extends VALUE_TYPE> map) {
+                return map.get(key)
+        }
+        
+        def protected dispatch getDefaultValue(SMTIntTypeReference reference) { 0 }
+        def protected dispatch getDefaultValue(SMTBoolTypeReference reference) { false }
+        def protected dispatch getDefaultValue(SMTComplexTypeReference reference) {
+                val type = reference.referred
+                if(type instanceof SMTEnumeratedTypeDeclaration) return type.elements.head
+                else {
+                        val definition = (output.getModelResult as SMTModelResult).typeDefinitions.filter[it.type == type].head
+                        return definition.elements.head
+                }
+        }
+            
+        def protected isTerminal(
+                SMTTerm term,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                /*
+                 * An undefined function is a terminal.
+                 */
+                if(term instanceof SMTSymbolicValue) {
+                        val symbolicValue = term as SMTSymbolicValue
+                        
+                        if(symbolicValue.symbolicReference instanceof SMTFunctionDeclaration)
+                        {
+                                val function = symbolicValue.symbolicReference as SMTFunctionDeclaration;
+                                val hasDefinition = functionDeclarationToDefinitions.get(function) != null
+                                return ! hasDefinition
+                        }
+                        else return false
+                }
+                /*
+                 * A finite element is a terminal.
+                 */
+                else if(term instanceof SMTEnumLiteral)
+                        return true
+                else return false
+        }
+        def protected resolveTerminal(
+                SMTTerm terminal,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                if(terminal instanceof SMTEnumLiteral) {
+                        return terminal;
+                }
+                else if(terminal instanceof SMTSymbolicValue) {
+                        val symbolicValue = terminal as SMTSymbolicValue
+                        if(symbolicValue.symbolicReference instanceof SMTFunctionDeclaration)
+                        {
+                                val function = symbolicValue.symbolicReference as SMTFunctionDeclaration;
+                                return function
+                        }
+                }
+        }
+        
+        def public Object resolveFunctionDeclaration(
+                SMTFunctionDeclaration declaration,
+                List<Object> params)
+        {
+                
+                val definition = declaration.lookup(functionDeclarationToDefinitions)
+                if(definition == null) return declaration.range.defaultValue
+                else return definition.resolveFunctionDefinition(params)
+        }
+        def public Object resolveFunctionDefinition(
+                SMTFunctionDefinition definition,
+                List<Object> params)
+        {
+                if(params.nullOrEmpty && definition.parameters.nullOrEmpty) {
+                        return definition.resolveFunctionDefinition(emptyMap)
+                }
+                else if(params.size!=definition.parameters.size)
+                        throw new IllegalArgumentException(
+                                "Incorrect number of parameters!")
+                else {
+                        val substitution = new HashMap<SMTSortedVariable,Object>
+                        if(! definition.parameters.nullOrEmpty) {
+                                for(i : 0..definition.parameters.size-1) {
+                                        substitution.put(
+                                                definition.parameters.get(i),
+                                                params.get(i))
+                                }
+                        }
+                        val result=definition.resolveFunctionDefinition(substitution)
+                        //System::out.println(definition.name+"("+params.map[toString] + ") = " + result)
+                        return result
+                }
+        }
+        def protected Object resolveFunctionDefinition(
+                SMTFunctionDefinition definition,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                definition.value.resolveValue(substitution)
+        }
+        
+        def protected isBoolLiteral(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                term instanceof SMTBoolLiteral
+        }
+        def protected resolveBoolLiteral(SMTTerm boolValue, Map<SMTSortedVariable,Object> substitution) {
+                return (boolValue as SMTBoolLiteral).^value
+        }
+        
+        def protected isIntLiteral(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                term instanceof SMTIntLiteral ||
+                (term instanceof SMTMinus && (term as SMTMinus).rightOperand==null)
+        }
+        def protected resolveIntLiteral(SMTTerm intValue, Map<SMTSortedVariable,Object> substitution) {
+                if(intValue instanceof SMTIntLiteral) return (intValue as SMTIntLiteral).^value
+                else return -((intValue as SMTMinus).leftOperand as SMTIntLiteral).value
+        }
+        
+        def protected isParameterValue(
+                SMTTerm term,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                if(term instanceof SMTSymbolicValue) {
+                        return substitution.containsKey((term as SMTSymbolicValue).symbolicReference)
+                }
+                else return false
+        }
+        def protected Object resolveParameterValue(
+                SMTTerm term,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                return substitution.get((term as SMTSymbolicValue).symbolicReference);
+        }
+        
+        def protected isITE(
+                SMTTerm term,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                return term instanceof SMTITE;
+        }
+        def protected resolveITE(
+                SMTTerm term,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                val ite = term as SMTITE
+                val condition = ite.condition.resolveValue(substitution) as Boolean
+                
+                if(condition){
+                        return resolveValue(ite.^if,substitution)
+                }else{
+                        return resolveValue(ite.^else,substitution)
+                }
+        }
+        
+        def protected isAnd(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                term instanceof SMTAnd
+        }
+        def protected resolveAnd(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                val and = term as SMTAnd
+                for(operand : and.operands) {
+                        val operandValue = operand.resolveValue(substitution) as Boolean
+                        if(!operandValue) return false
+                }
+                return true
+        }
+        
+        def protected isEquals(
+                SMTTerm operand, 
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                return operand instanceof SMTEquals
+        }
+        def protected resolveEquals(SMTTerm term, Map<SMTSortedVariable,Object> substitution){
+                val equals = term as SMTEquals
+                val left = equals.leftOperand.resolveValue(substitution)
+                val right = equals.rightOperand.resolveValue(substitution)
+                val res = left.equals(right)
+                return res
+        }
+        
+        def protected isFiniteElementReference(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                if(term instanceof SMTSymbolicValue) {
+                        if((term as SMTSymbolicValue).symbolicReference instanceof SMTEnumLiteral) {
+                                return true
+                        }
+                }
+                return false;
+        }
+        def protected resolveFiniteElementReference(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                (term as SMTSymbolicValue).symbolicReference
+        }
+        
+        def protected isFunctionCall(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                if(term instanceof SMTSymbolicValue) {
+                        val functionCall = (term as SMTSymbolicValue).symbolicReference
+                        return functionCall instanceof SMTFunctionDeclaration || functionCall instanceof SMTFunctionDefinition
+                }
+                return false;
+        }
+        def protected resolveFunctionCall(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
+                if(term.isTerminal(substitution))
+                {
+                        return term.resolveTerminal(substitution);
+                }
+                else{
+                        val functionCall = term as SMTSymbolicValue
+                        var SMTFunctionDefinition calledFunction;
+                        var SMTFunctionDeclaration calledDeclaration;
+                        if(functionCall.symbolicReference instanceof SMTFunctionDeclaration) {
+                                calledDeclaration = functionCall.symbolicReference as SMTFunctionDeclaration
+                                calledFunction = functionCall.symbolicReference.lookup(functionDeclarationToDefinitions)}
+                        else {
+                                calledDeclaration = null;
+                                calledFunction = functionCall.symbolicReference as SMTFunctionDefinition
+                        }
+                        
+                        val newSubstitution = new HashMap<SMTSortedVariable,Object>
+                        if(! calledFunction.parameters.nullOrEmpty) {
+                                for(i : 0..calledFunction.parameters.size-1) {
+                                        newSubstitution.put(
+                                                calledFunction.parameters.get(i),
+                                                functionCall.parameterSubstitutions.get(i).resolveValue(substitution)
+                                        )
+                                }
+                        }
+                        return calledFunction.resolveFunctionDefinition(newSubstitution)
+                }
+        }
+        
+        def protected Object resolveValue(
+                SMTTerm value,
+                Map<SMTSortedVariable,Object> substitution)
+        {
+                if(value instanceof SMTSymbolicValue){
+                        (value as SMTSymbolicValue).symbolicReference
+                }
+                
+                if(value.isTerminal(substitution)) {
+                        return value.resolveTerminal(substitution)
+                }else if(value.isBoolLiteral(substitution)){
+                        return resolveBoolLiteral(value, substitution)
+                }else if(value.isIntLiteral(substitution)){
+                        return resolveIntLiteral(value, substitution)
+                }else if(value.isParameterValue(substitution)) {
+                        return resolveParameterValue(value,substitution)
+                }else if(value.isITE(substitution)){
+                        return resolveITE(value, substitution)
+                }else if(value.isAnd(substitution)) {
+                        return resolveAnd(value,substitution)
+                }else if(value.isEquals(substitution)) {
+                        return resolveEquals(value,substitution)
+                }else if(value.isFiniteElementReference(substitution)) {
+                        return resolveFiniteElementReference(value,substitution)
+                }else if(value.isFunctionCall(substitution)) {
+                        return resolveFunctionCall(value,substitution)
+                }else{
+                        throw new IllegalArgumentException("Can not resolve this term: " + value)
+                }
+        }
+}
+\ No newline at end of file

diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend new file mode 100644 index 00000000..a259d103 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend
@@ -0,0 +1,314 @@
	1	package hu.bme.mit.inf.dslreasoner.smt.reasoner.builder
	2
	3	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd
	4	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolLiteral
	5	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference
	6	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference
	7	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
	8	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral
	9	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration
	10	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEquals
	11	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
	12	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
	13	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTITE
	14	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
	15	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral
	16	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference
	17	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMinus
	18	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult
	19	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput
	20	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable
	21	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
	22	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
	23	import java.util.HashMap
	24	import java.util.List
	25	import java.util.Map
	26
	27	class SmtModelQueryEngine {
	28	private Map<SMTFunctionDeclaration, SMTFunctionDefinition> functionDeclarationToDefinitions =
	29	new HashMap<SMTFunctionDeclaration, SMTFunctionDefinition>
	30
	31	private val SMTInput input;
	32	private val SMTOutput output
	33
	34	new(SMTDocument model) {
	35	val nameToFunctionDefiniton = new HashMap<String, SMTFunctionDefinition>
	36	input = model.input
	37	var SMTModelResult modelResult = null
	38
	39	output = model.output
	40	if(output!=null) {
	41	val result = output.getModelResult
	42	if(result instanceof SMTModelResult) {
	43	modelResult = result as SMTModelResult
	44	}
	45	}
	46
	47	input.functionDefinition.
	48	forEach[x\|nameToFunctionDefiniton.put(x.name,x)]
	49	if(modelResult!=null)
	50	modelResult.newFunctionDefinitions.
	51	forEach[x\|nameToFunctionDefiniton.put(x.name,x)]
	52
	53	input.functionDeclarations.
	54	forEach[x\|functionDeclarationToDefinitions.put(x,x.name.lookup(nameToFunctionDefiniton))]
	55	if(modelResult!=null)
	56	modelResult.newFunctionDeclarations.
	57	forEach[x\|functionDeclarationToDefinitions.put(x,x.name.lookup(nameToFunctionDefiniton))]
	58	}
	59
	60	def protected <KEY_TYPE,VALUE_TYPE> VALUE_TYPE lookup(KEY_TYPE key, Map<? extends KEY_TYPE,? extends VALUE_TYPE> map) {
	61	return map.get(key)
	62	}
	63
	64	def protected dispatch getDefaultValue(SMTIntTypeReference reference) { 0 }
	65	def protected dispatch getDefaultValue(SMTBoolTypeReference reference) { false }
	66	def protected dispatch getDefaultValue(SMTComplexTypeReference reference) {
	67	val type = reference.referred
	68	if(type instanceof SMTEnumeratedTypeDeclaration) return type.elements.head
	69	else {
	70	val definition = (output.getModelResult as SMTModelResult).typeDefinitions.filter[it.type == type].head
	71	return definition.elements.head
	72	}
	73	}
	74
	75	def protected isTerminal(
	76	SMTTerm term,
	77	Map<SMTSortedVariable,Object> substitution)
	78	{
	79	/*
	80	* An undefined function is a terminal.
	81	*/
	82	if(term instanceof SMTSymbolicValue) {
	83	val symbolicValue = term as SMTSymbolicValue
	84
	85	if(symbolicValue.symbolicReference instanceof SMTFunctionDeclaration)
	86	{
	87	val function = symbolicValue.symbolicReference as SMTFunctionDeclaration;
	88	val hasDefinition = functionDeclarationToDefinitions.get(function) != null
	89	return ! hasDefinition
	90	}
	91	else return false
	92	}
	93	/*
	94	* A finite element is a terminal.
	95	*/
	96	else if(term instanceof SMTEnumLiteral)
	97	return true
	98	else return false
	99	}
	100	def protected resolveTerminal(
	101	SMTTerm terminal,
	102	Map<SMTSortedVariable,Object> substitution)
	103	{
	104	if(terminal instanceof SMTEnumLiteral) {
	105	return terminal;
	106	}
	107	else if(terminal instanceof SMTSymbolicValue) {
	108	val symbolicValue = terminal as SMTSymbolicValue
	109	if(symbolicValue.symbolicReference instanceof SMTFunctionDeclaration)
	110	{
	111	val function = symbolicValue.symbolicReference as SMTFunctionDeclaration;
	112	return function
	113	}
	114	}
	115	}
	116
	117	def public Object resolveFunctionDeclaration(
	118	SMTFunctionDeclaration declaration,
	119	List<Object> params)
	120	{
	121
	122	val definition = declaration.lookup(functionDeclarationToDefinitions)
	123	if(definition == null) return declaration.range.defaultValue
	124	else return definition.resolveFunctionDefinition(params)
	125	}
	126	def public Object resolveFunctionDefinition(
	127	SMTFunctionDefinition definition,
	128	List<Object> params)
	129	{
	130	if(params.nullOrEmpty && definition.parameters.nullOrEmpty) {
	131	return definition.resolveFunctionDefinition(emptyMap)
	132	}
	133	else if(params.size!=definition.parameters.size)
	134	throw new IllegalArgumentException(
	135	"Incorrect number of parameters!")
	136	else {
	137	val substitution = new HashMap<SMTSortedVariable,Object>
	138	if(! definition.parameters.nullOrEmpty) {
	139	for(i : 0..definition.parameters.size-1) {
	140	substitution.put(
	141	definition.parameters.get(i),
	142	params.get(i))
	143	}
	144	}
	145	val result=definition.resolveFunctionDefinition(substitution)
	146	//System::out.println(definition.name+"("+params.map[toString] + ") = " + result)
	147	return result
	148	}
	149	}
	150	def protected Object resolveFunctionDefinition(
	151	SMTFunctionDefinition definition,
	152	Map<SMTSortedVariable,Object> substitution)
	153	{
	154	definition.value.resolveValue(substitution)
	155	}
	156
	157	def protected isBoolLiteral(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
	158	term instanceof SMTBoolLiteral
	159	}
	160	def protected resolveBoolLiteral(SMTTerm boolValue, Map<SMTSortedVariable,Object> substitution) {
	161	return (boolValue as SMTBoolLiteral).^value
	162	}
	163
	164	def protected isIntLiteral(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
	165	term instanceof SMTIntLiteral \|\|
	166	(term instanceof SMTMinus && (term as SMTMinus).rightOperand==null)
	167	}
	168	def protected resolveIntLiteral(SMTTerm intValue, Map<SMTSortedVariable,Object> substitution) {
	169	if(intValue instanceof SMTIntLiteral) return (intValue as SMTIntLiteral).^value
	170	else return -((intValue as SMTMinus).leftOperand as SMTIntLiteral).value
	171	}
	172
	173	def protected isParameterValue(
	174	SMTTerm term,
	175	Map<SMTSortedVariable,Object> substitution)
	176	{
	177	if(term instanceof SMTSymbolicValue) {
	178	return substitution.containsKey((term as SMTSymbolicValue).symbolicReference)
	179	}
	180	else return false
	181	}
	182	def protected Object resolveParameterValue(
	183	SMTTerm term,
	184	Map<SMTSortedVariable,Object> substitution)
	185	{
	186	return substitution.get((term as SMTSymbolicValue).symbolicReference);
	187	}
	188
	189	def protected isITE(
	190	SMTTerm term,
	191	Map<SMTSortedVariable,Object> substitution)
	192	{
	193	return term instanceof SMTITE;
	194	}
	195	def protected resolveITE(
	196	SMTTerm term,
	197	Map<SMTSortedVariable,Object> substitution)
	198	{
	199	val ite = term as SMTITE
	200	val condition = ite.condition.resolveValue(substitution) as Boolean
	201
	202	if(condition){
	203	return resolveValue(ite.^if,substitution)
	204	}else{
	205	return resolveValue(ite.^else,substitution)
	206	}
	207	}
	208
	209	def protected isAnd(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
	210	term instanceof SMTAnd
	211	}
	212	def protected resolveAnd(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
	213	val and = term as SMTAnd
	214	for(operand : and.operands) {
	215	val operandValue = operand.resolveValue(substitution) as Boolean
	216	if(!operandValue) return false
	217	}
	218	return true
	219	}
	220
	221	def protected isEquals(
	222	SMTTerm operand,
	223	Map<SMTSortedVariable,Object> substitution)
	224	{
	225	return operand instanceof SMTEquals
	226	}
	227	def protected resolveEquals(SMTTerm term, Map<SMTSortedVariable,Object> substitution){
	228	val equals = term as SMTEquals
	229	val left = equals.leftOperand.resolveValue(substitution)
	230	val right = equals.rightOperand.resolveValue(substitution)
	231	val res = left.equals(right)
	232	return res
	233	}
	234
	235	def protected isFiniteElementReference(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
	236	if(term instanceof SMTSymbolicValue) {
	237	if((term as SMTSymbolicValue).symbolicReference instanceof SMTEnumLiteral) {
	238	return true
	239	}
	240	}
	241	return false;
	242	}
	243	def protected resolveFiniteElementReference(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
	244	(term as SMTSymbolicValue).symbolicReference
	245	}
	246
	247	def protected isFunctionCall(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
	248	if(term instanceof SMTSymbolicValue) {
	249	val functionCall = (term as SMTSymbolicValue).symbolicReference
	250	return functionCall instanceof SMTFunctionDeclaration \|\| functionCall instanceof SMTFunctionDefinition
	251	}
	252	return false;
	253	}
	254	def protected resolveFunctionCall(SMTTerm term, Map<SMTSortedVariable,Object> substitution) {
	255	if(term.isTerminal(substitution))
	256	{
	257	return term.resolveTerminal(substitution);
	258	}
	259	else{
	260	val functionCall = term as SMTSymbolicValue
	261	var SMTFunctionDefinition calledFunction;
	262	var SMTFunctionDeclaration calledDeclaration;
	263	if(functionCall.symbolicReference instanceof SMTFunctionDeclaration) {
	264	calledDeclaration = functionCall.symbolicReference as SMTFunctionDeclaration
	265	calledFunction = functionCall.symbolicReference.lookup(functionDeclarationToDefinitions)}
	266	else {
	267	calledDeclaration = null;
	268	calledFunction = functionCall.symbolicReference as SMTFunctionDefinition
	269	}
	270
	271	val newSubstitution = new HashMap<SMTSortedVariable,Object>
	272	if(! calledFunction.parameters.nullOrEmpty) {
	273	for(i : 0..calledFunction.parameters.size-1) {
	274	newSubstitution.put(
	275	calledFunction.parameters.get(i),
	276	functionCall.parameterSubstitutions.get(i).resolveValue(substitution)
	277	)
	278	}
	279	}
	280	return calledFunction.resolveFunctionDefinition(newSubstitution)
	281	}
	282	}
	283
	284	def protected Object resolveValue(
	285	SMTTerm value,
	286	Map<SMTSortedVariable,Object> substitution)
	287	{
	288	if(value instanceof SMTSymbolicValue){
	289	(value as SMTSymbolicValue).symbolicReference
	290	}
	291
	292	if(value.isTerminal(substitution)) {
	293	return value.resolveTerminal(substitution)
	294	}else if(value.isBoolLiteral(substitution)){
	295	return resolveBoolLiteral(value, substitution)
	296	}else if(value.isIntLiteral(substitution)){
	297	return resolveIntLiteral(value, substitution)
	298	}else if(value.isParameterValue(substitution)) {
	299	return resolveParameterValue(value,substitution)
	300	}else if(value.isITE(substitution)){
	301	return resolveITE(value, substitution)
	302	}else if(value.isAnd(substitution)) {
	303	return resolveAnd(value,substitution)
	304	}else if(value.isEquals(substitution)) {
	305	return resolveEquals(value,substitution)
	306	}else if(value.isFiniteElementReference(substitution)) {
	307	return resolveFiniteElementReference(value,substitution)
	308	}else if(value.isFunctionCall(substitution)) {
	309	return resolveFunctionCall(value,substitution)
	310	}else{
	311	throw new IllegalArgumentException("Can not resolve this term: " + value)
	312	}
	313	}
	314	} \ No newline at end of file