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 | |
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')
3 files changed, 25 insertions, 6 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 => [ |
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 fbe6da9d..ebfd5d81 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 | |||
@@ -33,6 +33,11 @@ enum PunishSizeStrategy { | |||
33 | LARGER_IS_BETTER | 33 | LARGER_IS_BETTER |
34 | } | 34 | } |
35 | 35 | ||
36 | enum NumericSolverSelection { | ||
37 | DREAL, | ||
38 | Z3 | ||
39 | } | ||
40 | |||
36 | class ViatraReasonerConfiguration extends LogicSolverConfiguration { | 41 | class ViatraReasonerConfiguration extends LogicSolverConfiguration { |
37 | // public var Iterable<PQuery> existingQueries | 42 | // public var Iterable<PQuery> existingQueries |
38 | public var nameNewElements = false | 43 | public var nameNewElements = false |
@@ -70,6 +75,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
70 | public var nonContainmentWeight = 1 | 75 | public var nonContainmentWeight = 1 |
71 | public var unfinishedWFWeight = 1 | 76 | public var unfinishedWFWeight = 1 |
72 | public var calculateObjectCreationCosts = false | 77 | public var calculateObjectCreationCosts = false |
78 | public var numericSolverSelection = NumericSolverSelection.DREAL //currently defaulted to DREAL | ||
73 | 79 | ||
74 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( | 80 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( |
75 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) | 81 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) |
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) { |