+ * @param function The target function to be interpreted.
+ * @param parameterSubstitution The array of the substituted parameters encoded as defined in the table.
+ * @return The result of the function call encoded as defined in the table.
+ */
+ def Object getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution)
+ /**
+ * Returns the interpretation of a relation. The parameters are encoded to primitive java objects defined by the following table:
+ *
+ *
Term type
Java object type
+ *
Element of a type
DefinedElement
+ *
Boolean literal
Boolean
+ *
Integer literal
Integer
+ *
Real literal
BigDecimal
+ *
+ * @param relation The target relation to be interpreted.
+ * @param parameterSubstitution The array of the substituted parameters encoded as defined in the table.
+ * @return If the parameter tuple is in the relation.
+ */
+ def boolean getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution)
+ /**
+ * Returns the interpretation of a constant. The value is encoded to primitive java objects defined by the following table:
+ *
+ *
Term type
Java object type
+ *
Element of a type
DefinedElement
+ *
Boolean literal
Boolean
+ *
Integer literal
Integer
+ *
Real literal
BigDecimal
+ *
+ * @param constant The target constant to be interpreted.
+ * @return The value of the constant encoded as specified in the table.
+ */
+ def Object getInterpretation(ConstantDeclaration constant)
+ def int getMinimalInteger()
+ def int getMaximalInteger()
+}
+
+class Uninterpreted implements LogicModelInterpretation {
+ /*private val static unknownBecauseUninterpreted = LogiclanguageFactory.eINSTANCE.createUnknownBecauseUninterpreted
+ public def static getUnknownBecauseUninterpreted() {return Uninterpreted.unknownBecauseUninterpreted}*/
+
+ override getElements(Type type) {
+ throw new UnsupportedOperationException("The interpteration is unknown.")
+ }
+
+ def getKnownElements(Type type) {
+ val allSubtypes = type.transitiveClosureStar[it.subtypes]
+ return allSubtypes.filter(TypeDefinition).map[elements].flatten.toList
+ }
+
+ def allElementsAreInterpreted(Type type) {
+ val allSubtypes = type.transitiveClosureStar[it.subtypes]
+ return allSubtypes.exists[it instanceof TypeDeclaration]
+ }
+
+ override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
+ throw new UnsupportedOperationException("The interpteration is unknown.")
+ }
+
+ override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
+ throw new UnsupportedOperationException("The interpteration is unknown.")
+ }
+
+ override getInterpretation(ConstantDeclaration constant) {
+ throw new UnsupportedOperationException("The interpteration is unknown.")
+ }
+
+ override getMinimalInteger() {
+ throw new UnsupportedOperationException("The interpteration is unknown.")
+ }
+
+ override getMaximalInteger() {
+ throw new UnsupportedOperationException("The interpteration is unknown.")
+ }
+}
\ No newline at end of file
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
new file mode 100644
index 00000000..ba1b9fd6
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend
@@ -0,0 +1,563 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.builder
+
+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
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
+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.QuantifiedExpression
+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.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.TermDescription
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemFactory
+import hu.bme.mit.inf.dslreasoner.util.LogicProblemBuilder_AdvancedConstructs
+import java.math.BigDecimal
+import java.util.ArrayList
+import java.util.Collections
+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.Data
+import org.eclipse.xtext.xbase.lib.Functions.Function1
+
+@Data class FunctionDescription {
+ Iterable parameters
+ TypeReference range
+}
+
+class LogicProblemBuilderException extends Exception {
+ new(String reason) {
+ super(reason)
+ }
+}
+
+public 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 }
+
+ // Names
+ def protected String canonize(CharSequence name) {
+ if(name == null) return ""
+ val result = name.toString.split("\\s+");
+ if(result.size == 1) {
+ val element = result.get(0);
+ if(element == "bool" ||
+ element == "int" ||
+ element == "real") throw new LogicProblemBuilderException('''Reserved keyword "«element»"!''')
+ else return result.join(' ')
+ }
+ else return result.join(' ')
+ }
+ def protected String generateUniqueName(Iterable previous, Function1 namer) {
+ var int i = 0
+ var generateNew = false;
+ var String finalName;
+ do {
+ i = i+1;
+ val nameCandidate = namer.apply(i)
+ finalName = nameCandidate
+ generateNew = previous.exists[equals(nameCandidate)]
+ }
+ while(generateNew)
+ return finalName
+ }
+
+ // 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) {
+ subtype.supertypes+=supertype
+ }
+ def public 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) {
+ problem.nameIfAnonymType(type)
+ problem.types+=type
+ if(type instanceof TypeDefinition) {
+ problem.elements+=type.elements
+ }
+ return type
+ }
+ def protected dispatch nameIfAnonymType(LogicProblem problem, Type typeDeclaration) {
+ if(typeDeclaration.name.nullOrEmpty)
+ typeDeclaration.name = problem.types.map[it.name].generateUniqueName[i | '''type «i.toString»''']
+ }
+ def protected dispatch nameIfAnonymType(LogicProblem problem, TypeDefinition typeDefinition) {
+ if(typeDefinition.name.nullOrEmpty)
+ typeDefinition.name = problem.types.map[it.name].generateUniqueName[i | '''type «i.toString»''']
+ for(element : typeDefinition.elements)
+ if(element.name.nullOrEmpty)
+ 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 toTypeReference(TypeDescriptor descriptor) {
+ if(descriptor instanceof TypeReference) { return EcoreUtil.copy(descriptor); }
+ else if(descriptor instanceof Type) { return createComplexTypeReference => [referred = descriptor]}
+ else throw new UnsupportedOperationException("Unsupported type descriptor: " + descriptor.class)
+ }
+
+ // Variables
+ def public 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 extends TypeDescriptor> 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 extends TypeReference>) }
+ def public FunctionDeclaration(TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(range, parameters as Iterable extends TypeReference>) }
+ def public FunctionDeclaration(CharSequence name, TypeDescriptor range, Iterable extends TypeDescriptor> parameters) { return FunctionDeclaration(range,parameters) => [x|x.name = name.canonize] }
+ def public FunctionDeclaration(TypeDescriptor range, Iterable extends TypeDescriptor> 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) {
+ 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) {
+ return createFunctionDefinition => [
+ it.name = name.canonize
+ it.parameters += variables.map[it.range.toTypeReference]
+ it.variable += variables
+ it.range = range.toTypeReference
+ it.value = definition.toTerm
+ ]
+ }
+ def public 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) {
+ 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) {
+ input.nameIfAnonymFunction(function)
+ input.checkFunction(function)
+ input.functions += function
+ return function
+ }
+ def public 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]
+ }
+ }
+ def protected checkFunction(LogicProblem problem, Function function) {
+ if(problem.functions.exists(x|x.name == function.name))
+ throw new LogicProblemBuilderException('''Function with the following name is already defined: "«function.name»"!''')
+ for(ref : function.parameters.filter(typeof(ComplexTypeReference)).map[referred]) {
+ if(!problem.types.contains(ref))
+ throw new LogicProblemBuilderException('''Type "«ref.name»" is not availabe in the logic problem!''')
+ }
+ val range = function.range
+ if(range instanceof ComplexTypeReference) {
+ if(!problem.types.contains(range.referred))
+ throw new LogicProblemBuilderException('''Type "«range.referred.name»" is not availabe in the logic problem!''')
+ }
+ }
+
+ // 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 public 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) {
+ problem.nameIfAnonymConstant(constant);
+ problem.checkConstant(constant)
+ problem.constants += constant
+ return constant
+ }
+ def protected nameIfAnonymConstant(LogicProblem problem, Constant constant) {
+ if(constant.name.nullOrEmpty) {
+ constant.name = problem.constants.map[it.name].generateUniqueName[i | "constant"+i]
+ }
+ }
+ def protected checkConstant(LogicProblem problem, Constant constant) {
+ if(problem.constants.exists(x|x.name == constant.name))
+ throw new LogicProblemBuilderException('''Constant with the following name is already defined: "«constant.name»"!''')
+ if((constant.type instanceof ComplexTypeReference) && ! (problem.types.contains((constant.type as ComplexTypeReference).referred)))
+ throw new LogicProblemBuilderException('''Type "«(constant.type as ComplexTypeReference).referred.name»" is not availabe in the logic problem!''')
+ }
+
+ // Relations
+ def public RelationDeclaration(CharSequence name, TypeDescriptor... parameters) { return RelationDeclaration(name, parameters as Iterable extends TypeReference>) }
+ def public RelationDeclaration(CharSequence name, Iterable extends TypeDescriptor> parameters) { return RelationDeclaration(parameters) => [x|x.name = name.canonize] }
+ def public RelationDeclaration(TypeDescriptor... parameters) { RelationDeclaration( parameters as Iterable extends TypeReference>) }
+ def public RelationDeclaration(Iterable extends TypeDescriptor> parameters) {
+ val relation = createRelationDeclaration
+ for(parameter : parameters) {
+ relation.parameters+=parameter.toTypeReference
+ }
+ return relation
+ }
+
+ def public 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) {
+ return createRelationDefinition => [
+ it.name = name.canonize
+ it.parameters += variables.map[it.range.toTypeReference]
+ it.variables += variables
+ it.value = definition?.toTerm
+ ]
+ }
+ def public RelationDefinition(CharSequence name, Iterable extends TypeDescriptor> parameters, Iterable extends List extends TermDescription>> possibleValues) {
+ val res = createRelationDefinition => [it.name = name.canonize]
+ val variableMap = new ArrayList(parameters.size)
+ var index = 0
+ for(parameter : parameters) {
+ val actualIndex = index
+ val newVar = createVariable=>[it.name ='''var «actualIndex»'''.canonize it.range = parameter.toTypeReference]
+ variableMap.add(index,newVar)
+ res.variables+=newVar
+ res.parameters+=newVar.range
+ index+=1
+ }
+ res.value = possibleValues.map[possibleValue |(0.. [it.value = result]
+ }
+ def public 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) {
+ if(assertion.name.nullOrEmpty) {
+ val name = problem.assertions.map[name].generateUniqueName["assertion"+it]
+ assertion.name=name
+ }
+ checkAssertion(assertion)
+ problem.assertions+=assertion
+ return assertion
+ }
+
+ def public add(LogicProblem problem, TermDescription term) {
+ problem.add(Assertion(term))
+ }
+
+
+ def checkAssertion(Assertion assertion) {
+ for(value : assertion.eAllContents.filter(SymbolicValue).toIterable) {
+ var referred = value.symbolicReference
+ if(referred instanceof Variable) {
+ if(!value.hasDeclaredVariable(referred)){
+ throw new LogicProblemBuilderException('''Variable "«referred.name»" is not availabe in the logic problem!''')
+ }
+ }
+ }
+ }
+
+ def public checkDefinition(EObject definition) {
+ /*for(value : definition.eAllContents.filter(SymbolicValue).toIterable) {
+ var referred = value.symbolicReference
+ if(referred instanceof Variable) {
+ if(!value.hasDeclaredVariable(referred)){
+ throw new LogicProblemBuilderException('''Variable "«referred.name»" is not availabe in the logic problem!''')
+ }
+ }
+ }*/
+ }
+
+ // Containment
+ def public ContainmentHierarchy(
+ Iterable extends Type> typesInHierarchy,
+ Iterable extends Function> containmentFunctions,
+ Iterable extends Relation> containmentRelations,
+ Constant rootConstant
+ ) {
+ val result = createContainmentHierarchy => [
+ it.typesOrderedInHierarchy += typesInHierarchy
+ it.containmentFunctions += containmentFunctions
+ it.containmentRelations += containmentRelations
+ it.rootConstant = rootConstant
+ ]
+ return result
+ }
+ def public add(LogicProblem problem, ContainmentHierarchy hierarchy) {
+ problem.containmentHierarchies+=hierarchy
+ return hierarchy
+ }
+
+ // Terms
+
+ private dispatch def boolean hasDeclaredVariable(QuantifiedExpression term, Variable variable) {
+ return term.quantifiedVariables.contains(variable) || ((term.eContainer instanceof Term) && (term.eContainer as Term).hasDeclaredVariable(variable))
+ }
+ private dispatch def boolean hasDeclaredVariable(Term term, Variable variable) {
+ return (term.eContainer instanceof Term) && (term.eContainer as Term).hasDeclaredVariable(variable)
+ }
+ private dispatch def boolean hasDeclaredVariable(RelationDefinition relation, Variable variable) {
+ relation.variables.contains(variable)
+ }
+ private dispatch def boolean hasDeclaredVariable(Void term, Variable variable) {
+ return false
+ }
+
+ def protected void nameAnonymVariables(EObject termSegment, List previousNames) {
+ if(termSegment instanceof QuantifiedExpression) {
+ val newNames = new LinkedList(previousNames)
+ for(variable : termSegment.quantifiedVariables) {
+ var String newName
+ if(variable.name.nullOrEmpty) {
+ newName = newNames.generateUniqueName[i |
+ var x = variable.range.variableAnonymName
+ x+="var"+i.toString
+ //println(x)
+ return x
+ ]
+ variable.name = newName
+ }
+ else newName = variable.name
+ newNames+= newName
+ }
+ termSegment.expression.nameAnonymVariables(newNames)
+ }
+ else {
+ for(subTerm : termSegment.eContents) {
+ subTerm.nameAnonymVariables(previousNames)
+ }
+ }
+ }
+ def protected dispatch String variableAnonymName(BoolTypeReference ref) { "bool" }
+ def protected dispatch String variableAnonymName(IntTypeReference ref) { "int" }
+ def protected dispatch String variableAnonymName(RealTypeReference ref) { "real" }
+ def protected dispatch String variableAnonymName(ComplexTypeReference ref) { ref.referred.name.toLowerCase }
+
+ def protected allSubterms(Term term) {
+ val content = term.eAllContents
+ val result = new ArrayList(content.size+1)
+ result+=term
+ result+=content.toIterable
+ return result;
+ }
+
+ def public 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()
+ else if (term instanceof DefinedElement) return createSymbolicValue => [symbolicReference = term]
+ 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 public &&(TermDescription a, TermDescription b) { And(a,b) }
+ def public And(TermDescription... terms) { return And(terms as Iterable extends TermDescription>) }
+ def public And(Iterable extends TermDescription> terms) { createAnd => [operands += terms.map[toTerm]] }
+
+ def public ||(TermDescription a, TermDescription b) { Or(a,b) }
+ def public Or(TermDescription... terms) { Or(terms as Iterable extends TermDescription>) }
+ def public Or(Iterable extends TermDescription> 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 public <=>(TermDescription a, TermDescription b) { Iff(a,b)}
+ def public Iff(TermDescription a, TermDescription b) { createIff =>[leftOperand=a.toTerm rightOperand=b.toTerm] }
+
+ def public 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 public <(TermDescription left, TermDescription right) { LessThan(left,right)}
+ def public 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 public >=(TermDescription left, TermDescription right) { MoreOrEqual(left,right) }
+ def public 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 public !=(TermDescription left, TermDescription right) { Distinct(left,right) }
+ def public Distinct(TermDescription... terms) { return Distinct(terms as Iterable extends TermDescription>) }
+ def public Distinct(Iterable extends TermDescription> 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 public -(TermDescription left, TermDescription right) { Minus(left,right) }
+ def public 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 public /(TermDescription left, TermDescription right) { Divide(left,right) }
+ def public 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 public asTerm(boolean value) { createBoolLiteral => [x|x.value = value] }
+ def public asTerm(int value) { createIntLiteral => [x|x.value = value] }
+ def public asTerm(double value) { createRealLiteral => [x|x.value = BigDecimal.valueOf(value)] }
+
+ def public InstanceOf(TermDescription term, TypeDescriptor type) {
+ createInstanceOf => [
+ it.value = term.toTerm
+ it.range = type.toTypeReference
+ ]
+ }
+
+ // QuantifiedExpressions
+
+ def public 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) {
+ Forall(variables,expression) }
+ def public Forall(Iterable extends Variable> variables,TermDescription expression) {
+ val forallExpression = createForall
+ for(variable : variables) forallExpression.quantifiedVariables += variable
+ forallExpression.expression = expression.toTerm
+ return forallExpression
+ }
+
+ def public 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) {
+ Exists(variables,expression) }
+ def public Exists(Iterable extends Variable> variables, TermDescription expression) {
+ val existsExpression = createExists
+ for(variable : variables) existsExpression.quantifiedVariables += variable
+ existsExpression.expression = expression.toTerm
+ return existsExpression
+ }
+
+ // Function calls
+ def public call(Function function, TermDescription... substitutions) {
+ call(function, substitutions as Iterable extends TermDescription>) }
+ def public call(Function function, Iterable extends TermDescription> substitutions) {
+ val functionReference = createSymbolicValue
+ functionReference.symbolicReference=function
+ val List l= new LinkedList()
+ l.addAll(substitutions)
+ for(substitution : l)
+ functionReference.parameterSubstitutions += substitution.toTerm
+ functionReference.checkFunctionCall(function)
+ return functionReference
+ }
+ def private checkFunctionCall(SymbolicValue value, Function referredFunction) {
+ if(value.parameterSubstitutions.size != referredFunction.parameters.size)
+ throw new LogicProblemBuilderException(
+ '''The function called has «referredFunction.parameters.size» parameters but it is called with «value.parameterSubstitutions.size»!''')
+ }
+
+ // Relation calls
+ def public call(Relation relation, TermDescription... substitution) { relation.call(substitution as Iterable extends TermDescription>)}
+ def public call(Relation relation, Iterable extends TermDescription> substitution) {
+ val relationReference = createSymbolicValue
+ relationReference.symbolicReference = relation
+ //println('''«relation.name»(«substitution.size»->«relation.parameters»)''')
+ for(value : substitution)
+ relationReference.parameterSubstitutions += value.toTerm
+ relationReference.checkRelationCall(relation)
+ return relationReference
+ }
+ def private checkRelationCall(SymbolicValue value, Relation referredRelation) {
+ if(value.parameterSubstitutions.size != referredRelation.parameters.size) {
+ throw new LogicProblemBuilderException(
+ '''The relation "«referredRelation.name»" called has «referredRelation.parameters.size» parameters but it is called with «value.parameterSubstitutions.size»!''')
+ }
+ }
+
+ // constant evaluation
+ def public call(Constant constant) {
+ val constantReference = createSymbolicValue
+ constantReference.symbolicReference = constant
+ return constantReference
+ }
+
+
+}
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend
new file mode 100644
index 00000000..2e3d57cf
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend
@@ -0,0 +1,47 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.builder
+
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+
+abstract class LogicReasoner {
+ def abstract LogicResult solve(
+ LogicProblem problem,
+ LogicSolverConfiguration configuration,
+ ReasonerWorkspace workspace) throws LogicReasonerException
+ def abstract LogicModelInterpretation getInterpretation(ModelResult modelResult)
+}
+
+public class LogicReasonerException extends Exception {
+ new(String message, Exception cause) { super(message,cause) }
+ new(Exception cause) { super("The reasoner has failed",cause)}
+ new(String message) { super(message) }
+}
+
+abstract class LogicSolverConfiguration {
+ public static val Unlimited = -1;
+ public static val String UndefinedPath = null
+
+ /** The URI string to the independent solver application */
+ public String solverPath = UndefinedPath
+ /** Max runtime limit in seconds. */
+ public int runtimeLimit = Unlimited
+ /** Max runtime limit in seconds. */
+ public int memoryLimit = Unlimited
+
+ public var TypeScopes typeScopes = new TypeScopes;
+ public var SolutionScope solutionScope = new SolutionScope
+}
+
+public class TypeScopes{
+ public static val Unlimited = -1;
+ public var maxIntScope = Unlimited
+ public var minNewElements = 0
+ public var maxNewElements = Unlimited
+}
+
+public class SolutionScope{
+ public static val Unlimited = -1;
+ public var numberOfRequiredSolution = 1
+}
\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend
new file mode 100644
index 00000000..b3e44b46
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend
@@ -0,0 +1,407 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.builder
+
+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.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
+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.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.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.LogiclanguageFactory
+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.RealLiteral
+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.SymbolicDeclaration
+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.TermDescription
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import java.math.BigDecimal
+import java.util.ArrayList
+import java.util.Collection
+import java.util.Collections
+import java.util.HashMap
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import org.eclipse.xtend.lib.annotations.Data
+
+@Data class InterpretationValidationResult {
+ val List problems;
+ val List invalidAssertions;
+ def isValid() { return problems.empty && invalidAssertions.empty}
+}
+
+class LogicStructureBuilder{
+ val protected extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+
+ def public dispatch Collection getElements(LogicModelInterpretation interpretation, TypeDeclaration type) {
+ return interpretation.getElements(type)
+ }
+ def public dispatch Collection getElements(LogicModelInterpretation interpretation, TypeDefinition type) {
+ return type.elements
+ }
+
+ def public Term evalAsTerm(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap).toTerm }
+ def public boolean evalAsBool(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as Boolean}
+ def public int evalAsInt(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as Integer }
+ def public BigDecimal evalAsReal(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as BigDecimal }
+ /**
+ * Evaluate the expression on a solution to an logic element.
+ * @param interpretation The interpretation which the expression is evaluated on.
+ * @param term An expression which results in a logic element.
+ * @return The logic element value of the expression. Returns the element directly, not a symbolic reference!
+ */
+ def public DefinedElement evalAsElement(LogicModelInterpretation interpretation, TermDescription term) { term.resolve(interpretation,emptyMap) as DefinedElement}
+ /**
+ * Checks if the interpretation is a valid solution of the problem by checking the satisfactions of each assertion.
+ * Returns the collection of failed assertions.
+ * @param interpretation The checked interpretation.
+ * @param problem The interpretation is checked on this problem.
+ * @return The collection of failed assertions.
+ */
+ def public validateInterpretationOnProblem(LogicModelInterpretation interpretation, LogicProblem problem) {
+ val List problems = new LinkedList
+
+ // Checking types
+ val type2ElementsMap = problem.types.toInvertedMap[interpretation.getElements(it)]
+
+ // Checking definition does not changed
+ for(type : problem.types.filter(TypeDefinition)) {
+ val elements = type2ElementsMap.get(type)
+ if(!type.elements.containsAll(elements))
+ problems+='''The interpretation of «type.name» does not contains each elements of the problem'''
+ if(!elements.containsAll(type.elements))
+ problems+='''The interpretation of «type.name» does not contains additional elements not specified in the problem'''
+ }
+ // Checking the type table
+ val allElements = type2ElementsMap.values.flatten.toSet
+ for (element : allElements) {
+ if(! checkElement(problem, type2ElementsMap, element)) {
+ problems += '''«element.name» does not follows the type hierarchy'''
+ }
+ }
+
+ // Checking assertions
+ val List invalidAssertions = new LinkedList
+ for(assertion : problem.assertions) {
+ if(! interpretation.evalAsBool(assertion.value)) {
+ invalidAssertions+= assertion
+ problems += '''«assertion.name» is violated!'''
+ }
+ }
+ return new InterpretationValidationResult(problems,invalidAssertions)
+ //problem.assertions.filter[x | ! interpretation.evalAsBool(x.value)]
+ }
+
+ private def checkElement(LogicProblem problem, Map> type2ElementsMap, DefinedElement element) {
+ val compatibleDynamicTypes = new LinkedList
+ for(possibleDynamicType: problem.types.filter[!it.isIsAbstract]) {
+ //println(possibleDynamicType.name)
+ val compatibleTypes = possibleDynamicType.transitiveClosureStar[it.supertypes]
+ //compatibleTypes.forEach[print(''' + «it.name»''')]
+ val incompatibleTypes = problem.types.filter[!compatibleTypes.contains(it)]
+ //incompatibleTypes.forEach[print(''' - «it.name»''')]
+ if(compatibleTypes.forall[ type2ElementsMap.get(it).contains(element)] && incompatibleTypes.forall[!type2ElementsMap.get(it).contains(element)]) {
+ //println("Ok")
+ compatibleDynamicTypes += possibleDynamicType
+ }
+ }
+ return compatibleDynamicTypes.size == 1
+ }
+
+ def protected dispatch Term toTerm(Integer o) { createIntLiteral=>[value = o] }
+ def protected dispatch Term toTerm(BigDecimal o) { createRealLiteral=>[value = o]}
+ def protected dispatch Term toTerm(Boolean o) { createBoolLiteral=>[value = o]}
+ def protected dispatch Term toTerm(SymbolicDeclaration o) { createSymbolicValue=>[symbolicReference = o]}
+ def public Term termDescriptiontoTerm(TermDescription term) {
+ if(term instanceof Term) return term
+ else if (term instanceof Variable) return createSymbolicValue => [symbolicReference = term]
+ else if (term instanceof Constant) return createSymbolicValue=>[symbolicReference = term]
+ else if (term instanceof DefinedElement) return createSymbolicValue => [symbolicReference = term]
+ else throw new UnsupportedOperationException("Can not create reference for symbolic declaration " + term.class.name)
+ }
+ /**
+ * Returns if the operation with the numbers in the parameter requires the use of BigDecimal.
+ */
+ def private isBigDecimalRequired(Object... numbers) { return numbers.exists[it instanceof BigDecimal || it instanceof RealLiteral] }
+ def private dispatch BigDecimal asBigDecimal(IntLiteral i) { i.value.asBigDecimal }
+ def private dispatch BigDecimal asBigDecimal(RealLiteral i) { i.value.asBigDecimal }
+ def private dispatch BigDecimal asBigDecimal(Integer i) { BigDecimal.valueOf(i) }
+ def private dispatch BigDecimal asBigDecimal(BigDecimal i) { i }
+ def private dispatch Integer asInteger(Integer i) { i }
+ def private dispatch Integer asInteger(BigDecimal i) { i.intValue }
+ def private dispatch Integer asInteger(IntLiteral i) { i.value.asInteger }
+
+ // Atomic resoulutions
+ def protected dispatch Object resolve(IntLiteral literal, LogicModelInterpretation interpretation, Map variableBinding) { return literal.value as Integer }
+ def protected dispatch Object resolve(BoolLiteral literal, LogicModelInterpretation interpretation, Map variableBinding) { return literal.value }
+ def protected dispatch Object resolve(RealLiteral literal, LogicModelInterpretation interpretation, Map variableBinding) { return literal.value as BigDecimal }
+
+ def protected dispatch Object resolve(Not not, LogicModelInterpretation interpretation, Map variableBinding) {
+ return ! (not.operand.resolve(interpretation,variableBinding) as Boolean) }
+ def protected dispatch Object resolve(And and, LogicModelInterpretation interpretation, Map variableBinding) {
+ //for(operand : and.operands) {
+ //val r = operand.resolve(interpretation,variableBinding) as Boolean
+ //println(r)
+ //}
+ return and.operands.forall[resolve(interpretation,variableBinding) as Boolean] as Boolean }
+ def protected dispatch Object resolve(Or or, LogicModelInterpretation interpretation, Map variableBinding) {
+ //val resolved = or.operands.map[resolve(interpretation,variableBinding) as Boolean]
+ //println(resolved)
+ return or.operands.exists[resolve(interpretation,variableBinding) as Boolean] }
+ def protected dispatch Object resolve(Impl impl, LogicModelInterpretation interpretation, Map variableBinding) {
+ val left = impl.leftOperand. resolve(interpretation,variableBinding) as Boolean
+ val right = impl.rightOperand.resolve(interpretation,variableBinding) as Boolean
+ return (! left) || (right) }
+ def protected dispatch Object resolve(Iff iff, LogicModelInterpretation interpretation, Map variableBinding) {
+ return (iff.leftOperand.resolve(interpretation,variableBinding) as Boolean) ==
+ (iff.rightOperand.resolve(interpretation,variableBinding) as Boolean) }
+ def protected dispatch Object resolve(IfThenElse ite, LogicModelInterpretation interpretation, Map variableBinding) {
+ val condition = ite.condition.resolve(interpretation,variableBinding) as Boolean
+ if(condition) return ite.ifTrue.resolve(interpretation,variableBinding)
+ else return ite.ifFalse.resolve(interpretation,variableBinding)
+ }
+ def protected dispatch Object resolve(MoreThan moreThan, LogicModelInterpretation interpretation, Map variableBinding) {
+ val left = moreThan.leftOperand.resolve(interpretation,variableBinding) as Number
+ val right = moreThan.rightOperand.resolve(interpretation,variableBinding) as Number
+ if(isBigDecimalRequired(left,right)) {
+ return left.asBigDecimal.compareTo(right.asBigDecimal) > 0 }
+ else { return left.asInteger > right.asInteger } }
+ def protected dispatch Object resolve(LessThan lessThan, LogicModelInterpretation interpretation, Map variableBinding) {
+ val left = lessThan.leftOperand.resolve(interpretation,variableBinding) as Number
+ val right = lessThan.rightOperand.resolve(interpretation,variableBinding) as Number
+ if(isBigDecimalRequired(left,right)) {
+ return left.asBigDecimal.compareTo(right.asBigDecimal) < 0 }
+ else { return left.asInteger < right.asInteger } }
+ def protected dispatch Object resolve(MoreOrEqualThan moreThan, LogicModelInterpretation interpretation, Map variableBinding) {
+ val left = moreThan.leftOperand.resolve(interpretation,variableBinding) as Number
+ val right = moreThan.rightOperand.resolve(interpretation,variableBinding) as Number
+ if(isBigDecimalRequired(left,right)) {
+ return left.asBigDecimal.compareTo(right.asBigDecimal) >= 0 }
+ else { return left.asInteger >= right.asInteger } }
+ def protected dispatch Object resolve(LessOrEqualThan lessThan, LogicModelInterpretation interpretation, Map variableBinding) {
+ val left = lessThan.leftOperand.resolve(interpretation,variableBinding) as Number
+ val right = lessThan.rightOperand.resolve(interpretation,variableBinding) as Number
+ if(isBigDecimalRequired(left,right)) return left.asBigDecimal.compareTo(right.asBigDecimal) <= 0
+ else { return left.asInteger <= right.asInteger } }
+
+
+ def protected dispatch Object resolve(Equals equals, LogicModelInterpretation interpretation, Map variableBinding) {
+ val left = equals.leftOperand.resolve(interpretation,variableBinding)
+ val right = equals.rightOperand.resolve(interpretation,variableBinding)
+ return compare(left,right)
+ }
+ def protected dispatch Object resolve(Distinct distinct, LogicModelInterpretation interpretation, Map variableBinding) {
+ val elements = distinct.operands.map[it.resolve(interpretation,variableBinding)]
+ if(elements.size== 0) return true
+ else {
+ val res = (0.. variableBinding) {
+ val left = plus.leftOperand.resolve(interpretation,variableBinding) as Number
+ val right = plus.rightOperand.resolve(interpretation,variableBinding) as Number
+ if(isBigDecimalRequired(left,right)) return left.asBigDecimal.add(right.asBigDecimal)
+ else return left.asInteger + right.asInteger
+ }
+ def protected dispatch Object resolve(Minus minus, LogicModelInterpretation interpretation, Map variableBinding) {
+ val left = minus.leftOperand.resolve(interpretation,variableBinding) as Number
+ val right = minus.rightOperand.resolve(interpretation,variableBinding) as Number
+ if(isBigDecimalRequired(left,right)) return left.asBigDecimal.subtract(right.asBigDecimal)
+ else return left.asInteger - right.asInteger
+ }
+ def protected dispatch Object resolve(Multiply multiply, LogicModelInterpretation interpretation, Map variableBinding) {
+ val left = multiply.leftOperand.resolve(interpretation,variableBinding)
+ val right = multiply.rightOperand.resolve(interpretation,variableBinding)
+ if(isBigDecimalRequired(left,right)) return left.asBigDecimal.multiply(right.asBigDecimal)
+ else return left.asInteger * right.asInteger
+ }
+ def protected dispatch Object resolve(Divison divide, LogicModelInterpretation interpretation, Map variableBinding) {
+ val left = divide.leftOperand.resolve(interpretation,variableBinding) as Number
+ val right = divide.rightOperand.resolve(interpretation,variableBinding) as Number
+ if(isBigDecimalRequired(left,right)) return left.asBigDecimal.divide(right.asBigDecimal)
+ return left.asInteger / right.asInteger
+ }
+ def protected dispatch Object resolve(Mod modulo, LogicModelInterpretation interpretation, Map variableBinding) {
+ val left = modulo.leftOperand.resolve(interpretation,variableBinding) as Number
+ val right = modulo.rightOperand.resolve(interpretation,variableBinding) as Number
+ if(isBigDecimalRequired(left,right)) return left.asBigDecimal.remainder(right.asBigDecimal)
+ else return left.asInteger % right.asInteger
+ }
+
+ def protected dispatch Object resolve(Exists exists, LogicModelInterpretation interpretation, Map variableBinding) {
+ executeExists(exists.expression,interpretation,variableBinding,exists.quantifiedVariables) }
+ def protected dispatch Object resolve(Forall forall, LogicModelInterpretation interpretation, Map variableBinding) {
+ executeForall(forall.expression,interpretation,variableBinding,forall.quantifiedVariables) }
+
+ def protected dispatch Object resolve(SymbolicValue symbolicValue, LogicModelInterpretation interpretation, Map variableBinding) {
+ val referenced = symbolicValue.symbolicReference
+ if(referenced instanceof DefinedElement) {
+ return referenced
+ } else if(referenced instanceof Variable) {
+ return variableBinding.get(referenced)
+ } else if(referenced instanceof FunctionDeclaration) {
+ val parameterSubstitution = new ArrayList