001package org.clafer.ast.analysis;
002
003import gnu.trove.set.hash.TIntHashSet;
004import java.util.ArrayList;
005import java.util.HashMap;
006import java.util.List;
007import java.util.Map;
008import java.util.Map.Entry;
009import org.clafer.ast.AstAbstractClafer;
010import org.clafer.ast.AstBoolExpr;
011import org.clafer.ast.AstClafer;
012import org.clafer.ast.AstConcreteClafer;
013import org.clafer.ast.AstConstant;
014import org.clafer.ast.AstConstraint;
015import org.clafer.ast.AstGlobal;
016import org.clafer.ast.AstIntClafer;
017import org.clafer.ast.AstJoin;
018import org.clafer.ast.AstJoinRef;
019import org.clafer.ast.AstRef;
020import org.clafer.ast.AstSetExpr;
021import org.clafer.ast.AstSetTest;
022import org.clafer.ast.AstThis;
023import org.clafer.ast.AstUpcast;
024import org.clafer.ast.AstUtil;
025import org.clafer.collection.FList;
026import static org.clafer.collection.FList.*;
027import org.clafer.collection.Pair;
028import org.clafer.ir.IrDomain;
029import org.clafer.ir.IrUtil;
030import org.clafer.ir.Irs;
031import org.clafer.scope.Scope;
032
033/**
034 *
035 * @author jimmy
036 */
037public class PartialIntAnalyzer implements Analyzer {
038
039    @Override
040    public Analysis analyze(Analysis analysis) {
041        Map<AstRef, IrDomain[]> partialInts = new HashMap<>();
042
043        List<Pair<FList<AstConcreteClafer>, Integer>> assignments = new ArrayList<>();
044        for (AstConstraint constraint : analysis.getConstraints()) {
045            AstClafer clafer = constraint.getContext();
046            if (analysis.isSoft(constraint)) {
047                continue;
048            }
049            try {
050                Pair<FList<AstConcreteClafer>, Integer> assignment = analyze(analysis.getExpr(constraint));
051                FList<AstConcreteClafer> path = assignment.getFst();
052                Integer value = assignment.getSnd();
053                for (AstConcreteClafer concreteClafer : AstUtil.getConcreteSubs(clafer)) {
054                    assignments.add(new Pair<>(snoc(path, concreteClafer), value));
055                }
056            } catch (NotAssignmentException e) {
057                // Only analyze assignments
058            }
059        }
060        AssignmentAutomata automata = new AssignmentAutomata(assignments);
061        for (AstClafer clafer : analysis.getClafers()) {
062            if (clafer.hasRef()) {
063                int scope = analysis.getScope(clafer);
064                IrDomain[] ints = new IrDomain[scope];
065                for (int i = 0; i < scope; i++) {
066                    ints[i] = partialInts(i, clafer.getRef(), automata, analysis);
067                }
068                partialInts.put(clafer.getRef(), ints);
069            }
070        }
071        return analysis.setPartialIntsMap(partialInts);
072    }
073
074    private static IrDomain partialInts(
075            final int id, final AstRef ref, final AssignmentAutomata automata,
076            final Analysis analysis) {
077        TIntHashSet ints = new TIntHashSet();
078        AstClafer source = ref.getSourceType();
079        AstClafer target = ref.getTargetType();
080        if (!partialInts(new int[]{id}, source, automata, analysis, ints)) {
081            Scope scope = analysis.getScope();
082            IrDomain unbounded =
083                    target instanceof AstIntClafer
084                    ? Irs.boundDomain(scope.getIntLow(), scope.getIntHigh())
085                    : Irs.fromToDomain(0, scope.getScope(target));
086            return IrUtil.union(unbounded, Irs.enumDomain(ints));
087        }
088        return Irs.enumDomain(ints);
089    }
090
091    private static boolean partialInts(
092            final int[] ids, final AstClafer clafer, final AssignmentAutomata automata,
093            final Analysis analysis,
094            final TIntHashSet ints) {
095        if (clafer instanceof AstConcreteClafer) {
096            AstConcreteClafer concreteClafer = (AstConcreteClafer) clafer;
097            final Automata transition = automata.transition(concreteClafer);
098            if (transition instanceof FinalAutomata) {
099                ints.add(((FinalAutomata) transition).getValue());
100                return true;
101            }
102            if (transition instanceof AssignmentAutomata) {
103                AssignmentAutomata next = (AssignmentAutomata) transition;
104                assert !AstUtil.isTop(concreteClafer);
105                TIntHashSet parentIds = new TIntHashSet();
106                for (int id : ids) {
107                    parentIds.addAll(analysis.getPartialSolution(clafer).getPossibleParents(id));
108                }
109                return partialInts(parentIds.toArray(), concreteClafer.getParent(),
110                        next, analysis, ints);
111            }
112            return false;
113        }
114        assert clafer instanceof AstAbstractClafer;
115        Map<AstConcreteClafer, TIntHashSet> parentIdsMap = new HashMap<>();
116        for (int id : ids) {
117            Pair<AstConcreteClafer, Integer> concreteId = analysis.getConcreteId(clafer, id);
118            TIntHashSet parentIds = parentIdsMap.get(concreteId.getFst());
119            if (parentIds == null) {
120                parentIds = new TIntHashSet();
121                parentIdsMap.put(concreteId.getFst(), parentIds);
122            }
123            parentIds.add(concreteId.getSnd());
124        }
125        boolean covered = true;
126        for (Entry<AstConcreteClafer, TIntHashSet> entry : parentIdsMap.entrySet()) {
127            covered &= partialInts(entry.getValue().toArray(), entry.getKey(), automata, analysis, ints);
128        }
129        return covered;
130    }
131
132    private static Pair< FList<AstConcreteClafer>, Integer> analyze(
133            AstBoolExpr exp) throws NotAssignmentException {
134        if (exp instanceof AstSetTest) {
135            AstSetTest compare = (AstSetTest) exp;
136            if (AstSetTest.Op.Equal.equals(compare.getOp())) {
137                if (compare.getLeft() instanceof AstJoinRef && compare.getRight() instanceof AstConstant) {
138                    return analyzeEqual((AstJoinRef) compare.getLeft(), (AstConstant) compare.getRight());
139                }
140                if (compare.getRight() instanceof AstJoinRef && compare.getLeft() instanceof AstConstant) {
141                    return analyzeEqual((AstJoinRef) compare.getRight(), (AstConstant) compare.getLeft());
142                }
143            }
144        }
145        throw new NotAssignmentException();
146    }
147
148    private static Pair<FList<AstConcreteClafer>, Integer> analyzeEqual(
149            AstJoinRef exp, AstConstant constant) throws NotAssignmentException {
150        int[] value = constant.getValue();
151        if (value.length == 1) {
152            return new Pair<>(analyze(exp), value[0]);
153        }
154        throw new NotAssignmentException();
155    }
156
157    private static FList<AstConcreteClafer> analyze(AstJoinRef exp) throws NotAssignmentException {
158        return analyze(exp.getDeref());
159    }
160
161    private static FList<AstConcreteClafer> analyze(AstSetExpr exp) throws NotAssignmentException {
162        if (exp instanceof AstUpcast) {
163            return analyze(((AstUpcast) exp).getBase());
164        } else if (exp instanceof AstJoin) {
165            AstJoin join = ((AstJoin) exp);
166            return cons(join.getRight(), analyze(join.getLeft()));
167        } else if (exp instanceof AstThis || exp instanceof AstGlobal) {
168            return empty();
169        }
170        throw new NotAssignmentException();
171    }
172
173    private static interface Automata {
174    }
175
176    private static class AssignmentAutomata implements Automata {
177
178        private final List<Pair<FList<AstConcreteClafer>, Integer>> assignments;
179
180        AssignmentAutomata(List<Pair<FList<AstConcreteClafer>, Integer>> assignments) {
181            this.assignments = assignments;
182        }
183
184        public Automata transition(AstConcreteClafer symbol) {
185            List<Pair<FList<AstConcreteClafer>, Integer>> next = new ArrayList<>();
186
187            for (Pair<FList<AstConcreteClafer>, Integer> assignment : assignments) {
188                FList<AstConcreteClafer> path = assignment.getFst();
189                Integer value = assignment.getSnd();
190                if (symbol.equals(path.getHead())) {
191                    if (path.getTail().isEmpty()) {
192                        return new FinalAutomata(value.intValue());
193                    }
194                    next.add(new Pair<>(path.getTail(), value));
195                }
196            }
197            return next.isEmpty() ? null : new AssignmentAutomata(next);
198        }
199    }
200
201    private static class FinalAutomata implements Automata {
202
203        private final int value;
204
205        FinalAutomata(int value) {
206            this.value = value;
207        }
208
209        int getValue() {
210            return value;
211        }
212    }
213
214    private static class NotAssignmentException extends Exception {
215
216        NotAssignmentException() {
217        }
218    }
219}