diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu')
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.ArrayList | ||
4 | import java.util.Collection | ||
5 | import java.util.Random | ||
6 | |||
7 | abstract 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.Collection | ||
4 | import java.util.HashMap | ||
5 | import java.util.Map | ||
6 | import java.util.List | ||
7 | import java.util.Random | ||
8 | import java.util.ArrayList | ||
9 | import java.util.LinkedList | ||
10 | import java.util.Collections | ||
11 | |||
12 | class 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; | |||
17 | import java.util.Iterator; | 17 | import java.util.Iterator; |
18 | import java.util.LinkedList; | 18 | import java.util.LinkedList; |
19 | import java.util.List; | 19 | import java.util.List; |
20 | import java.util.Map; | ||
20 | import java.util.PriorityQueue; | 21 | import java.util.PriorityQueue; |
21 | import java.util.Random; | 22 | import java.util.Random; |
22 | 23 | ||
23 | import org.apache.log4j.Logger; | 24 | import org.apache.log4j.Logger; |
25 | import org.eclipse.emf.ecore.EObject; | ||
24 | import org.eclipse.emf.ecore.util.EcoreUtil; | 26 | import org.eclipse.emf.ecore.util.EcoreUtil; |
25 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; | 27 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; |
26 | import org.eclipse.viatra.dse.base.ThreadContext; | 28 | import org.eclipse.viatra.dse.base.ThreadContext; |
@@ -38,6 +40,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | |||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; | 40 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; |
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 41 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 42 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
43 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver; | ||
41 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; | 44 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; |
42 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; | 45 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; |
43 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; | 46 | import 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.Random | ||
4 | import java.util.Collection | ||
5 | import java.util.Collections | ||
6 | import java.util.ArrayList | ||
7 | |||
8 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
5 | import java.util.HashMap | ||
6 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
7 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
9 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
10 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | ||
11 | import org.eclipse.viatra.dse.base.ThreadContext | ||
12 | import org.eclipse.emf.ecore.EObject | ||
13 | import java.util.Map | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | ||
20 | import java.util.List | ||
21 | import java.math.BigDecimal | ||
22 | import java.util.LinkedHashSet | ||
23 | import java.util.LinkedHashMap | ||
24 | |||
25 | class 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 |