|
7 | 7 | import org.variantsync.diffdetective.util.fide.FixTrueFalse.Formula; |
8 | 8 | import org.variantsync.diffdetective.variation.tree.VariationNode; |
9 | 9 |
|
| 10 | +import java.util.Map; |
| 11 | +import java.util.Map.Entry; |
10 | 12 | import java.util.function.Consumer; |
11 | 13 |
|
12 | 14 | /** |
@@ -36,6 +38,39 @@ public Configure(final Node configuration) { |
36 | 38 | this(FixTrueFalse.EliminateTrueAndFalse(configuration)); |
37 | 39 | } |
38 | 40 |
|
| 41 | + /** |
| 42 | + * Create a configuration from an assignment of variable names to boolean values. |
| 43 | + * The given assignment may be complete or partial. |
| 44 | + * Internally, a big conjunction of literals is created: |
| 45 | + * <pre> |
| 46 | + * ⋀ f ∧ ⋀ ¬ f |
| 47 | + * (f, true) ∈ assignment (f, false) ∈ assignment |
| 48 | + * </pre> |
| 49 | + * |
| 50 | + * As an example, suppose the map contains the following entries: |
| 51 | + * <pre> |
| 52 | + * A ↦ true |
| 53 | + * B ↦ false |
| 54 | + * C ↦ true |
| 55 | + * </pre> |
| 56 | + * then we construct a formula A ∧ (¬ B) ∧ C. |
| 57 | + */ |
| 58 | + public Configure(final Map<String, Boolean> assignment) { |
| 59 | + // We use commutativity of ∧ to iterate the map only once instead of twice as shown in the formula above. |
| 60 | + final Formula[] fixedFeatures = new Formula[assignment.size()]; |
| 61 | + int i = 0; |
| 62 | + for (Entry<String, Boolean> entry : assignment.entrySet()) { |
| 63 | + fixedFeatures[i] = Formula.var(entry.getKey()); |
| 64 | + if (!entry.getValue()) { |
| 65 | + fixedFeatures[i] = Formula.not(fixedFeatures[i]); |
| 66 | + } |
| 67 | + |
| 68 | + ++i; |
| 69 | + } |
| 70 | + |
| 71 | + this.configuration = Formula.and(fixedFeatures); |
| 72 | + } |
| 73 | + |
39 | 74 | @Override |
40 | 75 | public boolean test(VariationNode<?, ?> v) { |
41 | 76 | return SAT.isSatisfiable( |
|
0 commit comments