From 9d33b30f59574cb896e9f33bfb4b902d217d1c93 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Fri, 8 May 2020 17:21:48 +0200 Subject: Unit propagation trace fixes --- .../UnitPropagationPreconditionGenerator.xtend | 109 +++++++++++---------- 1 file changed, 59 insertions(+), 50 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend index f726a24f..b5e344f7 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend @@ -22,6 +22,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativeP import java.util.Comparator import java.util.ArrayList import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction +import java.util.LinkedHashSet @Data class UnitPropagation { val PQuery q @@ -75,11 +76,11 @@ class UnitPropagationPreconditionGenerator { // Create an empty result val res = new UnitPropagationPreconditionGenerationResult val wfs = base.wfQueries(problem)//.map[it.patternPQuery] - val mainPropagationNames = new LinkedList + val mainPropagationNames = new LinkedHashSet for(wf : wfs) { val query = wf.patternPQuery as PQuery val relation = wf.target - val allReferredChecks = query.allReferredConstraints.filter(ExpressionEvaluation) + val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) for(referredCheck : allReferredChecks) { mainPropagationNames+= getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) @@ -90,15 +91,20 @@ class UnitPropagationPreconditionGenerator { «def» «ENDFOR» - // Main propagations: - «FOR name : mainPropagationNames» - «name» - «ENDFOR» + // Main propagations: «FOR name : mainPropagationNames SEPARATOR ", "»«name»«ENDFOR» ''' } - def allReferredConstraints(PQuery query) { + def allReferredConstraints(Relation relation, PQuery query) { val allReferredQueries = query.allReferredQueries - return (#[query]+allReferredQueries).map[it.disjunctBodies.bodies].flatten.map[constraints].flatten + val problem = relation.eContainer as LogicProblem + val constraints = new LinkedHashSet + for(referredQuery: #[query]+allReferredQueries) { + val referredRelation = problem.annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredQuery].head.target + val bodies = (referredRelation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies + constraints.addAll(bodies.map[getConstraints].flatten) + } + + return constraints } def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) { @@ -141,60 +147,63 @@ class UnitPropagationPreconditionGenerator { // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied } else { val positives = body.constraints.filter(PositivePatternCall) - val positiveRefers = positives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)] - for(positiveRefer: positiveRefers) { - val referredPQuery = positiveRefer.referredQuery + for(positive: positives) { + val referredPQuery = positive.referredQuery val referredRelation = (relation.eContainer as LogicProblem) .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target - val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3) - if(referredName !== null) { - generatedBodies += ''' - // Original Constraints - «FOR constraint : body.constraints.filter[it !== positiveRefer]» - «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» - «ENDFOR» - // Propagation for constraint referred indirectly from this pattern through «referredName» - find «referredName»(problem, interpretation, - «FOR index : 0..=0) { + if(generatedBodies.empty) { res.registerUnsatQuery(q,c,pm,m3) } else { val definition = ''' @@ -229,7 +238,7 @@ class UnitPropagationPreconditionGenerator { } val variablesInOrder = new ArrayList(c.affectedVariables) variablesInOrder.toList.sort(comparator) - return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).name»==«canonizeName(variableIndex,m)»;«ENDFOR»''' + return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).canonizeName»==«canonizeName(variableIndex,m)»;«ENDFOR»''' } def dispatch propagateVariables(PConstraint c, PropagationModality m) { throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''') -- cgit v1.2.3-70-g09d2 From bf0ddbc789689fdaa60d5f648fd35597b2b869b3 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Fri, 8 May 2020 18:46:10 +0200 Subject: contained objects instantiated immediately if target class non-abstract --- .../rules/RefinementRuleProvider.xtend | 59 +++++++++++----------- 1 file changed, 30 insertions(+), 29 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index b4cb9ec7..7e53f944 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend @@ -179,36 +179,37 @@ class RefinementRuleProvider { if(containmentReferences.contains(relation)) { val targetTypeInterpretation = getTypeInterpretation(i, relation, 1) - - val inverseAnnotation = p.assertions.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation] - if(!inverseAnnotation.empty) { - val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) { - inverseAnnotation.head.inverseB + if(!(targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.isIsAbstract) { + val inverseAnnotation = p.assertions.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation] + if(!inverseAnnotation.empty) { + val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) { + inverseAnnotation.head.inverseB + } else { + inverseAnnotation.head.inverseA + } + val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head + for(var times=0; times Date: Fri, 8 May 2020 23:32:07 +0200 Subject: UP patterns -> decision procedure trace finished --- .../logic2viatra/patterns/PatternGenerator.xtend | 8 ++-- .../logic2viatra/patterns/PatternProvider.xtend | 16 ++++++-- .../UnitPropagationPreconditionGenerator.xtend | 43 +++++++++++++++++++--- .../rules/RefinementRuleProvider.xtend | 6 +-- 4 files changed, 59 insertions(+), 14 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index 56138ee8..d5ebe318 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend @@ -155,8 +155,8 @@ class PatternGenerator { Map fqn2PQuery, TypeAnalysisResult typeAnalysisResult ) { - - return ''' + val first = + ''' import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" @@ -395,7 +395,9 @@ class PatternGenerator { ////////// // 5 Unit Propagations ////////// - «unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)» ''' + val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery) + val second = up.definitions + return (first+second) -> up.constraint2PreconditionName } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index 0e13a5e1..f576d1a1 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend @@ -21,6 +21,8 @@ import org.eclipse.xtend.lib.annotations.Data import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* import java.util.Collection import java.util.Set +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +import java.util.HashMap @Data class GeneratedPatterns { public Map>> invalidWFQueries @@ -29,6 +31,7 @@ import java.util.Set public Map>> refineObjectQueries public Map>> refineTypeQueries public Map, IQuerySpecification>> refinerelationQueries + public Map>> unitPropagationPreconditionPatterns public Collection>> allQueries } @@ -56,13 +59,15 @@ class PatternProvider { } else { null } - val baseIndexerFile = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) + val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) + val baseIndexerFile = patternGeneratorResult.key + val unitPropagationTrace = patternGeneratorResult.value if(writeToFile) { workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) } val ParseUtil parseUtil = new ParseUtil val generatedQueries = parseUtil.parse(baseIndexerFile) - val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,generatedQueries); + val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,unitPropagationTrace,generatedQueries); return runtimeQueries } @@ -71,7 +76,8 @@ class PatternProvider { LogicProblem problem, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult, - Map>> queries + HashMap unitPropagationTrace, + Map>> queries ) { val Map>> invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] @@ -85,6 +91,9 @@ class PatternProvider { refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] val Map, IQuerySpecification>> refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] + val Map>> + unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)] + unitPropagationPreconditionPatterns.entrySet.forEach[println(it.key + "->" +it.value)] return new GeneratedPatterns( invalidWFQueries, unfinishedWFQueries, @@ -92,6 +101,7 @@ class PatternProvider { refineObjectsQueries, refineTypeQueries, refineRelationQueries, + unitPropagationPreconditionPatterns, queries.values ) } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend index b5e344f7..7cf52b41 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend @@ -58,6 +58,11 @@ class UnitPropagationPreconditionGenerationResult { return unitPropagation2PatternName.get(key) !== null } } +@Data +class UnitPropagationPreconditionFinalResult { + CharSequence definitions + HashMap constraint2PreconditionName +} class UnitPropagationPreconditionGenerator { val PatternGenerator base @@ -76,23 +81,51 @@ class UnitPropagationPreconditionGenerator { // Create an empty result val res = new UnitPropagationPreconditionGenerationResult val wfs = base.wfQueries(problem)//.map[it.patternPQuery] - val mainPropagationNames = new LinkedHashSet + val Map>> mainPropagationNames = new HashMap for(wf : wfs) { val query = wf.patternPQuery as PQuery val relation = wf.target val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) for(referredCheck : allReferredChecks) { - mainPropagationNames+= getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) + val propagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) + if(!mainPropagationNames.containsKey(referredCheck)) { + mainPropagationNames.put(referredCheck,new LinkedList) + } + if(propagationPrecondition !== null) { + println(query.parameterNames) + println(query.parameterNames.size) + mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size) + } } } - return ''' + val preconditions = new LinkedList + val constraint2Precondition = new HashMap + for(entry : mainPropagationNames.entrySet) { + val name = '''UPMUSTPropagate«res.getOrGenerateConstraintName(entry.key)»'''; + val def = ''' + pattern «name»( + problem:LogicProblem, interpretation:PartialInterpretation, + «FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») + «FOR propagation : entry.value SEPARATOR " or "» + { find «propagation.key»(problem,interpretation,«FOR index : 0.. Date: Fri, 8 May 2020 23:45:36 +0200 Subject: removed unnecesary logging --- .../logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend | 2 -- 1 file changed, 2 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend index 7cf52b41..6c68ec94 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend @@ -93,8 +93,6 @@ class UnitPropagationPreconditionGenerator { mainPropagationNames.put(referredCheck,new LinkedList) } if(propagationPrecondition !== null) { - println(query.parameterNames) - println(query.parameterNames.size) mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size) } } -- cgit v1.2.3-70-g09d2 From 3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Sat, 9 May 2020 20:33:19 +0200 Subject: Numeric Solver integration to exploration --- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 2 +- .../viatra2logic/NumericProblemSolver.java | 334 +++++++++++---------- .../viatra2logic/NumericTranslator.xtend | 64 ++++ .../ModelGenerationMethodProvider.xtend | 7 + .../logic2viatra/patterns/PatternProvider.xtend | 1 - .../UnitPropagationPreconditionGenerator.xtend | 6 +- .../viatrasolver/reasoner/ViatraReasoner.xtend | 2 +- .../dse/BestFirstStrategyForModelGeneration.java | 32 +- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 114 +++++++ .../reasoner/dse/SolutionStoreWithCopy.xtend | 3 +- 10 files changed, 387 insertions(+), 178 deletions(-) create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend index a27e8904..b4303739 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend @@ -26,7 +26,7 @@ class ExpressionEvaluation2Logic { // numericSolver.testIsNotSat(expression, expression.transform(variable2Variable)); // numericSolver.testGetOneSol(expression, expression.transform(variable2Variable)); // numericSolver.testGetOneSol2(expression, expression.transform(variable2Variable)); - numericSolver.testGetOneSol3(expression, expression.transform(variable2Variable)); +// numericSolver.testGetOneSol3(expression, expression.transform(variable2Variable)); // numericSolver.testIsSat(expression, expression.transform(variable2Variable)); return expression.transform(variable2Variable) diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java index ff3a85eb..0e6e824c 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java @@ -5,9 +5,12 @@ import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Map; +import java.util.Map.Entry; import java.util.Random; import java.util.Set; +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint; +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation; import org.eclipse.xtext.common.types.JvmIdentifiableElement; import org.eclipse.xtext.xbase.XBinaryOperation; import org.eclipse.xtext.xbase.XExpression; @@ -46,6 +49,7 @@ public class NumericProblemSolver { private static final String N_EQUALS3 = "operator_tripleEquals"; private static final String N_NOTEQUALS3 = "operator_tripleNotEquals"; + private Context ctx; private Solver s; private Map varMap; @@ -63,6 +67,170 @@ public class NumericProblemSolver { return ctx; } + + private ArrayList getJvmIdentifiableElements(XExpression expression) { + ArrayList allElem = new ArrayList(); + XExpression left = ((XBinaryOperation) expression).getLeftOperand(); + XExpression right = ((XBinaryOperation) expression).getRightOperand(); + + getJvmIdentifiableElementsHelper(left, allElem); + getJvmIdentifiableElementsHelper(right, allElem); + return allElem; + } + + private void getJvmIdentifiableElementsHelper(XExpression e, List allElem) { + if (e instanceof XFeatureCall) { + allElem.add(((XFeatureCall) e).getFeature()); + } else if (e instanceof XBinaryOperation) { + getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem); + getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); + } + } + + public boolean isSatisfiable(Map>> matches) throws Exception { + BoolExpr problemInstance = formNumericProblemInstance(matches); + s.add(problemInstance); + return s.check() == Status.SATISFIABLE; + } + + public Map getOneSolution(List objs, Map>> matches) throws Exception { + Map sol = new HashMap(); + long startformingProblem = System.currentTimeMillis(); + BoolExpr problemInstance = formNumericProblemInstance(matches); + long endformingProblem = System.currentTimeMillis(); + System.out.println("Forming problem: " + (endformingProblem - startformingProblem)); + s.add(problemInstance); + long startSolvingProblem = System.currentTimeMillis(); + if (s.check() == Status.SATISFIABLE) { + Model m = s.getModel(); + long endSolvingProblem = System.currentTimeMillis(); + System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); + long startFormingSolution = System.currentTimeMillis(); + for (PrimitiveElement o: objs) { + if(varMap.containsKey(o)) { + IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); + Integer oSol = Integer.parseInt(val.toString()); + //System.out.println("Solution:" + o + "->" + oSol); + sol.put(o, oSol); + } else { + //System.out.println("not used var:" + o); + } + } + long endFormingSolution = System.currentTimeMillis(); + System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); + } else { + System.out.println("Unsatisfiable"); + } + + return sol; + } + + private BoolExpr formNumericConstraint(XExpression e, Map aMatch) throws Exception { + if (!(e instanceof XBinaryOperation)) { + throw new Exception ("error in check expression!!!"); + } + + String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); + + BoolExpr constraint = null; + + ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); + ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); + + if (nameEndsWith(name, N_LESSTHAN)) { + constraint = ctx.mkLt(left_operand, right_operand); + } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { + constraint = ctx.mkLe(left_operand, right_operand); + } else if (nameEndsWith(name, N_GREATERTHAN)) { + constraint = ctx.mkGt(left_operand, right_operand); + } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { + constraint = ctx.mkGe(left_operand, right_operand); + } else if (nameEndsWith(name, N_EQUALS)) { + constraint = ctx.mkEq(left_operand, right_operand); + } else if (nameEndsWith(name, N_NOTEQUALS)) { + constraint = ctx.mkDistinct(left_operand, right_operand); + } else if (nameEndsWith(name, N_EQUALS3)) { + constraint = ctx.mkGe(left_operand, right_operand); // ??? + } else if (nameEndsWith(name, N_NOTEQUALS3)) { + constraint = ctx.mkGe(left_operand, right_operand); // ??? + } else { + throw new Exception ("Unsupported binary operation " + name); + } + + return constraint; + } + + // TODO: add variable: state of the solver + private ArithExpr formNumericConstraintHelper(XExpression e, Map aMatch) throws Exception { + ArithExpr expr = null; + // Variables + if (e instanceof XFeatureCall) { + PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); + if (!matchedObj.isValueSet()) { + if (varMap.get(matchedObj) == null) { + String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString(); + expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); + varMap.put(matchedObj, expr); + } else { + expr = (ArithExpr) varMap.get(matchedObj); + } + } else { + int value = ((IntegerElement) matchedObj).getValue(); + expr = (ArithExpr) ctx.mkInt(value); + varMap.put(matchedObj, expr); + } + } + // Constants + else if (e instanceof XNumberLiteral) { + String value = ((XNumberLiteral) e).getValue(); + try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){} + } + // Expressions with operators + else if (e instanceof XBinaryOperation) { + String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); + ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); + ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); + + if (nameEndsWith(name, N_PLUS)) { + expr = ctx.mkAdd(left_operand, right_operand); + } else if (nameEndsWith(name, N_MINUS)) { + expr = ctx.mkAdd(left_operand, ctx.mkUnaryMinus(right_operand)); + } else if (nameEndsWith(name, N_POWER)) { + expr = ctx.mkPower(left_operand, right_operand); + } else if (nameEndsWith(name, N_MULTIPLY)) { + expr = ctx.mkMul(left_operand, right_operand); + } else if (nameEndsWith(name, N_DIVIDE)) { + expr = ctx.mkDiv(left_operand, right_operand); + } else if (nameEndsWith(name, N_MODULO)) { + expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); + } else { + throw new Exception ("Unsupported binary operation " + name); + } + } else { + throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); + } + return expr; + + } + + private boolean nameEndsWith(String name, String end) { + return name.startsWith(N_Base) && name.endsWith(end); + } + + private BoolExpr formNumericProblemInstance(Map>> matches) throws Exception { + BoolExpr constraintInstances = ctx.mkTrue(); + for (XExpression e: matches.keySet()) { + Iterable> matchSets = matches.get(e); + for (Map aMatch: matchSets) { + BoolExpr constraintInstance = ctx.mkNot(formNumericConstraint(e, aMatch)); + constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); + } + } + return constraintInstances; + } + + + /* public void testIsSat(XExpression expression, Term t) throws Exception { int count = 10000; Map>> matches = new HashMap>>(); @@ -87,7 +255,6 @@ public class NumericProblemSolver { System.out.println("Running time:" + (end - start)); } - public void testIsNotSat(XExpression expression, Term t) throws Exception { Map>> matches = new HashMap>>(); Set> matchSet = new HashSet>(); @@ -129,9 +296,9 @@ public class NumericProblemSolver { System.out.println("Number of matches: "); System.out.println("Running time:" + (end - start)); } - + */ - public void testGetOneSol(XExpression expression, Term t) throws Exception { + /*public void testGetOneSol(XExpression expression, Term t) throws Exception { int count = 10; Map>> matches = new HashMap>>(); Set> matchSet = new HashSet>(); @@ -163,8 +330,8 @@ public class NumericProblemSolver { System.out.println("Number of matches: " + count); System.out.println("Running time:" + (end - start)); - } - + }*/ + /* public void testGetOneSol2(XExpression expression, Term t) throws Exception { int count = 250; Map>> matches = new HashMap>>(); @@ -255,160 +422,5 @@ public class NumericProblemSolver { Thread.sleep(3000); } } - - private ArrayList getJvmIdentifiableElements(XExpression expression) { - ArrayList allElem = new ArrayList(); - XExpression left = ((XBinaryOperation) expression).getLeftOperand(); - XExpression right = ((XBinaryOperation) expression).getRightOperand(); - - getJvmIdentifiableElementsHelper(left, allElem); - getJvmIdentifiableElementsHelper(right, allElem); - return allElem; - } - - private void getJvmIdentifiableElementsHelper(XExpression e, List allElem) { - if (e instanceof XFeatureCall) { - allElem.add(((XFeatureCall) e).getFeature()); - } else if (e instanceof XBinaryOperation) { - getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem); - getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); - } - } - - public boolean isSatisfiable(Map>> matches) throws Exception { - BoolExpr problemInstance = formNumericProblemInstance(matches); - s.add(problemInstance); - return s.check() == Status.SATISFIABLE; - } - - public Map getOneSolution(List objs, Map>> matches) throws Exception { - Map sol = new HashMap(); - long startformingProblem = System.currentTimeMillis(); - BoolExpr problemInstance = formNumericProblemInstance(matches); - long endformingProblem = System.currentTimeMillis(); - System.out.println("Forming problem: " + (endformingProblem - startformingProblem)); - s.add(problemInstance); - long startSolvingProblem = System.currentTimeMillis(); - if (s.check() == Status.SATISFIABLE) { - Model m = s.getModel(); - long endSolvingProblem = System.currentTimeMillis(); - System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem)); - long startFormingSolution = System.currentTimeMillis(); - for (Object o: objs) { - IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false); - Integer oSol = Integer.parseInt(val.toString()); - sol.put(o, oSol); - } - long endFormingSolution = System.currentTimeMillis(); - System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution)); - } else { - System.out.println("Unsatisfiable"); - } - - return sol; - } - - private BoolExpr formNumericConstraint(XExpression e, Map aMatch) throws Exception { - if (!(e instanceof XBinaryOperation)) { - throw new Exception ("error in check expression!!!"); - } - - String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); - - BoolExpr constraint = null; - - ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); - ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); - - if (nameEndsWith(name, N_LESSTHAN)) { - constraint = ctx.mkLt(left_operand, right_operand); - } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) { - constraint = ctx.mkLe(left_operand, right_operand); - } else if (nameEndsWith(name, N_GREATERTHAN)) { - constraint = ctx.mkGt(left_operand, right_operand); - } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) { - constraint = ctx.mkGe(left_operand, right_operand); - } else if (nameEndsWith(name, N_EQUALS)) { - constraint = ctx.mkEq(left_operand, right_operand); - } else if (nameEndsWith(name, N_NOTEQUALS)) { - constraint = ctx.mkDistinct(left_operand, right_operand); - } else if (nameEndsWith(name, N_EQUALS3)) { - constraint = ctx.mkGe(left_operand, right_operand); // ??? - } else if (nameEndsWith(name, N_NOTEQUALS3)) { - constraint = ctx.mkGe(left_operand, right_operand); // ??? - } else { - throw new Exception ("Unsupported binary operation " + name); - } - - return constraint; - } - - // TODO: add variable: state of the solver - private ArithExpr formNumericConstraintHelper(XExpression e, Map aMatch) throws Exception { - ArithExpr expr = null; - // Variables - if (e instanceof XFeatureCall) { - PrimitiveElement matchedObj = aMatch.get(((XFeatureCall) e).getFeature()); - if (!matchedObj.isValueSet()) { - if (varMap.get(matchedObj) == null) { - String var_name = ((XFeatureCall) e).getFeature().getQualifiedName() + matchedObj.toString(); - expr = (ArithExpr) ctx.mkConst(ctx.mkSymbol(var_name), ctx.getIntSort()); - varMap.put(matchedObj, expr); - } else { - expr = (ArithExpr) varMap.get(matchedObj); - } - } else { - int value = ((IntegerElement) matchedObj).getValue(); - expr = (ArithExpr) ctx.mkInt(value); - varMap.put(matchedObj, expr); - } - } - // Constants - else if (e instanceof XNumberLiteral) { - String value = ((XNumberLiteral) e).getValue(); - try{ int val = Integer.parseInt(value); expr = (ArithExpr) ctx.mkInt(val);} catch(NumberFormatException err){} - } - // Expressions with operators - else if (e instanceof XBinaryOperation) { - String name = ((XBinaryOperation) e).getFeature().getQualifiedName(); - ArithExpr left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch); - ArithExpr right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch); - - if (nameEndsWith(name, N_PLUS)) { - expr = ctx.mkAdd(left_operand, right_operand); - } else if (nameEndsWith(name, N_MINUS)) { - expr = ctx.mkAdd(left_operand, ctx.mkUnaryMinus(right_operand)); - } else if (nameEndsWith(name, N_POWER)) { - expr = ctx.mkPower(left_operand, right_operand); - } else if (nameEndsWith(name, N_MULTIPLY)) { - expr = ctx.mkMul(left_operand, right_operand); - } else if (nameEndsWith(name, N_DIVIDE)) { - expr = ctx.mkDiv(left_operand, right_operand); - } else if (nameEndsWith(name, N_MODULO)) { - expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand); - } else { - throw new Exception ("Unsupported binary operation " + name); - } - } else { - throw new Exception ("Unsupported expression " + e.getClass().getSimpleName()); - } - return expr; - - } - - private boolean nameEndsWith(String name, String end) { - return name.startsWith(N_Base) && name.endsWith(end); - } - - private BoolExpr formNumericProblemInstance(Map>> matches) throws Exception { - BoolExpr constraintInstances = ctx.mkTrue(); - for (XExpression e: matches.keySet()) { - Set> matchSets = matches.get(e); - for (Map aMatch: matchSets) { - BoolExpr constraintInstance = formNumericConstraint(e, aMatch); - constraintInstances = ctx.mkAnd(constraintInstances, constraintInstance); - } - } - return constraintInstances; - } + */ } diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend new file mode 100644 index 00000000..89719b91 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend @@ -0,0 +1,64 @@ +package hu.bme.mit.inf.dslreasoner.viatra2logic + +import org.eclipse.xtext.xbase.XExpression +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation +import org.eclipse.xtext.common.types.JvmIdentifiableElement +import java.util.Set +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement +import java.util.Map +import com.microsoft.z3.BoolExpr +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +import java.util.Map.Entry +import org.eclipse.xtext.xbase.XFeatureCall +import java.util.Comparator +import java.util.ArrayList +import java.util.HashMap +import java.util.List + +class NumericTranslator { + + private XExpressionExtractor extractor = new XExpressionExtractor(); + + val comparator = new Comparator(){ + override compare(JvmIdentifiableElement o1, JvmIdentifiableElement o2) { + //println('''«o1.simpleName» - «o2.simpleName»''') + o1.simpleName.compareTo(o2.simpleName) + } + } + def Map arrayToMap(Object[] tuple, ArrayList variablesInOrder) { + val res = new HashMap + for(var i=0; i> matches) throws Exception { + val res = new HashMap + for (Entry> entry: matches.entrySet()) { + val ExpressionEvaluation constraint = entry.getKey() as ExpressionEvaluation; + val XExpression expression = extractor.extractExpression(constraint.getEvaluator()); + val Iterable tuples = entry.getValue(); + val features = expression.eAllContents.filter(XFeatureCall).map[it.feature].toSet + val variablesInOrder = new ArrayList(features) + variablesInOrder.toList.sort(comparator) + //println(variablesInOrder) + val map = tuples.map[it.arrayToMap(variablesInOrder)] + res.put(expression,map) + } + return res + } + + def delegateIsSatisfiable(Map> matches) { + val input = formNumericProblemInstance(matches) + val solver = new NumericProblemSolver + val satisfiability = solver.isSatisfiable(input) + return satisfiability + } + + def delegateGetSolution(List primitiveElements, Map> matches) { + val input = formNumericProblemInstance(matches) + val solver = new NumericProblemSolver + val solution = solver.getOneSolution(primitiveElements,input) + return solution + } +} \ 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/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index e7342ff7..975ace2f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend @@ -17,6 +17,8 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule import org.eclipse.xtend.lib.annotations.Data +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +import java.util.Map class ModelGenerationStatistics { public var long transformationExecutionTime = 0 @@ -36,6 +38,8 @@ class ModelGenerationStatistics { Collection>> invalidWF + Map>> unitPropagationPreconditions + Collection>> allPatterns } enum TypeInferenceMethod { @@ -77,6 +81,8 @@ class ModelGenerationMethodProvider { val invalidWF = queries.getInvalidWFQueries.values + val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns + return new ModelGenerationMethod( statistics, objectRefinementRules.values, @@ -84,6 +90,7 @@ class ModelGenerationMethodProvider { unfinishedMultiplicities, unfinishedWF, invalidWF, + unitPropagationPreconditions, queries.allQueries ) } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index f576d1a1..18e3018a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend @@ -93,7 +93,6 @@ class PatternProvider { refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] val Map>> unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)] - unitPropagationPreconditionPatterns.entrySet.forEach[println(it.key + "->" +it.value)] return new GeneratedPatterns( invalidWFQueries, unfinishedWFQueries, diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend index 6c68ec94..d487db64 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend @@ -100,11 +100,9 @@ class UnitPropagationPreconditionGenerator { val preconditions = new LinkedList val constraint2Precondition = new HashMap for(entry : mainPropagationNames.entrySet) { - val name = '''UPMUSTPropagate«res.getOrGenerateConstraintName(entry.key)»'''; + val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; val def = ''' - pattern «name»( - problem:LogicProblem, interpretation:PartialInterpretation, - «FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») + pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») «FOR propagation : entry.value SEPARATOR " or "» { find «propagation.key»(problem,interpretation,«FOR index : 0..> matchers; + //private Collection> matchers; // Statistics private int numberOfStatecoderFail = 0; private int numberOfPrintedModel = 0; private int numberOfSolverCalls = 0; + + private NumericSolver numericSolver = null; public BestFirstStrategyForModelGeneration( ReasonerWorkspace workspace, @@ -112,14 +117,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { this.context = context; this.solutionStore = context.getGlobalContext().getSolutionStore(); - ViatraQueryEngine engine = context.getQueryEngine(); +// ViatraQueryEngine engine = context.getQueryEngine(); // // TODO: visualisation - matchers = new LinkedList>(); - for(IQuerySpecification> p : this.method.getAllPatterns()) { - //System.out.println(p.getSimpleName()); - ViatraQueryMatcher matcher = p.getMatcher(engine); - matchers.add(matcher); - } +// matchers = new LinkedList>(); +// for(IQuerySpecification> p : this.method.getAllPatterns()) { +// //System.out.println(p.getSimpleName()); +// ViatraQueryMatcher matcher = p.getMatcher(engine); +// matchers.add(matcher); +// } this.solutionStoreWithCopy = new SolutionStoreWithCopy(); this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement); @@ -131,6 +136,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { return objectiveComparatorHelper.compare(o2.fitness, o1.fitness); } }; + + this.numericSolver = new NumericSolver(context, method); trajectoiresToExplore = new PriorityQueue(11, comparator); } @@ -140,6 +147,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { if (!context.checkGlobalConstraints()) { logger.info("Global contraint is not satisifed in the first state. Terminate."); return; + } else if(!numericSolver.isSatisfiable()) { + logger.info("Numeric contraints are not satisifed in the first state. Terminate."); + return; } if (configuration.searchSpaceConstraints.maxDepth == 0) { logger.info("Maximal depth is reached in the initial solution. Terminate."); @@ -218,6 +228,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { } else if (!context.checkGlobalConstraints()) { logger.debug("Global contraint is not satisifed."); context.backtrack(); + } else if (!numericSolver.isSatisfiable()) { + logger.debug("Numeric constraints are not satisifed."); + context.backtrack(); } else { final Fitness nextFitness = context.calculateFitness(); checkForSolution(nextFitness); @@ -272,7 +285,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { private void checkForSolution(final Fitness fittness) { if (fittness.isSatisifiesHardObjectives()) { if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { - solutionStoreWithCopy.newSolution(context); + Map trace = solutionStoreWithCopy.newSolution(context); + numericSolver.fillSolutionCopy(trace); solutionStoreWithDiversityDescriptor.newSolution(context); solutionStore.newSolution(context); configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend new file mode 100644 index 00000000..b72bdb44 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend @@ -0,0 +1,114 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod +import java.util.HashMap +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.emf.ecore.EObject +import java.util.Map +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement +import java.util.List +import java.math.BigDecimal + +class NumericSolver { + val ThreadContext threadContext; + val constraint2UnitPropagationPrecondition = new HashMap> + NumericTranslator t = new NumericTranslator + + new(ThreadContext threadContext, ModelGenerationMethod method) { + this.threadContext = threadContext + val engine = threadContext.queryEngine + for(entry : method.unitPropagationPreconditions.entrySet) { + val constraint = entry.key + val querySpec = entry.value + val matcher = querySpec.getMatcher(engine); + constraint2UnitPropagationPrecondition.put(constraint,matcher) + } + } + + def boolean isSatisfiable() { + if(constraint2UnitPropagationPrecondition.empty) return true + else { + val propagatedConstraints = new HashMap + for(entry : constraint2UnitPropagationPrecondition.entrySet) { + val constraint = entry.key + //println(constraint) + val allMatches = entry.value.allMatches.map[it.toArray] + //println(allMatches.toList) + propagatedConstraints.put(constraint,allMatches) + } + + if(propagatedConstraints.values.forall[empty]) { + return true + } else { + val res = t.delegateIsSatisfiable(propagatedConstraints) + //println(res) + return res + } + } + } + + def fillSolutionCopy(Map trace) { + val model = threadContext.getModel as PartialInterpretation + val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList + if(constraint2UnitPropagationPrecondition.empty) { + fillWithDefaultValues(dataObjects,trace) + } else { + val propagatedConstraints = new HashMap + for(entry : constraint2UnitPropagationPrecondition.entrySet) { + val constraint = entry.key + val allMatches = entry.value.allMatches.map[it.toArray] + propagatedConstraints.put(constraint,allMatches) + } + + if(propagatedConstraints.values.forall[empty]) { + fillWithDefaultValues(dataObjects,trace) + } else { + val solution = t.delegateGetSolution(dataObjects,propagatedConstraints) + fillWithSolutions(dataObjects,solution,trace) + } + } + } + + def protected fillWithDefaultValues(List elements, Map trace) { + for(element : elements) { + if(element.valueSet==false) { + val value = getDefaultValue(element) + val target = trace.get(element) as PrimitiveElement + target.fillWithValue(value) + } + } + } + + def protected dispatch getDefaultValue(BooleanElement e) {false} + def protected dispatch getDefaultValue(IntegerElement e) {0} + def protected dispatch getDefaultValue(RealElement e) {0.0} + def protected dispatch getDefaultValue(StringElement e) {""} + + def protected fillWithSolutions(List elements, Map solution, Map trace) { + for(element : elements) { + if(element.valueSet==false) { + if(solution.containsKey(element)) { + val value = solution.get(element) + val target = trace.get(element) as PrimitiveElement + target.fillWithValue(value) + } + } + } + } + + def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean} + def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} + def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=BigDecimal.valueOf(value as Double) } + def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend index a8b7301e..21867a4e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend @@ -25,7 +25,7 @@ class SolutionStoreWithCopy { newSolution(context) }*/ - def newSolution(ThreadContext context) { + def Map newSolution(ThreadContext context) { //print(System.nanoTime-initTime + ";") val copyStart = System.nanoTime val solution = context.model as PartialInterpretation @@ -36,6 +36,7 @@ class SolutionStoreWithCopy { copyTraces.add(copier) runtime += System.nanoTime - copyStart solutionTimes.add(System.nanoTime-sartTime) + return copier } def getSumRuntime() { return runtime -- cgit v1.2.3-70-g09d2