From a8eb346fb97b54b6ee693da4840abd8be8b43843 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Sun, 14 Feb 2021 08:01:00 +0100 Subject: Add strategy flag + implement alost working crossingScenarioStrategy --- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 2 +- .../viatra2logic/NumericDrealProblemSolver.java | 46 +++++++++++++++------- .../viatra2logic/NumericDynamicProblemSolver.java | 41 +++++++++++++++++++ .../viatra2logic/NumericTranslator.xtend | 19 +++++---- 4 files changed, 85 insertions(+), 23 deletions(-) create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend index 9e11d2cf..ae94c327 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend @@ -21,7 +21,7 @@ class ExpressionEvaluation2Logic { def getNumericSolver() { if(_numericSolver === null) { // it seems like this getter has no use - _numericSolver = (new NumericTranslator(null)).selectProblemSolver + _numericSolver = (new NumericTranslator(null)).selectProblemSolver("z3") } return _numericSolver } diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java index e0ebcb6b..36ea64aa 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java @@ -43,8 +43,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ private Map curVar2Decl; private final int TIMEOUT_DOCKER = 5000; - private final int TIMEOUT_LOCAL = 10000; - private final boolean DEBUG_PRINT = false; + private final int TIMEOUT_LOCAL = 100000; + private final int DEBUG_PRINT = 3; public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { this.useDocker = useDocker; @@ -87,7 +87,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ } return null; } - if (DEBUG_PRINT) { + if (DEBUG_PRINT > 1) { double duration = (double) (System.nanoTime() - startTime) / 1000000000; System.out.println("Dur = " + duration + " : "); } @@ -404,11 +404,13 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ System.err.println("TIMEOUT"); // printOutput(numProbContent); } - if (DEBUG_PRINT) { - // printOutput(numProbContent); - // if (outputs != null) printOutput(outputs.get(0)); + if (DEBUG_PRINT > 1) { System.out.println(result); } + if (DEBUG_PRINT > 2) { + printOutput(numProbContent); + if (outputs != null) printOutput(outputs.get(0)); + } return result; } @@ -455,16 +457,30 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ Process outputProcess; if (this.useDocker) outputProcess = callDrealDocker(numProbContent, true); else outputProcess = callDrealLocal(numProbContent, true); - - List> outputs = getProcessOutput(outputProcess); - boolean result = getDrealResult(outputProcess.exitValue(), outputs); + + boolean result = false; + List> outputs = null; + if (outputProcess != null) { + outputs = getProcessOutput(outputProcess); + result = getDrealResult(outputProcess.exitValue(), outputs); + } + endSolvingProblem = System.nanoTime()-startSolvingProblem; - if (DEBUG_PRINT) { - System.out.println("Getting Solution!"); - // printOutput(numProbContent); - // printOutput(outputs.get(0)); - // System.out.println(result); + if (outputProcess == null) { + System.err.println("TIMEOUT"); +// printOutput(numProbContent); + } else { + if (DEBUG_PRINT > 0) { + System.out.println("Getting Solution!"); + } + } + if (DEBUG_PRINT > 1) { + System.out.println(result); + } + if (DEBUG_PRINT > 2) { + printOutput(numProbContent); + if (outputs != null) printOutput(outputs.get(0)); } //GET SOLUTION @@ -498,7 +514,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ endFormingSolution = System.nanoTime() - startFormingSolution; } else { - System.out.println("Unsatisfiable numerical problem"); + System.out.println("Unsatisfiable numerical problem (trying to get solution...)"); } return sol; } diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java new file mode 100644 index 00000000..bd4a10ff --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java @@ -0,0 +1,41 @@ +package hu.bme.mit.inf.dslreasoner.viatra2logic; + +import java.io.IOException; +import java.util.List; +import java.util.Map; + +import org.eclipse.xtext.common.types.JvmIdentifiableElement; +import org.eclipse.xtext.xbase.XExpression; + +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; + +public class NumericDynamicProblemSolver extends NumericProblemSolver{ + +// private NumericZ3ProblemSolver z3Solver; + private NumericDrealProblemSolver drealSolver; + + public NumericDynamicProblemSolver(String drealLocalPath) throws IOException, InterruptedException { +// this.z3Solver = new NumericZ3ProblemSolver(); + this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath); + } + + public NumericProblemSolver selectSolver(String selection) { + switch (selection) { + case "z3": + return new NumericZ3ProblemSolver(); + case "dreal": + return this.drealSolver; + default: + throw new IllegalArgumentException("Unknown numeric solver selection: " + selection); + } + } + + public boolean isSatisfiable(Map>> matches) + throws Exception { + throw new Exception("Should not reach here - isSatisfiable"); + } + + public Map getOneSolution(List objs, + Map>> matches) throws Exception { + throw new Exception("Should not reach here - getOneSolution"); + }} diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend index 3d3f2f4a..791dd644 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend @@ -56,24 +56,29 @@ class NumericTranslator { return res } - def NumericProblemSolver selectProblemSolver() { + def NumericProblemSolver selectProblemSolver(String selection) { // return new NumericProblemSolver // add numeric solver decision procedure here - if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver - return numericSolver; + if (numericSolver instanceof NumericDynamicProblemSolver) { + val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver + return dynamicSolver.selectSolver(selection); + } else{ + if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver + return numericSolver; + } } - def delegateIsSatisfiable(Map> matches) { + def delegateIsSatisfiable(Map> matches, String select) { val input = formNumericProblemInstance(matches) - val solver = selectProblemSolver + val solver = selectProblemSolver(select) val satisfiability = solver.isSatisfiable(input) solver.updateTimes return satisfiability } - def delegateGetSolution(List primitiveElements, Map> matches) { + def delegateGetSolution(List primitiveElements, Map> matches, String select) { val input = formNumericProblemInstance(matches) - val solver = selectProblemSolver + val solver = selectProblemSolver(select) val solution = solver.getOneSolution(primitiveElements,input) solver.updateTimes return solution -- cgit v1.2.3-70-g09d2