From 9152a660dbfbf3294964233c76d6cf22111298ff Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 9 Jul 2019 20:49:10 +0200 Subject: aggregated partial substitution + builder --- .../logic/model/builder/LogicProblemBuilder.xtend | 261 ++++++++++++--------- 1 file changed, 151 insertions(+), 110 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend index f6bd9541..09bfbb39 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend @@ -1,5 +1,6 @@ package hu.bme.mit.inf.dslreasoner.logic.model.builder +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.AggregateExpression import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference @@ -8,6 +9,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ProjectedAggregateExpression import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation @@ -46,16 +48,16 @@ class LogicProblemBuilderException extends Exception { } } -public class LogicProblemBuilder{ +class LogicProblemBuilder{ val protected extension LogiclanguageFactory logicFactiory = LogiclanguageFactory.eINSTANCE val protected extension LogicproblemFactory problemFactory = LogicproblemFactory.eINSTANCE val protected advancedConstructs = new LogicProblemBuilder_AdvancedConstructs(this) - def public createProblem(){ createLogicProblem } + def createProblem(){ createLogicProblem } // Names def protected String canonize(CharSequence name) { - if(name == null) return "" + if(name === null) return "" val result = name.toString.split("\\s+"); if(result.size == 1) { val element = result.get(0); @@ -82,23 +84,23 @@ public class LogicProblemBuilder{ } // Type builders - def public Element(CharSequence elementName) { return createDefinedElement => [x|x.name = elementName.canonize] } - def public Element() { return createDefinedElement } - def public TypeDeclaration(CharSequence name, boolean isAbstract) { TypeDeclaration => [x | x.name = name.canonize x.isAbstract = isAbstract] } - def public TypeDeclaration() { createTypeDeclaration } - def public TypeDefinition(CharSequence name, boolean isAbstract, DefinedElement... elements) { TypeDefinition(name, isAbstract, elements as Iterable) } - def public TypeDefinition(CharSequence name, boolean isAbstract, Iterable elements) { createTypeDefinition => [x | x.name = name.canonize x.isAbstract = isAbstract x.elements += elements ] } - - def public Supertype(Type subtype, Type supertype) { + def Element(CharSequence elementName) { return createDefinedElement => [x|x.name = elementName.canonize] } + def Element() { return createDefinedElement } + def TypeDeclaration(CharSequence name, boolean isAbstract) { TypeDeclaration => [x | x.name = name.canonize x.isAbstract = isAbstract] } + def TypeDeclaration() { createTypeDeclaration } + def TypeDefinition(CharSequence name, boolean isAbstract, DefinedElement... elements) { TypeDefinition(name, isAbstract, elements as Iterable) } + def TypeDefinition(CharSequence name, boolean isAbstract, Iterable elements) { createTypeDefinition => [x | x.name = name.canonize x.isAbstract = isAbstract x.elements += elements ] } + + def Supertype(Type subtype, Type supertype) { subtype.supertypes+=supertype } - def public SetSupertype(Type subtype, Type supertype, boolean value) { + def SetSupertype(Type subtype, Type supertype, boolean value) { if(value) subtype.supertypes+=supertype else subtype.subtypes-=supertype } // Type add - def public add(LogicProblem problem, Type type) { + def add(LogicProblem problem, Type type) { problem.nameIfAnonymType(type) problem.types+=type if(type instanceof TypeDefinition) { @@ -118,10 +120,10 @@ public class LogicProblemBuilder{ element.name = typeDefinition.elements.map[it.name].generateUniqueName[i | '''type «i.toString»'''] } - def public LogicBool() { createBoolTypeReference } - def public LogicInt() { createIntTypeReference } - def public LogicReal() { createRealTypeReference } - def public LogicString() { createStringTypeReference } + def LogicBool() { createBoolTypeReference } + def LogicInt() { createIntTypeReference } + def LogicReal() { createRealTypeReference } + def LogicString() { createStringTypeReference } def toTypeReference(TypeDescriptor descriptor) { if(descriptor instanceof TypeReference) { return EcoreUtil.copy(descriptor); } else if(descriptor instanceof Type) { return createComplexTypeReference => [referred = descriptor]} @@ -129,31 +131,31 @@ public class LogicProblemBuilder{ } // Variables - def public createVar(CharSequence name, TypeDescriptor range) { + def createVar(CharSequence name, TypeDescriptor range) { return createVariable => [it.name = name.canonize it.range = range.toTypeReference] } // Functions - def public FunctionDescription ->(TypeDescriptor parameter, TypeDescriptor range) { return #[parameter] -> range } - def public FunctionDescription ->(Iterable parameters, TypeDescriptor range) { return new FunctionDescription(parameters.map[toTypeReference], range.toTypeReference); } - def public FunctionDeclaration(CharSequence name, FunctionDescription functionDescription) { FunctionDeclaration(name,functionDescription.range, functionDescription.parameters) } - def public FunctionDeclaration(FunctionDescription functionDescription) { FunctionDeclaration(functionDescription.range, functionDescription.parameters) } - def public FunctionDeclaration(CharSequence name, TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(name, range, parameters as Iterable) } - def public FunctionDeclaration(TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(range, parameters as Iterable) } - def public FunctionDeclaration(CharSequence name, TypeDescriptor range, Iterable parameters) { return FunctionDeclaration(range,parameters) => [x|x.name = name.canonize] } - def public FunctionDeclaration(TypeDescriptor range, Iterable parameters) { + def FunctionDescription ->(TypeDescriptor parameter, TypeDescriptor range) { return #[parameter] -> range } + def FunctionDescription ->(Iterable parameters, TypeDescriptor range) { return new FunctionDescription(parameters.map[toTypeReference], range.toTypeReference); } + def FunctionDeclaration(CharSequence name, FunctionDescription functionDescription) { FunctionDeclaration(name,functionDescription.range, functionDescription.parameters) } + def FunctionDeclaration(FunctionDescription functionDescription) { FunctionDeclaration(functionDescription.range, functionDescription.parameters) } + def FunctionDeclaration(CharSequence name, TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(name, range, parameters as Iterable) } + def FunctionDeclaration(TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(range, parameters as Iterable) } + def FunctionDeclaration(CharSequence name, TypeDescriptor range, Iterable parameters) { return FunctionDeclaration(range,parameters) => [x|x.name = name.canonize] } + def FunctionDeclaration(TypeDescriptor range, Iterable parameters) { val function = createFunctionDeclaration for(parameter : parameters) function.parameters+=parameter.toTypeReference function.range = range.toTypeReference return function } - def public FunctionDefinition(CharSequence name, TypeDescriptor range, Function1 expression) { + def FunctionDefinition(CharSequence name, TypeDescriptor range, Function1 expression) { val context = new VariableContext(this,logicFactiory) val definition = expression.apply(context) return FunctionDefinition(name,range,context.variables,definition); } - def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable variables, TermDescription definition) { + def FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable variables, TermDescription definition) { return createFunctionDefinition => [ it.name = name.canonize it.parameters += variables.map[it.range.toTypeReference] @@ -162,23 +164,23 @@ public class LogicProblemBuilder{ it.value = definition.toTerm ] } - def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable parameters, Map,Term> parametersToValue) { + def FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable parameters, Map,Term> parametersToValue) { return FunctionDefinition(name,range,parameters,parametersToValue,null) } - def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable parameters, Map,Term> parametersToValue, Term defaultValue) { + def FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable parameters, Map,Term> parametersToValue, Term defaultValue) { val parameterList = parameters.toList; val variableList = (1..parameterList.size).map[index | '''param «index»'''.createVar(parameterList.get(index-1))].toList return FunctionDefinition(name,range,variableList,advancedConstructs.FunctionDefinitionBody(variableList,parametersToValue,defaultValue)) } // Add function to a problem - def public add(LogicProblem input, Function function) { + def add(LogicProblem input, Function function) { input.nameIfAnonymFunction(function) input.checkFunction(function) input.functions += function return function } - def public add(LogicProblem input, FunctionDescription functionDescription) { input.add(FunctionDeclaration(functionDescription)) } + def add(LogicProblem input, FunctionDescription functionDescription) { input.add(FunctionDeclaration(functionDescription)) } def protected nameIfAnonymFunction(LogicProblem problem, Function functionDeclaration) { if(functionDeclaration.name.nullOrEmpty) { functionDeclaration.name = problem.functions.map[it.name].generateUniqueName[i | "function"+i] @@ -199,15 +201,15 @@ public class LogicProblemBuilder{ } // Constants - def public ConstantDeclaration(CharSequence name, TypeDescriptor type) { ConstantDeclaration(type) => [it.name = name.canonize] } - def public ConstantDeclaration(TypeDescriptor type) { createConstantDeclaration => [it.type = type.toTypeReference] } + def ConstantDeclaration(CharSequence name, TypeDescriptor type) { ConstantDeclaration(type) => [it.name = name.canonize] } + def ConstantDeclaration(TypeDescriptor type) { createConstantDeclaration => [it.type = type.toTypeReference] } - def public ConstantDefinition(CharSequence name, TypeDescriptor type, TermDescription value) { + def ConstantDefinition(CharSequence name, TypeDescriptor type, TermDescription value) { createConstantDefinition => [it.name = name.canonize it.type = type.toTypeReference it.value = value.toTerm] } // Add constant to a problem - def public add(LogicProblem problem, Constant constant) { + def add(LogicProblem problem, Constant constant) { problem.nameIfAnonymConstant(constant); problem.checkConstant(constant) problem.constants += constant @@ -226,10 +228,10 @@ public class LogicProblemBuilder{ } // Relations - def public RelationDeclaration(CharSequence name, TypeDescriptor... parameters) { return RelationDeclaration(name, parameters as Iterable) } - def public RelationDeclaration(CharSequence name, Iterable parameters) { return RelationDeclaration(parameters) => [x|x.name = name.canonize] } - def public RelationDeclaration(TypeDescriptor... parameters) { RelationDeclaration( parameters as Iterable) } - def public RelationDeclaration(Iterable parameters) { + def RelationDeclaration(CharSequence name, TypeDescriptor... parameters) { return RelationDeclaration(name, parameters as Iterable) } + def RelationDeclaration(CharSequence name, Iterable parameters) { return RelationDeclaration(parameters) => [x|x.name = name.canonize] } + def RelationDeclaration(TypeDescriptor... parameters) { RelationDeclaration( parameters as Iterable) } + def RelationDeclaration(Iterable parameters) { val relation = createRelationDeclaration for(parameter : parameters) { relation.parameters+=parameter.toTypeReference @@ -237,12 +239,12 @@ public class LogicProblemBuilder{ return relation } - def public RelationDefinition(CharSequence name, Function1 expression) { + def RelationDefinition(CharSequence name, Function1 expression) { val context = new VariableContext(this,logicFactiory); val definition = expression.apply(context); return RelationDefinition(name,context.variables,definition) } - def public RelationDefinition(CharSequence name, Iterable variables, TermDescription definition) { + def RelationDefinition(CharSequence name, Iterable variables, TermDescription definition) { return createRelationDefinition => [ it.name = name.canonize it.parameters += variables.map[it.range.toTypeReference] @@ -250,7 +252,7 @@ public class LogicProblemBuilder{ it.value = definition?.toTerm ] } - def public RelationDefinition(CharSequence name, Iterable parameters, Iterable> possibleValues) { + def RelationDefinition(CharSequence name, Iterable parameters, Iterable> possibleValues) { val res = createRelationDefinition => [it.name = name.canonize] val variableMap = new ArrayList(parameters.size) var index = 0 @@ -267,7 +269,7 @@ public class LogicProblemBuilder{ } // Add Relation to a problem - def public add(LogicProblem input, Relation relation) { + def add(LogicProblem input, Relation relation) { input.nameIfAnonymRelation(relation) input.checkRelation(relation) input.relations+=relation @@ -293,17 +295,17 @@ public class LogicProblemBuilder{ } // Assertion - def public Assertion(TermDescription term) { + def Assertion(TermDescription term) { val result = term.toTerm result.nameAnonymVariables(Collections.EMPTY_LIST) createAssertion => [it.value = result] } - def public Assertion(CharSequence name, TermDescription term) { + def Assertion(CharSequence name, TermDescription term) { val result = term.toTerm result.nameAnonymVariables(Collections.EMPTY_LIST) createAssertion => [it.value = result it.name=name.canonize] } - def public add(LogicProblem problem, Assertion assertion) { + def add(LogicProblem problem, Assertion assertion) { if(assertion.name.nullOrEmpty) { val name = problem.assertions.map[name].generateUniqueName["assertion"+it] assertion.name=name @@ -313,7 +315,7 @@ public class LogicProblemBuilder{ return assertion } - def public add(LogicProblem problem, TermDescription term) { + def add(LogicProblem problem, TermDescription term) { problem.add(Assertion(term)) } @@ -329,7 +331,7 @@ public class LogicProblemBuilder{ } } - def public checkDefinition(EObject definition) { + def checkDefinition(EObject definition) { /*for(value : definition.eAllContents.filter(SymbolicValue).toIterable) { var referred = value.symbolicReference if(referred instanceof Variable) { @@ -341,7 +343,7 @@ public class LogicProblemBuilder{ } // Containment - def public ContainmentHierarchy( + def ContainmentHierarchy( Iterable typesInHierarchy, Iterable containmentFunctions, Iterable containmentRelations, @@ -355,7 +357,7 @@ public class LogicProblemBuilder{ ] return result } - def public add(LogicProblem problem, ContainmentHierarchy hierarchy) { + def add(LogicProblem problem, ContainmentHierarchy hierarchy) { problem.containmentHierarchies+=hierarchy return hierarchy } @@ -413,7 +415,7 @@ public class LogicProblemBuilder{ return result; } - def public Term toTerm(TermDescription term) { + def Term toTerm(TermDescription term) { if(term instanceof Term) return term else if (term instanceof Variable) return createSymbolicValue => [symbolicReference = term] else if (term instanceof Constant) return term.call() @@ -421,74 +423,74 @@ public class LogicProblemBuilder{ else throw new UnsupportedOperationException("Can not create reference for symbolic declaration " + term.class.name) } - def public !(TermDescription term) { Not(term) } - def public Not(TermDescription term) { createNot => [operand = term.toTerm] } + def !(TermDescription term) { Not(term) } + def Not(TermDescription term) { createNot => [operand = term.toTerm] } - def public &&(TermDescription a, TermDescription b) { And(a,b) } - def public And(TermDescription... terms) { return And(terms as Iterable) } - def public And(Iterable terms) { createAnd => [operands += terms.map[toTerm]] } + def &&(TermDescription a, TermDescription b) { And(a,b) } + def And(TermDescription... terms) { return And(terms as Iterable) } + def And(Iterable terms) { createAnd => [operands += terms.map[toTerm]] } - def public ||(TermDescription a, TermDescription b) { Or(a,b) } - def public Or(TermDescription... terms) { Or(terms as Iterable) } - def public Or(Iterable terms) { createOr => [operands += terms.map[toTerm]] } + def ||(TermDescription a, TermDescription b) { Or(a,b) } + def Or(TermDescription... terms) { Or(terms as Iterable) } + def Or(Iterable terms) { createOr => [operands += terms.map[toTerm]] } - def public =>(TermDescription a, TermDescription b) { Impl(a,b) } - def public Impl(TermDescription a, TermDescription b) { createImpl => [leftOperand = a.toTerm rightOperand = b.toTerm] } + def =>(TermDescription a, TermDescription b) { Impl(a,b) } + def Impl(TermDescription a, TermDescription b) { createImpl => [leftOperand = a.toTerm rightOperand = b.toTerm] } - def public <=>(TermDescription a, TermDescription b) { Iff(a,b)} - def public Iff(TermDescription a, TermDescription b) { createIff =>[leftOperand=a.toTerm rightOperand=b.toTerm] } + def <=>(TermDescription a, TermDescription b) { Iff(a,b)} + def Iff(TermDescription a, TermDescription b) { createIff =>[leftOperand=a.toTerm rightOperand=b.toTerm] } - def public ITE(TermDescription condition, TermDescription ifTrue, TermDescription ifFalse) { + def ITE(TermDescription condition, TermDescription ifTrue, TermDescription ifFalse) { createIfThenElse => [it.condition = condition.toTerm it.ifTrue = ifTrue.toTerm it.ifFalse = ifFalse.toTerm] } - def public >(TermDescription left, TermDescription right) { MoreThan(left,right)} - def public MoreThan(TermDescription left, TermDescription right) { createMoreThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } + def >(TermDescription left, TermDescription right) { MoreThan(left,right)} + def MoreThan(TermDescription left, TermDescription right) { createMoreThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } - def public <(TermDescription left, TermDescription right) { LessThan(left,right)} - def public LessThan(TermDescription left, TermDescription right) { createLessThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } + def <(TermDescription left, TermDescription right) { LessThan(left,right)} + def LessThan(TermDescription left, TermDescription right) { createLessThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } - def public <=(TermDescription left, TermDescription right) { LessOrEqual(left,right) } - def public LessOrEqual(TermDescription left, TermDescription right) { createLessOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } + def <=(TermDescription left, TermDescription right) { LessOrEqual(left,right) } + def LessOrEqual(TermDescription left, TermDescription right) { createLessOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } - def public >=(TermDescription left, TermDescription right) { MoreOrEqual(left,right) } - def public MoreOrEqual(TermDescription left, TermDescription right) { createMoreOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } + def >=(TermDescription left, TermDescription right) { MoreOrEqual(left,right) } + def MoreOrEqual(TermDescription left, TermDescription right) { createMoreOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } - def public ==(TermDescription left, TermDescription right) {Equals(left,right)} - def public Equals(TermDescription left, TermDescription right) { createEquals => [leftOperand=left.toTerm rightOperand=right.toTerm] } + def ==(TermDescription left, TermDescription right) {Equals(left,right)} + def Equals(TermDescription left, TermDescription right) { createEquals => [leftOperand=left.toTerm rightOperand=right.toTerm] } - def public !=(TermDescription left, TermDescription right) { Distinct(left,right) } - def public Distinct(TermDescription... terms) { return Distinct(terms as Iterable) } - def public Distinct(Iterable terms) { createDistinct => [operands += terms.map[toTerm]] } + def !=(TermDescription left, TermDescription right) { Distinct(left,right) } + def Distinct(TermDescription... terms) { return Distinct(terms as Iterable) } + def Distinct(Iterable terms) { createDistinct => [operands += terms.map[toTerm]] } - def public +(TermDescription left, TermDescription right) { Plus(left,right) } - def public Plus(TermDescription left, TermDescription right) { createPlus => [leftOperand=left.toTerm rightOperand=right.toTerm] } + def +(TermDescription left, TermDescription right) { Plus(left,right) } + def Plus(TermDescription left, TermDescription right) { createPlus => [leftOperand=left.toTerm rightOperand=right.toTerm] } - def public -(TermDescription left, TermDescription right) { Minus(left,right) } - def public Minus(TermDescription left, TermDescription right) { createMinus => [leftOperand=left.toTerm rightOperand=right.toTerm] } + def -(TermDescription left, TermDescription right) { Minus(left,right) } + def Minus(TermDescription left, TermDescription right) { createMinus => [leftOperand=left.toTerm rightOperand=right.toTerm] } - def public *(TermDescription left, TermDescription right) { Multiply(left,right) } - def public Multiply(TermDescription left, TermDescription right) { createMultiply => [leftOperand=left.toTerm rightOperand=right.toTerm] } + def *(TermDescription left, TermDescription right) { Multiply(left,right) } + def Multiply(TermDescription left, TermDescription right) { createMultiply => [leftOperand=left.toTerm rightOperand=right.toTerm] } - def public /(TermDescription left, TermDescription right) { Divide(left,right) } - def public Divide(TermDescription left, TermDescription right) { createDivison => [leftOperand = left.toTerm rightOperand = right.toTerm]} + def /(TermDescription left, TermDescription right) { Divide(left,right) } + def Divide(TermDescription left, TermDescription right) { createDivison => [leftOperand = left.toTerm rightOperand = right.toTerm]} - def public %(TermDescription left, TermDescription right) { Modulo(left,right) } - def public Modulo(TermDescription left, TermDescription right) { createMod => [leftOperand = left.toTerm rightOperand = right.toTerm]} + def %(TermDescription left, TermDescription right) { Modulo(left,right) } + def Modulo(TermDescription left, TermDescription right) { createMod => [leftOperand = left.toTerm rightOperand = right.toTerm]} - def public asTerm(boolean value) { createBoolLiteral => [x|x.value = value] } - def public asTerm(int value) { createIntLiteral => [x|x.value = value] } - def public asTerm(double value) { BigDecimal.valueOf(value).asTerm } - def public asTerm(float value) { BigDecimal.valueOf(value).asTerm } - def public asTerm(BigDecimal value) { createRealLiteral => [x|x.value = value] } - def public asTerm(String value) { createStringLiteral => [x|x.value = value]} - def public InstanceOf(TermDescription term, TypeDescriptor type) { + def asTerm(boolean value) { createBoolLiteral => [x|x.value = value] } + def asTerm(int value) { createIntLiteral => [x|x.value = value] } + def asTerm(double value) { BigDecimal.valueOf(value).asTerm } + def asTerm(float value) { BigDecimal.valueOf(value).asTerm } + def asTerm(BigDecimal value) { createRealLiteral => [x|x.value = value] } + def asTerm(String value) { createStringLiteral => [x|x.value = value]} + def InstanceOf(TermDescription term, TypeDescriptor type) { createInstanceOf => [ it.value = term.toTerm it.range = type.toTypeReference ] } - def public transitiveClosure(Relation relation, TermDescription source, TermDescription target) { + def transitiveClosure(Relation relation, TermDescription source, TermDescription target) { createTransitiveClosure => [ it.relation = relation it.leftOperand = leftOperand @@ -498,38 +500,79 @@ public class LogicProblemBuilder{ // QuantifiedExpressions - def public Forall(Function1 expression) { + def Forall(Function1 expression) { val context = new VariableContext(this,logicFactiory) val term = expression.apply(context) return createForall => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] } - def public Forall(TermDescription expression, Variable... variables) { + def Forall(TermDescription expression, Variable... variables) { Forall(variables,expression) } - def public Forall(Iterable variables,TermDescription expression) { + def Forall(Iterable variables,TermDescription expression) { val forallExpression = createForall for(variable : variables) forallExpression.quantifiedVariables += variable forallExpression.expression = expression.toTerm return forallExpression } - def public Exists(Function1 expression) { + def Exists(Function1 expression) { val context = new VariableContext(this,logicFactiory) val term = expression.apply(context) return createExists => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] } - def public Exists(TermDescription expression, Variable... variables) { + def Exists(TermDescription expression, Variable... variables) { Exists(variables,expression) } - def public Exists(Iterable variables, TermDescription expression) { + def Exists(Iterable variables, TermDescription expression) { val existsExpression = createExists for(variable : variables) existsExpression.quantifiedVariables += variable existsExpression.expression = expression.toTerm return existsExpression } + // AggregatedExpression + + private def configureAggregateExpression(T expression, Relation referred, List terms) { + if(terms.size != referred.parameters.size) { + throw new LogicProblemBuilderException( + '''The function called has «referred.parameters.size» parameters but it is called with «terms.size»!''') + } else { + expression.relation = referred + for(var i=0; i [it.variable = target] + expression.parameterSubstitution += substitution + } + return expression + } + } + private def configureProjectedAggregateExpression(T expression, Relation referred, List terms, int projection) { + if(projection < 0 || projection >= referred.parameters.size) { + throw new LogicProblemBuilderException( + '''The function called has «referred.parameters.size» parameters but it is called with «terms.size»!''') + } else { + val res = expression.configureAggregateExpression(referred, terms) + if(res.parameterSubstitution.get(projection) !== null) { + throw new LogicProblemBuilderException( + '''Projection over set variable!''') + } + val projectionType = referred.parameters.get(projection) + if(!(projectionType instanceof IntTypeReference || projectionType instanceof RealTypeReference)) { + throw new LogicProblemBuilderException('''Projection over nunnumeric parameter!''' + ) + } + res.projectionIndex = projection + return res + } + + } + def Count(Relation referred, List terms) { createCount.configureAggregateExpression(referred,terms) } + def Sum(Relation referred, List terms, int projection) { createSum.configureProjectedAggregateExpression(referred,terms,projection) } + def Min(Relation referred, List terms, int projection) { createMin.configureProjectedAggregateExpression(referred,terms,projection) } + def Max(Relation referred, List terms, int projection) { createMax.configureProjectedAggregateExpression(referred,terms,projection) } + // Function calls - def public call(Function function, TermDescription... substitutions) { + def call(Function function, TermDescription... substitutions) { call(function, substitutions as Iterable) } - def public call(Function function, Iterable substitutions) { + def call(Function function, Iterable substitutions) { val functionReference = createSymbolicValue functionReference.symbolicReference=function val List l= new LinkedList() @@ -546,8 +589,8 @@ public class LogicProblemBuilder{ } // Relation calls - def public call(Relation relation, TermDescription... substitution) { relation.call(substitution as Iterable)} - def public call(Relation relation, Iterable substitution) { + def call(Relation relation, TermDescription... substitution) { relation.call(substitution as Iterable)} + def call(Relation relation, Iterable substitution) { val relationReference = createSymbolicValue relationReference.symbolicReference = relation //println('''«relation.name»(«substitution.size»->«relation.parameters»)''') @@ -567,11 +610,9 @@ public class LogicProblemBuilder{ } // constant evaluation - def public call(Constant constant) { + def call(Constant constant) { val constantReference = createSymbolicValue constantReference.symbolicReference = constant return constantReference - } - - + } } -- cgit v1.2.3-54-g00ecf