Index: /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CSTSimplifier.java =================================================================== --- /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CSTSimplifier.java (revision 426) +++ /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CSTSimplifier.java (revision 426) @@ -0,0 +1,268 @@ +package de.uni_hildesheim.sse.trans.convert; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +import de.uni_hildesheim.sse.model.cst.Comment; +import de.uni_hildesheim.sse.model.cst.CompoundAccess; +import de.uni_hildesheim.sse.model.cst.CompoundInitializer; +import de.uni_hildesheim.sse.model.cst.ConstantValue; +import de.uni_hildesheim.sse.model.cst.ConstraintSyntaxTree; +import de.uni_hildesheim.sse.model.cst.ContainerInitializer; +import de.uni_hildesheim.sse.model.cst.ContainerOperationCall; +import de.uni_hildesheim.sse.model.cst.IConstraintTreeVisitor; +import de.uni_hildesheim.sse.model.cst.IfThen; +import de.uni_hildesheim.sse.model.cst.Let; +import de.uni_hildesheim.sse.model.cst.OCLFeatureCall; +import de.uni_hildesheim.sse.model.cst.Parenthesis; +import de.uni_hildesheim.sse.model.cst.UnresolvedExpression; +import de.uni_hildesheim.sse.model.cst.Variable; +import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords; +import de.uni_hildesheim.sse.model.varModel.filter.DeclrationInConstraintFinder; + +/** + * Tries to simplify a {@link ConstraintSyntaxTree} by expanding a OR (b AND c) + * to (a OR b) AND (a OR c). + * Only works properly if the {@link ConstraintSyntaxTree} only contains AND, + * OR and NOT. First call accept(), then getTrees() to get the result. + * + * @author Adam Krafczyk + */ +class CSTSimplifier implements IConstraintTreeVisitor { + +// private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(CSTSimplifier.class, Main.ID); + + private static final int MIN_LENGTH = 14; + + /** + * Possible states of the visitor. + */ + private enum State { + FIND_POSSIBLE_EXPANSION, + } + private State state = State.FIND_POSSIBLE_EXPANSION; + + private String previousOperation; + + private List trees; + + /** + * Creates a {@link CSTSimplifier}. + */ + public CSTSimplifier() { + trees = new ArrayList(); + } + + /** + * Getter for the {@link ConstraintSyntaxTree}s created after an accept call. + * @return An unmodifiable list of {@link ConstraintSyntaxTree}s, to be + * interpreted as AND'd together, representing the + * {@link ConstraintSyntaxTree} that accept()'d this visitor. + */ + public List getTrees() { + return Collections.unmodifiableList(trees); + } + + /** + * Returns the "length" of a {@link ConstraintSyntaxTree}. + * @param cst The {@link ConstraintSyntaxTree} to get the "length" of. + * @return The "length" (i.e. the number of variables in the {@link ConstraintSyntaxTree}). + */ + private int getSyntaxTreeLength(ConstraintSyntaxTree cst) { + return new DeclrationInConstraintFinder(cst).getDeclarations().size(); + } + + @Override + public void visitConstantValue(ConstantValue value) {} + + @Override + public void visitVariable(Variable variable) {} + + @Override + public void visitParenthesis(Parenthesis parenthesis) {} + + @Override + public void visitComment(Comment comment) {} + + @Override + public void visitOclFeatureCall(OCLFeatureCall call) { + switch (state) { + case FIND_POSSIBLE_EXPANSION: + String currentOperation = call.getOperation(); + if (currentOperation.equals(OclKeyWords.AND) + && previousOperation.equals(OclKeyWords.OR)) { + + // TODO expand + + } else { + previousOperation = call.getOperation(); + if (getSyntaxTreeLength(call.getOperand()) >= MIN_LENGTH) { + call.getOperand().accept(this); + } + + if (currentOperation.equals(OclKeyWords.OR) + || currentOperation.equals(OclKeyWords.AND)) { + previousOperation = call.getOperation(); + if (getSyntaxTreeLength(call.getParameter(0)) >= MIN_LENGTH) { + call.getParameter(0).accept(this); + } + } + } + break; + + default: + break; + } +// switch (state) { +// case INITIAL: +// if (call.getOperation().equals(OclKeyWords.OR)) { +// LOGGER.info("Highest operation is an OR"); +// +// state = State.EXPAND; +// +// call.getOperand().accept(this); +// ConstraintSyntaxTree passedOperand = passUp; +// passUp = null; +// +// if (leftTree != null && rightTree != null) { +// trees.add(new OCLFeatureCall(leftTree, OclKeyWords.OR, call.getParameter(0))); +// trees.add(new OCLFeatureCall(rightTree, OclKeyWords.OR, call.getParameter(0))); +// } else { +// +// call.getParameter(0).accept(this); +// ConstraintSyntaxTree passedParameter = passUp; +// passUp = null; +// +// if (leftTree != null && rightTree != null) { +// trees.add(new OCLFeatureCall(leftTree, OclKeyWords.OR, call.getOperand())); +// trees.add(new OCLFeatureCall(rightTree, OclKeyWords.OR, +// call.getOperand())); +// } +// +// if (passedOperand != null) { +// if (passedParameter != null) { +// trees.add(new OCLFeatureCall(passedOperand, OclKeyWords.OR, passedParameter)); +// } else { +// trees.add(new OCLFeatureCall(passedOperand, OclKeyWords.OR, call.getParameter(0))); +// } +// } else { +// if (passedParameter != null) { +// trees.add(new OCLFeatureCall(call.getOperand(), OclKeyWords.OR, passedParameter)); +// } +// } +// } +// +// state = State.INITIAL; +// +// } else if (call.getOperation().equals(OclKeyWords.AND)) { +// LOGGER.info("Highest operation is an AND"); +// // split tree +// trees.add(call.getOperand()); +// trees.add(call.getParameter(0)); +// } +// break; +// +// case EXPAND: // highest operand is an OR +// if (call.getOperation().equals(OclKeyWords.AND)) { +// LOGGER.info("Second highest operation is an AND"); +// +// leftTree = call.getOperand(); +// rightTree = call.getParameter(0); +// } else if (call.getOperation().equals(OclKeyWords.NOT)) { +// LOGGER.info("Second highest operation is a NOT"); +// +// state = State.NEGATE_EXPAND; +// +// call.getOperand().accept(this); +// +// state = State.EXPAND; +// } +// break; +// +// case NEGATE_EXPAND: // highest operand is an OR; second highest is a NOT +// // if this operation is an OR then expand the NOT into it +// if (call.getOperation().equals(OclKeyWords.OR)) { +// LOGGER.info("Third highest (negated) operation is an OR"); +// leftTree = new OCLFeatureCall(call.getOperand(), OclKeyWords.NOT); +// rightTree = new OCLFeatureCall(call.getParameter(0), OclKeyWords.NOT); +// break; +// } +// state = State.NEGATE; +// +// // fall through +// case NEGATE: // some level below a NOT +// // recursively expand the not further down into the tree +// +// if (call.getOperation().equals(OclKeyWords.AND)) { +// LOGGER.info("Negating an AND"); +// +// call.getOperand().accept(this); +// ConstraintSyntaxTree leftSide = passUp; +// passUp = null; +// if (leftSide == null) { +// leftSide = new OCLFeatureCall(call.getOperand(), OclKeyWords.NOT); +// } +// +// call.getParameter(0).accept(this); +// ConstraintSyntaxTree rightSide = passUp; +// passUp = null; +// if (rightSide == null) { +// rightSide = new OCLFeatureCall(call.getParameter(0), OclKeyWords.NOT); +// } +// +// passUp = new OCLFeatureCall(leftSide, OclKeyWords.OR, rightSide); +// +// } else if (call.getOperation().equals(OclKeyWords.OR)) { +// LOGGER.info("Negating an OR"); +// +// call.getOperand().accept(this); +// ConstraintSyntaxTree leftSide = passUp; +// passUp = null; +// if (leftSide == null) { +// leftSide = new OCLFeatureCall(call.getOperand(), OclKeyWords.NOT); +// } +// +// call.getParameter(0).accept(this); +// ConstraintSyntaxTree rightSide = passUp; +// passUp = null; +// if (rightSide == null) { +// rightSide = new OCLFeatureCall(call.getParameter(0), OclKeyWords.NOT); +// } +// +// passUp = new OCLFeatureCall(leftSide, OclKeyWords.AND, rightSide); +// +// } else if (call.getOperation().equals(OclKeyWords.NOT)) { +// LOGGER.info("Negating a NOT"); +// +// passUp = call.getOperand(); +// } +// break; +// +// default: +// break; +// } + } + + @Override + public void visitLet(Let let) {} + + @Override + public void visitIfThen(IfThen ifThen) {} + + @Override + public void visitContainerOperationCall(ContainerOperationCall call) {} + + @Override + public void visitCompoundAccess(CompoundAccess access) {} + + @Override + public void visitUnresolvedExpression(UnresolvedExpression expression) {} + + @Override + public void visitCompoundInitializer(CompoundInitializer initializer) {} + + @Override + public void visitContainerInitializer(ContainerInitializer initializer) {} + +} Index: /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java =================================================================== --- /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 425) +++ /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 426) @@ -5,4 +5,5 @@ import java.util.Comparator; import java.util.HashMap; +import java.util.List; import java.util.Map; import java.util.Set; @@ -82,4 +83,6 @@ } +// originalConstraint.accept(new DebugConstraintTreeVisitor()); + // Split top level AND calls into two separate terms if (!handled && originalConstraint instanceof OCLFeatureCall) { @@ -93,132 +96,146 @@ } - // Handle an OR with an AND at one side - if (!handled && originalConstraint instanceof OCLFeatureCall) { - OCLFeatureCall highestOperation = (OCLFeatureCall) originalConstraint; - - // if highest operation is an OR - if (highestOperation.getOperation().equals(OclKeyWords.OR)) { - LOGGER.info("highest operation is an OR"); - if (highestOperation.getOperand() instanceof OCLFeatureCall) { - OCLFeatureCall leftOperation = (OCLFeatureCall) highestOperation.getOperand(); - - // if the left side of the OR is an AND - if (leftOperation.getOperation().equals(OclKeyWords.AND)) { - LOGGER.info("left side is an and"); - OCLFeatureCall call1 = new OCLFeatureCall(leftOperation.getOperand(), - OclKeyWords.OR, highestOperation.getParameter(0)); - OCLFeatureCall call2 = new OCLFeatureCall(leftOperation.getParameter(0), - OclKeyWords.OR, highestOperation.getParameter(0)); - - createCNFParts(call1); - createCNFParts(call2); - handled = true; - } - - // if the left side of the OR is a NOT - if (!handled && leftOperation.getOperation().equals(OclKeyWords.NOT)) { - LOGGER.info("left side is a NOT"); - if (leftOperation.getOperand() instanceof OCLFeatureCall) { - OCLFeatureCall negatedOperation = (OCLFeatureCall) leftOperation.getOperand(); - - // if the operation inside the NOT is an AND - if (negatedOperation.getOperation().equals(OclKeyWords.AND)) { - LOGGER.info("negated operation is an AND"); - - // expand the NOT into the and call - OCLFeatureCall newOperand2 = new OCLFeatureCall( - new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), - OclKeyWords.OR, - new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); - - OCLFeatureCall newCall = new OCLFeatureCall(newOperand2, - OclKeyWords.OR, highestOperation.getParameter(0)); - createCNFParts(newCall); - handled = true; - } - - // if the operation inside the NOT is an OR - if (negatedOperation.getOperation().equals(OclKeyWords.OR)) { - LOGGER.info("negated operation is an OR"); - - // expand the NOT into the and call - OCLFeatureCall newOperand2 = new OCLFeatureCall( - new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), - OclKeyWords.AND, - new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); - - OCLFeatureCall newCall = new OCLFeatureCall(newOperand2, - OclKeyWords.OR, highestOperation.getParameter(0)); - createCNFParts(newCall); - handled = true; - } - } - } + if (!handled) { + CSTSimplifier simplifier = new CSTSimplifier(); + originalConstraint.accept(simplifier); + List trees = simplifier.getTrees(); + if (trees.size() > 0) { + LOGGER.info("Optimized tree"); + for (ConstraintSyntaxTree tree : trees) { + createCNFParts(tree); } - - if (!handled && highestOperation.getParameter(0) instanceof OCLFeatureCall) { - OCLFeatureCall rightSide = (OCLFeatureCall) highestOperation.getParameter(0); - - // if the right side of the call is an AND - if (rightSide.getOperation().equals(OclKeyWords.AND)) { - LOGGER.info("right side is an AND"); - OCLFeatureCall call1 = new OCLFeatureCall(rightSide.getOperand(), - OclKeyWords.OR, highestOperation.getOperand()); - OCLFeatureCall call2 = new OCLFeatureCall(rightSide.getParameter(0), - OclKeyWords.OR, highestOperation.getOperand()); - - createCNFParts(call1); - createCNFParts(call2); - handled = true; - } - - // if the right side of the OR is a NOT - if (!handled && rightSide.getOperation().equals(OclKeyWords.NOT)) { - LOGGER.info("right side is a NOT"); - if (rightSide.getOperand() instanceof OCLFeatureCall) { - OCLFeatureCall negatedOperation = (OCLFeatureCall) rightSide.getOperand(); - - // if the operation inside the NOT is an AND - if (negatedOperation.getOperation().equals(OclKeyWords.AND)) { - LOGGER.info("negated operation is an AND"); - - // expand the NOT into the and call - OCLFeatureCall newOperand2 = new OCLFeatureCall( - new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), - OclKeyWords.OR, - new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); - - OCLFeatureCall newCall = new OCLFeatureCall(newOperand2, - OclKeyWords.OR, highestOperation.getOperand()); - createCNFParts(newCall); - handled = true; - } - - // if the operation inside the NOT is an OR - if (negatedOperation.getOperation().equals(OclKeyWords.OR)) { - LOGGER.info("negated operation is an OR"); - - // expand the NOT into the and call - OCLFeatureCall newOperand2 = new OCLFeatureCall( - new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), - OclKeyWords.AND, - new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); - - OCLFeatureCall newCall = new OCLFeatureCall(highestOperation.getOperand(), - OclKeyWords.OR, newOperand2); - createCNFParts(newCall); - handled = true; - } - } - } - } - - } - } + handled = true; + } + } + +// +// // Handle an OR with an AND at one side +// if (!handled && originalConstraint instanceof OCLFeatureCall) { +// OCLFeatureCall highestOperation = (OCLFeatureCall) originalConstraint; +// +// // if highest operation is an OR +// if (highestOperation.getOperation().equals(OclKeyWords.OR)) { +// LOGGER.info("highest operation is an OR"); +// if (highestOperation.getOperand() instanceof OCLFeatureCall) { +// OCLFeatureCall leftOperation = (OCLFeatureCall) highestOperation.getOperand(); +// +// // if the left side of the OR is an AND +// if (leftOperation.getOperation().equals(OclKeyWords.AND)) { +// LOGGER.info("left side is an and"); +// OCLFeatureCall call1 = new OCLFeatureCall(leftOperation.getOperand(), +// OclKeyWords.OR, highestOperation.getParameter(0)); +// OCLFeatureCall call2 = new OCLFeatureCall(leftOperation.getParameter(0), +// OclKeyWords.OR, highestOperation.getParameter(0)); +// +// createCNFParts(call1); +// createCNFParts(call2); +// handled = true; +// } +// +// // if the left side of the OR is a NOT +// if (!handled && leftOperation.getOperation().equals(OclKeyWords.NOT)) { +// LOGGER.info("left side is a NOT"); +// if (leftOperation.getOperand() instanceof OCLFeatureCall) { +// OCLFeatureCall negatedOperation = (OCLFeatureCall) leftOperation.getOperand(); +// +// // if the operation inside the NOT is an AND +// if (negatedOperation.getOperation().equals(OclKeyWords.AND)) { +// LOGGER.info("negated operation is an AND"); +// +// // expand the NOT into the and call +// OCLFeatureCall newOperand2 = new OCLFeatureCall( +// new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), +// OclKeyWords.OR, +// new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); +// +// OCLFeatureCall newCall = new OCLFeatureCall(newOperand2, +// OclKeyWords.OR, highestOperation.getParameter(0)); +// createCNFParts(newCall); +// handled = true; +// } +// +// // if the operation inside the NOT is an OR +// if (negatedOperation.getOperation().equals(OclKeyWords.OR)) { +// LOGGER.info("negated operation is an OR"); +// +// // expand the NOT into the and call +// OCLFeatureCall newOperand2 = new OCLFeatureCall( +// new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), +// OclKeyWords.AND, +// new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); +// +// OCLFeatureCall newCall = new OCLFeatureCall(newOperand2, +// OclKeyWords.OR, highestOperation.getParameter(0)); +// createCNFParts(newCall); +// handled = true; +// } +// } +// } +// } +// +// if (!handled && highestOperation.getParameter(0) instanceof OCLFeatureCall) { +// OCLFeatureCall rightSide = (OCLFeatureCall) highestOperation.getParameter(0); +// +// // if the right side of the call is an AND +// if (rightSide.getOperation().equals(OclKeyWords.AND)) { +// LOGGER.info("right side is an AND"); +// OCLFeatureCall call1 = new OCLFeatureCall(rightSide.getOperand(), +// OclKeyWords.OR, highestOperation.getOperand()); +// OCLFeatureCall call2 = new OCLFeatureCall(rightSide.getParameter(0), +// OclKeyWords.OR, highestOperation.getOperand()); +// +// createCNFParts(call1); +// createCNFParts(call2); +// handled = true; +// } +// +// // if the right side of the OR is a NOT +// if (!handled && rightSide.getOperation().equals(OclKeyWords.NOT)) { +// LOGGER.info("right side is a NOT"); +// if (rightSide.getOperand() instanceof OCLFeatureCall) { +// OCLFeatureCall negatedOperation = (OCLFeatureCall) rightSide.getOperand(); +// +// // if the operation inside the NOT is an AND +// if (negatedOperation.getOperation().equals(OclKeyWords.AND)) { +// LOGGER.info("negated operation is an AND"); +// +// // expand the NOT into the and call +// OCLFeatureCall newOperand2 = new OCLFeatureCall( +// new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), +// OclKeyWords.OR, +// new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); +// +// OCLFeatureCall newCall = new OCLFeatureCall(newOperand2, +// OclKeyWords.OR, highestOperation.getOperand()); +// createCNFParts(newCall); +// handled = true; +// } +// +// // if the operation inside the NOT is an OR +// if (negatedOperation.getOperation().equals(OclKeyWords.OR)) { +// LOGGER.info("negated operation is an OR"); +// +// // expand the NOT into the and call +// OCLFeatureCall newOperand2 = new OCLFeatureCall( +// new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), +// OclKeyWords.AND, +// new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); +// +// OCLFeatureCall newCall = new OCLFeatureCall(highestOperation.getOperand(), +// OclKeyWords.OR, newOperand2); +// createCNFParts(newCall); +// handled = true; +// } +// } +// } +// } +// +// } +// } if (!handled) { // Stop recursion! - originalConstraint.accept(new DebugConstraintTreeVisitor()); +// originalConstraint.accept(new DebugConstraintTreeVisitor()); // Get an array of all variables in the constraint