aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-16 01:11:15 +0100
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-16 01:11:15 +0100
commitacb8dedc9d03e1d17f570e07c9f75a571bd66cf8 (patch)
tree56d4f9899af7c70fa006395ffb0b93ff339fac7b /Solvers
parentMinor adjsutments to CrossScen ad FamTree local case studies (diff)
downloadVIATRA-Generator-acb8dedc9d03e1d17f570e07c9f75a571bd66cf8.tar.gz
VIATRA-Generator-acb8dedc9d03e1d17f570e07c9f75a571bd66cf8.tar.zst
VIATRA-Generator-acb8dedc9d03e1d17f570e07c9f75a571bd66cf8.zip
Ready for strategies case study
Diffstat (limited to 'Solvers')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend15
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend15
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend6
4 files changed, 35 insertions, 3 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
index 62ff92b2..9835356e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
@@ -10,6 +10,8 @@ import org.eclipse.xtext.xbase.XNumberLiteral
10import org.eclipse.xtext.xbase.XUnaryOperation 10import org.eclipse.xtext.xbase.XUnaryOperation
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference 11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference 12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
13import org.eclipse.xtext.xbase.XIfExpression
14import org.eclipse.xtext.xbase.XBlockExpression
13 15
14class PExpressionGenerator { 16class PExpressionGenerator {
15 static val N_Base = "org.eclipse.xtext.xbase.lib." 17 static val N_Base = "org.eclipse.xtext.xbase.lib."
@@ -113,4 +115,17 @@ class PExpressionGenerator {
113 def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) { 115 def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
114 throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''') 116 throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''')
115 } 117 }
118
119 def dispatch CharSequence translateExpression(XIfExpression e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
120 val i = e.^if.translateExpression(valueName,variable2Type)
121 val t = e.then.translateExpression(valueName,variable2Type)
122 val el = e.^else.translateExpression(valueName,variable2Type)
123
124 return '''(if(«i»){«t»}else{«el»})'''
125 }
126
127 def dispatch CharSequence translateExpression(XBlockExpression e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
128 //Assuming 1-item blocks only
129 return (e as XBlockExpression).expressions.get(0).translateExpression(valueName,variable2Type)
130 }
116} \ No newline at end of file 131} \ 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/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index 5ad78506..a692e1e5 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
@@ -110,7 +110,7 @@ class ViatraReasoner extends LogicReasoner {
110 new SolutionStore(numberOfRequiredSolutions) 110 new SolutionStore(numberOfRequiredSolutions)
111 } 111 }
112 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) 112 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))
113 val numericSolver = new NumericSolver(method, viatraConfig, true)//was formerly hard-coded to false for caching 113 val numericSolver = new NumericSolver(method, viatraConfig, false)//was formerly hard-coded to false for caching
114 val solutionSaver = method.solutionSaver 114 val solutionSaver = method.solutionSaver
115 solutionSaver.numericSolver = numericSolver 115 solutionSaver.numericSolver = numericSolver
116 val solutionCopier = solutionSaver.solutionCopier 116 val solutionCopier = solutionSaver.solutionCopier
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 44964079..28edff41 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
@@ -24,10 +24,12 @@ import java.util.List
24import java.util.Map 24import java.util.Map
25import org.eclipse.emf.ecore.EObject 25import org.eclipse.emf.ecore.EObject
26import org.eclipse.viatra.dse.base.ThreadContext 26import org.eclipse.viatra.dse.base.ThreadContext
27import org.eclipse.viatra.dse.objectives.Fitness
27import org.eclipse.viatra.query.runtime.api.IPatternMatch 28import org.eclipse.viatra.query.runtime.api.IPatternMatch
28import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 29import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
29import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint 30import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
30import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation 31import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
32import org.eclipse.viatra.dse.objectives.IObjective
31 33
32class NumericSolver { 34class NumericSolver {
33 val ModelGenerationMethod method 35 val ModelGenerationMethod method
@@ -206,7 +208,6 @@ class NumericSolver {
206 } 208 }
207 } else { 209 } else {
208 if (needsFilling){ 210 if (needsFilling){
209 //TODO ASSUME Always True
210 //GET LIST OF VARS TO FILL 211 //GET LIST OF VARS TO FILL
211 val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) 212 val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase))
212 if (fillMap === null) finalResult = false 213 if (fillMap === null) finalResult = false
@@ -225,7 +226,9 @@ class NumericSolver {
225 //STRATEGY 226 //STRATEGY
226 if (phase == 2) { 227 if (phase == 2) {
227 if (!finalResult) return finalResult 228 if (!finalResult) return finalResult
228 else finalResult = isSatisfiable(matches, 3) 229 else {
230 finalResult = isSatisfiable(matches, 3)
231 }
229 } 232 }
230 return finalResult 233 return finalResult
231 } 234 }
@@ -243,6 +246,14 @@ class NumericSolver {
243 // -1 : take all numeric constraints 246 // -1 : take all numeric constraints
244 // -2 : SKIP (take no numeric constraints) 247 // -2 : SKIP (take no numeric constraints)
245 if (strategy == ExplorationStrategy.CrossingScenario) { 248 if (strategy == ExplorationStrategy.CrossingScenario) {
249// //if has structural (non-WF) fitness issues, skip numeric handling
250// val IObjective ob = threadContext.objectives.filter[it instanceof ModelGenerationCompositeObjective].get(0)
251// val compo = ob as ModelGenerationCompositeObjective
252// if (compo.getNonWFFitness(threadContext) > 0) {
253// println("bootleg numeric-skip")
254// return -2;
255// }
256
246 //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors 257 //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors
247 val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; 258 val PartialInterpretation head = threadContext.getModel() as PartialInterpretation;
248 val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation(); 259 val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation();
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
index 1b61ffa5..b5b44254 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
@@ -37,6 +37,12 @@ class UnfinishedWFObjective implements IObjective {
37 override getComparator() { Comparators.LOWER_IS_BETTER } 37 override getComparator() { Comparators.LOWER_IS_BETTER }
38 38
39 override getFitness(ThreadContext context) { 39 override getFitness(ThreadContext context) {
40// //MEGA ASSUMPTION Below TODO
41// //if has no unfilled variables, return 0
42// val model = context.getModel as PartialInterpretation
43// val unfilledDataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].filter[!it.isValueSet].toList
44// if (unfilledDataObjects.isEmpty) return 0.0
45
40 var sumOfMatches = 0 46 var sumOfMatches = 0
41 for (matcher : matchers) { 47 for (matcher : matchers) {
42 val number = matcher.countMatches 48 val number = matcher.countMatches