diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit')
4 files changed, 51 insertions, 36 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 293df935..1fe65afe 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 | |||
@@ -113,8 +113,9 @@ class ViatraReasoner extends LogicReasoner{ | |||
113 | 113 | ||
114 | val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method) | 114 | val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method) |
115 | viatraConfig.progressMonitor.workedForwardTransformation | 115 | viatraConfig.progressMonitor.workedForwardTransformation |
116 | val transformationFinished = System.nanoTime | ||
117 | val transformationTime = transformationFinished - transformationStartTime | ||
116 | 118 | ||
117 | val transformationTime = System.nanoTime - transformationStartTime | ||
118 | val solverStartTime = System.nanoTime | 119 | val solverStartTime = System.nanoTime |
119 | 120 | ||
120 | var boolean stoppedByTimeout | 121 | var boolean stoppedByTimeout |
@@ -141,6 +142,9 @@ class ViatraReasoner extends LogicReasoner{ | |||
141 | ] | 142 | ] |
142 | } | 143 | } |
143 | it.entries += createIntStatisticEntry => [ | 144 | it.entries += createIntStatisticEntry => [ |
145 | it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int | ||
146 | ] | ||
147 | it.entries += createIntStatisticEntry => [ | ||
144 | it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int | 148 | it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int |
145 | ] | 149 | ] |
146 | it.entries += createIntStatisticEntry => [ | 150 | it.entries += createIntStatisticEntry => [ |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index c4d7e231..24578e7b 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend | |||
@@ -45,6 +45,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{ | |||
45 | * Configuration for cutting search space. | 45 | * Configuration for cutting search space. |
46 | */ | 46 | */ |
47 | public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint | 47 | public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint |
48 | |||
49 | public var runIntermediateNumericalConsistencyChecks = true | ||
48 | } | 50 | } |
49 | 51 | ||
50 | public class DiversityDescriptor { | 52 | public class DiversityDescriptor { |
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 45dffe7c..75ce7f10 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 | |||
@@ -91,6 +91,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
91 | private int numberOfPrintedModel = 0; | 91 | private int numberOfPrintedModel = 0; |
92 | private int numberOfSolverCalls = 0; | 92 | private int numberOfSolverCalls = 0; |
93 | 93 | ||
94 | public long explorationStarted = 0; | ||
94 | 95 | ||
95 | public BestFirstStrategyForModelGeneration( | 96 | public BestFirstStrategyForModelGeneration( |
96 | ReasonerWorkspace workspace, | 97 | ReasonerWorkspace workspace, |
@@ -119,7 +120,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
119 | 120 | ||
120 | // ViatraQueryEngine engine = context.getQueryEngine(); | 121 | // ViatraQueryEngine engine = context.getQueryEngine(); |
121 | // // TODO: visualisation | 122 | // // TODO: visualisation |
122 | // matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>(); | 123 | // LinkedList<ViatraQueryMatcher<? extends IPatternMatch>> matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>(); |
123 | // for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) { | 124 | // for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) { |
124 | // //System.out.println(p.getSimpleName()); | 125 | // //System.out.println(p.getSimpleName()); |
125 | // ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine); | 126 | // ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine); |
@@ -137,13 +138,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
137 | } | 138 | } |
138 | }; | 139 | }; |
139 | 140 | ||
140 | this.numericSolver = new NumericSolver(context, method, false); | 141 | this.numericSolver = new NumericSolver(context, method, false,this.configuration.runIntermediateNumericalConsistencyChecks); |
141 | 142 | ||
142 | trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); | 143 | trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); |
143 | } | 144 | } |
144 | 145 | ||
145 | @Override | 146 | @Override |
146 | public void explore() { | 147 | public void explore() { |
148 | this.explorationStarted=System.nanoTime(); | ||
147 | if (!context.checkGlobalConstraints()) { | 149 | if (!context.checkGlobalConstraints()) { |
148 | logger.info("Global contraint is not satisifed in the first state. Terminate."); | 150 | logger.info("Global contraint is not satisifed in the first state. Terminate."); |
149 | return; | 151 | return; |
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 0fb5d702..a012f51b 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 | |||
@@ -26,6 +26,7 @@ class NumericSolver { | |||
26 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 26 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
27 | NumericTranslator t = new NumericTranslator | 27 | NumericTranslator t = new NumericTranslator |
28 | 28 | ||
29 | val boolean intermediateConsistencyCheck | ||
29 | val boolean caching; | 30 | val boolean caching; |
30 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap | 31 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap |
31 | 32 | ||
@@ -34,7 +35,7 @@ class NumericSolver { | |||
34 | var int numberOfSolverCalls = 0 | 35 | var int numberOfSolverCalls = 0 |
35 | var int numberOfCachedSolverCalls = 0 | 36 | var int numberOfCachedSolverCalls = 0 |
36 | 37 | ||
37 | new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { | 38 | new(ThreadContext threadContext, ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) { |
38 | this.threadContext = threadContext | 39 | this.threadContext = threadContext |
39 | val engine = threadContext.queryEngine | 40 | val engine = threadContext.queryEngine |
40 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { | 41 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { |
@@ -49,6 +50,8 @@ class NumericSolver { | |||
49 | val matcher = querySpec.getMatcher(engine); | 50 | val matcher = querySpec.getMatcher(engine); |
50 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) | 51 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) |
51 | } | 52 | } |
53 | this.intermediateConsistencyCheck = true | ||
54 | println() | ||
52 | this.caching = caching | 55 | this.caching = caching |
53 | } | 56 | } |
54 | 57 | ||
@@ -70,44 +73,48 @@ class NumericSolver { | |||
70 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { | 73 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { |
71 | val start = System.nanoTime | 74 | val start = System.nanoTime |
72 | var boolean finalResult | 75 | var boolean finalResult |
73 | if(matches.empty){ | 76 | if(intermediateConsistencyCheck) { |
74 | finalResult=true | 77 | if(matches.empty){ |
75 | } else { | ||
76 | val propagatedConstraints = new HashMap | ||
77 | for(entry : matches.entrySet) { | ||
78 | val constraint = entry.key | ||
79 | //println(constraint) | ||
80 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
81 | //println(allMatches.toList) | ||
82 | propagatedConstraints.put(constraint,allMatches) | ||
83 | } | ||
84 | if(propagatedConstraints.values.forall[empty]) { | ||
85 | finalResult=true | 78 | finalResult=true |
86 | } else { | 79 | } else { |
87 | if(caching) { | 80 | val propagatedConstraints = new HashMap |
88 | val code = getCode(propagatedConstraints) | 81 | for(entry : matches.entrySet) { |
89 | val cachedResult = satisfiabilityCache.get(code) | 82 | val constraint = entry.key |
90 | if(cachedResult === null) { | 83 | //println(constraint) |
91 | // println('''new problem, call solver''') | 84 | val allMatches = entry.value.allMatches.map[it.toArray] |
92 | // for(entry : code.entrySet) { | 85 | //println(allMatches.toList) |
93 | // println('''«entry.key» -> «entry.value»''') | 86 | propagatedConstraints.put(constraint,allMatches) |
94 | // } | 87 | } |
95 | //println(code.hashCode) | 88 | if(propagatedConstraints.values.forall[empty]) { |
96 | this.numberOfSolverCalls++ | 89 | finalResult=true |
97 | val res = t.delegateIsSatisfiable(propagatedConstraints) | 90 | } else { |
98 | satisfiabilityCache.put(code,res) | 91 | if(caching) { |
99 | finalResult=res | 92 | val code = getCode(propagatedConstraints) |
93 | val cachedResult = satisfiabilityCache.get(code) | ||
94 | if(cachedResult === null) { | ||
95 | // println('''new problem, call solver''') | ||
96 | // for(entry : code.entrySet) { | ||
97 | // println('''«entry.key» -> «entry.value»''') | ||
98 | // } | ||
99 | //println(code.hashCode) | ||
100 | this.numberOfSolverCalls++ | ||
101 | val res = t.delegateIsSatisfiable(propagatedConstraints) | ||
102 | satisfiabilityCache.put(code,res) | ||
103 | finalResult=res | ||
104 | } else { | ||
105 | //println('''similar problem, answer from cache''') | ||
106 | finalResult=cachedResult | ||
107 | this.numberOfCachedSolverCalls++ | ||
108 | } | ||
100 | } else { | 109 | } else { |
101 | //println('''similar problem, answer from cache''') | 110 | finalResult= t.delegateIsSatisfiable(propagatedConstraints) |
102 | finalResult=cachedResult | 111 | this.numberOfSolverCalls++ |
103 | this.numberOfCachedSolverCalls++ | ||
104 | } | 112 | } |
105 | } else { | ||
106 | finalResult= t.delegateIsSatisfiable(propagatedConstraints) | ||
107 | this.numberOfSolverCalls++ | ||
108 | } | 113 | } |
109 | } | 114 | } |
110 | } | 115 | } else { |
116 | finalResult = true | ||
117 | } | ||
111 | this.runtime+=System.nanoTime-start | 118 | this.runtime+=System.nanoTime-start |
112 | return finalResult | 119 | return finalResult |
113 | } | 120 | } |