From a8eb346fb97b54b6ee693da4840abd8be8b43843 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Sun, 14 Feb 2021 08:01:00 +0100 Subject: Add strategy flag + implement alost working crossingScenarioStrategy --- .../application/execution/SolverLoader.xtend | 16 +- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 2 +- .../viatra2logic/NumericDrealProblemSolver.java | 46 ++- .../viatra2logic/NumericDynamicProblemSolver.java | 41 +++ .../viatra2logic/NumericTranslator.xtend | 19 +- .../patterns/RelationDefinitionIndexer.xtend | 15 + .../reasoner/ViatraReasonerConfiguration.xtend | 7 + .../viatrasolver/reasoner/dse/NumericSolver.xtend | 319 +++++++++++++++++++-- 8 files changed, 416 insertions(+), 49 deletions(-) create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend index da8ca0eb..045387a0 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend @@ -1,5 +1,6 @@ package hu.bme.mit.inf.dslreasoner.application.execution +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CostObjectiveFunction @@ -16,6 +17,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePro import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.PunishSizeStrategy import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration @@ -28,9 +31,6 @@ import java.util.Optional import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel import org.eclipse.xtext.EcoreUtil2 import org.eclipse.xtext.xbase.lib.Functions.Function1 -import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection -import java.util.HashMap class SolverLoader { def loadSolver(Solver solver, Map config) { @@ -171,6 +171,16 @@ class SolverLoader { val stringValue = config.get("ignored-attributes") c.ignoredAttributesMap = parseIgnoredAttributes(stringValue) } + if (config.containsKey("strategy")) { + val stringValue = config.get("strategy") + c.strategy = switch (stringValue) { + case "none": ExplorationStrategy.None + case "crossingScenario": ExplorationStrategy.CrossingScenario + case "cs-hacker": ExplorationStrategy.CSHacker + default: throw new IllegalArgumentException("Unknown strategy: " + stringValue) + } + } + for (objectiveEntry : objectiveEntries) { val costObjectiveConfig = new CostObjectiveConfiguration switch (objectiveEntry) { diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend index 9e11d2cf..ae94c327 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend @@ -21,7 +21,7 @@ class ExpressionEvaluation2Logic { def getNumericSolver() { if(_numericSolver === null) { // it seems like this getter has no use - _numericSolver = (new NumericTranslator(null)).selectProblemSolver + _numericSolver = (new NumericTranslator(null)).selectProblemSolver("z3") } return _numericSolver } 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 e0ebcb6b..36ea64aa 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,8 +43,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ private Map curVar2Decl; private final int TIMEOUT_DOCKER = 5000; - private final int TIMEOUT_LOCAL = 10000; - private final boolean DEBUG_PRINT = false; + private final int TIMEOUT_LOCAL = 100000; + private final int DEBUG_PRINT = 3; public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { this.useDocker = useDocker; @@ -87,7 +87,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ } return null; } - if (DEBUG_PRINT) { + if (DEBUG_PRINT > 1) { double duration = (double) (System.nanoTime() - startTime) / 1000000000; System.out.println("Dur = " + duration + " : "); } @@ -404,11 +404,13 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ System.err.println("TIMEOUT"); // printOutput(numProbContent); } - if (DEBUG_PRINT) { - // printOutput(numProbContent); - // if (outputs != null) printOutput(outputs.get(0)); + if (DEBUG_PRINT > 1) { System.out.println(result); } + if (DEBUG_PRINT > 2) { + printOutput(numProbContent); + if (outputs != null) printOutput(outputs.get(0)); + } return result; } @@ -455,16 +457,30 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ Process outputProcess; if (this.useDocker) outputProcess = callDrealDocker(numProbContent, true); else outputProcess = callDrealLocal(numProbContent, true); - - List> outputs = getProcessOutput(outputProcess); - boolean result = getDrealResult(outputProcess.exitValue(), outputs); + + boolean result = false; + List> outputs = null; + if (outputProcess != null) { + outputs = getProcessOutput(outputProcess); + result = getDrealResult(outputProcess.exitValue(), outputs); + } + endSolvingProblem = System.nanoTime()-startSolvingProblem; - if (DEBUG_PRINT) { - System.out.println("Getting Solution!"); - // printOutput(numProbContent); - // printOutput(outputs.get(0)); - // System.out.println(result); + if (outputProcess == null) { + System.err.println("TIMEOUT"); +// printOutput(numProbContent); + } else { + if (DEBUG_PRINT > 0) { + System.out.println("Getting Solution!"); + } + } + if (DEBUG_PRINT > 1) { + System.out.println(result); + } + if (DEBUG_PRINT > 2) { + printOutput(numProbContent); + if (outputs != null) printOutput(outputs.get(0)); } //GET SOLUTION @@ -498,7 +514,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ endFormingSolution = System.nanoTime() - startFormingSolution; } else { - System.out.println("Unsatisfiable numerical problem"); + System.out.println("Unsatisfiable numerical problem (trying to get solution...)"); } return sol; } diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java new file mode 100644 index 00000000..bd4a10ff --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java @@ -0,0 +1,41 @@ +package hu.bme.mit.inf.dslreasoner.viatra2logic; + +import java.io.IOException; +import java.util.List; +import java.util.Map; + +import org.eclipse.xtext.common.types.JvmIdentifiableElement; +import org.eclipse.xtext.xbase.XExpression; + +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; + +public class NumericDynamicProblemSolver extends NumericProblemSolver{ + +// private NumericZ3ProblemSolver z3Solver; + private NumericDrealProblemSolver drealSolver; + + public NumericDynamicProblemSolver(String drealLocalPath) throws IOException, InterruptedException { +// this.z3Solver = new NumericZ3ProblemSolver(); + this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath); + } + + public NumericProblemSolver selectSolver(String selection) { + switch (selection) { + case "z3": + return new NumericZ3ProblemSolver(); + case "dreal": + return this.drealSolver; + default: + throw new IllegalArgumentException("Unknown numeric solver selection: " + selection); + } + } + + public boolean isSatisfiable(Map>> matches) + throws Exception { + throw new Exception("Should not reach here - isSatisfiable"); + } + + public Map getOneSolution(List objs, + Map>> matches) throws Exception { + throw new Exception("Should not reach here - getOneSolution"); + }} diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend index 3d3f2f4a..791dd644 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend @@ -56,24 +56,29 @@ class NumericTranslator { return res } - def NumericProblemSolver selectProblemSolver() { + def NumericProblemSolver selectProblemSolver(String selection) { // return new NumericProblemSolver // add numeric solver decision procedure here - if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver - return numericSolver; + if (numericSolver instanceof NumericDynamicProblemSolver) { + val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver + return dynamicSolver.selectSolver(selection); + } else{ + if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver + return numericSolver; + } } - def delegateIsSatisfiable(Map> matches) { + def delegateIsSatisfiable(Map> matches, String select) { val input = formNumericProblemInstance(matches) - val solver = selectProblemSolver + val solver = selectProblemSolver(select) val satisfiability = solver.isSatisfiable(input) solver.updateTimes return satisfiability } - def delegateGetSolution(List primitiveElements, Map> matches) { + def delegateGetSolution(List primitiveElements, Map> matches, String select) { val input = formNumericProblemInstance(matches) - val solver = selectProblemSolver + val solver = selectProblemSolver(select) val solution = solver.getOneSolution(primitiveElements,input) solver.updateTimes return solution diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend index 338a9af2..0c9612e8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend @@ -11,6 +11,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation class RelationDefinitionIndexer { public val PatternGenerator base; @@ -70,6 +71,19 @@ class RelationDefinitionIndexer { private def transformPattern(RelationDefinition relation, PQuery p, Modality modality) { try { val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies + + //TODO ISSUE if a structural and numeric constraint are ORed in the same pattern + var boolean isCheck = false + for (body : bodies) { + for (constraint : body.constraints) { + if (constraint instanceof ExpressionEvaluation) { + // below not working +// return "" + isCheck = true + } + } + } + return ''' private pattern «relationDefinitionName(relation,modality)»( problem:LogicProblem, interpretation:PartialInterpretation, @@ -79,6 +93,7 @@ class RelationDefinitionIndexer { «FOR constraint : body.constraints» «this.constraintTransformer.transformConstraint(constraint,modality,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» «ENDFOR» + «IF isCheck»1 == 0;«ENDIF» }«ENDFOR» ''' } catch(UnsupportedOperationException e) { 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 61a2ac41..74388706 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 @@ -40,6 +40,12 @@ enum NumericSolverSelection { Z3 } +enum ExplorationStrategy { + None, + CrossingScenario, + CSHacker +} + class ViatraReasonerConfiguration extends LogicSolverConfiguration { // public var Iterable existingQueries public var nameNewElements = false @@ -80,6 +86,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3 public var drealLocalPath = ""; public var Map> ignoredAttributesMap = null; + public var ExplorationStrategy strategy = ExplorationStrategy.None public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) 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 b8ea25e5..b8fcb6a0 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 @@ -1,14 +1,19 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver +import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDynamicProblemSolver import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration @@ -22,6 +27,7 @@ import org.eclipse.viatra.dse.base.ThreadContext 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 class NumericSolver { val ModelGenerationMethod method @@ -34,6 +40,7 @@ class NumericSolver { val boolean caching; Map>>,Boolean> satisfiabilityCache = new HashMap val String drealLocalPath; + val ExplorationStrategy strategy; var long runtime = 0 var long cachingTime = 0 @@ -45,24 +52,43 @@ class NumericSolver { this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks this.caching = caching this.drealLocalPath = config.drealLocalPath - this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) + this.strategy = config.strategy + this.t = new NumericTranslator(createNumericTranslator(config)) } - def createNumericTranslator(NumericSolverSelection solverSelection) { - if (solverSelection == NumericSolverSelection.DREAL_DOCKER) - return new NumericDrealProblemSolver(true, null) - if (solverSelection == NumericSolverSelection.DREAL_LOCAL) - return new NumericDrealProblemSolver(false, drealLocalPath) - if (solverSelection == NumericSolverSelection.Z3) { + def createNumericTranslator(ViatraReasonerConfiguration config) { + val solverSelection = config.numericSolverSelection + val strategy = config.strategy + if (strategy == ExplorationStrategy.None) { + //initialise the specified + if (solverSelection == NumericSolverSelection.DREAL_DOCKER) + return new NumericDrealProblemSolver(true, null) + if (solverSelection == NumericSolverSelection.DREAL_LOCAL) + return new NumericDrealProblemSolver(false, drealLocalPath) + if (solverSelection == NumericSolverSelection.Z3) { + //TODO THIS IS HARD-CODED for now +// val root = "/data/viatra/VIATRA-Generator"; + val root = "/home/models/VIATRA-Generator"; + //END HARD-CODED + // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); + System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); + System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); + // System.load("libz3.so"); + // System.load("libz3java.so"); + return new NumericZ3ProblemSolver + } + } + else { + //initialise both dreal-local and z3 + //TODO THIS IS HARD-CODED for now - val root = "/data/viatra/VIATRA-Generator"; +// val root = "/data/viatra/VIATRA-Generator"; + val root = "/home/models/VIATRA-Generator"; //END HARD-CODED // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); -// System.load("libz3.so"); -// System.load("libz3java.so"); - return new NumericZ3ProblemSolver + return new NumericDynamicProblemSolver(drealLocalPath) } } @@ -95,31 +121,49 @@ class NumericSolver { def getNumericSolverSelection(){this.t.numericSolver} def boolean maySatisfiable() { + val int phase = determinePhase() + if(intermediateConsistencyCheck) { - return isSatisfiable(this.constraint2MustUnitPropagationPrecondition) + return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase) } else { return true } } def boolean currentSatisfiable() { - isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition) + val int phase = determinePhase() + //TODO generalize this + isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) } - private def boolean isSatisfiable(Map> matches) { + private def boolean isSatisfiable(Map> matches, int phase) { val start = System.nanoTime var boolean finalResult + val boolean needsFilling = needsFilling + val model = threadContext.getModel as PartialInterpretation + val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList + if(matches.empty){ finalResult=true } else { val propagatedConstraints = new HashMap -// println("<<<>>>") + //Filter constraints if there are phase-related restricutions + //null whitelist means accept everything + val whitelist = getConstraintWhitelist(phase) + println("<<<>>> (" + phase + ")") for(entry : matches.entrySet) { - val constraint = entry.key -// println("--match?-- " + constraint) - val allMatches = entry.value.allMatches.map[it.toArray] -// println("---------- " + entry.value.allMatches) - propagatedConstraints.put(constraint,allMatches) + if (entry.value !== null){ + val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName + if (whitelist === null || whitelist.contains(name)) { +// println(name) + val constraint = entry.key +// println("--match?-- " + constraint) + val allMatches = entry.value.allMatches.map[it.toArray] + // println("---------- " + entry.value.allMatches) + propagatedConstraints.put(constraint,allMatches) + } + } } + //check numeric problem if(propagatedConstraints.values.forall[empty]) { finalResult=true } else { @@ -133,16 +177,35 @@ class NumericSolver { // } //println(code.hashCode) this.numberOfSolverCalls++ - val res = t.delegateIsSatisfiable(propagatedConstraints) + var boolean res = false + if (needsFilling){ + //TODO ASSUME Always True + //GET LIST OF VARS TO FILL + val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) + fillWithPartialSolutionsDirectly(dataObjects, fillMap) + res = true + } else { + res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) + } + //TODO FIX CACHING satisfiabilityCache.put(code,res) finalResult=res } else { //println('''similar problem, answer from cache''') + println('''potential issue, answer from cache''') finalResult=cachedResult this.numberOfCachedSolverCalls++ } } else { - finalResult= t.delegateIsSatisfiable(propagatedConstraints) + if (needsFilling){ + //TODO ASSUME Always True + //GET LIST OF VARS TO FILL + val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) + fillWithPartialSolutionsDirectly(dataObjects, fillMap) + finalResult = true + } else { + finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) + } this.numberOfSolverCalls++ } } @@ -151,6 +214,201 @@ class NumericSolver { return finalResult } + def selectSolver(int phase) { + if (strategy === ExplorationStrategy.CrossingScenario){ + if (phase == 1) return "dreal" + else return "dreal" + } + return "irrelevant" + } + + def int determinePhase() { + // >= 0 : an actual phase + // -1 : take all numeric constraints + // -2 : SKIP (take no numeric constraints) + if (strategy == ExplorationStrategy.CrossingScenario) { + //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors + val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; + val List relations = head.getPartialrelationinterpretation(); + var boolean foundActorWithDefinedPos = false; + for (PartialRelationInterpretation rel : relations) { + if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) { + for (RelationLink link : rel.getRelationlinks()) { + val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement; + if (param2.isValueSet()) { + foundActorWithDefinedPos = true; + } + } + } + + if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { + if (!rel.getRelationlinks().isEmpty()) { + return 3; + } + } + } + //it means that there is no blockedBy + //so we are at most at phase 2 + if (foundActorWithDefinedPos) return 2; + return 1; + } + return -1; + } + + def getConstraintWhitelist(int phase) { + val List wl = newArrayList + //null return means accept everything + if (strategy === ExplorationStrategy.None){ + return null + } else if (strategy === ExplorationStrategy.CrossingScenario){ + /* + "define_placedOn_actorOnVerticalLane", + "define_placedOn_actorOnHorizLane", + + "define_actor_maxXp", + "define_actor_minXp", + "define_actor_maxYp", + "define_actor_minYp", + + "define_actor_wrtLane", + + "define_actor_minimumDistance", + + "define_actor_actorOnVertLaneHasxSpeed0", + "define_actor_actorOnVertLaneMinYs", + "define_actor_actorOnVertLaneMaxYs", + "define_actor_actorOnHorizLaneHasySpeed0", + "define_actor_actorOnHorizLaneMinXs", + "define_actor_actorOnHorizLaneMaxXs", + + "define_actor_pedestrianWidth", + "define_actor_pedestrianLength", + "define_actor_vehicleWidth", + "define_actor_vehicleWidth", + "define_actor_vehicleLength", + "define_actor_vehicleLength", + + "collisionExists_timeWithinBound", + "collisionExists_timeNotNegative", + "collisionExists_defineCollision_y1", + "collisionExists_defineCollision_y2", + "collisionExists_defineCollision_x1", + "collisionExists_defineCollision_x2", + + "visionBlocked_ites_notOnSameVertLine", + "visionBlocked_ites_top", + "visionBlocked_ites_bottom", + "visionBlocked_xdistBSlargerThanxdistTS", + "visionBlocked_xdistBTlargerThanxdistST", + "visionBlocked_ydistBSlargerThanydistTS", + "visionBlocked_ydistBTlargerThanydistST" + */ + + //HINTS: + //define_actor_wrtLane + //28.5 is structural hint + switch (phase) { + case 1: { + wl.addAll(#[ + "define_placedOn_actorOnVerticalLane", + "define_placedOn_actorOnHorizLane", + + "define_actor_maxXp", + "define_actor_minXp", + "define_actor_maxYp", + "define_actor_minYp", + + "define_actor_pedestrianWidth", + "define_actor_pedestrianLength", + "define_actor_vehicleWidth", + "define_actor_vehicleWidth", + "define_actor_vehicleLength", + "define_actor_vehicleLength" + + ]) + } + case 2: { + wl.addAll(#[ + + "define_placedOn_actorOnVerticalLane", + "define_placedOn_actorOnHorizLane", + + "define_actor_maxXp", + "define_actor_minXp", + "define_actor_maxYp", + "define_actor_minYp", + + "define_actor_minimumDistance", + + "define_actor_pedestrianWidth", + "define_actor_pedestrianLength", + "define_actor_vehicleWidth", + "define_actor_vehicleWidth", + "define_actor_vehicleLength", + "define_actor_vehicleLength", + + "visionBlocked_ites_notOnSameVertLine", + "visionBlocked_ites_top", + "visionBlocked_ites_bottom", + "visionBlocked_xdistBSlargerThanxdistTS", + "visionBlocked_xdistBTlargerThanxdistST", + "visionBlocked_ydistBSlargerThanydistTS", + "visionBlocked_ydistBTlargerThanydistST" + ]) + } + case 3: { + wl.addAll(#[ + + "define_placedOn_actorOnVerticalLane", + "define_placedOn_actorOnHorizLane", + + "define_actor_maxXp", + "define_actor_minXp", + "define_actor_maxYp", + "define_actor_minYp", + + "define_actor_minimumDistance", + + "define_actor_actorOnVertLaneHasxSpeed0", + "define_actor_actorOnVertLaneMinYs", + "define_actor_actorOnVertLaneMaxYs", + "define_actor_actorOnHorizLaneHasySpeed0", + "define_actor_actorOnHorizLaneMinXs", + "define_actor_actorOnHorizLaneMaxXs", + + "define_actor_pedestrianWidth", + "define_actor_pedestrianLength", + "define_actor_vehicleWidth", + "define_actor_vehicleWidth", + "define_actor_vehicleLength", + "define_actor_vehicleLength", + + "collisionExists_timeWithinBound", + "collisionExists_timeNotNegative", + "collisionExists_defineCollision_y1", + "collisionExists_defineCollision_y2", + "collisionExists_defineCollision_x1", + "collisionExists_defineCollision_x2" + ]) + } + default: { + //this is for 3 if we implement 4 +// bl.addAll(#[0, 1, 2, 3, 4, 5, 6, 7]) + + //this is for 4 if we do it + wl.addAll(#[]) + return null + } + } + } + return wl + } + + def getNeedsFilling(){ + if (strategy == ExplorationStrategy.CrossingScenario) return true + return false + } + def getCode(HashMap> propagatedConstraints) { val start = System.nanoTime val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList @@ -175,7 +433,7 @@ class NumericSolver { if(propagatedConstraints.values.forall[empty]) { fillWithDefaultValues(dataObjects,trace) } else { - val solution = t.delegateGetSolution(dataObjects,propagatedConstraints) + val solution = t.delegateGetSolution(dataObjects,propagatedConstraints, "dreal") fillWithSolutions(dataObjects,solution,trace) } } @@ -215,4 +473,19 @@ class NumericSolver { def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double } def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} + + def protected fillWithPartialSolutionsDirectly(List elements, Map solution) { + for(element : elements) { + //we allow overwriting of already set variables + if(solution.containsKey(element)) { + val value = solution.get(element) + if (value !== null){ + element.fillWithValue(value) + println("<" + element + "> is filled") + } else { + println("<" + element + "> is unfilled") + } + } + } + } } \ No newline at end of file -- cgit v1.2.3-54-g00ecf