diff options
author | 2020-12-15 13:18:17 -0500 | |
---|---|---|
committer | 2021-01-06 00:02:49 +0100 | |
commit | f5afda733ffdf4f52da932e03919c20b99bf7fa6 (patch) | |
tree | fc875240bafc47c02e19d22b32e4c5a99fcfd941 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | |
parent | implement getOneSolution with Dreal Integration (diff) | |
download | VIATRA-Generator-f5afda733ffdf4f52da932e03919c20b99bf7fa6.tar.gz VIATRA-Generator-f5afda733ffdf4f52da932e03919c20b99bf7fa6.tar.zst VIATRA-Generator-f5afda733ffdf4f52da932e03919c20b99bf7fa6.zip |
Add config flag for selecting numeric solver. Integ with Z3
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | 7 |
1 files changed, 5 insertions, 2 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 1f902b90..144e5e6f 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 | |||
@@ -38,6 +38,7 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer | |||
38 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel | 38 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel |
39 | import org.eclipse.viatra.dse.solutionstore.SolutionStore | 39 | import org.eclipse.viatra.dse.solutionstore.SolutionStore |
40 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory | 40 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory |
41 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver | ||
41 | 42 | ||
42 | class ViatraReasoner extends LogicReasoner { | 43 | class ViatraReasoner extends LogicReasoner { |
43 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() | 44 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() |
@@ -109,7 +110,7 @@ class ViatraReasoner extends LogicReasoner { | |||
109 | new SolutionStore(numberOfRequiredSolutions) | 110 | new SolutionStore(numberOfRequiredSolutions) |
110 | } | 111 | } |
111 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) | 112 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) |
112 | val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) | 113 | val numericSolver = new NumericSolver(method, viatraConfig, false) |
113 | val solutionSaver = method.solutionSaver | 114 | val solutionSaver = method.solutionSaver |
114 | solutionSaver.numericSolver = numericSolver | 115 | solutionSaver.numericSolver = numericSolver |
115 | val solutionCopier = solutionSaver.solutionCopier | 116 | val solutionCopier = solutionSaver.solutionCopier |
@@ -165,7 +166,9 @@ class ViatraReasoner extends LogicReasoner { | |||
165 | viatraConfig.progressMonitor.workedSearchFinished | 166 | viatraConfig.progressMonitor.workedSearchFinished |
166 | 167 | ||
167 | //dreal teardown | 168 | //dreal teardown |
168 | numericSolver.numericDrealSolver.teardown() | 169 | if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL){ |
170 | (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown() | ||
171 | } | ||
169 | 172 | ||
170 | // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches | 173 | // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches |
171 | val statistics = createStatistics => [ | 174 | val statistics = createStatistics => [ |