diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit')
7 files changed, 539 insertions, 540 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 a692e1e5..98d07069 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 | |||
@@ -22,7 +22,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyFor | |||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint | 22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint |
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler | 23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler |
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective | 24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective |
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.NumericSolver | ||
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation | 25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation |
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective | 26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective |
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective | 27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective |
@@ -39,6 +38,7 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel | |||
39 | import org.eclipse.viatra.dse.solutionstore.SolutionStore | 38 | import org.eclipse.viatra.dse.solutionstore.SolutionStore |
40 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory | 39 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory |
41 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver | 40 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver |
41 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.NumericRefinementUnit | ||
42 | 42 | ||
43 | class ViatraReasoner extends LogicReasoner { | 43 | class ViatraReasoner extends LogicReasoner { |
44 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() | 44 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() |
@@ -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, false)//was formerly hard-coded to false for caching | 113 | val numericSolver = new NumericRefinementUnit(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 |
@@ -156,7 +156,7 @@ class ViatraReasoner extends LogicReasoner { | |||
156 | val transformationTime = transformationFinished - transformationStartTime | 156 | val transformationTime = transformationFinished - transformationStartTime |
157 | val solverStartTime = System.nanoTime | 157 | val solverStartTime = System.nanoTime |
158 | 158 | ||
159 | println(">>begin exploration") | 159 | //println(">>begin exploration") |
160 | var boolean stoppedByTimeout | 160 | var boolean stoppedByTimeout |
161 | try { | 161 | try { |
162 | stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000); | 162 | stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000); |
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 923c847e..fc1fadf7 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 | |||
@@ -84,8 +84,9 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
84 | public var unfinishedWFWeight = 1 | 84 | public var unfinishedWFWeight = 1 |
85 | public var calculateObjectCreationCosts = false | 85 | public var calculateObjectCreationCosts = false |
86 | public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3 | 86 | public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3 |
87 | public var NumericSolverPath = "<path-to-numeric-solver>" | ||
87 | public var drealLocalPath = "<path-to-dreal>"; | 88 | public var drealLocalPath = "<path-to-dreal>"; |
88 | public var drealTimeout = 10000; | 89 | public var numericSolverTimeout = 10000; |
89 | public var Map<String, Map<String, String>> ignoredAttributesMap = null; | 90 | public var Map<String, Map<String, String>> ignoredAttributesMap = null; |
90 | public var ExplorationStrategy strategy = ExplorationStrategy.None | 91 | public var ExplorationStrategy strategy = ExplorationStrategy.None |
91 | 92 | ||
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 c62d124a..1ac12914 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 | |||
@@ -79,7 +79,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
79 | // private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; | 79 | // private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; |
80 | public ActivationSelector activationSelector = new EvenActivationSelector(random); | 80 | public ActivationSelector activationSelector = new EvenActivationSelector(random); |
81 | public ViatraReasonerSolutionSaver solutionSaver; | 81 | public ViatraReasonerSolutionSaver solutionSaver; |
82 | public NumericSolver numericSolver; | 82 | public NumericRefinementUnit numericSolver; |
83 | // Statistics | 83 | // Statistics |
84 | private int numberOfStatecoderFail = 0; | 84 | private int numberOfStatecoderFail = 0; |
85 | private int numberOfPrintedModel = 0; | 85 | private int numberOfPrintedModel = 0; |
@@ -94,7 +94,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
94 | ViatraReasonerConfiguration configuration, | 94 | ViatraReasonerConfiguration configuration, |
95 | ModelGenerationMethod method, | 95 | ModelGenerationMethod method, |
96 | ViatraReasonerSolutionSaver solutionSaver, | 96 | ViatraReasonerSolutionSaver solutionSaver, |
97 | NumericSolver numericSolver) { | 97 | NumericRefinementUnit numericSolver) { |
98 | this.workspace = workspace; | 98 | this.workspace = workspace; |
99 | this.configuration = configuration; | 99 | this.configuration = configuration; |
100 | this.method = method; | 100 | this.method = method; |
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/NumericRefinementUnit.xtend index a228afc6..b3e2d78d 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/NumericRefinementUnit.xtend | |||
@@ -1,533 +1,531 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver | 3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver |
4 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDynamicProblemSolver | 4 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator |
5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | 5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver |
6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink | 14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement |
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy |
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod |
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection | 18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration |
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | 19 | import java.util.HashMap |
20 | import java.util.HashMap | 20 | import java.util.LinkedHashMap |
21 | import java.util.LinkedHashMap | 21 | import java.util.LinkedHashSet |
22 | import java.util.LinkedHashSet | 22 | import java.util.List |
23 | import java.util.List | 23 | import java.util.Map |
24 | import java.util.Map | 24 | import org.eclipse.emf.ecore.EObject |
25 | import org.eclipse.emf.ecore.EObject | 25 | import org.eclipse.viatra.dse.base.ThreadContext |
26 | import org.eclipse.viatra.dse.base.ThreadContext | 26 | import org.eclipse.viatra.dse.objectives.Fitness |
27 | import org.eclipse.viatra.dse.objectives.Fitness | 27 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
28 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 28 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
29 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 29 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint |
30 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | 30 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation |
31 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | 31 | import org.eclipse.viatra.dse.objectives.IObjective |
32 | import org.eclipse.viatra.dse.objectives.IObjective | 32 | |
33 | 33 | class NumericRefinementUnit { | |
34 | class NumericSolver { | 34 | val ModelGenerationMethod method |
35 | val ModelGenerationMethod method | 35 | var ThreadContext threadContext |
36 | var ThreadContext threadContext | 36 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
37 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 37 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
38 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 38 | var NumericTranslator translator = null; |
39 | NumericTranslator t | 39 | |
40 | 40 | ||
41 | val boolean intermediateConsistencyCheck | 41 | val boolean intermediateConsistencyCheck |
42 | val boolean caching; | 42 | val boolean caching; |
43 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap | 43 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap |
44 | val String drealLocalPath; | 44 | val ExplorationStrategy strategy; |
45 | val ExplorationStrategy strategy; | 45 | |
46 | 46 | var long runtime = 0 | |
47 | var long runtime = 0 | 47 | var long cachingTime = 0 |
48 | var long cachingTime = 0 | 48 | var int numberOfSolverCalls = 0 |
49 | var int numberOfSolverCalls = 0 | 49 | var int numberOfCachedSolverCalls = 0 |
50 | var int numberOfCachedSolverCalls = 0 | 50 | |
51 | 51 | new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { | |
52 | new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { | 52 | this.method = method |
53 | this.method = method | 53 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks |
54 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks | 54 | this.caching = caching |
55 | this.caching = caching | 55 | this.strategy = config.strategy |
56 | this.drealLocalPath = config.drealLocalPath | 56 | this.translator = new NumericTranslator(createNumericTranslator(config),config.numericSolverTimeout) |
57 | this.strategy = config.strategy | 57 | } |
58 | this.t = new NumericTranslator(createNumericTranslator(config), config.drealTimeout) | 58 | |
59 | } | 59 | def createNumericTranslator(ViatraReasonerConfiguration config) { |
60 | 60 | val solverSelection = config.numericSolverSelection | |
61 | def createNumericTranslator(ViatraReasonerConfiguration config) { | 61 | val strategy = config.strategy |
62 | val solverSelection = config.numericSolverSelection | 62 | // if (strategy == ExplorationStrategy.None) { |
63 | val strategy = config.strategy | 63 | // initialise the specified |
64 | if (strategy == ExplorationStrategy.None) { | 64 | if (solverSelection == NumericSolverSelection.DREAL_DOCKER) |
65 | //initialise the specified | 65 | return new NumericDrealProblemSolver(true, null, config.numericSolverTimeout) |
66 | if (solverSelection == NumericSolverSelection.DREAL_DOCKER) | 66 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) |
67 | return new NumericDrealProblemSolver(true, null, config.drealTimeout) | 67 | return new NumericDrealProblemSolver(false, config.drealLocalPath, config.numericSolverTimeout) |
68 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) | 68 | if (solverSelection == NumericSolverSelection.Z3) { |
69 | return new NumericDrealProblemSolver(false, drealLocalPath, config.drealTimeout) | 69 | // TODO THIS IS HARD-CODED for now |
70 | if (solverSelection == NumericSolverSelection.Z3) { | 70 | // val root = "/data/viatra/VIATRA-Generator"; |
71 | //TODO THIS IS HARD-CODED for now | 71 | // val root = "/home/models/VIATRA-Generator"; |
72 | // val root = "/data/viatra/VIATRA-Generator"; | 72 | // END HARD-CODED |
73 | val root = "/home/models/VIATRA-Generator"; | 73 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); |
74 | //END HARD-CODED | 74 | // System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); |
75 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); | 75 | // System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); |
76 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); | 76 | // System.load("libz3.so"); |
77 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | 77 | // System.load("libz3java.so"); |
78 | // System.load("libz3.so"); | 78 | return new NumericZ3ProblemSolver(config.numericSolverTimeout) |
79 | // System.load("libz3java.so"); | 79 | // } |
80 | return new NumericZ3ProblemSolver(config.drealTimeout) | 80 | } |
81 | } | 81 | // else { |
82 | } | 82 | // //initialise both dreal-local and z3 |
83 | else { | 83 | // |
84 | //initialise both dreal-local and z3 | 84 | // //TODO THIS IS HARD-CODED for now |
85 | 85 | //// val root = "/data/viatra/VIATRA-Generator"; | |
86 | //TODO THIS IS HARD-CODED for now | 86 | // val root = "/home/models/VIATRA-Generator"; |
87 | // val root = "/data/viatra/VIATRA-Generator"; | 87 | // //END HARD-CODED |
88 | val root = "/home/models/VIATRA-Generator"; | 88 | //// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); |
89 | //END HARD-CODED | 89 | // System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); |
90 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); | 90 | // System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); |
91 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); | 91 | // return new NumericDynamicProblemSolver(drealLocalPath, config.drealTimeout) |
92 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | 92 | // } |
93 | return new NumericDynamicProblemSolver(drealLocalPath, config.drealTimeout) | 93 | } |
94 | } | 94 | |
95 | } | 95 | def init(ThreadContext context) { |
96 | 96 | // This makes the NumericSolver single-threaded, | |
97 | def init(ThreadContext context) { | 97 | // but that's not a problem, because we only use the solver on a single thread anyways. |
98 | // This makes the NumericSolver single-threaded, | 98 | this.threadContext = context |
99 | // but that's not a problem, because we only use the solver on a single thread anyways. | 99 | val engine = threadContext.queryEngine |
100 | this.threadContext = context | 100 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { |
101 | val engine = threadContext.queryEngine | 101 | val constraint = entry.key |
102 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { | 102 | val querySpec = entry.value |
103 | val constraint = entry.key | 103 | val matcher = querySpec.getMatcher(engine); |
104 | val querySpec = entry.value | 104 | constraint2MustUnitPropagationPrecondition.put(constraint,matcher) |
105 | val matcher = querySpec.getMatcher(engine); | 105 | } |
106 | constraint2MustUnitPropagationPrecondition.put(constraint,matcher) | 106 | for(entry : method.currentUnitPropagationPreconditions.entrySet) { |
107 | } | 107 | val constraint = entry.key |
108 | for(entry : method.currentUnitPropagationPreconditions.entrySet) { | 108 | val querySpec = entry.value |
109 | val constraint = entry.key | 109 | val matcher = querySpec.getMatcher(engine); |
110 | val querySpec = entry.value | 110 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) |
111 | val matcher = querySpec.getMatcher(engine); | 111 | } |
112 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) | 112 | } |
113 | } | 113 | |
114 | } | 114 | def getRuntime(){runtime} |
115 | 115 | def getCachingTime(){cachingTime} | |
116 | def getRuntime(){runtime} | 116 | def getNumberOfSolverCalls(){numberOfSolverCalls} |
117 | def getCachingTime(){cachingTime} | 117 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} |
118 | def getNumberOfSolverCalls(){numberOfSolverCalls} | 118 | def getSolverFormingProblem(){this.translator.formingProblemTime} |
119 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} | 119 | def getSolverSolvingProblem(){this.translator.solvingProblemTime} |
120 | def getSolverFormingProblem(){this.t.formingProblemTime} | 120 | def getSolverSolution(){this.translator.formingSolutionTime} |
121 | def getSolverSolvingProblem(){this.t.solvingProblemTime} | 121 | def getNumericSolverSelection(){this.translator.numericSolver} |
122 | def getSolverSolution(){this.t.formingSolutionTime} | 122 | |
123 | def getNumericSolverSelection(){this.t.numericSolver} | 123 | def boolean maySatisfiable() { |
124 | 124 | val int phase = determinePhase() | |
125 | def boolean maySatisfiable() { | 125 | |
126 | val int phase = determinePhase() | 126 | if(intermediateConsistencyCheck) { |
127 | 127 | return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase) | |
128 | if(intermediateConsistencyCheck) { | 128 | } else { |
129 | return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase) | 129 | return true |
130 | } else { | 130 | } |
131 | return true | 131 | } |
132 | } | 132 | def boolean currentSatisfiable() { |
133 | } | 133 | val int phase = determinePhase() |
134 | def boolean currentSatisfiable() { | 134 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) |
135 | val int phase = determinePhase() | 135 | } |
136 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) | 136 | |
137 | } | 137 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches, int phase) { |
138 | 138 | val start = System.nanoTime | |
139 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches, int phase) { | 139 | var boolean finalResult |
140 | val start = System.nanoTime | 140 | val boolean needsFilling = needsFilling |
141 | var boolean finalResult | 141 | val model = threadContext.getModel as PartialInterpretation |
142 | val boolean needsFilling = needsFilling | 142 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList |
143 | val model = threadContext.getModel as PartialInterpretation | 143 | |
144 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | 144 | if(matches.empty){ |
145 | 145 | finalResult=true | |
146 | if(matches.empty){ | 146 | } else { |
147 | finalResult=true | 147 | val propagatedConstraints = new HashMap |
148 | } else { | 148 | //Filter constraints if there are phase-related restricutions |
149 | val propagatedConstraints = new HashMap | 149 | //null whitelist means accept everything |
150 | //Filter constraints if there are phase-related restricutions | 150 | |
151 | //null whitelist means accept everything | 151 | // println("<<<<START-STEP>>>> (" + phase + ")") |
152 | 152 | if (phase == -2) { | |
153 | // println("<<<<START-STEP>>>> (" + phase + ")") | 153 | // println("Skipping numeric check") |
154 | if (phase == -2) { | 154 | //TODO Big assumption |
155 | // println("Skipping numeric check") | 155 | return true |
156 | //TODO Big assumption | 156 | } |
157 | return true | 157 | val whitelist = getConstraintWhitelist(phase) |
158 | } | 158 | for(entry : matches.entrySet) { |
159 | val whitelist = getConstraintWhitelist(phase) | 159 | if (entry.value !== null){ |
160 | for(entry : matches.entrySet) { | 160 | val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName |
161 | if (entry.value !== null){ | 161 | if (whitelist === null || whitelist.contains(name)) { |
162 | val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName | 162 | // println(name) |
163 | if (whitelist === null || whitelist.contains(name)) { | 163 | val constraint = entry.key |
164 | // println(name) | 164 | // println("--match?-- " + constraint) |
165 | val constraint = entry.key | 165 | val allMatches = entry.value.allMatches.map[it.toArray] |
166 | // println("--match?-- " + constraint) | 166 | // println("---------- " + entry.value.allMatches) |
167 | val allMatches = entry.value.allMatches.map[it.toArray] | 167 | propagatedConstraints.put(constraint,allMatches) |
168 | // println("---------- " + entry.value.allMatches) | 168 | } |
169 | propagatedConstraints.put(constraint,allMatches) | 169 | } |
170 | } | 170 | } |
171 | } | 171 | //check numeric problem |
172 | } | 172 | if(propagatedConstraints.values.forall[empty]) { |
173 | //check numeric problem | 173 | finalResult=true |
174 | if(propagatedConstraints.values.forall[empty]) { | 174 | } else { |
175 | finalResult=true | 175 | if(caching) { |
176 | } else { | 176 | val code = getCode(propagatedConstraints) |
177 | if(caching) { | 177 | val cachedResult = satisfiabilityCache.get(code) |
178 | val code = getCode(propagatedConstraints) | 178 | if(cachedResult === null) { |
179 | val cachedResult = satisfiabilityCache.get(code) | 179 | // println('''new problem, call solver''') |
180 | if(cachedResult === null) { | 180 | // for(entry : code.entrySet) { |
181 | // println('''new problem, call solver''') | 181 | // println('''«entry.key» -> «entry.value»''') |
182 | // for(entry : code.entrySet) { | 182 | // } |
183 | // println('''«entry.key» -> «entry.value»''') | 183 | //println(code.hashCode) |
184 | // } | 184 | this.numberOfSolverCalls++ |
185 | //println(code.hashCode) | 185 | var boolean res = false |
186 | this.numberOfSolverCalls++ | 186 | if (needsFilling){ |
187 | var boolean res = false | 187 | //TODO ASSUME Always True |
188 | if (needsFilling){ | 188 | //GET LIST OF VARS TO FILL |
189 | //TODO ASSUME Always True | 189 | val fillMap = translator.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) |
190 | //GET LIST OF VARS TO FILL | 190 | if (fillMap === null) res = false |
191 | val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) | ||
192 | if (fillMap === null) res = false | ||
193 | else { | 191 | else { |
194 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | 192 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) |
195 | res = true | 193 | res = true |
196 | } | 194 | } |
197 | } else { | 195 | } else { |
198 | res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) | 196 | res = translator.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) |
199 | } | 197 | } |
200 | //TODO FIX CACHING | 198 | //TODO FIX CACHING |
201 | satisfiabilityCache.put(code,res) | 199 | satisfiabilityCache.put(code,res) |
202 | finalResult=res | 200 | finalResult=res |
203 | } else { | 201 | } else { |
204 | //println('''similar problem, answer from cache''') | 202 | //println('''similar problem, answer from cache''') |
205 | println('''potential issue, answer from cache''') | 203 | println('''potential issue, answer from cache''') |
206 | finalResult=cachedResult | 204 | finalResult=cachedResult |
207 | this.numberOfCachedSolverCalls++ | 205 | this.numberOfCachedSolverCalls++ |
208 | } | 206 | } |
209 | } else { | 207 | } else { |
210 | if (needsFilling){ | 208 | if (needsFilling){ |
211 | //GET LIST OF VARS TO FILL | 209 | //GET LIST OF VARS TO FILL |
212 | val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) | 210 | val fillMap = translator.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) |
213 | if (fillMap === null) finalResult = false | 211 | if (fillMap === null) finalResult = false |
214 | else { | 212 | else { |
215 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | 213 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) |
216 | finalResult = true | 214 | finalResult = true |
217 | } | 215 | } |
218 | } else { | 216 | } else { |
219 | finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) | 217 | finalResult = translator.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) |
220 | } | 218 | } |
221 | this.numberOfSolverCalls++ | 219 | this.numberOfSolverCalls++ |
222 | } | 220 | } |
223 | } | 221 | } |
224 | } | 222 | } |
225 | this.runtime+=System.nanoTime-start | 223 | this.runtime+=System.nanoTime-start |
226 | //STRATEGY | 224 | //STRATEGY |
227 | if (phase == 2) { | 225 | if (phase == 2) { |
228 | if (!finalResult) return finalResult | 226 | if (!finalResult) return finalResult |
229 | else { | 227 | else { |
230 | finalResult = isSatisfiable(matches, 3) | 228 | finalResult = isSatisfiable(matches, 3) |
231 | } | 229 | } |
232 | } | 230 | } |
233 | return finalResult | 231 | return finalResult |
234 | } | 232 | } |
235 | 233 | ||
236 | def selectSolver(int phase) { | 234 | def selectSolver(int phase) { |
237 | if (strategy === ExplorationStrategy.CrossingScenario){ | 235 | if (strategy === ExplorationStrategy.CrossingScenario){ |
238 | if (phase == 1) return "z3" | 236 | if (phase == 1) return "z3" |
239 | else return "dreal" | 237 | else return "dreal" |
240 | } | 238 | } |
241 | return "irrelevant" | 239 | return "irrelevant" |
242 | } | 240 | } |
243 | 241 | ||
244 | def int determinePhase() { | 242 | def int determinePhase() { |
245 | // >= 0 : an actual phase | 243 | // >= 0 : an actual phase |
246 | // -1 : take all numeric constraints | 244 | // -1 : take all numeric constraints |
247 | // -2 : SKIP (take no numeric constraints) | 245 | // -2 : SKIP (take no numeric constraints) |
248 | if (strategy == ExplorationStrategy.CrossingScenario) { | 246 | if (strategy == ExplorationStrategy.CrossingScenario) { |
249 | // //if has structural (non-WF) fitness issues, skip numeric handling | 247 | // //if has structural (non-WF) fitness issues, skip numeric handling |
250 | // val IObjective ob = threadContext.objectives.filter[it instanceof ModelGenerationCompositeObjective].get(0) | 248 | // val IObjective ob = threadContext.objectives.filter[it instanceof ModelGenerationCompositeObjective].get(0) |
251 | // val compo = ob as ModelGenerationCompositeObjective | 249 | // val compo = ob as ModelGenerationCompositeObjective |
252 | // if (compo.getNonWFFitness(threadContext) > 0) { | 250 | // if (compo.getNonWFFitness(threadContext) > 0) { |
253 | // println("bootleg numeric-skip") | 251 | // println("bootleg numeric-skip") |
254 | // return -2; | 252 | // return -2; |
255 | // } | 253 | // } |
256 | 254 | ||
257 | //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors | 255 | //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors |
258 | val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; | 256 | val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; |
259 | val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation(); | 257 | val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation(); |
260 | var boolean foundBlockedBy = false; | 258 | var boolean foundBlockedBy = false; |
261 | 259 | ||
262 | var int numActors; | 260 | var int numActors; |
263 | var int numPlacedOn; | 261 | var int numPlacedOn; |
264 | var int numPlacements = 0; | 262 | var int numPlacements = 0; |
265 | 263 | ||
266 | for (PartialRelationInterpretation rel : relations) { | 264 | for (PartialRelationInterpretation rel : relations) { |
267 | if(rel.getInterpretationOf().getName().equals("actors reference CrossingScenario")) { | 265 | if(rel.getInterpretationOf().getName().equals("actors reference CrossingScenario")) { |
268 | numActors = rel.relationlinks.size | 266 | numActors = rel.relationlinks.size |
269 | } | 267 | } |
270 | 268 | ||
271 | if(rel.getInterpretationOf().getName().equals("placedOn reference Actor")) { | 269 | if(rel.getInterpretationOf().getName().equals("placedOn reference Actor")) { |
272 | numPlacedOn = rel.relationlinks.size | 270 | numPlacedOn = rel.relationlinks.size |
273 | } | 271 | } |
274 | 272 | ||
275 | if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) { | 273 | if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) { |
276 | for (RelationLink link : rel.getRelationlinks()) { | 274 | for (RelationLink link : rel.getRelationlinks()) { |
277 | val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement; | 275 | val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement; |
278 | if (param2.isValueSet()) { | 276 | if (param2.isValueSet()) { |
279 | numPlacements++ | 277 | numPlacements++ |
280 | } | 278 | } |
281 | } | 279 | } |
282 | } | 280 | } |
283 | 281 | ||
284 | if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { | 282 | if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { |
285 | if (!rel.getRelationlinks().isEmpty()) { | 283 | if (!rel.getRelationlinks().isEmpty()) { |
286 | foundBlockedBy = true | 284 | foundBlockedBy = true |
287 | } | 285 | } |
288 | } | 286 | } |
289 | } | 287 | } |
290 | val boolean unplacedActorExists = numPlacements < numActors | 288 | val boolean unplacedActorExists = numPlacements < numActors |
291 | //it means that there is no blockedBy | 289 | //it means that there is no blockedBy |
292 | //so we are at most at phase 2 | 290 | //so we are at most at phase 2 |
293 | if (numPlacedOn == 1 && numPlacements == 0) return 1 | 291 | if (numPlacedOn == 1 && numPlacements == 0) return 1 |
294 | if (foundBlockedBy && unplacedActorExists) return 2 | 292 | if (foundBlockedBy && unplacedActorExists) return 2 |
295 | if (numPlacements == numActors) return 3; | 293 | if (numPlacements == numActors) return 3; |
296 | return -2; | 294 | return -2; |
297 | } | 295 | } |
298 | return -1; | 296 | return -1; |
299 | } | 297 | } |
300 | 298 | ||
301 | def getConstraintWhitelist(int phase) { | 299 | def getConstraintWhitelist(int phase) { |
302 | val List<String> wl = newArrayList | 300 | val List<String> wl = newArrayList |
303 | //null return means accept everything | 301 | //null return means accept everything |
304 | if (strategy === ExplorationStrategy.None){ | 302 | if (strategy === ExplorationStrategy.None){ |
305 | return null | 303 | return null |
306 | } else if (strategy === ExplorationStrategy.CrossingScenario){ | 304 | } else if (strategy === ExplorationStrategy.CrossingScenario){ |
307 | /* | 305 | /* |
308 | "define_placedOn_actorOnVerticalLane", | 306 | "define_placedOn_actorOnVerticalLane", |
309 | "define_placedOn_actorOnHorizLane", | 307 | "define_placedOn_actorOnHorizLane", |
310 | 308 | ||
311 | "define_actor_maxXp", | 309 | "define_actor_maxXp", |
312 | "define_actor_minXp", | 310 | "define_actor_minXp", |
313 | "define_actor_maxYp", | 311 | "define_actor_maxYp", |
314 | "define_actor_minYp", | 312 | "define_actor_minYp", |
315 | 313 | ||
316 | "define_actor_wrtLane", | 314 | "define_actor_wrtLane", |
317 | 315 | ||
318 | "define_actor_minimumDistance", | 316 | "define_actor_minimumDistance", |
319 | 317 | ||
320 | "define_actor_actorOnVertLaneHasxSpeed0", | 318 | "define_actor_actorOnVertLaneHasxSpeed0", |
321 | "define_actor_actorOnVertLaneMinYs", | 319 | "define_actor_actorOnVertLaneMinYs", |
322 | "define_actor_actorOnVertLaneMaxYs", | 320 | "define_actor_actorOnVertLaneMaxYs", |
323 | "define_actor_actorOnHorizLaneHasySpeed0", | 321 | "define_actor_actorOnHorizLaneHasySpeed0", |
324 | "define_actor_actorOnHorizLaneMinXs", | 322 | "define_actor_actorOnHorizLaneMinXs", |
325 | "define_actor_actorOnHorizLaneMaxXs", | 323 | "define_actor_actorOnHorizLaneMaxXs", |
326 | 324 | ||
327 | "define_actor_pedestrianWidth", | 325 | "define_actor_pedestrianWidth", |
328 | "define_actor_pedestrianLength", | 326 | "define_actor_pedestrianLength", |
329 | "define_actor_vehicleWidth", | 327 | "define_actor_vehicleWidth", |
330 | "define_actor_vehicleWidth", | 328 | "define_actor_vehicleWidth", |
331 | "define_actor_vehicleLength", | 329 | "define_actor_vehicleLength", |
332 | "define_actor_vehicleLength", | 330 | "define_actor_vehicleLength", |
333 | 331 | ||
334 | "collisionExists_timeWithinBound", | 332 | "collisionExists_timeWithinBound", |
335 | "collisionExists_timeNotNegative", | 333 | "collisionExists_timeNotNegative", |
336 | "collisionExists_defineCollision_y1", | 334 | "collisionExists_defineCollision_y1", |
337 | "collisionExists_defineCollision_y2", | 335 | "collisionExists_defineCollision_y2", |
338 | "collisionExists_defineCollision_x1", | 336 | "collisionExists_defineCollision_x1", |
339 | "collisionExists_defineCollision_x2", | 337 | "collisionExists_defineCollision_x2", |
340 | 338 | ||
341 | "visionBlocked_ites_notOnSameVertLine", | 339 | "visionBlocked_ites_notOnSameVertLine", |
342 | "visionBlocked_ites_top", | 340 | "visionBlocked_ites_top", |
343 | "visionBlocked_ites_bottom", | 341 | "visionBlocked_ites_bottom", |
344 | "visionBlocked_xdistBSlargerThanxdistTS", | 342 | "visionBlocked_xdistBSlargerThanxdistTS", |
345 | "visionBlocked_xdistBTlargerThanxdistST", | 343 | "visionBlocked_xdistBTlargerThanxdistST", |
346 | "visionBlocked_ydistBSlargerThanydistTS", | 344 | "visionBlocked_ydistBSlargerThanydistTS", |
347 | "visionBlocked_ydistBTlargerThanydistST" | 345 | "visionBlocked_ydistBTlargerThanydistST" |
348 | */ | 346 | */ |
349 | 347 | ||
350 | //HINTS: | 348 | //HINTS: |
351 | //define_actor_wrtLane | 349 | //define_actor_wrtLane |
352 | //28.5 is structural hint | 350 | //28.5 is structural hint |
353 | switch (phase) { | 351 | switch (phase) { |
354 | case 1: { | 352 | case 1: { |
355 | wl.addAll(#[ | 353 | wl.addAll(#[ |
356 | "define_placedOn_actorOnVerticalLane", | 354 | "define_placedOn_actorOnVerticalLane", |
357 | "define_placedOn_actorOnHorizLane", | 355 | "define_placedOn_actorOnHorizLane", |
358 | 356 | ||
359 | "define_actor_maxXp", | 357 | "define_actor_maxXp", |
360 | "define_actor_minXp", | 358 | "define_actor_minXp", |
361 | "define_actor_maxYp", | 359 | "define_actor_maxYp", |
362 | "define_actor_minYp", | 360 | "define_actor_minYp", |
363 | 361 | ||
364 | "define_actor_pedestrianWidth", | 362 | "define_actor_pedestrianWidth", |
365 | "define_actor_pedestrianLength", | 363 | "define_actor_pedestrianLength", |
366 | "define_actor_vehicleWidth", | 364 | "define_actor_vehicleWidth", |
367 | "define_actor_vehicleWidth", | 365 | "define_actor_vehicleWidth", |
368 | "define_actor_vehicleLength", | 366 | "define_actor_vehicleLength", |
369 | "define_actor_vehicleLength" | 367 | "define_actor_vehicleLength" |
370 | 368 | ||
371 | ]) | 369 | ]) |
372 | } | 370 | } |
373 | case 2: { | 371 | case 2: { |
374 | wl.addAll(#[ | 372 | wl.addAll(#[ |
375 | 373 | ||
376 | "define_placedOn_actorOnVerticalLane", | 374 | "define_placedOn_actorOnVerticalLane", |
377 | "define_placedOn_actorOnHorizLane", | 375 | "define_placedOn_actorOnHorizLane", |
378 | 376 | ||
379 | "define_actor_maxXp", | 377 | "define_actor_maxXp", |
380 | "define_actor_minXp", | 378 | "define_actor_minXp", |
381 | "define_actor_maxYp", | 379 | "define_actor_maxYp", |
382 | "define_actor_minYp", | 380 | "define_actor_minYp", |
383 | 381 | ||
384 | "define_actor_minimumDistance", | 382 | "define_actor_minimumDistance", |
385 | 383 | ||
386 | "define_actor_pedestrianWidth", | 384 | "define_actor_pedestrianWidth", |
387 | "define_actor_pedestrianLength", | 385 | "define_actor_pedestrianLength", |
388 | "define_actor_vehicleWidth", | 386 | "define_actor_vehicleWidth", |
389 | "define_actor_vehicleWidth", | 387 | "define_actor_vehicleWidth", |
390 | "define_actor_vehicleLength", | 388 | "define_actor_vehicleLength", |
391 | "define_actor_vehicleLength", | 389 | "define_actor_vehicleLength", |
392 | 390 | ||
393 | "visionBlocked_ites_notOnSameVertLine", | 391 | "visionBlocked_ites_notOnSameVertLine", |
394 | "visionBlocked_ites_top", | 392 | "visionBlocked_ites_top", |
395 | "visionBlocked_ites_bottom", | 393 | "visionBlocked_ites_bottom", |
396 | "visionBlocked_xdistBSlargerThanxdistTS", | 394 | "visionBlocked_xdistBSlargerThanxdistTS", |
397 | "visionBlocked_xdistBTlargerThanxdistST", | 395 | "visionBlocked_xdistBTlargerThanxdistST", |
398 | "visionBlocked_ydistBSlargerThanydistTS", | 396 | "visionBlocked_ydistBSlargerThanydistTS", |
399 | "visionBlocked_ydistBTlargerThanydistST" | 397 | "visionBlocked_ydistBTlargerThanydistST" |
400 | ]) | 398 | ]) |
401 | } | 399 | } |
402 | case 3: { | 400 | case 3: { |
403 | wl.addAll(#[ | 401 | wl.addAll(#[ |
404 | 402 | ||
405 | "define_placedOn_actorOnVerticalLane", | 403 | "define_placedOn_actorOnVerticalLane", |
406 | "define_placedOn_actorOnHorizLane", | 404 | "define_placedOn_actorOnHorizLane", |
407 | 405 | ||
408 | "define_actor_maxXp", | 406 | "define_actor_maxXp", |
409 | "define_actor_minXp", | 407 | "define_actor_minXp", |
410 | "define_actor_maxYp", | 408 | "define_actor_maxYp", |
411 | "define_actor_minYp", | 409 | "define_actor_minYp", |
412 | 410 | ||
413 | "define_actor_minimumDistance", | 411 | "define_actor_minimumDistance", |
414 | 412 | ||
415 | "define_actor_actorOnVertLaneHasxSpeed0", | 413 | "define_actor_actorOnVertLaneHasxSpeed0", |
416 | "define_actor_actorOnVertLaneMinYs", | 414 | "define_actor_actorOnVertLaneMinYs", |
417 | "define_actor_actorOnVertLaneMaxYs", | 415 | "define_actor_actorOnVertLaneMaxYs", |
418 | "define_actor_actorOnHorizLaneHasySpeed0", | 416 | "define_actor_actorOnHorizLaneHasySpeed0", |
419 | "define_actor_actorOnHorizLaneMinXs", | 417 | "define_actor_actorOnHorizLaneMinXs", |
420 | "define_actor_actorOnHorizLaneMaxXs", | 418 | "define_actor_actorOnHorizLaneMaxXs", |
421 | 419 | ||
422 | "define_actor_pedestrianWidth", | 420 | "define_actor_pedestrianWidth", |
423 | "define_actor_pedestrianLength", | 421 | "define_actor_pedestrianLength", |
424 | "define_actor_vehicleWidth", | 422 | "define_actor_vehicleWidth", |
425 | "define_actor_vehicleWidth", | 423 | "define_actor_vehicleWidth", |
426 | "define_actor_vehicleLength", | 424 | "define_actor_vehicleLength", |
427 | "define_actor_vehicleLength", | 425 | "define_actor_vehicleLength", |
428 | 426 | ||
429 | "collisionExists_timeWithinBound", | 427 | "collisionExists_timeWithinBound", |
430 | "collisionExists_timeNotNegative", | 428 | "collisionExists_timeNotNegative", |
431 | "collisionExists_defineCollision_y1", | 429 | "collisionExists_defineCollision_y1", |
432 | "collisionExists_defineCollision_y2", | 430 | "collisionExists_defineCollision_y2", |
433 | "collisionExists_defineCollision_x1", | 431 | "collisionExists_defineCollision_x1", |
434 | "collisionExists_defineCollision_x2" | 432 | "collisionExists_defineCollision_x2" |
435 | ]) | 433 | ]) |
436 | } | 434 | } |
437 | default: { | 435 | default: { |
438 | //this is for 3 if we implement 4 | 436 | //this is for 3 if we implement 4 |
439 | // bl.addAll(#[0, 1, 2, 3, 4, 5, 6, 7]) | 437 | // bl.addAll(#[0, 1, 2, 3, 4, 5, 6, 7]) |
440 | 438 | ||
441 | //this is for 4 if we do it | 439 | //this is for 4 if we do it |
442 | wl.addAll(#[]) | 440 | wl.addAll(#[]) |
443 | return null | 441 | return null |
444 | } | 442 | } |
445 | } | 443 | } |
446 | } | 444 | } |
447 | return wl | 445 | return wl |
448 | } | 446 | } |
449 | 447 | ||
450 | def getNeedsFilling(){ | 448 | def getNeedsFilling(){ |
451 | if (strategy == ExplorationStrategy.CrossingScenario) return true | 449 | if (strategy == ExplorationStrategy.CrossingScenario) return true |
452 | return false | 450 | return false |
453 | } | 451 | } |
454 | 452 | ||
455 | def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) { | 453 | def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) { |
456 | val start = System.nanoTime | 454 | val start = System.nanoTime |
457 | val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList | 455 | val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList |
458 | val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]]) | 456 | val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]]) |
459 | this.cachingTime += System.nanoTime-start | 457 | this.cachingTime += System.nanoTime-start |
460 | return res | 458 | return res |
461 | } | 459 | } |
462 | 460 | ||
463 | def fillSolutionCopy(Map<EObject, EObject> trace) { | 461 | def fillSolutionCopy(Map<EObject, EObject> trace) { |
464 | //No need to do a final check to fill if we are using a strategy | 462 | //No need to do a final check to fill if we are using a strategy |
465 | if (strategy === ExplorationStrategy.CrossingScenario) return | 463 | if (strategy === ExplorationStrategy.CrossingScenario) return |
466 | val model = threadContext.getModel as PartialInterpretation | 464 | val model = threadContext.getModel as PartialInterpretation |
467 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | 465 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList |
468 | if(constraint2CurrentUnitPropagationPrecondition.empty) { | 466 | if(constraint2CurrentUnitPropagationPrecondition.empty) { |
469 | fillWithDefaultValues(dataObjects,trace) | 467 | fillWithDefaultValues(dataObjects,trace) |
470 | } else { | 468 | } else { |
471 | val propagatedConstraints = new HashMap | 469 | val propagatedConstraints = new HashMap |
472 | for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { | 470 | for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { |
473 | val constraint = entry.key | 471 | val constraint = entry.key |
474 | val allMatches = entry.value.allMatches.map[it.toArray] | 472 | val allMatches = entry.value.allMatches.map[it.toArray] |
475 | propagatedConstraints.put(constraint,allMatches) | 473 | propagatedConstraints.put(constraint,allMatches) |
476 | } | 474 | } |
477 | 475 | ||
478 | if(propagatedConstraints.values.forall[empty]) { | 476 | if(propagatedConstraints.values.forall[empty]) { |
479 | fillWithDefaultValues(dataObjects,trace) | 477 | fillWithDefaultValues(dataObjects,trace) |
480 | } else { | 478 | } else { |
481 | val solution = t.delegateGetSolution(dataObjects,propagatedConstraints, "dreal") | 479 | val solution = translator.delegateGetSolution(dataObjects,propagatedConstraints, "dreal") |
482 | fillWithSolutions(dataObjects,solution,trace) | 480 | fillWithSolutions(dataObjects,solution,trace) |
483 | } | 481 | } |
484 | } | 482 | } |
485 | } | 483 | } |
486 | 484 | ||
487 | def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) { | 485 | def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) { |
488 | for(element : elements) { | 486 | for(element : elements) { |
489 | if(element.valueSet==false) { | 487 | if(element.valueSet==false) { |
490 | val value = getDefaultValue(element) | 488 | val value = getDefaultValue(element) |
491 | val target = trace.get(element) as PrimitiveElement | 489 | val target = trace.get(element) as PrimitiveElement |
492 | target.fillWithValue(value) | 490 | target.fillWithValue(value) |
493 | } | 491 | } |
494 | } | 492 | } |
495 | } | 493 | } |
496 | 494 | ||
497 | def protected dispatch getDefaultValue(BooleanElement e) {false} | 495 | def protected dispatch getDefaultValue(BooleanElement e) {false} |
498 | def protected dispatch getDefaultValue(IntegerElement e) {0} | 496 | def protected dispatch getDefaultValue(IntegerElement e) {0} |
499 | def protected dispatch getDefaultValue(RealElement e) {0.0} | 497 | def protected dispatch getDefaultValue(RealElement e) {0.0} |
500 | def protected dispatch getDefaultValue(StringElement e) {""} | 498 | def protected dispatch getDefaultValue(StringElement e) {""} |
501 | 499 | ||
502 | def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution, Map<EObject, EObject> trace) { | 500 | def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution, Map<EObject, EObject> trace) { |
503 | for(element : elements) { | 501 | for(element : elements) { |
504 | if(element.valueSet==false) { | 502 | if(element.valueSet==false) { |
505 | if(solution.containsKey(element)) { | 503 | if(solution.containsKey(element)) { |
506 | val value = solution.get(element) | 504 | val value = solution.get(element) |
507 | val target = trace.get(element) as PrimitiveElement | 505 | val target = trace.get(element) as PrimitiveElement |
508 | target.fillWithValue(value) | 506 | target.fillWithValue(value) |
509 | } else { | 507 | } else { |
510 | val target = trace.get(element) as PrimitiveElement | 508 | val target = trace.get(element) as PrimitiveElement |
511 | target.fillWithValue(target.defaultValue) | 509 | target.fillWithValue(target.defaultValue) |
512 | } | 510 | } |
513 | } | 511 | } |
514 | } | 512 | } |
515 | } | 513 | } |
516 | 514 | ||
517 | def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean} | 515 | def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean} |
518 | def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} | 516 | def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} |
519 | def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double } | 517 | def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double } |
520 | def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} | 518 | def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} |
521 | 519 | ||
522 | def protected fillWithPartialSolutionsDirectly(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution) { | 520 | def protected fillWithPartialSolutionsDirectly(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution) { |
523 | for(element : elements) { | 521 | for(element : elements) { |
524 | //we allow overwriting of already set variables | 522 | //we allow overwriting of already set variables |
525 | if(solution.containsKey(element)) { | 523 | if(solution.containsKey(element)) { |
526 | val value = solution.get(element) | 524 | val value = solution.get(element) |
527 | if (value !== null){ | 525 | if (value !== null){ |
528 | element.fillWithValue(value) | 526 | element.fillWithValue(value) |
529 | } | 527 | } |
530 | } | 528 | } |
531 | } | 529 | } |
532 | } | 530 | } |
533 | } \ No newline at end of file | 531 | } \ 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/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend index 4484052d..0c170c2f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend | |||
@@ -222,4 +222,4 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | |||
222 | } | 222 | } |
223 | builder | 223 | builder |
224 | } | 224 | } |
225 | } | 225 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend index 33b69436..7c30bbb5 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend | |||
@@ -28,7 +28,7 @@ class CopiedSolution { | |||
28 | class SolutionCopier { | 28 | class SolutionCopier { |
29 | val copiedSolutions = new LinkedHashMap<Object, CopiedSolution> | 29 | val copiedSolutions = new LinkedHashMap<Object, CopiedSolution> |
30 | 30 | ||
31 | @Accessors NumericSolver numericSolver | 31 | @Accessors NumericRefinementUnit numericSolver |
32 | long startTime = System.nanoTime | 32 | long startTime = System.nanoTime |
33 | @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 | 33 | @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 |
34 | 34 | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend index e00f76ff..ac29c4ce 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend | |||
@@ -33,7 +33,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsPro | |||
33 | val ObjectiveComparatorHelper comparatorHelper | 33 | val ObjectiveComparatorHelper comparatorHelper |
34 | val Map<SolutionTrajectory, Fitness> trajectories = new HashMap | 34 | val Map<SolutionTrajectory, Fitness> trajectories = new HashMap |
35 | 35 | ||
36 | @Accessors var NumericSolver numericSolver | 36 | @Accessors var NumericRefinementUnit numericSolver |
37 | @Accessors var Map<Object, Solution> solutionsCollection | 37 | @Accessors var Map<Object, Solution> solutionsCollection |
38 | 38 | ||
39 | new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) { | 39 | new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) { |
@@ -45,7 +45,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsPro | |||
45 | this.solutionCopier = new SolutionCopier | 45 | this.solutionCopier = new SolutionCopier |
46 | } | 46 | } |
47 | 47 | ||
48 | def setNumericSolver(NumericSolver numericSolver) { | 48 | def setNumericSolver(NumericRefinementUnit numericSolver) { |
49 | this.numericSolver = numericSolver | 49 | this.numericSolver = numericSolver |
50 | solutionCopier.numericSolver = numericSolver | 50 | solutionCopier.numericSolver = numericSolver |
51 | } | 51 | } |
@@ -63,7 +63,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsPro | |||
63 | if (!shouldSaveSolution(fitness, context)) { | 63 | if (!shouldSaveSolution(fitness, context)) { |
64 | return false | 64 | return false |
65 | } | 65 | } |
66 | println("Found: " + fitness) | 66 | //println("Found: " + fitness) |
67 | val dominatedTrajectories = newArrayList | 67 | val dominatedTrajectories = newArrayList |
68 | for (entry : trajectories.entrySet) { | 68 | for (entry : trajectories.entrySet) { |
69 | val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) | 69 | val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) |