Ignore:
Timestamp:
Aug 15, 2015, 7:30:14 PM (4 years ago)
Author:
nmedfort
Message:

Temporary check-in.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_bddminimization.cpp

    r4711 r4725  
    1111#include <boost/circular_buffer.hpp>
    1212#include <pablo/optimizers/pablo_simplifier.hpp>
     13#include <boost/container/flat_set.hpp>
    1314
    1415using namespace llvm;
    1516using namespace boost;
     17using namespace boost::container;
    1618
    1719namespace pablo {
    1820
    19 bool BDDMinimizationPass::optimize(PabloFunction & function) {
    20     raw_os_ostream out(std::cerr);
    21     PabloPrinter::print(function.getEntryBlock(), "", out);
    22     out << "\n****************************************************************\n\n";
    23     out.flush();
    24 
    25     promoteCrossBlockReachingDefs(function);
    26 
     21bool BDDMinimizationPass::optimize(PabloFunction & function, const bool full) {
    2722    BDDMinimizationPass am;
    28     am.initialize(function);
    29     am.characterizeAndEliminateLogicallyEquivalentStatements(function);
    30     am.simplifyAST(function);
    31     am.shutdown();
    32 
     23    am.eliminateLogicallyEquivalentStatements(function);
     24    if (full) {
     25        am.simplifyAST(function);
     26    }
    3327    return Simplifier::optimize(function);
    34 }
    35 
    36 /** ------------------------------------------------------------------------------------------------------------- *
    37  * @brief promoteCrossBlockReachingDefs
    38  * @param function
    39   *
    40  * Scan through the function and promote any cross-block statements into Assign nodes to simplify the BDD node
    41  * generation.
    42  ** ------------------------------------------------------------------------------------------------------------- */
    43 void BDDMinimizationPass::promoteCrossBlockReachingDefs(const PabloFunction & function) {
    44 
    45     std::unordered_map<const PabloAST *, unsigned> block;
    46     std::stack<Statement *> scope;
    47 
    48     unsigned blockIndex = 0;
    49 
    50     for (const Statement * stmt = function.getEntryBlock().front(); ; ) {
    51         while ( stmt ) {
    52 
    53             if (LLVM_UNLIKELY(isa<If>(stmt) || isa<While>(stmt))) {
    54                 // Set the next statement to be the first statement of the inner scope and push the
    55                 // next statement of the current statement into the scope stack.
    56                 const PabloBlock & nested = isa<If>(stmt) ? cast<If>(stmt)->getBody() : cast<While>(stmt)->getBody();
    57                 scope.push(stmt->getNextNode());
    58                 stmt = nested.front();
    59                 assert (stmt);
    60                 ++blockIndex;
    61                 continue;
    62             }
    63 
    64             for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
    65                 Statement * const op = dyn_cast<Statement>(stmt->getOperand(i));
    66                 if (op == nullptr || isa<Assign>(op) || isa<Next>(op) || block[op] == blockIndex) {
    67                     continue;
    68                 }
    69                 PabloBlock * const block = op->getParent();
    70                 block->setInsertPoint(op);
    71 
    72                 op->replaceAllUsesWith(block->createAssign("t", op));
    73             }
    74 
    75             block[stmt] = blockIndex;
    76 
    77             stmt = stmt->getNextNode();
    78         }
    79         if (scope.empty()) {
    80             break;
    81         }
    82         stmt = scope.top();
    83         scope.pop();
    84         ++blockIndex;
    85     }
    8628}
    8729
     
    9436 * the proper variable ordering.
    9537 ** ------------------------------------------------------------------------------------------------------------- */
    96 void BDDMinimizationPass::initialize(const PabloFunction & function) {
     38void BDDMinimizationPass::eliminateLogicallyEquivalentStatements(PabloFunction & function) {
    9739
    9840    std::stack<Statement *> scope;
     
    14284        mCharacterizationMap[function.getParameter(i)] = NewVar(function.getParameter(i));
    14385    }
     86
     87    SubsitutionMap baseMap;
     88    baseMap.insert(Zero(), function.getEntryBlock().createZeroes());
     89    baseMap.insert(One(), function.getEntryBlock().createOnes());
     90
     91    Cudd_AutodynEnable(mManager, CUDD_REORDER_LAZY_SIFT);
     92
     93    eliminateLogicallyEquivalentStatements(function.getEntryBlock(), baseMap);
     94
     95    Cudd_Quit(mManager);
     96    mCharacterizationMap.clear();
    14497}
    14598
     
    150103 * Scan through the program and iteratively compute the BDDs for each statement.
    151104 ** ------------------------------------------------------------------------------------------------------------- */
    152 void BDDMinimizationPass::characterizeAndEliminateLogicallyEquivalentStatements(PabloFunction & function) {
    153     SubsitutionMap baseMap;
    154     baseMap.insert(Zero(), function.getEntryBlock().createZeroes());
    155     baseMap.insert(One(), function.getEntryBlock().createOnes());
    156     Cudd_AutodynEnable(mManager, CUDD_REORDER_LAZY_SIFT);
    157     characterizeAndEliminateLogicallyEquivalentStatements(function.getEntryBlock(), baseMap);
    158     Cudd_AutodynDisable(mManager);
    159     Cudd_ReduceHeap(mManager, CUDD_REORDER_EXACT, 0);
    160 }
    161 
    162 /** ------------------------------------------------------------------------------------------------------------- *
    163  * @brief characterize
    164  * @param vars the input vars for this program
    165  *
    166  * Scan through the program and iteratively compute the BDDs for each statement.
    167  ** ------------------------------------------------------------------------------------------------------------- */
    168 void BDDMinimizationPass::characterizeAndEliminateLogicallyEquivalentStatements(PabloBlock & block, SubsitutionMap & parent) {
     105void BDDMinimizationPass::eliminateLogicallyEquivalentStatements(PabloBlock & block, SubsitutionMap & parent) {
    169106    SubsitutionMap subsitutionMap(&parent);
    170107    Statement * stmt = block.front();
     108
    171109    while (stmt) {
    172         if (LLVM_UNLIKELY(isa<If>(stmt) || isa<While>(stmt))) {
    173 
    174             for (auto promotion : mPromotions) {
    175                 mCharacterizationMap[promotion] = NewVar(promotion);
    176             }
    177             mPromotions.clear();
    178 
    179             characterizeAndEliminateLogicallyEquivalentStatements(isa<If>(stmt) ? cast<If>(stmt)->getBody() : cast<While>(stmt)->getBody(), subsitutionMap);
    180 
    181             for (auto promotion : mPromotions) {
    182                 mCharacterizationMap[promotion] = NewVar(promotion);
    183             }
    184             mPromotions.clear();
    185 
     110        if (LLVM_UNLIKELY(isa<If>(stmt))) {
     111            eliminateLogicallyEquivalentStatements(cast<If>(stmt)->getBody(), subsitutionMap);
     112        } else if (LLVM_UNLIKELY(isa<While>(stmt))) {
     113            eliminateLogicallyEquivalentStatements(cast<While>(stmt)->getBody(), subsitutionMap);
    186114        } else { // attempt to characterize this statement and replace it if
    187             DdNode * bdd = characterizeAndEliminateLogicallyEquivalentStatements(stmt);
     115            DdNode * bdd = eliminateLogicallyEquivalentStatements(stmt);
    188116            if (LLVM_LIKELY(!isa<Assign>(stmt) && !isa<Next>(stmt))) {
    189117                PabloAST * replacement = subsitutionMap[bdd];
     
    205133 * @brief characterize
    206134 ** ------------------------------------------------------------------------------------------------------------- */
    207 inline DdNode * BDDMinimizationPass::characterizeAndEliminateLogicallyEquivalentStatements(const Statement * const stmt) {
     135inline DdNode * BDDMinimizationPass::eliminateLogicallyEquivalentStatements(const Statement * const stmt) {
    208136
    209137    DdNode * bdd = nullptr;
     
    228156        case PabloAST::ClassTypeId::Assign:
    229157        case PabloAST::ClassTypeId::Next:
    230             mPromotions.push_back(stmt);
    231158            return input[0];
    232159        case PabloAST::ClassTypeId::And:
     
    270197inline void BDDMinimizationPass::simplifyAST(PabloFunction & function) {
    271198    PabloBuilder builder(function.getEntryBlock());
    272     simplifyAST(builder);
     199    std::vector<Statement *> terminals;
     200    for (unsigned i = 0; i != function.getNumOfResults(); ++i) {
     201        terminals.push_back(function.getResult(i));
     202    }
     203    simplifyAST(builder, terminals);
     204}
     205
     206/** ------------------------------------------------------------------------------------------------------------- *
     207 * @brief isSimplifiable
     208 ** ------------------------------------------------------------------------------------------------------------- */
     209inline bool isSimplifiable(const PabloAST * const expr, const PabloBlock * const pb) {
     210    switch (expr->getClassTypeId()) {
     211        case PabloAST::ClassTypeId::And:
     212        case PabloAST::ClassTypeId::Or:
     213        case PabloAST::ClassTypeId::Not:
     214        case PabloAST::ClassTypeId::Sel:
     215            return cast<Statement>(expr)->getParent() == pb;
     216        default:
     217            return false;
     218    }
    273219}
    274220
     
    276222 * @brief simplifyAST
    277223 ** ------------------------------------------------------------------------------------------------------------- */
    278 void BDDMinimizationPass::simplifyAST(PabloBuilder & block) {
     224void BDDMinimizationPass::simplifyAST(PabloBuilder & block, std::vector<Statement *> & terminals) {
     225
    279226    for (Statement * stmt : block) {
    280         switch (stmt->getClassTypeId()) {
    281             case PabloAST::ClassTypeId::If:
    282             case PabloAST::ClassTypeId::While: {
    283                     PabloBlock & nested = isa<If>(stmt) ? cast<If>(stmt)->getBody() : cast<While>(stmt)->getBody();
    284                     PabloBuilder builder(nested, block);
    285                     simplifyAST(builder);
    286                     if (isa<If>(stmt)) {
    287                         for (Assign * var : cast<const If>(stmt)->getDefined()) {
    288                             block.record(var);
    289                         }
    290                     } else {
    291                         for (Next * var : cast<const While>(stmt)->getVariants()) {
    292                             block.record(var);
    293                         }
    294                     }
     227        if (isa<While>(stmt)) {
     228            PabloBuilder builder(cast<If>(stmt)->getBody(), block);
     229            std::vector<Statement *> terminals;
     230            for (Assign * var : cast<const If>(stmt)->getDefined()) {
     231                terminals.push_back(var);
     232            }
     233            simplifyAST(builder, terminals);
     234            for (Assign * var : cast<const If>(stmt)->getDefined()) {
     235                block.record(var);
     236            }
     237            continue;
     238        } else if (isa<While>(stmt)) {
     239            PabloBuilder builder(cast<While>(stmt)->getBody(), block);
     240            std::vector<Statement *> terminals;
     241            for (Next * var : cast<const While>(stmt)->getVariants()) {
     242                terminals.push_back(var);
     243            }
     244            simplifyAST(builder, terminals);
     245            for (Next * var : cast<const While>(stmt)->getVariants()) {
     246                block.record(var);
     247            }
     248            continue;
     249        }
     250        block.record(stmt);
     251    }
     252
     253    std::queue<Statement *> Q;
     254    std::vector<PabloAST *> variables;
     255
     256    while (!terminals.empty()) {
     257
     258        for (Statement * term : terminals) {
     259            Q.push(term);
     260        }
     261
     262        // find the variables for this set of terminals
     263        for (;;) {
     264            Statement * stmt = Q.front();
     265            Q.pop();
     266            mCharacterizationMap[stmt] = nullptr;
     267            for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
     268                if (isSimplifiable(stmt->getOperand(i), stmt->getParent())) {
     269                    Q.push(cast<Statement>(stmt->getOperand(i)));
     270                } else {
     271                    variables.push_back(stmt->getOperand(i));
    295272                }
     273            }
     274            if (Q.empty()) {
    296275                break;
    297             case PabloAST::ClassTypeId::ScanThru:
    298             case PabloAST::ClassTypeId::MatchStar:
    299                 simplifyAST(stmt, dyn_cast<Statement>(stmt->getOperand(1)), block);
    300             case PabloAST::ClassTypeId::Advance:
    301             case PabloAST::ClassTypeId::Assign:
    302             case PabloAST::ClassTypeId::Next:
    303                 simplifyAST(stmt, dyn_cast<Statement>(stmt->getOperand(0)), block);
    304             default: block.record(stmt);
    305         }       
    306     }
     276            }
     277        }
     278
     279        std::sort(variables.begin(), variables.end());
     280        std::unique(variables.begin(), variables.end());
     281
     282
     283        mManager = Cudd_Init(variables.size(), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
     284        Cudd_AutodynEnable(mManager, CUDD_REORDER_LAZY_SIFT);
     285
     286        unsigned i = 0;
     287        for (PabloAST * var : variables) {
     288            mCharacterizationMap[var] = Cudd_bddIthVar(mManager, i++);
     289        }
     290
     291        for (PabloAST * term : terminals) {
     292            characterizeTerminalBddTree(term);
     293        }
     294        Cudd_ReduceHeap(mManager, CUDD_REORDER_SIFT, 0);
     295
     296        for (Statement * term : terminals) {
     297            DdNode * const f = mCharacterizationMap[term];
     298            Cudd_Ref(f);
     299            PabloAST * replacement = simplifyAST(f, variables, block);
     300            if (replacement) {
     301                term->replaceWith(replacement, false, true);
     302            }
     303            Cudd_RecursiveDeref(mManager, f);
     304        }
     305
     306        Cudd_Quit(mManager);
     307
     308        mCharacterizationMap.clear();
     309
     310        // Now clear our terminals and test whether we can process another layer within this block
     311        terminals.clear();
     312        for (PabloAST * var : variables) {
     313            if (isa<Statement>(var) && cast<Statement>(var)->getParent() == block.getPabloBlock()) {
     314                terminals.push_back(cast<Statement>(var));
     315            }
     316        }
     317    }
     318
     319}
     320
     321///** ------------------------------------------------------------------------------------------------------------- *
     322// * @brief simplifyAST
     323// ** ------------------------------------------------------------------------------------------------------------- */
     324DdNode * BDDMinimizationPass::characterizeTerminalBddTree(PabloAST * expr) {
     325
     326    const auto f = mCharacterizationMap.find(expr);
     327    if (f == mCharacterizationMap.end()) {
     328        return nullptr;
     329    } else if (f->second) {
     330        return f->second;
     331    }
     332
     333    Statement * stmt = cast<Statement>(expr);
     334    std::array<DdNode *, 3> input;
     335
     336    for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
     337        input[i] = characterizeTerminalBddTree(stmt->getOperand(i));
     338    }
     339
     340    DdNode * bdd = nullptr;
     341    switch (expr->getClassTypeId()) {
     342        case PabloAST::ClassTypeId::And:
     343            bdd = And(input[0], input[1]);
     344            break;
     345        case PabloAST::ClassTypeId::Or:
     346            bdd = Or(input[0], input[1]);
     347            break;
     348        case PabloAST::ClassTypeId::Not:
     349            bdd = Not(input[0]);
     350            break;
     351        case PabloAST::ClassTypeId::Sel:
     352            bdd = Ite(input[0], input[1], input[2]);
     353            break;
     354        default:
     355            throw std::runtime_error("Unexpected operand given to BDDMinimizationPass::characterizeTerminalBddTree!");
     356    }
     357    Cudd_Ref(bdd);
     358    return bdd;
    307359}
    308360
     
    310362 * @brief simplifyAST
    311363 ** ------------------------------------------------------------------------------------------------------------- */
    312 void BDDMinimizationPass::simplifyAST(Statement * stmt, Statement * const expr, PabloBuilder & builder) {
    313     if (expr && expr->getParent() == stmt->getParent()) {
    314         DdNode * const bdd = mCharacterizationMap[expr];
    315         if (bdd) {
    316             builder.getPabloBlock()->setInsertPoint(stmt->getPrevNode());
    317             Cudd_Ref(bdd);
    318             PabloAST * replacement = simplifyAST(bdd, builder);
    319             Cudd_RecursiveDeref(mManager, bdd);
    320             if (replacement) {
    321                 expr->replaceWith(replacement, true, true);
    322             }
    323         }
    324     }
    325 }
    326 
    327 /** ------------------------------------------------------------------------------------------------------------- *
    328  * @brief simplifyAST
    329  ** ------------------------------------------------------------------------------------------------------------- */
    330 PabloAST * BDDMinimizationPass::simplifyAST(DdNode * const f, PabloBuilder & builder) {
     364PabloAST * BDDMinimizationPass::simplifyAST(DdNode * const f, const std::vector<PabloAST *> & variables, PabloBuilder & builder) {
     365    assert (!noSatisfyingAssignment(f));
    331366    DdNode * g = Cudd_FindEssential(mManager, f);
    332367    if (g && Cudd_SupportSize(mManager, g) > 0) {
    333368        if (g == f) { // every variable is essential
    334             return makeCoverAST(f, builder);
     369            return makeCoverAST(f, variables, builder);
    335370        }
    336371        Cudd_Ref(g);
    337         PabloAST * c0 = makeCoverAST(g, builder);
     372        PabloAST * c0 = makeCoverAST(g, variables, builder);
    338373        if (LLVM_UNLIKELY(c0 == nullptr)) {
    339374            Cudd_RecursiveDeref(mManager, g);
     
    342377        DdNode * h = Cudd_Cofactor(mManager, f, g);
    343378        Cudd_Ref(h);
     379        PabloAST * c1 = simplifyAST(h, variables, builder);
     380        if (LLVM_UNLIKELY(c1 == nullptr)) {
     381            Cudd_RecursiveDeref(mManager, g);
     382            Cudd_RecursiveDeref(mManager, h);
     383            cast<Statement>(c0)->eraseFromParent(true);
     384            return nullptr;
     385        }
     386        assert (And(g, h) == f);
    344387        Cudd_RecursiveDeref(mManager, g);
    345         PabloAST * c1 = simplifyAST(h, builder);
    346388        Cudd_RecursiveDeref(mManager, h);
    347         if (LLVM_UNLIKELY(c1 == nullptr)) {
    348             if (LLVM_LIKELY(isa<Statement>(c0))) {
    349                 cast<Statement>(c0)->eraseFromParent(true);
    350             }
    351             return nullptr;
    352         }
    353         return builder.createAnd(c0, c1);
    354     }
     389        return builder.createAnd(c0, c1, "escf");
     390    }
     391
    355392    DdNode ** disjunct = nullptr;
    356     const auto disjuncts = Cudd_bddVarConjDecomp(mManager, f, &disjunct);
    357     if (LLVM_LIKELY(disjuncts == 2)) {
    358         Cudd_Ref(disjunct[0]);
    359         Cudd_Ref(disjunct[1]);
    360         PabloAST * d0 = simplifyAST(disjunct[0], builder);
    361         Cudd_RecursiveDeref(mManager, disjunct[0]);
     393    int disjuncts = Cudd_bddIterDisjDecomp(mManager, f, &disjunct);
     394    assert (disjuncts < 2 || Or(disjunct[0], disjunct[1]) == f);
     395
     396    DdNode ** conjunct = nullptr;
     397    int conjuncts = Cudd_bddIterConjDecomp(mManager, f, &conjunct);
     398    assert (conjuncts < 2 || And(conjunct[0], conjunct[1]) == f);
     399
     400    if (LLVM_LIKELY(disjuncts == 2 && conjuncts == 2)) {
     401        if (Cudd_SharingSize(disjunct, 2) > Cudd_SharingSize(conjunct, 2)) {
     402            disjuncts = 0;
     403        }
     404    }
     405
     406    DdNode * decomp[] = { nullptr, nullptr };
     407    if (disjuncts == 2) {
     408        memcpy(decomp, disjunct, sizeof(DdNode *) * 2);
     409    } else if (conjuncts == 2) {
     410        memcpy(decomp, conjunct, sizeof(DdNode *) * 2);
     411    }
     412
     413    FREE(disjunct);
     414    FREE(conjunct);
     415
     416    if ((decomp[0] != decomp[1]) && (decomp[0] != f) && (decomp[1] != f)) {
     417        Cudd_Ref(decomp[0]);
     418        Cudd_Ref(decomp[1]);
     419        PabloAST * d0 = simplifyAST(decomp[0], variables, builder);
     420        Cudd_RecursiveDeref(mManager, decomp[0]);
    362421        if (LLVM_UNLIKELY(d0 == nullptr)) {
    363             Cudd_RecursiveDeref(mManager, disjunct[1]);
    364             return nullptr;
    365         }
    366         PabloAST * d1 = simplifyAST(disjunct[1], builder);
    367         Cudd_RecursiveDeref(mManager, disjunct[1]);
    368         FREE(disjunct);
     422            Cudd_RecursiveDeref(mManager, decomp[1]);
     423            return nullptr;
     424        }
     425
     426        PabloAST * d1 = simplifyAST(decomp[1], variables, builder);
     427        Cudd_RecursiveDeref(mManager, decomp[1]);
    369428        if (LLVM_UNLIKELY(d1 == nullptr)) {
    370             if (LLVM_LIKELY(isa<Statement>(d0))) {
    371                 cast<Statement>(d0)->eraseFromParent(true);
    372             }
    373             return nullptr;
    374         }
    375         return builder.createAnd(d0, d1);
    376     }
    377     FREE(disjunct);
    378     return makeCoverAST(f, builder);
     429            cast<Statement>(d0)->eraseFromParent(true);
     430            return nullptr;
     431        }
     432
     433        if (disjuncts == 2) {
     434            return builder.createOr(d0, d1, "disj");
     435        } else {
     436            return builder.createAnd(d0, d1, "conj");
     437        }
     438    }
     439    return makeCoverAST(f, variables, builder);
    379440}
    380441
     
    382443 * @brief makeCoverAST
    383444 ** ------------------------------------------------------------------------------------------------------------- */
    384 PabloAST * BDDMinimizationPass::makeCoverAST(DdNode * const f, PabloBuilder & builder) {
     445PabloAST * BDDMinimizationPass::makeCoverAST(DdNode * const f, const std::vector<PabloAST *> & variables, PabloBuilder & builder) {
    385446
    386447    std::queue<PabloAST *> SQ;
    387 
    388     circular_buffer<PabloAST *> CQE(mManager->size);
    389     circular_buffer<PabloAST *> CQO(mManager->size);
    390 
    391     circular_buffer<PabloAST *> DQE(mManager->size);
    392     circular_buffer<PabloAST *> DQO(mManager->size);
    393 
    394     int cube[mManager->size];
     448    const unsigned n = variables.size();
     449    circular_buffer<PabloAST *> CQ(n);
     450    circular_buffer<PabloAST *> DQ(n);
     451
     452    assert (mManager->size == variables.size());
     453
     454    int cube[n];
    395455
    396456    DdNode * g = f;
     
    399459
    400460    while (g != Cudd_ReadLogicZero(mManager)) {
    401         int length;
     461        int length = 0;
    402462        DdNode * implicant = Cudd_LargestCube(mManager, g, &length);
    403463        if (LLVM_UNLIKELY(implicant == nullptr)) {
     
    432492        Cudd_RecursiveDeref(mManager, prime);
    433493
    434         for (auto i = 0; i != mManager->size; ++i) {
    435             if ((i & 1) == 0) { // i is even
    436                 if (cube[i] == 0) {
    437                     DQE.push_back(mVariables[i]);
    438                 } else if (cube[i] == 1) {
    439                     CQE.push_back(mVariables[i]);
    440                 }
    441             } else { // i is odd
    442                 if (cube[i] == 0) {
    443                     DQO.push_back(mVariables[i]);
    444                 } else if (cube[i] == 1) {
    445                     CQO.push_back(mVariables[i]);
    446                 }
    447             }
    448         }
    449 
    450         PabloAST * dq = builder.createZeroes();
    451         if (!DQE.empty() || !DQO.empty()) {
    452             while (DQE.size() > 1) {
    453                 PabloAST * v1 = DQE.front(); DQE.pop_front();
    454                 PabloAST * v2 = DQE.front(); DQE.pop_front();
    455                 DQE.push_back(builder.createOr(v1, v2));
    456             }
    457             while (DQO.size() > 1) {
    458                 PabloAST * v1 = DQO.front(); DQO.pop_front();
    459                 PabloAST * v2 = DQO.front(); DQO.pop_front();
    460                 DQO.push_back(builder.createOr(v1, v2));
    461             }
    462             if (DQE.empty()) {
    463                 dq = DQO.front();
    464             } else if (DQO.empty()) {
    465                 dq = DQE.front();
    466             } else {
    467                 dq = builder.createOr(DQE.front(), DQO.front());
    468             }
    469             DQE.clear();
    470             DQO.clear();
    471         }
    472 
    473         PabloAST * cq = builder.createOnes();
    474         if (!CQE.empty() || !CQO.empty()) {
    475             while (CQE.size() > 1) {
    476                 PabloAST * v1 = CQE.front(); CQE.pop_front();
    477                 PabloAST * v2 = CQE.front(); CQE.pop_front();
    478                 CQE.push_back(builder.createOr(v1, v2));
    479             }
    480             while (CQO.size() > 1) {
    481                 PabloAST * v1 = CQO.front(); CQO.pop_front();
    482                 PabloAST * v2 = CQO.front(); CQO.pop_front();
    483                 CQO.push_back(builder.createOr(v1, v2));
    484             }
    485             if (CQE.empty()) {
    486                 dq = CQO.front();
    487             } else if (CQO.empty()) {
    488                 dq = CQE.front();
    489             } else {
    490                 dq = builder.createAnd(CQE.front(), CQO.front());
    491             }
    492             CQE.clear();
    493             CQO.clear();
    494         }
    495         SQ.push(builder.createAnd(cq, builder.createNot(dq)));
     494        assert (DQ.empty() && CQ.empty());
     495
     496        for (auto i = 0; i != n; ++i) {
     497            assert (cube[i] >= 0 && cube[i] <= 2);
     498            if (cube[i] == 0) {
     499                assert (!DQ.full());
     500                DQ.push_back(variables[i]);
     501            } else if (cube[i] == 1) {
     502                assert (!CQ.full());
     503                CQ.push_back(variables[i]);
     504            }
     505        }
     506
     507        if (LLVM_UNLIKELY(DQ.empty() && CQ.empty())) {
     508            throw std::runtime_error("Error! statement contains no elements!");
     509        }
     510
     511        if (DQ.size() > 0) {
     512            while (DQ.size() > 1) {
     513                PabloAST * v1 = DQ.front(); DQ.pop_front();
     514                PabloAST * v2 = DQ.front(); DQ.pop_front();
     515                DQ.push_back(builder.createOr(v1, v2));
     516            }
     517            CQ.push_back(builder.createNot(DQ.front()));
     518            DQ.pop_front();
     519        }
     520
     521        assert (!CQ.empty());
     522        while (CQ.size() > 1) {
     523            PabloAST * v1 = CQ.front(); CQ.pop_front();
     524            PabloAST * v2 = CQ.front(); CQ.pop_front();
     525            CQ.push_back(builder.createAnd(v1, v2));
     526        }
     527        SQ.push(CQ.front()); CQ.pop_front();
    496528    }
    497529    Cudd_RecursiveDeref(mManager, g);
    498 
     530    if (LLVM_UNLIKELY(SQ.empty())) {
     531        throw std::runtime_error("Error! statement queue empty!");
     532    }
    499533    while (SQ.size() > 1) {
    500534        PabloAST * v1 = SQ.front(); SQ.pop();
     
    502536        SQ.push(builder.createOr(v1, v2));
    503537    }
    504 
    505538    return SQ.front();
    506539}
Note: See TracChangeset for help on using the changeset viewer.