From 919afc0d81a8434c2c9c54b50576e3eb8120cc65 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Fri, 8 May 2020 03:01:30 +0200 Subject: Visualization fix for attributes with same value --- .../PartialInterpretation2Graphviz.xtend | 49 +++++++++++++++------- 1 file changed, 33 insertions(+), 16 deletions(-) (limited to 'Solvers') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/PartialInterpretation2Graphviz.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/PartialInterpretation2Graphviz.xtend index 05a4e6c2..cd0b3e00 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/PartialInterpretation2Graphviz.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/PartialInterpretation2Graphviz.xtend @@ -30,6 +30,7 @@ import org.eclipse.xtext.xbase.lib.Functions.Function1 import static guru.nidi.graphviz.model.Factory.* import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement class GraphvizVisualiser implements PartialInterpretationVisualiser { @@ -106,10 +107,10 @@ class GraphvizVisualiser implements PartialInterpretationVisualiser { // elements2Node.put(newElement,image) // } - partialInterpretation.newElements.filter(BooleanElement).drawDataTypes([it.value.toString],elements2Node,elements2ID) - partialInterpretation.newElements.filter(IntegerElement).drawDataTypes([it.value.toString],elements2Node,elements2ID) - partialInterpretation.newElements.filter(StringElement).drawDataTypes(['''"«it.value.toString»"'''],elements2Node,elements2ID) - partialInterpretation.newElements.filter(RealElement).drawDataTypes([it.value.toString],elements2Node,elements2ID) + //partialInterpretation.newElements.filter(BooleanElement).drawDataTypes([it.value.toString],elements2Node,elements2ID) + //partialInterpretation.newElements.filter(IntegerElement).drawDataTypes([it.value.toString],elements2Node,elements2ID) + //partialInterpretation.newElements.filter(StringElement).drawDataTypes(['''"«it.value.toString»"'''],elements2Node,elements2ID) + //partialInterpretation.newElements.filter(RealElement).drawDataTypes([it.value.toString],elements2Node,elements2ID) // Drawing the edges val edges = new HashMap @@ -135,35 +136,51 @@ class GraphvizVisualiser implements PartialInterpretationVisualiser { return new GraphvizVisualisation(graph) } - def protected void drawDataTypes(Iterable collection, Function1 namer, HashMap elements2Node, HashMap elements2ID) { - for(booleanElementIndex: 0.. void drawDataTypes(Iterable collection, Function1 namer, HashMap elements2Node, HashMap elements2ID) { +// for(booleanElementIndex: 0.. mustTypes, Set mayTypes) { var tableStyle = ''' CELLSPACING="0" BORDER="2" CELLBORDER="0" CELLPADDING="1" STYLE="ROUNDED"''' if(typeColoringStyle==TypeColoringStyle::AVERAGE) { tableStyle += ''' BGCOLOR="#«typePredicateColor(mustTypes).toBackgroundColorString»"''' } - val mainLabel = if(element.name !== null) { + val mainLabel = if(element instanceof PrimitiveElement) { + if(element.isValueSet) { + if(element instanceof BooleanElement) { element.value.toString } + else if(element instanceof IntegerElement) { element.value.toString } + else if(element instanceof RealElement) { element.value.toString } + else if(element instanceof StringElement) { "\""+element.value.toString+"\"" } + } else { + "?" + } + }else if(element.name !== null) { val parts = element.name.split("\\s+") textWithSubSup(parts.getOrNull(0),parts.getOrNull(1),parts.getOrNull(2),null) } else { val parts = ID.split("\\s+") textWithSubSup(parts.getOrNull(0),parts.getOrNull(1),parts.getOrNull(2),null) } - val label = Label.html( + val hasNoCompexType = (mustTypes.empty) && (mayTypes.empty) + + val label = if(hasNoCompexType) { + Label.html( + ''''''+ + ''' «mainLabel» '''+ + '''''') + } else { + Label.html( ''''''+ '''«mainLabel»'''+ '''«FOR mustTypeName : mustTypes.map[it.name].sort»«typePredicateDescription(mustTypeName,true)»«ENDFOR»'''+ '''«FOR mayTypeName : mayTypes.map[it.name].sort»«typePredicateDescription(mayTypeName,false)»«ENDFOR»'''+ '''''') - + } val node = node(ID).with(label).with( Shape.NONE //, -- cgit v1.2.3-70-g09d2 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') 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') 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') 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') 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') 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 From 4ccaba7ad5a23a060bca0fdf6660302f2bd9153c Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Sat, 9 May 2020 21:36:05 +0200 Subject: uninvolved objects are filled with a default value --- .../mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | 3 +++ 1 file changed, 3 insertions(+) (limited to 'Solvers') 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 index b72bdb44..e1745854 100644 --- 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 @@ -102,6 +102,9 @@ class NumericSolver { val value = solution.get(element) val target = trace.get(element) as PrimitiveElement target.fillWithValue(value) + } else { + val target = trace.get(element) as PrimitiveElement + target.fillWithValue(target.defaultValue) } } } -- cgit v1.2.3-70-g09d2 From 66cc2cc3b2f24d403167fd4e35cd69011d334b00 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Sun, 10 May 2020 18:38:20 +0200 Subject: measurement time statistics + activation selection strategies --- .../viatrasolver/reasoner/ViatraReasoner.xtend | 15 ++++++ .../reasoner/dse/ActivationSelector.xtend | 24 +++++++++ .../reasoner/dse/BalancedActivationSelector.xtend | 51 ++++++++++++++++++ .../dse/BestFirstStrategyForModelGeneration.java | 9 ++-- .../reasoner/dse/EvenActivationSelector.xtend | 20 +++++++ .../dse/ModelGenerationCompositeObjective.xtend | 12 +++-- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 63 +++++++++++++++++++--- 7 files changed, 176 insertions(+), 18 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend (limited to 'Solvers') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index cb73f4e8..bafe78f6 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend @@ -155,6 +155,21 @@ class ViatraReasoner extends LogicReasoner{ it.entries += createIntStatisticEntry => [ it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int ] + it.entries += createIntStatisticEntry => [ + it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int + ] + it.entries += createIntStatisticEntry => [ + it.name = "NumericalSolverTime" it.value = (strategy.numericSolver.runtime/1000000) as int + ] + it.entries += createIntStatisticEntry => [ + it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int + ] + it.entries += createIntStatisticEntry => [ + it.name = "NumericalSolverCallNumber" it.value = strategy.numericSolver.numberOfSolverCalls + ] + it.entries += createIntStatisticEntry => [ + it.name = "NumericalSolverCachedAnswerNumber" it.value = strategy.numericSolver.numberOfCachedSolverCalls + ] if(strategy.solutionStoreWithDiversityDescriptor.isActive) { it.entries += createIntStatisticEntry => [ it.name = "SolutionDiversityCheckTime" it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime/1000000) as int diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend new file mode 100644 index 00000000..65f9814c --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend @@ -0,0 +1,24 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import java.util.ArrayList +import java.util.Collection +import java.util.Random + +abstract class ActivationSelector { + long runtime = 0 + protected val Random r + new(Random r) { + this.r = r + } + + def randomizeActivationIDs(Collection activationIDs) { + val startTime = System.nanoTime + val res = internalRandomizationOfActivationIDs(activationIDs) + runtime+= System.nanoTime-startTime + return res + } + def protected ArrayList internalRandomizationOfActivationIDs(Collection activationIDs); + def getRuntime(){ + return runtime + } +} \ 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/BalancedActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend new file mode 100644 index 00000000..2df9957b --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend @@ -0,0 +1,51 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import java.util.Collection +import java.util.HashMap +import java.util.Map +import java.util.List +import java.util.Random +import java.util.ArrayList +import java.util.LinkedList +import java.util.Collections + +class BalancedActivationSelector extends ActivationSelector{ + val Random r = new Random + + new(Random r) { + super(r) + } + + override protected internalRandomizationOfActivationIDs(Collection activationIDs) { + val Map> urns = new HashMap + val res = new ArrayList(activationIDs.size) + for(activationID : activationIDs) { + val pair = activationID as Pair + val name = pair.key + val selectedUrn = urns.get(name) + if(selectedUrn!==null) { + selectedUrn.add(activationID) + } else { + val collection = new LinkedList + collection.add(activationID) + urns.put(name,collection) + } + } + + for(list:urns.values) { + Collections.shuffle(list,r) + } + + while(!urns.empty) { + val randomEntry = urns.entrySet.get(r.nextInt(urns.size)) + val list = randomEntry.value + val removedLast = list.remove(list.size-1) + res.add(removedLast) + if(list.empty) { + urns.remove(randomEntry.key) + } + } + return res + } + +} \ 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/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index 1cd61e9a..18fe94e4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java @@ -84,13 +84,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { private ModelResult modelResultByInternalSolver = null; private Random random = new Random(); //private Collection> matchers; - + public ActivationSelector activationSelector = new EvenActivationSelector(random); + public NumericSolver numericSolver = null; // Statistics private int numberOfStatecoderFail = 0; private int numberOfPrintedModel = 0; private int numberOfSolverCalls = 0; - private NumericSolver numericSolver = null; public BestFirstStrategyForModelGeneration( ReasonerWorkspace workspace, @@ -137,7 +137,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { } }; - this.numericSolver = new NumericSolver(context, method); + this.numericSolver = new NumericSolver(context, method, false); trajectoiresToExplore = new PriorityQueue(11, comparator); } @@ -273,8 +273,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { private List selectActivation() { List activationIds; try { - activationIds = new ArrayList(context.getUntraversedActivationIds()); - Collections.shuffle(activationIds); + activationIds = this.activationSelector.randomizeActivationIDs(context.getUntraversedActivationIds()); } catch (NullPointerException e) { numberOfStatecoderFail++; activationIds = Collections.emptyList(); diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend new file mode 100644 index 00000000..82a5f32d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend @@ -0,0 +1,20 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import java.util.Random +import java.util.Collection +import java.util.Collections +import java.util.ArrayList + +class EvenActivationSelector extends ActivationSelector { + + new(Random r) { + super(r) + } + + override protected internalRandomizationOfActivationIDs(Collection activationIDs) { + val toShuffle = new ArrayList(activationIDs); + Collections.shuffle(toShuffle); + return toShuffle + } + +} \ 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/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend index 2489c751..a75ddf76 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend @@ -50,20 +50,22 @@ class ModelGenerationCompositeObjective implements IObjective{ override getComparator() { Comparators.LOWER_IS_BETTER } override getFitness(ThreadContext context) { - var sum = 0.0 + val scopeFitnes = scopeObjective.getFitness(context) //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) - sum+=scopeFitnes + var multiplicity = 0.0 for(multiplicityObjective : unfinishedMultiplicityObjectives) { - multiplicity+=multiplicityObjective.getFitness(context)//*0.5 + multiplicity+=multiplicityObjective.getFitness(context) } - sum+=multiplicity + var sum = 0.0 + sum += scopeFitnes + sum +=Math.sqrt(multiplicity *0.1) sum += unfinishedWFsFitness//*0.5 - //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') + println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') return sum } 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 index e1745854..71793aa6 100644 --- 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 @@ -19,13 +19,23 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement import java.util.List import java.math.BigDecimal +import java.util.LinkedHashSet +import java.util.LinkedHashMap class NumericSolver { val ThreadContext threadContext; val constraint2UnitPropagationPrecondition = new HashMap> NumericTranslator t = new NumericTranslator - new(ThreadContext threadContext, ModelGenerationMethod method) { + val boolean caching; + Map>>,Boolean> satisfiabilityCache = new HashMap + + var long runtime = 0 + var long cachingTime = 0 + var int numberOfSolverCalls = 0 + var int numberOfCachedSolverCalls = 0 + + new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { this.threadContext = threadContext val engine = threadContext.queryEngine for(entry : method.unitPropagationPreconditions.entrySet) { @@ -34,11 +44,20 @@ class NumericSolver { val matcher = querySpec.getMatcher(engine); constraint2UnitPropagationPrecondition.put(constraint,matcher) } + this.caching = caching } + def getRuntime(){runtime} + def getCachingTime(){cachingTime} + def getNumberOfSolverCalls(){numberOfSolverCalls} + def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} + def boolean isSatisfiable() { - if(constraint2UnitPropagationPrecondition.empty) return true - else { + val start = System.nanoTime + var boolean finalResult + if(constraint2UnitPropagationPrecondition.empty){ + finalResult=true + } else { val propagatedConstraints = new HashMap for(entry : constraint2UnitPropagationPrecondition.entrySet) { val constraint = entry.key @@ -47,15 +66,43 @@ class NumericSolver { //println(allMatches.toList) propagatedConstraints.put(constraint,allMatches) } - if(propagatedConstraints.values.forall[empty]) { - return true + finalResult=true } else { - val res = t.delegateIsSatisfiable(propagatedConstraints) - //println(res) - return res + if(caching) { + val code = getCode(propagatedConstraints) + val cachedResult = satisfiabilityCache.get(code) + if(cachedResult === null) { + // println('''new problem, call solver''') + // for(entry : code.entrySet) { + // println('''«entry.key» -> «entry.value»''') + // } + //println(code.hashCode) + this.numberOfSolverCalls++ + val res = t.delegateIsSatisfiable(propagatedConstraints) + satisfiabilityCache.put(code,res) + finalResult=res + } else { + //println('''similar problem, answer from cache''') + finalResult=cachedResult + this.numberOfCachedSolverCalls++ + } + } else { + finalResult= t.delegateIsSatisfiable(propagatedConstraints) + this.numberOfSolverCalls++ + } } } + this.runtime+=System.nanoTime-start + return finalResult + } + + def getCode(HashMap> propagatedConstraints) { + val start = System.nanoTime + val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList + val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]]) + this.cachingTime += System.nanoTime-start + return res } def fillSolutionCopy(Map trace) { -- cgit v1.2.3-70-g09d2