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/dse/NumericSolver.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/dse/NumericSolver.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | 18 |
1 files changed, 14 insertions, 4 deletions
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 0e789671..4b0ea544 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 | |||
@@ -1,6 +1,8 @@ | |||
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.NumericTranslator | 4 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator |
5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
@@ -8,6 +10,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
11 | import java.math.BigDecimal | 15 | import java.math.BigDecimal |
12 | import java.util.HashMap | 16 | import java.util.HashMap |
13 | import java.util.LinkedHashMap | 17 | import java.util.LinkedHashMap |
@@ -25,7 +29,7 @@ class NumericSolver { | |||
25 | var ThreadContext threadContext | 29 | var ThreadContext threadContext |
26 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 30 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
27 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 31 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
28 | NumericTranslator t = new NumericTranslator | 32 | NumericTranslator t |
29 | 33 | ||
30 | val boolean intermediateConsistencyCheck | 34 | val boolean intermediateConsistencyCheck |
31 | val boolean caching; | 35 | val boolean caching; |
@@ -36,12 +40,18 @@ class NumericSolver { | |||
36 | var int numberOfSolverCalls = 0 | 40 | var int numberOfSolverCalls = 0 |
37 | var int numberOfCachedSolverCalls = 0 | 41 | var int numberOfCachedSolverCalls = 0 |
38 | 42 | ||
39 | new(ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) { | 43 | new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { |
40 | this.method = method | 44 | this.method = method |
41 | this.intermediateConsistencyCheck = intermediateConsistencyCheck | 45 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks |
46 | this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) | ||
42 | this.caching = caching | 47 | this.caching = caching |
43 | } | 48 | } |
44 | 49 | ||
50 | def createNumericTranslator(NumericSolverSelection solverSelection) { | ||
51 | if (solverSelection == NumericSolverSelection.DREAL) return new NumericDrealProblemSolver | ||
52 | if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver | ||
53 | } | ||
54 | |||
45 | def init(ThreadContext context) { | 55 | def init(ThreadContext context) { |
46 | // This makes the NumericSolver single-threaded, | 56 | // This makes the NumericSolver single-threaded, |
47 | // but that's not a problem, because we only use the solver on a single thread anyways. | 57 | // but that's not a problem, because we only use the solver on a single thread anyways. |
@@ -68,7 +78,7 @@ class NumericSolver { | |||
68 | def getSolverFormingProblem(){this.t.formingProblemTime} | 78 | def getSolverFormingProblem(){this.t.formingProblemTime} |
69 | def getSolverSolvingProblem(){this.t.solvingProblemTime} | 79 | def getSolverSolvingProblem(){this.t.solvingProblemTime} |
70 | def getSolverSolution(){this.t.formingSolutionTime} | 80 | def getSolverSolution(){this.t.formingSolutionTime} |
71 | def getNumericDrealSolver(){this.t.drealSolver} | 81 | def getNumericSolverSelection(){this.t.numericSolver} |
72 | 82 | ||
73 | def boolean maySatisfiable() { | 83 | def boolean maySatisfiable() { |
74 | if(intermediateConsistencyCheck) { | 84 | if(intermediateConsistencyCheck) { |