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

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

More minimization work.

File size: 24.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    if (full) {
26        am.simplifyAST(function);
27    }
28    am.eliminateLogicallyEquivalentStatements(function);
29    return Simplifier::optimize(function);
30}
31
32/** ------------------------------------------------------------------------------------------------------------- *
33 * @brief initialize
34 * @param vars the input vars for this program
35 * @param entry the entry block
36 *
37 * Scan through the program to identify any advances and calls then initialize the BDD engine with
38 * the proper variable ordering.
39 ** ------------------------------------------------------------------------------------------------------------- */
40void BDDMinimizationPass::eliminateLogicallyEquivalentStatements(PabloFunction & function) {
41
42    std::stack<Statement *> scope;
43    unsigned variableCount = 0; // number of statements that cannot always be categorized without generating a new variable
44
45    for (const Statement * stmt = function.getEntryBlock().front(); ; ) {
46        while ( stmt ) {
47            if (LLVM_UNLIKELY(isa<If>(stmt) || isa<While>(stmt))) {
48                // Set the next statement to be the first statement of the inner scope and push the
49                // next statement of the current statement into the scope stack.
50                const PabloBlock & nested = isa<If>(stmt) ? cast<If>(stmt)->getBody() : cast<While>(stmt)->getBody();
51                scope.push(stmt->getNextNode());
52                stmt = nested.front();
53                assert (stmt);
54                continue;
55            }
56            switch (stmt->getClassTypeId()) {
57                case PabloAST::ClassTypeId::Assign:
58                case PabloAST::ClassTypeId::Next:
59                case PabloAST::ClassTypeId::Advance:
60                case PabloAST::ClassTypeId::Call:
61                case PabloAST::ClassTypeId::MatchStar:
62                case PabloAST::ClassTypeId::ScanThru:
63                    variableCount++;
64                    break;                                   
65                default:
66                    break;
67            }
68            stmt = stmt->getNextNode();
69        }
70        if (scope.empty()) {
71            break;
72        }
73        stmt = scope.top();
74        scope.pop();
75    }
76
77    // Initialize the BDD engine ...
78    mManager = Cudd_Init(variableCount + function.getNumOfParameters() - function.getNumOfResults(), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
79    Cudd_MakeTreeNode(mManager, 0, function.getNumOfParameters(), MTR_DEFAULT);
80    // Map the predefined 0/1 entries
81    mCharacterizationMap[function.getEntryBlock().createZeroes()] = Zero();
82    mCharacterizationMap[function.getEntryBlock().createOnes()] = One();   
83    // Order the variables so the input Vars are pushed to the end; they ought to
84    // be the most complex to resolve.   
85    for (auto i = 0; i != function.getNumOfParameters(); ++i) {
86        mCharacterizationMap[function.getParameter(i)] = NewVar(function.getParameter(i));
87    }
88
89    SubsitutionMap baseMap;
90    baseMap.insert(Zero(), function.getEntryBlock().createZeroes());
91    baseMap.insert(One(), function.getEntryBlock().createOnes());
92
93    Cudd_AutodynEnable(mManager, CUDD_REORDER_LAZY_SIFT);
94
95    eliminateLogicallyEquivalentStatements(function.getEntryBlock(), baseMap);
96
97    Cudd_Quit(mManager);
98    mCharacterizationMap.clear();
99}
100
101/** ------------------------------------------------------------------------------------------------------------- *
102 * @brief characterize
103 * @param vars the input vars for this program
104 *
105 * Scan through the program and iteratively compute the BDDs for each statement.
106 ** ------------------------------------------------------------------------------------------------------------- */
107void BDDMinimizationPass::eliminateLogicallyEquivalentStatements(PabloBlock & block, SubsitutionMap & parent) {
108    SubsitutionMap subsitutionMap(&parent);
109    Statement * stmt = block.front();
110
111    while (stmt) {
112        if (LLVM_UNLIKELY(isa<If>(stmt))) {
113            eliminateLogicallyEquivalentStatements(cast<If>(stmt)->getBody(), subsitutionMap);
114        } else if (LLVM_UNLIKELY(isa<While>(stmt))) {
115            eliminateLogicallyEquivalentStatements(cast<While>(stmt)->getBody(), subsitutionMap);
116        } else { // attempt to characterize this statement and replace it if
117            DdNode * bdd = eliminateLogicallyEquivalentStatements(stmt);
118            if (LLVM_LIKELY(!isa<Assign>(stmt) && !isa<Next>(stmt))) {
119                PabloAST * replacement = subsitutionMap[bdd];
120                if (replacement) {
121                    Cudd_RecursiveDeref(mManager, bdd);
122                    stmt = stmt->replaceWith(replacement, false, true);
123                    continue;
124                }
125                subsitutionMap.insert(bdd, stmt);
126            }
127            mCharacterizationMap.insert(std::make_pair(stmt, bdd));
128        }
129        stmt = stmt->getNextNode();
130    }
131    Cudd_ReduceHeap(mManager, CUDD_REORDER_SIFT, 0);
132}
133
134/** ------------------------------------------------------------------------------------------------------------- *
135 * @brief characterize
136 ** ------------------------------------------------------------------------------------------------------------- */
137inline DdNode * BDDMinimizationPass::eliminateLogicallyEquivalentStatements(const Statement * const stmt) {
138
139    DdNode * bdd = nullptr;
140    // Map our operands to the computed BDDs
141    std::array<DdNode *, 3> input;
142    for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
143        PabloAST * const op = stmt->getOperand(i);
144        if (op == nullptr) {
145            throw std::runtime_error("Statement has Null operand!");
146        }
147        if (LLVM_UNLIKELY(isa<Integer>(op) || isa<String>(op))) {
148            continue;
149        }
150        auto f = mCharacterizationMap.find(op);
151        if (LLVM_UNLIKELY(f == mCharacterizationMap.end())) {
152            throw std::runtime_error("Error in AST: attempted to characterize statement with unknown operand!");
153        }
154        input[i] = f->second;
155    }
156
157    switch (stmt->getClassTypeId()) {
158        case PabloAST::ClassTypeId::Assign:
159        case PabloAST::ClassTypeId::Next:
160            return input[0];
161        case PabloAST::ClassTypeId::And:
162            bdd = And(input[0], input[1]);
163            break;       
164        case PabloAST::ClassTypeId::Or:
165            bdd = Or(input[0], input[1]);
166            break;
167        case PabloAST::ClassTypeId::Xor:
168            bdd = Xor(input[0], input[1]);
169            break;
170        case PabloAST::ClassTypeId::Not:
171            bdd = Not(input[0]);
172            break;
173        case PabloAST::ClassTypeId::Sel:
174            bdd = Ite(input[0], input[1], input[2]);
175            break;
176        case PabloAST::ClassTypeId::Call:
177            // TODO: we may have more than one output. Need to fix call class to allow for it.
178        case PabloAST::ClassTypeId::Advance:
179        case PabloAST::ClassTypeId::MatchStar:
180        case PabloAST::ClassTypeId::ScanThru:
181            return NewVar(stmt);
182        default:
183            throw std::runtime_error("Unexpected statement type " + stmt->getName()->to_string());
184    }
185
186    Cudd_Ref(bdd);
187
188    if (LLVM_UNLIKELY(noSatisfyingAssignment(bdd))) {
189        Cudd_RecursiveDeref(mManager, bdd);
190        bdd = Zero();
191    }
192
193    return bdd;
194}
195
196/** ------------------------------------------------------------------------------------------------------------- *
197 * @brief simplifyAST
198 ** ------------------------------------------------------------------------------------------------------------- */
199inline void BDDMinimizationPass::simplifyAST(PabloFunction & function) {
200    Terminals terminals;
201    for (unsigned i = 0; i != function.getNumOfResults(); ++i) {
202        terminals.push_back(function.getResult(i));
203    }
204    simplifyAST(function.getEntryBlock(), std::move(terminals));
205}
206
207/** ------------------------------------------------------------------------------------------------------------- *
208 * @brief promoteSimpleInputDerivationsToAssigns
209 ** ------------------------------------------------------------------------------------------------------------- */
210inline void BDDMinimizationPass::promoteSimpleInputDerivationsToAssigns(PabloFunction & function) {
211
212    using Graph = adjacency_list<hash_setS, vecS, bidirectionalS, PabloAST *>;
213    using Vertex = Graph::vertex_descriptor;
214
215    Graph G;
216    flat_map<PabloAST *, Vertex> M;
217    std::queue<Vertex> Q;
218    for (unsigned i = 0; i != function.getNumOfParameters(); ++i) {
219        PabloAST * var = function.getParameter(i);
220        const Vertex u = add_vertex(var, G);
221        Q.push(u);
222        M[var] = u;
223    }
224
225    for (;;) {
226        const Vertex u = Q.front(); Q.pop();
227        for (PabloAST * user : G[u]->users()) {
228            auto f = M.find(user);
229            Vertex v = 0;
230            if (f == M.end()) {
231                v = add_vertex(user, G);
232                switch (user->getClassTypeId()) {
233                    case PabloAST::ClassTypeId::And:
234                    case PabloAST::ClassTypeId::Or:
235                    case PabloAST::ClassTypeId::Not:
236                    case PabloAST::ClassTypeId::Xor:
237                    case PabloAST::ClassTypeId::Sel:
238                        Q.push(v);
239                    default:
240                        M[user] = v;
241                }
242            } else {
243                v = f->second;
244            }
245            add_edge(u, v, G);
246        }
247
248        if (Q.empty()) {
249            break;
250        }
251    }
252
253    flat_set<Statement *> promotions;
254
255    for (Vertex u : make_iterator_range(vertices(G))) {
256        if (out_degree(u, G) == 0) {
257            Statement * stmt = cast<Statement>(G[u]);
258            if (isa<Assign>(stmt)) {
259                continue;
260            }
261            for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
262                if (Statement * expr = dyn_cast<Statement>(stmt->getOperand(i))) {
263                    promotions.insert(expr);
264                }
265            }
266        }
267    }
268
269    for (Statement * promoted : promotions) {
270        PabloBlock * block = promoted->getParent();
271        block->setInsertPoint(promoted);
272        Assign * replacement = block->createAssign("t", promoted);
273        promoted->replaceAllUsesWith(replacement);
274    }
275
276    raw_os_ostream out(std::cerr);
277    PabloPrinter::print(function.getEntryBlock().statements(), out);
278    out << "**************************************\n";
279    out.flush();
280}
281
282
283/** ------------------------------------------------------------------------------------------------------------- *
284 * @brief isSimplifiable
285 ** ------------------------------------------------------------------------------------------------------------- */
286inline bool isSimplifiable(const PabloAST * const expr, const PabloBlock * const pb) {
287    switch (expr->getClassTypeId()) {
288        case PabloAST::ClassTypeId::And:
289        case PabloAST::ClassTypeId::Or:
290        case PabloAST::ClassTypeId::Not:
291//        case PabloAST::ClassTypeId::Sel:
292            return cast<Statement>(expr)->getParent() == pb;
293        default:
294            return false;
295    }
296}
297
298/** ------------------------------------------------------------------------------------------------------------- *
299 * @brief simplifyAST
300 ** ------------------------------------------------------------------------------------------------------------- */
301void BDDMinimizationPass::simplifyAST(PabloBlock & block, Terminals && terminals) {
302
303    for (Statement * stmt : block) {
304        if (isa<If>(stmt)) {
305            Terminals terminals;
306            for (Assign * var : cast<const If>(stmt)->getDefined()) {
307                terminals.push_back(var);
308            }
309            simplifyAST(cast<If>(stmt)->getBody(), std::move(terminals));
310//            for (Assign * var : cast<const If>(stmt)->getDefined()) {
311//                block.record(var);
312//            }
313//            continue;
314        } else if (isa<While>(stmt)) {
315            Terminals terminals;
316            for (Next * var : cast<const While>(stmt)->getVariants()) {
317                terminals.push_back(var);
318            }
319            simplifyAST(cast<While>(stmt)->getBody(), std::move(terminals));
320//            for (Next * var : cast<const While>(stmt)->getVariants()) {
321//                block.record(var);
322//            }
323//            continue;
324        }
325        // block.record(stmt);
326    }
327
328    for (;;) {
329
330        flat_set<Statement *> inputs;
331        for (Statement * term : terminals) {
332            for (unsigned i = 0; i != term->getNumOperands(); ++i) {
333                if (isSimplifiable(term->getOperand(i), term->getParent())) {
334                    inputs.insert(cast<Statement>(term->getOperand(i)));
335                }
336            }
337        }
338
339        if (inputs.empty()) {
340            break;
341        }
342
343        std::queue<Statement *> Q;
344        for (Statement * term : inputs) {
345            Q.push(term);
346        }
347
348        flat_set<PabloAST *> visited;
349        flat_set<PabloAST *> variables;
350        // find the variables for this set of terminals
351        for (;;) {
352            Statement * stmt = Q.front();
353            Q.pop();
354            for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
355                if (visited.count(stmt->getOperand(i)) == 0) {
356                    if (isSimplifiable(stmt->getOperand(i), stmt->getParent())) {
357                        Q.push(cast<Statement>(stmt->getOperand(i)));
358                    } else {
359                        variables.insert(stmt->getOperand(i));
360                    }
361                    visited.insert(stmt->getOperand(i));
362                }
363            }
364            if (Q.empty()) {
365                break;
366            }
367        }
368
369        mVariables.clear();
370        mManager = Cudd_Init(variables.size(), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
371        Cudd_AutodynEnable(mManager, CUDD_REORDER_LAZY_SIFT);
372        for (PabloAST * var : variables) {
373            mCharacterizationMap.insert(std::make_pair(var, Cudd_bddIthVar(mManager, mVariables.size())));
374            mVariables.push_back(var);
375        }
376
377
378        std::vector<DdNode *> nodes;
379        for (PabloAST * term : inputs) {
380            nodes.push_back(characterizeTerminal(term));
381        }
382        Cudd_AutodynDisable(mManager);
383        Cudd_ReduceHeap(mManager, CUDD_REORDER_SIFT, 0);
384
385        visited.clear();
386        for (Statement * input : inputs) {
387            DdNode * const f = mCharacterizationMap[input]; assert (f);
388            Cudd_Ref(f);
389            block.setInsertPoint(input);
390            PabloBuilder builder(block);
391            PabloAST * replacement = simplifyAST(f, builder);
392            if (replacement) {
393                input->replaceWith(replacement, false, true);
394            }
395            Cudd_RecursiveDeref(mManager, f);
396        }
397
398        Cudd_Quit(mManager);
399
400        mCharacterizationMap.clear();
401
402        // Now clear our terminals and test whether we can process another layer within this block
403        terminals.clear();
404        for (PabloAST * var : variables) {
405            if (LLVM_LIKELY(isa<Statement>(var) && cast<Statement>(var)->getParent() == &block)) {
406                terminals.push_back(cast<Statement>(var));
407            }
408        }
409
410        if (terminals.empty()) {
411            break;
412        }
413
414    }
415
416}
417
418/** ------------------------------------------------------------------------------------------------------------- *
419 * @brief characterizeTerminal
420 ** ------------------------------------------------------------------------------------------------------------- */
421DdNode * BDDMinimizationPass::characterizeTerminal(PabloAST * expr) {
422    const auto f = mCharacterizationMap.find(expr);
423    if (f != mCharacterizationMap.end()) {
424        return f->second;
425    }
426    std::array<DdNode *, 3> input;
427    for (unsigned i = 0; i != cast<Statement>(expr)->getNumOperands(); ++i) {
428        input[i] = characterizeTerminal(cast<Statement>(expr)->getOperand(i)); assert (input[i]);
429    }
430    DdNode * bdd = nullptr;
431    switch (expr->getClassTypeId()) {
432        case PabloAST::ClassTypeId::And:
433            bdd = And(input[0], input[1]);
434            break;
435        case PabloAST::ClassTypeId::Or:
436            bdd = Or(input[0], input[1]);
437            break;
438        case PabloAST::ClassTypeId::Not:
439            bdd = Not(input[0]);
440            break;
441//        case PabloAST::ClassTypeId::Sel:
442//            bdd = Ite(input[0], input[1], input[2]);
443//            break;
444        default:
445            return nullptr;
446    }
447    Cudd_Ref(bdd);
448    mCharacterizationMap.insert(std::make_pair(expr, bdd));
449    return bdd;
450}
451
452/** ------------------------------------------------------------------------------------------------------------- *
453 * @brief simplifyAST
454 ** ------------------------------------------------------------------------------------------------------------- */
455PabloAST * BDDMinimizationPass::simplifyAST(DdNode * const f, PabloBuilder &block) {
456    assert (!noSatisfyingAssignment(f));
457    DdNode * g = Cudd_FindEssential(mManager, f);
458    if (g && Cudd_SupportSize(mManager, g) > 0) {
459        if (g == f) { // every variable is essential
460            return makeCoverAST(f, block);
461        }
462        Cudd_Ref(g);
463        PabloAST * c0 = makeCoverAST(g, block);
464        if (LLVM_UNLIKELY(c0 == nullptr)) {
465            Cudd_RecursiveDeref(mManager, g);
466            return nullptr;
467        }
468        DdNode * h = Cudd_Cofactor(mManager, f, g);
469        Cudd_Ref(h);
470        PabloAST * c1 = simplifyAST(h, block);
471        if (LLVM_UNLIKELY(c1 == nullptr)) {
472            Cudd_RecursiveDeref(mManager, g);
473            Cudd_RecursiveDeref(mManager, h);
474            cast<Statement>(c0)->eraseFromParent(true);
475            return nullptr;
476        }
477        assert (And(g, h) == f);
478        Cudd_RecursiveDeref(mManager, g);
479        Cudd_RecursiveDeref(mManager, h);
480        return block.createAnd(c0, c1, "t");
481    }
482
483    DdNode ** disjunct = nullptr;
484    int disjuncts = Cudd_bddIterDisjDecomp(mManager, f, &disjunct);
485    assert (disjuncts < 2 || Or(disjunct[0], disjunct[1]) == f);
486
487    DdNode ** conjunct = nullptr;
488    int conjuncts = Cudd_bddIterConjDecomp(mManager, f, &conjunct);
489    assert (conjuncts < 2 || And(conjunct[0], conjunct[1]) == f);
490
491    if (LLVM_LIKELY(disjuncts == 2 && conjuncts == 2)) {
492        if (Cudd_SharingSize(disjunct, 2) > Cudd_SharingSize(conjunct, 2)) {
493            disjuncts = 0;
494        }
495    }
496
497    DdNode * decomp[] = { nullptr, nullptr };
498    if (disjuncts == 2) {
499        memcpy(decomp, disjunct, sizeof(DdNode *) * 2);
500    } else if (conjuncts == 2) {
501        memcpy(decomp, conjunct, sizeof(DdNode *) * 2);
502    }
503
504    FREE(disjunct);
505    FREE(conjunct);
506
507    if ((decomp[0] != decomp[1]) && (decomp[0] != f) && (decomp[1] != f)) {
508        Cudd_Ref(decomp[0]);
509        Cudd_Ref(decomp[1]);
510        PabloAST * d0 = simplifyAST(decomp[0], block);
511        Cudd_RecursiveDeref(mManager, decomp[0]);
512        if (LLVM_UNLIKELY(d0 == nullptr)) {
513            Cudd_RecursiveDeref(mManager, decomp[1]);
514            return nullptr;
515        }
516
517        PabloAST * d1 = simplifyAST(decomp[1], block);
518        Cudd_RecursiveDeref(mManager, decomp[1]);
519        if (LLVM_UNLIKELY(d1 == nullptr)) {
520            cast<Statement>(d0)->eraseFromParent(true);
521            return nullptr;
522        }
523
524        if (disjuncts == 2) {
525            return block.createOr(d0, d1, "t");
526        } else {
527            return block.createAnd(d0, d1, "t");
528        }
529    }
530    return makeCoverAST(f, block);
531}
532
533/** ------------------------------------------------------------------------------------------------------------- *
534 * @brief makeCoverAST
535 ** ------------------------------------------------------------------------------------------------------------- */
536PabloAST * BDDMinimizationPass::makeCoverAST(DdNode * const f, PabloBuilder & block) {
537
538    std::queue<PabloAST *> SQ;
539    const auto n = mVariables.size();
540    circular_buffer<PabloAST *> CQ(n + 1);
541    circular_buffer<PabloAST *> DQ(n + 1);
542
543    assert (mManager->size == n);
544
545    int cube[n];
546
547    DdNode * g = f;
548
549    Cudd_Ref(g);
550
551    while (g != Cudd_ReadLogicZero(mManager)) {
552        int length = 0;
553        DdNode * implicant = Cudd_LargestCube(mManager, g, &length);
554        if (LLVM_UNLIKELY(implicant == nullptr)) {
555            Cudd_RecursiveDeref(mManager, g);
556            return nullptr;
557        }
558        Cudd_Ref(implicant);
559        DdNode * prime = Cudd_bddMakePrime(mManager, implicant, f);
560        if (LLVM_UNLIKELY(prime == nullptr)) {
561            Cudd_RecursiveDeref(mManager, g);
562            Cudd_RecursiveDeref(mManager, implicant);
563            return nullptr;
564        }
565        Cudd_Ref(prime);
566        Cudd_RecursiveDeref(mManager, implicant);
567
568        DdNode * h = Cudd_bddAnd(mManager, g, Cudd_Not(prime));
569        if (LLVM_UNLIKELY(h == nullptr)) {
570            Cudd_RecursiveDeref(mManager, g);
571            Cudd_RecursiveDeref(mManager, prime);
572            return nullptr;
573        }
574        Cudd_Ref(h);
575        Cudd_RecursiveDeref(mManager, g);
576
577        g = h;
578        if (LLVM_UNLIKELY(Cudd_BddToCubeArray(mManager, prime, cube) == 0)) {
579            Cudd_RecursiveDeref(mManager, g);
580            Cudd_RecursiveDeref(mManager, prime);
581            return nullptr;
582        }
583        Cudd_RecursiveDeref(mManager, prime);
584
585        assert (DQ.empty() && CQ.empty());
586
587        for (auto i = 0; i != n; ++i) {
588            assert (cube[i] >= 0 && cube[i] <= 2);
589            if (cube[i] == 0) {
590                DQ.push_back(mVariables[i]);
591                // CQ.push_back(block.createOnes());
592            } else if (cube[i] == 1) {
593                CQ.push_back(mVariables[i]);
594                // DQ.push_back(block.createZeroes());
595            }
596        }
597
598        if (LLVM_UNLIKELY(DQ.empty() && CQ.empty())) {
599            throw std::runtime_error("Error! statement contains no elements!");
600        }
601
602        if (DQ.size() > 0) {
603            while (DQ.size() > 1) {
604                PabloAST * v1 = DQ.front(); DQ.pop_front();
605                PabloAST * v2 = DQ.front(); DQ.pop_front();
606                DQ.push_back(block.createOr(v1, v2));
607            }
608            CQ.push_back(block.createNot(DQ.front()));
609            DQ.pop_front();
610        }
611
612        assert (!CQ.empty());
613        while (CQ.size() > 1) {
614            PabloAST * v1 = CQ.front(); CQ.pop_front();
615            PabloAST * v2 = CQ.front(); CQ.pop_front();
616            CQ.push_back(block.createAnd(v1, v2));
617        }
618        SQ.push(CQ.front()); CQ.pop_front();
619    }
620    Cudd_RecursiveDeref(mManager, g);
621    if (LLVM_UNLIKELY(SQ.empty())) {
622        throw std::runtime_error("Error! statement queue empty!");
623    }
624    while (SQ.size() > 1) {
625        PabloAST * v1 = SQ.front(); SQ.pop();
626        PabloAST * v2 = SQ.front(); SQ.pop();
627        SQ.push(block.createOr(v1, v2));
628    }
629    return SQ.front();
630}
631
632/** ------------------------------------------------------------------------------------------------------------- *
633 * @brief CUDD wrappers
634 ** ------------------------------------------------------------------------------------------------------------- */
635
636inline DdNode * BDDMinimizationPass::Zero() const {
637    return Cudd_ReadLogicZero(mManager);
638}
639
640inline DdNode * BDDMinimizationPass::One() const {
641    return Cudd_ReadOne(mManager);
642}
643
644inline DdNode * BDDMinimizationPass::NewVar(const PabloAST * expr) {
645    DdNode * var = Cudd_bddIthVar(mManager, mVariables.size());
646    mVariables.push_back(const_cast<PabloAST *>(expr));
647    return var;
648}
649
650inline bool BDDMinimizationPass::isZero(DdNode * const x) const {
651    return x == Zero();
652}
653
654inline DdNode * BDDMinimizationPass::And(DdNode * const x, DdNode * const y) {
655    DdNode * r = Cudd_bddAnd(mManager, x, y);
656    return r;
657}
658
659inline DdNode * BDDMinimizationPass::Intersect(DdNode * const x, DdNode * const y) {
660    DdNode * r = Cudd_bddIntersect(mManager, x, y); Cudd_Ref(r);
661    return r;
662}
663
664inline DdNode * BDDMinimizationPass::Or(DdNode * const x, DdNode * const y) {
665    DdNode * r = Cudd_bddOr(mManager, x, y);
666    return r;
667}
668
669inline DdNode * BDDMinimizationPass::Xor(DdNode * const x, DdNode * const y) {
670    DdNode * r = Cudd_bddXor(mManager, x, y);
671    return r;
672}
673
674inline DdNode * BDDMinimizationPass::Not(DdNode * const x) const {
675    return Cudd_Not(x);
676}
677
678inline DdNode * BDDMinimizationPass::Ite(DdNode * const x, DdNode * const y, DdNode * const z) {
679    DdNode * r = Cudd_bddIte(mManager, x, y, z);
680    return r;
681}
682
683inline bool BDDMinimizationPass::noSatisfyingAssignment(DdNode * const x) {
684    return Cudd_bddLeq(mManager, x, Zero());
685}
686
687inline void BDDMinimizationPass::shutdown() {
688    Cudd_Quit(mManager);
689}
690
691} // end of namespace pablo
692
Note: See TracBrowser for help on using the repository browser.