From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- .../unused/Logic2AlloyApiMapper.xtend_ | 345 +++++++++++++++++++++ 1 file changed, 345 insertions(+) create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_') 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 typeDeclarations=new ArrayList + public val List functionDeclarations=new ArrayList + public val List assertions=new ArrayList + public val List multiplicityConstraints=new ArrayList + public val List inverseConstraints=new ArrayList +} + +class Logic2AlloyApiMapperTrace { + val Map typeMap + val Map elementMap + //val Map functionMap + val Map relationMap + //val Map constantMap + + new () { + this.typeMap = new HashMap + this.elementMap = new HashMap + //this.functionMap = new HashMap + this.relationMap = new HashMap + //this.constantMap = new HashMap + } + new (Map typeMap, + Map elementMap, + //Map functionMap, + Map relationMap/*, + Map 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, Logic2AlloyApiMapperTrace> transformProblem(LogicProblem problem) { + val documentInput = new AlloyInput() + //createSMTInput => [satCommand = createSMTSimpleSatCommand getModelCommand = createSMTGetModelCommand] + //val document = createSMTDocument => [input = documentInput] + val List 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 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 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 variables) { + return ExprConstant.makeNUMBER(literal.value) + } + def dispatch protected Expr transformTerm(RealLiteral literal, Logic2AlloyApiMapperTrace trace, Map variables) { + throw new UnsupportedOperationException("Real number is not supported") + } + def dispatch protected Expr transformTerm(Not not, Logic2AlloyApiMapperTrace trace, Map variables) { + return not.operand.transformTerm(trace,variables).not} + def dispatch protected Expr transformTerm(And and, Logic2AlloyApiMapperTrace trace, Map variables) { + val List 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 variables) { + val List 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 variables) { + return impl.leftOperand.transformTerm(trace,variables).implies(impl.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Iff ifExpression, Logic2AlloyApiMapperTrace trace, Map variables) { + return ifExpression.leftOperand.transformTerm(trace,variables).iff(ifExpression.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(MoreThan moreThan, Logic2AlloyApiMapperTrace trace, Map variables) { + return moreThan.leftOperand.transformTerm(trace,variables).gt(moreThan.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(LessThan lessThan, Logic2AlloyApiMapperTrace trace, Map variables) { + return lessThan.leftOperand.transformTerm(trace,variables).lt(lessThan.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(MoreOrEqualThan moreThan, Logic2AlloyApiMapperTrace trace, Map variables) { + return moreThan.leftOperand.transformTerm(trace,variables).gte(moreThan.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(LessOrEqualThan lessThan, Logic2AlloyApiMapperTrace trace, Map variables) { + return lessThan.leftOperand.transformTerm(trace,variables).lte(lessThan.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Equals equals, Logic2AlloyApiMapperTrace trace, Map variables) { + return equals.leftOperand.transformTerm(trace,variables).equal(equals.rightOperand.transformTerm(trace,variables)) + } + /*def dispatch protected Expr transformTerm(Distinct distinct, Logic2AlloyApiMapperTrace trace, Map variables) { + createSMTDistinct => [ operands += distinct.operands.map[transformTerm(trace,variables)]]}*/ + def dispatch protected Expr transformTerm(Plus plus, Logic2AlloyApiMapperTrace trace, Map variables) { + return plus.leftOperand.transformTerm(trace,variables).plus(plus.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Minus minus, Logic2AlloyApiMapperTrace trace, Map variables) { + return minus.leftOperand.transformTerm(trace,variables).minus(minus.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Multiply multiply, Logic2AlloyApiMapperTrace trace, Map variables) { + return multiply.leftOperand.transformTerm(trace,variables).mul(multiply.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Divison div, Logic2AlloyApiMapperTrace trace, Map variables) { + return div.leftOperand.transformTerm(trace,variables).div(div.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Mod mod, Logic2AlloyApiMapperTrace trace, Map variables) { + throw new UnsupportedOperationException("Modulo is not supported.") + } + def dispatch protected Expr transformTerm(Forall forall, Logic2AlloyApiMapperTrace trace, Map variables) { + return configureForall(forall,trace,variables) + } + def dispatch protected Expr transformTerm(Exists exists, Logic2AlloyApiMapperTrace trace, Map variables) { + return configureExists(exists,trace,variables) + } + def dispatch protected Expr transformTerm(SymbolicValue symbolicValue, Logic2AlloyApiMapperTrace trace, Map variables) { + symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } + + def private configureForall( + Forall quantifiedExpression, + Logic2AlloyApiMapperTrace trace, Map variables) + { + val allVariables = new HashMap(variables) + val newAlloyVariables = new ArrayList(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 variables) + { + val allVariables = new HashMap(variables) + val newAlloyVariables = new ArrayList(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 parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map variables) { + return trace.elements.get(referred) + } + def dispatch protected Expr transformSymbolicReference(Variable variable, List parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map variables) { + return variables.get(variable).get + } + /*def dispatch protected Expr transformSymbolicReference(Function function, List parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map 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 parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map variables) { + return trace.relations.get(relation) + } + def dispatch protected Expr transformSymbolicReference(Constant constant, List parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map variables) { + //createSMTSymbolicValue => [symbolicReference = trace.constants.get(constant)] + throw new UnsupportedOperationException("Constant is not supported") + } +} \ No newline at end of file -- cgit v1.2.3-54-g00ecf