From ed434397058fd520ad92a938eccd8f93ef378d8a Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 14 Apr 2020 22:45:52 +0200 Subject: restructured pattern generation --- .../formulacanonization/CanonisedFormulae.xtend | 2 - .../formulacanonization/FormulaCanoniser.xtend | 36 +++- .../patterns/PConstraintTransformer.xtend | 192 +++++++++++++++++++++ .../logic2viatra/patterns/PatternGenerator.xtend | 102 ++++++++++- .../patterns/RelationDefinitionIndexer.xtend | 173 +------------------ 5 files changed, 327 insertions(+), 178 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend index e511a961..fd4374f5 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend @@ -11,7 +11,5 @@ import org.eclipse.xtend.lib.annotations.Data class CanonisedFormulae { CharSequence viatraCode Map assertion2ConstraintPattern - Map constant2ValuePattern Map relation2ValuePattern - Map function2ValuePattern } \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend index 0af0b36a..182f3a3a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend @@ -5,17 +5,35 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition import java.util.List +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable /** - * Translates a set of assertions and definitions to viatra patterns. + * Translates a Terms into format + * := Bodies(x1,...,xn) + * := | or + * := Exists y1,...,ym : + * := Constraint(x1,...xn) | Constraint(x1,...,xn) and */ class FormulaCanoniser { - def canonise( - List assertions, - List relations, - List constants, - List functions) - { - - } +// def canonise( +// List assertions, +// List relations) +// { +// +// } +// +// +// def canoniseToConstraintBlock(Term predicate, List variables) { +// val +// } +// +// def freeVariables(Term t) { +// val subterms = #[t]+t.eAllContents.toList +// val variables = subterms.filter(Variable).toSet +// val variableReferences = subterms.filter(SymbolicValue).filter[it.symbolicReference instanceof Variable] +// val freeVariables = variableReferences.filter[!variables.contains(it.symbolicReference)] +// return freeVariables.map +// } } \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend new file mode 100644 index 00000000..64fbb2f1 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend @@ -0,0 +1,192 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.viatra2logic.XExpressionExtractor +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import org.eclipse.emf.ecore.EAttribute +import org.eclipse.emf.ecore.EEnumLiteral +import org.eclipse.emf.ecore.EReference +import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey +import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey +import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint + +class PConstraintTransformer { + val extension RelationDefinitionIndexer relationDefinitionIndexer; + val expressionExtractor = new XExpressionExtractor + + new(RelationDefinitionIndexer relationDefinitionIndexer) { + this.relationDefinitionIndexer = relationDefinitionIndexer + } + + dispatch def transformConstraint(TypeConstraint constraint, Modality modality) { + val touple = constraint.variablesTuple + if(touple.size == 1) { + val inputKey = constraint.equivalentJudgement.inputKey + if(inputKey instanceof EClassTransitiveInstancesKey) { + return relationDefinitionIndexer.base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, + constraint.getVariableInTuple(0).canonizeName) + } else if(inputKey instanceof EDataTypeInSlotsKey){ + return '''// type constraint is enforced by construction''' + } + + } else if(touple.size == 2){ + val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey + if(key instanceof EReference) { + return base.referRelationByName( + key, + constraint.getVariableInTuple(0).canonizeName, + constraint.getVariableInTuple(1).canonizeName, + modality.toMustMay) + } else if (key instanceof EAttribute) { + return base.referAttributeByName(key, + constraint.getVariableInTuple(0).canonizeName, + constraint.getVariableInTuple(1).canonizeName, + modality.toMustMay) + } else throw new UnsupportedOperationException('''unknown key: «key.class»''') + } else { + throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') + } + } + dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) { + val touple = constraint.variablesTuple + if(touple.size == 1) { + val inputKey = constraint.equivalentJudgement.inputKey + if(inputKey instanceof EClassTransitiveInstancesKey) { + return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, + (constraint.getVariablesTuple.get(0) as PVariable).canonizeName) + } else if(inputKey instanceof EDataTypeInSlotsKey){ + return '''// type constraint is enforced by construction''' + } + + } else if(touple.size == 2){ + val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey + if(key instanceof EReference) { + return base.referRelationByName( + key, + (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, + (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, + modality.toMustMay) + } else if (key instanceof EAttribute) { + return base.referAttributeByName(key, + (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, + (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, + modality.toMustMay) + } else throw new UnsupportedOperationException('''unknown key: «key.class»''') + } else { + throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') + } + } + + dispatch def transformConstraint(Equality equality, Modality modality) { + val a = equality.who + val b = equality.withWhom + transformEquality(modality.toMustMay, a, b) + } + + private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { + if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' + else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' + } + + dispatch def transformConstraint(Inequality inequality, Modality modality) { + val a = inequality.who + val b = inequality.withWhom + if(modality.isCurrent) { + return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' + } else if(modality.isMust) { + return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' + } else { // modality.isMay + return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' + } + } + + dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) { + val params = (0.. relations, Map fqn2PQuery) { @@ -74,7 +61,7 @@ class RelationDefinitionIndexer { private def relationDefinitionName(RelationDefinition relation, Modality modality) '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' - private def canonizeName(PVariable v) { + def canonizeName(PVariable v) { return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»''' } @@ -87,7 +74,7 @@ class RelationDefinitionIndexer { «FOR body : p.disjunctBodies.bodies SEPARATOR "or"»{ find interpretation(problem,interpretation); «FOR constraint : body.constraints» - «constraint.transformConstraint(modality)» + «this.constraintTransformer.transformConstraint(constraint,modality)» «ENDFOR» }«ENDFOR» ''' @@ -104,158 +91,14 @@ class RelationDefinitionIndexer { ''' } - private def toMustMay(Modality modality) { + def toMustMay(Modality modality) { if(modality == Modality::MAY) return Modality::MAY else return Modality::MUST } - def public referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) ''' + def referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) ''' «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»); ''' - private dispatch def transformConstraint(TypeConstraint constraint, Modality modality) { - val touple = constraint.variablesTuple - if(touple.size == 1) { - val inputKey = constraint.equivalentJudgement.inputKey - if(inputKey instanceof EClassTransitiveInstancesKey) { - return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, - constraint.getVariableInTuple(0).canonizeName) - } else if(inputKey instanceof EDataTypeInSlotsKey){ - return '''// type constraint is enforced by construction''' - } - - } else if(touple.size == 2){ - val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey - if(key instanceof EReference) { - return base.referRelationByName( - key, - constraint.getVariableInTuple(0).canonizeName, - constraint.getVariableInTuple(1).canonizeName, - modality.toMustMay) - } else if (key instanceof EAttribute) { - return base.referAttributeByName(key, - constraint.getVariableInTuple(0).canonizeName, - constraint.getVariableInTuple(1).canonizeName, - modality.toMustMay) - } else throw new UnsupportedOperationException('''unknown key: «key.class»''') - } else { - throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') - } - } - private dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) { - val touple = constraint.variablesTuple - if(touple.size == 1) { - val inputKey = constraint.equivalentJudgement.inputKey - if(inputKey instanceof EClassTransitiveInstancesKey) { - return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, - (constraint.getVariablesTuple.get(0) as PVariable).canonizeName) - } else if(inputKey instanceof EDataTypeInSlotsKey){ - return '''// type constraint is enforced by construction''' - } - - } else if(touple.size == 2){ - val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey - if(key instanceof EReference) { - return base.referRelationByName( - key, - (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, - (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, - modality.toMustMay) - } else if (key instanceof EAttribute) { - return base.referAttributeByName(key, - (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, - (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, - modality.toMustMay) - } else throw new UnsupportedOperationException('''unknown key: «key.class»''') - } else { - throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') - } - } - - private dispatch def transformConstraint(Equality equality, Modality modality) { - val a = equality.who - val b = equality.withWhom - transformEquality(modality.toMustMay, a, b) - } - - private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { - if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' - else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' - } - - private dispatch def transformConstraint(Inequality inequality, Modality modality) { - val a = inequality.who - val b = inequality.withWhom - if(modality.isCurrent) { - return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' - } else if(modality.isMust) { - return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' - } else { // modality.isMay - return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' - } - } - - private dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) { - val params = (0..