diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src')
7 files changed, 176 insertions, 18 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 cb73f4e8..bafe78f6 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | |||
@@ -155,6 +155,21 @@ class ViatraReasoner extends LogicReasoner{ | |||
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 1cd61e9a..18fe94e4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java | |||
@@ -84,13 +84,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
84 | private ModelResult modelResultByInternalSolver = null; | 84 | private ModelResult modelResultByInternalSolver = null; |
85 | private Random random = new Random(); | 85 | private Random random = new Random(); |
86 | //private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; | 86 | //private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; |
87 | 87 | public ActivationSelector activationSelector = new EvenActivationSelector(random); | |
88 | public NumericSolver numericSolver = null; | ||
88 | // Statistics | 89 | // Statistics |
89 | private int numberOfStatecoderFail = 0; | 90 | private int numberOfStatecoderFail = 0; |
90 | private int numberOfPrintedModel = 0; | 91 | private int numberOfPrintedModel = 0; |
91 | private int numberOfSolverCalls = 0; | 92 | private int numberOfSolverCalls = 0; |
92 | 93 | ||
93 | private NumericSolver numericSolver = null; | ||
94 | 94 | ||
95 | public BestFirstStrategyForModelGeneration( | 95 | public BestFirstStrategyForModelGeneration( |
96 | ReasonerWorkspace workspace, | 96 | ReasonerWorkspace workspace, |
@@ -137,7 +137,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
137 | } | 137 | } |
138 | }; | 138 | }; |
139 | 139 | ||
140 | this.numericSolver = new NumericSolver(context, method); | 140 | this.numericSolver = new NumericSolver(context, method, false); |
141 | 141 | ||
142 | trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); | 142 | trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); |
143 | } | 143 | } |
@@ -273,8 +273,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
273 | private List<Object> selectActivation() { | 273 | private List<Object> selectActivation() { |
274 | List<Object> activationIds; | 274 | List<Object> activationIds; |
275 | try { | 275 | try { |
276 | activationIds = new ArrayList<Object>(context.getUntraversedActivationIds()); | 276 | activationIds = this.activationSelector.randomizeActivationIDs(context.getUntraversedActivationIds()); |
277 | Collections.shuffle(activationIds); | ||
278 | } catch (NullPointerException e) { | 277 | } catch (NullPointerException e) { |
279 | numberOfStatecoderFail++; | 278 | numberOfStatecoderFail++; |
280 | activationIds = Collections.emptyList(); | 279 | activationIds = Collections.emptyList(); |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend new file mode 100644 index 00000000..82a5f32d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend | |||
@@ -0,0 +1,20 @@ | |||
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 index e1745854..71793aa6 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | |||
@@ -19,13 +19,23 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement |
20 | import java.util.List | 20 | import java.util.List |
21 | import java.math.BigDecimal | 21 | import java.math.BigDecimal |
22 | import java.util.LinkedHashSet | ||
23 | import java.util.LinkedHashMap | ||
22 | 24 | ||
23 | class NumericSolver { | 25 | class NumericSolver { |
24 | val ThreadContext threadContext; | 26 | val ThreadContext threadContext; |
25 | val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 27 | val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
26 | NumericTranslator t = new NumericTranslator | 28 | NumericTranslator t = new NumericTranslator |
27 | 29 | ||
28 | new(ThreadContext threadContext, ModelGenerationMethod method) { | 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) { | ||
29 | this.threadContext = threadContext | 39 | this.threadContext = threadContext |
30 | val engine = threadContext.queryEngine | 40 | val engine = threadContext.queryEngine |
31 | for(entry : method.unitPropagationPreconditions.entrySet) { | 41 | for(entry : method.unitPropagationPreconditions.entrySet) { |
@@ -34,11 +44,20 @@ class NumericSolver { | |||
34 | val matcher = querySpec.getMatcher(engine); | 44 | val matcher = querySpec.getMatcher(engine); |
35 | constraint2UnitPropagationPrecondition.put(constraint,matcher) | 45 | constraint2UnitPropagationPrecondition.put(constraint,matcher) |
36 | } | 46 | } |
47 | this.caching = caching | ||
37 | } | 48 | } |
38 | 49 | ||
50 | def getRuntime(){runtime} | ||
51 | def getCachingTime(){cachingTime} | ||
52 | def getNumberOfSolverCalls(){numberOfSolverCalls} | ||
53 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} | ||
54 | |||
39 | def boolean isSatisfiable() { | 55 | def boolean isSatisfiable() { |
40 | if(constraint2UnitPropagationPrecondition.empty) return true | 56 | val start = System.nanoTime |
41 | else { | 57 | var boolean finalResult |
58 | if(constraint2UnitPropagationPrecondition.empty){ | ||
59 | finalResult=true | ||
60 | } else { | ||
42 | val propagatedConstraints = new HashMap | 61 | val propagatedConstraints = new HashMap |
43 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { | 62 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { |
44 | val constraint = entry.key | 63 | val constraint = entry.key |
@@ -47,15 +66,43 @@ class NumericSolver { | |||
47 | //println(allMatches.toList) | 66 | //println(allMatches.toList) |
48 | propagatedConstraints.put(constraint,allMatches) | 67 | propagatedConstraints.put(constraint,allMatches) |
49 | } | 68 | } |
50 | |||
51 | if(propagatedConstraints.values.forall[empty]) { | 69 | if(propagatedConstraints.values.forall[empty]) { |
52 | return true | 70 | finalResult=true |
53 | } else { | 71 | } else { |
54 | val res = t.delegateIsSatisfiable(propagatedConstraints) | 72 | if(caching) { |
55 | //println(res) | 73 | val code = getCode(propagatedConstraints) |
56 | return res | 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 | } | ||
57 | } | 94 | } |
58 | } | 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 | ||
59 | } | 106 | } |
60 | 107 | ||
61 | def fillSolutionCopy(Map<EObject, EObject> trace) { | 108 | def fillSolutionCopy(Map<EObject, EObject> trace) { |