diff options
author | 2021-02-16 03:06:22 +0100 | |
---|---|---|
committer | 2021-02-16 03:06:22 +0100 | |
commit | 0ebddc8dd265cd5b1b439e3c06f1de1047641559 (patch) | |
tree | 7141673072f4d6a48a9b12d23b9f01261717a8f7 /Solvers/VIATRA-Solver | |
parent | Ready for strategies case study (diff) | |
download | VIATRA-Generator-0ebddc8dd265cd5b1b439e3c06f1de1047641559.tar.gz VIATRA-Generator-0ebddc8dd265cd5b1b439e3c06f1de1047641559.tar.zst VIATRA-Generator-0ebddc8dd265cd5b1b439e3c06f1de1047641559.zip |
add dreal-timeout flag
Diffstat (limited to 'Solvers/VIATRA-Solver')
2 files changed, 4 insertions, 3 deletions
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 74388706..923c847e 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 | |||
@@ -85,6 +85,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
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 drealLocalPath = "<path-to-dreal>"; | 87 | public var drealLocalPath = "<path-to-dreal>"; |
88 | public var drealTimeout = 10000; | ||
88 | public var Map<String, Map<String, String>> ignoredAttributesMap = null; | 89 | public var Map<String, Map<String, String>> ignoredAttributesMap = null; |
89 | public var ExplorationStrategy strategy = ExplorationStrategy.None | 90 | public var ExplorationStrategy strategy = ExplorationStrategy.None |
90 | 91 | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index 28edff41..8281c3c3 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | |||
@@ -64,9 +64,9 @@ class NumericSolver { | |||
64 | if (strategy == ExplorationStrategy.None) { | 64 | if (strategy == ExplorationStrategy.None) { |
65 | //initialise the specified | 65 | //initialise the specified |
66 | if (solverSelection == NumericSolverSelection.DREAL_DOCKER) | 66 | if (solverSelection == NumericSolverSelection.DREAL_DOCKER) |
67 | return new NumericDrealProblemSolver(true, null) | 67 | return new NumericDrealProblemSolver(true, null, config.drealTimeout) |
68 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) | 68 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) |
69 | return new NumericDrealProblemSolver(false, drealLocalPath) | 69 | return new NumericDrealProblemSolver(false, drealLocalPath, config.drealTimeout) |
70 | if (solverSelection == NumericSolverSelection.Z3) { | 70 | if (solverSelection == NumericSolverSelection.Z3) { |
71 | //TODO THIS IS HARD-CODED for now | 71 | //TODO THIS IS HARD-CODED for now |
72 | // val root = "/data/viatra/VIATRA-Generator"; | 72 | // val root = "/data/viatra/VIATRA-Generator"; |
@@ -90,7 +90,7 @@ class NumericSolver { | |||
90 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); | 90 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); |
91 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); | 91 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); |
92 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | 92 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); |
93 | return new NumericDynamicProblemSolver(drealLocalPath) | 93 | return new NumericDynamicProblemSolver(drealLocalPath, config.drealTimeout) |
94 | } | 94 | } |
95 | } | 95 | } |
96 | 96 | ||