From a0269e55eb5c1b136b3ae306985ca0d979ff9420 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Mon, 20 Sep 2021 15:53:22 +0200 Subject: Data structure for predicate representation --- .../viatra/solver/data/query/building/DNFAnd.java | 37 +++++++ .../viatra/solver/data/query/building/DNFAtom.java | 33 +++++++ .../solver/data/query/building/DNFPredicate.java | 72 ++++++++++++++ .../data/query/building/EquivalenceAtom.java | 44 +++++++++ .../solver/data/query/building/PredicateAtom.java | 57 +++++++++++ .../query/building/PredicateBuilder_string.java | 107 +++++++++++++++++++++ .../solver/data/query/building/RelationAtom.java | 45 +++++++++ .../solver/data/query/building/Variable.java | 22 +++++ 8 files changed, 417 insertions(+) create mode 100644 model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFAnd.java create mode 100644 model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFAtom.java create mode 100644 model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/DNFPredicate.java create mode 100644 model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/EquivalenceAtom.java create mode 100644 model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/PredicateAtom.java create mode 100644 model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/PredicateBuilder_string.java create mode 100644 model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/RelationAtom.java create mode 100644 model-data/src/main/java/org/eclipse/viatra/solver/data/query/building/Variable.java 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 existentiallyQuantified; + private List constraints; + public DNFAnd(Set quantifiedVariables, List constraints) { + super(); + this.existentiallyQuantified = quantifiedVariables; + this.constraints = constraints; + } + public Set getExistentiallyQuantified() { + return existentiallyQuantified; + } + public List getConstraints() { + return constraints; + } + void unifyVariables(Map uniqueVariableMap) { + Map uniqueVariableMapForClause = new HashMap<>(uniqueVariableMap); + for(DNFAtom atom : constraints) { + atom.unifyVariables(uniqueVariableMapForClause); + } + } + void collectQuantifiedVariables(Set parameters) { + Set 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 variables); + static Variable unifyVariables(Map 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 variables); + static void addToCollection(Set variables, Variable variable) { + if(variable != null) { + variables.add(variable); + } + } + static void addToCollection(Set variables, Collection variableCollection) { + Iterator 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 parameters; + private final List clauses; + + public DNFPredicate(String name, List parameters, List 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 getVariables() { + return parameters; + } + public List getClauses() { + return clauses; + } + + public void unifyVariables() { + Map 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 variables) { + this.left = DNFAtom.unifyVariables(variables,left); + this.right = DNFAtom.unifyVariables(variables,right); + } + @Override + public void collectAllVariables(Set 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 substitution; + private boolean positive; + private boolean transitive; + + public PredicateAtom(boolean positive, boolean transitive, DNFPredicate referred, List 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 getSubstitution() { + return substitution; + } + public void setSubstitution(List 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 variables) { + for(int i = 0; i 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.of(constraints)); + } + } + public static class PredicateBuild3 { + String name; + String[] parameters; + List clauses; + public PredicateBuild3(String name, String[] parameters, List clauses) { + super(); + this.name = name; + this.parameters = parameters; + this.clauses = clauses; + } + + public PredicateBuild3 clause(DNFAtom...constraints) { + List newClauses = new ArrayList<>(); + newClauses.addAll(clauses); + newClauses.add(constraints); + return new PredicateBuild3(name, parameters, newClauses); + } + public DNFPredicate build() { + List newParameters = new ArrayList<>(this.parameters.length); + for(int i = 0; i newClauses = new ArrayList<>(this.clauses.size()); + for(DNFAtom[] clause : this.clauses) { + List 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 stringToVariable(String[] names) { + List variables = new ArrayList<>(); + for(int i = 0; i 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 substitution; + + public RelationAtom(RelationView view, List substitution) { + this.view = view; + this.substitution = substitution; + } + public RelationView getView() { + return view; + } + public void setView(FilteredRelationView view) { + this.view = view; + } + public List getSubstitution() { + return substitution; + } + public void setSubstitution(List substitution) { + this.substitution = substitution; + } + + @Override + public void unifyVariables(Map variables) { + for(int i = 0; i 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; + } +} -- cgit v1.2.3-70-g09d2