Merge remote-tracking branch 'origin/web-demo'web-demo

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 @@
+package org.eclipse.viatra.solver.data.query.building;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+public class DNFAnd {
+        private Set<Variable> existentiallyQuantified;
+        private List<DNFAtom> constraints;
+        public DNFAnd(Set<Variable> quantifiedVariables, List<DNFAtom> constraints) {
+                super();
+                this.existentiallyQuantified = quantifiedVariables;
+                this.constraints = constraints;
+        }
+        public Set<Variable> getExistentiallyQuantified() {
+                return existentiallyQuantified;
+        }
+        public List<DNFAtom> getConstraints() {
+                return constraints;
+        }
+        void unifyVariables(Map<String,Variable> uniqueVariableMap) {
+                Map<String,Variable> uniqueVariableMapForClause = new HashMap<>(uniqueVariableMap);
+                for(DNFAtom atom : constraints) {
+                        atom.unifyVariables(uniqueVariableMapForClause);
+                }
+        }
+        void collectQuantifiedVariables(Set<Variable> parameters) {
+                Set<Variable> result = new HashSet<>();
+                for(DNFAtom constraint : constraints) {
+                        constraint.collectAllVariables(result);
+                }
+                result.removeAll(parameters);
+                existentiallyQuantified = result;
+        }
+}
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 @@
+package org.eclipse.viatra.solver.data.query.building;
+
+import java.util.Collection;
+import java.util.Iterator;
+import java.util.Map;
+import java.util.Set;
+
+public interface DNFAtom {
+        void unifyVariables(Map<String,Variable> variables);
+        static Variable unifyVariables(Map<String,Variable> unifiedVariables, Variable variable) {
+                if(variable != null) {
+                        if(variable.isNamed() && unifiedVariables.containsKey(variable.getName())) {
+                                return unifiedVariables.get(variable.getName());
+                        }
+                        return variable;
+                } else {
+                        return null;
+                }
+        }
+        void collectAllVariables(Set<Variable> variables);
+        static void addToCollection(Set<Variable> variables, Variable variable) {
+                if(variable != null) {
+                        variables.add(variable);
+                }
+        }
+        static void addToCollection(Set<Variable> variables, Collection<Variable> variableCollection) {
+                Iterator<Variable> iterator = variableCollection.iterator();
+                while(iterator.hasNext()) {
+                        Variable variable = iterator.next();
+                        addToCollection(variables, variable);
+                }
+        }
+}
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 @@
+package org.eclipse.viatra.solver.data.query.building;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.UUID;
+
+public class DNFPredicate {
+        private final String name;
+        private final String uniqueName;
+        private final List<Variable> parameters;
+        private final List<DNFAnd> clauses;
+        
+        public DNFPredicate(String name, List<Variable> parameters, List<DNFAnd> clauses) {
+                this.name = name;
+                this.uniqueName = generateUniqueName(name,"predicate");
+                this.parameters = parameters;
+                this.clauses = clauses;
+                
+                postProcess();
+        }
+        
+        public static String generateUniqueName(String originalName, String defaultPrefix) {
+                UUID uuid = UUID.randomUUID();
+                String uniqueString = uuid.toString().replace('-', '_');
+                if(originalName == null) {
+                        return defaultPrefix+uniqueString;
+                } else {
+                        return originalName+uniqueString;
+                }
+        }
+        
+        public String getName() {
+                return name;
+        }
+        public String getUniqueName() {
+                return uniqueName;
+        }
+        public List<Variable> getVariables() {
+                return parameters;
+        }
+        public List<DNFAnd> getClauses() {
+                return clauses;
+        }
+        
+        public void unifyVariables() {
+                Map<String,Variable> uniqueVariableMap = new HashMap<>();
+                for(Variable parameter : this.parameters) {
+                        if(parameter.isNamed()) {
+                                String parameterName = parameter.getName();
+                                if(uniqueVariableMap.containsKey(parameterName)) {
+                                        throw new IllegalArgumentException("Multiple parameters has the name "+parameterName);
+                                } else {
+                                        uniqueVariableMap.put(parameterName, parameter);
+                                }
+                        }
+                }
+                for(DNFAnd clause : this.clauses) {
+                        clause.unifyVariables(uniqueVariableMap);
+                }
+        }
+        public void collectQuantifiedVariables() {
+                for(DNFAnd clause : this.clauses) {
+                        clause.collectQuantifiedVariables(new HashSet<>(parameters));
+                }
+        }
+        public void postProcess() {
+                unifyVariables();
+                collectQuantifiedVariables();
+        }
+}
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 @@
+package org.eclipse.viatra.solver.data.query.building;
+
+import java.util.Map;
+import java.util.Set;
+
+public class EquivalenceAtom implements DNFAtom{
+        private boolean positive;
+        private Variable left;
+        private Variable right;
+        public EquivalenceAtom(boolean positive, Variable left, Variable right) {
+                this.positive = positive;
+                this.left = left;
+                this.right = right;
+        }
+        public boolean isPositive() {
+                return positive;
+        }
+        public void setPositive(boolean positive) {
+                this.positive = positive;
+        }
+        public Variable getLeft() {
+                return left;
+        }
+        public void setLeft(Variable left) {
+                this.left = left;
+        }
+        public Variable getRight() {
+                return right;
+        }
+        public void setRight(Variable right) {
+                this.right = right;
+        }
+        
+        @Override
+        public void unifyVariables(Map<String, Variable> variables) {
+                this.left = DNFAtom.unifyVariables(variables,left);
+                this.right = DNFAtom.unifyVariables(variables,right);
+        }
+        @Override
+        public void collectAllVariables(Set<Variable> variables) {
+                DNFAtom.addToCollection(variables, left);
+                DNFAtom.addToCollection(variables, right);
+        }
+}
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 @@
+package org.eclipse.viatra.solver.data.query.building;
+
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+public class PredicateAtom implements DNFAtom{
+        private DNFPredicate referred;
+        private List<Variable> substitution;
+        private boolean positive;
+        private boolean transitive;
+        
+        public PredicateAtom(boolean positive, boolean transitive, DNFPredicate referred, List<Variable> substitution) {
+                this.positive = positive;
+                this.referred = referred;
+                this.substitution = substitution;
+                this.transitive = transitive;
+        }
+        public DNFPredicate getReferred() {
+                return referred;
+        }
+        public void setReferred(DNFPredicate referred) {
+                this.referred = referred;
+        }
+        public List<Variable> getSubstitution() {
+                return substitution;
+        }
+        public void setSubstitution(List<Variable> substitution) {
+                this.substitution = substitution;
+        }
+        public boolean isPositive() {
+                return positive;
+        }
+        public void setPositive(boolean positive) {
+                this.positive = positive;
+        }
+        public boolean isTransitive() {
+                return transitive;
+        }
+        public void setTransitive(boolean transitive) {
+                this.transitive = transitive;
+        }
+        @Override
+        public void unifyVariables(Map<String, Variable> variables) {
+                for(int i = 0; i<this.substitution.size(); i++) {
+                        final Object term = this.substitution.get(i);
+                        if(term instanceof Variable) {
+                                Variable variableReference = (Variable) term;
+                                this.substitution.set(i, DNFAtom.unifyVariables(variables, variableReference));
+                        }
+                }
+        }
+        @Override
+        public void collectAllVariables(Set<Variable> variables) {
+                DNFAtom.addToCollection(variables, substitution);
+        }
+}
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 @@
+package org.eclipse.viatra.solver.data.query.building;
+
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.List;
+
+import org.eclipse.viatra.solver.data.query.view.RelationView;
+
+public class PredicateBuilder_string {
+        private PredicateBuilder_string() {}
+        
+        public static PredicateBuild1 predicate(String name) {
+                return new PredicateBuild1(name);
+        }
+        public static class PredicateBuild1 {
+                private String name;
+                public PredicateBuild1(String name) {
+                        this.name = name;
+                }
+                public PredicateBuild2 parameters(String... parameters) {
+                        return new PredicateBuild2(name, parameters);
+                }
+        }
+        public static class PredicateBuild2 {
+                private String name;
+                private String[] parameters;
+                public PredicateBuild2(String name, String[] parameters) {
+                        this.name = name;
+                        this.parameters = parameters;
+                }
+                
+                public PredicateBuild3 clause(DNFAtom...constraints) {
+                        return new PredicateBuild3(name,parameters,List.<DNFAtom[]>of(constraints));
+                }
+        }
+        public static class PredicateBuild3 {
+                String name;
+                String[] parameters;
+                List<DNFAtom[]> clauses;
+                public PredicateBuild3(String name, String[] parameters, List<DNFAtom[]> clauses) {
+                        super();
+                        this.name = name;
+                        this.parameters = parameters;
+                        this.clauses = clauses;
+                }
+                
+                public PredicateBuild3 clause(DNFAtom...constraints) {
+                        List<DNFAtom[]> newClauses = new ArrayList<>();
+                        newClauses.addAll(clauses);
+                        newClauses.add(constraints);
+                        return new PredicateBuild3(name, parameters, newClauses);
+                }
+                public DNFPredicate build() {
+                        List<Variable> newParameters = new ArrayList<>(this.parameters.length);
+                        for(int i = 0; i<this.parameters.length; i++) {
+                                newParameters.add(new Variable(parameters[i]));
+                        }
+                        
+                        List<DNFAnd> newClauses = new ArrayList<>(this.clauses.size());
+                        for(DNFAtom[] clause : this.clauses) {
+                                List<DNFAtom> constraints = new ArrayList<>(clause.length);
+                                Collections.addAll(constraints, clause);
+                                newClauses.add(new DNFAnd(new HashSet<>(), constraints));
+                        }
+                        
+                        return new DNFPredicate(name,newParameters,newClauses);
+                }
+        }
+        
+        private static Variable stringToVariable(String name) {
+                if(name != null) {
+                        return new Variable(name);
+                } else {
+                        return null;
+                }
+        }
+        private static List<Variable> stringToVariable(String[] names) {
+                List<Variable> variables = new ArrayList<>();
+                for(int i = 0; i<names.length; i++) {
+                        variables.add(stringToVariable(names[i]));
+                }
+                return variables;
+        }
+        
+        public static EquivalenceAtom cEquals(String v1, String v2) {
+                return new EquivalenceAtom(true,stringToVariable(v1),stringToVariable(v2));
+        }
+        public static EquivalenceAtom cNotEquals(String v1, String v2) {
+                return new EquivalenceAtom(false,stringToVariable(v1),stringToVariable(v2));
+        }
+        
+        public static RelationAtom cInRelation(RelationView<?> view, String... variables) {
+                
+                return new RelationAtom(view, stringToVariable(variables));
+        }
+        
+        public static PredicateAtom cInPredicate(DNFPredicate referred, String... variables) {
+                return new PredicateAtom(true, false, referred, stringToVariable(variables));
+        }
+        public static PredicateAtom cInTransitivePredicate(DNFPredicate referred, String... variables) {
+                return new PredicateAtom(true, true, referred, stringToVariable(variables));
+        }
+        public static PredicateAtom cNotInPredicate(DNFPredicate referred, String... variables) {
+                return new PredicateAtom(false, false, referred, stringToVariable(variables));
+        }
+}
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 @@
+package org.eclipse.viatra.solver.data.query.building;
+
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import org.eclipse.viatra.solver.data.query.view.FilteredRelationView;
+import org.eclipse.viatra.solver.data.query.view.RelationView;
+
+public class RelationAtom implements DNFAtom{
+        RelationView<?> view;
+        List<Variable> substitution;
+        
+        public RelationAtom(RelationView<?> view, List<Variable> substitution) {
+                this.view = view;
+                this.substitution = substitution;
+        }
+        public RelationView<?> getView() {
+                return view;
+        }
+        public void setView(FilteredRelationView<?> view) {
+                this.view = view;
+        }
+        public List<Variable> getSubstitution() {
+                return substitution;
+        }
+        public void setSubstitution(List<Variable> substitution) {
+                this.substitution = substitution;
+        }
+        
+        @Override
+        public void unifyVariables(Map<String, Variable> variables) {
+                for(int i = 0; i<this.substitution.size(); i++) {
+                        final Object term = this.substitution.get(i);
+                        if(term instanceof Variable) {
+                                Variable variableReference = (Variable) term;
+                                this.substitution.set(i, DNFAtom.unifyVariables(variables, variableReference));
+                        }
+                }
+        }
+        @Override
+        public void collectAllVariables(Set<Variable> variables) {
+                DNFAtom.addToCollection(variables, substitution);
+        }
+}
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 @@
+package org.eclipse.viatra.solver.data.query.building;
+
+public class Variable {
+        private final String name;
+        private final String uniqueName;
+
+        public Variable(String name) {
+                super();
+                this.name = name;
+                this.uniqueName = DNFPredicate.generateUniqueName(name, "variable");
+                
+        }
+        public String getName() {
+                return name;
+        }
+        public String getUniqueName() {
+                return uniqueName;
+        }
+        public boolean isNamed() {
+                return name != null;
+        }
+}