From acb8dedc9d03e1d17f570e07c9f75a571bd66cf8 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 16 Feb 2021 01:11:15 +0100 Subject: Ready for strategies case study --- .../viatra2logic/NumericDrealProblemSolver.java | 8 +++++--- .../logic2viatra/patterns/PExpressionGenerator.xtend | 15 +++++++++++++++ .../viatrasolver/reasoner/ViatraReasoner.xtend | 2 +- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 15 +++++++++++++-- .../viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend | 6 ++++++ 5 files changed, 40 insertions(+), 6 deletions(-) diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java index 70aa933a..f098d575 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java @@ -43,7 +43,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ private Map curVar2Decl; private final int TIMEOUT_DOCKER = 5000; - private final int TIMEOUT_LOCAL = 100000; + private final int TIMEOUT_LOCAL = -1; private final int DEBUG_PRINT = 3; public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { @@ -75,7 +75,9 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ // p.waitFor(); //TODO timeout if needed long startTime = System.nanoTime(); - if (!p.waitFor(timeout, TimeUnit.MILLISECONDS)) { + if (timeout == -1) { + p.waitFor(); + } else if (!p.waitFor(timeout, TimeUnit.MILLISECONDS)) { p.destroy(); if (p.isAlive()) { p.destroyForcibly(); @@ -406,6 +408,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ //CREATE DREAL STM2 FILE CONTENTS long startformingProblem = System.nanoTime(); List numProbContent = formNumericProblemInstance(matches); + if (DEBUG_PRINT > 2) printOutput(numProbContent); endformingProblem = System.nanoTime()-startformingProblem; if (numProbContent == null) { @@ -446,7 +449,6 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ System.out.println(result); } if (DEBUG_PRINT > 2) { - printOutput(numProbContent); if (outputs != null) printOutput(outputs.get(0)); } 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 import org.eclipse.xtext.xbase.XUnaryOperation import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference +import org.eclipse.xtext.xbase.XIfExpression +import org.eclipse.xtext.xbase.XBlockExpression class PExpressionGenerator { static val N_Base = "org.eclipse.xtext.xbase.lib." @@ -113,4 +115,17 @@ class PExpressionGenerator { def dispatch CharSequence translateExpression(XExpression expression, Map valueName, Map variable2Type) { throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''') } + + def dispatch CharSequence translateExpression(XIfExpression e, Map valueName, Map variable2Type) { + val i = e.^if.translateExpression(valueName,variable2Type) + val t = e.then.translateExpression(valueName,variable2Type) + val el = e.^else.translateExpression(valueName,variable2Type) + + return '''(if(«i»){«t»}else{«el»})''' + } + + def dispatch CharSequence translateExpression(XBlockExpression e, Map valueName, Map variable2Type) { + //Assuming 1-item blocks only + return (e as XBlockExpression).expressions.get(0).translateExpression(valueName,variable2Type) + } } \ 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 { new SolutionStore(numberOfRequiredSolutions) } solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) - val numericSolver = new NumericSolver(method, viatraConfig, true)//was formerly hard-coded to false for caching + val numericSolver = new NumericSolver(method, viatraConfig, false)//was formerly hard-coded to false for caching val solutionSaver = method.solutionSaver solutionSaver.numericSolver = numericSolver 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 import java.util.Map import org.eclipse.emf.ecore.EObject import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.viatra.dse.objectives.Fitness import org.eclipse.viatra.query.runtime.api.IPatternMatch import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation +import org.eclipse.viatra.dse.objectives.IObjective class NumericSolver { val ModelGenerationMethod method @@ -206,7 +208,6 @@ class NumericSolver { } } else { if (needsFilling){ - //TODO ASSUME Always True //GET LIST OF VARS TO FILL val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) if (fillMap === null) finalResult = false @@ -225,7 +226,9 @@ class NumericSolver { //STRATEGY if (phase == 2) { if (!finalResult) return finalResult - else finalResult = isSatisfiable(matches, 3) + else { + finalResult = isSatisfiable(matches, 3) + } } return finalResult } @@ -243,6 +246,14 @@ class NumericSolver { // -1 : take all numeric constraints // -2 : SKIP (take no numeric constraints) if (strategy == ExplorationStrategy.CrossingScenario) { +// //if has structural (non-WF) fitness issues, skip numeric handling +// val IObjective ob = threadContext.objectives.filter[it instanceof ModelGenerationCompositeObjective].get(0) +// val compo = ob as ModelGenerationCompositeObjective +// if (compo.getNonWFFitness(threadContext) > 0) { +// println("bootleg numeric-skip") +// return -2; +// } + //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; val List 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 { override getComparator() { Comparators.LOWER_IS_BETTER } override getFitness(ThreadContext context) { +// //MEGA ASSUMPTION Below TODO +// //if has no unfilled variables, return 0 +// val model = context.getModel as PartialInterpretation +// val unfilledDataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].filter[!it.isValueSet].toList +// if (unfilledDataObjects.isEmpty) return 0.0 + var sumOfMatches = 0 for (matcher : matchers) { val number = matcher.countMatches -- cgit v1.2.3-54-g00ecf