diff options
author | 2019-07-14 00:56:19 +0200 | |
---|---|---|
committer | 2019-07-14 00:56:19 +0200 | |
commit | fc505b6b171a2d54c3bad6078031b028b55131d3 (patch) | |
tree | 8eaa033e053e21ca60bd7f958055cc46e93b7cba /Solvers/VIATRA-Solver | |
parent | Try fix statecode bug (diff) | |
download | VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.tar.gz VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.tar.zst VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.zip |
Polyhedron abstraction with Z3 for cardinality propagation
Diffstat (limited to 'Solvers/VIATRA-Solver')
9 files changed, 563 insertions, 72 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF index b2ee3981..37495e50 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF | |||
@@ -4,6 +4,7 @@ Bundle-Name: Logic2viatra | |||
4 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;singleton:=true | 4 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;singleton:=true |
5 | Bundle-Version: 1.0.0.qualifier | 5 | Bundle-Version: 1.0.0.qualifier |
6 | Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra, | 6 | Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra, |
7 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality, | ||
7 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval, | 8 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval, |
8 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators, | 9 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators, |
9 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, | 10 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, |
@@ -22,7 +23,8 @@ Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | |||
22 | com.google.inject;bundle-version="3.0.0", | 23 | com.google.inject;bundle-version="3.0.0", |
23 | org.eclipse.xtext;bundle-version="2.10.0", | 24 | org.eclipse.xtext;bundle-version="2.10.0", |
24 | org.eclipse.viatra.transformation.runtime.emf;bundle-version="1.5.0", | 25 | org.eclipse.viatra.transformation.runtime.emf;bundle-version="1.5.0", |
25 | org.eclipse.xtext.xbase;bundle-version="2.10.0" | 26 | org.eclipse.xtext.xbase;bundle-version="2.10.0", |
27 | com.microsoft.z3;bundle-version="4.8.5" | ||
26 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 | 28 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 |
27 | Import-Package: org.apache.log4j | 29 | Import-Package: org.apache.log4j |
28 | Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery | 30 | Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index b6918294..0040dbcd 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend | |||
@@ -4,6 +4,11 @@ import com.google.common.collect.ImmutableMap | |||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | 6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | 14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider |
@@ -63,7 +68,7 @@ class ModelGenerationMethodProvider { | |||
63 | ReasonerWorkspace workspace, | 68 | ReasonerWorkspace workspace, |
64 | boolean nameNewElements, | 69 | boolean nameNewElements, |
65 | TypeInferenceMethod typeInferenceMethod, | 70 | TypeInferenceMethod typeInferenceMethod, |
66 | ScopePropagator scopePropagator, | 71 | ScopePropagatorStrategy scopePropagatorStrategy, |
67 | DocumentationLevel debugLevel | 72 | DocumentationLevel debugLevel |
68 | ) { | 73 | ) { |
69 | val statistics = new ModelGenerationStatistics | 74 | val statistics = new ModelGenerationStatistics |
@@ -74,6 +79,8 @@ class ModelGenerationMethodProvider { | |||
74 | 79 | ||
75 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | 80 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, |
76 | workspace, typeInferenceMethod, writeFiles) | 81 | workspace, typeInferenceMethod, writeFiles) |
82 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries) | ||
83 | scopePropagator.propagateAllScopeConstraints | ||
77 | val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> | 84 | val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> |
78 | objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, | 85 | objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, |
79 | nameNewElements, statistics) | 86 | nameNewElements, statistics) |
@@ -104,4 +111,19 @@ class ModelGenerationMethodProvider { | |||
104 | queries.allQueries | 111 | queries.allQueries |
105 | ) | 112 | ) |
106 | } | 113 | } |
114 | |||
115 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | ||
116 | PartialInterpretation emptySolution, GeneratedPatterns queries) { | ||
117 | switch (scopePropagatorStrategy) { | ||
118 | case BasicTypeHierarchy: | ||
119 | new ScopePropagator(emptySolution) | ||
120 | case PolyhedralTypeHierarchy: { | ||
121 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | ||
122 | val solver = new Z3PolyhedronSolver | ||
123 | new PolyhedronScopePropagator(emptySolution, types, solver) | ||
124 | } | ||
125 | default: | ||
126 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) | ||
127 | } | ||
128 | } | ||
107 | } | 129 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend new file mode 100644 index 00000000..8f210ffb --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | |||
@@ -0,0 +1,153 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableMap | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
10 | import java.util.ArrayDeque | ||
11 | import java.util.HashMap | ||
12 | import java.util.HashSet | ||
13 | import java.util.Map | ||
14 | import java.util.Set | ||
15 | |||
16 | class PolyhedronScopePropagator extends ScopePropagator { | ||
17 | val Map<Scope, LinearBoundedExpression> scopeBounds | ||
18 | val LinearConstraint topLevelBounds | ||
19 | val PolyhedronSaturationOperator operator | ||
20 | |||
21 | new(PartialInterpretation p, Set<? extends Type> possibleNewDynamicTypes, PolyhedronSolver solver) { | ||
22 | super(p) | ||
23 | val instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] | ||
24 | val primitiveDimensions = new HashMap | ||
25 | val constraintsBuilder = ImmutableList.builder | ||
26 | val scopeBoundsBuilder = ImmutableMap.builder | ||
27 | // Dimensions for instantiable types were created according to the type analysis, | ||
28 | // but for any possible primitive types, we create them on demand, | ||
29 | // as there is no Type directly associated with a PartialPrimitiveInterpretation. | ||
30 | for (scope : p.scopes) { | ||
31 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { | ||
32 | PartialPrimitiveInterpretation: { | ||
33 | val dimension = primitiveDimensions.computeIfAbsent(targetTypeInterpretation) [ interpretation | | ||
34 | new Dimension(interpretation.eClass.name, 0, null) | ||
35 | ] | ||
36 | scopeBoundsBuilder.put(scope, dimension) | ||
37 | } | ||
38 | PartialComplexTypeInterpretation: { | ||
39 | val complexType = targetTypeInterpretation.interpretationOf | ||
40 | val dimensions = findSubtypeDimensions(complexType, instanceCounts) | ||
41 | switch (dimensions.size) { | ||
42 | case 0: | ||
43 | if (scope.minNewElements > 0) { | ||
44 | throw new IllegalArgumentException("Found scope for " + complexType.name + | ||
45 | ", but the type cannot be instantiated") | ||
46 | } | ||
47 | case 1: | ||
48 | scopeBoundsBuilder.put(scope, dimensions.head) | ||
49 | default: { | ||
50 | val constraint = new LinearConstraint(dimensions.toInvertedMap[1], null, null) | ||
51 | constraintsBuilder.add(constraint) | ||
52 | scopeBoundsBuilder.put(scope, constraint) | ||
53 | } | ||
54 | } | ||
55 | } | ||
56 | default: | ||
57 | throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + targetTypeInterpretation) | ||
58 | } | ||
59 | } | ||
60 | val allDimensions = ImmutableList.builder.addAll(instanceCounts.values).addAll(primitiveDimensions.values).build | ||
61 | scopeBounds = scopeBoundsBuilder.build | ||
62 | topLevelBounds = new LinearConstraint(allDimensions.toInvertedMap[1], null, null) | ||
63 | constraintsBuilder.add(topLevelBounds) | ||
64 | val expressionsToSaturate = ImmutableList.builder.addAll(scopeBounds.values).add(topLevelBounds).build | ||
65 | val polyhedron = new Polyhedron(allDimensions, constraintsBuilder.build, expressionsToSaturate) | ||
66 | operator = solver.createSaturationOperator(polyhedron) | ||
67 | } | ||
68 | |||
69 | private def findSubtypeDimensions(Type type, Map<Type, Dimension> instanceCounts) { | ||
70 | val subtypes = new HashSet | ||
71 | val dimensions = new HashSet | ||
72 | val stack = new ArrayDeque | ||
73 | stack.addLast(type) | ||
74 | while (!stack.empty) { | ||
75 | val subtype = stack.removeLast | ||
76 | if (subtypes.add(subtype)) { | ||
77 | val dimension = instanceCounts.get(subtype) | ||
78 | if (dimension !== null) { | ||
79 | dimensions.add(dimension) | ||
80 | } | ||
81 | stack.addAll(subtype.subtypes) | ||
82 | } | ||
83 | } | ||
84 | dimensions | ||
85 | } | ||
86 | |||
87 | override void propagateAllScopeConstraints() { | ||
88 | populatePolyhedronFromScope() | ||
89 | val result = operator.saturate() | ||
90 | if (result == PolyhedronSaturationResult.EMPTY) { | ||
91 | throw new IllegalStateException("Scope bounds cannot be satisfied") | ||
92 | } else { | ||
93 | populateScopesFromPolyhedron() | ||
94 | if (result != PolyhedronSaturationResult.SATURATED) { | ||
95 | super.propagateAllScopeConstraints() | ||
96 | } | ||
97 | } | ||
98 | } | ||
99 | |||
100 | private def populatePolyhedronFromScope() { | ||
101 | topLevelBounds.lowerBound = partialInterpretation.minNewElements | ||
102 | if (partialInterpretation.maxNewElements >= 0) { | ||
103 | topLevelBounds.upperBound = partialInterpretation.maxNewElements | ||
104 | } | ||
105 | for (pair : scopeBounds.entrySet) { | ||
106 | val scope = pair.key | ||
107 | val bounds = pair.value | ||
108 | bounds.lowerBound = scope.minNewElements | ||
109 | if (scope.maxNewElements >= 0) { | ||
110 | bounds.upperBound = scope.maxNewElements | ||
111 | } | ||
112 | } | ||
113 | } | ||
114 | |||
115 | private def populateScopesFromPolyhedron() { | ||
116 | checkFiniteBounds(topLevelBounds) | ||
117 | if (partialInterpretation.minNewElements > topLevelBounds.lowerBound) { | ||
118 | throw new IllegalArgumentException('''Lower bound of «topLevelBounds» smaller than top-level scope: «partialInterpretation.minNewElements»''') | ||
119 | } else if (partialInterpretation.minNewElements != topLevelBounds.lowerBound) { | ||
120 | partialInterpretation.minNewElements = topLevelBounds.lowerBound | ||
121 | } | ||
122 | if (partialInterpretation.maxNewElements >= 0 && | ||
123 | partialInterpretation.maxNewElements < topLevelBounds.upperBound) { | ||
124 | throw new IllegalArgumentException('''Upper bound of «topLevelBounds» larger than top-level scope: «partialInterpretation.maxNewElements»''') | ||
125 | } else if (partialInterpretation.maxNewElements != topLevelBounds.upperBound) { | ||
126 | partialInterpretation.maxNewElements = topLevelBounds.upperBound | ||
127 | } | ||
128 | for (pair : scopeBounds.entrySet) { | ||
129 | val scope = pair.key | ||
130 | val bounds = pair.value | ||
131 | checkFiniteBounds(bounds) | ||
132 | if (scope.minNewElements > bounds.lowerBound) { | ||
133 | throw new IllegalArgumentException('''Lower bound of «bounds» smaller than «scope.targetTypeInterpretation» scope: «scope.minNewElements»''') | ||
134 | } else if (scope.minNewElements != bounds.lowerBound) { | ||
135 | scope.minNewElements = bounds.lowerBound | ||
136 | } | ||
137 | if (scope.maxNewElements >= 0 && scope.maxNewElements < bounds.upperBound) { | ||
138 | throw new IllegalArgumentException('''Upper bound of «bounds» larger than «scope.targetTypeInterpretation» scope: «scope.maxNewElements»''') | ||
139 | } else if (scope.maxNewElements != bounds.upperBound) { | ||
140 | scope.maxNewElements = bounds.upperBound | ||
141 | } | ||
142 | } | ||
143 | } | ||
144 | |||
145 | private def checkFiniteBounds(LinearBoundedExpression bounds) { | ||
146 | if (bounds.lowerBound === null) { | ||
147 | throw new IllegalArgumentException("Infinite lower bound: " + bounds) | ||
148 | } | ||
149 | if (bounds.upperBound === null) { | ||
150 | throw new IllegalArgumentException("Infinite upper bound: " + bounds) | ||
151 | } | ||
152 | } | ||
153 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend new file mode 100644 index 00000000..08bf25b9 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend | |||
@@ -0,0 +1,115 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import java.util.List | ||
4 | import java.util.Map | ||
5 | import org.eclipse.xtend.lib.annotations.Accessors | ||
6 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
7 | |||
8 | interface PolyhedronSolver { | ||
9 | def PolyhedronSaturationOperator createSaturationOperator(Polyhedron polyhedron) | ||
10 | } | ||
11 | |||
12 | enum PolyhedronSaturationResult { | ||
13 | SATURATED, | ||
14 | EMPTY, | ||
15 | UNKNOWN | ||
16 | } | ||
17 | |||
18 | interface PolyhedronSaturationOperator extends AutoCloseable { | ||
19 | def Polyhedron getPolyhedron() | ||
20 | |||
21 | def PolyhedronSaturationResult saturate() | ||
22 | } | ||
23 | |||
24 | @FinalFieldsConstructor | ||
25 | @Accessors | ||
26 | class Polyhedron { | ||
27 | /** | ||
28 | * The list of dimensions (variables) for this polyhedron. | ||
29 | * | ||
30 | * This list must not be modified after the polyhedron was created. | ||
31 | * However, lower and upper bounds of the dimensions may be changed. | ||
32 | * | ||
33 | * Names of dimensions in this list are assumed to be unique. | ||
34 | */ | ||
35 | val List<Dimension> dimensions | ||
36 | |||
37 | /** | ||
38 | * The list of constraints defining this polyhedron. | ||
39 | * | ||
40 | * The list and its elements may be freely modified. | ||
41 | */ | ||
42 | val List<LinearConstraint> constraints | ||
43 | |||
44 | /** | ||
45 | * The list of constraints that should be saturated (tightened) | ||
46 | * when a {@link PolyhedronSaturationOperator} is invoked. | ||
47 | * | ||
48 | * This list may be freely modified. | ||
49 | * | ||
50 | * Place all dimensions and constraints here to saturate all the bounds. | ||
51 | */ | ||
52 | val List<LinearBoundedExpression> expressionsToSaturate | ||
53 | |||
54 | override toString() ''' | ||
55 | Dimensions: | ||
56 | «FOR dimension : dimensions» | ||
57 | «dimension» | ||
58 | «ENDFOR» | ||
59 | Constraints: | ||
60 | «FOR constraint : constraints» | ||
61 | «constraint» | ||
62 | «ENDFOR» | ||
63 | ««« Saturate: | ||
64 | ««« «FOR expression : expressionsToSaturate» | ||
65 | ««« «IF expression instanceof Dimension»dimension«ELSEIF expression instanceof LinearConstraint»constraint«ELSE»unknown«ENDIF» «expression» | ||
66 | ««« «ENDFOR» | ||
67 | ''' | ||
68 | |||
69 | } | ||
70 | |||
71 | @Accessors | ||
72 | abstract class LinearBoundedExpression { | ||
73 | var Integer lowerBound | ||
74 | var Integer upperBound | ||
75 | } | ||
76 | |||
77 | @Accessors | ||
78 | class Dimension extends LinearBoundedExpression { | ||
79 | val String name | ||
80 | |||
81 | @FinalFieldsConstructor | ||
82 | new() { | ||
83 | } | ||
84 | |||
85 | new(String name, Integer lowerBound, Integer upperBound) { | ||
86 | this(name) | ||
87 | this.lowerBound = lowerBound | ||
88 | this.upperBound = upperBound | ||
89 | } | ||
90 | |||
91 | override toString() { | ||
92 | '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«name»«IF upperBound !== null» <= «upperBound»«ENDIF»''' | ||
93 | } | ||
94 | |||
95 | } | ||
96 | |||
97 | @Accessors | ||
98 | class LinearConstraint extends LinearBoundedExpression { | ||
99 | val Map<Dimension, Integer> coefficients | ||
100 | |||
101 | @FinalFieldsConstructor | ||
102 | new() { | ||
103 | } | ||
104 | |||
105 | new(Map<Dimension, Integer> coefficients, Integer lowerBound, Integer upperBound) { | ||
106 | this(coefficients) | ||
107 | this.lowerBound = lowerBound | ||
108 | this.upperBound = upperBound | ||
109 | } | ||
110 | |||
111 | override toString() { | ||
112 | '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«FOR pair : coefficients.entrySet SEPARATOR " + "»«IF pair.value != 1»«pair.value» * «ENDIF»«pair.key.name»«ENDFOR»«IF upperBound !== null» <= «upperBound»«ENDIF»''' | ||
113 | } | ||
114 | |||
115 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend index 38633c07..c8fb3409 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend | |||
@@ -1,40 +1,46 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope |
6 | import java.util.HashMap | 7 | import java.util.HashMap |
8 | import java.util.HashSet | ||
7 | import java.util.Map | 9 | import java.util.Map |
8 | import java.util.Set | 10 | import java.util.Set |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | 11 | import org.eclipse.xtend.lib.annotations.Accessors |
10 | import java.util.HashSet | 12 | |
13 | enum ScopePropagatorStrategy { | ||
14 | BasicTypeHierarchy, | ||
15 | PolyhedralTypeHierarchy | ||
16 | } | ||
11 | 17 | ||
12 | class ScopePropagator { | 18 | class ScopePropagator { |
13 | PartialInterpretation partialInterpretation | 19 | @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation |
14 | Map<PartialTypeInterpratation,Scope> type2Scope | 20 | Map<PartialTypeInterpratation, Scope> type2Scope |
15 | 21 | ||
16 | val Map<Scope, Set<Scope>> superScopes | 22 | val Map<Scope, Set<Scope>> superScopes |
17 | val Map<Scope, Set<Scope>> subScopes | 23 | val Map<Scope, Set<Scope>> subScopes |
18 | 24 | ||
19 | public new(PartialInterpretation p) { | 25 | new(PartialInterpretation p) { |
20 | partialInterpretation = p | 26 | partialInterpretation = p |
21 | type2Scope = new HashMap | 27 | type2Scope = new HashMap |
22 | for(scope : p.scopes) { | 28 | for (scope : p.scopes) { |
23 | type2Scope.put(scope.targetTypeInterpretation,scope) | 29 | type2Scope.put(scope.targetTypeInterpretation, scope) |
24 | } | 30 | } |
25 | 31 | ||
26 | superScopes = new HashMap | 32 | superScopes = new HashMap |
27 | subScopes = new HashMap | 33 | subScopes = new HashMap |
28 | for(scope : p.scopes) { | 34 | for (scope : p.scopes) { |
29 | superScopes.put(scope,new HashSet) | 35 | superScopes.put(scope, new HashSet) |
30 | subScopes.put(scope,new HashSet) | 36 | subScopes.put(scope, new HashSet) |
31 | } | 37 | } |
32 | 38 | ||
33 | for(scope : p.scopes) { | 39 | for (scope : p.scopes) { |
34 | val target = scope.targetTypeInterpretation | 40 | val target = scope.targetTypeInterpretation |
35 | if(target instanceof PartialComplexTypeInterpretation) { | 41 | if (target instanceof PartialComplexTypeInterpretation) { |
36 | val supertypeInterpretations = target.supertypeInterpretation | 42 | val supertypeInterpretations = target.supertypeInterpretation |
37 | for(supertypeInterpretation : supertypeInterpretations) { | 43 | for (supertypeInterpretation : supertypeInterpretations) { |
38 | val supertypeScope = type2Scope.get(supertypeInterpretation) | 44 | val supertypeScope = type2Scope.get(supertypeInterpretation) |
39 | superScopes.get(scope).add(supertypeScope) | 45 | superScopes.get(scope).add(supertypeScope) |
40 | subScopes.get(supertypeScope).add(scope) | 46 | subScopes.get(supertypeScope).add(scope) |
@@ -42,70 +48,57 @@ class ScopePropagator { | |||
42 | } | 48 | } |
43 | } | 49 | } |
44 | } | 50 | } |
45 | 51 | ||
46 | def public propagateAllScopeConstraints() { | 52 | def propagateAllScopeConstraints() { |
47 | var boolean hadChanged | 53 | var boolean hadChanged |
48 | do{ | 54 | do { |
49 | hadChanged = false | 55 | hadChanged = false |
50 | for(superScopeEntry : superScopes.entrySet) { | 56 | for (superScopeEntry : superScopes.entrySet) { |
51 | val sub = superScopeEntry.key | 57 | val sub = superScopeEntry.key |
52 | hadChanged = propagateLowerLimitUp(sub,partialInterpretation) || hadChanged | 58 | hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged |
53 | hadChanged = propagateUpperLimitDown(sub,partialInterpretation) || hadChanged | 59 | hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged |
54 | for(sup: superScopeEntry.value) { | 60 | for (sup : superScopeEntry.value) { |
55 | hadChanged = propagateLowerLimitUp(sub,sup) || hadChanged | 61 | hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged |
56 | hadChanged = propagateUpperLimitDown(sub,sup) || hadChanged | 62 | hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged |
57 | } | 63 | } |
58 | } | 64 | } |
59 | } while(hadChanged) | 65 | } while (hadChanged) |
60 | // println('''All constraints are propagated.''') | ||
61 | } | 66 | } |
62 | 67 | ||
63 | def public propagateAdditionToType(PartialTypeInterpratation t) { | 68 | def propagateAdditionToType(PartialTypeInterpratation t) { |
64 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | 69 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') |
65 | val targetScope = type2Scope.get(t) | 70 | val targetScope = type2Scope.get(t) |
66 | targetScope.removeOne | 71 | targetScope.removeOne |
67 | val sups = superScopes.get(targetScope) | 72 | val sups = superScopes.get(targetScope) |
68 | sups.forEach[removeOne] | 73 | sups.forEach[removeOne] |
69 | if(this.partialInterpretation.minNewElements > 0) { | 74 | if (this.partialInterpretation.minNewElements > 0) { |
70 | this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1 | 75 | this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 |
71 | } | 76 | } |
72 | if(this.partialInterpretation.maxNewElements > 0) { | 77 | if (this.partialInterpretation.maxNewElements > 0) { |
73 | this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1 | 78 | this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 |
74 | } else if(this.partialInterpretation.maxNewElements === 0) { | 79 | } else if (this.partialInterpretation.maxNewElements === 0) { |
75 | throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') | 80 | throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') |
76 | } | 81 | } |
77 | |||
78 | // subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)] | ||
79 | // for(sup: sups) { | ||
80 | // subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)] | ||
81 | // } | ||
82 | // for(scope : type2Scope.values) { | ||
83 | // propagateUpperLimitDown(scope,partialInterpretation) | ||
84 | // } | ||
85 | |||
86 | propagateAllScopeConstraints | 82 | propagateAllScopeConstraints |
87 | 83 | ||
88 | // println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') | 84 | // println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') |
89 | // println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') | 85 | // println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') |
90 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] | 86 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] |
91 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | 87 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') |
92 | } | 88 | } |
93 | 89 | ||
94 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { | 90 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { |
95 | if(subScope.minNewElements>superScope.minNewElements) { | 91 | if (subScope.minNewElements > superScope.minNewElements) { |
96 | // println(''' | ||
97 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» | ||
98 | // superScope.minNewElements «superScope.minNewElements» = subScope.minNewElements «subScope.minNewElements» | ||
99 | // ''') | ||
100 | superScope.minNewElements = subScope.minNewElements | 92 | superScope.minNewElements = subScope.minNewElements |
101 | return true | 93 | return true |
102 | } else { | 94 | } else { |
103 | return false | 95 | return false |
104 | } | 96 | } |
105 | } | 97 | } |
106 | 98 | ||
107 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { | 99 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { |
108 | if(superScope.maxNewElements>=0 && (superScope.maxNewElements<subScope.maxNewElements || subScope.maxNewElements<0)) { | 100 | if (superScope.maxNewElements >= 0 && |
101 | (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { | ||
109 | // println(''' | 102 | // println(''' |
110 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» | 103 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» |
111 | // subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» | 104 | // subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» |
@@ -116,9 +109,9 @@ class ScopePropagator { | |||
116 | return false | 109 | return false |
117 | } | 110 | } |
118 | } | 111 | } |
119 | 112 | ||
120 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { | 113 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { |
121 | if(subScope.minNewElements>p.minNewElements) { | 114 | if (subScope.minNewElements > p.minNewElements) { |
122 | // println(''' | 115 | // println(''' |
123 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | 116 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes |
124 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» | 117 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» |
@@ -129,9 +122,9 @@ class ScopePropagator { | |||
129 | return false | 122 | return false |
130 | } | 123 | } |
131 | } | 124 | } |
132 | 125 | ||
133 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { | 126 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { |
134 | if(p.maxNewElements>=0 && (p.maxNewElements<subScope.maxNewElements || subScope.maxNewElements<0)) { | 127 | if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { |
135 | // println(''' | 128 | // println(''' |
136 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | 129 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes |
137 | // subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» | 130 | // subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» |
@@ -142,15 +135,15 @@ class ScopePropagator { | |||
142 | return false | 135 | return false |
143 | } | 136 | } |
144 | } | 137 | } |
138 | |||
145 | private def removeOne(Scope scope) { | 139 | private def removeOne(Scope scope) { |
146 | if(scope.maxNewElements===0) { | 140 | if (scope.maxNewElements === 0) { |
147 | throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') | 141 | throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') |
148 | } else if(scope.maxNewElements>0) { | 142 | } else if (scope.maxNewElements > 0) { |
149 | scope.maxNewElements= scope.maxNewElements-1 | 143 | scope.maxNewElements = scope.maxNewElements - 1 |
150 | } | 144 | } |
151 | if(scope.minNewElements>0) { | 145 | if (scope.minNewElements > 0) { |
152 | scope.minNewElements= scope.minNewElements-1 | 146 | scope.minNewElements = scope.minNewElements - 1 |
153 | } | 147 | } |
154 | } | 148 | } |
155 | } | 149 | } |
156 | \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend new file mode 100644 index 00000000..f1a84f2d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend | |||
@@ -0,0 +1,206 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.microsoft.z3.ArithExpr | ||
4 | import com.microsoft.z3.Context | ||
5 | import com.microsoft.z3.Expr | ||
6 | import com.microsoft.z3.IntNum | ||
7 | import com.microsoft.z3.Optimize | ||
8 | import com.microsoft.z3.Status | ||
9 | import com.microsoft.z3.Symbol | ||
10 | import java.util.Map | ||
11 | import org.eclipse.xtend.lib.annotations.Accessors | ||
12 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
13 | |||
14 | class Z3PolyhedronSolver implements PolyhedronSolver { | ||
15 | val boolean lpRelaxation | ||
16 | |||
17 | @FinalFieldsConstructor | ||
18 | new() { | ||
19 | } | ||
20 | |||
21 | new() { | ||
22 | this(true) | ||
23 | } | ||
24 | |||
25 | override createSaturationOperator(Polyhedron polyhedron) { | ||
26 | new Z3SaturationOperator(polyhedron, lpRelaxation) | ||
27 | } | ||
28 | } | ||
29 | |||
30 | class Z3SaturationOperator implements PolyhedronSaturationOperator { | ||
31 | static val INFINITY_SYMBOL_NAME = "oo" | ||
32 | static val MULT_SYMBOL_NAME = "*" | ||
33 | |||
34 | extension val Context context | ||
35 | val Symbol infinitySymbol | ||
36 | val Symbol multSymbol | ||
37 | @Accessors val Polyhedron polyhedron | ||
38 | val Map<Dimension, ArithExpr> variables | ||
39 | |||
40 | new(Polyhedron polyhedron, boolean lpRelaxation) { | ||
41 | context = new Context | ||
42 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) | ||
43 | multSymbol = context.mkSymbol(MULT_SYMBOL_NAME) | ||
44 | this.polyhedron = polyhedron | ||
45 | variables = polyhedron.dimensions.toInvertedMap [ dimension | | ||
46 | val name = dimension.name | ||
47 | if (lpRelaxation) { | ||
48 | mkRealConst(name) | ||
49 | } else { | ||
50 | mkIntConst(name) | ||
51 | } | ||
52 | ] | ||
53 | } | ||
54 | |||
55 | override saturate() { | ||
56 | val status = doSaturate() | ||
57 | convertStatusToSaturationResult(status) | ||
58 | } | ||
59 | |||
60 | private def convertStatusToSaturationResult(Status status) { | ||
61 | switch (status) { | ||
62 | case SATISFIABLE: | ||
63 | PolyhedronSaturationResult.SATURATED | ||
64 | case UNSATISFIABLE: | ||
65 | PolyhedronSaturationResult.EMPTY | ||
66 | case UNKNOWN: | ||
67 | PolyhedronSaturationResult.UNKNOWN | ||
68 | default: | ||
69 | throw new IllegalArgumentException("Unknown Status: " + status) | ||
70 | } | ||
71 | } | ||
72 | |||
73 | private def doSaturate() { | ||
74 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { | ||
75 | val expr = expressionToSaturate.toExpr | ||
76 | val lowerResult = saturateLowerBound(expr, expressionToSaturate) | ||
77 | if (lowerResult != Status.SATISFIABLE) { | ||
78 | return lowerResult | ||
79 | } | ||
80 | val upperResult = saturateUpperBound(expr, expressionToSaturate) | ||
81 | if (upperResult != Status.SATISFIABLE) { | ||
82 | return upperResult | ||
83 | } | ||
84 | } | ||
85 | Status.SATISFIABLE | ||
86 | } | ||
87 | |||
88 | private def saturateLowerBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { | ||
89 | val optimize = prepareOptimize | ||
90 | val handle = optimize.MkMinimize(expr) | ||
91 | val status = optimize.Check() | ||
92 | if (status == Status.SATISFIABLE) { | ||
93 | val value = switch (resultExpr : handle.lower) { | ||
94 | IntNum: | ||
95 | resultExpr.getInt() | ||
96 | default: | ||
97 | if (isNegativeInfinity(resultExpr)) { | ||
98 | null | ||
99 | } else { | ||
100 | throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) | ||
101 | } | ||
102 | } | ||
103 | expressionToSaturate.lowerBound = value | ||
104 | } | ||
105 | status | ||
106 | } | ||
107 | |||
108 | private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { | ||
109 | val optimize = prepareOptimize | ||
110 | val handle = optimize.MkMaximize(expr) | ||
111 | val status = optimize.Check() | ||
112 | if (status == Status.SATISFIABLE) { | ||
113 | val value = switch (resultExpr : handle.upper) { | ||
114 | IntNum: | ||
115 | resultExpr.getInt() | ||
116 | default: | ||
117 | if (isPositiveInfinity(resultExpr)) { | ||
118 | null | ||
119 | } else { | ||
120 | throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) | ||
121 | } | ||
122 | } | ||
123 | expressionToSaturate.upperBound = value | ||
124 | } | ||
125 | status | ||
126 | } | ||
127 | |||
128 | private def isPositiveInfinity(Expr expr) { | ||
129 | expr.app && expr.getFuncDecl.name == infinitySymbol | ||
130 | } | ||
131 | |||
132 | private def isNegativeInfinity(Expr expr) { | ||
133 | // Negative infinity is represented as (* (- 1) oo) | ||
134 | if (!expr.app || expr.getFuncDecl.name != multSymbol || expr.numArgs != 2) { | ||
135 | return false | ||
136 | } | ||
137 | isPositiveInfinity(expr.args.get(1)) | ||
138 | } | ||
139 | |||
140 | private def prepareOptimize() { | ||
141 | val optimize = mkOptimize() | ||
142 | assertConstraints(optimize) | ||
143 | optimize | ||
144 | } | ||
145 | |||
146 | private def assertConstraints(Optimize it) { | ||
147 | for (pair : variables.entrySet) { | ||
148 | assertBounds(pair.value, pair.key) | ||
149 | } | ||
150 | for (constraint : polyhedron.constraints) { | ||
151 | val expr = createLinearCombination(constraint.coefficients) | ||
152 | assertBounds(expr, constraint) | ||
153 | } | ||
154 | } | ||
155 | |||
156 | private def assertBounds(Optimize it, ArithExpr expression, LinearBoundedExpression bounds) { | ||
157 | val lowerBound = bounds.lowerBound | ||
158 | val upperBound = bounds.upperBound | ||
159 | if (lowerBound == upperBound) { | ||
160 | if (lowerBound === null) { | ||
161 | return | ||
162 | } | ||
163 | Assert(mkEq(expression, mkInt(lowerBound))) | ||
164 | } else { | ||
165 | if (lowerBound !== null) { | ||
166 | Assert(mkGe(expression, mkInt(lowerBound))) | ||
167 | } | ||
168 | if (upperBound !== null) { | ||
169 | Assert(mkLe(expression, mkInt(upperBound))) | ||
170 | } | ||
171 | } | ||
172 | } | ||
173 | |||
174 | private def toExpr(LinearBoundedExpression linearBoundedExpression) { | ||
175 | switch (linearBoundedExpression) { | ||
176 | Dimension: variables.get(linearBoundedExpression) | ||
177 | LinearConstraint: createLinearCombination(linearBoundedExpression.coefficients) | ||
178 | default: throw new IllegalArgumentException("Unknown linear bounded expression:" + linearBoundedExpression) | ||
179 | } | ||
180 | } | ||
181 | |||
182 | private def createLinearCombination(Map<Dimension, Integer> coefficients) { | ||
183 | val size = coefficients.size | ||
184 | val array = newArrayOfSize(size) | ||
185 | var int i = 0 | ||
186 | for (pair : coefficients.entrySet) { | ||
187 | val variable = variables.get(pair.key) | ||
188 | if (variable === null) { | ||
189 | throw new IllegalArgumentException("Unknown dimension: " + pair.key.name) | ||
190 | } | ||
191 | val coefficient = pair.value | ||
192 | val term = if (coefficient == 1) { | ||
193 | variable | ||
194 | } else { | ||
195 | mkMul(mkInt(coefficient), variable) | ||
196 | } | ||
197 | array.set(i, term) | ||
198 | i++ | ||
199 | } | ||
200 | mkAdd(array) | ||
201 | } | ||
202 | |||
203 | override close() throws Exception { | ||
204 | context.close() | ||
205 | } | ||
206 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index 20d24b77..5fefa551 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend | |||
@@ -6,7 +6,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | |||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ScopePropagator | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation |
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 701eb054..101f0a3e 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 | |||
@@ -12,7 +12,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | |||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider | 14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider |
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ScopePropagator | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator |
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser |
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | 18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage |
@@ -71,16 +71,13 @@ class ViatraReasoner extends LogicReasoner { | |||
71 | } | 71 | } |
72 | emptySolution.problemConainer = problem | 72 | emptySolution.problemConainer = problem |
73 | 73 | ||
74 | val ScopePropagator scopePropagator = new ScopePropagator(emptySolution) | ||
75 | scopePropagator.propagateAllScopeConstraints | ||
76 | |||
77 | val method = modelGenerationMethodProvider.createModelGenerationMethod( | 74 | val method = modelGenerationMethodProvider.createModelGenerationMethod( |
78 | problem, | 75 | problem, |
79 | emptySolution, | 76 | emptySolution, |
80 | workspace, | 77 | workspace, |
81 | viatraConfig.nameNewElements, | 78 | viatraConfig.nameNewElements, |
82 | viatraConfig.typeInferenceMethod, | 79 | viatraConfig.typeInferenceMethod, |
83 | scopePropagator, | 80 | viatraConfig.scopePropagatorStrategy, |
84 | viatraConfig.documentationLevel | 81 | viatraConfig.documentationLevel |
85 | ) | 82 | ) |
86 | 83 | ||
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 99decdd9..7a3a2d67 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 | |||
@@ -6,6 +6,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | |||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold |
@@ -49,6 +50,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
49 | * Configuration for cutting search space. | 50 | * Configuration for cutting search space. |
50 | */ | 51 | */ |
51 | public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint | 52 | public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint |
53 | |||
54 | public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.PolyhedralTypeHierarchy | ||
52 | 55 | ||
53 | public var List<CostObjectiveConfiguration> costObjectives = newArrayList | 56 | public var List<CostObjectiveConfiguration> costObjectives = newArrayList |
54 | } | 57 | } |