diff options
Diffstat (limited to 'Solvers/VIATRA-Solver')
4 files changed, 30 insertions, 23 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml index 05e00983..6e4d96ca 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml | |||
@@ -1,14 +1,14 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?><plugin> | 1 | <?xml version="1.0" encoding="UTF-8"?><plugin> |
2 | <extension id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" point="org.eclipse.viatra.query.runtime.queryspecification"> | 2 | <extension id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" point="org.eclipse.viatra.query.runtime.queryspecification"> |
3 | <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis"> | 3 | <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis"> |
4 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.hasDefinedSupertype"/> | 4 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.hasDefinedSupertype"/> |
5 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.dontHaveDefinedSupertype"/> | 5 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.dontHaveDefinedSupertype"/> |
6 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeConstructor"/> | 6 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeConstructor"/> |
7 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementTarget"/> | 7 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementTarget"/> |
8 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleSuperType"/> | 8 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleSuperType"/> |
9 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleTopType"/> | 9 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleTopType"/> |
10 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementNegativeConstraint"/> | 10 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementNegativeConstraint"/> |
11 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementMayTypeNegativeConstraint"/> | 11 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementMayTypeNegativeConstraint"/> |
12 | </group> | 12 | </group> |
13 | </extension> | 13 | </extension> |
14 | </plugin> | 14 | </plugin> |
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 d386241d..ed04ae4a 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 | |||
@@ -165,8 +165,8 @@ class ViatraReasoner extends LogicReasoner { | |||
165 | val solverTime = System.nanoTime - solverStartTime | 165 | val solverTime = System.nanoTime - solverStartTime |
166 | viatraConfig.progressMonitor.workedSearchFinished | 166 | viatraConfig.progressMonitor.workedSearchFinished |
167 | 167 | ||
168 | //dreal teardown | 168 | //dreal docker teardown |
169 | if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL){ | 169 | if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL_DOCKER){ |
170 | (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown() | 170 | (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown() |
171 | } | 171 | } |
172 | 172 | ||
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 ebfd5d81..c0daaad2 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 | |||
@@ -34,7 +34,8 @@ enum PunishSizeStrategy { | |||
34 | } | 34 | } |
35 | 35 | ||
36 | enum NumericSolverSelection { | 36 | enum NumericSolverSelection { |
37 | DREAL, | 37 | DREAL_DOCKER, |
38 | DREAL_LOCAL, | ||
38 | Z3 | 39 | Z3 |
39 | } | 40 | } |
40 | 41 | ||
@@ -75,7 +76,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
75 | public var nonContainmentWeight = 1 | 76 | public var nonContainmentWeight = 1 |
76 | public var unfinishedWFWeight = 1 | 77 | public var unfinishedWFWeight = 1 |
77 | public var calculateObjectCreationCosts = false | 78 | public var calculateObjectCreationCosts = false |
78 | public var numericSolverSelection = NumericSolverSelection.DREAL //currently defaulted to DREAL | 79 | public var numericSolverSelection = NumericSolverSelection.DREAL_DOCKER //currently defaulted to DREAL |
80 | public var drealLocalPath = "<path-to-dreal>"; | ||
79 | 81 | ||
80 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( | 82 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( |
81 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) | 83 | 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 ab3e6601..9223ecc8 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 | |||
@@ -34,6 +34,7 @@ class NumericSolver { | |||
34 | val boolean intermediateConsistencyCheck | 34 | val boolean intermediateConsistencyCheck |
35 | val boolean caching; | 35 | val boolean caching; |
36 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap | 36 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap |
37 | val String drealLocalPath; | ||
37 | 38 | ||
38 | var long runtime = 0 | 39 | var long runtime = 0 |
39 | var long cachingTime = 0 | 40 | var long cachingTime = 0 |
@@ -43,12 +44,16 @@ class NumericSolver { | |||
43 | new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { | 44 | new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { |
44 | this.method = method | 45 | this.method = method |
45 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks | 46 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks |
46 | this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) | ||
47 | this.caching = caching | 47 | this.caching = caching |
48 | this.drealLocalPath = config.drealLocalPath | ||
49 | this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) | ||
48 | } | 50 | } |
49 | 51 | ||
50 | def createNumericTranslator(NumericSolverSelection solverSelection) { | 52 | def createNumericTranslator(NumericSolverSelection solverSelection) { |
51 | if (solverSelection == NumericSolverSelection.DREAL) return new NumericDrealProblemSolver | 53 | if (solverSelection == NumericSolverSelection.DREAL_DOCKER) |
54 | return new NumericDrealProblemSolver(true, null) | ||
55 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) | ||
56 | return new NumericDrealProblemSolver(false, drealLocalPath) | ||
52 | if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver | 57 | if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver |
53 | } | 58 | } |
54 | 59 | ||
@@ -98,12 +103,12 @@ class NumericSolver { | |||
98 | finalResult=true | 103 | finalResult=true |
99 | } else { | 104 | } else { |
100 | val propagatedConstraints = new HashMap | 105 | val propagatedConstraints = new HashMap |
101 | println("------ Any matches?") | 106 | println("<<<<START-STEP>>>>") |
102 | for(entry : matches.entrySet) { | 107 | for(entry : matches.entrySet) { |
103 | val constraint = entry.key | 108 | val constraint = entry.key |
104 | println("------ " + constraint) | 109 | // println("--match?-- " + constraint) |
105 | val allMatches = entry.value.allMatches.map[it.toArray] | 110 | val allMatches = entry.value.allMatches.map[it.toArray] |
106 | println("------ " + allMatches.toList) | 111 | // println("---------- " + entry.value.allMatches) |
107 | propagatedConstraints.put(constraint,allMatches) | 112 | propagatedConstraints.put(constraint,allMatches) |
108 | } | 113 | } |
109 | if(propagatedConstraints.values.forall[empty]) { | 114 | if(propagatedConstraints.values.forall[empty]) { |