aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-05-10 22:13:21 +0200
committerLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-05-10 22:13:21 +0200
commit5a6eea9bd15597eab77bbcedb4b5116020f0a67d (patch)
tree6c86f7e5bd3d86fde29d3fee4fb4f912f35057bc /Solvers
parentAdd satellite case study (diff)
parentMerge branch 'master' of https://github.com/viatra/VIATRA-Generator (diff)
downloadVIATRA-Generator-5a6eea9bd15597eab77bbcedb4b5116020f0a67d.tar.gz
VIATRA-Generator-5a6eea9bd15597eab77bbcedb4b5116020f0a67d.tar.zst
VIATRA-Generator-5a6eea9bd15597eab77bbcedb4b5116020f0a67d.zip
Merge branch 'master' of github.com:viatra/VIATRA-Generator
Diffstat (limited to 'Solvers')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend7
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend8
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend15
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend142
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend65
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend17
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend24
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend51
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java37
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend20
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend12
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend164
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend3
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/PartialInterpretation2Graphviz.xtend49
14 files changed, 489 insertions, 125 deletions
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
17import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 17import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
18import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule 18import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
19import org.eclipse.xtend.lib.annotations.Data 19import org.eclipse.xtend.lib.annotations.Data
20import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
21import java.util.Map
20 22
21class ModelGenerationStatistics { 23class ModelGenerationStatistics {
22 public var long transformationExecutionTime = 0 24 public var long transformationExecutionTime = 0
@@ -36,6 +38,8 @@ class ModelGenerationStatistics {
36 38
37 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF 39 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF
38 40
41 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditions
42
39 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns 43 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns
40} 44}
41enum TypeInferenceMethod { 45enum TypeInferenceMethod {
@@ -77,6 +81,8 @@ class ModelGenerationMethodProvider {
77 81
78 val invalidWF = queries.getInvalidWFQueries.values 82 val invalidWF = queries.getInvalidWFQueries.values
79 83
84 val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns
85
80 return new ModelGenerationMethod( 86 return new ModelGenerationMethod(
81 statistics, 87 statistics,
82 objectRefinementRules.values, 88 objectRefinementRules.values,
@@ -84,6 +90,7 @@ class ModelGenerationMethodProvider {
84 unfinishedMultiplicities, 90 unfinishedMultiplicities,
85 unfinishedWF, 91 unfinishedWF,
86 invalidWF, 92 invalidWF,
93 unitPropagationPreconditions,
87 queries.allQueries 94 queries.allQueries
88 ) 95 )
89 } 96 }
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 {
155 Map<String,PQuery> fqn2PQuery, 155 Map<String,PQuery> fqn2PQuery,
156 TypeAnalysisResult typeAnalysisResult 156 TypeAnalysisResult typeAnalysisResult
157 ) { 157 ) {
158 158 val first =
159 return ''' 159 '''
160 import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" 160 import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage"
161 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" 161 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"
162 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" 162 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"
@@ -395,7 +395,9 @@ class PatternGenerator {
395 ////////// 395 //////////
396 // 5 Unit Propagations 396 // 5 Unit Propagations
397 ////////// 397 //////////
398 «unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)»
399 ''' 398 '''
399 val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)
400 val second = up.definitions
401 return (first+second) -> up.constraint2PreconditionName
400 } 402 }
401} 403}
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..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
@@ -21,6 +21,8 @@ import org.eclipse.xtend.lib.annotations.Data
21import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 21import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
22import java.util.Collection 22import java.util.Collection
23import java.util.Set 23import java.util.Set
24import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
25import java.util.HashMap
24 26
25@Data class GeneratedPatterns { 27@Data class GeneratedPatterns {
26 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries 28 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries
@@ -29,6 +31,7 @@ import java.util.Set
29 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries 31 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries
30 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries 32 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries
31 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries 33 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries
34 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditionPatterns
32 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries 35 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries
33} 36}
34 37
@@ -56,13 +59,15 @@ class PatternProvider {
56 } else { 59 } else {
57 null 60 null
58 } 61 }
59 val baseIndexerFile = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) 62 val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult)
63 val baseIndexerFile = patternGeneratorResult.key
64 val unitPropagationTrace = patternGeneratorResult.value
60 if(writeToFile) { 65 if(writeToFile) {
61 workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) 66 workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile)
62 } 67 }
63 val ParseUtil parseUtil = new ParseUtil 68 val ParseUtil parseUtil = new ParseUtil
64 val generatedQueries = parseUtil.parse(baseIndexerFile) 69 val generatedQueries = parseUtil.parse(baseIndexerFile)
65 val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,generatedQueries); 70 val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,unitPropagationTrace,generatedQueries);
66 return runtimeQueries 71 return runtimeQueries
67 } 72 }
68 73
@@ -71,7 +76,8 @@ class PatternProvider {
71 LogicProblem problem, 76 LogicProblem problem,
72 PartialInterpretation emptySolution, 77 PartialInterpretation emptySolution,
73 TypeAnalysisResult typeAnalysisResult, 78 TypeAnalysisResult typeAnalysisResult,
74 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries 79 HashMap<PConstraint, String> unitPropagationTrace,
80 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries
75 ) { 81 ) {
76 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 82 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
77 invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] 83 invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)]
@@ -85,6 +91,8 @@ class PatternProvider {
85 refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] 91 refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]
86 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 92 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
87 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] 93 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]
94 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
95 unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)]
88 return new GeneratedPatterns( 96 return new GeneratedPatterns(
89 invalidWFQueries, 97 invalidWFQueries,
90 unfinishedWFQueries, 98 unfinishedWFQueries,
@@ -92,6 +100,7 @@ class PatternProvider {
92 refineObjectsQueries, 100 refineObjectsQueries,
93 refineTypeQueries, 101 refineTypeQueries,
94 refineRelationQueries, 102 refineRelationQueries,
103 unitPropagationPreconditionPatterns,
95 queries.values 104 queries.values
96 ) 105 )
97 } 106 }
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..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
@@ -22,6 +22,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativeP
22import java.util.Comparator 22import java.util.Comparator
23import java.util.ArrayList 23import java.util.ArrayList
24import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction 24import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
25import java.util.LinkedHashSet
25 26
26@Data class UnitPropagation { 27@Data class UnitPropagation {
27 val PQuery q 28 val PQuery q
@@ -57,6 +58,11 @@ class UnitPropagationPreconditionGenerationResult {
57 return unitPropagation2PatternName.get(key) !== null 58 return unitPropagation2PatternName.get(key) !== null
58 } 59 }
59} 60}
61@Data
62class UnitPropagationPreconditionFinalResult {
63 CharSequence definitions
64 HashMap<PConstraint,String> constraint2PreconditionName
65}
60 66
61class UnitPropagationPreconditionGenerator { 67class UnitPropagationPreconditionGenerator {
62 val PatternGenerator base 68 val PatternGenerator base
@@ -75,30 +81,59 @@ class UnitPropagationPreconditionGenerator {
75 // Create an empty result 81 // Create an empty result
76 val res = new UnitPropagationPreconditionGenerationResult 82 val res = new UnitPropagationPreconditionGenerationResult
77 val wfs = base.wfQueries(problem)//.map[it.patternPQuery] 83 val wfs = base.wfQueries(problem)//.map[it.patternPQuery]
78 val mainPropagationNames = new LinkedList 84 val Map<PConstraint,List<Pair<String,Integer>>> mainPropagationNames = new HashMap
79 for(wf : wfs) { 85 for(wf : wfs) {
80 val query = wf.patternPQuery as PQuery 86 val query = wf.patternPQuery as PQuery
81 val relation = wf.target 87 val relation = wf.target
82 val allReferredChecks = query.allReferredConstraints.filter(ExpressionEvaluation) 88 val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation)
83 89
84 for(referredCheck : allReferredChecks) { 90 for(referredCheck : allReferredChecks) {
85 mainPropagationNames+= getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) 91 val propagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST)
92 if(!mainPropagationNames.containsKey(referredCheck)) {
93 mainPropagationNames.put(referredCheck,new LinkedList)
94 }
95 if(propagationPrecondition !== null) {
96 mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size)
97 }
86 } 98 }
87 } 99 }
88 return ''' 100 val preconditions = new LinkedList
101 val constraint2Precondition = new HashMap
102 for(entry : mainPropagationNames.entrySet) {
103 val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
104 val def = '''
105 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
106 «FOR propagation : entry.value SEPARATOR " or "»
107 { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }
108 «ENDFOR»'''
109 preconditions+=def
110 constraint2Precondition.put(entry.key,name)
111 }
112
113 val definitions = '''
89 «FOR def : res.definitions» 114 «FOR def : res.definitions»
90 «def» 115 «def»
91 «ENDFOR» 116 «ENDFOR»
92 117
93 // Main propagations: 118 // Collected propagation preconditions:
94 «FOR name : mainPropagationNames» 119
95 «name» 120 «FOR predondition : preconditions»
121 «predondition»
96 «ENDFOR» 122 «ENDFOR»
97 ''' 123 '''
124 return new UnitPropagationPreconditionFinalResult(definitions,constraint2Precondition)
98 } 125 }
99 def allReferredConstraints(PQuery query) { 126 def allReferredConstraints(Relation relation, PQuery query) {
100 val allReferredQueries = query.allReferredQueries 127 val allReferredQueries = query.allReferredQueries
101 return (#[query]+allReferredQueries).map[it.disjunctBodies.bodies].flatten.map[constraints].flatten 128 val problem = relation.eContainer as LogicProblem
129 val constraints = new LinkedHashSet
130 for(referredQuery: #[query]+allReferredQueries) {
131 val referredRelation = problem.annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredQuery].head.target
132 val bodies = (referredRelation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
133 constraints.addAll(bodies.map[getConstraints].flatten)
134 }
135
136 return constraints
102 } 137 }
103 138
104 def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) { 139 def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
@@ -141,64 +176,67 @@ class UnitPropagationPreconditionGenerator {
141 // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied 176 // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied
142 } else { 177 } else {
143 val positives = body.constraints.filter(PositivePatternCall) 178 val positives = body.constraints.filter(PositivePatternCall)
144 val positiveRefers = positives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)] 179 for(positive: positives) {
145 for(positiveRefer: positiveRefers) { 180 val referredPQuery = positive.referredQuery
146 val referredPQuery = positiveRefer.referredQuery
147 val referredRelation = (relation.eContainer as LogicProblem) 181 val referredRelation = (relation.eContainer as LogicProblem)
148 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target 182 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
149 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3) 183 if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
150 if(referredName !== null) { 184 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3)
151 generatedBodies += ''' 185 if(referredName !== null) {
152 // Original Constraints 186 generatedBodies += '''
153 «FOR constraint : body.constraints.filter[it !== positiveRefer]» 187 // Original Constraints
154 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» 188 «FOR constraint : body.constraints.filter[it !== positive]»
155 «ENDFOR» 189 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
156 // Propagation for constraint referred indirectly from this pattern through «referredName» 190 «ENDFOR»
157 find «referredName»(problem, interpretation, 191 // Propagation for constraint referred indirectly from this pattern through «referredName»
158 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positiveRefer.getVariableInTuple(index).canonizeName»«ENDFOR», 192 find «referredName»(problem, interpretation,
159 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); 193 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR»,
160 ''' 194 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
195 '''
196 }
197 // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either
161 } 198 }
162 // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either
163 } 199 }
200
164 val negatives = body.constraints.filter(NegativePatternCall) 201 val negatives = body.constraints.filter(NegativePatternCall)
165 val negativeRefers = negatives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)] 202 for(negative : negatives) {
166 for(negativeRefer : negativeRefers) { 203 val referredPQuery = negative.referredQuery
167 val referredPQuery = negativeRefer.referredQuery
168 val referredRelation = (relation.eContainer as LogicProblem) 204 val referredRelation = (relation.eContainer as LogicProblem)
169 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target 205 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
170 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual) 206 if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
171 if(referredName !== null) { 207 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual)
172 generatedBodies += ''' 208 if(referredName !== null) {
173 // Original Constraints 209 generatedBodies += '''
174 «FOR constraint : body.constraints.filter[it !== negativeRefer]» 210 // Original Constraints
175 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» 211 «FOR constraint : body.constraints.filter[it !== negative]»
176 «ENDFOR» 212 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
177 // Propagation for constraint referred indirectly from this pattern through «referredName» 213 «ENDFOR»
178 find «referredName»(problem, interpretation, 214 // Propagation for constraint referred indirectly from this pattern through «referredName»
179 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negativeRefer.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR», 215 find «referredName»(problem, interpretation,
180 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); 216 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR»,
181 ''' 217 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
182 } else { 218 '''
183 generatedBodies += ''' 219 } else {
184 // Original Constraints 220 generatedBodies += '''
185 «FOR constraint : body.constraints.filter[it !== negativeRefer]» 221 // Original Constraints
186 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» 222 «FOR constraint : body.constraints.filter[it !== negative]»
187 «ENDFOR» 223 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
188 // Propagation for constraint referred indirectly from this pattern through «referredName», 224 «ENDFOR»
189 // which was unsatisfiable 225 // Propagation for constraint referred indirectly from this pattern through «referredName»,
190 ''' 226 // which was unsatisfiable
227 '''
228 }
191 } 229 }
192 } 230 }
193 } 231 }
194 } 232 }
195 233
196 // Register the result 234 // Register the result
197 if(generatedBodies.size>=0) { 235 if(generatedBodies.empty) {
198 res.registerUnsatQuery(q,c,pm,m3) 236 res.registerUnsatQuery(q,c,pm,m3)
199 } else { 237 } else {
200 val definition = ''' 238 val definition = '''
201 pattern «name»( 239 private pattern «name»(
202 problem:LogicProblem, interpretation:PartialInterpretation, 240 problem:LogicProblem, interpretation:PartialInterpretation,
203 «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR», 241 «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR»,
204 «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR») 242 «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR»)
@@ -229,7 +267,7 @@ class UnitPropagationPreconditionGenerator {
229 } 267 }
230 val variablesInOrder = new ArrayList(c.affectedVariables) 268 val variablesInOrder = new ArrayList(c.affectedVariables)
231 variablesInOrder.toList.sort(comparator) 269 variablesInOrder.toList.sort(comparator)
232 return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).name»==«canonizeName(variableIndex,m)»;«ENDFOR»''' 270 return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).canonizeName»==«canonizeName(variableIndex,m)»;«ENDFOR»'''
233 } 271 }
234 def dispatch propagateVariables(PConstraint c, PropagationModality m) { 272 def dispatch propagateVariables(PConstraint c, PropagationModality m) {
235 throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''') 273 throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
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..db0e17b9 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
@@ -90,7 +90,7 @@ class RefinementRuleProvider {
90 if(containmentRelation !== null) { 90 if(containmentRelation !== null) {
91 if(inverseRelation!== null) { 91 if(inverseRelation!== null) {
92 ruleBuilder.action[match | 92 ruleBuilder.action[match |
93 println(name) 93 //println(name)
94 val startTime = System.nanoTime 94 val startTime = System.nanoTime
95 //val problem = match.get(0) as LogicProblem 95 //val problem = match.get(0) as LogicProblem
96 val interpretation = match.get(1) as PartialInterpretation 96 val interpretation = match.get(1) as PartialInterpretation
@@ -115,7 +115,7 @@ class RefinementRuleProvider {
115 ] 115 ]
116 } else { 116 } else {
117 ruleBuilder.action[match | 117 ruleBuilder.action[match |
118 println(name) 118 //println(name)
119 val startTime = System.nanoTime 119 val startTime = System.nanoTime
120 //val problem = match.get(0) as LogicProblem 120 //val problem = match.get(0) as LogicProblem
121 val interpretation = match.get(1) as PartialInterpretation 121 val interpretation = match.get(1) as PartialInterpretation
@@ -139,7 +139,7 @@ class RefinementRuleProvider {
139 } 139 }
140 } else { 140 } else {
141 ruleBuilder.action[match | 141 ruleBuilder.action[match |
142 println(name) 142 //println(name)
143 val startTime = System.nanoTime 143 val startTime = System.nanoTime
144 //val problem = match.get(0) as LogicProblem 144 //val problem = match.get(0) as LogicProblem
145 val interpretation = match.get(1) as PartialInterpretation 145 val interpretation = match.get(1) as PartialInterpretation
@@ -179,36 +179,37 @@ class RefinementRuleProvider {
179 179
180 if(containmentReferences.contains(relation)) { 180 if(containmentReferences.contains(relation)) {
181 val targetTypeInterpretation = getTypeInterpretation(i, relation, 1) 181 val targetTypeInterpretation = getTypeInterpretation(i, relation, 1)
182 182 if(!(targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.isIsAbstract) {
183 val inverseAnnotation = p.assertions.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation] 183 val inverseAnnotation = p.assertions.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation]
184 if(!inverseAnnotation.empty) { 184 if(!inverseAnnotation.empty) {
185 val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) { 185 val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) {
186 inverseAnnotation.head.inverseB 186 inverseAnnotation.head.inverseB
187 } else {
188 inverseAnnotation.head.inverseA
189 }
190 val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head
191 for(var times=0; times<number; times++) {
192 recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) +=
193 new ObjectCreationInterpretationData(
194 i,
195 targetTypeInterpretation,
196 relationInterpretation,
197 inverseRelationInterpretation,
198 targetTypeInterpretation.getTypeConstructor
199 )
200 }
201
187 } else { 202 } else {
188 inverseAnnotation.head.inverseA 203 for(var times=0; times<number; times++) {
189 } 204 recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) +=
190 val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head 205 new ObjectCreationInterpretationData(
191 for(var times=0; times<number; times++) { 206 i,
192 recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) += 207 targetTypeInterpretation,
193 new ObjectCreationInterpretationData( 208 relationInterpretation,
194 i, 209 null,
195 targetTypeInterpretation, 210 targetTypeInterpretation.getTypeConstructor
196 relationInterpretation, 211 )
197 inverseRelationInterpretation, 212 }
198 targetTypeInterpretation.getTypeConstructor
199 )
200 }
201
202 } else {
203 for(var times=0; times<number; times++) {
204 recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) +=
205 new ObjectCreationInterpretationData(
206 i,
207 targetTypeInterpretation,
208 relationInterpretation,
209 null,
210 targetTypeInterpretation.getTypeConstructor
211 )
212 } 213 }
213 } 214 }
214 } else if(relation.parameters.get(1) instanceof PrimitiveTypeReference) { 215 } else if(relation.parameters.get(1) instanceof PrimitiveTypeReference) {
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 1e623823..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
@@ -77,7 +77,7 @@ class ViatraReasoner extends LogicReasoner{
77 scopePropagator, 77 scopePropagator,
78 viatraConfig.documentationLevel 78 viatraConfig.documentationLevel
79 ) 79 )
80 println("parsed") 80 //println("parsed")
81 81
82 dse.addObjective(new ModelGenerationCompositeObjective( 82 dse.addObjective(new ModelGenerationCompositeObjective(
83 new ScopeObjective, 83 new ScopeObjective,
@@ -155,6 +155,21 @@ class ViatraReasoner extends LogicReasoner{
155 it.entries += createIntStatisticEntry => [ 155 it.entries += createIntStatisticEntry => [
156 it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int 156 it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int
157 ] 157 ]
158 it.entries += createIntStatisticEntry => [
159 it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int
160 ]
161 it.entries += createIntStatisticEntry => [
162 it.name = "NumericalSolverTime" it.value = (strategy.numericSolver.runtime/1000000) as int
163 ]
164 it.entries += createIntStatisticEntry => [
165 it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int
166 ]
167 it.entries += createIntStatisticEntry => [
168 it.name = "NumericalSolverCallNumber" it.value = strategy.numericSolver.numberOfSolverCalls
169 ]
170 it.entries += createIntStatisticEntry => [
171 it.name = "NumericalSolverCachedAnswerNumber" it.value = strategy.numericSolver.numberOfCachedSolverCalls
172 ]
158 if(strategy.solutionStoreWithDiversityDescriptor.isActive) { 173 if(strategy.solutionStoreWithDiversityDescriptor.isActive) {
159 it.entries += createIntStatisticEntry => [ 174 it.entries += createIntStatisticEntry => [
160 it.name = "SolutionDiversityCheckTime" it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime/1000000) as int 175 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.ArrayList
4import java.util.Collection
5import java.util.Random
6
7abstract class ActivationSelector {
8 long runtime = 0
9 protected val Random r
10 new(Random r) {
11 this.r = r
12 }
13
14 def randomizeActivationIDs(Collection<Object> activationIDs) {
15 val startTime = System.nanoTime
16 val res = internalRandomizationOfActivationIDs(activationIDs)
17 runtime+= System.nanoTime-startTime
18 return res
19 }
20 def protected ArrayList<Object> internalRandomizationOfActivationIDs(Collection<Object> activationIDs);
21 def getRuntime(){
22 return runtime
23 }
24} \ 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.Collection
4import java.util.HashMap
5import java.util.Map
6import java.util.List
7import java.util.Random
8import java.util.ArrayList
9import java.util.LinkedList
10import java.util.Collections
11
12class BalancedActivationSelector extends ActivationSelector{
13 val Random r = new Random
14
15 new(Random r) {
16 super(r)
17 }
18
19 override protected internalRandomizationOfActivationIDs(Collection<Object> activationIDs) {
20 val Map<String,List<Object>> urns = new HashMap
21 val res = new ArrayList(activationIDs.size)
22 for(activationID : activationIDs) {
23 val pair = activationID as Pair<String,? extends Object>
24 val name = pair.key
25 val selectedUrn = urns.get(name)
26 if(selectedUrn!==null) {
27 selectedUrn.add(activationID)
28 } else {
29 val collection = new LinkedList
30 collection.add(activationID)
31 urns.put(name,collection)
32 }
33 }
34
35 for(list:urns.values) {
36 Collections.shuffle(list,r)
37 }
38
39 while(!urns.empty) {
40 val randomEntry = urns.entrySet.get(r.nextInt(urns.size))
41 val list = randomEntry.value
42 val removedLast = list.remove(list.size-1)
43 res.add(removedLast)
44 if(list.empty) {
45 urns.remove(randomEntry.key)
46 }
47 }
48 return res
49 }
50
51} \ 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 60f46033..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
@@ -17,10 +17,12 @@ import java.util.Comparator;
17import java.util.Iterator; 17import java.util.Iterator;
18import java.util.LinkedList; 18import java.util.LinkedList;
19import java.util.List; 19import java.util.List;
20import java.util.Map;
20import java.util.PriorityQueue; 21import java.util.PriorityQueue;
21import java.util.Random; 22import java.util.Random;
22 23
23import org.apache.log4j.Logger; 24import org.apache.log4j.Logger;
25import org.eclipse.emf.ecore.EObject;
24import org.eclipse.emf.ecore.util.EcoreUtil; 26import org.eclipse.emf.ecore.util.EcoreUtil;
25import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; 27import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;
26import org.eclipse.viatra.dse.base.ThreadContext; 28import org.eclipse.viatra.dse.base.ThreadContext;
@@ -38,6 +40,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
38import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; 40import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult;
39import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; 41import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
40import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; 42import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
43import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver;
41import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; 44import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod;
42import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; 45import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;
43import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; 46import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
@@ -80,12 +83,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
80 private volatile boolean isInterrupted = false; 83 private volatile boolean isInterrupted = false;
81 private ModelResult modelResultByInternalSolver = null; 84 private ModelResult modelResultByInternalSolver = null;
82 private Random random = new Random(); 85 private Random random = new Random();
83 private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; 86 //private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;
84 87 public ActivationSelector activationSelector = new EvenActivationSelector(random);
88 public NumericSolver numericSolver = null;
85 // Statistics 89 // Statistics
86 private int numberOfStatecoderFail = 0; 90 private int numberOfStatecoderFail = 0;
87 private int numberOfPrintedModel = 0; 91 private int numberOfPrintedModel = 0;
88 private int numberOfSolverCalls = 0; 92 private int numberOfSolverCalls = 0;
93
89 94
90 public BestFirstStrategyForModelGeneration( 95 public BestFirstStrategyForModelGeneration(
91 ReasonerWorkspace workspace, 96 ReasonerWorkspace workspace,
@@ -112,14 +117,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
112 this.context = context; 117 this.context = context;
113 this.solutionStore = context.getGlobalContext().getSolutionStore(); 118 this.solutionStore = context.getGlobalContext().getSolutionStore();
114 119
115 ViatraQueryEngine engine = context.getQueryEngine(); 120// ViatraQueryEngine engine = context.getQueryEngine();
116// // TODO: visualisation 121// // TODO: visualisation
117 matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>(); 122// matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
118 for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) { 123// for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {
119 //System.out.println(p.getSimpleName()); 124// //System.out.println(p.getSimpleName());
120 ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine); 125// ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);
121 matchers.add(matcher); 126// matchers.add(matcher);
122 } 127// }
123 128
124 this.solutionStoreWithCopy = new SolutionStoreWithCopy(); 129 this.solutionStoreWithCopy = new SolutionStoreWithCopy();
125 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement); 130 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
@@ -131,6 +136,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
131 return objectiveComparatorHelper.compare(o2.fitness, o1.fitness); 136 return objectiveComparatorHelper.compare(o2.fitness, o1.fitness);
132 } 137 }
133 }; 138 };
139
140 this.numericSolver = new NumericSolver(context, method, false);
134 141
135 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); 142 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);
136 } 143 }
@@ -140,6 +147,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
140 if (!context.checkGlobalConstraints()) { 147 if (!context.checkGlobalConstraints()) {
141 logger.info("Global contraint is not satisifed in the first state. Terminate."); 148 logger.info("Global contraint is not satisifed in the first state. Terminate.");
142 return; 149 return;
150 } else if(!numericSolver.isSatisfiable()) {
151 logger.info("Numeric contraints are not satisifed in the first state. Terminate.");
152 return;
143 } 153 }
144 if (configuration.searchSpaceConstraints.maxDepth == 0) { 154 if (configuration.searchSpaceConstraints.maxDepth == 0) {
145 logger.info("Maximal depth is reached in the initial solution. Terminate."); 155 logger.info("Maximal depth is reached in the initial solution. Terminate.");
@@ -218,6 +228,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
218 } else if (!context.checkGlobalConstraints()) { 228 } else if (!context.checkGlobalConstraints()) {
219 logger.debug("Global contraint is not satisifed."); 229 logger.debug("Global contraint is not satisifed.");
220 context.backtrack(); 230 context.backtrack();
231 } else if (!numericSolver.isSatisfiable()) {
232 logger.debug("Numeric constraints are not satisifed.");
233 context.backtrack();
221 } else { 234 } else {
222 final Fitness nextFitness = context.calculateFitness(); 235 final Fitness nextFitness = context.calculateFitness();
223 checkForSolution(nextFitness); 236 checkForSolution(nextFitness);
@@ -260,8 +273,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
260 private List<Object> selectActivation() { 273 private List<Object> selectActivation() {
261 List<Object> activationIds; 274 List<Object> activationIds;
262 try { 275 try {
263 activationIds = new ArrayList<Object>(context.getUntraversedActivationIds()); 276 activationIds = this.activationSelector.randomizeActivationIDs(context.getUntraversedActivationIds());
264 Collections.shuffle(activationIds);
265 } catch (NullPointerException e) { 277 } catch (NullPointerException e) {
266 numberOfStatecoderFail++; 278 numberOfStatecoderFail++;
267 activationIds = Collections.emptyList(); 279 activationIds = Collections.emptyList();
@@ -272,7 +284,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
272 private void checkForSolution(final Fitness fittness) { 284 private void checkForSolution(final Fitness fittness) {
273 if (fittness.isSatisifiesHardObjectives()) { 285 if (fittness.isSatisifiesHardObjectives()) {
274 if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { 286 if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {
275 solutionStoreWithCopy.newSolution(context); 287 Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context);
288 numericSolver.fillSolutionCopy(trace);
276 solutionStoreWithDiversityDescriptor.newSolution(context); 289 solutionStoreWithDiversityDescriptor.newSolution(context);
277 solutionStore.newSolution(context); 290 solutionStore.newSolution(context);
278 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); 291 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/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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.Random
4import java.util.Collection
5import java.util.Collections
6import java.util.ArrayList
7
8class EvenActivationSelector extends ActivationSelector {
9
10 new(Random r) {
11 super(r)
12 }
13
14 override protected internalRandomizationOfActivationIDs(Collection<Object> activationIDs) {
15 val toShuffle = new ArrayList<Object>(activationIDs);
16 Collections.shuffle(toShuffle);
17 return toShuffle
18 }
19
20} \ 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{
50 50
51 override getComparator() { Comparators.LOWER_IS_BETTER } 51 override getComparator() { Comparators.LOWER_IS_BETTER }
52 override getFitness(ThreadContext context) { 52 override getFitness(ThreadContext context) {
53 var sum = 0.0 53
54 val scopeFitnes = scopeObjective.getFitness(context) 54 val scopeFitnes = scopeObjective.getFitness(context)
55 //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] 55 //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]
56 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) 56 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)
57 57
58 sum+=scopeFitnes 58
59 var multiplicity = 0.0 59 var multiplicity = 0.0
60 for(multiplicityObjective : unfinishedMultiplicityObjectives) { 60 for(multiplicityObjective : unfinishedMultiplicityObjectives) {
61 multiplicity+=multiplicityObjective.getFitness(context)//*0.5 61 multiplicity+=multiplicityObjective.getFitness(context)
62 } 62 }
63 sum+=multiplicity 63 var sum = 0.0
64 sum += scopeFitnes
65 sum +=Math.sqrt(multiplicity *0.1)
64 sum += unfinishedWFsFitness//*0.5 66 sum += unfinishedWFsFitness//*0.5
65 67
66 //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') 68 println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
67 69
68 return sum 70 return sum
69 } 71 }
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..71793aa6
--- /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,164 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
5import java.util.HashMap
6import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
7import org.eclipse.viatra.query.runtime.api.IPatternMatch
8import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
9import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
10import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator
11import org.eclipse.viatra.dse.base.ThreadContext
12import org.eclipse.emf.ecore.EObject
13import java.util.Map
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
20import java.util.List
21import java.math.BigDecimal
22import java.util.LinkedHashSet
23import java.util.LinkedHashMap
24
25class NumericSolver {
26 val ThreadContext threadContext;
27 val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
28 NumericTranslator t = new NumericTranslator
29
30 val boolean caching;
31 Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap
32
33 var long runtime = 0
34 var long cachingTime = 0
35 var int numberOfSolverCalls = 0
36 var int numberOfCachedSolverCalls = 0
37
38 new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) {
39 this.threadContext = threadContext
40 val engine = threadContext.queryEngine
41 for(entry : method.unitPropagationPreconditions.entrySet) {
42 val constraint = entry.key
43 val querySpec = entry.value
44 val matcher = querySpec.getMatcher(engine);
45 constraint2UnitPropagationPrecondition.put(constraint,matcher)
46 }
47 this.caching = caching
48 }
49
50 def getRuntime(){runtime}
51 def getCachingTime(){cachingTime}
52 def getNumberOfSolverCalls(){numberOfSolverCalls}
53 def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls}
54
55 def boolean isSatisfiable() {
56 val start = System.nanoTime
57 var boolean finalResult
58 if(constraint2UnitPropagationPrecondition.empty){
59 finalResult=true
60 } else {
61 val propagatedConstraints = new HashMap
62 for(entry : constraint2UnitPropagationPrecondition.entrySet) {
63 val constraint = entry.key
64 //println(constraint)
65 val allMatches = entry.value.allMatches.map[it.toArray]
66 //println(allMatches.toList)
67 propagatedConstraints.put(constraint,allMatches)
68 }
69 if(propagatedConstraints.values.forall[empty]) {
70 finalResult=true
71 } else {
72 if(caching) {
73 val code = getCode(propagatedConstraints)
74 val cachedResult = satisfiabilityCache.get(code)
75 if(cachedResult === null) {
76 // println('''new problem, call solver''')
77 // for(entry : code.entrySet) {
78 // println('''«entry.key» -> «entry.value»''')
79 // }
80 //println(code.hashCode)
81 this.numberOfSolverCalls++
82 val res = t.delegateIsSatisfiable(propagatedConstraints)
83 satisfiabilityCache.put(code,res)
84 finalResult=res
85 } else {
86 //println('''similar problem, answer from cache''')
87 finalResult=cachedResult
88 this.numberOfCachedSolverCalls++
89 }
90 } else {
91 finalResult= t.delegateIsSatisfiable(propagatedConstraints)
92 this.numberOfSolverCalls++
93 }
94 }
95 }
96 this.runtime+=System.nanoTime-start
97 return finalResult
98 }
99
100 def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) {
101 val start = System.nanoTime
102 val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList
103 val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]])
104 this.cachingTime += System.nanoTime-start
105 return res
106 }
107
108 def fillSolutionCopy(Map<EObject, EObject> trace) {
109 val model = threadContext.getModel as PartialInterpretation
110 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
111 if(constraint2UnitPropagationPrecondition.empty) {
112 fillWithDefaultValues(dataObjects,trace)
113 } else {
114 val propagatedConstraints = new HashMap
115 for(entry : constraint2UnitPropagationPrecondition.entrySet) {
116 val constraint = entry.key
117 val allMatches = entry.value.allMatches.map[it.toArray]
118 propagatedConstraints.put(constraint,allMatches)
119 }
120
121 if(propagatedConstraints.values.forall[empty]) {
122 fillWithDefaultValues(dataObjects,trace)
123 } else {
124 val solution = t.delegateGetSolution(dataObjects,propagatedConstraints)
125 fillWithSolutions(dataObjects,solution,trace)
126 }
127 }
128 }
129
130 def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) {
131 for(element : elements) {
132 if(element.valueSet==false) {
133 val value = getDefaultValue(element)
134 val target = trace.get(element) as PrimitiveElement
135 target.fillWithValue(value)
136 }
137 }
138 }
139
140 def protected dispatch getDefaultValue(BooleanElement e) {false}
141 def protected dispatch getDefaultValue(IntegerElement e) {0}
142 def protected dispatch getDefaultValue(RealElement e) {0.0}
143 def protected dispatch getDefaultValue(StringElement e) {""}
144
145 def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Integer> solution, Map<EObject, EObject> trace) {
146 for(element : elements) {
147 if(element.valueSet==false) {
148 if(solution.containsKey(element)) {
149 val value = solution.get(element)
150 val target = trace.get(element) as PrimitiveElement
151 target.fillWithValue(value)
152 } else {
153 val target = trace.get(element) as PrimitiveElement
154 target.fillWithValue(target.defaultValue)
155 }
156 }
157 }
158 }
159
160 def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean}
161 def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer}
162 def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=BigDecimal.valueOf(value as Double) }
163 def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String}
164} \ 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 {
25 newSolution(context) 25 newSolution(context)
26 }*/ 26 }*/
27 27
28 def newSolution(ThreadContext context) { 28 def Map<EObject,EObject> newSolution(ThreadContext context) {
29 //print(System.nanoTime-initTime + ";") 29 //print(System.nanoTime-initTime + ";")
30 val copyStart = System.nanoTime 30 val copyStart = System.nanoTime
31 val solution = context.model as PartialInterpretation 31 val solution = context.model as PartialInterpretation
@@ -36,6 +36,7 @@ class SolutionStoreWithCopy {
36 copyTraces.add(copier) 36 copyTraces.add(copier)
37 runtime += System.nanoTime - copyStart 37 runtime += System.nanoTime - copyStart
38 solutionTimes.add(System.nanoTime-sartTime) 38 solutionTimes.add(System.nanoTime-sartTime)
39 return copier
39 } 40 }
40 def getSumRuntime() { 41 def getSumRuntime() {
41 return runtime 42 return runtime
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
30import static guru.nidi.graphviz.model.Factory.* 30import static guru.nidi.graphviz.model.Factory.*
31 31
32import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 32import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
33import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
33 34
34class GraphvizVisualiser implements PartialInterpretationVisualiser { 35class GraphvizVisualiser implements PartialInterpretationVisualiser {
35 36
@@ -106,10 +107,10 @@ class GraphvizVisualiser implements PartialInterpretationVisualiser {
106// elements2Node.put(newElement,image) 107// elements2Node.put(newElement,image)
107// } 108// }
108 109
109 partialInterpretation.newElements.filter(BooleanElement).drawDataTypes([it.value.toString],elements2Node,elements2ID) 110 //partialInterpretation.newElements.filter(BooleanElement).drawDataTypes([it.value.toString],elements2Node,elements2ID)
110 partialInterpretation.newElements.filter(IntegerElement).drawDataTypes([it.value.toString],elements2Node,elements2ID) 111 //partialInterpretation.newElements.filter(IntegerElement).drawDataTypes([it.value.toString],elements2Node,elements2ID)
111 partialInterpretation.newElements.filter(StringElement).drawDataTypes(['''"«it.value.toString»"'''],elements2Node,elements2ID) 112 //partialInterpretation.newElements.filter(StringElement).drawDataTypes(['''"«it.value.toString»"'''],elements2Node,elements2ID)
112 partialInterpretation.newElements.filter(RealElement).drawDataTypes([it.value.toString],elements2Node,elements2ID) 113 //partialInterpretation.newElements.filter(RealElement).drawDataTypes([it.value.toString],elements2Node,elements2ID)
113 114
114 // Drawing the edges 115 // Drawing the edges
115 val edges = new HashMap 116 val edges = new HashMap
@@ -135,35 +136,51 @@ class GraphvizVisualiser implements PartialInterpretationVisualiser {
135 return new GraphvizVisualisation(graph) 136 return new GraphvizVisualisation(graph)
136 } 137 }
137 138
138 def protected <T extends DefinedElement> void drawDataTypes(Iterable<T> collection, Function1<T,String> namer, HashMap<DefinedElement, Node> elements2Node, HashMap<DefinedElement, String> elements2ID) { 139// def protected <T extends DefinedElement> void drawDataTypes(Iterable<T> collection, Function1<T,String> namer, HashMap<DefinedElement, Node> elements2Node, HashMap<DefinedElement, String> elements2ID) {
139 for(booleanElementIndex: 0..<collection.size) { 140// for(booleanElementIndex: 0..<collection.size) {
140 val newElement = collection.get(booleanElementIndex) 141// val newElement = collection.get(booleanElementIndex)
141 val id = namer.apply(newElement) 142// val name = namer.apply(newElement)
142 val image = drawElement(newElement,id,false,emptySet,emptySet) 143// val image = drawElement(newElement,name,newElement.lookup(elements2ID),false,emptySet,emptySet)
143 elements2ID.put(newElement,id) 144// elements2Node.put(newElement,image)
144 elements2Node.put(newElement,image) 145// }
145 } 146// }
146 }
147 147
148 def protected drawElement(DefinedElement element, String ID, boolean old, Set<Type> mustTypes, Set<Type> mayTypes) { 148 def protected drawElement(DefinedElement element, String ID, boolean old, Set<Type> mustTypes, Set<Type> mayTypes) {
149 var tableStyle = ''' CELLSPACING="0" BORDER="2" CELLBORDER="0" CELLPADDING="1" STYLE="ROUNDED"''' 149 var tableStyle = ''' CELLSPACING="0" BORDER="2" CELLBORDER="0" CELLPADDING="1" STYLE="ROUNDED"'''
150 if(typeColoringStyle==TypeColoringStyle::AVERAGE) { 150 if(typeColoringStyle==TypeColoringStyle::AVERAGE) {
151 tableStyle += ''' BGCOLOR="#«typePredicateColor(mustTypes).toBackgroundColorString»"''' 151 tableStyle += ''' BGCOLOR="#«typePredicateColor(mustTypes).toBackgroundColorString»"'''
152 } 152 }
153 val mainLabel = if(element.name !== null) { 153 val mainLabel = if(element instanceof PrimitiveElement) {
154 if(element.isValueSet) {
155 if(element instanceof BooleanElement) { element.value.toString }
156 else if(element instanceof IntegerElement) { element.value.toString }
157 else if(element instanceof RealElement) { element.value.toString }
158 else if(element instanceof StringElement) { "\""+element.value.toString+"\"" }
159 } else {
160 "?"
161 }
162 }else if(element.name !== null) {
154 val parts = element.name.split("\\s+") 163 val parts = element.name.split("\\s+")
155 textWithSubSup(parts.getOrNull(0),parts.getOrNull(1),parts.getOrNull(2),null) 164 textWithSubSup(parts.getOrNull(0),parts.getOrNull(1),parts.getOrNull(2),null)
156 } else { 165 } else {
157 val parts = ID.split("\\s+") 166 val parts = ID.split("\\s+")
158 textWithSubSup(parts.getOrNull(0),parts.getOrNull(1),parts.getOrNull(2),null) 167 textWithSubSup(parts.getOrNull(0),parts.getOrNull(1),parts.getOrNull(2),null)
159 } 168 }
160 val label = Label.html( 169 val hasNoCompexType = (mustTypes.empty) && (mayTypes.empty)
170
171 val label = if(hasNoCompexType) {
172 Label.html(
173 '''<TABLE«tableStyle»>'''+
174 '''<TR><TD COLSPAN="2"> «mainLabel» </TD></TR>'''+
175 '''</TABLE>''')
176 } else {
177 Label.html(
161 '''<TABLE«tableStyle»>'''+ 178 '''<TABLE«tableStyle»>'''+
162 '''<TR><TD COLSPAN="2" BORDER="2" SIDES="B">«mainLabel»</TD></TR>'''+ 179 '''<TR><TD COLSPAN="2" BORDER="2" SIDES="B">«mainLabel»</TD></TR>'''+
163 '''«FOR mustTypeName : mustTypes.map[it.name].sort»«typePredicateDescription(mustTypeName,true)»«ENDFOR»'''+ 180 '''«FOR mustTypeName : mustTypes.map[it.name].sort»«typePredicateDescription(mustTypeName,true)»«ENDFOR»'''+
164 '''«FOR mayTypeName : mayTypes.map[it.name].sort»«typePredicateDescription(mayTypeName,false)»«ENDFOR»'''+ 181 '''«FOR mayTypeName : mayTypes.map[it.name].sort»«typePredicateDescription(mayTypeName,false)»«ENDFOR»'''+
165 '''</TABLE>''') 182 '''</TABLE>''')
166 183 }
167 val node = node(ID).with(label).with( 184 val node = node(ID).with(label).with(
168 Shape.NONE 185 Shape.NONE
169 //, 186 //,
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-16 18:18:50 +0000