aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers
diff options
context:
space:
mode:
authorLibravatar Oszkar Semerath <semerath@mit.bme.hu>2020-05-11 02:22:15 +0200
committerLibravatar Oszkar Semerath <semerath@mit.bme.hu>2020-05-11 02:22:15 +0200
commit91b772506f00ce2e317027dd384b82dc7a1295fd (patch)
tree19fd1b945cae52a4b32357f48ee2da3aa7ca1d5b /Solvers
parentautomated containment and attribute addition for subclasses (diff)
downloadVIATRA-Generator-91b772506f00ce2e317027dd384b82dc7a1295fd.tar.gz
VIATRA-Generator-91b772506f00ce2e317027dd384b82dc7a1295fd.tar.zst
VIATRA-Generator-91b772506f00ce2e317027dd384b82dc7a1295fd.zip
separated must and current UP rules to support non-prop neg finds
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.xtend9
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend12
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend20
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend42
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java18
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend58
7 files changed, 106 insertions, 55 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 975ace2f..be11ed78 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
@@ -38,7 +38,8 @@ class ModelGenerationStatistics {
38 38
39 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF 39 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF
40 40
41 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditions 41 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions
42 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions
42 43
43 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns 44 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns
44} 45}
@@ -81,7 +82,8 @@ class ModelGenerationMethodProvider {
81 82
82 val invalidWF = queries.getInvalidWFQueries.values 83 val invalidWF = queries.getInvalidWFQueries.values
83 84
84 val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns 85 val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns
86 val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns
85 87
86 return new ModelGenerationMethod( 88 return new ModelGenerationMethod(
87 statistics, 89 statistics,
@@ -90,7 +92,8 @@ class ModelGenerationMethodProvider {
90 unfinishedMultiplicities, 92 unfinishedMultiplicities,
91 unfinishedWF, 93 unfinishedWF,
92 invalidWF, 94 invalidWF,
93 unitPropagationPreconditions, 95 mustUnitPropagationPreconditions,
96 currentUnitPropagationPreconditions,
94 queries.allQueries 97 queries.allQueries
95 ) 98 )
96 } 99 }
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 d5ebe318..219f99e9 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
@@ -26,6 +26,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
26import org.eclipse.xtend.lib.annotations.Accessors 26import org.eclipse.xtend.lib.annotations.Accessors
27 27
28import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 28import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
29import org.eclipse.xtend.lib.annotations.Data
30import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
31
32@Data class PatternGeneratorResult {
33 CharSequence patternText
34 HashMap<PConstraint,String> constraint2MustPreconditionName
35 HashMap<PConstraint,String> constraint2CurrentPreconditionName
36}
29 37
30class PatternGenerator { 38class PatternGenerator {
31 @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) 39 @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this)
@@ -149,7 +157,7 @@ class PatternGenerator {
149 problem.allTypeReferences.exists[it instanceof StringTypeReference] 157 problem.allTypeReferences.exists[it instanceof StringTypeReference]
150 } 158 }
151 159
152 public def transformBaseProperties( 160 public def PatternGeneratorResult transformBaseProperties(
153 LogicProblem problem, 161 LogicProblem problem,
154 PartialInterpretation emptySolution, 162 PartialInterpretation emptySolution,
155 Map<String,PQuery> fqn2PQuery, 163 Map<String,PQuery> fqn2PQuery,
@@ -398,6 +406,6 @@ class PatternGenerator {
398 ''' 406 '''
399 val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery) 407 val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)
400 val second = up.definitions 408 val second = up.definitions
401 return (first+second) -> up.constraint2PreconditionName 409 return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName)
402 } 410 }
403} 411}
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 18e3018a..750107f6 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
@@ -31,7 +31,8 @@ import java.util.HashMap
31 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries 31 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries
32 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries 32 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries
33 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 34 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns
35 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns
35 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries 36 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries
36} 37}
37 38
@@ -60,14 +61,15 @@ class PatternProvider {
60 null 61 null
61 } 62 }
62 val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) 63 val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult)
63 val baseIndexerFile = patternGeneratorResult.key 64 val baseIndexerFile = patternGeneratorResult.patternText
64 val unitPropagationTrace = patternGeneratorResult.value 65 val mustUnitPropagationTrace = patternGeneratorResult.constraint2MustPreconditionName
66 val currentUnitPropagationTrace = patternGeneratorResult.constraint2CurrentPreconditionName
65 if(writeToFile) { 67 if(writeToFile) {
66 workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) 68 workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile)
67 } 69 }
68 val ParseUtil parseUtil = new ParseUtil 70 val ParseUtil parseUtil = new ParseUtil
69 val generatedQueries = parseUtil.parse(baseIndexerFile) 71 val generatedQueries = parseUtil.parse(baseIndexerFile)
70 val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,unitPropagationTrace,generatedQueries); 72 val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,mustUnitPropagationTrace,currentUnitPropagationTrace,generatedQueries);
71 return runtimeQueries 73 return runtimeQueries
72 } 74 }
73 75
@@ -76,7 +78,8 @@ class PatternProvider {
76 LogicProblem problem, 78 LogicProblem problem,
77 PartialInterpretation emptySolution, 79 PartialInterpretation emptySolution,
78 TypeAnalysisResult typeAnalysisResult, 80 TypeAnalysisResult typeAnalysisResult,
79 HashMap<PConstraint, String> unitPropagationTrace, 81 HashMap<PConstraint, String> mustUnitPropagationTrace,
82 HashMap<PConstraint, String> currentUnitPropagationTrace,
80 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries 83 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries
81 ) { 84 ) {
82 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 85 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
@@ -92,7 +95,9 @@ class PatternProvider {
92 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 95 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
93 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] 96 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]
94 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 97 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
95 unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)] 98 mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)]
99 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
100 currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)]
96 return new GeneratedPatterns( 101 return new GeneratedPatterns(
97 invalidWFQueries, 102 invalidWFQueries,
98 unfinishedWFQueries, 103 unfinishedWFQueries,
@@ -100,7 +105,8 @@ class PatternProvider {
100 refineObjectsQueries, 105 refineObjectsQueries,
101 refineTypeQueries, 106 refineTypeQueries,
102 refineRelationQueries, 107 refineRelationQueries,
103 unitPropagationPreconditionPatterns, 108 mustUnitPropagationPreconditionPatterns,
109 currentUnitPropagationPreconditionPatterns,
104 queries.values 110 queries.values
105 ) 111 )
106 } 112 }
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 d487db64..91a7a2c2 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
@@ -61,7 +61,8 @@ class UnitPropagationPreconditionGenerationResult {
61@Data 61@Data
62class UnitPropagationPreconditionFinalResult { 62class UnitPropagationPreconditionFinalResult {
63 CharSequence definitions 63 CharSequence definitions
64 HashMap<PConstraint,String> constraint2PreconditionName 64 HashMap<PConstraint,String> constraint2MustPreconditionName
65 HashMap<PConstraint,String> constraint2CurrentPreconditionName
65} 66}
66 67
67class UnitPropagationPreconditionGenerator { 68class UnitPropagationPreconditionGenerator {
@@ -81,25 +82,34 @@ class UnitPropagationPreconditionGenerator {
81 // Create an empty result 82 // Create an empty result
82 val res = new UnitPropagationPreconditionGenerationResult 83 val res = new UnitPropagationPreconditionGenerationResult
83 val wfs = base.wfQueries(problem)//.map[it.patternPQuery] 84 val wfs = base.wfQueries(problem)//.map[it.patternPQuery]
84 val Map<PConstraint,List<Pair<String,Integer>>> mainPropagationNames = new HashMap 85 val Map<PConstraint,List<Pair<String,Integer>>> mainMustPropagationNames = new HashMap
86 val Map<PConstraint,List<Pair<String,Integer>>> mainCurrentPropagationNames = new HashMap
85 for(wf : wfs) { 87 for(wf : wfs) {
86 val query = wf.patternPQuery as PQuery 88 val query = wf.patternPQuery as PQuery
87 val relation = wf.target 89 val relation = wf.target
88 val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) 90 val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation)
89 91
90 for(referredCheck : allReferredChecks) { 92 for(referredCheck : allReferredChecks) {
91 val propagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) 93 val mustPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST)
92 if(!mainPropagationNames.containsKey(referredCheck)) { 94 val currentPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::CURRENT)
93 mainPropagationNames.put(referredCheck,new LinkedList) 95 if(!mainMustPropagationNames.containsKey(referredCheck)) {
96 mainMustPropagationNames.put(referredCheck,new LinkedList)
94 } 97 }
95 if(propagationPrecondition !== null) { 98 if(!mainCurrentPropagationNames.containsKey(referredCheck)) {
96 mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size) 99 mainCurrentPropagationNames.put(referredCheck,new LinkedList)
100 }
101 if(mustPropagationPrecondition !== null) {
102 mainMustPropagationNames.get(referredCheck).add(mustPropagationPrecondition->query.parameterNames.size)
103 }
104 if(currentPropagationPrecondition !== null) {
105 mainCurrentPropagationNames.get(referredCheck).add(currentPropagationPrecondition->query.parameterNames.size)
97 } 106 }
98 } 107 }
99 } 108 }
100 val preconditions = new LinkedList 109 val preconditions = new LinkedList
101 val constraint2Precondition = new HashMap 110 val constraint2MustPrecondition = new HashMap
102 for(entry : mainPropagationNames.entrySet) { 111 val constraint2CurrentPrecondition = new HashMap
112 for(entry : mainMustPropagationNames.entrySet) {
103 val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; 113 val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
104 val def = ''' 114 val def = '''
105 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») 115 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
@@ -107,7 +117,17 @@ class UnitPropagationPreconditionGenerator {
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»); } 117 { 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»''' 118 «ENDFOR»'''
109 preconditions+=def 119 preconditions+=def
110 constraint2Precondition.put(entry.key,name) 120 constraint2MustPrecondition.put(entry.key,name)
121 }
122 for(entry : mainCurrentPropagationNames.entrySet) {
123 val name = '''UPCurrentPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
124 val def = '''
125 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
126 «FOR propagation : entry.value SEPARATOR " or "»
127 { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }
128 «ENDFOR»'''
129 preconditions+=def
130 constraint2CurrentPrecondition.put(entry.key,name)
111 } 131 }
112 132
113 val definitions = ''' 133 val definitions = '''
@@ -121,7 +141,7 @@ class UnitPropagationPreconditionGenerator {
121 «predondition» 141 «predondition»
122 «ENDFOR» 142 «ENDFOR»
123 ''' 143 '''
124 return new UnitPropagationPreconditionFinalResult(definitions,constraint2Precondition) 144 return new UnitPropagationPreconditionFinalResult(definitions,constraint2MustPrecondition,constraint2CurrentPrecondition)
125 } 145 }
126 def allReferredConstraints(Relation relation, PQuery query) { 146 def allReferredConstraints(Relation relation, PQuery query) {
127 val allReferredQueries = query.allReferredQueries 147 val allReferredQueries = query.allReferredQueries
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 18fe94e4..45dffe7c 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
@@ -147,7 +147,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
147 if (!context.checkGlobalConstraints()) { 147 if (!context.checkGlobalConstraints()) {
148 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.");
149 return; 149 return;
150 } else if(!numericSolver.isSatisfiable()) { 150 } else if(!numericSolver.maySatisfiable()) {
151 logger.info("Numeric contraints are not satisifed in the first state. Terminate."); 151 logger.info("Numeric contraints are not satisifed in the first state. Terminate.");
152 return; 152 return;
153 } 153 }
@@ -228,7 +228,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
228 } else if (!context.checkGlobalConstraints()) { 228 } else if (!context.checkGlobalConstraints()) {
229 logger.debug("Global contraint is not satisifed."); 229 logger.debug("Global contraint is not satisifed.");
230 context.backtrack(); 230 context.backtrack();
231 } else if (!numericSolver.isSatisfiable()) { 231 } else if (!numericSolver.maySatisfiable()) {
232 logger.debug("Numeric constraints are not satisifed."); 232 logger.debug("Numeric constraints are not satisifed.");
233 context.backtrack(); 233 context.backtrack();
234 } else { 234 } else {
@@ -284,13 +284,15 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
284 private void checkForSolution(final Fitness fittness) { 284 private void checkForSolution(final Fitness fittness) {
285 if (fittness.isSatisifiesHardObjectives()) { 285 if (fittness.isSatisifiesHardObjectives()) {
286 if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { 286 if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {
287 Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context); 287 if(numericSolver.currentSatisfiable()) {
288 numericSolver.fillSolutionCopy(trace); 288 Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context);
289 solutionStoreWithDiversityDescriptor.newSolution(context); 289 numericSolver.fillSolutionCopy(trace);
290 solutionStore.newSolution(context); 290 solutionStoreWithDiversityDescriptor.newSolution(context);
291 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); 291 solutionStore.newSolution(context);
292 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);
292 293
293 logger.debug("Found a solution."); 294 logger.debug("Found a solution.");
295 }
294 } 296 }
295 } 297 }
296 } 298 }
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 a75ddf76..9e4792e0 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
@@ -62,7 +62,7 @@ class ModelGenerationCompositeObjective implements IObjective{
62 } 62 }
63 var sum = 0.0 63 var sum = 0.0
64 sum += scopeFitnes 64 sum += scopeFitnes
65 sum +=Math.sqrt(multiplicity *0.1) 65 sum +=multiplicity
66 sum += unfinishedWFsFitness//*0.5 66 sum += unfinishedWFsFitness//*0.5
67 67
68 println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') 68 println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
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 71793aa6..fe378bd3 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
@@ -1,30 +1,29 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 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 3import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator
11import org.eclipse.viatra.dse.base.ThreadContext 4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
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 5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement 6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement 7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement 9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
20import java.util.List 10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
21import java.math.BigDecimal 11import java.math.BigDecimal
22import java.util.LinkedHashSet 12import java.util.HashMap
23import java.util.LinkedHashMap 13import java.util.LinkedHashMap
14import java.util.LinkedHashSet
15import java.util.List
16import java.util.Map
17import org.eclipse.emf.ecore.EObject
18import org.eclipse.viatra.dse.base.ThreadContext
19import org.eclipse.viatra.query.runtime.api.IPatternMatch
20import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
21import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
24 22
25class NumericSolver { 23class NumericSolver {
26 val ThreadContext threadContext; 24 val ThreadContext threadContext;
27 val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> 25 val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
26 val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
28 NumericTranslator t = new NumericTranslator 27 NumericTranslator t = new NumericTranslator
29 28
30 val boolean caching; 29 val boolean caching;
@@ -38,11 +37,17 @@ class NumericSolver {
38 new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { 37 new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) {
39 this.threadContext = threadContext 38 this.threadContext = threadContext
40 val engine = threadContext.queryEngine 39 val engine = threadContext.queryEngine
41 for(entry : method.unitPropagationPreconditions.entrySet) { 40 for(entry : method.mustUnitPropagationPreconditions.entrySet) {
41 val constraint = entry.key
42 val querySpec = entry.value
43 val matcher = querySpec.getMatcher(engine);
44 constraint2MustUnitPropagationPrecondition.put(constraint,matcher)
45 }
46 for(entry : method.currentUnitPropagationPreconditions.entrySet) {
42 val constraint = entry.key 47 val constraint = entry.key
43 val querySpec = entry.value 48 val querySpec = entry.value
44 val matcher = querySpec.getMatcher(engine); 49 val matcher = querySpec.getMatcher(engine);
45 constraint2UnitPropagationPrecondition.put(constraint,matcher) 50 constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher)
46 } 51 }
47 this.caching = caching 52 this.caching = caching
48 } 53 }
@@ -52,14 +57,21 @@ class NumericSolver {
52 def getNumberOfSolverCalls(){numberOfSolverCalls} 57 def getNumberOfSolverCalls(){numberOfSolverCalls}
53 def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} 58 def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls}
54 59
55 def boolean isSatisfiable() { 60 def boolean maySatisfiable() {
61 isSatisfiable(this.constraint2MustUnitPropagationPrecondition)
62 }
63 def boolean currentSatisfiable() {
64 isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition)
65 }
66
67 private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) {
56 val start = System.nanoTime 68 val start = System.nanoTime
57 var boolean finalResult 69 var boolean finalResult
58 if(constraint2UnitPropagationPrecondition.empty){ 70 if(matches.empty){
59 finalResult=true 71 finalResult=true
60 } else { 72 } else {
61 val propagatedConstraints = new HashMap 73 val propagatedConstraints = new HashMap
62 for(entry : constraint2UnitPropagationPrecondition.entrySet) { 74 for(entry : matches.entrySet) {
63 val constraint = entry.key 75 val constraint = entry.key
64 //println(constraint) 76 //println(constraint)
65 val allMatches = entry.value.allMatches.map[it.toArray] 77 val allMatches = entry.value.allMatches.map[it.toArray]
@@ -108,11 +120,11 @@ class NumericSolver {
108 def fillSolutionCopy(Map<EObject, EObject> trace) { 120 def fillSolutionCopy(Map<EObject, EObject> trace) {
109 val model = threadContext.getModel as PartialInterpretation 121 val model = threadContext.getModel as PartialInterpretation
110 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList 122 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList
111 if(constraint2UnitPropagationPrecondition.empty) { 123 if(constraint2CurrentUnitPropagationPrecondition.empty) {
112 fillWithDefaultValues(dataObjects,trace) 124 fillWithDefaultValues(dataObjects,trace)
113 } else { 125 } else {
114 val propagatedConstraints = new HashMap 126 val propagatedConstraints = new HashMap
115 for(entry : constraint2UnitPropagationPrecondition.entrySet) { 127 for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) {
116 val constraint = entry.key 128 val constraint = entry.key
117 val allMatches = entry.value.allMatches.map[it.toArray] 129 val allMatches = entry.value.allMatches.map[it.toArray]
118 propagatedConstraints.put(constraint,allMatches) 130 propagatedConstraints.put(constraint,allMatches)
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-07 20:56:47 +0000