001package org.clafer.ir.analysis;
002
003import java.util.ArrayList;
004import java.util.List;
005import org.clafer.ir.IrAnd;
006import org.clafer.ir.IrBoolExpr;
007import org.clafer.ir.IrIfThenElse;
008import org.clafer.ir.IrImplies;
009import org.clafer.ir.IrModule;
010import org.clafer.ir.IrNotImplies;
011import org.clafer.ir.IrRewriter;
012import static org.clafer.ir.Irs.*;
013
014/**
015 *
016 * @author jimmy
017 */
018public class ImplicationFlattener {
019
020    private ImplicationFlattener() {
021    }
022
023    /**
024     * Rewrites expressions so that ands are never directly under the implies
025     * consequent and if-then-else are rewritten to implications. Some analysis
026     * become easier while others become harder.
027     *
028     * @param module the module to flatten
029     * @return the flattened module
030     */
031    public static IrModule flatten(IrModule module) {
032        List<IrBoolExpr> constraints = new ArrayList<>();
033        for (IrBoolExpr constraint : module.getConstraints()) {
034            constraints.add(flattener.rewrite(constraint, null));
035        }
036        return new IrModule().addVariables(module.getVariables()).addConstraints(constraints);
037    }
038    private static final IrRewriter<Void> flattener = new IrRewriter<Void>() {
039        @Override
040        public IrBoolExpr visit(IrImplies ir, Void a) {
041            if (ir.getConsequent() instanceof IrAnd) {
042                IrAnd and = (IrAnd) ir.getConsequent();
043                IrBoolExpr[] inverted = new IrBoolExpr[and.getOperands().length];
044                for (int i = 0; i < inverted.length; i++) {
045                    inverted[i] = rewrite(implies(ir.getAntecedent(), rewrite(and.getOperands()[i], a)), a);
046                }
047                return and(inverted);
048            }
049            return ir;
050        }
051
052        @Override
053        public IrBoolExpr visit(IrNotImplies ir, Void a) {
054            if (ir.getConsequent() instanceof IrAnd) {
055                IrAnd and = (IrAnd) ir.getConsequent();
056                IrBoolExpr[] inverted = new IrBoolExpr[and.getOperands().length];
057                for (int i = 0; i < inverted.length; i++) {
058                    inverted[i] = rewrite(notImplies(ir.getAntecedent(), rewrite(and.getOperands()[i], a)), a);
059                }
060                return and(inverted);
061            }
062            return ir;
063        }
064
065        @Override
066        public IrBoolExpr visit(IrIfThenElse ir, Void a) {
067            return and(
068                    rewrite(implies(ir.getAntecedent(), ir.getConsequent()), a),
069                    rewrite(implies(not(ir.getAntecedent()), ir.getAlternative()), a));
070        }
071    };
072}