aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner
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/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner
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/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner')
-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
8 files changed, 309 insertions, 19 deletions
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
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-08-30 04:44:24 +0000