Refactor constraints, conversion strategies, and print

src/main/java/de/vill/conversion/ConvertFeatureCardinality.java

@@ -1,10 +1,9 @@
 package de.vill.conversion;
 
 import de.vill.model.*;
-import de.vill.model.constraint.Constraint;
-import de.vill.model.constraint.ImplicationConstraint;
-import de.vill.model.constraint.LiteralConstraint;
-import de.vill.model.constraint.ParenthesisConstraint;
+import de.vill.model.constraint.*;
+import de.vill.model.expression.Expression;
+import de.vill.model.expression.LiteralExpression;
 
 import java.util.*;
 
@@ -52,6 +51,7 @@ private void removeFeatureCardinality(Feature feature, FeatureModel featureModel
 
         for (int i = min; i <= max; i++) {
             Feature newChild = new Feature(feature.getFeatureName() + "-" + i);
+            featureModel.getFeatureMap().put(newChild.getFeatureName(), newChild);
             newChild.getAttributes().put("abstract", new Attribute<Boolean>("abstract", true, feature));
             newChildren.getFeatures().add(newChild);
             newChild.setParentGroup(newChildren);
@@ -62,7 +62,9 @@ private void removeFeatureCardinality(Feature feature, FeatureModel featureModel
             }
             for (int j = 1; j <= i; j++) {
                 Feature subTreeClone = feature.clone();
-                addPrefixToNamesRecursively(subTreeClone, "-" + i + "-" + j);
+                subTreeClone.getAttributes().clear();
+                subTreeClone.getAttributes().put("abstract", new Attribute<Boolean>("abstract", true, subTreeClone));
+                addPrefixToNamesRecursively(subTreeClone, "-" + i + "-" + j, featureModel);
                 mandatoryGroup.getFeatures().add(subTreeClone);
                 subTreeClone.setParentGroup(mandatoryGroup);
 
@@ -71,22 +73,77 @@ private void removeFeatureCardinality(Feature feature, FeatureModel featureModel
                 constraintReplacementMap.remove(feature.getFeatureName());
                 for (Constraint constraint : constraintsToClone) {
                     Constraint newConstraint = constraint.clone();
+                    if (newConstraint instanceof LiteralConstraint) {
+                        String toReplace = ((LiteralConstraint) newConstraint).getReference().getIdentifier();
+                        if (constraintReplacementMap.containsKey(toReplace)) {
+                            LiteralConstraint newLiteral = new LiteralConstraint(constraintReplacementMap.get(toReplace));
+                            LiteralConstraint subTreeRootConstraint = new LiteralConstraint(newChild);
+                            newConstraint = new ImplicationConstraint(subTreeRootConstraint, new ParenthesisConstraint(newLiteral));
+                        }
+                    } else {
+                        adaptConstraint(subTreeClone, newConstraint, constraintReplacementMap);
+                        LiteralConstraint subTreeRootConstraint = new LiteralConstraint(newChild);
+                        newConstraint = new ImplicationConstraint(subTreeRootConstraint, new ParenthesisConstraint(newConstraint));
+                    }
                     featureModel.getOwnConstraints().add(newConstraint);
-                    adaptConstraint(subTreeClone, newConstraint, constraintReplacementMap);
                 }
             }
         }
+/*
+additional constraint with all cloned versions ored
+        Set<String> allFeatureNamesInSubTree = new HashSet<>();
+        getAllSubFeatureNamesRecursively(feature, allFeatureNamesInSubTree);
+        for (Constraint constraint : constraintsToClone) {
+            Constraint newConstraint = constraint.clone();
+            orAdaptedConstraint(newConstraint, allFeatureNamesInSubTree, min, max, featureModel);
+            featureModel.getOwnConstraints().add(newConstraint);
+        }
+
+ */
+
+
         feature.getChildren().removeAll(feature.getChildren());
         feature.getChildren().add(newChildren);
         newChildren.setParentFeature(feature);
     }
 
-    private void addPrefixToNamesRecursively(Feature feature, String prefix) {
+    private void orAdaptedConstraint(Constraint constraint, Set<String> featuresToReplace, int min, int max, FeatureModel featureModel) {
+        for (Constraint subPart : constraint.getConstraintSubParts()) {
+            if (subPart instanceof LiteralConstraint) {
+                String toReplace = ((LiteralConstraint) subPart).getReference().getIdentifier();
+                if (featuresToReplace.contains(toReplace)) {
+                    Feature f = featureModel.getFeatureMap().get(toReplace + "-" + (min == 0 ? 1 : min) + "-1");
+                    Constraint newOr = new LiteralConstraint(f);
+                    for (int i = min + 1; i <= max; i++) {
+                        for (int j = 1; j <= i; j++) {
+                            newOr = new OrConstraint(newOr, new LiteralConstraint(featureModel.getFeatureMap().get(toReplace + "-" + i + "-" + j)));
+                        }
+                    }
+                    constraint.replaceConstraintSubPart(subPart, new ParenthesisConstraint(newOr));
+                }
+            } else {
+                orAdaptedConstraint(subPart, featuresToReplace, min, max, featureModel);
+            }
+        }
+    }
+
+    private void getAllSubFeatureNamesRecursively(Feature feature, Set<String> names) {
+        names.add(feature.getFeatureName());
+        for (Group child : feature.getChildren()) {
+            for (Feature childFeature : child.getFeatures()) {
+                getAllSubFeatureNamesRecursively(childFeature, names);
+            }
+        }
+    }
+
+    private void addPrefixToNamesRecursively(Feature feature, String prefix, FeatureModel featureModel) {
         feature.setFeatureName(feature.getFeatureName() + prefix);
+        var attributes = feature.getAttributes();
+        featureModel.getFeatureMap().put(feature.getFeatureName(), feature);
         if (!feature.isSubmodelRoot()) {
             for (Group group : feature.getChildren()) {
                 for (Feature subFeature : group.getFeatures()) {
-                    addPrefixToNamesRecursively(subFeature, prefix);
+                    addPrefixToNamesRecursively(subFeature, prefix, featureModel);
                 }
             }
         }
@@ -118,14 +175,46 @@ private List<Feature> getFeatureFromSubTree(Group group) {
 
     private boolean constraintContains(Constraint constraint, List<Feature> subTreeFeatures) {
         List<Constraint> subParts = constraint.getConstraintSubParts();
+        if (constraint instanceof LiteralConstraint && ((LiteralConstraint) constraint).getReference() instanceof Feature) {
+            Feature feature = (Feature) ((LiteralConstraint) constraint).getReference();
+            if (subTreeFeatures.contains(feature)) {
+                return true;
+            }
+        } else if (constraint instanceof ExpressionConstraint) {
+            Expression left = ((ExpressionConstraint) constraint).getLeft();
+            Expression right = ((ExpressionConstraint) constraint).getRight();
+            return expressionContains(left, subTreeFeatures) || expressionContains(right, subTreeFeatures);
+        }
+
         for (Constraint subPart : subParts) {
             if (subPart instanceof LiteralConstraint && ((LiteralConstraint) subPart).getReference() instanceof Feature) {
                 Feature feature = (Feature) ((LiteralConstraint) subPart).getReference();
                 if (subTreeFeatures.contains(feature)) {
                     return true;
                 }
-            } else {
-                constraintContains(subPart, subTreeFeatures);
+            } else if (constraintContains(subPart, subTreeFeatures)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    private boolean expressionContains(Expression expression, List<Feature> subTreeFeatures) {
+        if (expression instanceof LiteralExpression) {
+            Feature feature = (Feature) ((Attribute<?>) ((LiteralExpression) expression).getContent()).getFeature();
+            if (subTreeFeatures.contains(feature)) {
+                return true;
+            }
+        }
+
+        for (Expression subExpression : expression.getExpressionSubParts()) {
+            if (expression instanceof LiteralExpression) {
+                Feature feature = (Feature) ((LiteralExpression) expression).getContent();
+                if (subTreeFeatures.contains(feature)) {
+                    return true;
+                }
+            } else if (expressionContains(subExpression, subTreeFeatures)) {
+                return true;
             }
         }
         return false;
@@ -144,17 +233,38 @@ private void createFeatureReplacementMap(Feature oldSubTree, Feature newSubTree,
     }
 
     private void adaptConstraint(Feature subTreeRoot, Constraint constraint, Map<String, Feature> featureReplacementMap) {
-        List<Constraint> subParts = constraint.getConstraintSubParts();
-        for (Constraint subPart : subParts) {
-            if (subPart instanceof LiteralConstraint) {
-                String toReplace = ((LiteralConstraint) subPart).getReference().getIdentifier();
-                if (featureReplacementMap.containsKey(toReplace)) {
-                    LiteralConstraint subTreeRootConstraint = new LiteralConstraint(subTreeRoot);
-                    LiteralConstraint newLiteral = new LiteralConstraint(featureReplacementMap.get(toReplace));
-                    constraint.replaceConstraintSubPart(subPart, new ParenthesisConstraint(new ImplicationConstraint(subTreeRootConstraint, newLiteral)));
+        if (constraint instanceof ExpressionConstraint) {
+            adaptExpression(((ExpressionConstraint) constraint).getLeft(), featureReplacementMap);
+            adaptExpression(((ExpressionConstraint) constraint).getRight(), featureReplacementMap);
+        } else {
+            List<Constraint> subParts = constraint.getConstraintSubParts();
+            for (Constraint subPart : subParts) {
+                if (subPart instanceof LiteralConstraint) {
+                    String toReplace = ((LiteralConstraint) subPart).getReference().getIdentifier();
+                    if (featureReplacementMap.containsKey(toReplace)) {
+                        LiteralConstraint newLiteral = new LiteralConstraint(featureReplacementMap.get(toReplace));
+                        constraint.replaceConstraintSubPart(subPart, newLiteral);
+                    }
+                } else {
+                    adaptConstraint(subTreeRoot, subPart, featureReplacementMap);
                 }
-            } else {
-                adaptConstraint(subTreeRoot, subPart, featureReplacementMap);
+            }
+        }
+    }
+
+    private void adaptExpression(Expression expression, Map<String, Feature> featureReplacementMap) {
+        if (expression instanceof LiteralExpression) {
+            LiteralExpression literalExpression = (LiteralExpression) expression;
+            Attribute<?> attribute = (Attribute<?>) literalExpression.getContent();
+            if (featureReplacementMap.containsKey(attribute.getFeature().getFeatureName())) {
+                var newAttribute = attribute.clone();
+                newAttribute.setFeature(featureReplacementMap.get(attribute.getFeature().getFeatureName()));
+                literalExpression.setContent(newAttribute);
+            }
+
+        } else {
+            for (Expression subExpression : expression.getExpressionSubParts()) {
+                adaptExpression(subExpression, featureReplacementMap);
             }
         }
     }

src/main/java/de/vill/conversion/ConvertGroupCardinality.java

@@ -47,7 +47,7 @@ private void removeGroupCardinality(Group group, FeatureModel featureModel) {
         Set<Feature> groupMembers = new HashSet<>(group.getFeatures());
 
         int lowerBound = group.getCardinality().lower;
-        int upperBound = Math.max(group.getCardinality().upper, groupMembers.size());
+        int upperBound = Math.min(group.getCardinality().upper, groupMembers.size());
         Set<Set<Feature>> featureCombinations = new HashSet<>();
         for (int i = lowerBound; i <= upperBound; i++) {
             featureCombinations.addAll(Sets.combinations(groupMembers, i));
@@ -81,6 +81,11 @@ private Constraint createConjunction(Set<Feature> selectedFeatures, Set<Feature>
     }
 
     private Constraint createDisjunction(Set<Constraint> constraints) {
+        MultiOrConstraint orConstraint = new MultiOrConstraint();
+        for (Constraint constraint : constraints) {
+            orConstraint.add_sub_part(constraint);
+        }
+        /*
         Constraint orConstraint;
         if (constraints.size() == 1) {
             Constraint constraint = constraints.iterator().next();
@@ -92,6 +97,8 @@ private Constraint createDisjunction(Set<Constraint> constraints) {
             orConstraint = new OrConstraint(constraint, createDisjunction(constraints));
         }
 
+         */
+
         return orConstraint;
     }
 }

src/main/java/de/vill/conversion/ConvertSMTLevel.java

@@ -19,33 +19,53 @@ public Set<LanguageLevel> getTargetLevelsOfConversion() {
         return new HashSet<>(Arrays.asList(LanguageLevel.BOOLEAN_LEVEL));
     }
 
+    private Constraint getFalseConstraint(FeatureModel featureModel){
+        return new NotConstraint(new LiteralConstraint(featureModel.getRootFeature()));
+    }
+
     @Override
     public void convertFeatureModel(FeatureModel rootFeatureModel, FeatureModel featureModel) {
         List<Constraint> constraints = featureModel.getFeatureConstraints();
         constraints.addAll(featureModel.getOwnConstraints());
-        constraints.stream().forEach(this::replaceEquationInConstraint);
+        for(Constraint constraint : constraints) {
+            replaceEquationInConstraint(constraint, featureModel);
+        }
         List<Constraint> replacements = new LinkedList<>();
         for (Constraint constraint : featureModel.getOwnConstraints()) {
             if (constraint instanceof ExpressionConstraint) {
-                Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) constraint);
+                Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) constraint, getFalseConstraint(featureModel));
                 replacements.add(equationReplacement);
             }
         }
         featureModel.getOwnConstraints().removeIf(x -> x instanceof ExpressionConstraint);
         featureModel.getOwnConstraints().addAll(replacements);
-        traverseFeatures(featureModel.getRootFeature());
+        for (Constraint constraint : featureModel.getOwnConstraints()) {
+            convertConstraint(constraint, featureModel);
+        }
+        traverseFeatures(featureModel.getRootFeature(), featureModel);
     }
 
-    private void replaceEquationInConstraint(Constraint constraint) {
+    private void convertConstraint(Constraint constraint, FeatureModel featureModel) {
         for (Constraint subConstraint : constraint.getConstraintSubParts()) {
             if (subConstraint instanceof ExpressionConstraint) {
-                Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) subConstraint);
+                Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) subConstraint, getFalseConstraint(featureModel));
                 constraint.replaceConstraintSubPart(subConstraint, equationReplacement);
+            }else{
+                convertConstraint(subConstraint, featureModel);
             }
         }
     }
 
-    private Constraint convertEquationToConstraint(ExpressionConstraint equation) {
+    private void replaceEquationInConstraint(Constraint constraint, FeatureModel featureModel) {
+        for (Constraint subConstraint : constraint.getConstraintSubParts()) {
+            if (subConstraint instanceof ExpressionConstraint) {
+                Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) subConstraint, getFalseConstraint(featureModel));
+                constraint.replaceConstraintSubPart(subConstraint, equationReplacement);
+            }
+        }
+    }
+
+    private Constraint convertEquationToConstraint(ExpressionConstraint equation, Constraint falseConstraint) {
         Set<Feature> featuresInEquation = getFeaturesInEquation(equation);
         Set<Set<Feature>> featureCombinations = getFeatureCombinations(featuresInEquation);
         Set<Constraint> disjunction = new HashSet<>();
@@ -55,7 +75,11 @@ private Constraint convertEquationToConstraint(ExpressionConstraint equation) {
                 disjunction.add(createConjunction(configuration, new HashSet<>(featuresInEquation)));
             }
         }
-        return new ParenthesisConstraint(createDisjunction(disjunction));
+        if (disjunction.isEmpty()) {
+            return falseConstraint;
+        }else{
+            return new ParenthesisConstraint(createDisjunction(disjunction));
+        }
     }
 
     private Set<Feature> getFeaturesInEquation(ExpressionConstraint equation) {
@@ -112,6 +136,11 @@ private Constraint createConjunction(Set<Feature> selectedFeatures, Set<Feature>
     }
 
     private Constraint createDisjunction(Set<Constraint> constraints) {
+        MultiOrConstraint orConstraint = new MultiOrConstraint();
+        for (Constraint constraint : constraints) {
+            orConstraint.add_sub_part(constraint);
+        }
+        /*
         Constraint orConstraint;
         if (constraints.size() == 1) {
             Constraint constraint = constraints.iterator().next();
@@ -123,23 +152,25 @@ private Constraint createDisjunction(Set<Constraint> constraints) {
             orConstraint = new OrConstraint(constraint, createDisjunction(constraints));
         }
 
+         */
+
         return orConstraint;
     }
 
-    private void removeEquationFromAttributes(Feature feature) {
+    private void removeEquationFromAttributes(Feature feature, FeatureModel featureModel) {
         Attribute<?> attributeConstraint = feature.getAttributes().get("constraint");
         Attribute<?> attributeConstraintList = feature.getAttributes().get("constraints");
         if (attributeConstraint != null) {
             if (attributeConstraint.getValue() instanceof ExpressionConstraint) {
-                Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) attributeConstraint.getValue());
+                Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) attributeConstraint.getValue(), getFalseConstraint(featureModel));
                 feature.getAttributes().put("constraint", new Attribute<>("constraint", equationReplacement, feature));
             }
         }
         if (attributeConstraintList != null && attributeConstraintList.getValue() instanceof List<?>) {
             List<Object> newConstraintList = new LinkedList<>();
             for (Object constraint : (List<?>) attributeConstraintList.getValue()) {
                 if (constraint instanceof ExpressionConstraint) {
-                    Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) constraint);
+                    Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) constraint, getFalseConstraint(featureModel));
                     newConstraintList.add(equationReplacement);
                 } else {
                     newConstraintList.add(constraint);
@@ -149,11 +180,11 @@ private void removeEquationFromAttributes(Feature feature) {
         }
     }
 
-    private void traverseFeatures(Feature feature) {
-        removeEquationFromAttributes(feature);
+    private void traverseFeatures(Feature feature, FeatureModel featureModel) {
+        removeEquationFromAttributes(feature, featureModel);
         for (Group group : feature.getChildren()) {
             for (Feature subFeature : group.getFeatures()) {
-                traverseFeatures(subFeature);
+                traverseFeatures(subFeature, featureModel);
             }
         }
     }