1 files changed, 345 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_
new file mode 100644
index 00000000..29acd681
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_
@@ -0,0 +1,345 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import java.util.Map
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import java.util.List
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant
+import edu.mit.csail.sdg.alloy4compiler.ast.Expr
+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.IntLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
+import java.util.HashMap
+import edu.mit.csail.sdg.alloy4compiler.ast.Decl
+import java.util.ArrayList
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import edu.mit.csail.sdg.alloy4compiler.ast.Attr
+import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import javax.naming.OperationNotSupportedException
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.AlloySpecification
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.Multiplicity
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.InverseReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+class AlloyInput{
+        public val List<PrimSig> typeDeclarations=new ArrayList
+        public val List<Expr> functionDeclarations=new ArrayList
+        public val List<Expr> assertions=new ArrayList
+        public val List<Expr> multiplicityConstraints=new ArrayList
+        public val List<Expr> inverseConstraints=new ArrayList
+}
+class Logic2AlloyApiMapperTrace {
+        val Map<Type, PrimSig> typeMap
+        val Map<DefinedElement, PrimSig> elementMap
+        //val Map<Function, SMTFunctionDeclaration> functionMap
+        val Map<Relation,Expr> relationMap
+        //val Map<Constant,SMTFunctionDeclaration> constantMap
+        
+        new () {
+                this.typeMap = new HashMap
+                this.elementMap = new HashMap
+                //this.functionMap = new HashMap
+                this.relationMap = new HashMap
+                //this.constantMap = new HashMap
+        }
+        new (Map<Type, PrimSig> typeMap,
+                 Map<DefinedElement, PrimSig> elementMap,
+                 //Map<Function, SMTFunctionDeclaration> functionMap,
+                 Map<Relation,Expr> relationMap/*,
+                 Map<Constant,SMTFunctionDeclaration> constantMap*/)
+        {
+                this.typeMap = typeMap
+                this.elementMap = elementMap
+                //this.functionMap = functionMap
+                this.relationMap = relationMap
+                //this.constantMap = constantMap
+        }
+        
+        def types() { typeMap }
+        def elements() { elementMap }
+        //def functions() { functionMap }
+        def relations() { relationMap }
+        //def constants() { constantMap }
+}
+class Logic2AlloyApiMapper{
+        //TODO output
+        public def TracedOutput<List<PrimSig>, Logic2AlloyApiMapperTrace> transformProblem(LogicProblem problem) {
+                val documentInput = new AlloyInput()
+                //createSMTInput => [satCommand = createSMTSimpleSatCommand getModelCommand = createSMTGetModelCommand]
+                //val document = createSMTDocument => [input = documentInput]
+                val List<PrimSig> document=new ArrayList
+                val trace = new Logic2AlloyApiMapperTrace
+                
+                // Trafo
+                documentInput.typeDeclarations          += problem.types.map[transformType(trace)]
+                //documentInput.functionDeclarations    += problem.functions.map[transformFunction(trace)]
+                documentInput.functionDeclarations      += problem.relations.map[transformRelation(trace)]
+                //documentInput.functionDeclarations    += problem.constants.map[transformConstant(trace)]
+                documentInput.assertions                        += problem.assertions.map[transformAssertion(trace)]
+                
+                
+                val alloySpecification = problem.specifications.filter(AlloySpecification).head
+                
+                for(mult: alloySpecification.multiplicities){
+                        if(mult.min>0){
+                                documentInput.multiplicityConstraints+=mult.transformMultiplicityLowerBound(trace)
+                        }
+                        if(mult.max!=-1){
+                                documentInput.multiplicityConstraints+=mult.transformMultiplicityUpperBound(trace)
+                        }
+                }
+                
+                for(inv: alloySpecification.inverses){
+                        documentInput.inverseConstraints += inv.transformInverse(trace)
+                }
+                // End trafo
+                
+                return new TracedOutput(document,trace)
+        }
+        
+        def Expr transformMultiplicityLowerBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){
+                
+                val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl
+                return (forallVariable.get.cardinality.gte(ExprConstant.makeNUMBER(multiplicity.min))).forAll(forallVariable)
+                
+        }
+        
+        def Expr transformMultiplicityUpperBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){
+                
+                val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl
+                return (forallVariable.get.cardinality.lte(ExprConstant.makeNUMBER(multiplicity.max))).forAll(forallVariable)
+                
+        }
+        
+        def Expr transformInverse(InverseReference inverse, Logic2AlloyApiMapperTrace trace){
+                return trace.relations.get(inverse.inverseOf.get(0)).equal(trace.relations.get(inverse.inverseOf.get(1)).transpose)     
+        }
+        
+        private def toID(List<String> names) {names.join("!") }
+        
+        def dispatch protected transformType(TypeDefinition declaration, Logic2AlloyApiMapperTrace trace) {
+                val result = new PrimSig(declaration.name.toID, Attr.ABSTRACT)
+                trace.types.put(declaration,result)
+                return result
+        }
+        
+        def protected transformDefinedElement(TypeDefinition enumType, DefinedElement element, Logic2AlloyApiMapperTrace trace) {
+                val result=new PrimSig(element.name.toID, trace.types.get(enumType), Attr.ONE)
+                trace.elements.put(element,result)
+                return result
+        }
+                
+        def dispatch protected transformType(TypeDeclaration declaration, Logic2AlloyApiMapperTrace trace) {
+                //TODO �r�kles, absztrakt
+                val result = new PrimSig(declaration.name.toID)
+                trace.types.put(declaration,result)
+                return result
+        }
+        
+        def dispatch protected transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyApiMapperTrace trace) {
+                throw new UnsupportedOperationException("BoolTypeReference is not supported.")
+        }
+        def dispatch protected transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyApiMapperTrace trace) {
+                return PrimSig.SIGINT
+        }
+        def dispatch protected transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyApiMapperTrace trace) {
+                throw new UnsupportedOperationException("RealTypeReference is not supported.")
+        }
+        def dispatch protected PrimSig transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyApiMapperTrace trace) {
+                return trace.types.get(complexTypeReference.referred)
+        }
+        
+        /*def protected transformFunction(Function declaration, Logic2AlloyApiMapperTrace trace) {
+                val functionDeclaration = createSMTFunctionDeclaration => [
+                        name = declaration.name.toID
+                        range = declaration.range.transformTypeReference(trace)
+                        parameters+= declaration.parameters.map[transformTypeReference(trace)]
+                ]
+                trace.functions.put(declaration,functionDeclaration)
+                return functionDeclaration
+        }*/
+        
+        def transformRelation(Relation relation, Logic2AlloyApiMapperTrace trace) {
+                if(relation.parameters.size==2){
+                        trace.relations.put(relation,(relation.parameters.get(0).transformTypeReference(trace) as PrimSig).addField(relation.name.toID, (relation.parameters.get(1).transformTypeReference(trace) as PrimSig).setOf))
+                } else{
+                        throw new OperationNotSupportedException("More parameters are not supported.")
+                } 
+        }
+        
+        /*def transformConstant(Constant constant, Logic2AlloyApiMapperTrace trace) {
+                val smtConstant = createSMTFunctionDeclaration => [
+                        name = constant.name.toID
+                        range = transformTypeReference(constant.type, trace)
+                ]
+                trace.constants.put(constant,smtConstant)
+                return smtConstant
+        }*/
+        
+        def protected Expr transformAssertion(Assertion assertion, Logic2AlloyApiMapperTrace trace) {
+                
+                return assertion.value.transformTerm(trace,emptyMap)
+        }
+        
+        def dispatch protected Expr transformTerm(BoolLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                throw new UnsupportedOperationException("Bool is not supported")
+                //open util/boolean, autoPay: Bool
+                //https://code.google.com/p/valloy2009/source/browse/trunk/src/models/util/boolean.als?r=142
+        }
+        def dispatch protected Expr transformTerm(IntLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)  {
+                return ExprConstant.makeNUMBER(literal.value)
+        }
+        def dispatch protected Expr transformTerm(RealLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                throw new UnsupportedOperationException("Real number is not supported")
+        }
+        def dispatch protected Expr transformTerm(Not not, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return not.operand.transformTerm(trace,variables).not}
+        def dispatch protected Expr transformTerm(And and, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                val List<Expr> operands= and.operands.map[transformTerm(trace,variables)]
+                var andTerm=operands.get(0)
+                for(Integer i: 1..(operands.size-1)){
+                        andTerm=andTerm.and(operands.get(i))
+                }
+                return andTerm
+        }
+        def dispatch protected Expr transformTerm(Or or, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                val List<Expr> operands= or.operands.map[transformTerm(trace,variables)]
+                var orTerm=operands.get(0)
+                for(Integer i: 1..(operands.size-1)){
+                        orTerm=orTerm.or(operands.get(i))
+                }
+                return orTerm
+        }
+        def dispatch protected Expr transformTerm(Impl impl, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return impl.leftOperand.transformTerm(trace,variables).implies(impl.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Iff ifExpression, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return ifExpression.leftOperand.transformTerm(trace,variables).iff(ifExpression.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(MoreThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return moreThan.leftOperand.transformTerm(trace,variables).gt(moreThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(LessThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return lessThan.leftOperand.transformTerm(trace,variables).lt(lessThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(MoreOrEqualThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return moreThan.leftOperand.transformTerm(trace,variables).gte(moreThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(LessOrEqualThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return lessThan.leftOperand.transformTerm(trace,variables).lte(lessThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Equals equals, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return equals.leftOperand.transformTerm(trace,variables).equal(equals.rightOperand.transformTerm(trace,variables))
+        }
+        /*def dispatch protected Expr transformTerm(Distinct distinct, Logic2AlloyApiMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                createSMTDistinct => [ operands += distinct.operands.map[transformTerm(trace,variables)]]}*/
+        def dispatch protected Expr transformTerm(Plus plus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return plus.leftOperand.transformTerm(trace,variables).plus(plus.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Minus minus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return minus.leftOperand.transformTerm(trace,variables).minus(minus.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Multiply multiply, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return multiply.leftOperand.transformTerm(trace,variables).mul(multiply.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Divison div, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return div.leftOperand.transformTerm(trace,variables).div(div.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Mod mod, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                throw new UnsupportedOperationException("Modulo is not supported.")
+        }
+        def dispatch protected Expr transformTerm(Forall forall, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return configureForall(forall,trace,variables) 
+        }
+        def dispatch protected Expr transformTerm(Exists exists, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return configureExists(exists,trace,variables)
+        }
+        def dispatch protected Expr transformTerm(SymbolicValue symbolicValue, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) }
+        
+        def private configureForall(
+                Forall quantifiedExpression,
+                Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)
+        {
+                val allVariables = new HashMap(variables)
+                val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size)
+                
+                for(logicVariable: quantifiedExpression.quantifiedVariables) {
+                        val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl
+                        allVariables.put(logicVariable, newAlloyVariable)
+                        newAlloyVariables += newAlloyVariable
+                }
+                val variable0=newAlloyVariables.get(0)
+                newAlloyVariables.remove(0)
+                return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forAll(variable0, newAlloyVariables)
+        }
+        
+        def private configureExists(
+                Exists quantifiedExpression,
+                Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)
+        {
+                val allVariables = new HashMap(variables)
+                val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size)
+                
+                for(logicVariable: quantifiedExpression.quantifiedVariables) {
+                        val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl
+                        allVariables.put(logicVariable, newAlloyVariable)
+                        newAlloyVariables += newAlloyVariable
+                }
+                val variable0=newAlloyVariables.get(0)
+                newAlloyVariables.remove(0)
+                return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forSome(variable0, newAlloyVariables)
+        }
+        
+        def dispatch protected Expr transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return trace.elements.get(referred)
+        }
+        def dispatch protected Expr transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return variables.get(variable).get
+        }
+        /*def dispatch protected Expr transformSymbolicReference(Function function, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                val result = createSMTSymbolicValue => [sv | sv.symbolicReference = trace.functions.get(function)]
+                for(paramSubstitution : parameterSubstitutions) {
+                        result.parameterSubstitutions.add(paramSubstitution.transformTerm(trace,variables))
+                }
+                return result
+        }*/
+        def dispatch protected Expr transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return trace.relations.get(relation)
+        }
+        def dispatch protected Expr transformSymbolicReference(Constant constant, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                //createSMTSymbolicValue => [symbolicReference = trace.constants.get(constant)]
+                throw new UnsupportedOperationException("Constant is not supported")
+        }
+}
+\ No newline at end of file

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ new file mode 100644 index 00000000..29acd681 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_
@@ -0,0 +1,345 @@
	1	package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
	2
	3	import java.util.Map
	4	import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
	5	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
	6	import java.util.List
	7	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
	8	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
	9	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
	10	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
	11	import edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant
	12	import edu.mit.csail.sdg.alloy4compiler.ast.Expr
	13	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
	14	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
	15	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
	16	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
	17	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
	18	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
	19	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
	20	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
	21	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
	22	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan
	23	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan
	24	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan
	25	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan
	26	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
	27	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus
	28	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus
	29	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply
	30	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison
	31	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod
	32	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
	33	import java.util.HashMap
	34	import edu.mit.csail.sdg.alloy4compiler.ast.Decl
	35	import java.util.ArrayList
	36	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
	37	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
	38	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
	39	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
	40	import edu.mit.csail.sdg.alloy4compiler.ast.Attr
	41	import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig
	42	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
	43	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
	44	import javax.naming.OperationNotSupportedException
	45	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
	46	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
	47	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.AlloySpecification
	48	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.Multiplicity
	49	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.InverseReference
	50	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
	51	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
	52
	53	class AlloyInput{
	54	public val List<PrimSig> typeDeclarations=new ArrayList
	55	public val List<Expr> functionDeclarations=new ArrayList
	56	public val List<Expr> assertions=new ArrayList
	57	public val List<Expr> multiplicityConstraints=new ArrayList
	58	public val List<Expr> inverseConstraints=new ArrayList
	59	}
	60
	61	class Logic2AlloyApiMapperTrace {
	62	val Map<Type, PrimSig> typeMap
	63	val Map<DefinedElement, PrimSig> elementMap
	64	//val Map<Function, SMTFunctionDeclaration> functionMap
	65	val Map<Relation,Expr> relationMap
	66	//val Map<Constant,SMTFunctionDeclaration> constantMap
	67
	68	new () {
	69	this.typeMap = new HashMap
	70	this.elementMap = new HashMap
	71	//this.functionMap = new HashMap
	72	this.relationMap = new HashMap
	73	//this.constantMap = new HashMap
	74	}
	75	new (Map<Type, PrimSig> typeMap,
	76	Map<DefinedElement, PrimSig> elementMap,
	77	//Map<Function, SMTFunctionDeclaration> functionMap,
	78	Map<Relation,Expr> relationMap/*,
	79	Map<Constant,SMTFunctionDeclaration> constantMap*/)
	80	{
	81	this.typeMap = typeMap
	82	this.elementMap = elementMap
	83	//this.functionMap = functionMap
	84	this.relationMap = relationMap
	85	//this.constantMap = constantMap
	86	}
	87
	88	def types() { typeMap }
	89	def elements() { elementMap }
	90	//def functions() { functionMap }
	91	def relations() { relationMap }
	92	//def constants() { constantMap }
	93	}
	94
	95	class Logic2AlloyApiMapper{
	96	//TODO output
	97	public def TracedOutput<List<PrimSig>, Logic2AlloyApiMapperTrace> transformProblem(LogicProblem problem) {
	98	val documentInput = new AlloyInput()
	99	//createSMTInput => [satCommand = createSMTSimpleSatCommand getModelCommand = createSMTGetModelCommand]
	100	//val document = createSMTDocument => [input = documentInput]
	101	val List<PrimSig> document=new ArrayList
	102	val trace = new Logic2AlloyApiMapperTrace
	103
	104	// Trafo
	105	documentInput.typeDeclarations += problem.types.map[transformType(trace)]
	106	//documentInput.functionDeclarations += problem.functions.map[transformFunction(trace)]
	107	documentInput.functionDeclarations += problem.relations.map[transformRelation(trace)]
	108	//documentInput.functionDeclarations += problem.constants.map[transformConstant(trace)]
	109	documentInput.assertions += problem.assertions.map[transformAssertion(trace)]
	110
	111
	112	val alloySpecification = problem.specifications.filter(AlloySpecification).head
	113
	114	for(mult: alloySpecification.multiplicities){
	115	if(mult.min>0){
	116	documentInput.multiplicityConstraints+=mult.transformMultiplicityLowerBound(trace)
	117	}
	118	if(mult.max!=-1){
	119	documentInput.multiplicityConstraints+=mult.transformMultiplicityUpperBound(trace)
	120	}
	121	}
	122
	123	for(inv: alloySpecification.inverses){
	124	documentInput.inverseConstraints += inv.transformInverse(trace)
	125	}
	126	// End trafo
	127
	128	return new TracedOutput(document,trace)
	129	}
	130
	131	def Expr transformMultiplicityLowerBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){
	132
	133	val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl
	134	return (forallVariable.get.cardinality.gte(ExprConstant.makeNUMBER(multiplicity.min))).forAll(forallVariable)
	135
	136	}
	137
	138	def Expr transformMultiplicityUpperBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){
	139
	140	val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl
	141	return (forallVariable.get.cardinality.lte(ExprConstant.makeNUMBER(multiplicity.max))).forAll(forallVariable)
	142
	143	}
	144
	145	def Expr transformInverse(InverseReference inverse, Logic2AlloyApiMapperTrace trace){
	146	return trace.relations.get(inverse.inverseOf.get(0)).equal(trace.relations.get(inverse.inverseOf.get(1)).transpose)
	147	}
	148
	149	private def toID(List<String> names) {names.join("!") }
	150
	151	def dispatch protected transformType(TypeDefinition declaration, Logic2AlloyApiMapperTrace trace) {
	152	val result = new PrimSig(declaration.name.toID, Attr.ABSTRACT)
	153	trace.types.put(declaration,result)
	154	return result
	155	}
	156
	157	def protected transformDefinedElement(TypeDefinition enumType, DefinedElement element, Logic2AlloyApiMapperTrace trace) {
	158	val result=new PrimSig(element.name.toID, trace.types.get(enumType), Attr.ONE)
	159	trace.elements.put(element,result)
	160	return result
	161	}
	162
	163	def dispatch protected transformType(TypeDeclaration declaration, Logic2AlloyApiMapperTrace trace) {
	164	//TODO �r�kles, absztrakt
	165	val result = new PrimSig(declaration.name.toID)
	166	trace.types.put(declaration,result)
	167	return result
	168	}
	169
	170	def dispatch protected transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyApiMapperTrace trace) {
	171	throw new UnsupportedOperationException("BoolTypeReference is not supported.")
	172	}
	173	def dispatch protected transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyApiMapperTrace trace) {
	174	return PrimSig.SIGINT
	175	}
	176	def dispatch protected transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyApiMapperTrace trace) {
	177	throw new UnsupportedOperationException("RealTypeReference is not supported.")
	178	}
	179	def dispatch protected PrimSig transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyApiMapperTrace trace) {
	180	return trace.types.get(complexTypeReference.referred)
	181	}
	182
	183	/*def protected transformFunction(Function declaration, Logic2AlloyApiMapperTrace trace) {
	184	val functionDeclaration = createSMTFunctionDeclaration => [
	185	name = declaration.name.toID
	186	range = declaration.range.transformTypeReference(trace)
	187	parameters+= declaration.parameters.map[transformTypeReference(trace)]
	188	]
	189	trace.functions.put(declaration,functionDeclaration)
	190	return functionDeclaration
	191	}*/
	192
	193	def transformRelation(Relation relation, Logic2AlloyApiMapperTrace trace) {
	194	if(relation.parameters.size==2){
	195	trace.relations.put(relation,(relation.parameters.get(0).transformTypeReference(trace) as PrimSig).addField(relation.name.toID, (relation.parameters.get(1).transformTypeReference(trace) as PrimSig).setOf))
	196	} else{
	197	throw new OperationNotSupportedException("More parameters are not supported.")
	198	}
	199	}
	200
	201	/*def transformConstant(Constant constant, Logic2AlloyApiMapperTrace trace) {
	202	val smtConstant = createSMTFunctionDeclaration => [
	203	name = constant.name.toID
	204	range = transformTypeReference(constant.type, trace)
	205	]
	206	trace.constants.put(constant,smtConstant)
	207	return smtConstant
	208	}*/
	209
	210	def protected Expr transformAssertion(Assertion assertion, Logic2AlloyApiMapperTrace trace) {
	211
	212	return assertion.value.transformTerm(trace,emptyMap)
	213	}
	214
	215	def dispatch protected Expr transformTerm(BoolLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	216	throw new UnsupportedOperationException("Bool is not supported")
	217	//open util/boolean, autoPay: Bool
	218	//https://code.google.com/p/valloy2009/source/browse/trunk/src/models/util/boolean.als?r=142
	219	}
	220	def dispatch protected Expr transformTerm(IntLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	221	return ExprConstant.makeNUMBER(literal.value)
	222	}
	223	def dispatch protected Expr transformTerm(RealLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	224	throw new UnsupportedOperationException("Real number is not supported")
	225	}
	226	def dispatch protected Expr transformTerm(Not not, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	227	return not.operand.transformTerm(trace,variables).not}
	228	def dispatch protected Expr transformTerm(And and, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	229	val List<Expr> operands= and.operands.map[transformTerm(trace,variables)]
	230	var andTerm=operands.get(0)
	231	for(Integer i: 1..(operands.size-1)){
	232	andTerm=andTerm.and(operands.get(i))
	233	}
	234	return andTerm
	235	}
	236	def dispatch protected Expr transformTerm(Or or, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	237	val List<Expr> operands= or.operands.map[transformTerm(trace,variables)]
	238	var orTerm=operands.get(0)
	239	for(Integer i: 1..(operands.size-1)){
	240	orTerm=orTerm.or(operands.get(i))
	241	}
	242	return orTerm
	243	}
	244	def dispatch protected Expr transformTerm(Impl impl, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	245	return impl.leftOperand.transformTerm(trace,variables).implies(impl.rightOperand.transformTerm(trace,variables))
	246	}
	247	def dispatch protected Expr transformTerm(Iff ifExpression, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	248	return ifExpression.leftOperand.transformTerm(trace,variables).iff(ifExpression.rightOperand.transformTerm(trace,variables))
	249	}
	250	def dispatch protected Expr transformTerm(MoreThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	251	return moreThan.leftOperand.transformTerm(trace,variables).gt(moreThan.rightOperand.transformTerm(trace,variables))
	252	}
	253	def dispatch protected Expr transformTerm(LessThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	254	return lessThan.leftOperand.transformTerm(trace,variables).lt(lessThan.rightOperand.transformTerm(trace,variables))
	255	}
	256	def dispatch protected Expr transformTerm(MoreOrEqualThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	257	return moreThan.leftOperand.transformTerm(trace,variables).gte(moreThan.rightOperand.transformTerm(trace,variables))
	258	}
	259	def dispatch protected Expr transformTerm(LessOrEqualThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	260	return lessThan.leftOperand.transformTerm(trace,variables).lte(lessThan.rightOperand.transformTerm(trace,variables))
	261	}
	262	def dispatch protected Expr transformTerm(Equals equals, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	263	return equals.leftOperand.transformTerm(trace,variables).equal(equals.rightOperand.transformTerm(trace,variables))
	264	}
	265	/*def dispatch protected Expr transformTerm(Distinct distinct, Logic2AlloyApiMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
	266	createSMTDistinct => [ operands += distinct.operands.map[transformTerm(trace,variables)]]}*/
	267	def dispatch protected Expr transformTerm(Plus plus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	268	return plus.leftOperand.transformTerm(trace,variables).plus(plus.rightOperand.transformTerm(trace,variables))
	269	}
	270	def dispatch protected Expr transformTerm(Minus minus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	271	return minus.leftOperand.transformTerm(trace,variables).minus(minus.rightOperand.transformTerm(trace,variables))
	272	}
	273	def dispatch protected Expr transformTerm(Multiply multiply, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	274	return multiply.leftOperand.transformTerm(trace,variables).mul(multiply.rightOperand.transformTerm(trace,variables))
	275	}
	276	def dispatch protected Expr transformTerm(Divison div, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	277	return div.leftOperand.transformTerm(trace,variables).div(div.rightOperand.transformTerm(trace,variables))
	278	}
	279	def dispatch protected Expr transformTerm(Mod mod, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	280	throw new UnsupportedOperationException("Modulo is not supported.")
	281	}
	282	def dispatch protected Expr transformTerm(Forall forall, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	283	return configureForall(forall,trace,variables)
	284	}
	285	def dispatch protected Expr transformTerm(Exists exists, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	286	return configureExists(exists,trace,variables)
	287	}
	288	def dispatch protected Expr transformTerm(SymbolicValue symbolicValue, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	289	symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) }
	290
	291	def private configureForall(
	292	Forall quantifiedExpression,
	293	Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)
	294	{
	295	val allVariables = new HashMap(variables)
	296	val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size)
	297
	298	for(logicVariable: quantifiedExpression.quantifiedVariables) {
	299	val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl
	300	allVariables.put(logicVariable, newAlloyVariable)
	301	newAlloyVariables += newAlloyVariable
	302	}
	303	val variable0=newAlloyVariables.get(0)
	304	newAlloyVariables.remove(0)
	305	return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forAll(variable0, newAlloyVariables)
	306	}
	307
	308	def private configureExists(
	309	Exists quantifiedExpression,
	310	Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)
	311	{
	312	val allVariables = new HashMap(variables)
	313	val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size)
	314
	315	for(logicVariable: quantifiedExpression.quantifiedVariables) {
	316	val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl
	317	allVariables.put(logicVariable, newAlloyVariable)
	318	newAlloyVariables += newAlloyVariable
	319	}
	320	val variable0=newAlloyVariables.get(0)
	321	newAlloyVariables.remove(0)
	322	return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forSome(variable0, newAlloyVariables)
	323	}
	324
	325	def dispatch protected Expr transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	326	return trace.elements.get(referred)
	327	}
	328	def dispatch protected Expr transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	329	return variables.get(variable).get
	330	}
	331	/*def dispatch protected Expr transformSymbolicReference(Function function, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	332	val result = createSMTSymbolicValue => [sv \| sv.symbolicReference = trace.functions.get(function)]
	333	for(paramSubstitution : parameterSubstitutions) {
	334	result.parameterSubstitutions.add(paramSubstitution.transformTerm(trace,variables))
	335	}
	336	return result
	337	}*/
	338	def dispatch protected Expr transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	339	return trace.relations.get(relation)
	340	}
	341	def dispatch protected Expr transformSymbolicReference(Constant constant, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
	342	//createSMTSymbolicValue => [symbolicReference = trace.constants.get(constant)]
	343	throw new UnsupportedOperationException("Constant is not supported")
	344	}
	345	} \ No newline at end of file