From aaa67b0ef8840d97b062a4f1383bf93410984af3 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Fri, 30 Jul 2021 10:04:27 +0200 Subject: Numeric solver dreal hardcoding -> config --- .../viatrasolver/reasoner/ViatraReasoner.xtend | 6 +- .../reasoner/ViatraReasonerConfiguration.xtend | 3 +- .../dse/BestFirstStrategyForModelGeneration.java | 4 +- .../reasoner/dse/NumericRefinementUnit.xtend | 531 ++++++++++++++++++++ .../viatrasolver/reasoner/dse/NumericSolver.xtend | 533 --------------------- .../dse/PartialModelAsLogicInterpretation.xtend | 2 +- .../viatrasolver/reasoner/dse/SolutionCopier.xtend | 2 +- .../reasoner/dse/ViatraReasonerSolutionSaver.xtend | 6 +- .../viatra/dse/solutionstore/SolutionStore.java | 2 +- 9 files changed, 544 insertions(+), 545 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend delete mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend (limited to 'Solvers/VIATRA-Solver') 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 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.NumericSolver import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective @@ -39,6 +38,7 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel import org.eclipse.viatra.dse.solutionstore.SolutionStore import org.eclipse.viatra.dse.statecode.IStateCoderFactory import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.NumericRefinementUnit class ViatraReasoner extends LogicReasoner { val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() @@ -110,7 +110,7 @@ class ViatraReasoner extends LogicReasoner { new SolutionStore(numberOfRequiredSolutions) } solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) - val numericSolver = new NumericSolver(method, viatraConfig, false)//was formerly hard-coded to false for caching + val numericSolver = new NumericRefinementUnit(method, viatraConfig, false)//was formerly hard-coded to false for caching val solutionSaver = method.solutionSaver solutionSaver.numericSolver = numericSolver val solutionCopier = solutionSaver.solutionCopier @@ -156,7 +156,7 @@ class ViatraReasoner extends LogicReasoner { val transformationTime = transformationFinished - transformationStartTime val solverStartTime = System.nanoTime - println(">>begin exploration") + //println(">>begin exploration") var boolean stoppedByTimeout try { 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 { public var unfinishedWFWeight = 1 public var calculateObjectCreationCosts = false public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3 + public var NumericSolverPath = "" public var drealLocalPath = ""; - public var drealTimeout = 10000; + public var numericSolverTimeout = 10000; public var Map> ignoredAttributesMap = null; public var ExplorationStrategy strategy = ExplorationStrategy.None 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 { // private Collection> matchers; public ActivationSelector activationSelector = new EvenActivationSelector(random); public ViatraReasonerSolutionSaver solutionSaver; - public NumericSolver numericSolver; + public NumericRefinementUnit numericSolver; // Statistics private int numberOfStatecoderFail = 0; private int numberOfPrintedModel = 0; @@ -94,7 +94,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { ViatraReasonerConfiguration configuration, ModelGenerationMethod method, ViatraReasonerSolutionSaver solutionSaver, - NumericSolver numericSolver) { + NumericRefinementUnit numericSolver) { this.workspace = workspace; this.configuration = configuration; 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/NumericRefinementUnit.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend new file mode 100644 index 00000000..b3e2d78d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend @@ -0,0 +1,531 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver +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 +import java.util.HashMap +import java.util.LinkedHashMap +import java.util.LinkedHashSet +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 NumericRefinementUnit { + val ModelGenerationMethod method + var ThreadContext threadContext + val constraint2MustUnitPropagationPrecondition = new HashMap> + val constraint2CurrentUnitPropagationPrecondition = new HashMap> + var NumericTranslator translator = null; + + + val boolean intermediateConsistencyCheck + val boolean caching; + Map>>,Boolean> satisfiabilityCache = new HashMap + val ExplorationStrategy strategy; + + var long runtime = 0 + var long cachingTime = 0 + var int numberOfSolverCalls = 0 + var int numberOfCachedSolverCalls = 0 + + new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { + this.method = method + this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks + this.caching = caching + this.strategy = config.strategy + this.translator = new NumericTranslator(createNumericTranslator(config),config.numericSolverTimeout) + } + + 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, config.numericSolverTimeout) + if (solverSelection == NumericSolverSelection.DREAL_LOCAL) + return new NumericDrealProblemSolver(false, config.drealLocalPath, config.numericSolverTimeout) + 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(config.numericSolverTimeout) +// } + } +// else { +// //initialise both dreal-local and 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"); +// return new NumericDynamicProblemSolver(drealLocalPath, config.drealTimeout) +// } + } + + def init(ThreadContext context) { + // This makes the NumericSolver single-threaded, + // but that's not a problem, because we only use the solver on a single thread anyways. + this.threadContext = context + val engine = threadContext.queryEngine + for(entry : method.mustUnitPropagationPreconditions.entrySet) { + val constraint = entry.key + val querySpec = entry.value + val matcher = querySpec.getMatcher(engine); + constraint2MustUnitPropagationPrecondition.put(constraint,matcher) + } + for(entry : method.currentUnitPropagationPreconditions.entrySet) { + val constraint = entry.key + val querySpec = entry.value + val matcher = querySpec.getMatcher(engine); + constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) + } + } + + def getRuntime(){runtime} + def getCachingTime(){cachingTime} + def getNumberOfSolverCalls(){numberOfSolverCalls} + def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} + def getSolverFormingProblem(){this.translator.formingProblemTime} + def getSolverSolvingProblem(){this.translator.solvingProblemTime} + def getSolverSolution(){this.translator.formingSolutionTime} + def getNumericSolverSelection(){this.translator.numericSolver} + + def boolean maySatisfiable() { + val int phase = determinePhase() + + if(intermediateConsistencyCheck) { + return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase) + } else { + return true + } + } + def boolean currentSatisfiable() { + val int phase = determinePhase() + isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) + } + + 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 + //Filter constraints if there are phase-related restricutions + //null whitelist means accept everything + +// println("<<<>>> (" + phase + ")") + if (phase == -2) { +// println("Skipping numeric check") + //TODO Big assumption + return true + } + val whitelist = getConstraintWhitelist(phase) + for(entry : matches.entrySet) { + 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 { + if(caching) { + val code = getCode(propagatedConstraints) + val cachedResult = satisfiabilityCache.get(code) + if(cachedResult === null) { + // println('''new problem, call solver''') + // for(entry : code.entrySet) { + // println('''«entry.key» -> «entry.value»''') + // } + //println(code.hashCode) + this.numberOfSolverCalls++ + var boolean res = false + if (needsFilling){ + //TODO ASSUME Always True + //GET LIST OF VARS TO FILL + val fillMap = translator.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) + if (fillMap === null) res = false + else { + fillWithPartialSolutionsDirectly(dataObjects, fillMap) + res = true + } + } else { + res = translator.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 { + if (needsFilling){ + //GET LIST OF VARS TO FILL + val fillMap = translator.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) + if (fillMap === null) finalResult = false + else { + fillWithPartialSolutionsDirectly(dataObjects, fillMap) + finalResult = true + } + } else { + finalResult = translator.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) + } + this.numberOfSolverCalls++ + } + } + } + this.runtime+=System.nanoTime-start + //STRATEGY + if (phase == 2) { + if (!finalResult) return finalResult + else { + finalResult = isSatisfiable(matches, 3) + } + } + return finalResult + } + + def selectSolver(int phase) { + if (strategy === ExplorationStrategy.CrossingScenario){ + if (phase == 1) return "z3" + 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) { +// //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(); + var boolean foundBlockedBy = false; + + var int numActors; + var int numPlacedOn; + var int numPlacements = 0; + + for (PartialRelationInterpretation rel : relations) { + if(rel.getInterpretationOf().getName().equals("actors reference CrossingScenario")) { + numActors = rel.relationlinks.size + } + + if(rel.getInterpretationOf().getName().equals("placedOn reference Actor")) { + numPlacedOn = rel.relationlinks.size + } + + 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()) { + numPlacements++ + } + } + } + + if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { + if (!rel.getRelationlinks().isEmpty()) { + foundBlockedBy = true + } + } + } + val boolean unplacedActorExists = numPlacements < numActors + //it means that there is no blockedBy + //so we are at most at phase 2 + if (numPlacedOn == 1 && numPlacements == 0) return 1 + if (foundBlockedBy && unplacedActorExists) return 2 + if (numPlacements == numActors) return 3; + return -2; + } + 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 + val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]]) + this.cachingTime += System.nanoTime-start + return res + } + + def fillSolutionCopy(Map trace) { + //No need to do a final check to fill if we are using a strategy + if (strategy === ExplorationStrategy.CrossingScenario) return + val model = threadContext.getModel as PartialInterpretation + val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList + if(constraint2CurrentUnitPropagationPrecondition.empty) { + fillWithDefaultValues(dataObjects,trace) + } else { + val propagatedConstraints = new HashMap + for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { + val constraint = entry.key + val allMatches = entry.value.allMatches.map[it.toArray] + propagatedConstraints.put(constraint,allMatches) + } + + if(propagatedConstraints.values.forall[empty]) { + fillWithDefaultValues(dataObjects,trace) + } else { + val solution = translator.delegateGetSolution(dataObjects,propagatedConstraints, "dreal") + fillWithSolutions(dataObjects,solution,trace) + } + } + } + + def protected fillWithDefaultValues(List elements, Map trace) { + for(element : elements) { + if(element.valueSet==false) { + val value = getDefaultValue(element) + val target = trace.get(element) as PrimitiveElement + target.fillWithValue(value) + } + } + } + + def protected dispatch getDefaultValue(BooleanElement e) {false} + def protected dispatch getDefaultValue(IntegerElement e) {0} + def protected dispatch getDefaultValue(RealElement e) {0.0} + def protected dispatch getDefaultValue(StringElement e) {""} + + def protected fillWithSolutions(List elements, Map solution, Map trace) { + for(element : elements) { + if(element.valueSet==false) { + if(solution.containsKey(element)) { + val value = solution.get(element) + val target = trace.get(element) as PrimitiveElement + target.fillWithValue(value) + } else { + val target = trace.get(element) as PrimitiveElement + target.fillWithValue(target.defaultValue) + } + } + } + } + + def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean} + 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) + } + } + } + } +} \ 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/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend deleted file mode 100644 index a228afc6..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ /dev/null @@ -1,533 +0,0 @@ -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 -import java.util.HashMap -import java.util.LinkedHashMap -import java.util.LinkedHashSet -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 - var ThreadContext threadContext - val constraint2MustUnitPropagationPrecondition = new HashMap> - val constraint2CurrentUnitPropagationPrecondition = new HashMap> - NumericTranslator t - - val boolean intermediateConsistencyCheck - val boolean caching; - Map>>,Boolean> satisfiabilityCache = new HashMap - val String drealLocalPath; - val ExplorationStrategy strategy; - - var long runtime = 0 - var long cachingTime = 0 - var int numberOfSolverCalls = 0 - var int numberOfCachedSolverCalls = 0 - - new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { - this.method = method - this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks - this.caching = caching - this.drealLocalPath = config.drealLocalPath - this.strategy = config.strategy - this.t = new NumericTranslator(createNumericTranslator(config), config.drealTimeout) - } - - 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, config.drealTimeout) - if (solverSelection == NumericSolverSelection.DREAL_LOCAL) - return new NumericDrealProblemSolver(false, drealLocalPath, config.drealTimeout) - 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(config.drealTimeout) - } - } - else { - //initialise both dreal-local and 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"); - return new NumericDynamicProblemSolver(drealLocalPath, config.drealTimeout) - } - } - - def init(ThreadContext context) { - // This makes the NumericSolver single-threaded, - // but that's not a problem, because we only use the solver on a single thread anyways. - this.threadContext = context - val engine = threadContext.queryEngine - for(entry : method.mustUnitPropagationPreconditions.entrySet) { - val constraint = entry.key - val querySpec = entry.value - val matcher = querySpec.getMatcher(engine); - constraint2MustUnitPropagationPrecondition.put(constraint,matcher) - } - for(entry : method.currentUnitPropagationPreconditions.entrySet) { - val constraint = entry.key - val querySpec = entry.value - val matcher = querySpec.getMatcher(engine); - constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) - } - } - - def getRuntime(){runtime} - def getCachingTime(){cachingTime} - def getNumberOfSolverCalls(){numberOfSolverCalls} - def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} - def getSolverFormingProblem(){this.t.formingProblemTime} - def getSolverSolvingProblem(){this.t.solvingProblemTime} - def getSolverSolution(){this.t.formingSolutionTime} - def getNumericSolverSelection(){this.t.numericSolver} - - def boolean maySatisfiable() { - val int phase = determinePhase() - - if(intermediateConsistencyCheck) { - return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase) - } else { - return true - } - } - def boolean currentSatisfiable() { - val int phase = determinePhase() - isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) - } - - 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 - //Filter constraints if there are phase-related restricutions - //null whitelist means accept everything - -// println("<<<>>> (" + phase + ")") - if (phase == -2) { -// println("Skipping numeric check") - //TODO Big assumption - return true - } - val whitelist = getConstraintWhitelist(phase) - for(entry : matches.entrySet) { - 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 { - if(caching) { - val code = getCode(propagatedConstraints) - val cachedResult = satisfiabilityCache.get(code) - if(cachedResult === null) { - // println('''new problem, call solver''') - // for(entry : code.entrySet) { - // println('''«entry.key» -> «entry.value»''') - // } - //println(code.hashCode) - this.numberOfSolverCalls++ - var boolean res = false - if (needsFilling){ - //TODO ASSUME Always True - //GET LIST OF VARS TO FILL - val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) - if (fillMap === null) res = false - else { - 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 { - if (needsFilling){ - //GET LIST OF VARS TO FILL - val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) - if (fillMap === null) finalResult = false - else { - fillWithPartialSolutionsDirectly(dataObjects, fillMap) - finalResult = true - } - } else { - finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) - } - this.numberOfSolverCalls++ - } - } - } - this.runtime+=System.nanoTime-start - //STRATEGY - if (phase == 2) { - if (!finalResult) return finalResult - else { - finalResult = isSatisfiable(matches, 3) - } - } - return finalResult - } - - def selectSolver(int phase) { - if (strategy === ExplorationStrategy.CrossingScenario){ - if (phase == 1) return "z3" - 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) { -// //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(); - var boolean foundBlockedBy = false; - - var int numActors; - var int numPlacedOn; - var int numPlacements = 0; - - for (PartialRelationInterpretation rel : relations) { - if(rel.getInterpretationOf().getName().equals("actors reference CrossingScenario")) { - numActors = rel.relationlinks.size - } - - if(rel.getInterpretationOf().getName().equals("placedOn reference Actor")) { - numPlacedOn = rel.relationlinks.size - } - - 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()) { - numPlacements++ - } - } - } - - if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { - if (!rel.getRelationlinks().isEmpty()) { - foundBlockedBy = true - } - } - } - val boolean unplacedActorExists = numPlacements < numActors - //it means that there is no blockedBy - //so we are at most at phase 2 - if (numPlacedOn == 1 && numPlacements == 0) return 1 - if (foundBlockedBy && unplacedActorExists) return 2 - if (numPlacements == numActors) return 3; - return -2; - } - 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 - val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]]) - this.cachingTime += System.nanoTime-start - return res - } - - def fillSolutionCopy(Map trace) { - //No need to do a final check to fill if we are using a strategy - if (strategy === ExplorationStrategy.CrossingScenario) return - val model = threadContext.getModel as PartialInterpretation - val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList - if(constraint2CurrentUnitPropagationPrecondition.empty) { - fillWithDefaultValues(dataObjects,trace) - } else { - val propagatedConstraints = new HashMap - for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { - val constraint = entry.key - val allMatches = entry.value.allMatches.map[it.toArray] - propagatedConstraints.put(constraint,allMatches) - } - - if(propagatedConstraints.values.forall[empty]) { - fillWithDefaultValues(dataObjects,trace) - } else { - val solution = t.delegateGetSolution(dataObjects,propagatedConstraints, "dreal") - fillWithSolutions(dataObjects,solution,trace) - } - } - } - - def protected fillWithDefaultValues(List elements, Map trace) { - for(element : elements) { - if(element.valueSet==false) { - val value = getDefaultValue(element) - val target = trace.get(element) as PrimitiveElement - target.fillWithValue(value) - } - } - } - - def protected dispatch getDefaultValue(BooleanElement e) {false} - def protected dispatch getDefaultValue(IntegerElement e) {0} - def protected dispatch getDefaultValue(RealElement e) {0.0} - def protected dispatch getDefaultValue(StringElement e) {""} - - def protected fillWithSolutions(List elements, Map solution, Map trace) { - for(element : elements) { - if(element.valueSet==false) { - if(solution.containsKey(element)) { - val value = solution.get(element) - val target = trace.get(element) as PrimitiveElement - target.fillWithValue(value) - } else { - val target = trace.get(element) as PrimitiveElement - target.fillWithValue(target.defaultValue) - } - } - } - } - - def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean} - 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) - } - } - } - } -} \ 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{ } builder } -} +} 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 { class SolutionCopier { val copiedSolutions = new LinkedHashMap - @Accessors NumericSolver numericSolver + @Accessors NumericRefinementUnit numericSolver long startTime = System.nanoTime @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 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 val ObjectiveComparatorHelper comparatorHelper val Map trajectories = new HashMap - @Accessors var NumericSolver numericSolver + @Accessors var NumericRefinementUnit numericSolver @Accessors var Map solutionsCollection new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) { @@ -45,7 +45,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsPro this.solutionCopier = new SolutionCopier } - def setNumericSolver(NumericSolver numericSolver) { + def setNumericSolver(NumericRefinementUnit numericSolver) { this.numericSolver = numericSolver solutionCopier.numericSolver = numericSolver } @@ -63,7 +63,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsPro if (!shouldSaveSolution(fitness, context)) { return false } - println("Found: " + fitness) + //println("Found: " + fitness) val dominatedTrajectories = newArrayList for (entry : trajectories.entrySet) { val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java index 6e0abd0b..5448d61a 100644 --- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java +++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java @@ -212,7 +212,7 @@ public class SolutionStore { unsavedSolutionCallbacks(context, solutionTrajectory); return; } - System.out.println("SAVING SOLUTION"); +// System.out.println("SAVING SOLUTION"); boolean solutionSaved = solutionSaver.saveSolution(context, id, solutionTrajectory); if (solutionSaved) { -- cgit v1.2.3-70-g09d2