diff options
author | 2021-09-20 15:53:22 +0200 | |
---|---|---|
committer | 2021-09-20 15:53:22 +0200 | |
commit | a0269e55eb5c1b136b3ae306985ca0d979ff9420 (patch) | |
tree | 7a24de449e8dfdb656267a9f1c92151cbe907fb5 /model-data | |
parent | Import fix (diff) | |
download | refinery-a0269e55eb5c1b136b3ae306985ca0d979ff9420.tar.gz refinery-a0269e55eb5c1b136b3ae306985ca0d979ff9420.tar.zst refinery-a0269e55eb5c1b136b3ae306985ca0d979ff9420.zip |
Data structure for predicate representation
Diffstat (limited to 'model-data')
8 files changed, 417 insertions, 0 deletions
diff --git a/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFAnd.java b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFAnd.java new file mode 100644 index 00000000..ff5a7848 --- /dev/null +++ b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFAnd.java | |||
@@ -0,0 +1,37 @@ | |||
1 | package org.eclipse.viatra.solver.data.query.building; | ||
2 | |||
3 | import java.util.HashMap; | ||
4 | import java.util.HashSet; | ||
5 | import java.util.List; | ||
6 | import java.util.Map; | ||
7 | import java.util.Set; | ||
8 | |||
9 | public class DNFAnd { | ||
10 | private Set<Variable> existentiallyQuantified; | ||
11 | private List<DNFAtom> constraints; | ||
12 | public DNFAnd(Set<Variable> quantifiedVariables, List<DNFAtom> constraints) { | ||
13 | super(); | ||
14 | this.existentiallyQuantified = quantifiedVariables; | ||
15 | this.constraints = constraints; | ||
16 | } | ||
17 | public Set<Variable> getExistentiallyQuantified() { | ||
18 | return existentiallyQuantified; | ||
19 | } | ||
20 | public List<DNFAtom> getConstraints() { | ||
21 | return constraints; | ||
22 | } | ||
23 | void unifyVariables(Map<String,Variable> uniqueVariableMap) { | ||
24 | Map<String,Variable> uniqueVariableMapForClause = new HashMap<>(uniqueVariableMap); | ||
25 | for(DNFAtom atom : constraints) { | ||
26 | atom.unifyVariables(uniqueVariableMapForClause); | ||
27 | } | ||
28 | } | ||
29 | void collectQuantifiedVariables(Set<Variable> parameters) { | ||
30 | Set<Variable> result = new HashSet<>(); | ||
31 | for(DNFAtom constraint : constraints) { | ||
32 | constraint.collectAllVariables(result); | ||
33 | } | ||
34 | result.removeAll(parameters); | ||
35 | existentiallyQuantified = result; | ||
36 | } | ||
37 | } | ||
diff --git a/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFAtom.java b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFAtom.java new file mode 100644 index 00000000..05a3e3f8 --- /dev/null +++ b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFAtom.java | |||
@@ -0,0 +1,33 @@ | |||
1 | package org.eclipse.viatra.solver.data.query.building; | ||
2 | |||
3 | import java.util.Collection; | ||
4 | import java.util.Iterator; | ||
5 | import java.util.Map; | ||
6 | import java.util.Set; | ||
7 | |||
8 | public interface DNFAtom { | ||
9 | void unifyVariables(Map<String,Variable> variables); | ||
10 | static Variable unifyVariables(Map<String,Variable> unifiedVariables, Variable variable) { | ||
11 | if(variable != null) { | ||
12 | if(variable.isNamed() && unifiedVariables.containsKey(variable.getName())) { | ||
13 | return unifiedVariables.get(variable.getName()); | ||
14 | } | ||
15 | return variable; | ||
16 | } else { | ||
17 | return null; | ||
18 | } | ||
19 | } | ||
20 | void collectAllVariables(Set<Variable> variables); | ||
21 | static void addToCollection(Set<Variable> variables, Variable variable) { | ||
22 | if(variable != null) { | ||
23 | variables.add(variable); | ||
24 | } | ||
25 | } | ||
26 | static void addToCollection(Set<Variable> variables, Collection<Variable> variableCollection) { | ||
27 | Iterator<Variable> iterator = variableCollection.iterator(); | ||
28 | while(iterator.hasNext()) { | ||
29 | Variable variable = iterator.next(); | ||
30 | addToCollection(variables, variable); | ||
31 | } | ||
32 | } | ||
33 | } | ||
diff --git a/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFPredicate.java b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFPredicate.java new file mode 100644 index 00000000..8ee540ae --- /dev/null +++ b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFPredicate.java | |||
@@ -0,0 +1,72 @@ | |||
1 | package org.eclipse.viatra.solver.data.query.building; | ||
2 | |||
3 | import java.util.HashMap; | ||
4 | import java.util.HashSet; | ||
5 | import java.util.List; | ||
6 | import java.util.Map; | ||
7 | import java.util.UUID; | ||
8 | |||
9 | public class DNFPredicate { | ||
10 | private final String name; | ||
11 | private final String uniqueName; | ||
12 | private final List<Variable> parameters; | ||
13 | private final List<DNFAnd> clauses; | ||
14 | |||
15 | public DNFPredicate(String name, List<Variable> parameters, List<DNFAnd> clauses) { | ||
16 | this.name = name; | ||
17 | this.uniqueName = generateUniqueName(name,"predicate"); | ||
18 | this.parameters = parameters; | ||
19 | this.clauses = clauses; | ||
20 | |||
21 | postProcess(); | ||
22 | } | ||
23 | |||
24 | public static String generateUniqueName(String originalName, String defaultPrefix) { | ||
25 | UUID uuid = UUID.randomUUID(); | ||
26 | String uniqueString = uuid.toString().replace('-', '_'); | ||
27 | if(originalName == null) { | ||
28 | return defaultPrefix+uniqueString; | ||
29 | } else { | ||
30 | return originalName+uniqueString; | ||
31 | } | ||
32 | } | ||
33 | |||
34 | public String getName() { | ||
35 | return name; | ||
36 | } | ||
37 | public String getUniqueName() { | ||
38 | return uniqueName; | ||
39 | } | ||
40 | public List<Variable> getVariables() { | ||
41 | return parameters; | ||
42 | } | ||
43 | public List<DNFAnd> getClauses() { | ||
44 | return clauses; | ||
45 | } | ||
46 | |||
47 | public void unifyVariables() { | ||
48 | Map<String,Variable> uniqueVariableMap = new HashMap<>(); | ||
49 | for(Variable parameter : this.parameters) { | ||
50 | if(parameter.isNamed()) { | ||
51 | String parameterName = parameter.getName(); | ||
52 | if(uniqueVariableMap.containsKey(parameterName)) { | ||
53 | throw new IllegalArgumentException("Multiple parameters has the name "+parameterName); | ||
54 | } else { | ||
55 | uniqueVariableMap.put(parameterName, parameter); | ||
56 | } | ||
57 | } | ||
58 | } | ||
59 | for(DNFAnd clause : this.clauses) { | ||
60 | clause.unifyVariables(uniqueVariableMap); | ||
61 | } | ||
62 | } | ||
63 | public void collectQuantifiedVariables() { | ||
64 | for(DNFAnd clause : this.clauses) { | ||
65 | clause.collectQuantifiedVariables(new HashSet<>(parameters)); | ||
66 | } | ||
67 | } | ||
68 | public void postProcess() { | ||
69 | unifyVariables(); | ||
70 | collectQuantifiedVariables(); | ||
71 | } | ||
72 | } | ||
diff --git a/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/EquivalenceAtom.java b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/EquivalenceAtom.java new file mode 100644 index 00000000..b47fe2a8 --- /dev/null +++ b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/EquivalenceAtom.java | |||
@@ -0,0 +1,44 @@ | |||
1 | package org.eclipse.viatra.solver.data.query.building; | ||
2 | |||
3 | import java.util.Map; | ||
4 | import java.util.Set; | ||
5 | |||
6 | public class EquivalenceAtom implements DNFAtom{ | ||
7 | private boolean positive; | ||
8 | private Variable left; | ||
9 | private Variable right; | ||
10 | public EquivalenceAtom(boolean positive, Variable left, Variable right) { | ||
11 | this.positive = positive; | ||
12 | this.left = left; | ||
13 | this.right = right; | ||
14 | } | ||
15 | public boolean isPositive() { | ||
16 | return positive; | ||
17 | } | ||
18 | public void setPositive(boolean positive) { | ||
19 | this.positive = positive; | ||
20 | } | ||
21 | public Variable getLeft() { | ||
22 | return left; | ||
23 | } | ||
24 | public void setLeft(Variable left) { | ||
25 | this.left = left; | ||
26 | } | ||
27 | public Variable getRight() { | ||
28 | return right; | ||
29 | } | ||
30 | public void setRight(Variable right) { | ||
31 | this.right = right; | ||
32 | } | ||
33 | |||
34 | @Override | ||
35 | public void unifyVariables(Map<String, Variable> variables) { | ||
36 | this.left = DNFAtom.unifyVariables(variables,left); | ||
37 | this.right = DNFAtom.unifyVariables(variables,right); | ||
38 | } | ||
39 | @Override | ||
40 | public void collectAllVariables(Set<Variable> variables) { | ||
41 | DNFAtom.addToCollection(variables, left); | ||
42 | DNFAtom.addToCollection(variables, right); | ||
43 | } | ||
44 | } | ||
diff --git a/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/PredicateAtom.java b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/PredicateAtom.java new file mode 100644 index 00000000..3e5ef88e --- /dev/null +++ b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/PredicateAtom.java | |||
@@ -0,0 +1,57 @@ | |||
1 | package org.eclipse.viatra.solver.data.query.building; | ||
2 | |||
3 | import java.util.List; | ||
4 | import java.util.Map; | ||
5 | import java.util.Set; | ||
6 | |||
7 | public class PredicateAtom implements DNFAtom{ | ||
8 | private DNFPredicate referred; | ||
9 | private List<Variable> substitution; | ||
10 | private boolean positive; | ||
11 | private boolean transitive; | ||
12 | |||
13 | public PredicateAtom(boolean positive, boolean transitive, DNFPredicate referred, List<Variable> substitution) { | ||
14 | this.positive = positive; | ||
15 | this.referred = referred; | ||
16 | this.substitution = substitution; | ||
17 | this.transitive = transitive; | ||
18 | } | ||
19 | public DNFPredicate getReferred() { | ||
20 | return referred; | ||
21 | } | ||
22 | public void setReferred(DNFPredicate referred) { | ||
23 | this.referred = referred; | ||
24 | } | ||
25 | public List<Variable> getSubstitution() { | ||
26 | return substitution; | ||
27 | } | ||
28 | public void setSubstitution(List<Variable> substitution) { | ||
29 | this.substitution = substitution; | ||
30 | } | ||
31 | public boolean isPositive() { | ||
32 | return positive; | ||
33 | } | ||
34 | public void setPositive(boolean positive) { | ||
35 | this.positive = positive; | ||
36 | } | ||
37 | public boolean isTransitive() { | ||
38 | return transitive; | ||
39 | } | ||
40 | public void setTransitive(boolean transitive) { | ||
41 | this.transitive = transitive; | ||
42 | } | ||
43 | @Override | ||
44 | public void unifyVariables(Map<String, Variable> variables) { | ||
45 | for(int i = 0; i<this.substitution.size(); i++) { | ||
46 | final Object term = this.substitution.get(i); | ||
47 | if(term instanceof Variable) { | ||
48 | Variable variableReference = (Variable) term; | ||
49 | this.substitution.set(i, DNFAtom.unifyVariables(variables, variableReference)); | ||
50 | } | ||
51 | } | ||
52 | } | ||
53 | @Override | ||
54 | public void collectAllVariables(Set<Variable> variables) { | ||
55 | DNFAtom.addToCollection(variables, substitution); | ||
56 | } | ||
57 | } | ||
diff --git a/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/PredicateBuilder_string.java b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/PredicateBuilder_string.java new file mode 100644 index 00000000..41f85d39 --- /dev/null +++ b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/PredicateBuilder_string.java | |||
@@ -0,0 +1,107 @@ | |||
1 | package org.eclipse.viatra.solver.data.query.building; | ||
2 | |||
3 | import java.util.ArrayList; | ||
4 | import java.util.Collections; | ||
5 | import java.util.HashSet; | ||
6 | import java.util.List; | ||
7 | |||
8 | import org.eclipse.viatra.solver.data.query.view.RelationView; | ||
9 | |||
10 | public class PredicateBuilder_string { | ||
11 | private PredicateBuilder_string() {} | ||
12 | |||
13 | public static PredicateBuild1 predicate(String name) { | ||
14 | return new PredicateBuild1(name); | ||
15 | } | ||
16 | public static class PredicateBuild1 { | ||
17 | private String name; | ||
18 | public PredicateBuild1(String name) { | ||
19 | this.name = name; | ||
20 | } | ||
21 | public PredicateBuild2 parameters(String... parameters) { | ||
22 | return new PredicateBuild2(name, parameters); | ||
23 | } | ||
24 | } | ||
25 | public static class PredicateBuild2 { | ||
26 | private String name; | ||
27 | private String[] parameters; | ||
28 | public PredicateBuild2(String name, String[] parameters) { | ||
29 | this.name = name; | ||
30 | this.parameters = parameters; | ||
31 | } | ||
32 | |||
33 | public PredicateBuild3 clause(DNFAtom...constraints) { | ||
34 | return new PredicateBuild3(name,parameters,List.<DNFAtom[]>of(constraints)); | ||
35 | } | ||
36 | } | ||
37 | public static class PredicateBuild3 { | ||
38 | String name; | ||
39 | String[] parameters; | ||
40 | List<DNFAtom[]> clauses; | ||
41 | public PredicateBuild3(String name, String[] parameters, List<DNFAtom[]> clauses) { | ||
42 | super(); | ||
43 | this.name = name; | ||
44 | this.parameters = parameters; | ||
45 | this.clauses = clauses; | ||
46 | } | ||
47 | |||
48 | public PredicateBuild3 clause(DNFAtom...constraints) { | ||
49 | List<DNFAtom[]> newClauses = new ArrayList<>(); | ||
50 | newClauses.addAll(clauses); | ||
51 | newClauses.add(constraints); | ||
52 | return new PredicateBuild3(name, parameters, newClauses); | ||
53 | } | ||
54 | public DNFPredicate build() { | ||
55 | List<Variable> newParameters = new ArrayList<>(this.parameters.length); | ||
56 | for(int i = 0; i<this.parameters.length; i++) { | ||
57 | newParameters.add(new Variable(parameters[i])); | ||
58 | } | ||
59 | |||
60 | List<DNFAnd> newClauses = new ArrayList<>(this.clauses.size()); | ||
61 | for(DNFAtom[] clause : this.clauses) { | ||
62 | List<DNFAtom> constraints = new ArrayList<>(clause.length); | ||
63 | Collections.addAll(constraints, clause); | ||
64 | newClauses.add(new DNFAnd(new HashSet<>(), constraints)); | ||
65 | } | ||
66 | |||
67 | return new DNFPredicate(name,newParameters,newClauses); | ||
68 | } | ||
69 | } | ||
70 | |||
71 | private static Variable stringToVariable(String name) { | ||
72 | if(name != null) { | ||
73 | return new Variable(name); | ||
74 | } else { | ||
75 | return null; | ||
76 | } | ||
77 | } | ||
78 | private static List<Variable> stringToVariable(String[] names) { | ||
79 | List<Variable> variables = new ArrayList<>(); | ||
80 | for(int i = 0; i<names.length; i++) { | ||
81 | variables.add(stringToVariable(names[i])); | ||
82 | } | ||
83 | return variables; | ||
84 | } | ||
85 | |||
86 | public static EquivalenceAtom cEquals(String v1, String v2) { | ||
87 | return new EquivalenceAtom(true,stringToVariable(v1),stringToVariable(v2)); | ||
88 | } | ||
89 | public static EquivalenceAtom cNotEquals(String v1, String v2) { | ||
90 | return new EquivalenceAtom(false,stringToVariable(v1),stringToVariable(v2)); | ||
91 | } | ||
92 | |||
93 | public static RelationAtom cInRelation(RelationView<?> view, String... variables) { | ||
94 | |||
95 | return new RelationAtom(view, stringToVariable(variables)); | ||
96 | } | ||
97 | |||
98 | public static PredicateAtom cInPredicate(DNFPredicate referred, String... variables) { | ||
99 | return new PredicateAtom(true, false, referred, stringToVariable(variables)); | ||
100 | } | ||
101 | public static PredicateAtom cInTransitivePredicate(DNFPredicate referred, String... variables) { | ||
102 | return new PredicateAtom(true, true, referred, stringToVariable(variables)); | ||
103 | } | ||
104 | public static PredicateAtom cNotInPredicate(DNFPredicate referred, String... variables) { | ||
105 | return new PredicateAtom(false, false, referred, stringToVariable(variables)); | ||
106 | } | ||
107 | } | ||
diff --git a/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/RelationAtom.java b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/RelationAtom.java new file mode 100644 index 00000000..f7152bba --- /dev/null +++ b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/RelationAtom.java | |||
@@ -0,0 +1,45 @@ | |||
1 | package org.eclipse.viatra.solver.data.query.building; | ||
2 | |||
3 | import java.util.List; | ||
4 | import java.util.Map; | ||
5 | import java.util.Set; | ||
6 | |||
7 | import org.eclipse.viatra.solver.data.query.view.FilteredRelationView; | ||
8 | import org.eclipse.viatra.solver.data.query.view.RelationView; | ||
9 | |||
10 | public class RelationAtom implements DNFAtom{ | ||
11 | RelationView<?> view; | ||
12 | List<Variable> substitution; | ||
13 | |||
14 | public RelationAtom(RelationView<?> view, List<Variable> substitution) { | ||
15 | this.view = view; | ||
16 | this.substitution = substitution; | ||
17 | } | ||
18 | public RelationView<?> getView() { | ||
19 | return view; | ||
20 | } | ||
21 | public void setView(FilteredRelationView<?> view) { | ||
22 | this.view = view; | ||
23 | } | ||
24 | public List<Variable> getSubstitution() { | ||
25 | return substitution; | ||
26 | } | ||
27 | public void setSubstitution(List<Variable> substitution) { | ||
28 | this.substitution = substitution; | ||
29 | } | ||
30 | |||
31 | @Override | ||
32 | public void unifyVariables(Map<String, Variable> variables) { | ||
33 | for(int i = 0; i<this.substitution.size(); i++) { | ||
34 | final Object term = this.substitution.get(i); | ||
35 | if(term instanceof Variable) { | ||
36 | Variable variableReference = (Variable) term; | ||
37 | this.substitution.set(i, DNFAtom.unifyVariables(variables, variableReference)); | ||
38 | } | ||
39 | } | ||
40 | } | ||
41 | @Override | ||
42 | public void collectAllVariables(Set<Variable> variables) { | ||
43 | DNFAtom.addToCollection(variables, substitution); | ||
44 | } | ||
45 | } | ||
diff --git a/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/Variable.java b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/Variable.java new file mode 100644 index 00000000..29f9fc8b --- /dev/null +++ b/model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/Variable.java | |||
@@ -0,0 +1,22 @@ | |||
1 | package org.eclipse.viatra.solver.data.query.building; | ||
2 | |||
3 | public class Variable { | ||
4 | private final String name; | ||
5 | private final String uniqueName; | ||
6 | |||
7 | public Variable(String name) { | ||
8 | super(); | ||
9 | this.name = name; | ||
10 | this.uniqueName = DNFPredicate.generateUniqueName(name, "variable"); | ||
11 | |||
12 | } | ||
13 | public String getName() { | ||
14 | return name; | ||
15 | } | ||
16 | public String getUniqueName() { | ||
17 | return uniqueName; | ||
18 | } | ||
19 | public boolean isNamed() { | ||
20 | return name != null; | ||
21 | } | ||
22 | } | ||