Skip to content

Commit 7a02ec0

Browse files
SundermannCst-vi
SundermannC
and
st-vi
authored
refactor: updates to constraints, conversion strategies, and print (#18)
* feat: print the feature model without cross tree constraints as pseudo-boolean constraints in .opb format * feat: worked on pseudo boolean encoding * feat: added constraint to pbc translation * fix: constraint pbc encoding * fix: fixed wrong constraint encoding * fix: fixed wrong constraint encoding * fix: error in group cardinality conversion and multi or for larger possible group cardinality conversions * feat: printing fm to z3 input format * feat: uvl to opb and dimacs pipeline * fix: only include satisfying assignments for an ExpressionsConstraint during conversion strategy * fix: also include feature constraints for pseudo-boolean encoding * feat: pseudo boolean encoding of feature attribute constraints without division * feat: pseudo boolean encoding of feature attribute constraints with division * feat: pseudo boolean encoding of feature attribute constraints that contain doubles by encoding them in integer values * refactor: renaming * fix: check for division by 0 in smt conversion * fix: check for division by 0 in smt conversion * fix: simplify and fix multiplication of number and literal (before handled as literal times literal) * fix: wrong factor sign after denominator removal * fix: error during biimplicatino transformation * fix: fixed pseudo boolean encoding of division (now directly like all other mathematical operators) * multiple changes * feat: automated evaluation * fix: wrong opb encoding for group cardinality * fix: opb encoding for double negated literals * feat: eval pipeline * fix: error in feature cardinality conversion strategy * feat: encode feature cardinality in pseudo-boolean * feat: encode aggregate functions and string constraints in pseudo-boolean * fix: remove multi or in feature cardinality conversion * fix: biimplication of literal and pb constraint (because former assumption that constraint is always >= does not hold for random uvl expressions) * fix: conversion strategy for feature attribute constraints only searches for expressions as direct constraints but not as expressions that are part of a normal constraint * feat: changed or-group pseudo-boolean encoding to are more concise one (old one was not wrong) * feat: removed unnecessary IO from dimacs encoding * fix: fixed and refactored pbc encoding * fix: fixed pbc encoding for single negated literal constraints * fix: simplified and fixed opb encoding * refactor: simplified PBConstraint * refactor: default value for literal sign * refactor: escape every feature name with " to avoid errors with solver (e.g. for - in name) * refactor: escape every feature name with " to avoid errors with solver (e.g. for - in name) * fix: feature cardinality conversion strategy (set right constraint replacement, like described in UVL BA) * fix: several bugs and added new semantic for constraints containing cloned features * fix: attribute cloning, remove unnecessary attributes for cloned feature cardinality subtree roots, expression contains feature from feature cardinality, unsatisfiable expression should return false and not throw error, several issues with opb division encoding, removed unnecessary overwrites of left and right in expression constraints, force order of featurecardinality and aggregate function conversion, several to string methods for better debugging, issues with whole number encoding because numbers get larger than long value, uniform substitution, simpler substitution code, * feat: added support for distributive cross-tree constraint encoding (vs tseitin style cross-tree constraint encoding) * feat: added support for distributive opb encoding * fix: set quotes for feature name "false" * refactor: moved all pseudo-boolean related code into another project * fix: use multior in smt conversion to prevent stack overflow * fix: drop typelevel conversion also considers constraints with type related concepts * Delete .idea/.gitignore * Delete .idea directory * refactor: removed unnecessary files * refactor: applied code auto-formatting * refactor: changed back to maven dependencies * Added automatic bracket creation when printing UVL models * Added unit tests for brackets; small fix * Several changes to simplify changing identifiers programatically with the fm builder * Resolved issues following merge * misc: updated changes according to Kevin's review --------- Co-authored-by: Stefan <svill33@gmail.com> Co-authored-by: Stefan <76208574+st-vi@users.noreply.github.com>
1 parent 660f453 commit 7a02ec0

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

44 files changed

+718
-180
lines changed

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

Lines changed: 88 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,9 @@
11
package de.vill.conversion;
22

33
import de.vill.model.*;
4-
import de.vill.model.constraint.Constraint;
5-
import de.vill.model.constraint.ImplicationConstraint;
6-
import de.vill.model.constraint.LiteralConstraint;
7-
import de.vill.model.constraint.ParenthesisConstraint;
4+
import de.vill.model.constraint.*;
5+
import de.vill.model.expression.Expression;
6+
import de.vill.model.expression.LiteralExpression;
87

98
import java.util.*;
109

@@ -52,6 +51,7 @@ private void removeFeatureCardinality(Feature feature, FeatureModel featureModel
5251

5352
for (int i = min; i <= max; i++) {
5453
Feature newChild = new Feature(feature.getFeatureName() + "-" + i);
54+
featureModel.getFeatureMap().put(newChild.getFeatureName(), newChild);
5555
newChild.getAttributes().put("abstract", new Attribute<Boolean>("abstract", true, feature));
5656
newChildren.getFeatures().add(newChild);
5757
newChild.setParentGroup(newChildren);
@@ -62,7 +62,9 @@ private void removeFeatureCardinality(Feature feature, FeatureModel featureModel
6262
}
6363
for (int j = 1; j <= i; j++) {
6464
Feature subTreeClone = feature.clone();
65-
addPrefixToNamesRecursively(subTreeClone, "-" + i + "-" + j);
65+
subTreeClone.getAttributes().clear();
66+
subTreeClone.getAttributes().put("abstract", new Attribute<Boolean>("abstract", true, subTreeClone));
67+
addPrefixToNamesRecursively(subTreeClone, "-" + i + "-" + j, featureModel);
6668
mandatoryGroup.getFeatures().add(subTreeClone);
6769
subTreeClone.setParentGroup(mandatoryGroup);
6870

@@ -71,22 +73,35 @@ private void removeFeatureCardinality(Feature feature, FeatureModel featureModel
7173
constraintReplacementMap.remove(feature.getFeatureName());
7274
for (Constraint constraint : constraintsToClone) {
7375
Constraint newConstraint = constraint.clone();
76+
if (newConstraint instanceof LiteralConstraint) {
77+
String toReplace = ((LiteralConstraint) newConstraint).getReference().getIdentifier();
78+
if (constraintReplacementMap.containsKey(toReplace)) {
79+
LiteralConstraint newLiteral = new LiteralConstraint(constraintReplacementMap.get(toReplace));
80+
LiteralConstraint subTreeRootConstraint = new LiteralConstraint(newChild);
81+
newConstraint = new ImplicationConstraint(subTreeRootConstraint, new ParenthesisConstraint(newLiteral));
82+
}
83+
} else {
84+
adaptConstraint(subTreeClone, newConstraint, constraintReplacementMap);
85+
LiteralConstraint subTreeRootConstraint = new LiteralConstraint(newChild);
86+
newConstraint = new ImplicationConstraint(subTreeRootConstraint, new ParenthesisConstraint(newConstraint));
87+
}
7488
featureModel.getOwnConstraints().add(newConstraint);
75-
adaptConstraint(subTreeClone, newConstraint, constraintReplacementMap);
7689
}
7790
}
7891
}
92+
7993
feature.getChildren().removeAll(feature.getChildren());
8094
feature.getChildren().add(newChildren);
8195
newChildren.setParentFeature(feature);
8296
}
8397

84-
private void addPrefixToNamesRecursively(Feature feature, String prefix) {
98+
private void addPrefixToNamesRecursively(Feature feature, String prefix, FeatureModel featureModel) {
8599
feature.setFeatureName(feature.getFeatureName() + prefix);
100+
featureModel.getFeatureMap().put(feature.getFeatureName(), feature);
86101
if (!feature.isSubmodelRoot()) {
87102
for (Group group : feature.getChildren()) {
88103
for (Feature subFeature : group.getFeatures()) {
89-
addPrefixToNamesRecursively(subFeature, prefix);
104+
addPrefixToNamesRecursively(subFeature, prefix, featureModel);
90105
}
91106
}
92107
}
@@ -118,14 +133,46 @@ private List<Feature> getFeatureFromSubTree(Group group) {
118133

119134
private boolean constraintContains(Constraint constraint, List<Feature> subTreeFeatures) {
120135
List<Constraint> subParts = constraint.getConstraintSubParts();
136+
if (constraint instanceof LiteralConstraint && ((LiteralConstraint) constraint).getReference() instanceof Feature) {
137+
Feature feature = (Feature) ((LiteralConstraint) constraint).getReference();
138+
if (subTreeFeatures.contains(feature)) {
139+
return true;
140+
}
141+
} else if (constraint instanceof ExpressionConstraint) {
142+
Expression left = ((ExpressionConstraint) constraint).getLeft();
143+
Expression right = ((ExpressionConstraint) constraint).getRight();
144+
return expressionContains(left, subTreeFeatures) || expressionContains(right, subTreeFeatures);
145+
}
146+
121147
for (Constraint subPart : subParts) {
122148
if (subPart instanceof LiteralConstraint && ((LiteralConstraint) subPart).getReference() instanceof Feature) {
123149
Feature feature = (Feature) ((LiteralConstraint) subPart).getReference();
124150
if (subTreeFeatures.contains(feature)) {
125151
return true;
126152
}
127-
} else {
128-
constraintContains(subPart, subTreeFeatures);
153+
} else if (constraintContains(subPart, subTreeFeatures)) {
154+
return true;
155+
}
156+
}
157+
return false;
158+
}
159+
160+
private boolean expressionContains(Expression expression, List<Feature> subTreeFeatures) {
161+
if (expression instanceof LiteralExpression) {
162+
Feature feature = (Feature) ((Attribute<?>) ((LiteralExpression) expression).getContent()).getFeature();
163+
if (subTreeFeatures.contains(feature)) {
164+
return true;
165+
}
166+
}
167+
168+
for (Expression subExpression : expression.getExpressionSubParts()) {
169+
if (expression instanceof LiteralExpression) {
170+
Feature feature = (Feature) ((LiteralExpression) expression).getContent();
171+
if (subTreeFeatures.contains(feature)) {
172+
return true;
173+
}
174+
} else if (expressionContains(subExpression, subTreeFeatures)) {
175+
return true;
129176
}
130177
}
131178
return false;
@@ -144,17 +191,38 @@ private void createFeatureReplacementMap(Feature oldSubTree, Feature newSubTree,
144191
}
145192

146193
private void adaptConstraint(Feature subTreeRoot, Constraint constraint, Map<String, Feature> featureReplacementMap) {
147-
List<Constraint> subParts = constraint.getConstraintSubParts();
148-
for (Constraint subPart : subParts) {
149-
if (subPart instanceof LiteralConstraint) {
150-
String toReplace = ((LiteralConstraint) subPart).getReference().getIdentifier();
151-
if (featureReplacementMap.containsKey(toReplace)) {
152-
LiteralConstraint subTreeRootConstraint = new LiteralConstraint(subTreeRoot);
153-
LiteralConstraint newLiteral = new LiteralConstraint(featureReplacementMap.get(toReplace));
154-
constraint.replaceConstraintSubPart(subPart, new ParenthesisConstraint(new ImplicationConstraint(subTreeRootConstraint, newLiteral)));
194+
if (constraint instanceof ExpressionConstraint) {
195+
adaptExpression(((ExpressionConstraint) constraint).getLeft(), featureReplacementMap);
196+
adaptExpression(((ExpressionConstraint) constraint).getRight(), featureReplacementMap);
197+
} else {
198+
List<Constraint> subParts = constraint.getConstraintSubParts();
199+
for (Constraint subPart : subParts) {
200+
if (subPart instanceof LiteralConstraint) {
201+
String toReplace = ((LiteralConstraint) subPart).getReference().getIdentifier();
202+
if (featureReplacementMap.containsKey(toReplace)) {
203+
LiteralConstraint newLiteral = new LiteralConstraint(featureReplacementMap.get(toReplace));
204+
constraint.replaceConstraintSubPart(subPart, newLiteral);
205+
}
206+
} else {
207+
adaptConstraint(subTreeRoot, subPart, featureReplacementMap);
155208
}
156-
} else {
157-
adaptConstraint(subTreeRoot, subPart, featureReplacementMap);
209+
}
210+
}
211+
}
212+
213+
private void adaptExpression(Expression expression, Map<String, Feature> featureReplacementMap) {
214+
if (expression instanceof LiteralExpression) {
215+
LiteralExpression literalExpression = (LiteralExpression) expression;
216+
Attribute<?> attribute = (Attribute<?>) literalExpression.getContent();
217+
if (featureReplacementMap.containsKey(attribute.getFeature().getFeatureName())) {
218+
var newAttribute = attribute.clone();
219+
newAttribute.setFeature(featureReplacementMap.get(attribute.getFeature().getFeatureName()));
220+
literalExpression.setContent(newAttribute);
221+
}
222+
223+
} else {
224+
for (Expression subExpression : expression.getExpressionSubParts()) {
225+
adaptExpression(subExpression, featureReplacementMap);
158226
}
159227
}
160228
}

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

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ private void removeGroupCardinality(Group group, FeatureModel featureModel) {
4747
Set<Feature> groupMembers = new HashSet<>(group.getFeatures());
4848

4949
int lowerBound = group.getCardinality().lower;
50-
int upperBound = Math.max(group.getCardinality().upper, groupMembers.size());
50+
int upperBound = Math.min(group.getCardinality().upper, groupMembers.size());
5151
Set<Set<Feature>> featureCombinations = new HashSet<>();
5252
for (int i = lowerBound; i <= upperBound; i++) {
5353
featureCombinations.addAll(Sets.combinations(groupMembers, i));
@@ -81,17 +81,10 @@ private Constraint createConjunction(Set<Feature> selectedFeatures, Set<Feature>
8181
}
8282

8383
private Constraint createDisjunction(Set<Constraint> constraints) {
84-
Constraint orConstraint;
85-
if (constraints.size() == 1) {
86-
Constraint constraint = constraints.iterator().next();
87-
constraints.remove(constraint);
88-
orConstraint = constraint;
89-
} else {
90-
Constraint constraint = constraints.iterator().next();
91-
constraints.remove(constraint);
92-
orConstraint = new OrConstraint(constraint, createDisjunction(constraints));
84+
MultiOrConstraint orConstraint = new MultiOrConstraint();
85+
for (Constraint constraint : constraints) {
86+
orConstraint.add_sub_part(constraint);
9387
}
94-
9588
return orConstraint;
9689
}
9790
}

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

Lines changed: 40 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -19,33 +19,53 @@ public Set<LanguageLevel> getTargetLevelsOfConversion() {
1919
return new HashSet<>(Arrays.asList(LanguageLevel.BOOLEAN_LEVEL));
2020
}
2121

22+
private Constraint getFalseConstraint(FeatureModel featureModel){
23+
return new NotConstraint(new LiteralConstraint(featureModel.getRootFeature()));
24+
}
25+
2226
@Override
2327
public void convertFeatureModel(FeatureModel rootFeatureModel, FeatureModel featureModel) {
2428
List<Constraint> constraints = featureModel.getFeatureConstraints();
2529
constraints.addAll(featureModel.getOwnConstraints());
26-
constraints.stream().forEach(this::replaceEquationInConstraint);
30+
for(Constraint constraint : constraints) {
31+
replaceEquationInConstraint(constraint, featureModel);
32+
}
2733
List<Constraint> replacements = new LinkedList<>();
2834
for (Constraint constraint : featureModel.getOwnConstraints()) {
2935
if (constraint instanceof ExpressionConstraint) {
30-
Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) constraint);
36+
Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) constraint, getFalseConstraint(featureModel));
3137
replacements.add(equationReplacement);
3238
}
3339
}
3440
featureModel.getOwnConstraints().removeIf(x -> x instanceof ExpressionConstraint);
3541
featureModel.getOwnConstraints().addAll(replacements);
36-
traverseFeatures(featureModel.getRootFeature());
42+
for (Constraint constraint : featureModel.getOwnConstraints()) {
43+
convertConstraint(constraint, featureModel);
44+
}
45+
traverseFeatures(featureModel.getRootFeature(), featureModel);
3746
}
3847

39-
private void replaceEquationInConstraint(Constraint constraint) {
48+
private void convertConstraint(Constraint constraint, FeatureModel featureModel) {
4049
for (Constraint subConstraint : constraint.getConstraintSubParts()) {
4150
if (subConstraint instanceof ExpressionConstraint) {
42-
Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) subConstraint);
51+
Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) subConstraint, getFalseConstraint(featureModel));
4352
constraint.replaceConstraintSubPart(subConstraint, equationReplacement);
53+
}else{
54+
convertConstraint(subConstraint, featureModel);
4455
}
4556
}
4657
}
4758

48-
private Constraint convertEquationToConstraint(ExpressionConstraint equation) {
59+
private void replaceEquationInConstraint(Constraint constraint, FeatureModel featureModel) {
60+
for (Constraint subConstraint : constraint.getConstraintSubParts()) {
61+
if (subConstraint instanceof ExpressionConstraint) {
62+
Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) subConstraint, getFalseConstraint(featureModel));
63+
constraint.replaceConstraintSubPart(subConstraint, equationReplacement);
64+
}
65+
}
66+
}
67+
68+
private Constraint convertEquationToConstraint(ExpressionConstraint equation, Constraint falseConstraint) {
4969
Set<Feature> featuresInEquation = getFeaturesInEquation(equation);
5070
Set<Set<Feature>> featureCombinations = getFeatureCombinations(featuresInEquation);
5171
Set<Constraint> disjunction = new HashSet<>();
@@ -55,7 +75,11 @@ private Constraint convertEquationToConstraint(ExpressionConstraint equation) {
5575
disjunction.add(createConjunction(configuration, new HashSet<>(featuresInEquation)));
5676
}
5777
}
58-
return new ParenthesisConstraint(createDisjunction(disjunction));
78+
if (disjunction.isEmpty()) {
79+
return falseConstraint;
80+
}else{
81+
return new ParenthesisConstraint(createDisjunction(disjunction));
82+
}
5983
}
6084

6185
private Set<Feature> getFeaturesInEquation(ExpressionConstraint equation) {
@@ -112,34 +136,27 @@ private Constraint createConjunction(Set<Feature> selectedFeatures, Set<Feature>
112136
}
113137

114138
private Constraint createDisjunction(Set<Constraint> constraints) {
115-
Constraint orConstraint;
116-
if (constraints.size() == 1) {
117-
Constraint constraint = constraints.iterator().next();
118-
constraints.remove(constraint);
119-
orConstraint = constraint;
120-
} else {
121-
Constraint constraint = constraints.iterator().next();
122-
constraints.remove(constraint);
123-
orConstraint = new OrConstraint(constraint, createDisjunction(constraints));
139+
MultiOrConstraint orConstraint = new MultiOrConstraint();
140+
for (Constraint constraint : constraints) {
141+
orConstraint.add_sub_part(constraint);
124142
}
125-
126143
return orConstraint;
127144
}
128145

129-
private void removeEquationFromAttributes(Feature feature) {
146+
private void removeEquationFromAttributes(Feature feature, FeatureModel featureModel) {
130147
Attribute<?> attributeConstraint = feature.getAttributes().get("constraint");
131148
Attribute<?> attributeConstraintList = feature.getAttributes().get("constraints");
132149
if (attributeConstraint != null) {
133150
if (attributeConstraint.getValue() instanceof ExpressionConstraint) {
134-
Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) attributeConstraint.getValue());
151+
Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) attributeConstraint.getValue(), getFalseConstraint(featureModel));
135152
feature.getAttributes().put("constraint", new Attribute<>("constraint", equationReplacement, feature));
136153
}
137154
}
138155
if (attributeConstraintList != null && attributeConstraintList.getValue() instanceof List<?>) {
139156
List<Object> newConstraintList = new LinkedList<>();
140157
for (Object constraint : (List<?>) attributeConstraintList.getValue()) {
141158
if (constraint instanceof ExpressionConstraint) {
142-
Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) constraint);
159+
Constraint equationReplacement = convertEquationToConstraint((ExpressionConstraint) constraint, getFalseConstraint(featureModel));
143160
newConstraintList.add(equationReplacement);
144161
} else {
145162
newConstraintList.add(constraint);
@@ -149,11 +166,11 @@ private void removeEquationFromAttributes(Feature feature) {
149166
}
150167
}
151168

152-
private void traverseFeatures(Feature feature) {
153-
removeEquationFromAttributes(feature);
169+
private void traverseFeatures(Feature feature, FeatureModel featureModel) {
170+
removeEquationFromAttributes(feature, featureModel);
154171
for (Group group : feature.getChildren()) {
155172
for (Feature subFeature : group.getFeatures()) {
156-
traverseFeatures(subFeature);
173+
traverseFeatures(subFeature, featureModel);
157174
}
158175
}
159176
}

‎src/main/java/de/vill/conversion/DropTypeLevel.java‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,15 @@
11
package de.vill.conversion;
22

3+
import de.vill.main.Example;
34
import de.vill.model.Feature;
45
import de.vill.model.FeatureModel;
56
import de.vill.model.Group;
67
import de.vill.model.LanguageLevel;
8+
import de.vill.model.constraint.Constraint;
9+
import de.vill.model.constraint.ExpressionConstraint;
10+
import de.vill.model.expression.Expression;
11+
import de.vill.model.expression.LengthAggregateFunctionExpression;
12+
import de.vill.model.expression.StringExpression;
713
import de.vill.util.Constants;
814

915
import java.util.Collections;
@@ -24,6 +30,7 @@ public Set<LanguageLevel> getTargetLevelsOfConversion() {
2430
@Override
2531
public void convertFeatureModel(final FeatureModel rootFeatureModel, final FeatureModel featureModel) {
2632
this.traverseFeatures(featureModel.getRootFeature());
33+
traverseConstraints(featureModel);
2734
}
2835

2936
private void traverseFeatures(final Feature feature) {
@@ -37,4 +44,44 @@ private void traverseFeatures(final Feature feature) {
3744
}
3845
}
3946
}
47+
48+
private void traverseConstraints(FeatureModel featureModel) {
49+
for(Constraint constraint : featureModel.getConstraints()){
50+
if (containsTypeConcept(constraint)){
51+
featureModel.getOwnConstraints().remove(constraint);
52+
}
53+
}
54+
}
55+
56+
private boolean containsTypeConcept(Constraint constraint) {
57+
if (constraint instanceof ExpressionConstraint){
58+
for(Expression subExpression : ((ExpressionConstraint) constraint).getExpressionSubParts()){
59+
if (containsTypeConcept(subExpression)){
60+
return true;
61+
}
62+
}
63+
64+
}
65+
for(Constraint subConstraints : constraint.getConstraintSubParts()){
66+
if (containsTypeConcept(subConstraints)){
67+
return true;
68+
}
69+
}
70+
return false;
71+
}
72+
73+
private boolean containsTypeConcept(Expression expression) {
74+
if (expression instanceof LengthAggregateFunctionExpression){
75+
return true;
76+
}
77+
if (expression instanceof StringExpression){
78+
return true;
79+
}
80+
for(Expression subExpressions : expression.getExpressionSubParts()){
81+
if (containsTypeConcept(subExpressions)){
82+
return true;
83+
}
84+
}
85+
return false;
86+
}
4087
}

0 commit comments

Comments
 (0)