Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java (revision 67) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java (revision 68) @@ -36,9 +36,11 @@ project.add(declaration); } + declfinder = null; + declarations = null; // 2. Convert the constraints List constraints = constFinder.getConstraints(); - int num = 0; - for (Constraint constraint : constraints) { + for (int i = 0, n = constraints.size(); i < n; i++) { + Constraint constraint = constraints.get(i); DisjunctionChecker checker = new DisjunctionChecker(constraint); if (checker.isDisjunctionTerm()) { @@ -46,9 +48,13 @@ } else { converter.convert(constraint); - num++; - if (num % 100 == 0) { - System.out.println("Progress: " + num); + if (i % 100 == 0) { + System.out.println("Progress: " + i); } } + /* + * Release constraint to deallocate memory. + * set(index, null) avoids Array.copy + */ + constraints.set(i, null); } } Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 67) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 68) @@ -29,5 +29,6 @@ /** * Converts a boolean formula in a list of disjunction terms by means of - * max terms. + * max terms. * @author Adam Krafczyk * @author El-Sharkawy @@ -216,18 +217,4 @@ } -// /** -// * Returns whether the boolean expression with the given variable states is true or false. -// * @param expression The boolean expression -// * @param config The {@link Configuration} that defines the state of the variables -// * @return The result of the boolean expression -// */ -// private boolean getResult(ConstraintSyntaxTree expression, Configuration config) { -// EvaluationVisitor evalVisitor = new EvaluationVisitor(); -// evalVisitor.init(config, null, false, null); -// expression.accept(evalVisitor); -// BooleanValue result = (BooleanValue) evalVisitor.getResult(); -// return result.equals(BooleanValue.TRUE); -// } - /** * Creates an {@link ConstraintSyntaxTree} with the variables negated and OR'd together. Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2.java (revision 68) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2.java (revision 68) @@ -0,0 +1,114 @@ +package de.uni_hildesheim.sse.trans.convert; + +import java.math.BigInteger; +import java.util.List; + +import de.uni_hildesheim.sse.model.confModel.AssignmentState; +import de.uni_hildesheim.sse.model.confModel.Configuration; +import de.uni_hildesheim.sse.model.confModel.ConfigurationException; +import de.uni_hildesheim.sse.model.confModel.IDecisionVariable; +import de.uni_hildesheim.sse.model.cst.ConstraintSyntaxTree; +import de.uni_hildesheim.sse.model.cst.OCLFeatureCall; +import de.uni_hildesheim.sse.model.cst.Variable; +import de.uni_hildesheim.sse.model.cstEvaluation.EvaluationVisitor; +import de.uni_hildesheim.sse.model.varModel.AbstractVariable; +import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords; +import de.uni_hildesheim.sse.model.varModel.values.BooleanValue; +import de.uni_hildesheim.sse.trans.Bundle; +import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory; +import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory.EASyLogger; + +/** + * Alternative implementation of {@link MaxTermConverter}, which uses a backtracking algorithm + * instead of iteration to find all max terms. + * @author El-Sharkawy + * + */ +public class MaxTermConverter2 extends MaxTermConverter { + private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(MaxTermConverter2.class, Bundle.ID); + + + @Override + protected void handleSmallConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray, + Configuration config, List parts) { + + handleBigConstraint(originalConstraint, declarationArray, config, parts); + } + + @Override + protected void handleBigConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray, + Configuration config, List parts) { + + EvaluationVisitor evalVisitor = new EvaluationVisitor(); + evalVisitor.init(config, null, false, null); + // for each combination of the variables (true or false) + for (BigInteger i = new BigInteger("0"); i.compareTo(new BigInteger("2").pow(declarationArray.length)) == -1; + i = i.add(new BigInteger("1"))) { + if (i.mod(new BigInteger("1000")).compareTo(new BigInteger("0")) == 0) { + System.out.println(i + "/" + new BigInteger("2").pow(declarationArray.length)); + } + boolean[] state = new boolean[declarationArray.length]; + for (int j = 0; j < state.length; j++) { + IDecisionVariable decisionVar = config.getDecision(declarationArray[j]); + /* + * i is a bit-field where each bit represents one variable + * j is the current variable + * To test if variable #j is true check if the bit #j in i is 0 or 1 + */ + if (i.testBit(j)) { + state[j] = true; + try { + decisionVar.setValue(BooleanValue.TRUE, AssignmentState.ASSIGNED); + } catch (ConfigurationException e) { + // TODO + LOGGER.exception(e); + } + } else { + state[j] = false; + try { + decisionVar.setValue(BooleanValue.FALSE, AssignmentState.ASSIGNED); + } catch (ConfigurationException e) { + // TODO + LOGGER.exception(e); + } + } + } + + // get the result + originalConstraint.accept(evalVisitor); + boolean result = evalVisitor.constraintFulfilled(); + + // if the result it false, add the negated combination to the list of expressions + if (!result) { + parts.add(createNegatedORExpression(declarationArray, state)); + } + + // 1 * init() + n * clearResult() is much faster than n * (init() + clear()) + evalVisitor.clearResult(); + } + } + + /** + * Creates an {@link ConstraintSyntaxTree} with the variables negated and OR'd together. + * @param variables Array of Variables + * @param states Array whether each variable is true or false + * @return the {@link ConstraintSyntaxTree} + */ + private ConstraintSyntaxTree createNegatedORExpression(AbstractVariable[] variables, boolean[] states) { + ConstraintSyntaxTree call = null; + if (!states[0]) { + call = new Variable(variables[0]); + } else { + call = new OCLFeatureCall(new Variable(variables[0]), OclKeyWords.NOT); + } + + for (int i = 1; i < variables.length; i++) { + ConstraintSyntaxTree variable = new Variable(variables[i]); + if (states[i]) { + variable = new OCLFeatureCall(variable, OclKeyWords.NOT); + } + call = new OCLFeatureCall(call, OclKeyWords.OR, variable); + } + return call; + } +}