Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java (revision 92) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java (revision 93) @@ -83,13 +83,16 @@ LOGGER.info("2.) Convert model."); CNFConverter.convert(model, new MaxTermConverter2()); - System.out.println("Conversion completed."); LOGGER.info("3.) Optimize model."); ModelOptimizer optimizer = new ModelOptimizer(model); + int removed = optimizer.removeUnusedVariables(); - System.out.println("Removed " + removed + " variables."); + LOGGER.info("Removed " + removed + " unused variables."); + removed = optimizer.handleConstantVariables(); - System.out.println("Removed " + removed + " constraints."); - System.out.println("Optimizing completed."); + LOGGER.info("Removed " + removed + " constraints with constant variables."); + + removed = optimizer.removeDuplicatedConstraints(); + LOGGER.info("Removed " + removed + " duplicated constraints."); LOGGER.info("4.) Write model."); @@ -102,5 +105,4 @@ LOGGER.exception(e); } - System.out.println("Writing completed."); break; default: Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ModelOptimizer.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ModelOptimizer.java (revision 92) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ModelOptimizer.java (revision 93) @@ -1,4 +1,5 @@ package de.uni_hildesheim.sse.trans.convert; +import java.util.ArrayList; import java.util.HashSet; import java.util.List; @@ -18,11 +19,15 @@ import de.uni_hildesheim.sse.model.varModel.filter.DeclrationInConstraintFinder; import de.uni_hildesheim.sse.model.varModel.filter.FilterType; +import de.uni_hildesheim.sse.trans.Bundle; +import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory; +import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory.EASyLogger; /** - * Optimizes a model in CNF in various ways. + * Optimizes a model with constraints in CNF in various ways. * * @author Adam Krafczyk */ public class ModelOptimizer { + private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(ModelOptimizer.class, Bundle.ID); private Project model; @@ -111,5 +116,5 @@ Set declarations = declarationFinder.getDeclarations(); - // Skip constraints with only 1 variable since this are the constraints that define the constatn variables + // Skip constraints with only 1 variable since this are the constraints that define the constant variables if (declarations.size() <= 1) { continue; @@ -122,5 +127,4 @@ break; } - // TODO: we could say that the model is not solvable if the else branch is reached } else if (alwaysTrueVariables.contains(var)) { if (!isVariableNegated(tree, var)) { @@ -128,5 +132,4 @@ break; } - // TODO: we could say that the model is not solvable if the else branch is reached } } @@ -145,4 +148,99 @@ return numRemoved; + } + + /** + * Removes all duplicated constraints from the model. Alternative implementation with equivalence classes. + * + * @return Number of removed constraints + */ + public int removeDuplicatedConstraints() { + List[] equivalenceClasses = createEquivalenceClasses(); + + // 2) Remove duplicated constraints in the equivalence classes + int removed = 0; + + for (int h = 0; h < equivalenceClasses.length; h++) { + for (int i = 0, n = equivalenceClasses[h].size(); i < n; i++) { + Constraint constraint = equivalenceClasses[h].get(i); + if (constraint == null) { + continue; + } + + ConstraintSyntaxTree tree = constraint.getConsSyntax(); + DeclrationInConstraintFinder finder = new DeclrationInConstraintFinder(tree); + Set declarations = finder.getDeclarations(); + + for (int j = i + 1; j < n; j++) { + Constraint otherConstraint = equivalenceClasses[h].get(j); + if (otherConstraint == null) { + continue; + } + + ConstraintSyntaxTree otherTree = otherConstraint.getConsSyntax(); + DeclrationInConstraintFinder otherFinder = new DeclrationInConstraintFinder(otherTree); + Set otherDeclarations = otherFinder.getDeclarations(); + + if (otherDeclarations.containsAll(declarations)) { + boolean equal = true; + + AbstractVariable[] declarationArray = declarations.toArray(new AbstractVariable[] {}); + + for (int k = 0; k < declarationArray.length; k++) { + if (isVariableNegated(tree, declarationArray[k]) + != isVariableNegated(otherTree, declarationArray[k])) { + equal = false; + break; + } + } + + if (equal) { + model.removeElement(otherConstraint); + equivalenceClasses[h].set(j, null); + removed++; + } + } + } + + /* + * Release constraint to deallocate memory. + * set(index, null) avoids Array.copy + */ + equivalenceClasses[h].set(i, null); + } + } + + return removed; + } + + /** + * Split all constraints of the project into equivalence classes according to their length. + * @return An array of lists with constraint that all have the same length. + */ + private List[] createEquivalenceClasses() { + ConstraintFinder cFinder = new ConstraintFinder(model); + List constraints = cFinder.getConstraints(); + + List[] equivalenceClasses = new List[10]; // TODO 10? + for (int i = 0; i < equivalenceClasses.length; i++) { + equivalenceClasses[i] = new ArrayList(); + } + + for (int i = 0, n = constraints.size(); i < n; i++) { + Constraint constraint = constraints.get(i); + ConstraintSyntaxTree tree = constraint.getConsSyntax(); + DeclrationInConstraintFinder finder = new DeclrationInConstraintFinder(tree); + Set declarations = finder.getDeclarations(); + + int length = Math.min(declarations.size(), equivalenceClasses.length); + equivalenceClasses[length - 1].add(constraint); + + /* + * Release constraint to deallocate memory. + * set(index, null) avoids Array.copy + */ + constraints.set(i, null); + } + return equivalenceClasses; } @@ -179,5 +277,5 @@ } else { // TODO - throw new RuntimeException(); + LOGGER.error("Unexpected operator in CNF formula."); } } @@ -192,6 +290,5 @@ } else { // TODO - System.out.println(tree); - throw new RuntimeException(); + LOGGER.error("Unexpected ConstraintSyntaxTree in CNF formula."); } Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/ModelOptimizerTest.java =================================================================== --- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/ModelOptimizerTest.java (revision 92) +++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/ModelOptimizerTest.java (revision 93) @@ -14,4 +14,7 @@ import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords; import de.uni_hildesheim.sse.model.varModel.filter.ConstraintFinder; +import de.uni_hildesheim.sse.model.varModel.filter.DeclarationFinder; +import de.uni_hildesheim.sse.model.varModel.filter.DeclarationFinder.VisibilityType; +import de.uni_hildesheim.sse.model.varModel.filter.FilterType; /** @@ -51,5 +54,14 @@ ModelOptimizer optimizer = new ModelOptimizer(model); - Assert.assertEquals(2, optimizer.removeUnusedVariables()); + int removed = optimizer.removeUnusedVariables(); + + /* + * c and d should be removed + */ + + Assert.assertEquals(2, removed); + + DeclarationFinder declarationFinder = new DeclarationFinder(model, FilterType.ALL, null); + Assert.assertEquals(2, declarationFinder.getVariableDeclarations(VisibilityType.ALL).size()); } @@ -94,5 +106,5 @@ ModelOptimizer optimizer = new ModelOptimizer(model); - optimizer.handleConstantVariables(); + int removed = optimizer.handleConstantVariables(); /* @@ -100,7 +112,52 @@ */ + Assert.assertEquals(2, removed); + ConstraintFinder cFinder = new ConstraintFinder(model); Assert.assertEquals(4, cFinder.getConstraints().size()); } + /** + * Tests the removeDuplicatedConstraints() method. + * + * @throws CSTSemanticException can't happen. + */ + @Test + public void testRemoveDuplicatedConstraints() throws CSTSemanticException { + Project model = new Project("TestModel"); + + DecisionVariableDeclaration declA = new DecisionVariableDeclaration("a", BooleanType.TYPE, null); + DecisionVariableDeclaration declB = new DecisionVariableDeclaration("b", BooleanType.TYPE, null); + + model.add(declA); + model.add(declB); + + ConstraintSyntaxTree[] terms = new ConstraintSyntaxTree[3]; + + Variable varA = new Variable(declA); + Variable varB = new Variable(declB); + + terms[0] = new OCLFeatureCall(varA, OclKeyWords.OR, varB); + terms[1] = new OCLFeatureCall(varB, OclKeyWords.OR, varA); + terms[2] = new OCLFeatureCall(varA, OclKeyWords.OR, new OCLFeatureCall(varB, OclKeyWords.NOT)); + + for (ConstraintSyntaxTree tree : terms) { + Constraint constraint = new Constraint(model); + constraint.setConsSyntax(tree); + model.add(constraint); + } + + ModelOptimizer optimizer = new ModelOptimizer(model); + int removed = optimizer.removeDuplicatedConstraints(); + + /* + * term [1] should be removed + */ + + Assert.assertEquals(1, removed); + + ConstraintFinder cFinder = new ConstraintFinder(model); + Assert.assertEquals(2, cFinder.getConstraints().size()); + } + }