source: icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_bddminimization.cpp @ 4736

Last change on this file since 4736 was 4736, checked in by nmedfort, 4 years ago

Initial stages of a simple boolean equation reassociation pass.

File size: 29.7 KB
Line 
1#include "pablo_bddminimization.h"
2#include <pablo/codegenstate.h>
3#include <pablo/builder.hpp>
4#include <stack>
5#include <iostream>
6#include <pablo/printer_pablos.h>
7#include <cudd.h>
8#include <cuddInt.h>
9#include <util.h>
10#include <queue>
11#include <boost/circular_buffer.hpp>
12#include <pablo/optimizers/pablo_simplifier.hpp>
13#include <boost/container/flat_set.hpp>
14#include <boost/container/flat_map.hpp>
15#include <boost/graph/adjacency_list.hpp>
16
17using namespace llvm;
18using namespace boost;
19using namespace boost::container;
20
21namespace pablo {
22
23bool BDDMinimizationPass::optimize(PabloFunction & function, const bool full) {
24    BDDMinimizationPass am;
25    am.eliminateLogicallyEquivalentStatements(function);
26    if (full) {
27        am.simplifyAST(function);
28    }
29    am.shutdown();
30    return Simplifier::optimize(function);
31}
32
33/** ------------------------------------------------------------------------------------------------------------- *
34 * @brief initialize
35 * @param vars the input vars for this program
36 * @param entry the entry block
37 *
38 * Scan through the program to identify any advances and calls then initialize the BDD engine with
39 * the proper variable ordering.
40 ** ------------------------------------------------------------------------------------------------------------- */
41void BDDMinimizationPass::eliminateLogicallyEquivalentStatements(PabloFunction & function) {
42
43    std::stack<Statement *> scope;
44    unsigned variableCount = 0; // number of statements that cannot always be categorized without generating a new variable
45
46    for (const Statement * stmt = function.getEntryBlock().front(); ; ) {
47        while ( stmt ) {
48            if (LLVM_UNLIKELY(isa<If>(stmt) || isa<While>(stmt))) {
49                // Set the next statement to be the first statement of the inner scope and push the
50                // next statement of the current statement into the scope stack.
51                const PabloBlock & nested = isa<If>(stmt) ? cast<If>(stmt)->getBody() : cast<While>(stmt)->getBody();
52                scope.push(stmt->getNextNode());
53                stmt = nested.front();
54                assert (stmt);
55                continue;
56            }
57            switch (stmt->getClassTypeId()) {
58                case PabloAST::ClassTypeId::Assign:
59                case PabloAST::ClassTypeId::Next:
60                case PabloAST::ClassTypeId::Advance:
61                case PabloAST::ClassTypeId::Call:
62                case PabloAST::ClassTypeId::MatchStar:
63                case PabloAST::ClassTypeId::ScanThru:
64                    variableCount++;
65                    break;                                   
66                default:
67                    break;
68            }
69            stmt = stmt->getNextNode();
70        }
71        if (scope.empty()) {
72            break;
73        }
74        stmt = scope.top();
75        scope.pop();
76    }
77
78    // Initialize the BDD engine ...
79    mManager = Cudd_Init(variableCount + function.getNumOfParameters() - function.getNumOfResults(), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
80    Cudd_MakeTreeNode(mManager, 0, function.getNumOfParameters(), MTR_DEFAULT);
81    // Map the predefined 0/1 entries
82    mCharacterizationMap[function.getEntryBlock().createZeroes()] = Zero();
83    mCharacterizationMap[function.getEntryBlock().createOnes()] = One();   
84    // Order the variables so the input Vars are pushed to the end; they ought to
85    // be the most complex to resolve.   
86    for (auto i = 0; i != function.getNumOfParameters(); ++i) {
87        mCharacterizationMap[function.getParameter(i)] = NewVar(function.getParameter(i));
88    }
89
90    SubsitutionMap baseMap;
91    baseMap.insert(Zero(), function.getEntryBlock().createZeroes());
92    baseMap.insert(One(), function.getEntryBlock().createOnes());
93
94    Cudd_SetSiftMaxVar(mManager, 1000000);
95    Cudd_SetSiftMaxSwap(mManager, 1000000000);
96    Cudd_AutodynEnable(mManager, CUDD_REORDER_LAZY_SIFT);
97
98    eliminateLogicallyEquivalentStatements(function.getEntryBlock(), baseMap);
99
100    Cudd_AutodynDisable(mManager);
101}
102
103/** ------------------------------------------------------------------------------------------------------------- *
104 * @brief characterize
105 * @param vars the input vars for this program
106 *
107 * Scan through the program and iteratively compute the BDDs for each statement.
108 ** ------------------------------------------------------------------------------------------------------------- */
109void BDDMinimizationPass::eliminateLogicallyEquivalentStatements(PabloBlock & block, SubsitutionMap & parent) {
110    SubsitutionMap subsitutionMap(&parent);
111    Statement * stmt = block.front();
112    while (stmt) {
113        if (LLVM_UNLIKELY(isa<If>(stmt))) {
114            eliminateLogicallyEquivalentStatements(cast<If>(stmt)->getBody(), subsitutionMap);
115            for (Assign * var : cast<const If>(stmt)->getDefined()) {
116                mCharacterizationMap[var] = NewVar(var);
117            }
118        } else if (LLVM_UNLIKELY(isa<While>(stmt))) {
119            eliminateLogicallyEquivalentStatements(cast<While>(stmt)->getBody(), subsitutionMap);
120            for (Next * var : cast<const While>(stmt)->getVariants()) {
121                mCharacterizationMap[var] = NewVar(var);
122            }
123        } else { // attempt to characterize this statement and replace it if
124            DdNode * bdd = eliminateLogicallyEquivalentStatements(stmt);
125            if (LLVM_LIKELY(!isa<Assign>(stmt) && !isa<Next>(stmt))) {
126                PabloAST * replacement = subsitutionMap[bdd];
127                if (replacement) {
128                    Cudd_RecursiveDeref(mManager, bdd);
129                    stmt = stmt->replaceWith(replacement, false, true);
130                    continue;
131                }
132                subsitutionMap.insert(bdd, stmt);
133            }
134            mCharacterizationMap.insert(std::make_pair(stmt, bdd));
135        }
136        stmt = stmt->getNextNode();
137    }   
138    Cudd_ReduceHeap(mManager, CUDD_REORDER_SIFT, 1);
139}
140
141/** ------------------------------------------------------------------------------------------------------------- *
142 * @brief characterize
143 ** ------------------------------------------------------------------------------------------------------------- */
144inline DdNode * BDDMinimizationPass::eliminateLogicallyEquivalentStatements(const Statement * const stmt) {
145
146    DdNode * bdd = nullptr;
147    // Map our operands to the computed BDDs
148    std::array<DdNode *, 3> input;
149    for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
150        PabloAST * const op = stmt->getOperand(i);
151        if (op == nullptr) {
152            throw std::runtime_error("Statement has Null operand!");
153        }
154        if (LLVM_UNLIKELY(isa<Integer>(op) || isa<String>(op))) {
155            continue;
156        }
157        auto f = mCharacterizationMap.find(op);
158        if (LLVM_UNLIKELY(f == mCharacterizationMap.end())) {
159            throw std::runtime_error("Error in AST: attempted to characterize statement with unknown operand!");
160        }
161        input[i] = f->second;
162    }
163
164    switch (stmt->getClassTypeId()) {
165        case PabloAST::ClassTypeId::Assign:
166        case PabloAST::ClassTypeId::Next:
167            return input[0];
168        case PabloAST::ClassTypeId::And:
169            bdd = And(input[0], input[1]);
170            break;       
171        case PabloAST::ClassTypeId::Or:
172            bdd = Or(input[0], input[1]);
173            break;
174        case PabloAST::ClassTypeId::Xor:
175            bdd = Xor(input[0], input[1]);
176            break;
177        case PabloAST::ClassTypeId::Not:
178            bdd = Not(input[0]);
179            break;
180        case PabloAST::ClassTypeId::Sel:
181            bdd = Ite(input[0], input[1], input[2]);
182            break;
183        case PabloAST::ClassTypeId::MatchStar:
184        case PabloAST::ClassTypeId::ScanThru:
185            if (LLVM_UNLIKELY(isZero(input[1]))) {
186                return Zero();
187            }
188        case PabloAST::ClassTypeId::Advance:
189            if (LLVM_UNLIKELY(isZero(input[0]))) {
190                return Zero();
191            }
192        case PabloAST::ClassTypeId::Call:
193            // TODO: we may have more than one output. Need to fix call class to allow for it.
194            return NewVar(stmt);
195        default:
196            throw std::runtime_error("Unexpected statement type " + stmt->getName()->to_string());
197    }
198
199    Cudd_Ref(bdd);
200
201    if (LLVM_UNLIKELY(noSatisfyingAssignment(bdd))) {
202        Cudd_RecursiveDeref(mManager, bdd);
203        bdd = Zero();
204    }
205
206    return bdd;
207}
208
209/** ------------------------------------------------------------------------------------------------------------- *
210 * @brief simplifyAST
211 ** ------------------------------------------------------------------------------------------------------------- */
212inline void BDDMinimizationPass::simplifyAST(PabloFunction & function) {
213    Terminals terminals;
214    for (unsigned i = 0; i != function.getNumOfResults(); ++i) {
215        terminals.push_back(function.getResult(i));
216    }   
217    Cudd_ReduceHeap(mManager, CUDD_REORDER_EXACT, 1);
218    simplifyAST(function.getEntryBlock(), std::move(terminals));
219}
220
221
222/** ------------------------------------------------------------------------------------------------------------- *
223 * @brief simplifyAST
224 ** ------------------------------------------------------------------------------------------------------------- */
225void BDDMinimizationPass::simplifyAST(PabloBlock & block, Terminals && terminals) {
226
227    for (Statement * stmt : block) {
228        if (isa<If>(stmt)) {
229            Terminals terminals;
230            for (Assign * var : cast<const If>(stmt)->getDefined()) {
231                terminals.push_back(var);
232            }
233            simplifyAST(cast<If>(stmt)->getBody(), std::move(terminals));
234        } else if (isa<While>(stmt)) {
235            Terminals terminals;
236            for (Next * var : cast<const While>(stmt)->getVariants()) {
237                terminals.push_back(var);
238            }
239            simplifyAST(cast<While>(stmt)->getBody(), std::move(terminals));
240        }
241    }
242
243//    // find the variables for this set of terminals
244//    DdNode * careSet = One();
245//    std::queue<Statement *> Q;
246//    for (Statement * term : terminals) {
247//        Q.push(term);
248//    }
249//    flat_set<PabloAST *> visited;
250//    for (;;) {
251//        Statement * stmt = Q.front();
252//        Q.pop();
253//        for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
254//            PabloAST * const op = stmt->getOperand(i);
255//            if (visited.count(op) == 0) {
256//                DdNode * n = mCharacterizationMap[op];
257//                if (Cudd_bddIsVar(mManager, n)) {
258//                    careSet = And(careSet, n);
259//                    Cudd_Ref(careSet);
260//                } else if (isa<Statement>(op)){
261//                    Q.push(cast<Statement>(op));
262//                }
263//                visited.insert(op);
264//            }
265//        }
266//        if (Q.empty()) {
267//            break;
268//        }
269//    }
270
271    flat_set<Statement *> inputs;
272
273    for (Statement * term : terminals) {
274        for (unsigned i = 0; i != term->getNumOperands(); ++i) {
275            if (isa<Statement>(term->getOperand(i))) {
276                inputs.insert(cast<Statement>(term->getOperand(i)));
277            }
278        }
279    }
280
281    for (Statement * input : inputs) {
282
283        DdNode * f = mCharacterizationMap[input]; assert (f);
284        Cudd_Ref(f);
285
286        block.setInsertPoint(input);
287        PabloAST * replacement = simplifyAST(f, block);
288        if (replacement) {
289            input->replaceWith(replacement, false, true);
290        }
291
292        Cudd_RecursiveDeref(mManager, f);
293    }
294}
295
296
297/** ------------------------------------------------------------------------------------------------------------- *
298 * @brief simplifyAST
299 ** ------------------------------------------------------------------------------------------------------------- */
300PabloAST * BDDMinimizationPass::simplifyAST(DdNode * const f, PabloBlock &block) {
301
302    DdNode * g = Cudd_FindEssential(mManager, f);
303
304    if (g && Cudd_SupportSize(mManager, g) > 0) {
305        if (g == f) { // every variable is essential
306            return makeCoverAST(f, block);
307        }
308        Cudd_Ref(g);
309        PabloAST * c0 = makeCoverAST(g, block);
310        if (LLVM_UNLIKELY(c0 == nullptr)) {
311            Cudd_RecursiveDeref(mManager, g);
312            return nullptr;
313        }
314        DdNode * h = Cudd_Cofactor(mManager, f, g);
315        Cudd_Ref(h);
316        PabloAST * c1 = simplifyAST(h, block);
317        if (LLVM_UNLIKELY(c1 == nullptr)) {
318            Cudd_RecursiveDeref(mManager, g);
319            Cudd_RecursiveDeref(mManager, h);
320            cast<Statement>(c0)->eraseFromParent(true);
321            return nullptr;
322        }
323        assert (And(g, h) == f);
324        Cudd_RecursiveDeref(mManager, g);
325        Cudd_RecursiveDeref(mManager, h);
326        return block.createAnd(c0, c1, "e");
327    }
328
329    DdNode ** disjunct = nullptr;
330    int disjuncts = Cudd_bddIterDisjDecomp(mManager, f, &disjunct);
331    assert (disjuncts < 2 || Or(disjunct[0], disjunct[1]) == f);
332
333    DdNode ** conjunct = nullptr;
334    int conjuncts = Cudd_bddIterConjDecomp(mManager, f, &conjunct);
335    assert (conjuncts < 2 || And(conjunct[0], conjunct[1]) == f);
336
337    if (LLVM_LIKELY(disjuncts == 2 && conjuncts == 2)) {
338        if (Cudd_SharingSize(disjunct, 2) > Cudd_SharingSize(conjunct, 2)) {
339            disjuncts = 0;
340        }
341    }
342
343    DdNode * decomp[] = { nullptr, nullptr };
344    if (disjuncts == 2) {
345        memcpy(decomp, disjunct, sizeof(DdNode *) * 2);
346    } else if (conjuncts == 2) {
347        memcpy(decomp, conjunct, sizeof(DdNode *) * 2);
348    }
349
350    FREE(disjunct);
351    FREE(conjunct);
352
353    if ((decomp[0] != decomp[1]) && (decomp[0] != f) && (decomp[1] != f)) {
354
355        Cudd_Ref(decomp[0]);
356        Cudd_Ref(decomp[1]);
357        PabloAST * d0 = simplifyAST(decomp[0], block);
358        Cudd_RecursiveDeref(mManager, decomp[0]);
359        if (LLVM_UNLIKELY(d0 == nullptr)) {
360            Cudd_RecursiveDeref(mManager, decomp[1]);
361            return nullptr;
362        }
363
364        PabloAST * d1 = simplifyAST(decomp[1], block);
365        Cudd_RecursiveDeref(mManager, decomp[1]);
366        if (LLVM_UNLIKELY(d1 == nullptr)) {
367            cast<Statement>(d0)->eraseFromParent(true);
368            return nullptr;
369        }
370
371        if (disjuncts == 2) {
372            return block.createOr(d0, d1, "d");
373        } else {
374            return block.createAnd(d0, d1, "c");
375        }
376    }
377    return makeCoverAST(f, block);
378}
379
380///** ------------------------------------------------------------------------------------------------------------- *
381// * @brief makeCoverAST
382// ** ------------------------------------------------------------------------------------------------------------- */
383//PabloAST * BDDMinimizationPass::makeCover(DdNode * const f, PabloBlock & block) {
384
385//    const auto n = mVariables.size();
386
387//    if (Cudd_DagSize(f) > 100) {
388
389//        int * indices = nullptr;
390//        const int count = Cudd_SupportIndices(mManager, f, &indices);
391//        DdManager * manager = Cudd_Init(count, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
392
393//        std::vector<DdNode *> var(n, nullptr);
394
395//        for (unsigned i = 0; i != count; ++i) {
396//            var[indicies[i]] = Cudd_bddIthVar(manager, i);
397//        }
398
399//        makeCloneOf()
400
401
402
403//        Cudd_Quit(manager);
404//    }
405
406
407
408//}
409
410/** ------------------------------------------------------------------------------------------------------------- *
411 * @brief makeCoverAST
412 ** ------------------------------------------------------------------------------------------------------------- */
413PabloAST * BDDMinimizationPass::makeCoverAST(DdNode * const f, PabloBlock & block) {
414
415    const auto n = mVariables.size();
416    assert (mManager->size == n);
417
418    DdNode * g = f;
419
420    Cudd_Ref(g);
421
422    std::queue<PabloAST *> SQ;
423    circular_buffer<PabloAST *> CQ(n + 1);
424    circular_buffer<PabloAST *> DQ(n + 1);
425
426    int cube[n];
427
428    while (g != Cudd_ReadLogicZero(mManager)) {
429        int length = 0;
430        DdNode * implicant = Cudd_LargestCube(mManager, g, &length);
431        if (LLVM_UNLIKELY(implicant == nullptr)) {
432            Cudd_RecursiveDeref(mManager, g);
433            return nullptr;
434        }
435        Cudd_Ref(implicant);
436        DdNode * prime = Cudd_bddMakePrime(mManager, implicant, f);
437        if (LLVM_UNLIKELY(prime == nullptr)) {
438            Cudd_RecursiveDeref(mManager, g);
439            Cudd_RecursiveDeref(mManager, implicant);
440            return nullptr;
441        }
442        Cudd_Ref(prime);
443        Cudd_RecursiveDeref(mManager, implicant);
444
445        DdNode * h = Cudd_bddAnd(mManager, g, Cudd_Not(prime));
446        if (LLVM_UNLIKELY(h == nullptr)) {
447            Cudd_RecursiveDeref(mManager, g);
448            Cudd_RecursiveDeref(mManager, prime);
449            return nullptr;
450        }
451        Cudd_Ref(h);
452        Cudd_RecursiveDeref(mManager, g);
453
454        g = h;
455        if (LLVM_UNLIKELY(Cudd_BddToCubeArray(mManager, prime, cube) == 0)) {
456            Cudd_RecursiveDeref(mManager, g);
457            Cudd_RecursiveDeref(mManager, prime);
458            return nullptr;
459        }
460        Cudd_RecursiveDeref(mManager, prime);
461
462        assert (DQ.empty() && CQ.empty());
463
464        for (auto i = 0; i != n; ++i) {
465            assert (cube[i] >= 0 && cube[i] <= 2);
466            if (cube[i] == 0) {
467                DQ.push_back(mVariables[i]);
468            } else if (cube[i] == 1) {
469                CQ.push_back(mVariables[i]);
470            }
471        }
472
473        if (LLVM_UNLIKELY(DQ.empty() && CQ.empty())) {
474            throw std::runtime_error("Error! statement contains no elements!");
475        }
476
477        if (DQ.size() > 0) {
478            while (DQ.size() > 1) {
479                PabloAST * v1 = DQ.front(); DQ.pop_front();
480                PabloAST * v2 = DQ.front(); DQ.pop_front();
481                DQ.push_back(block.createOr(v1, v2));
482            }
483            CQ.push_back(block.createNot(DQ.front()));
484            DQ.pop_front();
485        }
486
487        assert (!CQ.empty());
488        while (CQ.size() > 1) {
489            PabloAST * v1 = CQ.front(); CQ.pop_front();
490            PabloAST * v2 = CQ.front(); CQ.pop_front();
491            CQ.push_back(block.createAnd(v1, v2));
492        }
493        SQ.push(CQ.front()); CQ.pop_front();
494    }
495
496    Cudd_RecursiveDeref(mManager, g);
497
498    if (LLVM_UNLIKELY(SQ.empty())) {
499        throw std::runtime_error("Error! statement queue empty!");
500    }
501
502    while (SQ.size() > 1) {
503        PabloAST * v1 = SQ.front(); SQ.pop();
504        PabloAST * v2 = SQ.front(); SQ.pop();
505        SQ.push(block.createOr(v1, v2));
506    }
507    return SQ.front();
508
509}
510
511//DdNode * BDDMinimizationPass::makeCloneOf(DdManager * sourceMgr, DdNode * const f, DdManager * destinationMgr) {
512
513//    const auto n = mVariables.size();
514//    assert (sourceMgr->size == n);
515
516//    std::queue<DdNode *> SQ;
517//    circular_buffer<DdNode *> CQ(n + 1);
518//    circular_buffer<DdNode *> DQ(n + 1);
519
520//    int cube[n];
521
522//    DdNode * g = f;
523
524//    Cudd_Ref(g);
525
526//    Cudd_AutodynEnable(destinationMgr, CUDD_REORDER_SIFT);
527
528//    while (g != Cudd_ReadLogicZero(sourceMgr)) {
529//        int length = 0;
530//        DdNode * implicant = Cudd_LargestCube(sourceMgr, g, &length);
531//        if (LLVM_UNLIKELY(implicant == nullptr)) {
532//            Cudd_RecursiveDeref(sourceMgr, g);
533//            return nullptr;
534//        }
535//        Cudd_Ref(implicant);
536//        DdNode * prime = Cudd_bddMakePrime(sourceMgr, implicant, f);
537//        if (LLVM_UNLIKELY(prime == nullptr)) {
538//            Cudd_RecursiveDeref(sourceMgr, g);
539//            Cudd_RecursiveDeref(sourceMgr, implicant);
540//            return nullptr;
541//        }
542//        Cudd_Ref(prime);
543//        Cudd_RecursiveDeref(sourceMgr, implicant);
544
545//        DdNode * h = Cudd_bddAnd(sourceMgr, g, Cudd_Not(prime));
546//        if (LLVM_UNLIKELY(h == nullptr)) {
547//            Cudd_RecursiveDeref(sourceMgr, g);
548//            Cudd_RecursiveDeref(sourceMgr, prime);
549//            return nullptr;
550//        }
551//        Cudd_Ref(h);
552//        Cudd_RecursiveDeref(sourceMgr, g);
553
554//        g = h;
555//        if (LLVM_UNLIKELY(Cudd_BddToCubeArray(sourceMgr, prime, cube) == 0)) {
556//            Cudd_RecursiveDeref(sourceMgr, g);
557//            Cudd_RecursiveDeref(sourceMgr, prime);
558//            return nullptr;
559//        }
560//        Cudd_RecursiveDeref(sourceMgr, prime);
561
562//        assert (DQ.empty() && CQ.empty());
563
564//        for (auto i = 0; i != n; ++i) {
565//            assert (cube[i] >= 0 && cube[i] <= 2);
566//            if (cube[i] == 0) {
567//                DQ.push_back(var[i]);
568//            } else if (cube[i] == 1) {
569//                CQ.push_back(var[i]);
570//            }
571//        }
572
573//        if (LLVM_UNLIKELY(DQ.empty() && CQ.empty())) {
574//            throw std::runtime_error("Error! statement contains no elements!");
575//        }
576
577//        if (DQ.size() > 0) {
578//            while (DQ.size() > 1) {
579//                PabloAST * v1 = DQ.front(); DQ.pop_front();
580//                PabloAST * v2 = DQ.front(); DQ.pop_front();
581//                DQ.push_back(Cudd_bddOr(destinationMgr, v1, v2));
582//            }
583//            CQ.push_back(Cudd_Not(DQ.front()));
584//            DQ.pop_front();
585//        }
586
587//        assert (!CQ.empty());
588//        while (CQ.size() > 1) {
589//            PabloAST * v1 = CQ.front(); CQ.pop_front();
590//            PabloAST * v2 = CQ.front(); CQ.pop_front();
591//            CQ.push_back(Cudd_bddOr(destinationMgr, v1, v2));
592//        }
593//        SQ.push(CQ.front()); CQ.pop_front();
594//    }
595
596//    Cudd_RecursiveDeref(sourceMgr, g);
597
598//    if (LLVM_UNLIKELY(SQ.empty())) {
599//        throw std::runtime_error("Error! statement queue empty!");
600//    }
601
602//    while (SQ.size() > 1) {
603//        PabloAST * v1 = SQ.front(); SQ.pop();
604//        PabloAST * v2 = SQ.front(); SQ.pop();
605//        SQ.push(Cudd_bddOr(destinationMgr, v1, v2));
606//    }
607
608//    Cudd_ReduceHeap(destinationMgr, CUDD_REORDER_EXACT, 0);
609
610//    return SQ.front();
611
612//}
613
614///** ------------------------------------------------------------------------------------------------------------- *
615// * @brief simplifyAST
616// ** ------------------------------------------------------------------------------------------------------------- */
617//PabloAST * BDDMinimizationPass::simplifyAST(DdNode * const f, PabloBlock &block) {
618
619//    DdNode * g = Cudd_FindEssential(mManager, f);
620
621//    if (g && Cudd_SupportSize(mManager, g) > 0) {
622//        if (g == f) { // every variable is essential
623//            return makeCoverAST(f, block);
624//        }
625//        Cudd_Ref(g);
626//        PabloAST * c0 = makeCoverAST(g, block);
627//        if (LLVM_UNLIKELY(c0 == nullptr)) {
628//            Cudd_RecursiveDeref(mManager, g);
629//            return nullptr;
630//        }
631//        DdNode * h = Cudd_Cofactor(mManager, f, g);
632//        Cudd_Ref(h);
633//        PabloAST * c1 = simplifyAST(h, block);
634//        if (LLVM_UNLIKELY(c1 == nullptr)) {
635//            Cudd_RecursiveDeref(mManager, g);
636//            Cudd_RecursiveDeref(mManager, h);
637//            cast<Statement>(c0)->eraseFromParent(true);
638//            return nullptr;
639//        }
640//        assert (And(g, h) == f);
641//        Cudd_RecursiveDeref(mManager, g);
642//        Cudd_RecursiveDeref(mManager, h);
643//        return block.createAnd(c0, c1, "e");
644//    }
645
646//    DdNode ** disjunct = nullptr;
647//    int disjuncts = Cudd_bddIterDisjDecomp(mManager, f, &disjunct);
648//    assert (disjuncts < 2 || Or(disjunct[0], disjunct[1]) == f);
649
650//    DdNode ** conjunct = nullptr;
651//    int conjuncts = Cudd_bddIterConjDecomp(mManager, f, &conjunct);
652//    assert (conjuncts < 2 || And(conjunct[0], conjunct[1]) == f);
653
654//    if (LLVM_LIKELY(disjuncts == 2 && conjuncts == 2)) {
655//        if (Cudd_SharingSize(disjunct, 2) > Cudd_SharingSize(conjunct, 2)) {
656//            disjuncts = 0;
657//        }
658//    }
659
660//    DdNode * decomp[] = { nullptr, nullptr };
661//    if (disjuncts == 2) {
662//        memcpy(decomp, disjunct, sizeof(DdNode *) * 2);
663//    } else if (conjuncts == 2) {
664//        memcpy(decomp, conjunct, sizeof(DdNode *) * 2);
665//    }
666
667//    FREE(disjunct);
668//    FREE(conjunct);
669
670//    if ((decomp[0] != decomp[1]) && (decomp[0] != f) && (decomp[1] != f)) {
671//        Cudd_Ref(decomp[0]);
672//        Cudd_Ref(decomp[1]);
673//        PabloAST * d0 = simplifyAST(decomp[0], block);
674//        Cudd_RecursiveDeref(mManager, decomp[0]);
675//        if (LLVM_UNLIKELY(d0 == nullptr)) {
676//            Cudd_RecursiveDeref(mManager, decomp[1]);
677//            return nullptr;
678//        }
679
680//        PabloAST * d1 = simplifyAST(decomp[1], block);
681//        Cudd_RecursiveDeref(mManager, decomp[1]);
682//        if (LLVM_UNLIKELY(d1 == nullptr)) {
683//            cast<Statement>(d0)->eraseFromParent(true);
684//            return nullptr;
685//        }
686
687//        if (disjuncts == 2) {
688//            return block.createOr(d0, d1, "t");
689//        } else {
690//            return block.createAnd(d0, d1, "t");
691//        }
692//    }
693//    return makeCoverAST(f, block);
694//}
695
696///** ------------------------------------------------------------------------------------------------------------- *
697// * @brief makeCoverAST
698// ** ------------------------------------------------------------------------------------------------------------- */
699//PabloAST * BDDMinimizationPass::makeCoverAST(DdNode * const f, PabloBlock & block) {
700
701//    std::queue<PabloAST *> SQ;
702
703//    const auto n = mVariables.size();
704//    circular_buffer<PabloAST *> CQ(n + 1);
705//    circular_buffer<PabloAST *> DQ(n + 1);
706
707//    assert (mManager->size == n);
708
709//    int cube[n];
710
711//    std::cout << std::endl;
712
713//    Cudd_PrintMinterm(mManager, f);
714
715//    DdNode * g = f;
716
717//    Cudd_Ref(g);
718
719//    PabloBuilder builder(block);
720
721//    while (g != Cudd_ReadLogicZero(mManager)) {
722//        int length = 0;
723//        DdNode * implicant = Cudd_LargestCube(mManager, g, &length);
724//        if (LLVM_UNLIKELY(implicant == nullptr)) {
725//            Cudd_RecursiveDeref(mManager, g);
726//            return nullptr;
727//        }
728//        Cudd_Ref(implicant);
729//        DdNode * prime = Cudd_bddMakePrime(mManager, implicant, f);
730//        if (LLVM_UNLIKELY(prime == nullptr)) {
731//            Cudd_RecursiveDeref(mManager, g);
732//            Cudd_RecursiveDeref(mManager, implicant);
733//            return nullptr;
734//        }
735//        Cudd_Ref(prime);
736//        Cudd_RecursiveDeref(mManager, implicant);
737
738//        DdNode * h = Cudd_bddAnd(mManager, g, Cudd_Not(prime));
739//        if (LLVM_UNLIKELY(h == nullptr)) {
740//            Cudd_RecursiveDeref(mManager, g);
741//            Cudd_RecursiveDeref(mManager, prime);
742//            return nullptr;
743//        }
744//        Cudd_Ref(h);
745//        Cudd_RecursiveDeref(mManager, g);
746
747//        g = h;
748//        if (LLVM_UNLIKELY(Cudd_BddToCubeArray(mManager, prime, cube) == 0)) {
749//            Cudd_RecursiveDeref(mManager, g);
750//            Cudd_RecursiveDeref(mManager, prime);
751//            return nullptr;
752//        }
753//        Cudd_RecursiveDeref(mManager, prime);
754
755//        assert (DQ.empty() && CQ.empty());
756
757//        for (auto i = 0; i != n; ++i) {
758//            assert (cube[i] >= 0 && cube[i] <= 2);
759//            if (cube[i] == 0) {
760//                DQ.push_back(mVariables[i]);
761//                CQ.push_back(builder.createOnes());
762//            } else if (cube[i] == 1) {
763//                CQ.push_back(mVariables[i]);
764//                DQ.push_back(builder.createZeroes());
765//            }
766//        }
767
768//        if (LLVM_UNLIKELY(DQ.empty() && CQ.empty())) {
769//            throw std::runtime_error("Error! statement contains no elements!");
770//        }
771
772//        if (DQ.size() > 0) {
773//            while (DQ.size() > 1) {
774//                PabloAST * v1 = DQ.front(); DQ.pop_front();
775//                PabloAST * v2 = DQ.front(); DQ.pop_front();
776//                DQ.push_back(builder.createOr(v1, v2));
777//            }
778//            CQ.push_back(builder.createNot(DQ.front()));
779//            DQ.pop_front();
780//        }
781
782//        assert (!CQ.empty());
783//        while (CQ.size() > 1) {
784//            PabloAST * v1 = CQ.front(); CQ.pop_front();
785//            PabloAST * v2 = CQ.front(); CQ.pop_front();
786//            CQ.push_back(builder.createAnd(v1, v2));
787//        }
788//        SQ.push(CQ.front()); CQ.pop_front();
789//    }
790//    Cudd_RecursiveDeref(mManager, g);
791
792//    if (LLVM_UNLIKELY(SQ.empty())) {
793//        throw std::runtime_error("Error! statement queue empty!");
794//    }
795
796//    while (SQ.size() > 1) {
797//        PabloAST * v1 = SQ.front(); SQ.pop();
798//        PabloAST * v2 = SQ.front(); SQ.pop();
799//        SQ.push(builder.createOr(v1, v2));
800//    }
801//    return SQ.front();
802//}
803
804/** ------------------------------------------------------------------------------------------------------------- *
805 * @brief CUDD wrappers
806 ** ------------------------------------------------------------------------------------------------------------- */
807
808inline DdNode * BDDMinimizationPass::Zero() const {
809    return Cudd_ReadLogicZero(mManager);
810}
811
812inline DdNode * BDDMinimizationPass::One() const {
813    return Cudd_ReadOne(mManager);
814}
815
816inline DdNode * BDDMinimizationPass::NewVar(const PabloAST * expr) {
817    DdNode * var = Cudd_bddIthVar(mManager, mVariables.size());
818    mVariables.push_back(const_cast<PabloAST *>(expr));
819    return var;
820}
821
822inline bool BDDMinimizationPass::isZero(DdNode * const x) const {
823    return x == Zero();
824}
825
826inline DdNode * BDDMinimizationPass::And(DdNode * const x, DdNode * const y) {
827    DdNode * r = Cudd_bddAnd(mManager, x, y);
828    return r;
829}
830
831inline DdNode * BDDMinimizationPass::Intersect(DdNode * const x, DdNode * const y) {
832    DdNode * r = Cudd_bddIntersect(mManager, x, y); Cudd_Ref(r);
833    return r;
834}
835
836inline DdNode * BDDMinimizationPass::Or(DdNode * const x, DdNode * const y) {
837    DdNode * r = Cudd_bddOr(mManager, x, y);
838    return r;
839}
840
841inline DdNode * BDDMinimizationPass::Xor(DdNode * const x, DdNode * const y) {
842    DdNode * r = Cudd_bddXor(mManager, x, y);
843    return r;
844}
845
846inline DdNode * BDDMinimizationPass::Not(DdNode * const x) const {
847    return Cudd_Not(x);
848}
849
850inline DdNode * BDDMinimizationPass::Ite(DdNode * const x, DdNode * const y, DdNode * const z) {
851    DdNode * r = Cudd_bddIte(mManager, x, y, z);
852    return r;
853}
854
855inline bool BDDMinimizationPass::noSatisfyingAssignment(DdNode * const x) {
856    return Cudd_bddLeq(mManager, x, Zero());
857}
858
859inline void BDDMinimizationPass::shutdown() {
860    Cudd_Quit(mManager);
861    mCharacterizationMap.clear();
862    mVariables.clear();
863}
864
865} // end of namespace pablo
866
Note: See TracBrowser for help on using the repository browser.