diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra')
15 files changed, 2498 insertions, 61 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 23e3ad13..b2ee3981 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,8 @@ 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.interval, | ||
8 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators, | ||
7 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, | 9 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, |
8 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries | 10 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries |
9 | Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | 11 | Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/build.properties b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/build.properties index 585df5ce..9ffc994a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/build.properties +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/build.properties | |||
@@ -4,6 +4,5 @@ bin.includes = META-INF/,\ | |||
4 | source.. = src/,\ | 4 | source.. = src/,\ |
5 | patterns/,\ | 5 | patterns/,\ |
6 | vql-gen/,\ | 6 | vql-gen/,\ |
7 | xtend-gen/,\ | 7 | xtend-gen/ |
8 | src-gen/ | ||
9 | output.. = bin/ | 8 | output.. = bin/ |
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.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 f43ab96d..b6918294 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 | |||
@@ -1,8 +1,10 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableMap | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
5 | 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.patterns.ModalPatternQueries | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider |
@@ -10,6 +12,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
10 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 12 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
11 | import java.util.Collection | 13 | import java.util.Collection |
12 | import java.util.List | 14 | import java.util.List |
15 | import java.util.Map | ||
13 | import java.util.Set | 16 | import java.util.Set |
14 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 17 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
15 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 18 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
@@ -20,34 +23,41 @@ import org.eclipse.xtend.lib.annotations.Data | |||
20 | 23 | ||
21 | class ModelGenerationStatistics { | 24 | class ModelGenerationStatistics { |
22 | public var long transformationExecutionTime = 0 | 25 | public var long transformationExecutionTime = 0 |
26 | |||
23 | synchronized def addExecutionTime(long amount) { | 27 | synchronized def addExecutionTime(long amount) { |
24 | transformationExecutionTime+=amount | 28 | transformationExecutionTime += amount |
25 | } | 29 | } |
30 | |||
26 | public var long PreliminaryTypeAnalisisTime = 0 | 31 | public var long PreliminaryTypeAnalisisTime = 0 |
27 | } | 32 | } |
33 | |||
28 | @Data class ModelGenerationMethod { | 34 | @Data class ModelGenerationMethod { |
29 | ModelGenerationStatistics statistics | 35 | ModelGenerationStatistics statistics |
30 | 36 | ||
31 | Collection<? extends BatchTransformationRule<?,?>> objectRefinementRules | 37 | Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules |
32 | Collection<? extends BatchTransformationRule<?,?>> relationRefinementRules | 38 | Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules |
33 | 39 | ||
34 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities | 40 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities |
35 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF | 41 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF |
36 | 42 | ||
37 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | 43 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF |
38 | 44 | ||
39 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | 45 | Map<String, ModalPatternQueries> modalRelationQueries |
46 | |||
47 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | ||
40 | } | 48 | } |
49 | |||
41 | enum TypeInferenceMethod { | 50 | enum TypeInferenceMethod { |
42 | Generic, PreliminaryAnalysis | 51 | Generic, |
52 | PreliminaryAnalysis | ||
43 | } | 53 | } |
44 | 54 | ||
45 | class ModelGenerationMethodProvider { | 55 | class ModelGenerationMethodProvider { |
46 | private val PatternProvider patternProvider = new PatternProvider | 56 | val PatternProvider patternProvider = new PatternProvider |
47 | private val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider | 57 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider |
48 | private val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider | 58 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider |
49 | 59 | ||
50 | public def ModelGenerationMethod createModelGenerationMethod( | 60 | def ModelGenerationMethod createModelGenerationMethod( |
51 | LogicProblem logicProblem, | 61 | LogicProblem logicProblem, |
52 | PartialInterpretation emptySolution, | 62 | PartialInterpretation emptySolution, |
53 | ReasonerWorkspace workspace, | 63 | ReasonerWorkspace workspace, |
@@ -58,25 +68,31 @@ class ModelGenerationMethodProvider { | |||
58 | ) { | 68 | ) { |
59 | val statistics = new ModelGenerationStatistics | 69 | val statistics = new ModelGenerationStatistics |
60 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) | 70 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) |
61 | 71 | ||
62 | val Set<PQuery> existingQueries = logicProblem | 72 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). |
63 | .relations | 73 | map[it.patternPQuery as PQuery].toSet |
64 | .map[annotations] | 74 | |
65 | .flatten | 75 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, |
66 | .filter(TransfomedViatraQuery) | 76 | workspace, typeInferenceMethod, writeFiles) |
67 | .map[it.patternPQuery as PQuery] | 77 | val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> |
68 | .toSet | 78 | objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, |
69 | 79 | nameNewElements, statistics) | |
70 | val queries = patternProvider.generateQueries(logicProblem,emptySolution,statistics,existingQueries,workspace,typeInferenceMethod,writeFiles) | 80 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, statistics) |
71 | val //LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> | 81 | |
72 | objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries,scopePropagator,nameNewElements,statistics) | ||
73 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics) | ||
74 | |||
75 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) | 82 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) |
76 | val unfinishedWF = queries.getUnfinishedWFQueries.values | 83 | val unfinishedWF = queries.getUnfinishedWFQueries.values |
77 | 84 | ||
85 | val modalRelationQueriesBuilder = ImmutableMap.builder | ||
86 | for (entry : queries.modalRelationQueries.entrySet) { | ||
87 | val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head | ||
88 | if (annotation !== null) { | ||
89 | modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) | ||
90 | } | ||
91 | } | ||
92 | val modalRelationQueries = modalRelationQueriesBuilder.build | ||
93 | |||
78 | val invalidWF = queries.getInvalidWFQueries.values | 94 | val invalidWF = queries.getInvalidWFQueries.values |
79 | 95 | ||
80 | return new ModelGenerationMethod( | 96 | return new ModelGenerationMethod( |
81 | statistics, | 97 | statistics, |
82 | objectRefinementRules.values, | 98 | objectRefinementRules.values, |
@@ -84,6 +100,7 @@ class ModelGenerationMethodProvider { | |||
84 | unfinishedMultiplicities, | 100 | unfinishedMultiplicities, |
85 | unfinishedWF, | 101 | unfinishedWF, |
86 | invalidWF, | 102 | invalidWF, |
103 | modalRelationQueries, | ||
87 | queries.allQueries | 104 | queries.allQueries |
88 | ) | 105 | ) |
89 | } | 106 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend index e05160d0..4b9629df 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend | |||
@@ -11,28 +11,28 @@ class MultiplicityGoalConstraintCalculator { | |||
11 | val IQuerySpecification<?> querySpecification; | 11 | val IQuerySpecification<?> querySpecification; |
12 | var ViatraQueryMatcher<?> matcher; | 12 | var ViatraQueryMatcher<?> matcher; |
13 | 13 | ||
14 | public new(String targetRelationName, IQuerySpecification<?> querySpecification) { | 14 | new(String targetRelationName, IQuerySpecification<?> querySpecification) { |
15 | this.targetRelationName = targetRelationName | 15 | this.targetRelationName = targetRelationName |
16 | this.querySpecification = querySpecification | 16 | this.querySpecification = querySpecification |
17 | this.matcher = null | 17 | this.matcher = null |
18 | } | 18 | } |
19 | 19 | ||
20 | public new(MultiplicityGoalConstraintCalculator other) { | 20 | new(MultiplicityGoalConstraintCalculator other) { |
21 | this.targetRelationName = other.targetRelationName | 21 | this.targetRelationName = other.targetRelationName |
22 | this.querySpecification = other.querySpecification | 22 | this.querySpecification = other.querySpecification |
23 | this.matcher = null | 23 | this.matcher = null |
24 | } | 24 | } |
25 | 25 | ||
26 | def public getName() { | 26 | def getName() { |
27 | targetRelationName | 27 | targetRelationName |
28 | } | 28 | } |
29 | 29 | ||
30 | def public init(Notifier notifier) { | 30 | def init(Notifier notifier) { |
31 | val engine = ViatraQueryEngine.on(new EMFScope(notifier)) | 31 | val engine = ViatraQueryEngine.on(new EMFScope(notifier)) |
32 | matcher = querySpecification.getMatcher(engine) | 32 | matcher = querySpecification.getMatcher(engine) |
33 | } | 33 | } |
34 | 34 | ||
35 | def public calculateValue() { | 35 | def calculateValue() { |
36 | var res = 0 | 36 | var res = 0 |
37 | val allMatches = this.matcher.allMatches | 37 | val allMatches = this.matcher.allMatches |
38 | for(match : allMatches) { | 38 | for(match : allMatches) { |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Interval.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Interval.xtend new file mode 100644 index 00000000..4f0f594f --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Interval.xtend | |||
@@ -0,0 +1,584 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval | ||
2 | |||
3 | import java.math.BigDecimal | ||
4 | import java.math.MathContext | ||
5 | import java.math.RoundingMode | ||
6 | import org.eclipse.xtend.lib.annotations.Data | ||
7 | |||
8 | abstract class Interval implements Comparable<Interval> { | ||
9 | static val PRECISION = 32 | ||
10 | static val ROUND_DOWN = new MathContext(PRECISION, RoundingMode.FLOOR) | ||
11 | static val ROUND_UP = new MathContext(PRECISION, RoundingMode.CEILING) | ||
12 | |||
13 | private new() { | ||
14 | } | ||
15 | |||
16 | abstract def boolean mustEqual(Interval other) | ||
17 | |||
18 | abstract def boolean mayEqual(Interval other) | ||
19 | |||
20 | def mustNotEqual(Interval other) { | ||
21 | !mayEqual(other) | ||
22 | } | ||
23 | |||
24 | def mayNotEqual(Interval other) { | ||
25 | !mustEqual(other) | ||
26 | } | ||
27 | |||
28 | abstract def boolean mustBeLessThan(Interval other) | ||
29 | |||
30 | abstract def boolean mayBeLessThan(Interval other) | ||
31 | |||
32 | def mustBeLessThanOrEqual(Interval other) { | ||
33 | !mayBeGreaterThan(other) | ||
34 | } | ||
35 | |||
36 | def mayBeLessThanOrEqual(Interval other) { | ||
37 | !mustBeGreaterThan(other) | ||
38 | } | ||
39 | |||
40 | def mustBeGreaterThan(Interval other) { | ||
41 | other.mustBeLessThan(this) | ||
42 | } | ||
43 | |||
44 | def mayBeGreaterThan(Interval other) { | ||
45 | other.mayBeLessThan(this) | ||
46 | } | ||
47 | |||
48 | def mustBeGreaterThanOrEqual(Interval other) { | ||
49 | other.mustBeLessThanOrEqual(this) | ||
50 | } | ||
51 | |||
52 | def mayBeGreaterThanOrEqual(Interval other) { | ||
53 | other.mayBeLessThanOrEqual(this) | ||
54 | } | ||
55 | |||
56 | abstract def Interval min(Interval other) | ||
57 | |||
58 | abstract def Interval max(Interval other) | ||
59 | |||
60 | abstract def Interval join(Interval other) | ||
61 | |||
62 | def +() { | ||
63 | this | ||
64 | } | ||
65 | |||
66 | abstract def Interval -() | ||
67 | |||
68 | abstract def Interval +(Interval other) | ||
69 | |||
70 | abstract def Interval -(Interval other) | ||
71 | |||
72 | abstract def Interval *(int count) | ||
73 | |||
74 | abstract def Interval *(Interval other) | ||
75 | |||
76 | abstract def Interval /(Interval other) | ||
77 | |||
78 | abstract def Interval **(Interval other) | ||
79 | |||
80 | public static val EMPTY = new Interval { | ||
81 | override mustEqual(Interval other) { | ||
82 | true | ||
83 | } | ||
84 | |||
85 | override mayEqual(Interval other) { | ||
86 | false | ||
87 | } | ||
88 | |||
89 | override mustBeLessThan(Interval other) { | ||
90 | true | ||
91 | } | ||
92 | |||
93 | override mayBeLessThan(Interval other) { | ||
94 | false | ||
95 | } | ||
96 | |||
97 | override min(Interval other) { | ||
98 | EMPTY | ||
99 | } | ||
100 | |||
101 | override max(Interval other) { | ||
102 | EMPTY | ||
103 | } | ||
104 | |||
105 | override join(Interval other) { | ||
106 | other | ||
107 | } | ||
108 | |||
109 | override -() { | ||
110 | EMPTY | ||
111 | } | ||
112 | |||
113 | override +(Interval other) { | ||
114 | EMPTY | ||
115 | } | ||
116 | |||
117 | override -(Interval other) { | ||
118 | EMPTY | ||
119 | } | ||
120 | |||
121 | override *(int count) { | ||
122 | EMPTY | ||
123 | } | ||
124 | |||
125 | override *(Interval other) { | ||
126 | EMPTY | ||
127 | } | ||
128 | |||
129 | override /(Interval other) { | ||
130 | EMPTY | ||
131 | } | ||
132 | |||
133 | override **(Interval other) { | ||
134 | EMPTY | ||
135 | } | ||
136 | |||
137 | override toString() { | ||
138 | "∅" | ||
139 | } | ||
140 | |||
141 | override compareTo(Interval o) { | ||
142 | if (o == EMPTY) { | ||
143 | 0 | ||
144 | } else { | ||
145 | -1 | ||
146 | } | ||
147 | } | ||
148 | |||
149 | } | ||
150 | |||
151 | public static val Interval ZERO = new NonEmpty(BigDecimal.ZERO, BigDecimal.ZERO) | ||
152 | |||
153 | public static val Interval UNBOUNDED = new NonEmpty(null, null) | ||
154 | |||
155 | static def Interval of(BigDecimal lower, BigDecimal upper) { | ||
156 | new NonEmpty(lower, upper) | ||
157 | } | ||
158 | |||
159 | static def between(double lower, double upper) { | ||
160 | of(new BigDecimal(lower, ROUND_DOWN), new BigDecimal(upper, ROUND_UP)) | ||
161 | } | ||
162 | |||
163 | static def upTo(double upper) { | ||
164 | of(null, new BigDecimal(upper, ROUND_UP)) | ||
165 | } | ||
166 | |||
167 | static def above(double lower) { | ||
168 | of(new BigDecimal(lower, ROUND_DOWN), null) | ||
169 | } | ||
170 | |||
171 | @Data | ||
172 | private static class NonEmpty extends Interval { | ||
173 | val BigDecimal lower | ||
174 | val BigDecimal upper | ||
175 | |||
176 | /** | ||
177 | * Construct a new non-empty interval. | ||
178 | * | ||
179 | * @param lower The lower bound of the interval. Use <code>null</code> for negative infinity. | ||
180 | * @param upper The upper bound of the interval. Use <code>null</code> for positive infinity. | ||
181 | */ | ||
182 | new(BigDecimal lower, BigDecimal upper) { | ||
183 | if (lower !== null && upper !== null && lower > upper) { | ||
184 | throw new IllegalArgumentException("Lower bound of interval must not be larger than upper bound") | ||
185 | } | ||
186 | this.lower = lower | ||
187 | this.upper = upper | ||
188 | } | ||
189 | |||
190 | override mustEqual(Interval other) { | ||
191 | switch (other) { | ||
192 | case EMPTY: true | ||
193 | NonEmpty: lower == upper && lower == other.lower && lower == other.upper | ||
194 | default: throw new IllegalArgumentException("Unknown interval: " + other) | ||
195 | } | ||
196 | } | ||
197 | |||
198 | override mayEqual(Interval other) { | ||
199 | if (other instanceof NonEmpty) { | ||
200 | (lower === null || other.upper === null || lower <= other.upper) && | ||
201 | (other.lower === null || upper === null || other.lower <= upper) | ||
202 | } else { | ||
203 | false | ||
204 | } | ||
205 | } | ||
206 | |||
207 | override mustBeLessThan(Interval other) { | ||
208 | switch (other) { | ||
209 | case EMPTY: true | ||
210 | NonEmpty: upper !== null && other.lower !== null && upper < other.lower | ||
211 | default: throw new IllegalArgumentException("Unknown interval: " + other) | ||
212 | } | ||
213 | } | ||
214 | |||
215 | override mayBeLessThan(Interval other) { | ||
216 | if (other instanceof NonEmpty) { | ||
217 | lower === null || other.upper === null || lower < other.upper | ||
218 | } else { | ||
219 | false | ||
220 | } | ||
221 | } | ||
222 | |||
223 | override min(Interval other) { | ||
224 | switch (other) { | ||
225 | case EMPTY: this | ||
226 | NonEmpty: min(other) | ||
227 | default: throw new IllegalArgumentException("Unknown interval: " + other) | ||
228 | } | ||
229 | } | ||
230 | |||
231 | def min(NonEmpty other) { | ||
232 | new NonEmpty( | ||
233 | lower.tryMin(other.lower), | ||
234 | if(other.upper === null) upper else if(upper === null) other.upper else upper.min(other.upper) | ||
235 | ) | ||
236 | } | ||
237 | |||
238 | override max(Interval other) { | ||
239 | switch (other) { | ||
240 | case EMPTY: this | ||
241 | NonEmpty: max(other) | ||
242 | default: throw new IllegalArgumentException("Unknown interval: " + other) | ||
243 | } | ||
244 | } | ||
245 | |||
246 | def max(NonEmpty other) { | ||
247 | new NonEmpty( | ||
248 | if(other.lower === null) lower else if(lower === null) other.lower else lower.max(other.lower), | ||
249 | upper.tryMax(other.upper) | ||
250 | ) | ||
251 | } | ||
252 | |||
253 | override join(Interval other) { | ||
254 | switch (other) { | ||
255 | case EMPTY: this | ||
256 | NonEmpty: new NonEmpty(lower.tryMin(other.lower), upper.tryMax(other.upper)) | ||
257 | default: throw new IllegalArgumentException("Unknown interval: " + other) | ||
258 | } | ||
259 | } | ||
260 | |||
261 | override -() { | ||
262 | new NonEmpty(upper?.negate(ROUND_DOWN), lower?.negate(ROUND_UP)) | ||
263 | } | ||
264 | |||
265 | override +(Interval other) { | ||
266 | switch (other) { | ||
267 | case EMPTY: EMPTY | ||
268 | NonEmpty: this + other | ||
269 | default: throw new IllegalArgumentException("Unknown interval: " + other) | ||
270 | } | ||
271 | } | ||
272 | |||
273 | def +(NonEmpty other) { | ||
274 | new NonEmpty( | ||
275 | lower.tryAdd(other.lower, ROUND_DOWN), | ||
276 | upper.tryAdd(other.upper, ROUND_UP) | ||
277 | ) | ||
278 | } | ||
279 | |||
280 | private static def tryAdd(BigDecimal a, BigDecimal b, MathContext mc) { | ||
281 | if (b === null) { | ||
282 | null | ||
283 | } else { | ||
284 | a?.add(b, mc) | ||
285 | } | ||
286 | } | ||
287 | |||
288 | override -(Interval other) { | ||
289 | switch (other) { | ||
290 | case EMPTY: EMPTY | ||
291 | NonEmpty: this - other | ||
292 | default: throw new IllegalArgumentException("Unknown interval: " + other) | ||
293 | } | ||
294 | } | ||
295 | |||
296 | def -(NonEmpty other) { | ||
297 | new NonEmpty( | ||
298 | lower.trySubtract(other.upper, ROUND_DOWN), | ||
299 | upper.trySubtract(other.lower, ROUND_UP) | ||
300 | ) | ||
301 | } | ||
302 | |||
303 | private static def trySubtract(BigDecimal a, BigDecimal b, MathContext mc) { | ||
304 | if (b === null) { | ||
305 | null | ||
306 | } else { | ||
307 | a?.subtract(b, mc) | ||
308 | } | ||
309 | } | ||
310 | |||
311 | override *(int count) { | ||
312 | val bigCount = new BigDecimal(count) | ||
313 | new NonEmpty( | ||
314 | lower.tryMultiply(bigCount, ROUND_DOWN), | ||
315 | upper.tryMultiply(bigCount, ROUND_UP) | ||
316 | ) | ||
317 | } | ||
318 | |||
319 | override *(Interval other) { | ||
320 | switch (other) { | ||
321 | case EMPTY: EMPTY | ||
322 | NonEmpty: this * other | ||
323 | default: throw new IllegalArgumentException("Unknown interval: " + other) | ||
324 | } | ||
325 | } | ||
326 | |||
327 | def *(NonEmpty other) { | ||
328 | if (this == ZERO || other == ZERO) { | ||
329 | ZERO | ||
330 | } else if (nonpositive) { | ||
331 | if (other.nonpositive) { | ||
332 | new NonEmpty( | ||
333 | upper.multiply(other.upper, ROUND_DOWN), | ||
334 | lower.tryMultiply(other.lower, ROUND_UP) | ||
335 | ) | ||
336 | } else if (other.nonnegative) { | ||
337 | new NonEmpty( | ||
338 | lower.tryMultiply(other.upper, ROUND_DOWN), | ||
339 | upper.multiply(other.lower, ROUND_UP) | ||
340 | ) | ||
341 | } else { | ||
342 | new NonEmpty( | ||
343 | lower.tryMultiply(other.upper, ROUND_DOWN), | ||
344 | lower.tryMultiply(other.lower, ROUND_UP) | ||
345 | ) | ||
346 | } | ||
347 | } else if (nonnegative) { | ||
348 | if (other.nonpositive) { | ||
349 | new NonEmpty( | ||
350 | upper.tryMultiply(other.lower, ROUND_DOWN), | ||
351 | lower.multiply(other.upper, ROUND_UP) | ||
352 | ) | ||
353 | } else if (other.nonnegative) { | ||
354 | new NonEmpty( | ||
355 | lower.multiply(other.lower, ROUND_DOWN), | ||
356 | upper.tryMultiply(other.upper, ROUND_UP) | ||
357 | ) | ||
358 | } else { | ||
359 | new NonEmpty( | ||
360 | upper.tryMultiply(other.lower, ROUND_DOWN), | ||
361 | upper.tryMultiply(other.upper, ROUND_UP) | ||
362 | ) | ||
363 | } | ||
364 | } else { | ||
365 | if (other.nonpositive) { | ||
366 | new NonEmpty( | ||
367 | upper.tryMultiply(other.lower, ROUND_DOWN), | ||
368 | lower.tryMultiply(other.lower, ROUND_UP) | ||
369 | ) | ||
370 | } else if (other.nonnegative) { | ||
371 | new NonEmpty( | ||
372 | lower.tryMultiply(other.upper, ROUND_DOWN), | ||
373 | upper.tryMultiply(other.upper, ROUND_UP) | ||
374 | ) | ||
375 | } else { | ||
376 | new NonEmpty( | ||
377 | lower.tryMultiply(other.upper, ROUND_DOWN).tryMin(upper.tryMultiply(other.lower, ROUND_DOWN)), | ||
378 | lower.tryMultiply(other.lower, ROUND_UP).tryMax(upper.tryMultiply(other.upper, ROUND_UP)) | ||
379 | ) | ||
380 | } | ||
381 | } | ||
382 | } | ||
383 | |||
384 | private def isNonpositive() { | ||
385 | upper !== null && upper <= BigDecimal.ZERO | ||
386 | } | ||
387 | |||
388 | private def isNonnegative() { | ||
389 | lower !== null && lower >= BigDecimal.ZERO | ||
390 | } | ||
391 | |||
392 | private static def tryMultiply(BigDecimal a, BigDecimal b, MathContext mc) { | ||
393 | if (b === null) { | ||
394 | null | ||
395 | } else { | ||
396 | a?.multiply(b, mc) | ||
397 | } | ||
398 | } | ||
399 | |||
400 | private static def tryMin(BigDecimal a, BigDecimal b) { | ||
401 | if (b === null) { | ||
402 | null | ||
403 | } else { | ||
404 | a?.min(b) | ||
405 | } | ||
406 | } | ||
407 | |||
408 | private static def tryMax(BigDecimal a, BigDecimal b) { | ||
409 | if (b === null) { | ||
410 | null | ||
411 | } else { | ||
412 | a?.max(b) | ||
413 | } | ||
414 | } | ||
415 | |||
416 | override /(Interval other) { | ||
417 | switch (other) { | ||
418 | case EMPTY: EMPTY | ||
419 | NonEmpty: this / other | ||
420 | default: throw new IllegalArgumentException("Unknown interval: " + other) | ||
421 | } | ||
422 | } | ||
423 | |||
424 | def /(NonEmpty other) { | ||
425 | if (other == ZERO) { | ||
426 | EMPTY | ||
427 | } else if (this == ZERO) { | ||
428 | ZERO | ||
429 | } else if (other.strictlyNegative) { | ||
430 | if (nonpositive) { | ||
431 | new NonEmpty( | ||
432 | upper.tryDivide(other.lower, ROUND_DOWN), | ||
433 | lower.tryDivide(other.upper, ROUND_UP) | ||
434 | ) | ||
435 | } else if (nonnegative) { | ||
436 | new NonEmpty( | ||
437 | upper.tryDivide(other.upper, ROUND_DOWN), | ||
438 | lower.tryDivide(other.lower, ROUND_UP) | ||
439 | ) | ||
440 | } else { // lower < 0 < upper | ||
441 | new NonEmpty( | ||
442 | upper.tryDivide(other.upper, ROUND_DOWN), | ||
443 | lower.tryDivide(other.upper, ROUND_UP) | ||
444 | ) | ||
445 | } | ||
446 | } else if (other.strictlyPositive) { | ||
447 | if (nonpositive) { | ||
448 | new NonEmpty( | ||
449 | lower.tryDivide(other.lower, ROUND_DOWN), | ||
450 | upper.tryDivide(other.upper, ROUND_UP) | ||
451 | ) | ||
452 | } else if (nonnegative) { | ||
453 | new NonEmpty( | ||
454 | lower.tryDivide(other.upper, ROUND_DOWN), | ||
455 | upper.tryDivide(other.lower, ROUND_UP) | ||
456 | ) | ||
457 | } else { // lower < 0 < upper | ||
458 | new NonEmpty( | ||
459 | lower.tryDivide(other.lower, ROUND_DOWN), | ||
460 | upper.tryDivide(other.lower, ROUND_UP) | ||
461 | ) | ||
462 | } | ||
463 | } else { // other contains 0 | ||
464 | if (other.lower == BigDecimal.ZERO) { // 0 == other.lower < other.upper, because [0, 0] was exluded earlier | ||
465 | if (nonpositive) { | ||
466 | new NonEmpty(null, upper.tryDivide(other.upper, ROUND_UP)) | ||
467 | } else if (nonnegative) { | ||
468 | new NonEmpty(lower.tryDivide(other.upper, ROUND_DOWN), null) | ||
469 | } else { // lower < 0 < upper | ||
470 | UNBOUNDED | ||
471 | } | ||
472 | } else if (other.upper == BigDecimal.ZERO) { // other.lower < other.upper == 0 | ||
473 | if (nonpositive) { | ||
474 | new NonEmpty(upper.tryDivide(other.lower, ROUND_DOWN), null) | ||
475 | } else if (nonnegative) { | ||
476 | new NonEmpty(null, lower.tryDivide(other.lower, ROUND_UP)) | ||
477 | } else { // lower < 0 < upper | ||
478 | UNBOUNDED | ||
479 | } | ||
480 | } else { // other.lower < 0 < other.upper | ||
481 | UNBOUNDED | ||
482 | } | ||
483 | } | ||
484 | } | ||
485 | |||
486 | private def isStrictlyNegative() { | ||
487 | upper !== null && upper < BigDecimal.ZERO | ||
488 | } | ||
489 | |||
490 | private def isStrictlyPositive() { | ||
491 | lower !== null && lower > BigDecimal.ZERO | ||
492 | } | ||
493 | |||
494 | private static def tryDivide(BigDecimal a, BigDecimal b, MathContext mc) { | ||
495 | if (b === null) { | ||
496 | BigDecimal.ZERO | ||
497 | } else { | ||
498 | a?.divide(b, mc) | ||
499 | } | ||
500 | } | ||
501 | |||
502 | override **(Interval other) { | ||
503 | switch (other) { | ||
504 | case EMPTY: EMPTY | ||
505 | NonEmpty: this ** other | ||
506 | default: throw new IllegalArgumentException("Unknown interval: " + other) | ||
507 | } | ||
508 | } | ||
509 | |||
510 | def **(NonEmpty other) { | ||
511 | // XXX This should use proper rounding for log and exp instead of | ||
512 | // converting to double. | ||
513 | // XXX We should not ignore (integer) powers of negative numbers. | ||
514 | val lowerLog = if (lower === null || lower <= BigDecimal.ZERO) { | ||
515 | null | ||
516 | } else { | ||
517 | new BigDecimal(Math.log(lower.doubleValue), ROUND_DOWN) | ||
518 | } | ||
519 | val upperLog = if (upper === null) { | ||
520 | null | ||
521 | } else if (upper == BigDecimal.ZERO) { | ||
522 | return ZERO | ||
523 | } else if (upper < BigDecimal.ZERO) { | ||
524 | return EMPTY | ||
525 | } else { | ||
526 | new BigDecimal(Math.log(upper.doubleValue), ROUND_UP) | ||
527 | } | ||
528 | val log = new NonEmpty(lowerLog, upperLog) | ||
529 | val product = log * other | ||
530 | if (product instanceof NonEmpty) { | ||
531 | val lowerResult = if (product.lower === null) { | ||
532 | BigDecimal.ZERO | ||
533 | } else { | ||
534 | new BigDecimal(Math.exp(product.lower.doubleValue), ROUND_DOWN) | ||
535 | } | ||
536 | val upperResult = if (product.upper === null) { | ||
537 | null | ||
538 | } else { | ||
539 | new BigDecimal(Math.exp(product.upper.doubleValue), ROUND_UP) | ||
540 | } | ||
541 | new NonEmpty(lowerResult, upperResult) | ||
542 | } else { | ||
543 | throw new IllegalArgumentException("Unknown interval: " + product) | ||
544 | } | ||
545 | } | ||
546 | |||
547 | override toString() { | ||
548 | '''«IF lower === null»(-∞«ELSE»[«lower»«ENDIF», «IF upper === null»∞)«ELSE»«upper»]«ENDIF»''' | ||
549 | } | ||
550 | |||
551 | override compareTo(Interval o) { | ||
552 | switch (o) { | ||
553 | case EMPTY: 1 | ||
554 | NonEmpty: compareTo(o) | ||
555 | default: throw new IllegalArgumentException("Unknown interval: " + o) | ||
556 | } | ||
557 | } | ||
558 | |||
559 | def compareTo(NonEmpty o) { | ||
560 | if (lower === null) { | ||
561 | if (o.lower !== null) { | ||
562 | return -1 | ||
563 | } | ||
564 | } else if (o.lower === null) { // lower !== null | ||
565 | return 1 | ||
566 | } else { // both lower and o.lower are finite | ||
567 | val lowerDifference = lower.compareTo(o.lower) | ||
568 | if (lowerDifference != 0) { | ||
569 | return lowerDifference | ||
570 | } | ||
571 | } | ||
572 | if (upper === null) { | ||
573 | if (o.upper === null) { | ||
574 | return 0 | ||
575 | } else { | ||
576 | return 1 | ||
577 | } | ||
578 | } else if (o.upper === null) { // upper !== null | ||
579 | return -1 | ||
580 | } | ||
581 | upper.compareTo(o.upper) | ||
582 | } | ||
583 | } | ||
584 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalAggregationMode.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalAggregationMode.java new file mode 100644 index 00000000..f106e305 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalAggregationMode.java | |||
@@ -0,0 +1,99 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval; | ||
2 | |||
3 | import java.util.function.BinaryOperator; | ||
4 | |||
5 | public enum IntervalAggregationMode implements BinaryOperator<Interval> { | ||
6 | SUM("intervalSum", "Sum a set of intervals") { | ||
7 | @Override | ||
8 | public IntervalRedBlackNode createNode(Interval interval) { | ||
9 | return new IntervalRedBlackNode(interval) { | ||
10 | public boolean isMultiplicitySensitive() { | ||
11 | return true; | ||
12 | } | ||
13 | |||
14 | public Interval multiply(Interval interval, int count) { | ||
15 | return interval.operator_multiply(count); | ||
16 | }; | ||
17 | |||
18 | @Override | ||
19 | public Interval op(Interval left, Interval right) { | ||
20 | return left.operator_plus(right); | ||
21 | } | ||
22 | }; | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public Interval getNeutral() { | ||
27 | return Interval.ZERO; | ||
28 | } | ||
29 | }, | ||
30 | |||
31 | MIN("intervalMin", "Find the minimum a set of intervals") { | ||
32 | @Override | ||
33 | public IntervalRedBlackNode createNode(Interval interval) { | ||
34 | return new IntervalRedBlackNode(interval) { | ||
35 | @Override | ||
36 | public Interval op(Interval left, Interval right) { | ||
37 | return left.min(right); | ||
38 | } | ||
39 | }; | ||
40 | } | ||
41 | }, | ||
42 | |||
43 | MAX("intervalMax", "Find the maximum a set of intervals") { | ||
44 | @Override | ||
45 | public IntervalRedBlackNode createNode(Interval interval) { | ||
46 | return new IntervalRedBlackNode(interval) { | ||
47 | @Override | ||
48 | public Interval op(Interval left, Interval right) { | ||
49 | return left.max(right); | ||
50 | } | ||
51 | }; | ||
52 | } | ||
53 | }, | ||
54 | |||
55 | JOIN("intervalJoin", "Calculate the smallest interval containing all the intervals in a set") { | ||
56 | @Override | ||
57 | public IntervalRedBlackNode createNode(Interval interval) { | ||
58 | return new IntervalRedBlackNode(interval) { | ||
59 | @Override | ||
60 | public Interval op(Interval left, Interval right) { | ||
61 | return left.join(right); | ||
62 | } | ||
63 | }; | ||
64 | } | ||
65 | }; | ||
66 | |||
67 | private final String modeName; | ||
68 | private final String description; | ||
69 | private final IntervalRedBlackNode empty; | ||
70 | |||
71 | IntervalAggregationMode(String modeName, String description) { | ||
72 | this.modeName = modeName; | ||
73 | this.description = description; | ||
74 | empty = createNode(null); | ||
75 | } | ||
76 | |||
77 | public String getModeName() { | ||
78 | return modeName; | ||
79 | } | ||
80 | |||
81 | public String getDescription() { | ||
82 | return description; | ||
83 | } | ||
84 | |||
85 | public IntervalRedBlackNode getEmpty() { | ||
86 | return empty; | ||
87 | } | ||
88 | |||
89 | @Override | ||
90 | public Interval apply(Interval left, Interval right) { | ||
91 | return empty.op(left, right); | ||
92 | } | ||
93 | |||
94 | public abstract IntervalRedBlackNode createNode(Interval interval); | ||
95 | |||
96 | public Interval getNeutral() { | ||
97 | return Interval.EMPTY; | ||
98 | } | ||
99 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalAggregationOperator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalAggregationOperator.xtend new file mode 100644 index 00000000..21d3d73b --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalAggregationOperator.xtend | |||
@@ -0,0 +1,48 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval | ||
2 | |||
3 | import java.util.stream.Stream | ||
4 | import org.eclipse.viatra.query.runtime.matchers.psystem.aggregations.IMultisetAggregationOperator | ||
5 | import org.eclipse.xtend.lib.annotations.Accessors | ||
6 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
7 | |||
8 | @FinalFieldsConstructor | ||
9 | class IntervalAggregationOperator implements IMultisetAggregationOperator<Interval, IntervalRedBlackNode, Interval> { | ||
10 | @Accessors val IntervalAggregationMode mode | ||
11 | |||
12 | override getName() { | ||
13 | mode.modeName | ||
14 | } | ||
15 | |||
16 | override getShortDescription() { | ||
17 | mode.description | ||
18 | } | ||
19 | |||
20 | override createNeutral() { | ||
21 | mode.empty | ||
22 | } | ||
23 | |||
24 | override isNeutral(IntervalRedBlackNode result) { | ||
25 | result.leaf | ||
26 | } | ||
27 | |||
28 | override update(IntervalRedBlackNode oldResult, Interval updateValue, boolean isInsertion) { | ||
29 | if (isInsertion) { | ||
30 | val newNode = mode.createNode(updateValue) | ||
31 | oldResult.add(newNode) | ||
32 | } else { | ||
33 | oldResult.remove(updateValue) | ||
34 | } | ||
35 | } | ||
36 | |||
37 | override getAggregate(IntervalRedBlackNode result) { | ||
38 | if (result.leaf) { | ||
39 | mode.neutral | ||
40 | } else { | ||
41 | result.result | ||
42 | } | ||
43 | } | ||
44 | |||
45 | override aggregateStream(Stream<Interval> stream) { | ||
46 | stream.reduce(mode).orElse(mode.neutral) | ||
47 | } | ||
48 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalRedBlackNode.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalRedBlackNode.xtend new file mode 100644 index 00000000..3aa575bc --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalRedBlackNode.xtend | |||
@@ -0,0 +1,177 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval | ||
2 | |||
3 | abstract class IntervalRedBlackNode extends RedBlackNode<IntervalRedBlackNode> { | ||
4 | public val Interval interval | ||
5 | public var int count = 1 | ||
6 | public var Interval result | ||
7 | |||
8 | new(Interval interval) { | ||
9 | this.interval = interval | ||
10 | } | ||
11 | |||
12 | def boolean isMultiplicitySensitive() { | ||
13 | false | ||
14 | } | ||
15 | |||
16 | def Interval multiply(Interval interval, int count) { | ||
17 | interval | ||
18 | } | ||
19 | |||
20 | abstract def Interval op(Interval left, Interval right) | ||
21 | |||
22 | override augment() { | ||
23 | val value = calcualteAugmentation() | ||
24 | if (result == value) { | ||
25 | false | ||
26 | } else { | ||
27 | result = value | ||
28 | true | ||
29 | } | ||
30 | } | ||
31 | |||
32 | private def calcualteAugmentation() { | ||
33 | var value = multiply(interval, count) | ||
34 | if (!left.leaf) { | ||
35 | value = op(value, left.result) | ||
36 | } | ||
37 | if (!right.leaf) { | ||
38 | value = op(value, right.result) | ||
39 | } | ||
40 | value | ||
41 | } | ||
42 | |||
43 | override assertNodeIsValid() { | ||
44 | super.assertNodeIsValid() | ||
45 | if (leaf) { | ||
46 | return | ||
47 | } | ||
48 | if (count <= 0) { | ||
49 | throw new IllegalStateException("Node with nonpositive count") | ||
50 | } | ||
51 | val value = calcualteAugmentation() | ||
52 | if (result != value) { | ||
53 | throw new IllegalStateException("Node with invalid augmentation: " + result + " != " + value) | ||
54 | } | ||
55 | } | ||
56 | |||
57 | override assertSubtreeIsValid() { | ||
58 | super.assertSubtreeIsValid() | ||
59 | assertNodeIsValid() | ||
60 | } | ||
61 | |||
62 | override compareTo(IntervalRedBlackNode other) { | ||
63 | if (leaf || other.leaf) { | ||
64 | throw new IllegalArgumentException("One of the nodes is a leaf node") | ||
65 | } | ||
66 | interval.compareTo(other.interval) | ||
67 | } | ||
68 | |||
69 | def add(IntervalRedBlackNode newNode) { | ||
70 | if (parent !== null) { | ||
71 | throw new IllegalArgumentException("This is not the root of a tree") | ||
72 | } | ||
73 | if (leaf) { | ||
74 | newNode.isRed = false | ||
75 | newNode.left = this | ||
76 | newNode.right = this | ||
77 | newNode.parent = null | ||
78 | newNode.augment | ||
79 | return newNode | ||
80 | } | ||
81 | val modifiedNode = addWithoutFixup(newNode) | ||
82 | if (modifiedNode === newNode) { | ||
83 | // Must augment here, because fixInsertion() might call augment() | ||
84 | // on a node repeatedly, which might lose the change notification the | ||
85 | // second time it is called, and the augmentation will fail to | ||
86 | // reach the root. | ||
87 | modifiedNode.augmentRecursively | ||
88 | modifiedNode.isRed = true | ||
89 | return modifiedNode.fixInsertion | ||
90 | } | ||
91 | if (multiplicitySensitive) { | ||
92 | modifiedNode.augmentRecursively | ||
93 | } | ||
94 | this | ||
95 | } | ||
96 | |||
97 | private def addWithoutFixup(IntervalRedBlackNode newNode) { | ||
98 | var node = this | ||
99 | while (!node.leaf) { | ||
100 | val comparison = node.interval.compareTo(newNode.interval) | ||
101 | if (comparison < 0) { | ||
102 | if (node.left.leaf) { | ||
103 | newNode.left = node.left | ||
104 | newNode.right = node.left | ||
105 | node.left = newNode | ||
106 | newNode.parent = node | ||
107 | return newNode | ||
108 | } else { | ||
109 | node = node.left | ||
110 | } | ||
111 | } else if (comparison > 0) { | ||
112 | if (node.right.leaf) { | ||
113 | newNode.left = node.right | ||
114 | newNode.right = node.right | ||
115 | node.right = newNode | ||
116 | newNode.parent = node | ||
117 | return newNode | ||
118 | } else { | ||
119 | node = node.right | ||
120 | } | ||
121 | } else { // comparison == 0 | ||
122 | newNode.parent = null | ||
123 | node.count++ | ||
124 | return node | ||
125 | } | ||
126 | } | ||
127 | throw new IllegalStateException("Reached leaf node while searching for insertion point") | ||
128 | } | ||
129 | |||
130 | private def augmentRecursively() { | ||
131 | for (var node = this; node !== null; node = node.parent) { | ||
132 | if (!node.augment) { | ||
133 | return | ||
134 | } | ||
135 | } | ||
136 | } | ||
137 | |||
138 | def remove(Interval interval) { | ||
139 | val node = find(interval) | ||
140 | node.count-- | ||
141 | if (node.count == 0) { | ||
142 | return node.remove | ||
143 | } | ||
144 | if (multiplicitySensitive) { | ||
145 | node.augmentRecursively | ||
146 | } | ||
147 | this | ||
148 | } | ||
149 | |||
150 | private def find(Interval interval) { | ||
151 | var node = this | ||
152 | while (!node.leaf) { | ||
153 | val comparison = node.interval.compareTo(interval) | ||
154 | if (comparison < 0) { | ||
155 | node = node.left | ||
156 | } else if (comparison > 0) { | ||
157 | node = node.right | ||
158 | } else { // comparison == 0 | ||
159 | return node | ||
160 | } | ||
161 | } | ||
162 | throw new IllegalStateException("Reached leaf node while searching for interval to remove") | ||
163 | } | ||
164 | |||
165 | override toString() { | ||
166 | if (leaf) { | ||
167 | "L" | ||
168 | } else { | ||
169 | ''' | ||
170 | «IF isRed»R«ELSE»B«ENDIF» «count»«interval» : «result» | ||
171 | «left» | ||
172 | «right» | ||
173 | ''' | ||
174 | } | ||
175 | } | ||
176 | |||
177 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/RedBlackNode.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/RedBlackNode.java new file mode 100644 index 00000000..8c40816b --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/RedBlackNode.java | |||
@@ -0,0 +1,1392 @@ | |||
1 | /* | ||
2 | * The MIT License (MIT) | ||
3 | * | ||
4 | * Copyright (c) 2016 btrekkie | ||
5 | * | ||
6 | * Permission is hereby granted, free of charge, to any person obtaining a copy | ||
7 | * of this software and associated documentation files (the "Software"), to deal | ||
8 | * in the Software without restriction, including without limitation the rights | ||
9 | * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell | ||
10 | * copies of the Software, and to permit persons to whom the Software is | ||
11 | * furnished to do so, subject to the following conditions: | ||
12 | * | ||
13 | * The above copyright notice and this permission notice shall be included in all | ||
14 | * copies or substantial portions of the Software. | ||
15 | * | ||
16 | * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR | ||
17 | * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, | ||
18 | * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE | ||
19 | * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER | ||
20 | * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, | ||
21 | * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE | ||
22 | * SOFTWARE. | ||
23 | */ | ||
24 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval; | ||
25 | |||
26 | import java.lang.reflect.Array; | ||
27 | import java.util.Collection; | ||
28 | import java.util.Comparator; | ||
29 | import java.util.HashSet; | ||
30 | import java.util.Iterator; | ||
31 | import java.util.Set; | ||
32 | |||
33 | /** | ||
34 | * A node in a red-black tree ( https://en.wikipedia.org/wiki/Red%E2%80%93black_tree ). Compared to a class like Java's | ||
35 | * TreeMap, RedBlackNode is a low-level data structure. The internals of a node are exposed as public fields, allowing | ||
36 | * clients to directly observe and manipulate the structure of the tree. This gives clients flexibility, although it | ||
37 | * also enables them to violate the red-black or BST properties. The RedBlackNode class provides methods for performing | ||
38 | * various standard operations, such as insertion and removal. | ||
39 | * | ||
40 | * Unlike most implementations of binary search trees, RedBlackNode supports arbitrary augmentation. By subclassing | ||
41 | * RedBlackNode, clients can add arbitrary data and augmentation information to each node. For example, if we were to | ||
42 | * use a RedBlackNode subclass to implement a sorted set, the subclass would have a field storing an element in the set. | ||
43 | * If we wanted to keep track of the number of non-leaf nodes in each subtree, we would store this as a "size" field and | ||
44 | * override augment() to update this field. All RedBlackNode methods (such as "insert" and remove()) call augment() as | ||
45 | * necessary to correctly maintain the augmentation information, unless otherwise indicated. | ||
46 | * | ||
47 | * The values of the tree are stored in the non-leaf nodes. RedBlackNode does not support use cases where values must be | ||
48 | * stored in the leaf nodes. It is recommended that all of the leaf nodes in a given tree be the same (black) | ||
49 | * RedBlackNode instance, to save space. The root of an empty tree is a leaf node, as opposed to null. | ||
50 | * | ||
51 | * For reference, a red-black tree is a binary search tree satisfying the following properties: | ||
52 | * | ||
53 | * - Every node is colored red or black. | ||
54 | * - The leaf nodes, which are dummy nodes that do not store any values, are colored black. | ||
55 | * - The root is black. | ||
56 | * - Both children of each red node are black. | ||
57 | * - Every path from the root to a leaf contains the same number of black nodes. | ||
58 | * | ||
59 | * @param <N> The type of node in the tree. For example, we might have | ||
60 | * "class FooNode<T> extends RedBlackNode<FooNode<T>>". | ||
61 | * @author Bill Jacobs | ||
62 | */ | ||
63 | public abstract class RedBlackNode<N extends RedBlackNode<N>> implements Comparable<N> { | ||
64 | /** A Comparator that compares Comparable elements using their natural order. */ | ||
65 | private static final Comparator<Comparable<Object>> NATURAL_ORDER = new Comparator<Comparable<Object>>() { | ||
66 | @Override | ||
67 | public int compare(Comparable<Object> value1, Comparable<Object> value2) { | ||
68 | return value1.compareTo(value2); | ||
69 | } | ||
70 | }; | ||
71 | |||
72 | /** The parent of this node, if any. "parent" is null if this is a leaf node. */ | ||
73 | public N parent; | ||
74 | |||
75 | /** The left child of this node. "left" is null if this is a leaf node. */ | ||
76 | public N left; | ||
77 | |||
78 | /** The right child of this node. "right" is null if this is a leaf node. */ | ||
79 | public N right; | ||
80 | |||
81 | /** Whether the node is colored red, as opposed to black. */ | ||
82 | public boolean isRed; | ||
83 | |||
84 | /** | ||
85 | * Sets any augmentation information about the subtree rooted at this node that is stored in this node. For | ||
86 | * example, if we augment each node by subtree size (the number of non-leaf nodes in the subtree), this method would | ||
87 | * set the size field of this node to be equal to the size field of the left child plus the size field of the right | ||
88 | * child plus one. | ||
89 | * | ||
90 | * "Augmentation information" is information that we can compute about a subtree rooted at some node, preferably | ||
91 | * based only on the augmentation information in the node's two children and the information in the node. Examples | ||
92 | * of augmentation information are the sum of the values in a subtree and the number of non-leaf nodes in a subtree. | ||
93 | * Augmentation information may not depend on the colors of the nodes. | ||
94 | * | ||
95 | * This method returns whether the augmentation information in any of the ancestors of this node might have been | ||
96 | * affected by changes in this subtree since the last call to augment(). In the usual case, where the augmentation | ||
97 | * information depends only on the information in this node and the augmentation information in its immediate | ||
98 | * children, this is equivalent to whether the augmentation information changed as a result of this call to | ||
99 | * augment(). For example, in the case of subtree size, this returns whether the value of the size field prior to | ||
100 | * calling augment() differed from the size field of the left child plus the size field of the right child plus one. | ||
101 | * False positives are permitted. The return value is unspecified if we have not called augment() on this node | ||
102 | * before. | ||
103 | * | ||
104 | * This method may assume that this is not a leaf node. It may not assume that the augmentation information stored | ||
105 | * in any of the tree's nodes is correct. However, if the augmentation information stored in all of the node's | ||
106 | * descendants is correct, then the augmentation information stored in this node must be correct after calling | ||
107 | * augment(). | ||
108 | */ | ||
109 | public boolean augment() { | ||
110 | return false; | ||
111 | } | ||
112 | |||
113 | /** | ||
114 | * Throws a RuntimeException if we detect that this node locally violates any invariants specific to this subclass | ||
115 | * of RedBlackNode. For example, if this stores the size of the subtree rooted at this node, this should throw a | ||
116 | * RuntimeException if the size field of this is not equal to the size field of the left child plus the size field | ||
117 | * of the right child plus one. Note that we may call this on a leaf node. | ||
118 | * | ||
119 | * assertSubtreeIsValid() calls assertNodeIsValid() on each node, or at least starts to do so until it detects a | ||
120 | * problem. assertNodeIsValid() should assume the node is in a tree that satisfies all properties common to all | ||
121 | * red-black trees, as assertSubtreeIsValid() is responsible for such checks. assertNodeIsValid() should be | ||
122 | * "downward-looking", i.e. it should ignore any information in "parent", and it should be "local", i.e. it should | ||
123 | * only check a constant number of descendants. To include "global" checks, such as verifying the BST property | ||
124 | * concerning ordering, override assertSubtreeIsValid(). assertOrderIsValid is useful for checking the BST | ||
125 | * property. | ||
126 | */ | ||
127 | public void assertNodeIsValid() { | ||
128 | |||
129 | } | ||
130 | |||
131 | /** Returns whether this is a leaf node. */ | ||
132 | public boolean isLeaf() { | ||
133 | return left == null; | ||
134 | } | ||
135 | |||
136 | /** Returns the root of the tree that contains this node. */ | ||
137 | public N root() { | ||
138 | @SuppressWarnings("unchecked") | ||
139 | N node = (N)this; | ||
140 | while (node.parent != null) { | ||
141 | node = node.parent; | ||
142 | } | ||
143 | return node; | ||
144 | } | ||
145 | |||
146 | /** Returns the first node in the subtree rooted at this node, if any. */ | ||
147 | public N min() { | ||
148 | if (isLeaf()) { | ||
149 | return null; | ||
150 | } | ||
151 | @SuppressWarnings("unchecked") | ||
152 | N node = (N)this; | ||
153 | while (!node.left.isLeaf()) { | ||
154 | node = node.left; | ||
155 | } | ||
156 | return node; | ||
157 | } | ||
158 | |||
159 | /** Returns the last node in the subtree rooted at this node, if any. */ | ||
160 | public N max() { | ||
161 | if (isLeaf()) { | ||
162 | return null; | ||
163 | } | ||
164 | @SuppressWarnings("unchecked") | ||
165 | N node = (N)this; | ||
166 | while (!node.right.isLeaf()) { | ||
167 | node = node.right; | ||
168 | } | ||
169 | return node; | ||
170 | } | ||
171 | |||
172 | /** Returns the node immediately before this in the tree that contains this node, if any. */ | ||
173 | public N predecessor() { | ||
174 | if (!left.isLeaf()) { | ||
175 | N node; | ||
176 | for (node = left; !node.right.isLeaf(); node = node.right); | ||
177 | return node; | ||
178 | } else if (parent == null) { | ||
179 | return null; | ||
180 | } else { | ||
181 | @SuppressWarnings("unchecked") | ||
182 | N node = (N)this; | ||
183 | while (node.parent != null && node.parent.left == node) { | ||
184 | node = node.parent; | ||
185 | } | ||
186 | return node.parent; | ||
187 | } | ||
188 | } | ||
189 | |||
190 | /** Returns the node immediately after this in the tree that contains this node, if any. */ | ||
191 | public N successor() { | ||
192 | if (!right.isLeaf()) { | ||
193 | N node; | ||
194 | for (node = right; !node.left.isLeaf(); node = node.left); | ||
195 | return node; | ||
196 | } else if (parent == null) { | ||
197 | return null; | ||
198 | } else { | ||
199 | @SuppressWarnings("unchecked") | ||
200 | N node = (N)this; | ||
201 | while (node.parent != null && node.parent.right == node) { | ||
202 | node = node.parent; | ||
203 | } | ||
204 | return node.parent; | ||
205 | } | ||
206 | } | ||
207 | |||
208 | /** | ||
209 | * Performs a left rotation about this node. This method assumes that !isLeaf() && !right.isLeaf(). It calls | ||
210 | * augment() on this node and on its resulting parent. However, it does not call augment() on any of the resulting | ||
211 | * parent's ancestors, because that is normally the responsibility of the caller. | ||
212 | * @return The return value from calling augment() on the resulting parent. | ||
213 | */ | ||
214 | public boolean rotateLeft() { | ||
215 | if (isLeaf() || right.isLeaf()) { | ||
216 | throw new IllegalArgumentException("The node or its right child is a leaf"); | ||
217 | } | ||
218 | N newParent = right; | ||
219 | right = newParent.left; | ||
220 | @SuppressWarnings("unchecked") | ||
221 | N nThis = (N)this; | ||
222 | if (!right.isLeaf()) { | ||
223 | right.parent = nThis; | ||
224 | } | ||
225 | newParent.parent = parent; | ||
226 | parent = newParent; | ||
227 | newParent.left = nThis; | ||
228 | if (newParent.parent != null) { | ||
229 | if (newParent.parent.left == this) { | ||
230 | newParent.parent.left = newParent; | ||
231 | } else { | ||
232 | newParent.parent.right = newParent; | ||
233 | } | ||
234 | } | ||
235 | augment(); | ||
236 | return newParent.augment(); | ||
237 | } | ||
238 | |||
239 | /** | ||
240 | * Performs a right rotation about this node. This method assumes that !isLeaf() && !left.isLeaf(). It calls | ||
241 | * augment() on this node and on its resulting parent. However, it does not call augment() on any of the resulting | ||
242 | * parent's ancestors, because that is normally the responsibility of the caller. | ||
243 | * @return The return value from calling augment() on the resulting parent. | ||
244 | */ | ||
245 | public boolean rotateRight() { | ||
246 | if (isLeaf() || left.isLeaf()) { | ||
247 | throw new IllegalArgumentException("The node or its left child is a leaf"); | ||
248 | } | ||
249 | N newParent = left; | ||
250 | left = newParent.right; | ||
251 | @SuppressWarnings("unchecked") | ||
252 | N nThis = (N)this; | ||
253 | if (!left.isLeaf()) { | ||
254 | left.parent = nThis; | ||
255 | } | ||
256 | newParent.parent = parent; | ||
257 | parent = newParent; | ||
258 | newParent.right = nThis; | ||
259 | if (newParent.parent != null) { | ||
260 | if (newParent.parent.left == this) { | ||
261 | newParent.parent.left = newParent; | ||
262 | } else { | ||
263 | newParent.parent.right = newParent; | ||
264 | } | ||
265 | } | ||
266 | augment(); | ||
267 | return newParent.augment(); | ||
268 | } | ||
269 | |||
270 | /** | ||
271 | * Performs red-black insertion fixup. To be more precise, this fixes a tree that satisfies all of the requirements | ||
272 | * of red-black trees, except that this may be a red child of a red node, and if this is the root, the root may be | ||
273 | * red. node.isRed must initially be true. This method assumes that this is not a leaf node. The method performs | ||
274 | * any rotations by calling rotateLeft() and rotateRight(). This method is more efficient than fixInsertion if | ||
275 | * "augment" is false or augment() might return false. | ||
276 | * @param augment Whether to set the augmentation information for "node" and its ancestors, by calling augment(). | ||
277 | */ | ||
278 | public void fixInsertionWithoutGettingRoot(boolean augment) { | ||
279 | if (!isRed) { | ||
280 | throw new IllegalArgumentException("The node must be red"); | ||
281 | } | ||
282 | boolean changed = augment; | ||
283 | if (augment) { | ||
284 | augment(); | ||
285 | } | ||
286 | |||
287 | RedBlackNode<N> node = this; | ||
288 | while (node.parent != null && node.parent.isRed) { | ||
289 | N parent = node.parent; | ||
290 | N grandparent = parent.parent; | ||
291 | if (grandparent.left.isRed && grandparent.right.isRed) { | ||
292 | grandparent.left.isRed = false; | ||
293 | grandparent.right.isRed = false; | ||
294 | grandparent.isRed = true; | ||
295 | |||
296 | if (changed) { | ||
297 | changed = parent.augment(); | ||
298 | if (changed) { | ||
299 | changed = grandparent.augment(); | ||
300 | } | ||
301 | } | ||
302 | node = grandparent; | ||
303 | } else { | ||
304 | if (parent.left == node) { | ||
305 | if (grandparent.right == parent) { | ||
306 | parent.rotateRight(); | ||
307 | node = parent; | ||
308 | parent = node.parent; | ||
309 | } | ||
310 | } else if (grandparent.left == parent) { | ||
311 | parent.rotateLeft(); | ||
312 | node = parent; | ||
313 | parent = node.parent; | ||
314 | } | ||
315 | |||
316 | if (parent.left == node) { | ||
317 | boolean grandparentChanged = grandparent.rotateRight(); | ||
318 | if (augment) { | ||
319 | changed = grandparentChanged; | ||
320 | } | ||
321 | } else { | ||
322 | boolean grandparentChanged = grandparent.rotateLeft(); | ||
323 | if (augment) { | ||
324 | changed = grandparentChanged; | ||
325 | } | ||
326 | } | ||
327 | |||
328 | parent.isRed = false; | ||
329 | grandparent.isRed = true; | ||
330 | node = parent; | ||
331 | break; | ||
332 | } | ||
333 | } | ||
334 | |||
335 | if (node.parent == null) { | ||
336 | node.isRed = false; | ||
337 | } | ||
338 | if (changed) { | ||
339 | for (node = node.parent; node != null; node = node.parent) { | ||
340 | if (!node.augment()) { | ||
341 | break; | ||
342 | } | ||
343 | } | ||
344 | } | ||
345 | } | ||
346 | |||
347 | /** | ||
348 | * Performs red-black insertion fixup. To be more precise, this fixes a tree that satisfies all of the requirements | ||
349 | * of red-black trees, except that this may be a red child of a red node, and if this is the root, the root may be | ||
350 | * red. node.isRed must initially be true. This method assumes that this is not a leaf node. The method performs | ||
351 | * any rotations by calling rotateLeft() and rotateRight(). This method is more efficient than fixInsertion() if | ||
352 | * augment() might return false. | ||
353 | */ | ||
354 | public void fixInsertionWithoutGettingRoot() { | ||
355 | fixInsertionWithoutGettingRoot(true); | ||
356 | } | ||
357 | |||
358 | /** | ||
359 | * Performs red-black insertion fixup. To be more precise, this fixes a tree that satisfies all of the requirements | ||
360 | * of red-black trees, except that this may be a red child of a red node, and if this is the root, the root may be | ||
361 | * red. node.isRed must initially be true. This method assumes that this is not a leaf node. The method performs | ||
362 | * any rotations by calling rotateLeft() and rotateRight(). | ||
363 | * @param augment Whether to set the augmentation information for "node" and its ancestors, by calling augment(). | ||
364 | * @return The root of the resulting tree. | ||
365 | */ | ||
366 | public N fixInsertion(boolean augment) { | ||
367 | fixInsertionWithoutGettingRoot(augment); | ||
368 | return root(); | ||
369 | } | ||
370 | |||
371 | /** | ||
372 | * Performs red-black insertion fixup. To be more precise, this fixes a tree that satisfies all of the requirements | ||
373 | * of red-black trees, except that this may be a red child of a red node, and if this is the root, the root may be | ||
374 | * red. node.isRed must initially be true. This method assumes that this is not a leaf node. The method performs | ||
375 | * any rotations by calling rotateLeft() and rotateRight(). | ||
376 | * @return The root of the resulting tree. | ||
377 | */ | ||
378 | public N fixInsertion() { | ||
379 | fixInsertionWithoutGettingRoot(true); | ||
380 | return root(); | ||
381 | } | ||
382 | |||
383 | /** Returns a Comparator that compares instances of N using their natural order, as in N.compareTo. */ | ||
384 | @SuppressWarnings({"rawtypes", "unchecked"}) | ||
385 | private Comparator<N> naturalOrder() { | ||
386 | Comparator comparator = (Comparator)NATURAL_ORDER; | ||
387 | return (Comparator<N>)comparator; | ||
388 | } | ||
389 | |||
390 | /** | ||
391 | * Inserts the specified node into the tree rooted at this node. Assumes this is the root. We treat newNode as a | ||
392 | * solitary node that does not belong to any tree, and we ignore its initial "parent", "left", "right", and isRed | ||
393 | * fields. | ||
394 | * | ||
395 | * If it is not efficient or convenient to find the location for a node using a Comparator, then you should manually | ||
396 | * add the node to the appropriate location, color it red, and call fixInsertion(). | ||
397 | * | ||
398 | * @param newNode The node to insert. | ||
399 | * @param allowDuplicates Whether to insert newNode if there is an equal node in the tree. To check whether we | ||
400 | * inserted newNode, check whether newNode.parent is null and the return value differs from newNode. | ||
401 | * @param comparator A comparator indicating where to put the node. If this is null, we use the nodes' natural | ||
402 | * order, as in N.compareTo. If you are passing null, then you must override the compareTo method, because the | ||
403 | * default implementation requires the nodes to already be in the same tree. | ||
404 | * @return The root of the resulting tree. | ||
405 | */ | ||
406 | public N insert(N newNode, boolean allowDuplicates, Comparator<? super N> comparator) { | ||
407 | if (parent != null) { | ||
408 | throw new IllegalArgumentException("This is not the root of a tree"); | ||
409 | } | ||
410 | @SuppressWarnings("unchecked") | ||
411 | N nThis = (N)this; | ||
412 | if (isLeaf()) { | ||
413 | newNode.isRed = false; | ||
414 | newNode.left = nThis; | ||
415 | newNode.right = nThis; | ||
416 | newNode.parent = null; | ||
417 | newNode.augment(); | ||
418 | return newNode; | ||
419 | } | ||
420 | if (comparator == null) { | ||
421 | comparator = naturalOrder(); | ||
422 | } | ||
423 | |||
424 | N node = nThis; | ||
425 | int comparison; | ||
426 | while (true) { | ||
427 | comparison = comparator.compare(newNode, node); | ||
428 | if (comparison < 0) { | ||
429 | if (!node.left.isLeaf()) { | ||
430 | node = node.left; | ||
431 | } else { | ||
432 | newNode.left = node.left; | ||
433 | newNode.right = node.left; | ||
434 | node.left = newNode; | ||
435 | newNode.parent = node; | ||
436 | break; | ||
437 | } | ||
438 | } else if (comparison > 0 || allowDuplicates) { | ||
439 | if (!node.right.isLeaf()) { | ||
440 | node = node.right; | ||
441 | } else { | ||
442 | newNode.left = node.right; | ||
443 | newNode.right = node.right; | ||
444 | node.right = newNode; | ||
445 | newNode.parent = node; | ||
446 | break; | ||
447 | } | ||
448 | } else { | ||
449 | newNode.parent = null; | ||
450 | return nThis; | ||
451 | } | ||
452 | } | ||
453 | newNode.isRed = true; | ||
454 | return newNode.fixInsertion(); | ||
455 | } | ||
456 | |||
457 | /** | ||
458 | * Moves this node to its successor's former position in the tree and vice versa, i.e. sets the "left", "right", | ||
459 | * "parent", and isRed fields of each. This method assumes that this is not a leaf node. | ||
460 | * @return The node with which we swapped. | ||
461 | */ | ||
462 | private N swapWithSuccessor() { | ||
463 | N replacement = successor(); | ||
464 | boolean oldReplacementIsRed = replacement.isRed; | ||
465 | N oldReplacementLeft = replacement.left; | ||
466 | N oldReplacementRight = replacement.right; | ||
467 | N oldReplacementParent = replacement.parent; | ||
468 | |||
469 | replacement.isRed = isRed; | ||
470 | replacement.left = left; | ||
471 | replacement.right = right; | ||
472 | replacement.parent = parent; | ||
473 | if (parent != null) { | ||
474 | if (parent.left == this) { | ||
475 | parent.left = replacement; | ||
476 | } else { | ||
477 | parent.right = replacement; | ||
478 | } | ||
479 | } | ||
480 | |||
481 | @SuppressWarnings("unchecked") | ||
482 | N nThis = (N)this; | ||
483 | isRed = oldReplacementIsRed; | ||
484 | left = oldReplacementLeft; | ||
485 | right = oldReplacementRight; | ||
486 | if (oldReplacementParent == this) { | ||
487 | parent = replacement; | ||
488 | parent.right = nThis; | ||
489 | } else { | ||
490 | parent = oldReplacementParent; | ||
491 | parent.left = nThis; | ||
492 | } | ||
493 | |||
494 | replacement.right.parent = replacement; | ||
495 | if (!replacement.left.isLeaf()) { | ||
496 | replacement.left.parent = replacement; | ||
497 | } | ||
498 | if (!right.isLeaf()) { | ||
499 | right.parent = nThis; | ||
500 | } | ||
501 | return replacement; | ||
502 | } | ||
503 | |||
504 | /** | ||
505 | * Performs red-black deletion fixup. To be more precise, this fixes a tree that satisfies all of the requirements | ||
506 | * of red-black trees, except that all paths from the root to a leaf that pass through the sibling of this node have | ||
507 | * one fewer black node than all other root-to-leaf paths. This method assumes that this is not a leaf node. | ||
508 | */ | ||
509 | private void fixSiblingDeletion() { | ||
510 | RedBlackNode<N> sibling = this; | ||
511 | boolean changed = true; | ||
512 | boolean haveAugmentedParent = false; | ||
513 | boolean haveAugmentedGrandparent = false; | ||
514 | while (true) { | ||
515 | N parent = sibling.parent; | ||
516 | if (sibling.isRed) { | ||
517 | parent.isRed = true; | ||
518 | sibling.isRed = false; | ||
519 | if (parent.left == sibling) { | ||
520 | changed = parent.rotateRight(); | ||
521 | sibling = parent.left; | ||
522 | } else { | ||
523 | changed = parent.rotateLeft(); | ||
524 | sibling = parent.right; | ||
525 | } | ||
526 | haveAugmentedParent = true; | ||
527 | haveAugmentedGrandparent = true; | ||
528 | } else if (!sibling.left.isRed && !sibling.right.isRed) { | ||
529 | sibling.isRed = true; | ||
530 | if (parent.isRed) { | ||
531 | parent.isRed = false; | ||
532 | break; | ||
533 | } else { | ||
534 | if (changed && !haveAugmentedParent) { | ||
535 | changed = parent.augment(); | ||
536 | } | ||
537 | N grandparent = parent.parent; | ||
538 | if (grandparent == null) { | ||
539 | break; | ||
540 | } else if (grandparent.left == parent) { | ||
541 | sibling = grandparent.right; | ||
542 | } else { | ||
543 | sibling = grandparent.left; | ||
544 | } | ||
545 | haveAugmentedParent = haveAugmentedGrandparent; | ||
546 | haveAugmentedGrandparent = false; | ||
547 | } | ||
548 | } else { | ||
549 | if (sibling == parent.left) { | ||
550 | if (!sibling.left.isRed) { | ||
551 | sibling.rotateLeft(); | ||
552 | sibling = sibling.parent; | ||
553 | } | ||
554 | } else if (!sibling.right.isRed) { | ||
555 | sibling.rotateRight(); | ||
556 | sibling = sibling.parent; | ||
557 | } | ||
558 | sibling.isRed = parent.isRed; | ||
559 | parent.isRed = false; | ||
560 | if (sibling == parent.left) { | ||
561 | sibling.left.isRed = false; | ||
562 | changed = parent.rotateRight(); | ||
563 | } else { | ||
564 | sibling.right.isRed = false; | ||
565 | changed = parent.rotateLeft(); | ||
566 | } | ||
567 | haveAugmentedParent = haveAugmentedGrandparent; | ||
568 | haveAugmentedGrandparent = false; | ||
569 | break; | ||
570 | } | ||
571 | } | ||
572 | |||
573 | // Update augmentation info | ||
574 | N parent = sibling.parent; | ||
575 | if (changed && parent != null) { | ||
576 | if (!haveAugmentedParent) { | ||
577 | changed = parent.augment(); | ||
578 | } | ||
579 | if (changed && parent.parent != null) { | ||
580 | parent = parent.parent; | ||
581 | if (!haveAugmentedGrandparent) { | ||
582 | changed = parent.augment(); | ||
583 | } | ||
584 | if (changed) { | ||
585 | for (parent = parent.parent; parent != null; parent = parent.parent) { | ||
586 | if (!parent.augment()) { | ||
587 | break; | ||
588 | } | ||
589 | } | ||
590 | } | ||
591 | } | ||
592 | } | ||
593 | } | ||
594 | |||
595 | /** | ||
596 | * Removes this node from the tree that contains it. The effect of this method on the fields of this node is | ||
597 | * unspecified. This method assumes that this is not a leaf node. This method is more efficient than remove() if | ||
598 | * augment() might return false. | ||
599 | * | ||
600 | * If the node has two children, we begin by moving the node's successor to its former position, by changing the | ||
601 | * successor's "left", "right", "parent", and isRed fields. | ||
602 | */ | ||
603 | public void removeWithoutGettingRoot() { | ||
604 | if (isLeaf()) { | ||
605 | throw new IllegalArgumentException("Attempted to remove a leaf node"); | ||
606 | } | ||
607 | N replacement; | ||
608 | if (left.isLeaf() || right.isLeaf()) { | ||
609 | replacement = null; | ||
610 | } else { | ||
611 | replacement = swapWithSuccessor(); | ||
612 | } | ||
613 | |||
614 | N child; | ||
615 | if (!left.isLeaf()) { | ||
616 | child = left; | ||
617 | } else if (!right.isLeaf()) { | ||
618 | child = right; | ||
619 | } else { | ||
620 | child = null; | ||
621 | } | ||
622 | |||
623 | if (child != null) { | ||
624 | // Replace this node with its child | ||
625 | child.parent = parent; | ||
626 | if (parent != null) { | ||
627 | if (parent.left == this) { | ||
628 | parent.left = child; | ||
629 | } else { | ||
630 | parent.right = child; | ||
631 | } | ||
632 | } | ||
633 | child.isRed = false; | ||
634 | |||
635 | if (child.parent != null) { | ||
636 | N parent; | ||
637 | for (parent = child.parent; parent != null; parent = parent.parent) { | ||
638 | if (!parent.augment()) { | ||
639 | break; | ||
640 | } | ||
641 | } | ||
642 | } | ||
643 | } else if (parent != null) { | ||
644 | // Replace this node with a leaf node | ||
645 | N leaf = left; | ||
646 | N parent = this.parent; | ||
647 | N sibling; | ||
648 | if (parent.left == this) { | ||
649 | parent.left = leaf; | ||
650 | sibling = parent.right; | ||
651 | } else { | ||
652 | parent.right = leaf; | ||
653 | sibling = parent.left; | ||
654 | } | ||
655 | |||
656 | if (!isRed) { | ||
657 | RedBlackNode<N> siblingNode = sibling; | ||
658 | siblingNode.fixSiblingDeletion(); | ||
659 | } else { | ||
660 | while (parent != null) { | ||
661 | if (!parent.augment()) { | ||
662 | break; | ||
663 | } | ||
664 | parent = parent.parent; | ||
665 | } | ||
666 | } | ||
667 | } | ||
668 | |||
669 | if (replacement != null) { | ||
670 | replacement.augment(); | ||
671 | for (N parent = replacement.parent; parent != null; parent = parent.parent) { | ||
672 | if (!parent.augment()) { | ||
673 | break; | ||
674 | } | ||
675 | } | ||
676 | } | ||
677 | |||
678 | // Clear any previously existing links, so that we're more likely to encounter an exception if we attempt to | ||
679 | // access the removed node | ||
680 | parent = null; | ||
681 | left = null; | ||
682 | right = null; | ||
683 | isRed = true; | ||
684 | } | ||
685 | |||
686 | /** | ||
687 | * Removes this node from the tree that contains it. The effect of this method on the fields of this node is | ||
688 | * unspecified. This method assumes that this is not a leaf node. | ||
689 | * | ||
690 | * If the node has two children, we begin by moving the node's successor to its former position, by changing the | ||
691 | * successor's "left", "right", "parent", and isRed fields. | ||
692 | * | ||
693 | * @return The root of the resulting tree. | ||
694 | */ | ||
695 | public N remove() { | ||
696 | if (isLeaf()) { | ||
697 | throw new IllegalArgumentException("Attempted to remove a leaf node"); | ||
698 | } | ||
699 | |||
700 | // Find an arbitrary non-leaf node in the tree other than this node | ||
701 | N node; | ||
702 | if (parent != null) { | ||
703 | node = parent; | ||
704 | } else if (!left.isLeaf()) { | ||
705 | node = left; | ||
706 | } else if (!right.isLeaf()) { | ||
707 | node = right; | ||
708 | } else { | ||
709 | return left; | ||
710 | } | ||
711 | |||
712 | removeWithoutGettingRoot(); | ||
713 | return node.root(); | ||
714 | } | ||
715 | |||
716 | /** | ||
717 | * Returns the root of a perfectly height-balanced subtree containing the next "size" (non-leaf) nodes from | ||
718 | * "iterator", in iteration order. This method is responsible for setting the "left", "right", "parent", and isRed | ||
719 | * fields of the nodes, and calling augment() as appropriate. It ignores the initial values of the "left", "right", | ||
720 | * "parent", and isRed fields. | ||
721 | * @param iterator The nodes. | ||
722 | * @param size The number of nodes. | ||
723 | * @param height The "height" of the subtree's root node above the deepest leaf in the tree that contains it. Since | ||
724 | * insertion fixup is slow if there are too many red nodes and deleteion fixup is slow if there are too few red | ||
725 | * nodes, we compromise and have red nodes at every fourth level. We color a node red iff its "height" is equal | ||
726 | * to 1 mod 4. | ||
727 | * @param leaf The leaf node. | ||
728 | * @return The root of the subtree. | ||
729 | */ | ||
730 | private static <N extends RedBlackNode<N>> N createTree( | ||
731 | Iterator<? extends N> iterator, int size, int height, N leaf) { | ||
732 | if (size == 0) { | ||
733 | return leaf; | ||
734 | } else { | ||
735 | N left = createTree(iterator, (size - 1) / 2, height - 1, leaf); | ||
736 | N node = iterator.next(); | ||
737 | N right = createTree(iterator, size / 2, height - 1, leaf); | ||
738 | |||
739 | node.isRed = height % 4 == 1; | ||
740 | node.left = left; | ||
741 | node.right = right; | ||
742 | if (!left.isLeaf()) { | ||
743 | left.parent = node; | ||
744 | } | ||
745 | if (!right.isLeaf()) { | ||
746 | right.parent = node; | ||
747 | } | ||
748 | |||
749 | node.augment(); | ||
750 | return node; | ||
751 | } | ||
752 | } | ||
753 | |||
754 | /** | ||
755 | * Returns the root of a perfectly height-balanced tree containing the specified nodes, in iteration order. This | ||
756 | * method is responsible for setting the "left", "right", "parent", and isRed fields of the nodes (excluding | ||
757 | * "leaf"), and calling augment() as appropriate. It ignores the initial values of the "left", "right", "parent", | ||
758 | * and isRed fields. | ||
759 | * @param nodes The nodes. | ||
760 | * @param leaf The leaf node. | ||
761 | * @return The root of the tree. | ||
762 | */ | ||
763 | public static <N extends RedBlackNode<N>> N createTree(Collection<? extends N> nodes, N leaf) { | ||
764 | int size = nodes.size(); | ||
765 | if (size == 0) { | ||
766 | return leaf; | ||
767 | } | ||
768 | |||
769 | int height = 0; | ||
770 | for (int subtreeSize = size; subtreeSize > 0; subtreeSize /= 2) { | ||
771 | height++; | ||
772 | } | ||
773 | |||
774 | N node = createTree(nodes.iterator(), size, height, leaf); | ||
775 | node.parent = null; | ||
776 | node.isRed = false; | ||
777 | return node; | ||
778 | } | ||
779 | |||
780 | /** | ||
781 | * Concatenates to the end of the tree rooted at this node. To be precise, given that all of the nodes in this | ||
782 | * precede the node "pivot", which precedes all of the nodes in "last", this returns the root of a tree containing | ||
783 | * all of these nodes. This method destroys the trees rooted at "this" and "last". We treat "pivot" as a solitary | ||
784 | * node that does not belong to any tree, and we ignore its initial "parent", "left", "right", and isRed fields. | ||
785 | * This method assumes that this node and "last" are the roots of their respective trees. | ||
786 | * | ||
787 | * This method takes O(log N) time. It is more efficient than inserting "pivot" and then calling concatenate(last). | ||
788 | * It is considerably more efficient than inserting "pivot" and all of the nodes in "last". | ||
789 | */ | ||
790 | public N concatenate(N last, N pivot) { | ||
791 | // If the black height of "first", where first = this, is less than or equal to that of "last", starting at the | ||
792 | // root of "last", we keep going left until we reach a black node whose black height is equal to that of | ||
793 | // "first". Then, we make "pivot" the parent of that node and of "first", coloring it red, and perform | ||
794 | // insertion fixup on the pivot. If the black height of "first" is greater than that of "last", we do the | ||
795 | // mirror image of the above. | ||
796 | |||
797 | if (parent != null) { | ||
798 | throw new IllegalArgumentException("This is not the root of a tree"); | ||
799 | } | ||
800 | if (last.parent != null) { | ||
801 | throw new IllegalArgumentException("\"last\" is not the root of a tree"); | ||
802 | } | ||
803 | |||
804 | // Compute the black height of the trees | ||
805 | int firstBlackHeight = 0; | ||
806 | @SuppressWarnings("unchecked") | ||
807 | N first = (N)this; | ||
808 | for (N node = first; node != null; node = node.right) { | ||
809 | if (!node.isRed) { | ||
810 | firstBlackHeight++; | ||
811 | } | ||
812 | } | ||
813 | int lastBlackHeight = 0; | ||
814 | for (N node = last; node != null; node = node.right) { | ||
815 | if (!node.isRed) { | ||
816 | lastBlackHeight++; | ||
817 | } | ||
818 | } | ||
819 | |||
820 | // Identify the children and parent of pivot | ||
821 | N firstChild = first; | ||
822 | N lastChild = last; | ||
823 | N parent; | ||
824 | if (firstBlackHeight <= lastBlackHeight) { | ||
825 | parent = null; | ||
826 | int blackHeight = lastBlackHeight; | ||
827 | while (blackHeight > firstBlackHeight) { | ||
828 | if (!lastChild.isRed) { | ||
829 | blackHeight--; | ||
830 | } | ||
831 | parent = lastChild; | ||
832 | lastChild = lastChild.left; | ||
833 | } | ||
834 | if (lastChild.isRed) { | ||
835 | parent = lastChild; | ||
836 | lastChild = lastChild.left; | ||
837 | } | ||
838 | } else { | ||
839 | parent = null; | ||
840 | int blackHeight = firstBlackHeight; | ||
841 | while (blackHeight > lastBlackHeight) { | ||
842 | if (!firstChild.isRed) { | ||
843 | blackHeight--; | ||
844 | } | ||
845 | parent = firstChild; | ||
846 | firstChild = firstChild.right; | ||
847 | } | ||
848 | if (firstChild.isRed) { | ||
849 | parent = firstChild; | ||
850 | firstChild = firstChild.right; | ||
851 | } | ||
852 | } | ||
853 | |||
854 | // Add "pivot" to the tree | ||
855 | pivot.isRed = true; | ||
856 | pivot.parent = parent; | ||
857 | if (parent != null) { | ||
858 | if (firstBlackHeight < lastBlackHeight) { | ||
859 | parent.left = pivot; | ||
860 | } else { | ||
861 | parent.right = pivot; | ||
862 | } | ||
863 | } | ||
864 | pivot.left = firstChild; | ||
865 | if (!firstChild.isLeaf()) { | ||
866 | firstChild.parent = pivot; | ||
867 | } | ||
868 | pivot.right = lastChild; | ||
869 | if (!lastChild.isLeaf()) { | ||
870 | lastChild.parent = pivot; | ||
871 | } | ||
872 | |||
873 | // Perform insertion fixup | ||
874 | return pivot.fixInsertion(); | ||
875 | } | ||
876 | |||
877 | /** | ||
878 | * Concatenates the tree rooted at "last" to the end of the tree rooted at this node. To be precise, given that all | ||
879 | * of the nodes in this precede all of the nodes in "last", this returns the root of a tree containing all of these | ||
880 | * nodes. This method destroys the trees rooted at "this" and "last". It assumes that this node and "last" are the | ||
881 | * roots of their respective trees. This method takes O(log N) time. It is considerably more efficient than | ||
882 | * inserting all of the nodes in "last". | ||
883 | */ | ||
884 | public N concatenate(N last) { | ||
885 | if (parent != null || last.parent != null) { | ||
886 | throw new IllegalArgumentException("The node is not the root of a tree"); | ||
887 | } | ||
888 | if (isLeaf()) { | ||
889 | return last; | ||
890 | } else if (last.isLeaf()) { | ||
891 | @SuppressWarnings("unchecked") | ||
892 | N nThis = (N)this; | ||
893 | return nThis; | ||
894 | } else { | ||
895 | N node = last.min(); | ||
896 | last = node.remove(); | ||
897 | return concatenate(last, node); | ||
898 | } | ||
899 | } | ||
900 | |||
901 | /** | ||
902 | * Splits the tree rooted at this node into two trees, so that the first element of the return value is the root of | ||
903 | * a tree consisting of the nodes that were before the specified node, and the second element of the return value is | ||
904 | * the root of a tree consisting of the nodes that were equal to or after the specified node. This method is | ||
905 | * destructive, meaning it does not preserve the original tree. It assumes that this node is the root and is in the | ||
906 | * same tree as splitNode. It takes O(log N) time. It is considerably more efficient than removing all of the | ||
907 | * nodes at or after splitNode and then creating a new tree from those nodes. | ||
908 | * @param The node at which to split the tree. | ||
909 | * @return An array consisting of the resulting trees. | ||
910 | */ | ||
911 | public N[] split(N splitNode) { | ||
912 | // To split the tree, we accumulate a pre-split tree and a post-split tree. We walk down the tree toward the | ||
913 | // position where we are splitting. Whenever we go left, we concatenate the right subtree with the post-split | ||
914 | // tree, and whenever we go right, we concatenate the pre-split tree with the left subtree. We use the | ||
915 | // concatenation algorithm described in concatenate(Object, Object). For the pivot, we use the last node where | ||
916 | // we went left in the case of a left move, and the last node where we went right in the case of a right move. | ||
917 | // | ||
918 | // The method uses the following variables: | ||
919 | // | ||
920 | // node: The current node in our walk down the tree. | ||
921 | // first: A node on the right spine of the pre-split tree. At the beginning of each iteration, it is the black | ||
922 | // node with the same black height as "node". If the pre-split tree is empty, this is null instead. | ||
923 | // firstParent: The parent of "first". If the pre-split tree is empty, this is null. Otherwise, this is the | ||
924 | // same as first.parent, unless first.isLeaf(). | ||
925 | // firstPivot: The node where we last went right, i.e. the next node to use as a pivot when concatenating with | ||
926 | // the pre-split tree. | ||
927 | // advanceFirst: Whether to set "first" to be its next black descendant at the end of the loop. | ||
928 | // last, lastParent, lastPivot, advanceLast: Analogous to "first", firstParent, firstPivot, and advanceFirst, | ||
929 | // but for the post-split tree. | ||
930 | if (parent != null) { | ||
931 | throw new IllegalArgumentException("This is not the root of a tree"); | ||
932 | } | ||
933 | if (isLeaf() || splitNode.isLeaf()) { | ||
934 | throw new IllegalArgumentException("The root or the split node is a leaf"); | ||
935 | } | ||
936 | |||
937 | // Create an array containing the path from the root to splitNode | ||
938 | int depth = 1; | ||
939 | N parent; | ||
940 | for (parent = splitNode; parent.parent != null; parent = parent.parent) { | ||
941 | depth++; | ||
942 | } | ||
943 | if (parent != this) { | ||
944 | throw new IllegalArgumentException("The split node does not belong to this tree"); | ||
945 | } | ||
946 | RedBlackNode<?>[] path = new RedBlackNode<?>[depth]; | ||
947 | for (parent = splitNode; parent != null; parent = parent.parent) { | ||
948 | depth--; | ||
949 | path[depth] = parent; | ||
950 | } | ||
951 | |||
952 | @SuppressWarnings("unchecked") | ||
953 | N node = (N)this; | ||
954 | N first = null; | ||
955 | N firstParent = null; | ||
956 | N last = null; | ||
957 | N lastParent = null; | ||
958 | N firstPivot = null; | ||
959 | N lastPivot = null; | ||
960 | while (!node.isLeaf()) { | ||
961 | boolean advanceFirst = !node.isRed && firstPivot != null; | ||
962 | boolean advanceLast = !node.isRed && lastPivot != null; | ||
963 | if ((depth + 1 < path.length && path[depth + 1] == node.left) || depth + 1 == path.length) { | ||
964 | // Left move | ||
965 | if (lastPivot == null) { | ||
966 | // The post-split tree is empty | ||
967 | last = node.right; | ||
968 | last.parent = null; | ||
969 | if (last.isRed) { | ||
970 | last.isRed = false; | ||
971 | lastParent = last; | ||
972 | last = last.left; | ||
973 | } | ||
974 | } else { | ||
975 | // Concatenate node.right and the post-split tree | ||
976 | if (node.right.isRed) { | ||
977 | node.right.isRed = false; | ||
978 | } else if (!node.isRed) { | ||
979 | lastParent = last; | ||
980 | last = last.left; | ||
981 | if (last.isRed) { | ||
982 | lastParent = last; | ||
983 | last = last.left; | ||
984 | } | ||
985 | advanceLast = false; | ||
986 | } | ||
987 | lastPivot.isRed = true; | ||
988 | lastPivot.parent = lastParent; | ||
989 | if (lastParent != null) { | ||
990 | lastParent.left = lastPivot; | ||
991 | } | ||
992 | lastPivot.left = node.right; | ||
993 | if (!lastPivot.left.isLeaf()) { | ||
994 | lastPivot.left.parent = lastPivot; | ||
995 | } | ||
996 | lastPivot.right = last; | ||
997 | if (!last.isLeaf()) { | ||
998 | last.parent = lastPivot; | ||
999 | } | ||
1000 | last = lastPivot.left; | ||
1001 | lastParent = lastPivot; | ||
1002 | lastPivot.fixInsertionWithoutGettingRoot(false); | ||
1003 | } | ||
1004 | lastPivot = node; | ||
1005 | node = node.left; | ||
1006 | } else { | ||
1007 | // Right move | ||
1008 | if (firstPivot == null) { | ||
1009 | // The pre-split tree is empty | ||
1010 | first = node.left; | ||
1011 | first.parent = null; | ||
1012 | if (first.isRed) { | ||
1013 | first.isRed = false; | ||
1014 | firstParent = first; | ||
1015 | first = first.right; | ||
1016 | } | ||
1017 | } else { | ||
1018 | // Concatenate the post-split tree and node.left | ||
1019 | if (node.left.isRed) { | ||
1020 | node.left.isRed = false; | ||
1021 | } else if (!node.isRed) { | ||
1022 | firstParent = first; | ||
1023 | first = first.right; | ||
1024 | if (first.isRed) { | ||
1025 | firstParent = first; | ||
1026 | first = first.right; | ||
1027 | } | ||
1028 | advanceFirst = false; | ||
1029 | } | ||
1030 | firstPivot.isRed = true; | ||
1031 | firstPivot.parent = firstParent; | ||
1032 | if (firstParent != null) { | ||
1033 | firstParent.right = firstPivot; | ||
1034 | } | ||
1035 | firstPivot.right = node.left; | ||
1036 | if (!firstPivot.right.isLeaf()) { | ||
1037 | firstPivot.right.parent = firstPivot; | ||
1038 | } | ||
1039 | firstPivot.left = first; | ||
1040 | if (!first.isLeaf()) { | ||
1041 | first.parent = firstPivot; | ||
1042 | } | ||
1043 | first = firstPivot.right; | ||
1044 | firstParent = firstPivot; | ||
1045 | firstPivot.fixInsertionWithoutGettingRoot(false); | ||
1046 | } | ||
1047 | firstPivot = node; | ||
1048 | node = node.right; | ||
1049 | } | ||
1050 | |||
1051 | depth++; | ||
1052 | |||
1053 | // Update "first" and "last" to be the nodes at the proper black height | ||
1054 | if (advanceFirst) { | ||
1055 | firstParent = first; | ||
1056 | first = first.right; | ||
1057 | if (first.isRed) { | ||
1058 | firstParent = first; | ||
1059 | first = first.right; | ||
1060 | } | ||
1061 | } | ||
1062 | if (advanceLast) { | ||
1063 | lastParent = last; | ||
1064 | last = last.left; | ||
1065 | if (last.isRed) { | ||
1066 | lastParent = last; | ||
1067 | last = last.left; | ||
1068 | } | ||
1069 | } | ||
1070 | } | ||
1071 | |||
1072 | // Add firstPivot to the pre-split tree | ||
1073 | N leaf = node; | ||
1074 | if (first == null) { | ||
1075 | first = leaf; | ||
1076 | } else { | ||
1077 | firstPivot.isRed = true; | ||
1078 | firstPivot.parent = firstParent; | ||
1079 | if (firstParent != null) { | ||
1080 | firstParent.right = firstPivot; | ||
1081 | } | ||
1082 | firstPivot.left = leaf; | ||
1083 | firstPivot.right = leaf; | ||
1084 | firstPivot.fixInsertionWithoutGettingRoot(false); | ||
1085 | for (first = firstPivot; first.parent != null; first = first.parent) { | ||
1086 | first.augment(); | ||
1087 | } | ||
1088 | first.augment(); | ||
1089 | } | ||
1090 | |||
1091 | // Add lastPivot to the post-split tree | ||
1092 | lastPivot.isRed = true; | ||
1093 | lastPivot.parent = lastParent; | ||
1094 | if (lastParent != null) { | ||
1095 | lastParent.left = lastPivot; | ||
1096 | } | ||
1097 | lastPivot.left = leaf; | ||
1098 | lastPivot.right = leaf; | ||
1099 | lastPivot.fixInsertionWithoutGettingRoot(false); | ||
1100 | for (last = lastPivot; last.parent != null; last = last.parent) { | ||
1101 | last.augment(); | ||
1102 | } | ||
1103 | last.augment(); | ||
1104 | |||
1105 | @SuppressWarnings("unchecked") | ||
1106 | N[] result = (N[])Array.newInstance(getClass(), 2); | ||
1107 | result[0] = first; | ||
1108 | result[1] = last; | ||
1109 | return result; | ||
1110 | } | ||
1111 | |||
1112 | /** | ||
1113 | * Returns the lowest common ancestor of this node and "other" - the node that is an ancestor of both and is not the | ||
1114 | * parent of a node that is an ancestor of both. Assumes that this is in the same tree as "other". Assumes that | ||
1115 | * neither "this" nor "other" is a leaf node. This method may return "this" or "other". | ||
1116 | * | ||
1117 | * Note that while it is possible to compute the lowest common ancestor in O(P) time, where P is the length of the | ||
1118 | * path from this node to "other", the "lca" method is not guaranteed to take O(P) time. If your application | ||
1119 | * requires this, then you should write your own lowest common ancestor method. | ||
1120 | */ | ||
1121 | public N lca(N other) { | ||
1122 | if (isLeaf() || other.isLeaf()) { | ||
1123 | throw new IllegalArgumentException("One of the nodes is a leaf node"); | ||
1124 | } | ||
1125 | |||
1126 | // Compute the depth of each node | ||
1127 | int depth = 0; | ||
1128 | for (N parent = this.parent; parent != null; parent = parent.parent) { | ||
1129 | depth++; | ||
1130 | } | ||
1131 | int otherDepth = 0; | ||
1132 | for (N parent = other.parent; parent != null; parent = parent.parent) { | ||
1133 | otherDepth++; | ||
1134 | } | ||
1135 | |||
1136 | // Go up to nodes of the same depth | ||
1137 | @SuppressWarnings("unchecked") | ||
1138 | N parent = (N)this; | ||
1139 | N otherParent = other; | ||
1140 | if (depth <= otherDepth) { | ||
1141 | for (int i = otherDepth; i > depth; i--) { | ||
1142 | otherParent = otherParent.parent; | ||
1143 | } | ||
1144 | } else { | ||
1145 | for (int i = depth; i > otherDepth; i--) { | ||
1146 | parent = parent.parent; | ||
1147 | } | ||
1148 | } | ||
1149 | |||
1150 | // Find the LCA | ||
1151 | while (parent != otherParent) { | ||
1152 | parent = parent.parent; | ||
1153 | otherParent = otherParent.parent; | ||
1154 | } | ||
1155 | if (parent != null) { | ||
1156 | return parent; | ||
1157 | } else { | ||
1158 | throw new IllegalArgumentException("The nodes do not belong to the same tree"); | ||
1159 | } | ||
1160 | } | ||
1161 | |||
1162 | /** | ||
1163 | * Returns an integer comparing the position of this node in the tree that contains it with that of "other". Returns | ||
1164 | * a negative number if this is earlier, a positive number if this is later, and 0 if this is at the same position. | ||
1165 | * Assumes that this is in the same tree as "other". Assumes that neither "this" nor "other" is a leaf node. | ||
1166 | * | ||
1167 | * The base class's implementation takes O(log N) time. If a RedBlackNode subclass stores a value used to order the | ||
1168 | * nodes, then it could override compareTo to compare the nodes' values, which would take O(1) time. | ||
1169 | * | ||
1170 | * Note that while it is possible to compare the positions of two nodes in O(P) time, where P is the length of the | ||
1171 | * path from this node to "other", the default implementation of compareTo is not guaranteed to take O(P) time. If | ||
1172 | * your application requires this, then you should write your own comparison method. | ||
1173 | */ | ||
1174 | @Override | ||
1175 | public int compareTo(N other) { | ||
1176 | if (isLeaf() || other.isLeaf()) { | ||
1177 | throw new IllegalArgumentException("One of the nodes is a leaf node"); | ||
1178 | } | ||
1179 | |||
1180 | // The algorithm operates as follows: compare the depth of this node to that of "other". If the depth of | ||
1181 | // "other" is greater, keep moving up from "other" until we find the ancestor at the same depth. Then, keep | ||
1182 | // moving up from "this" and from that node until we reach the lowest common ancestor. The node that arrived | ||
1183 | // from the left child of the common ancestor is earlier. The algorithm is analogous if the depth of "other" is | ||
1184 | // not greater. | ||
1185 | if (this == other) { | ||
1186 | return 0; | ||
1187 | } | ||
1188 | |||
1189 | // Compute the depth of each node | ||
1190 | int depth = 0; | ||
1191 | RedBlackNode<N> parent; | ||
1192 | for (parent = this; parent.parent != null; parent = parent.parent) { | ||
1193 | depth++; | ||
1194 | } | ||
1195 | int otherDepth = 0; | ||
1196 | N otherParent; | ||
1197 | for (otherParent = other; otherParent.parent != null; otherParent = otherParent.parent) { | ||
1198 | otherDepth++; | ||
1199 | } | ||
1200 | |||
1201 | // Go up to nodes of the same depth | ||
1202 | if (depth < otherDepth) { | ||
1203 | otherParent = other; | ||
1204 | for (int i = otherDepth - 1; i > depth; i--) { | ||
1205 | otherParent = otherParent.parent; | ||
1206 | } | ||
1207 | if (otherParent.parent != this) { | ||
1208 | otherParent = otherParent.parent; | ||
1209 | } else if (left == otherParent) { | ||
1210 | return 1; | ||
1211 | } else { | ||
1212 | return -1; | ||
1213 | } | ||
1214 | parent = this; | ||
1215 | } else if (depth > otherDepth) { | ||
1216 | parent = this; | ||
1217 | for (int i = depth - 1; i > otherDepth; i--) { | ||
1218 | parent = parent.parent; | ||
1219 | } | ||
1220 | if (parent.parent != other) { | ||
1221 | parent = parent.parent; | ||
1222 | } else if (other.left == parent) { | ||
1223 | return -1; | ||
1224 | } else { | ||
1225 | return 1; | ||
1226 | } | ||
1227 | otherParent = other; | ||
1228 | } else { | ||
1229 | parent = this; | ||
1230 | otherParent = other; | ||
1231 | } | ||
1232 | |||
1233 | // Keep going up until we reach the lowest common ancestor | ||
1234 | while (parent.parent != otherParent.parent) { | ||
1235 | parent = parent.parent; | ||
1236 | otherParent = otherParent.parent; | ||
1237 | } | ||
1238 | if (parent.parent == null) { | ||
1239 | throw new IllegalArgumentException("The nodes do not belong to the same tree"); | ||
1240 | } | ||
1241 | if (parent.parent.left == parent) { | ||
1242 | return -1; | ||
1243 | } else { | ||
1244 | return 1; | ||
1245 | } | ||
1246 | } | ||
1247 | |||
1248 | /** Throws a RuntimeException if the RedBlackNode fields of this are not correct for a leaf node. */ | ||
1249 | private void assertIsValidLeaf() { | ||
1250 | if (left != null || right != null || parent != null || isRed) { | ||
1251 | throw new RuntimeException("A leaf node's \"left\", \"right\", \"parent\", or isRed field is incorrect"); | ||
1252 | } | ||
1253 | } | ||
1254 | |||
1255 | /** | ||
1256 | * Throws a RuntimeException if the subtree rooted at this node does not satisfy the red-black properties, excluding | ||
1257 | * the requirement that the root be black, or it contains a repeated node other than a leaf node. | ||
1258 | * @param blackHeight The required number of black nodes in each path from this to a leaf node, including this and | ||
1259 | * the leaf node. | ||
1260 | * @param visited The nodes we have reached thus far, other than leaf nodes. This method adds the non-leaf nodes in | ||
1261 | * the subtree rooted at this node to "visited". | ||
1262 | */ | ||
1263 | private void assertSubtreeIsValidRedBlack(int blackHeight, Set<Reference<N>> visited) { | ||
1264 | @SuppressWarnings("unchecked") | ||
1265 | N nThis = (N)this; | ||
1266 | if (left == null || right == null) { | ||
1267 | assertIsValidLeaf(); | ||
1268 | if (blackHeight != 1) { | ||
1269 | throw new RuntimeException("Not all root-to-leaf paths have the same number of black nodes"); | ||
1270 | } | ||
1271 | return; | ||
1272 | } else if (!visited.add(new Reference<N>(nThis))) { | ||
1273 | throw new RuntimeException("The tree contains a repeated non-leaf node"); | ||
1274 | } else { | ||
1275 | int childBlackHeight; | ||
1276 | if (isRed) { | ||
1277 | if ((!left.isLeaf() && left.isRed) || (!right.isLeaf() && right.isRed)) { | ||
1278 | throw new RuntimeException("A red node has a red child"); | ||
1279 | } | ||
1280 | childBlackHeight = blackHeight; | ||
1281 | } else if (blackHeight == 0) { | ||
1282 | throw new RuntimeException("Not all root-to-leaf paths have the same number of black nodes"); | ||
1283 | } else { | ||
1284 | childBlackHeight = blackHeight - 1; | ||
1285 | } | ||
1286 | |||
1287 | if (!left.isLeaf() && left.parent != this) { | ||
1288 | throw new RuntimeException("left.parent != this"); | ||
1289 | } | ||
1290 | if (!right.isLeaf() && right.parent != this) { | ||
1291 | throw new RuntimeException("right.parent != this"); | ||
1292 | } | ||
1293 | RedBlackNode<N> leftNode = left; | ||
1294 | RedBlackNode<N> rightNode = right; | ||
1295 | leftNode.assertSubtreeIsValidRedBlack(childBlackHeight, visited); | ||
1296 | rightNode.assertSubtreeIsValidRedBlack(childBlackHeight, visited); | ||
1297 | } | ||
1298 | } | ||
1299 | |||
1300 | /** Calls assertNodeIsValid() on every node in the subtree rooted at this node. */ | ||
1301 | private void assertNodesAreValid() { | ||
1302 | assertNodeIsValid(); | ||
1303 | if (left != null) { | ||
1304 | RedBlackNode<N> leftNode = left; | ||
1305 | RedBlackNode<N> rightNode = right; | ||
1306 | leftNode.assertNodesAreValid(); | ||
1307 | rightNode.assertNodesAreValid(); | ||
1308 | } | ||
1309 | } | ||
1310 | |||
1311 | /** | ||
1312 | * Throws a RuntimeException if the subtree rooted at this node is not a valid red-black tree, e.g. if a red node | ||
1313 | * has a red child or it contains a non-leaf node "node" for which node.left.parent != node. (If parent != null, | ||
1314 | * it's okay if isRed is true.) This method is useful for debugging. See also assertSubtreeIsValid(). | ||
1315 | */ | ||
1316 | public void assertSubtreeIsValidRedBlack() { | ||
1317 | if (isLeaf()) { | ||
1318 | assertIsValidLeaf(); | ||
1319 | } else { | ||
1320 | if (parent == null && isRed) { | ||
1321 | throw new RuntimeException("The root is red"); | ||
1322 | } | ||
1323 | |||
1324 | // Compute the black height of the tree | ||
1325 | Set<Reference<N>> nodes = new HashSet<Reference<N>>(); | ||
1326 | int blackHeight = 0; | ||
1327 | @SuppressWarnings("unchecked") | ||
1328 | N node = (N)this; | ||
1329 | while (node != null) { | ||
1330 | if (!nodes.add(new Reference<N>(node))) { | ||
1331 | throw new RuntimeException("The tree contains a repeated non-leaf node"); | ||
1332 | } | ||
1333 | if (!node.isRed) { | ||
1334 | blackHeight++; | ||
1335 | } | ||
1336 | node = node.left; | ||
1337 | } | ||
1338 | |||
1339 | assertSubtreeIsValidRedBlack(blackHeight, new HashSet<Reference<N>>()); | ||
1340 | } | ||
1341 | } | ||
1342 | |||
1343 | /** | ||
1344 | * Throws a RuntimeException if we detect a problem with the subtree rooted at this node, such as a red child of a | ||
1345 | * red node or a non-leaf descendant "node" for which node.left.parent != node. This method is useful for | ||
1346 | * debugging. RedBlackNode subclasses may want to override assertSubtreeIsValid() to call assertOrderIsValid. | ||
1347 | */ | ||
1348 | public void assertSubtreeIsValid() { | ||
1349 | assertSubtreeIsValidRedBlack(); | ||
1350 | assertNodesAreValid(); | ||
1351 | } | ||
1352 | |||
1353 | /** | ||
1354 | * Throws a RuntimeException if the nodes in the subtree rooted at this node are not in the specified order or they | ||
1355 | * do not lie in the specified range. Assumes that the subtree rooted at this node is a valid binary tree, i.e. it | ||
1356 | * has no repeated nodes other than leaf nodes. | ||
1357 | * @param comparator A comparator indicating how the nodes should be ordered. | ||
1358 | * @param start The lower limit for nodes in the subtree, if any. | ||
1359 | * @param end The upper limit for nodes in the subtree, if any. | ||
1360 | */ | ||
1361 | private void assertOrderIsValid(Comparator<? super N> comparator, N start, N end) { | ||
1362 | if (!isLeaf()) { | ||
1363 | @SuppressWarnings("unchecked") | ||
1364 | N nThis = (N)this; | ||
1365 | if (start != null && comparator.compare(nThis, start) < 0) { | ||
1366 | throw new RuntimeException("The nodes are not ordered correctly"); | ||
1367 | } | ||
1368 | if (end != null && comparator.compare(nThis, end) > 0) { | ||
1369 | throw new RuntimeException("The nodes are not ordered correctly"); | ||
1370 | } | ||
1371 | RedBlackNode<N> leftNode = left; | ||
1372 | RedBlackNode<N> rightNode = right; | ||
1373 | leftNode.assertOrderIsValid(comparator, start, nThis); | ||
1374 | rightNode.assertOrderIsValid(comparator, nThis, end); | ||
1375 | } | ||
1376 | } | ||
1377 | |||
1378 | /** | ||
1379 | * Throws a RuntimeException if the nodes in the subtree rooted at this node are not in the specified order. | ||
1380 | * Assumes that this is a valid binary tree, i.e. there are no repeated nodes other than leaf nodes. This method is | ||
1381 | * useful for debugging. RedBlackNode subclasses may want to override assertSubtreeIsValid() to call | ||
1382 | * assertOrderIsValid. | ||
1383 | * @param comparator A comparator indicating how the nodes should be ordered. If this is null, we use the nodes' | ||
1384 | * natural order, as in N.compareTo. | ||
1385 | */ | ||
1386 | public void assertOrderIsValid(Comparator<? super N> comparator) { | ||
1387 | if (comparator == null) { | ||
1388 | comparator = naturalOrder(); | ||
1389 | } | ||
1390 | assertOrderIsValid(comparator, null, null); | ||
1391 | } | ||
1392 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Reference.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Reference.java new file mode 100644 index 00000000..a25c167d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Reference.java | |||
@@ -0,0 +1,51 @@ | |||
1 | /* | ||
2 | * The MIT License (MIT) | ||
3 | * | ||
4 | * Copyright (c) 2016 btrekkie | ||
5 | * | ||
6 | * Permission is hereby granted, free of charge, to any person obtaining a copy | ||
7 | * of this software and associated documentation files (the "Software"), to deal | ||
8 | * in the Software without restriction, including without limitation the rights | ||
9 | * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell | ||
10 | * copies of the Software, and to permit persons to whom the Software is | ||
11 | * furnished to do so, subject to the following conditions: | ||
12 | * | ||
13 | * The above copyright notice and this permission notice shall be included in all | ||
14 | * copies or substantial portions of the Software. | ||
15 | * | ||
16 | * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR | ||
17 | * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, | ||
18 | * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE | ||
19 | * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER | ||
20 | * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, | ||
21 | * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE | ||
22 | * SOFTWARE. | ||
23 | */ | ||
24 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval; | ||
25 | |||
26 | /** | ||
27 | * Wraps a value using reference equality. In other words, two references are equal only if their values are the same | ||
28 | * object instance, as in ==. | ||
29 | * @param <T> The type of value. | ||
30 | */ | ||
31 | class Reference<T> { | ||
32 | /** The value this wraps. */ | ||
33 | private final T value; | ||
34 | |||
35 | public Reference(T value) { | ||
36 | this.value = value; | ||
37 | } | ||
38 | |||
39 | public boolean equals(Object obj) { | ||
40 | if (!(obj instanceof Reference)) { | ||
41 | return false; | ||
42 | } | ||
43 | Reference<?> reference = (Reference<?>)obj; | ||
44 | return value == reference.value; | ||
45 | } | ||
46 | |||
47 | @Override | ||
48 | public int hashCode() { | ||
49 | return System.identityHashCode(value); | ||
50 | } | ||
51 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/aggregators/IntervalAggregatorFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/aggregators/IntervalAggregatorFactory.xtend new file mode 100644 index 00000000..2b6059da --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/aggregators/IntervalAggregatorFactory.xtend | |||
@@ -0,0 +1,50 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.IntervalAggregationMode | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.IntervalAggregationOperator | ||
6 | import org.eclipse.viatra.query.runtime.matchers.psystem.aggregations.AggregatorType | ||
7 | import org.eclipse.viatra.query.runtime.matchers.psystem.aggregations.BoundAggregator | ||
8 | import org.eclipse.viatra.query.runtime.matchers.psystem.aggregations.IAggregatorFactory | ||
9 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
10 | |||
11 | @AggregatorType(parameterTypes = #[Interval], returnTypes = #[Interval]) | ||
12 | abstract class IntervalAggregatorFactory implements IAggregatorFactory { | ||
13 | val IntervalAggregationMode mode | ||
14 | |||
15 | @FinalFieldsConstructor | ||
16 | protected new() { | ||
17 | } | ||
18 | |||
19 | override getAggregatorLogic(Class<?> domainClass) { | ||
20 | if (domainClass == Interval) { | ||
21 | new BoundAggregator(new IntervalAggregationOperator(mode), Interval, Interval) | ||
22 | } else { | ||
23 | throw new IllegalArgumentException("Unknown domain class: " + domainClass) | ||
24 | } | ||
25 | } | ||
26 | } | ||
27 | |||
28 | class intervalSum extends IntervalAggregatorFactory { | ||
29 | new() { | ||
30 | super(IntervalAggregationMode.SUM) | ||
31 | } | ||
32 | } | ||
33 | |||
34 | class intervalMin extends IntervalAggregatorFactory { | ||
35 | new() { | ||
36 | super(IntervalAggregationMode.MIN) | ||
37 | } | ||
38 | } | ||
39 | |||
40 | class intervalMax extends IntervalAggregatorFactory { | ||
41 | new() { | ||
42 | super(IntervalAggregationMode.MAX) | ||
43 | } | ||
44 | } | ||
45 | |||
46 | class intervalJoin extends IntervalAggregatorFactory { | ||
47 | new() { | ||
48 | super(IntervalAggregationMode.JOIN) | ||
49 | } | ||
50 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index d4c76bb4..24b3e870 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend | |||
@@ -55,7 +55,7 @@ class PatternGenerator { | |||
55 | typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis | 55 | typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis |
56 | } | 56 | } |
57 | 57 | ||
58 | public dispatch def referRelation( | 58 | public dispatch def CharSequence referRelation( |
59 | RelationDeclaration referred, | 59 | RelationDeclaration referred, |
60 | String sourceVariable, | 60 | String sourceVariable, |
61 | String targetVariable, | 61 | String targetVariable, |
@@ -64,7 +64,7 @@ class PatternGenerator { | |||
64 | { | 64 | { |
65 | return this.relationDeclarationIndexer.referRelation(referred,sourceVariable,targetVariable,modality) | 65 | return this.relationDeclarationIndexer.referRelation(referred,sourceVariable,targetVariable,modality) |
66 | } | 66 | } |
67 | public dispatch def referRelation( | 67 | public dispatch def CharSequence referRelation( |
68 | RelationDefinition referred, | 68 | RelationDefinition referred, |
69 | String sourceVariable, | 69 | String sourceVariable, |
70 | String targetVariable, | 70 | String targetVariable, |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index 0e13a5e1..e87f52af 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend | |||
@@ -2,8 +2,10 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | |||
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult |
@@ -11,7 +13,9 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | |||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
13 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 15 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
16 | import java.util.Collection | ||
14 | import java.util.Map | 17 | import java.util.Map |
18 | import java.util.Set | ||
15 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 19 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
16 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 20 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
17 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 21 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
@@ -19,8 +23,6 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | |||
19 | import org.eclipse.xtend.lib.annotations.Data | 23 | import org.eclipse.xtend.lib.annotations.Data |
20 | 24 | ||
21 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 25 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
22 | import java.util.Collection | ||
23 | import java.util.Set | ||
24 | 26 | ||
25 | @Data class GeneratedPatterns { | 27 | @Data class GeneratedPatterns { |
26 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries | 28 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries |
@@ -29,9 +31,16 @@ import java.util.Set | |||
29 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries | 31 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries |
30 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries | 32 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries |
31 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries | 33 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries |
34 | public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries | ||
32 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries | 35 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries |
33 | } | 36 | } |
34 | 37 | ||
38 | @Data class ModalPatternQueries { | ||
39 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayQuery | ||
40 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustQuery | ||
41 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentQuery | ||
42 | } | ||
43 | |||
35 | class PatternProvider { | 44 | class PatternProvider { |
36 | 45 | ||
37 | val TypeAnalysis typeAnalysis = new TypeAnalysis | 46 | val TypeAnalysis typeAnalysis = new TypeAnalysis |
@@ -71,7 +80,7 @@ class PatternProvider { | |||
71 | LogicProblem problem, | 80 | LogicProblem problem, |
72 | PartialInterpretation emptySolution, | 81 | PartialInterpretation emptySolution, |
73 | TypeAnalysisResult typeAnalysisResult, | 82 | TypeAnalysisResult typeAnalysisResult, |
74 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries | 83 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries |
75 | ) { | 84 | ) { |
76 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 85 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
77 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] | 86 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] |
@@ -85,6 +94,14 @@ class PatternProvider { | |||
85 | refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 94 | refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] |
86 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 95 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
87 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] | 96 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] |
97 | val Map<RelationDefinition, ModalPatternQueries> modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | | ||
98 | val indexer = patternGenerator.relationDefinitionIndexer | ||
99 | new ModalPatternQueries( | ||
100 | indexer.relationDefinitionName(relationDefinition, Modality.MAY).lookup(queries), | ||
101 | indexer.relationDefinitionName(relationDefinition, Modality.MUST).lookup(queries), | ||
102 | indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries) | ||
103 | ) | ||
104 | ]) | ||
88 | return new GeneratedPatterns( | 105 | return new GeneratedPatterns( |
89 | invalidWFQueries, | 106 | invalidWFQueries, |
90 | unfinishedWFQueries, | 107 | unfinishedWFQueries, |
@@ -92,6 +109,7 @@ class PatternProvider { | |||
92 | refineObjectsQueries, | 109 | refineObjectsQueries, |
93 | refineTypeQueries, | 110 | refineTypeQueries, |
94 | refineRelationQueries, | 111 | refineRelationQueries, |
112 | modalRelationQueries, | ||
95 | queries.values | 113 | queries.values |
96 | ) | 114 | ) |
97 | } | 115 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend index 9723373f..cedcec5a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend | |||
@@ -71,7 +71,7 @@ class RelationDefinitionIndexer { | |||
71 | ] | 71 | ] |
72 | } | 72 | } |
73 | 73 | ||
74 | private def relationDefinitionName(RelationDefinition relation, Modality modality) | 74 | def String relationDefinitionName(RelationDefinition relation, Modality modality) |
75 | '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' | 75 | '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' |
76 | 76 | ||
77 | private def canonizeName(PVariable v) { | 77 | private def canonizeName(PVariable v) { |