Index: /ModelExtender/src/de/uni_hildesheim/sse/model_extender/convert/ModelExtender.java =================================================================== --- /ModelExtender/src/de/uni_hildesheim/sse/model_extender/convert/ModelExtender.java (revision 199) +++ /ModelExtender/src/de/uni_hildesheim/sse/model_extender/convert/ModelExtender.java (revision 200) @@ -54,5 +54,13 @@ this.variables = new HashMap(); this.newVariables = new ArrayList(); - + } + + /** + * Adds the given constraint to the model. + * + * @param constraint The constraint to add to the model. + * @throws ParserException If the constraint is not correctly formatted. + */ + public void addConstraint(String constraint) throws ParserException { DeclarationFinder declarationFinder = new DeclarationFinder(model, FilterType.ALL, null); List variableDeclarations = declarationFinder.getVariableDeclarations(VisibilityType.ALL); @@ -61,13 +69,5 @@ variables.put(var.getName(), var); } - } - - /** - * Adds the given constraint to the model. - * - * @param constraint The constraint to add to the model. - * @throws ParserException If the constraint is not correctly formatted. - */ - public void addConstraint(String constraint) throws ParserException { + ConstraintSyntaxTree tree = toCST(constraint); Constraint tmp = new Constraint(null); @@ -84,7 +84,10 @@ for (AbstractVariable var : newVariables) { -// System.out.println("Warning: Added completly new variable to model: " + name); addAdditionalConstraints(var); } + + varPool.clear(); + variables.clear(); + newVariables.clear(); } @@ -106,6 +109,5 @@ /** * Searches all variables with the given basename. All variables in the returned list - * look like this: <basename>=<something> - * Does not return variables that are in the newVariables list. + * look like this: <basename>[=,<,>,<=,>=]<something> * * @param baseName The beginning of the variable name. @@ -117,9 +119,6 @@ for (AbstractVariable var : variables.values()) { String name = var.getName(); - if (name.startsWith(baseName) && !newVariables.contains(var)) { - char firstCharAfter = name.charAt(baseName.length()); - if (firstCharAfter == '=') { - list.add(var); - } + if (name.startsWith(baseName) && name.length() > baseName.length()) { + list.add(var); } } @@ -158,4 +157,8 @@ for (AbstractVariable variableWithSameBaseName : variablesWithSameBasename) { + if (variableWithSameBaseName.equals(additionalVariable)) { + continue; + } + Matcher varMatcher = VARIABLE_PATTERN.matcher(variableWithSameBaseName.getName()); @@ -172,5 +175,5 @@ String op2 = varMatcher.group(2); int val2 = Integer.parseInt(varMatcher.group(3)); - + switch (intersect(op1, val1, op2, val2)) { case NONE: @@ -197,6 +200,5 @@ case INTERSECT: - // TODO: no constraints? - + // No constraints here break; @@ -269,5 +271,5 @@ op2 = ">"; val2 -= 1; - } else if (op1.equals("<=")) { + } else if (op2.equals("<=")) { op2 = "<"; val2 += 1; @@ -301,11 +303,11 @@ */ } else if (op2.equals("=") && op1.equals(">")) { + if (val1 < val2) { + result = IntersectionType.ONE_IS_SUPERSET_OF_TWO; + } else { + result = IntersectionType.NONE; + } + } else if (op2.equals("=") && op1.equals("<")) { if (val1 > val2) { - result = IntersectionType.ONE_IS_SUPERSET_OF_TWO; - } else { - result = IntersectionType.NONE; - } - } else if (op2.equals("=") && op1.equals("<")) { - if (val1 < val2) { result = IntersectionType.ONE_IS_SUPERSET_OF_TWO; } else { Index: /ModelExtender/test/de/uni_hildesheim/de/see/model_extender/test/ModelExtenderTest.java =================================================================== --- /ModelExtender/test/de/uni_hildesheim/de/see/model_extender/test/ModelExtenderTest.java (revision 199) +++ /ModelExtender/test/de/uni_hildesheim/de/see/model_extender/test/ModelExtenderTest.java (revision 200) @@ -4,4 +4,5 @@ import java.io.FileNotFoundException; import java.io.IOException; +import java.io.StringWriter; import junit.framework.Assert; @@ -17,5 +18,7 @@ import de.uni_hildesheim.sse.model_extender.in.DimacsReader; import de.uni_hildesheim.sse.model_extender.in.MalformedFileException; +import de.uni_hildesheim.sse.trans.DimacsTestUtils; import de.uni_hildesheim.sse.trans.in.ParserException; +import de.uni_hildesheim.sse.trans.out.DimacsWriter; /** @@ -87,4 +90,173 @@ /** + * Tests whether additional constraints for variables with <, > or = are + * added correctly. + */ + @Test + public void testAdditionalConstraints() { + try { + Project model = loadModel("testdata/testAdditionalConstraints.dimacs"); + + ModelExtender extender = new ModelExtender(model); + + extender.addConstraint("A<6"); + extender.addConstraint("A<4"); + + extender.addConstraint("B>1"); + extender.addConstraint("B>2"); + + extender.addConstraint("C=8"); + + extender.addConstraint("D>=2"); + extender.addConstraint("D>=6"); + extender.addConstraint("D>1"); + + + extender.addConstraint("E<=8"); + extender.addConstraint("E<=3"); + extender.addConstraint("E<4"); + + StringWriter dimacsStringWriter = new StringWriter(); + DimacsWriter writer = new DimacsWriter(model, dimacsStringWriter); + writer.write(); + + String dimacsString = dimacsStringWriter.toString(); + + testA(dimacsString); + testB(dimacsString); + testC(dimacsString); + testD(dimacsString); + testE(dimacsString); + + } catch (IOException | MalformedFileException | ParserException e) { + e.printStackTrace(); + Assert.fail(); + } + } + + /** + * Tests whether the correct constraints for the variable E are added. + * + * @param dimacsString The DIMACS model as string. + */ + private void testE(String dimacsString) { + int eE8 = DimacsTestUtils.getNumberOfVariable(dimacsString, "E=8"); + int eLE8 = DimacsTestUtils.getNumberOfVariable(dimacsString, "E<=8"); + int eLE3 = DimacsTestUtils.getNumberOfVariable(dimacsString, "E<=3"); + int eL4 = DimacsTestUtils.getNumberOfVariable(dimacsString, "E<4"); + + // E<=8 is superset of E=8 + // E=8 -> E<=8 == E<=8 || !E=8 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, eLE8, -eE8)); + + // E=8 and E<=3 do not intersect: + // E=8 XOR E<=3 == !E=8 || !E<=3 AND E=8 || E<=3 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, -eE8, -eLE3)); + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, eE8, eLE3)); + + // E<=8 is superset of E<=3 + // E<=3 -> E<=8 == E<=8 || !E<=3 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, eLE8, -eLE3)); + + // E<4 is equal to E<=3 + // E<4 = E<=3 == !E<=3 || E<4 AND E<=3 || !E<4 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, -eLE3, eL4)); + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, eLE3, -eL4)); + } + + /** + * Tests whether the correct constraints for the variable D are added. + * + * @param dimacsString The DIMACS model as string. + */ + private void testD(String dimacsString) { + int dE5 = DimacsTestUtils.getNumberOfVariable(dimacsString, "D=5"); + int dGE2 = DimacsTestUtils.getNumberOfVariable(dimacsString, "D>=2"); + int dGE6 = DimacsTestUtils.getNumberOfVariable(dimacsString, "D>=6"); + int dG1 = DimacsTestUtils.getNumberOfVariable(dimacsString, "D>1"); + + // D>=2 is superset of D=5 + // D=5 -> D>=2 == D>=2 || !D=5 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, dGE2, -dE5)); + + // D=5 and D>=6 do not intersect: + // D=5 XOR D>=6 == !D=5 || !D>=6 AND D=5 || D>=6 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, -dE5, -dGE6)); + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, dE5, dGE6)); + + // D>=2 is superset of D>=6 + // D>=6 -> D>=2 == D>=2 || !D>=6 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, dGE2, -dGE6)); + + // D>1 is equal to D>=2 + // D>1 = D>=2 == !D>=2 || D>1 AND D>=2 || !D>1 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, -dGE2, dG1)); + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, dGE2, -dG1)); + } + + /** + * Tests whether the correct constraints for the variable C are added. + * + * @param dimacsString The DIMACS model as string. + */ + private void testC(String dimacsString) { + int cE9 = DimacsTestUtils.getNumberOfVariable(dimacsString, "C=9"); + int cE8 = DimacsTestUtils.getNumberOfVariable(dimacsString, "C=8"); + + // C=9 and C=9 do not intersect: + // C=9 XOR C=8 == !C=9 || !C=8 AND C=9 || C=8 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, -cE8, -cE9)); + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, cE8, cE9)); + } + + /** + * Tests whether the correct constraints for the variable B are added. + * + * @param dimacsString The DIMACS model as string. + */ + private void testB(String dimacsString) { + int bE2 = DimacsTestUtils.getNumberOfVariable(dimacsString, "B=2"); + int bG2 = DimacsTestUtils.getNumberOfVariable(dimacsString, "B>2"); + int bG1 = DimacsTestUtils.getNumberOfVariable(dimacsString, "B>1"); + + // B>1 is superset of B=2: + // B=2 -> B>1 == B>1 || !B=2 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, -bE2, bG1)); + + // B=2 and B>2 do not intersect: + // B=2 XOR B>2 == !B=2 || !B>2 AND B=2 || B>2 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, -bE2, -bG2)); + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, bE2, bG2)); + + // B>1 is superset of B>2: + // B>2 -> B>1 == B>1 || !B>2 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, -bG2, bG1)); + } + + /** + * Tests whether the correct constraints for the variable A are added. + * + * @param dimacsString The DIMACS model as string. + */ + private void testA(String dimacsString) { + int aE5 = DimacsTestUtils.getNumberOfVariable(dimacsString, "A=5"); + int aL6 = DimacsTestUtils.getNumberOfVariable(dimacsString, "A<6"); + int aL4 = DimacsTestUtils.getNumberOfVariable(dimacsString, "A<4"); + + // A<6 is superset of A=5: + // A=5 -> A<6 == A<6 || !A=5 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, -aE5, aL6)); + + // A=6 and A<4 do not intersect: + // A=5 XOR A<4 == !A=5 || !A<4 AND A=5 || A<4 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, -aE5, -aL4)); + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, aE5, aL4)); + + // A<6 is superset of A<4: + // A<4 -> A<6 == A<6 || !A<4 + Assert.assertTrue(DimacsTestUtils.containsConstraint(dimacsString, -aL4, aL6)); + } + + /** * Loads the given model from a .dimacs file. * Index: /ModelExtender/testdata/testAdditionalConstraints.dimacs =================================================================== --- /ModelExtender/testdata/testAdditionalConstraints.dimacs (revision 200) +++ /ModelExtender/testdata/testAdditionalConstraints.dimacs (revision 200) @@ -0,0 +1,7 @@ +c 1 A=5 +c 2 B=2 +c 3 C=9 +c 4 D=5 +c 5 E=8 +p CNF 5 1 +1 2 3 4 5 0