package hu.bme.mit.inf.dslreasoner.smt.reasoner

import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion
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.SMTInput
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealTypeReference
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTReasoningTactic
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 hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType
import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
import java.util.ArrayList
import java.util.HashMap
import java.util.LinkedHashMap
import java.util.LinkedList
import java.util.List
import java.util.Map
import org.eclipse.emf.ecore.EObject
import org.eclipse.emf.ecore.util.EcoreUtil
import org.eclipse.xtend.lib.annotations.Accessors
import org.eclipse.xtext.xbase.lib.Functions.Function0
import org.eclipse.xtext.xbase.lib.Functions.Function1
import org.eclipse.xtext.xbase.lib.Functions.Function2
import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder

class Logic2SmtMapper{
	val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
	val Logic2SmtMapper_UnfoldingSupport unfolder = new Logic2SmtMapper_UnfoldingSupport
	@Accessors val Logic2Smt_TypeMapper typeMapper;
	
	LogicProblemBuilder b
	
	new(Logic2Smt_TypeMapper typeMapper) {
		this.typeMapper = typeMapper
	}
	
	public def TracedOutput<SMTDocument, Logic2SmtMapperTrace> transformProblem(LogicProblem problem, TypeScopes scope, SMTReasoningTactic strategy) {
		val documentInput = createSMTInput => [getModelCommand = createSMTGetModelCommand]
		if(strategy == null) documentInput.satCommand = createSMTSimpleSatCommand
		else documentInput.satCommand = createSMTComplexSatCommand => [it.method = EcoreUtil.copy(strategy)]
		
		val document = createSMTDocument => [input = documentInput]
		val trace = new Logic2SmtMapperTrace => [
			it.forwardMapper = this
			it.problem = problem
		]
		// Trafo
		this.typeMapper.transformTypes(documentInput,problem,trace, scope)
		problem.functions.filter(FunctionDeclaration).forEach[it.transformFunctionDeclaration(documentInput,trace)]
		problem.functions.filter(FunctionDefinition) .forEach[it.transformFunctionDefinition(documentInput,trace)]
		problem.relations.filter(RelationDeclaration).forEach[it.transformRelationDeclaration(documentInput,trace)]
		problem.relations.filter(RelationDefinition) .forEach[it.transformRelationDefinition(documentInput,trace)]
		problem.constants.filter(ConstantDeclaration).forEach[it.transformConstantDeclaration(documentInput,trace)]
		problem.constants.filter(ConstantDefinition) .forEach[it.transformConstantDefinition(documentInput,trace)]
		
		problem.relations.filter(RelationDefinition).forEach[it.transformRelationDefinition_definition(documentInput,trace)]
		documentInput.assertions += problem.assertions.map[transformAssertion(trace)]
		// End trafo
		
		document.input.assertions.forEach[it.value.nameAllUnnamedVariable]
		document.input.functionDefinition.forEach[it.value.nameAllUnnamedVariable]
		document.cleanDocument
		return new TracedOutput(document,trace)
	}
	
	private def toID(String name) {name.split("\\s+").join("!") }
	
	private def nameAllUnnamedVariable(SMTTerm root) {
		var index = 1
		val unnamedVariables = root.eAllContents.filter(SMTSortedVariable).filter[it.name == null].toList
		for(unnamedVariable : unnamedVariables) {
			unnamedVariable.name = '''var«index++»'''
		}
	}
	
//	def protected maxIntegerRageDefiniton(SMTInput documentInput) {
//		val upperlimit = createSMTFunctionDeclaration
//	}
	
	def dispatch protected List<TypeConstraint> transformTypeReference(BoolTypeReference boolTypeReference, Logic2SmtMapperTrace trace) {
		return #[new TypeConstraint(createSMTBoolTypeReference,null)]
	}
	def dispatch protected List<TypeConstraint> transformTypeReference(IntTypeReference intTypeReference, Logic2SmtMapperTrace trace) {
		return #[new TypeConstraint(createSMTIntTypeReference,null)]
	}
	def dispatch protected List<TypeConstraint> transformTypeReference(RealTypeReference realTypeReference, Logic2SmtMapperTrace trace) {
		return #[new TypeConstraint(createSMTRealTypeReference,null)]
	}
	def dispatch protected List<TypeConstraint> transformTypeReference(ComplexTypeReference complexTypeReference, Logic2SmtMapperTrace trace) {
		return typeMapper.transformTypeReference(complexTypeReference.referred,trace)
	}
	
	///////////////////////////////////////////////////////
	// Definitions
	///////////////////////////////////////////////////////
	
	def transformFunctionDeclaration(FunctionDeclaration function, SMTInput input, Logic2SmtMapperTrace trace) {
		val parameterTypeCombinations = unfolder.getPermutations(function.parameters.map[x|transformTypeReference(x,trace)])
		val rangeTypeCombinations = function.range.transformTypeReference(trace)
		
		if(rangeTypeCombinations.size == 1) {
			val rangeType = rangeTypeCombinations.head
			// Map it as function
			var index = 1
			for(combination : parameterTypeCombinations) {
				val nameWithIndex = if (parameterTypeCombinations.size > 1)
					toID('''function «function.name.toID» «index++»''')
				else
					toID('''function «function.name.toID»''')
					
				createFunctionDeclaration(function,nameWithIndex,combination,rangeType,true, input,trace)
			}
		} else {
			// Map it as a relation
			var index = 1
			for(combination : parameterTypeCombinations) {
				val type2function = new HashMap
				for(rangeType : rangeTypeCombinations) {
					val nameWithIndex = toID('''function «function.name.toID» «index++»''')
					val f = createFunctionDeclaration(function,nameWithIndex,combination,rangeType,false,input,trace)
					type2function.put(rangeType,f)
				}
				// for all rangeTypes, there is
				// 1. at least one range type that satisfies the relation
				input.assertions+=createSMTAssertion => [
					it.value = createSMTForall => [f|
						var paramIndex = 1
						for(param : combination) {
							val paramName = '''p«paramIndex++»'''
							val variable = createSMTSortedVariable => [
								it.name = paramName
								it.range = param.type
							]
							f.quantifiedVariables += variable
						}
						f.expression = createSMTOr => [
							operands+=rangeTypeCombinations.map[t|
								createSMTExists => [
									val v = createSMTSortedVariable => [
										it.name = "r"
										it.range = EcoreUtil.copy(t.type)
									]
									it.quantifiedVariables += v
									it.expression = createSMTSymbolicValue => [
										it.symbolicReference = type2function.get(t)
										it.parameterSubstitutions += f.quantifiedVariables.map[fv|
											createSMTSymbolicValue => [it.symbolicReference = fv]
										]
										it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = v]	
									]
								]
							]
						]
					]
				]
				// 2. at most one range type that satisfies the relation
				// TODO a
			}
		}
	}
	
	private def createFunctionDeclaration(
		Function function,
		String nameWithIndex,
		List<TypeConstraint> combination,
		TypeConstraint rangeType,
		boolean useFunction,
		SMTInput input,
		Logic2SmtMapperTrace trace
	) {
		val smtFunction = if(useFunction) {
			createSMTFunctionDeclaration => [
				it.name = nameWithIndex
				it.parameters += combination.map[it.type]
				it.range = rangeType.type
			]
		} else {
			createSMTFunctionDeclaration => [
				it.name = nameWithIndex
				it.parameters += combination.map[it.type]
				it.parameters += rangeType.type
				it.range = createSMTBoolTypeReference
			]
		}
		
		val descriptor = new Descriptor<Function>((combination+#[rangeType]).toList.map[
			TypeDescriptor.createFromTypeReference(it.type)],function)
		trace.functionMap.put(descriptor,smtFunction)
		input.functionDeclarations += smtFunction
		trace.functionUnfolding.put(function,#[descriptor])
		
		if(!useFunction) {
			input.assertions += createSMTAssertion => [
				it.value = createSMTForall => [f|
					var pi = 0
					for(param : combination) {
						val variable = createSMTSortedVariable
						variable.name = "p"+pi.toString
						variable.range = EcoreUtil.copy(combination.get(pi).type)
						f.quantifiedVariables+=variable
						pi++
					}
					val resultParam1 = createSMTSortedVariable => [
						it.name = "res1"
						it.range = EcoreUtil.copy(rangeType.type)
					]
					f.quantifiedVariables+=resultParam1
					val resultParam2 = createSMTSortedVariable => [
						it.name = "res2"
						it.range = EcoreUtil.copy(rangeType.type)
					]
					f.quantifiedVariables+=resultParam2
					f.expression = createSMTImpl => [
						it.leftOperand = createSMTAnd => [
							it.operands += createSMTSymbolicValue => [
								it.symbolicReference = smtFunction
								it.parameterSubstitutions += (0..<combination.size).map[x|
									createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]]
								it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam1]
							]
							it.operands += createSMTSymbolicValue => [
								it.symbolicReference = smtFunction
								it.parameterSubstitutions += (0..<combination.size).map[x|
									createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]]
								it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam2]
							]
						]
						it.rightOperand = createSMTEquals => [
							it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam1]
							it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam2]
						]
					]
				]
			]
		}
		
		if(rangeType.constraint != null) {
			input.assertions += createSMTAssertion => [
				it.value = createSMTForall => [f|
					var pi = 0
					for(param : combination) {
						val variable = createSMTSortedVariable
						variable.name = "p"+pi.toString
						variable.range = EcoreUtil.copy(combination.get(pi).type)
						f.quantifiedVariables+=variable
						pi++
					}
					val resultParam = createSMTSortedVariable => [
						it.name = "res"
						it.range = EcoreUtil.copy(rangeType.type)
					]
					f.quantifiedVariables += resultParam
					f.expression = createSMTImpl => [
						it.leftOperand = if(useFunction)
						{
							createSMTEquals => [
								leftOperand = createSMTSymbolicValue => [
									it.symbolicReference = smtFunction
									it.parameterSubstitutions += (0..<combination.size).map[x|
										createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]
									]
								]
								rightOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam]
							]
						} else {
							createSMTSymbolicValue => [
								it.symbolicReference = smtFunction
								it.parameterSubstitutions += (0..<combination.size).map[x|
									createSMTSymbolicValue => [it.symbolicReference = f.quantifiedVariables.get(x)]]
								it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam]
							]
						}
						it.rightOperand = rangeType.constraint.apply(resultParam)
					]
				]
			]
		}
		return smtFunction
	}
	
	def transformFunctionDefinition(FunctionDefinition function, SMTInput input, Logic2SmtMapperTrace trace) {
		throw new UnsupportedOperationException("TODO: auto-generated method stub")
	}
	
	def protected transformRelationDeclaration(RelationDeclaration relation, SMTInput input, Logic2SmtMapperTrace trace) {
		val parameterTypeCombinations = unfolder.getPermutations(relation.parameters.map[x|transformTypeReference(x,trace)])
		var relationIndex = 1
		val unfolding = new ArrayList(parameterTypeCombinations.size)
		for(parameterTypeCombination : parameterTypeCombinations) {
			/// Create a name for the relation
			val nameWithIndex = if (parameterTypeCombinations.size > 1)
					toID('''relation «relation.name.toID» «relationIndex++»''')
				else
					toID('''relation «relation.name.toID»''')
			
			// Adding an unfolded relation
			val smtRelation = createSMTFunctionDeclaration => [
				name = nameWithIndex
				parameters+= parameterTypeCombination.map[typeConstraint | EcoreUtil.copy(typeConstraint.type)]
				range = createSMTBoolTypeReference
			]
			val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[
				TypeDescriptor.createFromTypeReference(it.type)],relation)
			trace.relationMap.put(descriptor,smtRelation)
			input.functionDeclarations += smtRelation
			unfolding += descriptor
			
			// If there is a type constraint
			if(parameterTypeCombination.exists[it.constraint != null]) {
				// create a constraint that specifies that the relation contains elemenents with the required properties
				val and = createSMTAnd
				val rel = createSMTSymbolicValue => [it.symbolicReference = smtRelation]
				val forall = createSMTForall => [
					it.expression = createSMTImpl => [
						it.leftOperand = rel
						it.rightOperand = and
					]
				]
				var paramIndex = 0
				for(param : parameterTypeCombination) {
					val paramName = '''p«paramIndex++»'''
					val variable = createSMTSortedVariable => [
						it.name = paramName
						it.range = param.type
					]
					forall.quantifiedVariables += variable
					rel.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = variable]
					if(param.constraint != null) {
						and.operands+=param.constraint.apply(variable)
					}
				}
				input.assertions += createSMTAssertion => [
					it.value = forall
				]
			}
		}
		trace.relationUnfolding.put(relation,unfolding)
	}
	def protected transformRelationDefinition(RelationDefinition relation, SMTInput input, Logic2SmtMapperTrace trace) {
		val parameterTypeCombinations = unfolder.getPermutations(relation.variables.map[x|transformTypeReference(x.range,trace)]).toList
		var relationIndex = 1
		val unfolding = new ArrayList(parameterTypeCombinations.size)
		for(parameterTypeCombination : parameterTypeCombinations) {
			/// Create a name for the relation
			val nameWithIndex = if (parameterTypeCombinations.size > 1)
					toID('''relation «relation.name.toID» «relationIndex++»''')
				else
					toID('''relation «relation.name.toID»''')
			
			// creating an unfolded relation
			val smtRelation = createSMTFunctionDefinition => [
				name = nameWithIndex
				range = createSMTBoolTypeReference
			]
			/*
			// adding variables as parameters
			val Map<Variable, SMTSortedVariable> variables = new HashMap
			var paramIndex = 0
			val constraintList = new LinkedList
			for(param : parameterTypeCombination) {
				val paramName = relation.variables.get(paramIndex).name.toID
				val variable = createSMTSortedVariable => [
					it.name = paramName
					it.range = param.type
				]
				
				smtRelation.parameters+=variable
				variables.put(relation.variables.get(paramIndex),variable)
				if(param.constraint != null) {
					constraintList+=param.constraint.apply(variable)
				}
				paramIndex++
			}
			val definition = transformTerm(relation.value,trace,variables)
			if(constraintList.empty) {
				smtRelation.value = definition.expectLogic.value
			} else if(constraintList.size == 1) {
				smtRelation.value = createSMTAnd => [
					it.operands += constraintList.head
					it.operands += definition.expectLogic.value
				]
			} else {
				smtRelation.value = createSMTAnd => [
					it.operands += createSMTAnd => [operands += constraintList]
					it.operands += definition.expectLogic.value
				]
			}
			*/
			// 
			val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[
				TypeDescriptor.createFromTypeReference(it.type)],relation)
			trace.relationMap.put(descriptor,smtRelation)
			input.functionDefinition += smtRelation
			unfolding += descriptor
		}
		trace.relationUnfolding.put(relation,unfolding)
	}
	def transformRelationDefinition_definition(RelationDefinition relation, SMTInput input, Logic2SmtMapperTrace trace) {
		val parameterTypeCombinations = unfolder.getPermutations(relation.variables.map[x|transformTypeReference(x.range,trace)]).toList
		for(parameterTypeCombination : parameterTypeCombinations) {
			val Descriptor<Relation> descriptor = new Descriptor<Relation>(parameterTypeCombination.map[
				TypeDescriptor.createFromTypeReference(it.type)],relation)
			val smtRelation = descriptor.lookup(trace.relationMap) as SMTFunctionDefinition
			
			// adding variables as parameters
			val Map<Variable, SMTSortedVariable> variables = new HashMap
			var paramIndex = 0
			val constraintList = new LinkedList
			for(param : parameterTypeCombination) {
				val paramName = relation.variables.get(paramIndex).name.toID
				val variable = createSMTSortedVariable => [
					it.name = paramName
					it.range = param.type
				]
				
				smtRelation.parameters+=variable
				variables.put(relation.variables.get(paramIndex),variable)
				if(param.constraint != null) {
					constraintList+=param.constraint.apply(variable)
				}
				paramIndex++
			}
			val definition = transformTerm(relation.value,trace,variables)
			if(constraintList.empty) {
				smtRelation.value = definition.expectLogic.value
			} else if(constraintList.size == 1) {
				smtRelation.value = createSMTAnd => [
					it.operands += constraintList.head
					it.operands += definition.expectLogic.value
				]
			} else {
				smtRelation.value = createSMTAnd => [
					it.operands += createSMTAnd => [operands += constraintList]
					it.operands += definition.expectLogic.value
				]
			}
		}
	}
	
	def transformConstantDeclaration(ConstantDeclaration constant,SMTInput input, Logic2SmtMapperTrace trace) {
		throw new UnsupportedOperationException("TODO: auto-generated method stub")
	}
	
	def transformConstantDefinition(ConstantDefinition constant, SMTInput input, Logic2SmtMapperTrace trace) {
		throw new UnsupportedOperationException("TODO: auto-generated method stub")
	}
	
	
	def protected SMTAssertion transformAssertion(Assertion assertion, Logic2SmtMapperTrace trace) {
		val a = assertion.value.transformTerm(trace,emptyMap)
		createSMTAssertion => [value = a.expectLogic.value]
	}
	
	///////////////////////////////////////////////////////
	// Logic -> Logic value transformation
	///////////////////////////////////////////////////////
	
	///////////////////////////////////////////////////////
	// Literals
	///////////////////////////////////////////////////////
	def dispatch protected TransformedSubterm transformTerm(BoolLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		new LogicSubterm(createSMTBoolLiteral => [value = literal.value])	}
	def dispatch protected TransformedSubterm transformTerm(IntLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables)  {
		if(literal.value>=0) { new NumericSubterm(#[],#[],createSMTIntLiteral  => [value = literal.value])}
		else {new NumericSubterm(#[],#[],createSMTMinus => [ leftOperand = (createSMTIntLiteral => [value = - (literal.value) ] ) ]) } }
	def dispatch protected TransformedSubterm transformTerm(RealLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		new NumericSubterm(#[],#[],createSMTRealLiteral => [value = literal.value])	}
	
	///////////////////////////////////////////////////////
	// NumericOperators
	///////////////////////////////////////////////////////
	def dispatch protected TransformedSubterm transformTerm(Plus plus, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		return transformBinaryNumericOperator(
			plus.leftOperand,plus.rightOperand,
			[l,r|createSMTPlus => [ leftOperand = l rightOperand = r ]],
			trace,variables)
	}
	def dispatch protected TransformedSubterm transformTerm(Minus minus, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		return transformBinaryNumericOperator(
			minus.leftOperand,minus.rightOperand,
			[l,r|createSMTMinus => [ leftOperand = l rightOperand = r ]],
			trace,variables)
	}
	def dispatch protected TransformedSubterm transformTerm(Multiply multiply, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		return transformBinaryNumericOperator(
			multiply.leftOperand,multiply.rightOperand,
			[l,r|createSMTMultiply => [ leftOperand = l rightOperand = r ]],
			trace,variables)
	}
	def dispatch protected TransformedSubterm transformTerm(Divison div, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		return transformBinaryNumericOperator(
			div.leftOperand,div.rightOperand,
			[l,r|createSMTDiv => [ leftOperand = l rightOperand = r ]],
			trace,variables)
	}
	def dispatch protected TransformedSubterm transformTerm(Mod mod, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		return transformBinaryNumericOperator(
			mod.leftOperand,mod.rightOperand,
			[l,r|createSMTMod => [ leftOperand = l rightOperand = r ]],
			trace,variables)
	}
	
	def protected TransformedSubterm transformBinaryNumericOperator(
		Term leftOperand,
		Term rightOperand,
		Function2<SMTTerm,SMTTerm,SMTTerm> combinator,
		Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables)
	{
		val left  = leftOperand. transformTerm(trace,variables).expectNumber.getPossibleValues
		val right = rightOperand.transformTerm(trace,variables).expectNumber.getPossibleValues
		val values = new ArrayList(left.size * right.size)
		for(combination : TransformedSubterm.allCombinations(left,right)) {
			val l = combination.get(0)
			val r = combination.get(1)
			values += new SubtermOption(
				#[l,r],#[],#[],
				combinator.apply(l.expression, r.expression),
				TypeDescriptor.numericTypeDescriptor_Instance
			)
		}
		return new NumericSubterm(values)
	}
	
	///////////////////////////////////////////////////////
	// LogicOperators
	///////////////////////////////////////////////////////
	def dispatch protected TransformedSubterm transformTerm(Not not, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		val operand = not.operand.transformTerm(trace,variables).expectLogic
		new LogicSubterm(createSMTNot => [operand = operand.value]) }
	def dispatch protected TransformedSubterm transformTerm(And and, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		transformBinaryLogicOperator2(and.operands,[x|createSMTAnd => [operands += x]],trace,variables) }
	def dispatch protected TransformedSubterm transformTerm(Or or, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		transformBinaryLogicOperator2(or.operands,[x|createSMTOr => [operands += x]],trace,variables) }
	def dispatch protected TransformedSubterm transformTerm(Impl impl, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		transformBinaryLogicOperator1(impl.leftOperand,impl.rightOperand,[l,r|createSMTImpl =>[leftOperand = l rightOperand = r]],trace,variables) }
	def dispatch protected TransformedSubterm transformTerm(Iff iff, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		transformBinaryLogicOperator1(iff.leftOperand,iff.rightOperand,[l,r|createSMTIff => [leftOperand = l rightOperand = r]],trace,variables)}
	
	/**
	 * Logic combinator with two values
	 */
	def protected transformBinaryLogicOperator1(
		Term leftOperand, Term rightOperand,
		Function2<SMTTerm,SMTTerm,SMTTerm> combinator,
		Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		val left = leftOperand.transformTerm(trace,variables).expectLogic
		val right = rightOperand.transformTerm(trace,variables).expectLogic
		return new LogicSubterm(combinator.apply(left.value, right.value))
	}
	/**
	 * Logic combinator with multiple values
	 */
	def protected transformBinaryLogicOperator2(
		Iterable<? extends Term> operands,
		Function1<Iterable<? extends SMTTerm>,SMTTerm> combinator,
		Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		val smtOperands = operands.map[transformTerm(trace,variables).expectLogic.value]
		return new LogicSubterm(combinator.apply(smtOperands))
	}
	
	///////////////////////////////////////////////////////
	// Numeric -> Logic
	///////////////////////////////////////////////////////
	def dispatch protected TransformedSubterm transformTerm(MoreThan moreThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		transformNumericComparison(moreThan.leftOperand,moreThan.rightOperand, [l,r|createSMTMT => [ leftOperand = l rightOperand = r ]],trace,variables)}
	def dispatch protected TransformedSubterm transformTerm(LessThan lessThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		transformNumericComparison(lessThan.leftOperand,lessThan.rightOperand, [l,r|createSMTLT => [ leftOperand = l rightOperand = r ]],trace,variables)}
	def dispatch protected TransformedSubterm transformTerm(MoreOrEqualThan moreThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		transformNumericComparison(moreThan.leftOperand,moreThan.rightOperand, [l,r|createSMTMEQ => [ leftOperand = l rightOperand = r ]],trace,variables)}
	def dispatch protected TransformedSubterm transformTerm(LessOrEqualThan lessThan, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		transformNumericComparison(lessThan.leftOperand,lessThan.rightOperand, [l,r|createSMTLEQ => [ leftOperand = l rightOperand = r ]],trace,variables)}
	
	def protected transformNumericComparison(Term leftOperand, Term rightOperand, Function2<SMTTerm,SMTTerm,SMTTerm> combinator, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables){
		val left = leftOperand.transformTerm(trace,variables).getPossibleValues
		val right = rightOperand.transformTerm(trace,variables).getPossibleValues
		val values = new ArrayList(left.size * right.size)
		for(combination : TransformedSubterm.allCombinations(left,right)) {
			val l = combination.get(0)
			val r = combination.get(1)
			values += LogicSubterm::resolveToLogic(#[l,r],combinator.apply(l.expression, r.expression))
		}
		val res = createSMTOr =>[operands += values]
		return new LogicSubterm(res)
	}
	
	///////////////////////////////////////////////////////
	// Equals and Distinct
	///////////////////////////////////////////////////////
	
	def dispatch protected TransformedSubterm transformTerm(Equals equals, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		val left = equals.leftOperand.transformTerm(trace,variables)
		val rightX = equals.rightOperand.transformTerm(trace,variables)
		if(left instanceof LogicSubterm) {
			val right = rightX.expectLogic
			new LogicSubterm(createSMTEquals => [
				leftOperand = left.value
				rightOperand = right.value ])
		} else if(left instanceof NumericSubterm) {
			val right = rightX.expectNumber
			val leftOperands = left.possibleValues
			val rightOperands = right.possibleValues
			val values = new ArrayList(leftOperands.size * rightOperands.size)
			for(combination : TransformedSubterm.allCombinations(left.possibleValues,right.possibleValues)) {
				val l = combination.get(0)
				val r = combination.get(1)
				values += TransformedSubterm.resolveToLogic(#[l,r],
				createSMTEquals => [
					leftOperand = combination.get(0).expression
					rightOperand = combination.get(1).expression])
			}
			return new LogicSubterm(createSMTOr =>[operands += values])
		} else if(left instanceof ComplexSubterm){
			val right = rightX as ComplexSubterm
			
			val values = new LinkedList
			for(combination : TransformedSubterm.allCombinations(left.possibleValues,right.possibleValues)) {
				val l = combination.get(0)
				val r = combination.get(1)
				if(l.type.complexType == r.type.complexType) {
					values += TransformedSubterm.resolveToLogic(#[l,r],createSMTEquals => [
						leftOperand = l.expression
						rightOperand = r.expression ])
				} /*else dont add*/
			}
			
			if(values.size == 0) {
				return new LogicSubterm(createSMTBoolLiteral => [it.value = false])
			} else if(values.size == 1) {
				return new LogicSubterm(values.head)
			} else {
				return new LogicSubterm(createSMTOr => [operands += values])
			}
		}
	}
	
	def dispatch protected TransformedSubterm transformTerm(Distinct distinct, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		val o = distinct.operands.map[transformTerm(trace,variables)]
		if(o.empty) {
			throw new IllegalArgumentException('''empty distinct''')
		} else if(o.size == 1) {
			// 1 element is always distinct
			new LogicSubterm(createSMTBoolLiteral => [it.value = true])
		} else {
			val head = o.head
			if(head instanceof LogicSubterm) {
				return new LogicSubterm(createSMTDistinct => [
						it.operands += o.map[expectLogic.value]])
			} else if(head instanceof NumericSubterm) {
				val numbers = o.map[expectNumber.possibleValues]
				val distincts = new LinkedList
				for(combination : TransformedSubterm.allCombinations(numbers)) {
					distincts += LogicSubterm::resolveToLogic(combination,createSMTDistinct => [operands += combination.map[it.expression]])
				}
				new LogicSubterm(createSMTOr => [it.operands += distincts])
			} else {
				val objects = o.map[possibleValues]
				val distincts = new LinkedList
				for(combination : TransformedSubterm.allCombinations(objects)) {		
					val Map<SMTType,LinkedList<SubtermOption>> type2Terms = new LinkedHashMap;
					for(param:combination) {
						val type = param.type.complexType
						val value = param
						var LinkedList<SubtermOption> list;
						if(type2Terms.containsKey(type)) {
							list = type2Terms.get(type)
						} else {
							list = new LinkedList
							type2Terms.put(type,list)
						}
						list+=value
					}
					
					val groups = type2Terms.values.map[elementList|
						if(elementList.size == 1) return null
						else return LogicSubterm.resolveToLogic(elementList,createSMTDistinct => [it.operands += elementList.map[expression]])
					].filterNull
					if(groups.empty) {
						// One of the group is trivially satisfied
						return new LogicSubterm(createSMTBoolLiteral => [it.value = true])
					} else {
						val and = createSMTAnd => [operands += groups]
						distincts.add(and)
					}
				}
				if(distincts.size == 1) {
					return new LogicSubterm(distincts.head)
				} else {
					return new LogicSubterm(createSMTOr => [it.operands += distincts])
				}
			}
		}
	}
	
	///////////////////////////////////////////////////////
	// Quantifiers
	///////////////////////////////////////////////////////
	
	def dispatch protected TransformedSubterm transformTerm(Forall forall, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		new LogicSubterm(transformQuantifiedExpression(forall,trace,variables,
			[createSMTForall],
			[q|createSMTAnd=>[operands+=q]],
			[precondition,expression|createSMTImpl=>[leftOperand=precondition rightOperand=expression]]))
	}
	def dispatch protected TransformedSubterm transformTerm(Exists exists, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		new LogicSubterm(transformQuantifiedExpression(exists,trace,variables,
			[createSMTExists],
			[q|createSMTOr=>[operands+=q]],
			[precondition,expression|createSMTAnd=>[operands+=precondition operands+=expression]]))
	}
	
	def protected SMTTerm transformQuantifiedExpression(
		QuantifiedExpression q, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables,
		Function0<SMTQuantifiedExpression> constructor,
		Function1<Iterable<SMTQuantifiedExpression>,SMTTerm> combinator,
		Function2<SMTTerm,SMTTerm,SMTTerm> preconditionCombinator
	) {
		val permutations = unfolder.getPermutations(q.quantifiedVariables.map[it.range.transformTypeReference(trace)])
		val ArrayList<SMTQuantifiedExpression> unfoldedQuantification = new ArrayList(permutations.size)
		
		for(permutation : permutations) {
			val allVariables = new HashMap(variables)
			val newSMTVariables = new ArrayList(q.quantifiedVariables.size)
			val typePrecondition = new ArrayList<SMTTerm>(q.quantifiedVariables.size)
			
			for(variableIndex: 0..<q.quantifiedVariables.size) {
				val logicVariable = q.quantifiedVariables.get(variableIndex)
				val elementInPermutation = permutation.get(variableIndex)
				
				val newSMTVariable = createSMTSortedVariable => [
					name = logicVariable.name.toID
					range = elementInPermutation.type
				]
				allVariables.put(logicVariable, newSMTVariable)
				newSMTVariables+=newSMTVariable
				if(elementInPermutation.constraint != null) {
					typePrecondition += elementInPermutation.constraint.apply(newSMTVariable)
				}
			}
			
			val expressionOfQuantifiedFormula =
				if(typePrecondition.isEmpty)
					q.expression.transformTerm(trace,allVariables).expectLogic.value
				else if(typePrecondition.size == 1)
					preconditionCombinator.apply(
						typePrecondition.head,
						q.expression.transformTerm(trace,allVariables).expectLogic.value)
				else
					preconditionCombinator.apply(
						createSMTAnd => [it.operands += typePrecondition],
						q.expression.transformTerm(trace,allVariables).expectLogic.value)
			
			unfoldedQuantification += constructor.apply => [
				quantifiedVariables += newSMTVariables
				expression = expressionOfQuantifiedFormula
			]
			
//			if(newSMTVariables.exists[it.range == null]) {
//				println(newSMTVariables.filter[it.range == null].map[name])
//			}
		}
		
		if(permutations.size == 1) return unfoldedQuantification.head
		else return combinator.apply(unfoldedQuantification)
	}
	
	///////////////////////////////////////////////////////
	// If - Then - Else
	///////////////////////////////////////////////////////
	def dispatch protected TransformedSubterm transformTerm(IfThenElse ite, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		val condition = ite.condition.transformTerm(trace,variables).expectLogic.value
		val positiveTerm = ite.ifTrue.transformTerm(trace,variables)
		val positives = positiveTerm.possibleValues
		val negativeTerm = ite.ifFalse.transformTerm(trace,variables)
		val negatives = negativeTerm.possibleValues
		// Simple ITE
		if(positives.size == 1 && negatives.size == 1 && positives.head.type == negatives.head.type) {
			val t = positives.head.type
			if(t.isLogic) {
				return new LogicSubterm(createSMTITE => [
					it.condition = condition
					it.^if = positives.head.expression
					it.^else = negatives.head.expression])
			} else if(t.isNumeric) {
				return new NumericSubterm(
					(positives.head.variables + negatives.head.variables).toList,
					(positives.head.preconditions + negatives.head.preconditions).toList,
					createSMTITE => [
					it.condition = condition
					it.^if = positives.head.expression
					it.^else = negatives.head.expression
				])
			} else {
				return new ComplexSubterm(
					(positives.head.variables + negatives.head.variables).toList,
					(positives.head.preconditions + negatives.head.preconditions).toList,
					createSMTITE => [
						it.condition = condition
						it.^if = positives.head.expression
						it.^else = negatives.head.expression],
					t
				)
			}
		// else the ite need to be unfolded
		} else {
			if(positiveTerm instanceof LogicSubterm) {
				throw new AssertionError('''If the subterm has logic value it should be transformed as "Simple ITE""''')
			} else if (positiveTerm instanceof NumericSubterm){
				return new NumericSubterm(unfoldIte(positives, condition, negatives))
			} else {
				return new ComplexSubterm(unfoldIte(positives, condition, negatives))
			}
		}
	}
	
	private def List<SubtermOption> unfoldIte(List<SubtermOption> positives, SMTTerm condition, List<SubtermOption> negatives) {
		(positives.map[
			new SubtermOption(#[it],#[],#[condition],it.expression,it.type)
		] +
		negatives.map[
			new SubtermOption(#[it],#[],#[createSMTNot => [it.operand = condition]],it.expression,it.type)
		]).toList
	}
	
	///////////////////////////////////////////////////////
	// instanceof
	///////////////////////////////////////////////////////
	
	def dispatch protected TransformedSubterm transformTerm(InstanceOf i, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		val value = i.value.transformTerm(trace,variables)
		val range = i.range
		if(range instanceof BoolTypeReference) {
			return new LogicSubterm(createSMTBoolLiteral=>[it.value = (value instanceof LogicSubterm)])
		} else if(range instanceof IntTypeReference || range instanceof RealTypeReference) {
			return new LogicSubterm(createSMTBoolLiteral=>[it.value = (value instanceof NumericSubterm)])
		} else {
			val requestedTypes = this.typeMapper.transformTypeReference((range as ComplexTypeReference).referred,trace)
			val possileValues = value.possibleValues
			val options = new ArrayList(requestedTypes.size)
			for(typeConstraint : requestedTypes) {
				val possibleValue = possileValues.filter[it.type.complexType == (typeConstraint.type as SMTComplexTypeReference).referred].head
				if(possibleValue != null) {
					val x = if(typeConstraint.constraint != null ) {
						if(possibleValue.expression instanceof SMTSymbolicValue && (possibleValue.expression as SMTSymbolicValue).symbolicReference instanceof SMTSortedVariable) {
							val referred = (possibleValue.expression as SMTSymbolicValue).symbolicReference as SMTSortedVariable
							typeConstraint.constraint.apply(referred)
						} else {
							createSMTForall => [
								val v = createSMTSortedVariable => [it.range = EcoreUtil.copy(typeConstraint.type)]
								it.quantifiedVariables += v
								it.expression = createSMTImpl => [
									leftOperand = createSMTEquals => [
										it.leftOperand = possibleValue.expression
										it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = v]
									]
									rightOperand = typeConstraint.constraint.apply(v)
								]
							]
						}
					} else if(typeConstraint.constraint == null) {
						createSMTBoolLiteral => [it.value = true]
					}
					options += LogicSubterm::resolveToLogic(#[possibleValue],x)
				}
			}
			
			if(options.size == 0) {
				return new LogicSubterm(createSMTBoolLiteral=>[it.value = false])
			} else if(options.size == 1) {
				return new LogicSubterm(options.head)
			} else {
				return new LogicSubterm(createSMTOr => [it.operands += options])
			}
		}
		
	}
	
	///////////////////////////////////////////////////////
	// SymbolicReference
	///////////////////////////////////////////////////////
	
	def dispatch protected TransformedSubterm transformTerm(SymbolicValue symbolicValue, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		val referred = symbolicValue.symbolicReference
		val params = symbolicValue.parameterSubstitutions
		return transformSymbolicReference(referred,params,trace,variables)
	}
	
	def dispatch protected TransformedSubterm transformSymbolicReference(Relation referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		val parameters = parameterSubstitution.map[transformTerm(it,trace,variables)]
		val list = new LinkedList
		for(combination : TransformedSubterm.allCombinations(parameters.map[it.possibleValues])) {
			val descriptor = new Descriptor(combination.map[it.type],referred)
			val targetRelation = descriptor.lookup(trace.relationMap)
			if(targetRelation == null) {
				throw new AssertionError('''target relation should not be null (yet)''')
			
			} else {
				list += TransformedSubterm.resolveToLogic(combination,createSMTSymbolicValue => [
					it.symbolicReference = targetRelation
					it.parameterSubstitutions += combination.map[it.expression]
				])
			}
		}
		
		if(list.size == 1) {
			return new LogicSubterm(list.head)
		} else {
			return new LogicSubterm(createSMTOr => [ operands += list ])
		}
	}
	
	
	def dispatch protected TransformedSubterm transformSymbolicReference(Function referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		throw new UnsupportedOperationException
	}
	
	def dispatch protected TransformedSubterm transformSymbolicReference(Variable referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		if(!variables.containsKey(referred)) {
			val container = referred.eContainer
			println("X" + container)
			for(v : variables.keySet) {
				println(v)
				println("in " +v.eContainer)
			}
			return null
		}
		val v = referred.lookup(variables)
		
		val expression = createSMTSymbolicValue => [it.symbolicReference = v]
		if(v.range instanceof SMTBoolTypeReference) {
			return new LogicSubterm(expression)
		} else if(v.range instanceof SMTIntTypeReference || v.range instanceof SMTRealTypeReference) {
			return new NumericSubterm(#[],#[],expression)
		} else {
			return new ComplexSubterm(#[],#[],expression,
				new TypeDescriptor((v.range as SMTComplexTypeReference).referred));
		}
	}
	
	def dispatch protected TransformedSubterm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		this.typeMapper.transformSymbolicReference(referred,trace)
	}
	
	def dispatch protected TransformedSubterm transformSymbolicReference(Void referred, List<Term> parameterSubstitution, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		throw new NullPointerException('''unfilled symbolic reference!''')
	}
	
	///////////
	
	/*def transformContainment(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) {
		val containmentRelation_oo = createSMTFunctionDefinition=>[
			it.name="containment!oo"
			it.range=createSMTBoolTypeReference
			val child = createSMTSortedVariable => [
				it.name = 
			]
		]
	}*/
	
	///////////
	
	def cleanDocument(SMTDocument document) {
		val content = document.eAllContents.toList
		for(object:content) {
			for(containmentReference : object.eClass.EAllReferences.filter[containment]) {
				val child = object.eGet(containmentReference) {
					if(child!=null) {
						if(containmentReference.isMany) {
							val list = child as List<EObject>
							for(index : 0..<list.size) {
								val single = list.get(index)
								val newSingle = replaceWith(single)
								if(newSingle!=null) {
									list.set(index,newSingle)
								}
							}
						} else {
							val single = child as EObject
							val newSingle = replaceWith(single)
							if(newSingle!=null) {
								object.eSet(containmentReference,newSingle)
							}
						}
					}
				}
			}
		}
	}
	def private dispatch replaceWith(SMTOr or) {
		if(or.operands.empty) {
			return createSMTBoolLiteral => [it.value = false]
		} else return null
	}
	def private dispatch replaceWith(SMTAnd and) {
		if(and.operands.empty) {
			return createSMTBoolLiteral => [it.value = true]
		} else return null
	}
	def private dispatch replaceWith(EObject object)  {
		null
	}
}