Ignore:
Timestamp:
Aug 21, 2015, 4:12:09 PM (4 years ago)
Author:
nmedfort
Message:

Initial stages of a simple boolean equation reassociation pass.

Location:
icGREP/icgrep-devel/icgrep/pablo
Files:
2 added
6 edited

Legend:

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

    r4718 r4736  
    221221}
    222222
    223 
    224 
    225 
    226223PabloAST * PabloBlock::createAnd(PabloAST * expr1, PabloAST * expr2) {
    227224    assert (expr1 && expr2);
    228225    if (isa<Zeroes>(expr2) || isa<Ones>(expr1)) {
    229226        return expr2;
    230     }
    231     else if (isa<Zeroes>(expr1) || isa<Ones>(expr2) || equals(expr1, expr2)){
     227    } else if (isa<Zeroes>(expr1) || isa<Ones>(expr2) || equals(expr1, expr2)){
    232228        return expr1;
    233     }
    234     else if (Not * not1 = dyn_cast<Not>(expr1)) {
     229    } else if (Not * not1 = dyn_cast<Not>(expr1)) {
    235230        if (Not * not2 = dyn_cast<Not>(expr2)) {
    236231            return createNot(createOr(not1->getExpr(), not2->getExpr()));
    237         }
    238         else if (equals(not1->getExpr(), expr2)) {
     232        } else if (equals(not1->getExpr(), expr2)) {
    239233            return createZeroes();
    240234        }
    241     }
    242     else if (Not * not2 = dyn_cast<Not>(expr2)) {
     235    } else if (Not * not2 = dyn_cast<Not>(expr2)) {
    243236        if (equals(expr1, not2->getExpr())) {
    244237            return createZeroes();
    245238        }
     239    } else if (Or * or1 = dyn_cast<Or>(expr1)) {
     240        if (equals(or1->getExpr1(), expr2) || equals(or1->getExpr2(), expr2)) {
     241            return expr2;
     242        }
     243    } else if (Or * or2 = dyn_cast<Or>(expr2)) {
     244        if (equals(or2->getExpr1(), expr1) || equals(or2->getExpr2(), expr1)) {
     245            return expr1;
     246        }
    246247    }
    247248    if (isa<Not>(expr1) || expr1 > expr2) {
     
    250251    return insertAtInsertionPoint(new And(expr1, expr2, makeName("and_")));
    251252}
    252 
    253253
    254254PabloAST * PabloBlock::createAnd(PabloAST * expr1, PabloAST * expr2, const std::string prefix) {
     
    256256    if (isa<Zeroes>(expr2) || isa<Ones>(expr1)) {
    257257        return renameNonNamedNode(expr2, std::move(prefix));
    258     }
    259     else if (isa<Zeroes>(expr1) || isa<Ones>(expr2) || equals(expr1, expr2)){
     258    } else if (isa<Zeroes>(expr1) || isa<Ones>(expr2) || equals(expr1, expr2)){
    260259        return renameNonNamedNode(expr1, std::move(prefix));
    261     }
    262     else if (Not * not1 = dyn_cast<Not>(expr1)) {
     260    } else if (Not * not1 = dyn_cast<Not>(expr1)) {
    263261        if (Not * not2 = dyn_cast<Not>(expr2)) {
    264262            return createNot(createOr(not1->getExpr(), not2->getExpr()), prefix);
     
    267265            return createZeroes();
    268266        }
    269     }
    270     else if (Not * not2 = dyn_cast<Not>(expr2)) {
     267    } else if (Not * not2 = dyn_cast<Not>(expr2)) {
    271268        if (equals(expr1, not2->getExpr())) {
    272269            return createZeroes();
     270        }
     271    } else if (Or * or1 = dyn_cast<Or>(expr1)) {
     272        if (equals(or1->getExpr1(), expr2) || equals(or1->getExpr2(), expr2)) {
     273            return expr2;
     274        }
     275    } else if (Or * or2 = dyn_cast<Or>(expr2)) {
     276        if (equals(or2->getExpr1(), expr1) || equals(or2->getExpr2(), expr1)) {
     277            return expr1;
    273278        }
    274279    }
     
    286291    if (isa<Zeroes>(expr2) || isa<Ones>(expr1) || equals(expr1, expr2)) {
    287292        return expr1;
    288     }
    289     else if (Not * not1 = dyn_cast<Not>(expr1)) {
     293    } else if (Not * not1 = dyn_cast<Not>(expr1)) {
    290294        // ¬a√b = ¬¬(¬a√b) = ¬(a ∧ ¬b)
    291295        return createNot(createAnd(not1->getExpr(), createNot(expr2)));
    292     }
    293     else if (Not * not2 = dyn_cast<Not>(expr2)) {
     296    } else if (Not * not2 = dyn_cast<Not>(expr2)) {
    294297        // a√¬b = ¬¬(¬b√a) = ¬(b ∧ ¬a)
    295298        return createNot(createAnd(not2->getExpr(), createNot(expr1)));
    296     }
    297     else if (equals(expr1, expr2)) {
     299    } else if (equals(expr1, expr2)) {
    298300        return expr1;
    299     }
    300     else if (And * and_expr1 = dyn_cast<And>(expr1)) {
    301         if (And * and_expr2 = dyn_cast<And>(expr2)) {
    302             PabloAST * const expr1a = and_expr1->getExpr1();
    303             PabloAST * const expr1b = and_expr1->getExpr2();
    304             PabloAST * const expr2a = and_expr2->getExpr1();
    305             PabloAST * const expr2b = and_expr2->getExpr2();
     301    } else if (And * and1 = dyn_cast<And>(expr1)) {
     302        if (And * and2 = dyn_cast<And>(expr2)) {
     303            PabloAST * const expr1a = and1->getExpr1();
     304            PabloAST * const expr1b = and1->getExpr2();
     305            PabloAST * const expr2a = and2->getExpr1();
     306            PabloAST * const expr2b = and2->getExpr2();
    306307            //These optimizations factor out common components that can occur when sets are formed by union
    307308            //(e.g., union of [a-z] and [A-Z].
    308309            if (equals(expr1a, expr2a)) {
    309310                return createAnd(expr1a, createOr(expr1b, expr2b));
    310             }
    311             else if (equals(expr1b, expr2b)) {
     311            } else if (equals(expr1b, expr2b)) {
    312312                return createAnd(expr1b, createOr(expr1a, expr2a));
    313             }
    314             else if (equals(expr1a, expr2b)) {
     313            } else if (equals(expr1a, expr2b)) {
    315314                return createAnd(expr1a, createOr(expr1b, expr2a));
    316             }
    317             else if (equals(expr1b, expr2a)) {
     315            } else if (equals(expr1b, expr2a)) {
    318316                return createAnd(expr1b, createOr(expr1a, expr2b));
    319317            }
     318        } else if (equals(and1->getExpr1(), expr2) || equals(and1->getExpr2(), expr2)){
     319            // (a∧b) √ a = a
     320            return expr2;
     321        }
     322    } else if (And * and2 = dyn_cast<And>(expr2)) {
     323        if (equals(and2->getExpr1(), expr1) || equals(and2->getExpr2(), expr1)) {
     324            return expr1;
    320325        }
    321326    }
     
    342347        return createNot(createAnd(not2->getExpr(), createNot(expr1)), prefix);
    343348    }
    344     else if (And * and_expr1 = dyn_cast<And>(expr1)) {
    345         if (And * and_expr2 = dyn_cast<And>(expr2)) {
    346             PabloAST * const expr1a = and_expr1->getExpr1();
    347             PabloAST * const expr1b = and_expr1->getExpr2();
    348             PabloAST * const expr2a = and_expr2->getExpr1();
    349             PabloAST * const expr2b = and_expr2->getExpr2();
     349    else if (And * and1 = dyn_cast<And>(expr1)) {
     350        if (And * and2 = dyn_cast<And>(expr2)) {
     351            PabloAST * const expr1a = and1->getExpr1();
     352            PabloAST * const expr1b = and1->getExpr2();
     353            PabloAST * const expr2a = and2->getExpr1();
     354            PabloAST * const expr2b = and2->getExpr2();
    350355            //These optimizations factor out common components that can occur when sets are formed by union
    351356            //(e.g., union of [a-z] and [A-Z].
     
    362367                return createAnd(expr1b, createOr(expr1a, expr2b), prefix);
    363368            }
     369        } else if (equals(and1->getExpr1(), expr2) || equals(and1->getExpr2(), expr2)) {
     370            // (a∧b) √ a = a
     371            return expr2;
     372        }
     373    } else if (And * and2 = dyn_cast<And>(expr2)) {
     374        if (equals(and2->getExpr1(), expr1) || equals(and2->getExpr2(), expr1)) {
     375            return expr1;
    364376        }
    365377    }
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_automultiplexing.cpp

    r4728 r4736  
    160160        LOG("SelectedIndependentSets: " << (end_select_independent_sets - start_select_independent_sets));
    161161
     162        BooleanReassociationPass::optimize(function);
     163
    162164        RECORD_TIMESTAMP(start_topological_sort);
    163165        am.topologicalSort(function.getEntryBlock());
     
    165167        LOG("TopologicalSort (1):     " << (end_topological_sort - start_topological_sort));
    166168
    167         BDDMinimizationPass::optimize(function, true);
     169        BDDMinimizationPass::optimize(function, false);
    168170    }
    169171
    170172    LOG_NUMBER_OF_ADVANCES(function.getEntryBlock());
    171 
    172173    return multiplex;
    173174}
     
    645646    }
    646647
     648    assert (S.size() > 0);
     649
    647650    auto remainingVerticies = num_vertices(mConstraintGraph) - S.size();
    648651
     
    653656        bool noNewElements = true;
    654657        do {
     658            assert (S.size() > 0);
    655659            // Randomly choose a vertex in S and discard it.
    656660            const auto i = S.begin() + IntDistribution(0, S.size() - 1)(rng);
    657             const ConstraintVertex u = *i;
    658             S.erase(i);
    659             --remainingVerticies;
     661            assert (i != S.end());
     662            const ConstraintVertex u = *i;           
     663            S.erase(i);           
    660664
    661665            for (auto e : make_iterator_range(out_edges(u, mConstraintGraph))) {
     
    663667                if ((--D[v]) == 0) {
    664668                    S.push_back(v);
     669                    --remainingVerticies;
    665670                    noNewElements = false;
    666671                }
     
    851856            graph_traits<MultiplexSetGraph>::out_edge_iterator ei, ei_end;
    852857            // For each member of a "set vertex" ...
    853             std::tie(ei, ei_end) = out_edges(i, mMultiplexSetGraph);
    854             for (; ei != ei_end; ++ei) {
    855                 const auto s = source(*ei, mMultiplexSetGraph);
     858            for (auto e : make_iterator_range(out_edges(i, mMultiplexSetGraph))) {
     859                const auto s = source(e, mMultiplexSetGraph);
    856860                if (out_degree(s, mMultiplexSetGraph) != 0) {
    857861                    // First scan through the subgraph of vertices in M dominated by s and build up the set T,
     
    942946void AutoMultiplexing::multiplexSelectedIndependentSets() {
    943947
    944     const unsigned f = num_vertices(mConstraintGraph);
    945     const unsigned l = num_vertices(mMultiplexSetGraph);
     948    const unsigned first_set = num_vertices(mConstraintGraph);
     949    const unsigned last_set = num_vertices(mMultiplexSetGraph);
    946950
    947951    // Preallocate the structures based on the size of the largest multiplex set
    948952    size_t max_n = 3;
    949     for (unsigned s = f; s != l; ++s) {
    950         max_n = std::max<unsigned>(max_n, out_degree(s, mMultiplexSetGraph));
     953    for (unsigned idx = first_set; idx != last_set; ++idx) {
     954        max_n = std::max<unsigned>(max_n, out_degree(idx, mMultiplexSetGraph));
    951955    }
    952956
     
    956960    // relationships of our independent sets.
    957961
    958     for (unsigned s = f; s != l; ++s) {
    959         const size_t n = out_degree(s, mMultiplexSetGraph);
     962    for (unsigned idx = first_set; idx != last_set; ++idx) {
     963        const size_t n = out_degree(idx, mMultiplexSetGraph);
    960964        if (n) {
    961965            const size_t m = log2_plus_one(n);           
    962966            Advance * input[n];
    963             Advance * muxed[m];
     967            Advance * muxed[m];           
    964968
    965969            unsigned i = 0;
    966             for (const auto e : make_iterator_range(out_edges(s, mMultiplexSetGraph))) {
     970            for (const auto e : make_iterator_range(out_edges(idx, mMultiplexSetGraph))) {
    967971                input[i] = std::get<0>(mAdvance[target(e, mMultiplexSetGraph)]);
    968972                assert (input[i]);
     
    980984
    981985                std::ostringstream prefix;
    982                 prefix << "mux" << n << "to" << m << '_';
    983                 for (size_t i = 1; i <= n; ++i) {
    984                     if ((i & (static_cast<size_t>(1) << j)) != 0) {
    985                         Q.push_back(input[i - 1]->getOperand(0));
     986                prefix << "mux" << n << "to" << m << '.' << (j + 1);
     987                for (size_t i = 0; i != n; ++i) {
     988                    if (((i + 1) & (1ULL << j)) != 0) {
     989                        Q.push_back(input[i]->getOperand(0));
    986990                    }
    987991                }
     
    10001004            }
    10011005
    1002             /// Perform m-to-n Demultiplexing           
    1003             for (size_t i = 1; i <= n; ++i) {
     1006            /// Perform m-to-n Demultiplexing                       
     1007            for (size_t i = 0; i != n; ++i) {
    10041008
    10051009                // Construct the demuxed values and replaces all the users of the original advances with them.
    10061010                for (size_t j = 0; j != m; ++j) {
    1007                     if ((i & (1ULL << j)) == 0) {
     1011                    if (((i + 1) & (1ULL << j)) == 0) {
    10081012                        Q.push_back(muxed[j]);
    10091013                    }
     
    10231027
    10241028                for (unsigned j = 0; j != m; ++j) {
    1025                     if ((i & (1ULL << j)) != 0) {
     1029                    if (((i + 1) & (1ULL << j)) != 0) {
    10261030                        assert (!Q.full());
    10271031                        Q.push_back(muxed[j]);
     
    10371041
    10381042                PabloAST * demuxed = Q.front(); Q.pop_front(); assert (demuxed);
    1039                 input[i - 1]->replaceWith(demuxed, true, true);
     1043                input[i]->replaceWith(demuxed, true, true);
    10401044            }
    10411045        }       
     
    10591063    std::stack<Statement *> scope;
    10601064
     1065    raw_os_ostream out(std::cerr);
     1066
    10611067    for (Statement * stmt = entry.front(); ; ) { restart:
    10621068        while ( stmt ) {
    1063 
    10641069            for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
    10651070                PabloAST * const op = stmt->getOperand(i);
     
    10981103}
    10991104
     1105/** ------------------------------------------------------------------------------------------------------------- *
     1106 * @brief reassociate
     1107 ** ------------------------------------------------------------------------------------------------------------- */
     1108inline void AutoMultiplexing::reassociate(PabloBuilder & builder, PabloAST * const demuxed[], const unsigned n) const {
     1109    using Graph = boost::adjacency_list<boost::hash_setS, boost::vecS, boost::bidirectionalS, PabloAST *>;
     1110    using Map = std::unordered_map<PabloAST *, Graph::vertex_descriptor>;
     1111    using Queue = std::queue<Graph::vertex_descriptor>;
     1112    using Or = pablo::Or;
     1113    using And = pablo::And;
     1114
     1115
     1116    flat_set<PabloAST *> initial_vars;
     1117
     1118
     1119    std::queue<And *> andQ;
     1120    for (unsigned i = 0; i != n; ++i) {
     1121        for (PabloAST * user : demuxed[i]->users()) {
     1122            if (isa<And>(user)) {
     1123                andQ.push(cast<And>(user));
     1124            } else if (isa<Or>(user)) {
     1125                initial_vars.insert(demuxed[i]);
     1126            }
     1127        }
     1128    }
     1129
     1130    while (!andQ.empty()) {
     1131        And * inst = andQ.front(); andQ.pop();
     1132        for (PabloAST * user : inst->users()) {
     1133            if (isa<And>(user)) {
     1134                andQ.push(cast<And>(user));
     1135            } else if (isa<Or>(user)) {
     1136                initial_vars.insert(inst);
     1137            }
     1138        }
     1139    }
     1140
     1141    Graph G;
     1142    Map M;
     1143    Queue Q;
     1144
     1145    // First insert the demuxed variables as our initial sources (as vertices 0 ... n-1)
     1146    for (PabloAST * inst : initial_vars) {
     1147        M.insert(std::make_pair(inst, add_vertex(inst, G)));
     1148    }
     1149
     1150    // Now add in the users of those demuxed variables
     1151    for (PabloAST * inst : initial_vars) {
     1152        const auto i = M[inst];
     1153        for (PabloAST * user : inst->users()) {
     1154            const auto f = M.find(user);
     1155            if (LLVM_LIKELY(f == M.end())) {
     1156                const auto j = add_vertex(user, G);
     1157                M.insert(std::make_pair(user, j));
     1158                add_edge(i, j, G);
     1159                if (isa<Or>(user)) {
     1160                    Q.push(j);
     1161                }
     1162            } else {
     1163                add_edge(i, f->second, G);
     1164            }
     1165        }
     1166    }
     1167
     1168    // Now scan through the graph to locate any disjunctions and the final outputs
     1169    while (!Q.empty()) {
     1170        const auto u = Q.front(); Q.pop();
     1171        Or * expr = cast<Or>(G[u]);
     1172        for (unsigned i = 0; i != 2; ++i) {
     1173            PabloAST * op = expr->getOperand(i);
     1174            const auto f = M.find(op);
     1175            if (LLVM_UNLIKELY(f == M.end())) {
     1176                const auto v = add_vertex(op, G);
     1177                M.insert(std::make_pair(op, v));
     1178                add_edge(v, u, G);
     1179                if (isa<Or>(op)) {
     1180                    Q.push(v);
     1181                }
     1182            }
     1183        }
     1184        for (PabloAST * user : expr->users()) {
     1185            const auto f = M.find(user);
     1186            if (LLVM_UNLIKELY(f == M.end())) {
     1187                const auto v = add_vertex(user, G);
     1188                M.insert(std::make_pair(user, v));
     1189                add_edge(u, v, G);
     1190                if (isa<Or>(user)) {
     1191                    Q.push(v);
     1192                }
     1193            } else {
     1194                add_edge(u, f->second, G);
     1195            }
     1196        }
     1197    }
     1198
     1199    // Clean up the graph to remove any non-disjunctions and their dependencies
     1200    for (auto u : make_iterator_range(vertices(G))) {
     1201        if (in_degree(u, G) == 0 || isa<Or>(G[u])) {
     1202            continue;
     1203        }
     1204        clear_in_edges(u, G);
     1205        for (;;) {
     1206            for (auto e : make_iterator_range(out_edges(u, G))) {
     1207                Q.push(target(e, G));
     1208            }
     1209            clear_out_edges(u, G);
     1210            if (Q.empty()) {
     1211                break;
     1212            }
     1213            u = Q.front(); Q.pop();
     1214        }
     1215    }
     1216
     1217    // Now determine the number of source variables
     1218    unsigned m = 0;
     1219    for (auto u : make_iterator_range(vertices(G))) {
     1220        if (in_degree(u, G) == 0 && out_degree(u, G) > 0) {
     1221            ++m;
     1222        }
     1223    }
     1224
     1225
     1226    circular_buffer<PabloAST *> R(m);
     1227    // And then which variables required to compute each disjunction
     1228    for (const auto u : make_iterator_range(vertices(G))) {
     1229        if (out_degree(u, G) == 0 && in_degree(u, G) > 0) {
     1230
     1231            std::vector<bool> visited(num_vertices(G), false);
     1232            flat_set<Graph::vertex_descriptor> variables;
     1233            for (auto v = u; ; ) {
     1234                if (in_degree(v, G) == 0) {
     1235                    variables.insert(v);
     1236                } else {
     1237                    for (auto e : make_iterator_range(in_edges(v, G))) {
     1238                        const auto w = source(e, G);
     1239                        if (!visited[w]) {
     1240                            Q.push(w);
     1241                            visited[w] = true;
     1242                        }
     1243                    }
     1244                }
     1245                if (Q.empty()) {
     1246                    break;
     1247                }
     1248                v = Q.front(); Q.pop();
     1249            }
     1250            if (variables.size() > 3) {
     1251                unsigned i = 0;
     1252                for (auto j : variables) {
     1253                    for (; i < j; ++i) {
     1254                        R.push_back(builder.createZeroes());
     1255                    }
     1256                    R.push_back(G[j]);
     1257                }
     1258                for (; i < m; ++i) {
     1259                    R.push_back(builder.createZeroes());
     1260                }
     1261                while (R.size() > 1) {
     1262                    PabloAST * e1 = R.front(); R.pop_front();
     1263                    PabloAST * e2 = R.front(); R.pop_front();
     1264                    R.push_back(builder.createOr(e1, e2));
     1265                }
     1266                Statement * stmt = cast<Statement>(G[u]);
     1267                stmt->replaceAllUsesWith(R.front());
     1268                R.clear();
     1269            }
     1270        }
     1271    }
     1272
     1273}
     1274
     1275
    11001276} // end of namespace pablo
    11011277
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_automultiplexing.hpp

    r4728 r4736  
    2929    using IntDistribution = std::uniform_int_distribution<RNG::result_type>;
    3030    using MultiplexSetGraph = boost::adjacency_list<boost::hash_setS, boost::vecS, boost::bidirectionalS>;
    31     using Trie = boost::adjacency_list<boost::hash_setS, boost::vecS, boost::directedS, ConstraintVertex, boost::no_property>;
    3231    using SubsetGraph = boost::adjacency_list<boost::hash_setS, boost::vecS, boost::bidirectionalS>;
    3332    // the Advance pointer, input BDD and the BDD variable of the i-th Advance
     
    4948    void applySubsetConstraints();
    5049    void multiplexSelectedIndependentSets();
     50    void reassociate(PabloBuilder & builder, PabloAST * const demuxed[], const unsigned n) const;
    5151    void topologicalSort(PabloBlock & entry) const;
    5252    inline AutoMultiplexing()
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_bddminimization.cpp

    r4728 r4736  
    2323bool BDDMinimizationPass::optimize(PabloFunction & function, const bool full) {
    2424    BDDMinimizationPass am;
     25    am.eliminateLogicallyEquivalentStatements(function);
    2526    if (full) {
    2627        am.simplifyAST(function);
    2728    }
    28     am.eliminateLogicallyEquivalentStatements(function);
     29    am.shutdown();
    2930    return Simplifier::optimize(function);
    3031}
     
    9192    baseMap.insert(One(), function.getEntryBlock().createOnes());
    9293
     94    Cudd_SetSiftMaxVar(mManager, 1000000);
     95    Cudd_SetSiftMaxSwap(mManager, 1000000000);
    9396    Cudd_AutodynEnable(mManager, CUDD_REORDER_LAZY_SIFT);
    9497
    9598    eliminateLogicallyEquivalentStatements(function.getEntryBlock(), baseMap);
    9699
    97     Cudd_Quit(mManager);
    98     mCharacterizationMap.clear();
     100    Cudd_AutodynDisable(mManager);
    99101}
    100102
     
    108110    SubsitutionMap subsitutionMap(&parent);
    109111    Statement * stmt = block.front();
    110 
    111112    while (stmt) {
    112113        if (LLVM_UNLIKELY(isa<If>(stmt))) {
    113114            eliminateLogicallyEquivalentStatements(cast<If>(stmt)->getBody(), subsitutionMap);
     115            for (Assign * var : cast<const If>(stmt)->getDefined()) {
     116                mCharacterizationMap[var] = NewVar(var);
     117            }
    114118        } else if (LLVM_UNLIKELY(isa<While>(stmt))) {
    115119            eliminateLogicallyEquivalentStatements(cast<While>(stmt)->getBody(), subsitutionMap);
     120            for (Next * var : cast<const While>(stmt)->getVariants()) {
     121                mCharacterizationMap[var] = NewVar(var);
     122            }
    116123        } else { // attempt to characterize this statement and replace it if
    117124            DdNode * bdd = eliminateLogicallyEquivalentStatements(stmt);
     
    128135        }
    129136        stmt = stmt->getNextNode();
    130     }
    131     Cudd_ReduceHeap(mManager, CUDD_REORDER_SIFT, 0);
     137    }   
     138    Cudd_ReduceHeap(mManager, CUDD_REORDER_SIFT, 1);
    132139}
    133140
     
    207214    for (unsigned i = 0; i != function.getNumOfResults(); ++i) {
    208215        terminals.push_back(function.getResult(i));
    209     }
     216    }   
     217    Cudd_ReduceHeap(mManager, CUDD_REORDER_EXACT, 1);
    210218    simplifyAST(function.getEntryBlock(), std::move(terminals));
    211219}
    212220
    213 /** ------------------------------------------------------------------------------------------------------------- *
    214  * @brief promoteSimpleInputDerivationsToAssigns
    215  ** ------------------------------------------------------------------------------------------------------------- */
    216 inline void BDDMinimizationPass::promoteSimpleInputDerivationsToAssigns(PabloFunction & function) {
    217 
    218     using Graph = adjacency_list<hash_setS, vecS, bidirectionalS, PabloAST *>;
    219     using Vertex = Graph::vertex_descriptor;
    220 
    221     Graph G;
    222     flat_map<PabloAST *, Vertex> M;
    223     std::queue<Vertex> Q;
    224     for (unsigned i = 0; i != function.getNumOfParameters(); ++i) {
    225         PabloAST * var = function.getParameter(i);
    226         const Vertex u = add_vertex(var, G);
    227         Q.push(u);
    228         M[var] = u;
    229     }
    230 
    231     for (;;) {
    232         const Vertex u = Q.front(); Q.pop();
    233         for (PabloAST * user : G[u]->users()) {
    234             auto f = M.find(user);
    235             Vertex v = 0;
    236             if (f == M.end()) {
    237                 v = add_vertex(user, G);
    238                 switch (user->getClassTypeId()) {
    239                     case PabloAST::ClassTypeId::And:
    240                     case PabloAST::ClassTypeId::Or:
    241                     case PabloAST::ClassTypeId::Not:
    242                     case PabloAST::ClassTypeId::Xor:
    243                     case PabloAST::ClassTypeId::Sel:
    244                         Q.push(v);
    245                     default:
    246                         M[user] = v;
    247                 }
    248             } else {
    249                 v = f->second;
    250             }
    251             add_edge(u, v, G);
    252         }
    253 
    254         if (Q.empty()) {
    255             break;
    256         }
    257     }
    258 
    259     flat_set<Statement *> promotions;
    260 
    261     for (Vertex u : make_iterator_range(vertices(G))) {
    262         if (out_degree(u, G) == 0) {
    263             Statement * stmt = cast<Statement>(G[u]);
    264             if (isa<Assign>(stmt)) {
    265                 continue;
    266             }
    267             for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
    268                 if (Statement * expr = dyn_cast<Statement>(stmt->getOperand(i))) {
    269                     promotions.insert(expr);
    270                 }
    271             }
    272         }
    273     }
    274 
    275     for (Statement * promoted : promotions) {
    276         PabloBlock * block = promoted->getParent();
    277         block->setInsertPoint(promoted);
    278         Assign * replacement = block->createAssign("t", promoted);
    279         promoted->replaceAllUsesWith(replacement);
    280     }
    281 
    282     raw_os_ostream out(std::cerr);
    283     PabloPrinter::print(function.getEntryBlock().statements(), out);
    284     out << "**************************************\n";
    285     out.flush();
    286 }
    287 
    288 
    289 /** ------------------------------------------------------------------------------------------------------------- *
    290  * @brief isSimplifiable
    291  ** ------------------------------------------------------------------------------------------------------------- */
    292 inline bool isSimplifiable(const PabloAST * const expr, const PabloBlock * const pb) {
    293     switch (expr->getClassTypeId()) {
    294         case PabloAST::ClassTypeId::And:
    295         case PabloAST::ClassTypeId::Or:
    296         case PabloAST::ClassTypeId::Not:
    297 //        case PabloAST::ClassTypeId::Sel:
    298             return cast<Statement>(expr)->getParent() == pb;
    299         default:
    300             return false;
    301     }
    302 }
    303221
    304222/** ------------------------------------------------------------------------------------------------------------- *
     
    314232            }
    315233            simplifyAST(cast<If>(stmt)->getBody(), std::move(terminals));
    316 //            for (Assign * var : cast<const If>(stmt)->getDefined()) {
    317 //                block.record(var);
    318 //            }
    319 //            continue;
    320234        } else if (isa<While>(stmt)) {
    321235            Terminals terminals;
     
    324238            }
    325239            simplifyAST(cast<While>(stmt)->getBody(), std::move(terminals));
    326 //            for (Next * var : cast<const While>(stmt)->getVariants()) {
    327 //                block.record(var);
     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);
    328264//            }
    329 //            continue;
    330         }
    331         // block.record(stmt);
    332     }
    333 
    334     for (;;) {
    335 
    336         flat_set<Statement *> inputs;
    337         for (Statement * term : terminals) {
    338             for (unsigned i = 0; i != term->getNumOperands(); ++i) {
    339                 if (isSimplifiable(term->getOperand(i), term->getParent())) {
    340                     inputs.insert(cast<Statement>(term->getOperand(i)));
    341                 }
    342             }
    343         }
    344 
    345         if (inputs.empty()) {
    346             break;
    347         }
    348 
    349         std::queue<Statement *> Q;
    350         for (Statement * term : inputs) {
    351             Q.push(term);
    352         }
    353 
    354         flat_set<PabloAST *> visited;
    355         flat_set<PabloAST *> variables;
    356         // find the variables for this set of terminals
    357         for (;;) {
    358             Statement * stmt = Q.front();
    359             Q.pop();
    360             for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
    361                 if (visited.count(stmt->getOperand(i)) == 0) {
    362                     if (isSimplifiable(stmt->getOperand(i), stmt->getParent())) {
    363                         Q.push(cast<Statement>(stmt->getOperand(i)));
    364                     } else {
    365                         variables.insert(stmt->getOperand(i));
    366                     }
    367                     visited.insert(stmt->getOperand(i));
    368                 }
    369             }
    370             if (Q.empty()) {
    371                 break;
    372             }
    373         }
    374 
    375         mVariables.clear();
    376         mManager = Cudd_Init(variables.size(), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
    377         Cudd_AutodynEnable(mManager, CUDD_REORDER_LAZY_SIFT);
    378         for (PabloAST * var : variables) {
    379             mCharacterizationMap.insert(std::make_pair(var, Cudd_bddIthVar(mManager, mVariables.size())));
    380             mVariables.push_back(var);
    381         }
    382 
    383 
    384         std::vector<DdNode *> nodes;
    385         for (PabloAST * term : inputs) {
    386             nodes.push_back(characterizeTerminal(term));
    387         }
    388         Cudd_AutodynDisable(mManager);
    389         Cudd_ReduceHeap(mManager, CUDD_REORDER_SIFT, 0);
    390 
    391         visited.clear();
    392         for (Statement * input : inputs) {
    393             DdNode * const f = mCharacterizationMap[input]; assert (f);
    394             Cudd_Ref(f);
    395             block.setInsertPoint(input);
    396             PabloBuilder builder(block);
    397             PabloAST * replacement = simplifyAST(f, builder);
    398             if (replacement) {
    399                 input->replaceWith(replacement, false, true);
    400             }
    401             Cudd_RecursiveDeref(mManager, f);
    402         }
    403 
    404         Cudd_Quit(mManager);
    405 
    406         mCharacterizationMap.clear();
    407 
    408         // Now clear our terminals and test whether we can process another layer within this block
    409         terminals.clear();
    410         for (PabloAST * var : variables) {
    411             if (LLVM_LIKELY(isa<Statement>(var) && cast<Statement>(var)->getParent() == &block)) {
    412                 terminals.push_back(cast<Statement>(var));
    413             }
    414         }
    415 
    416         if (terminals.empty()) {
    417             break;
    418         }
    419 
    420     }
    421 
    422 }
    423 
    424 /** ------------------------------------------------------------------------------------------------------------- *
    425  * @brief characterizeTerminal
    426  ** ------------------------------------------------------------------------------------------------------------- */
    427 DdNode * BDDMinimizationPass::characterizeTerminal(PabloAST * expr) {
    428     const auto f = mCharacterizationMap.find(expr);
    429     if (f != mCharacterizationMap.end()) {
    430         return f->second;
    431     }
    432     std::array<DdNode *, 3> input;
    433     for (unsigned i = 0; i != cast<Statement>(expr)->getNumOperands(); ++i) {
    434         input[i] = characterizeTerminal(cast<Statement>(expr)->getOperand(i)); assert (input[i]);
    435     }
    436     DdNode * bdd = nullptr;
    437     switch (expr->getClassTypeId()) {
    438         case PabloAST::ClassTypeId::And:
    439             bdd = And(input[0], input[1]);
    440             break;
    441         case PabloAST::ClassTypeId::Or:
    442             bdd = Or(input[0], input[1]);
    443             break;
    444         case PabloAST::ClassTypeId::Not:
    445             bdd = Not(input[0]);
    446             break;
    447 //        case PabloAST::ClassTypeId::Sel:
    448 //            bdd = Ite(input[0], input[1], input[2]);
     265//        }
     266//        if (Q.empty()) {
    449267//            break;
    450         default:
    451             return nullptr;
    452     }
    453     Cudd_Ref(bdd);
    454     mCharacterizationMap.insert(std::make_pair(expr, bdd));
    455     return bdd;
    456 }
     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
    457296
    458297/** ------------------------------------------------------------------------------------------------------------- *
    459298 * @brief simplifyAST
    460299 ** ------------------------------------------------------------------------------------------------------------- */
    461 PabloAST * BDDMinimizationPass::simplifyAST(DdNode * const f, PabloBuilder &block) {
    462     assert (!noSatisfyingAssignment(f));
     300PabloAST * BDDMinimizationPass::simplifyAST(DdNode * const f, PabloBlock &block) {
     301
    463302    DdNode * g = Cudd_FindEssential(mManager, f);
     303
    464304    if (g && Cudd_SupportSize(mManager, g) > 0) {
    465305        if (g == f) { // every variable is essential
     
    484324        Cudd_RecursiveDeref(mManager, g);
    485325        Cudd_RecursiveDeref(mManager, h);
    486         return block.createAnd(c0, c1, "t");
     326        return block.createAnd(c0, c1, "e");
    487327    }
    488328
     
    512352
    513353    if ((decomp[0] != decomp[1]) && (decomp[0] != f) && (decomp[1] != f)) {
     354
    514355        Cudd_Ref(decomp[0]);
    515356        Cudd_Ref(decomp[1]);
     
    529370
    530371        if (disjuncts == 2) {
    531             return block.createOr(d0, d1, "t");
     372            return block.createOr(d0, d1, "d");
    532373        } else {
    533             return block.createAnd(d0, d1, "t");
     374            return block.createAnd(d0, d1, "c");
    534375        }
    535376    }
    536377    return makeCoverAST(f, block);
    537378}
     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//}
    538409
    539410/** ------------------------------------------------------------------------------------------------------------- *
    540411 * @brief makeCoverAST
    541412 ** ------------------------------------------------------------------------------------------------------------- */
    542 PabloAST * BDDMinimizationPass::makeCoverAST(DdNode * const f, PabloBuilder & block) {
     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);
    543421
    544422    std::queue<PabloAST *> SQ;
    545     const auto n = mVariables.size();
    546423    circular_buffer<PabloAST *> CQ(n + 1);
    547424    circular_buffer<PabloAST *> DQ(n + 1);
    548425
    549     assert (mManager->size == n);
    550 
    551426    int cube[n];
    552 
    553     DdNode * g = f;
    554 
    555     Cudd_Ref(g);
    556427
    557428    while (g != Cudd_ReadLogicZero(mManager)) {
     
    595466            if (cube[i] == 0) {
    596467                DQ.push_back(mVariables[i]);
    597                 // CQ.push_back(block.createOnes());
    598468            } else if (cube[i] == 1) {
    599469                CQ.push_back(mVariables[i]);
    600                 // DQ.push_back(block.createZeroes());
    601470            }
    602471        }
     
    624493        SQ.push(CQ.front()); CQ.pop_front();
    625494    }
     495
    626496    Cudd_RecursiveDeref(mManager, g);
     497
    627498    if (LLVM_UNLIKELY(SQ.empty())) {
    628499        throw std::runtime_error("Error! statement queue empty!");
    629500    }
     501
    630502    while (SQ.size() > 1) {
    631503        PabloAST * v1 = SQ.front(); SQ.pop();
     
    634506    }
    635507    return SQ.front();
    636 }
     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//}
    637803
    638804/** ------------------------------------------------------------------------------------------------------------- *
     
    693859inline void BDDMinimizationPass::shutdown() {
    694860    Cudd_Quit(mManager);
     861    mCharacterizationMap.clear();
     862    mVariables.clear();
    695863}
    696864
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_bddminimization.h

    r4727 r4736  
    4949    void simplifyAST(PabloBlock & block, Terminals && terminals);
    5050    DdNode * characterizeTerminal(PabloAST * expr);
    51     PabloAST * simplifyAST(DdNode * const f, PabloBuilder &block);
    52     PabloAST * makeCoverAST(DdNode * const f, PabloBuilder &block);
     51    PabloAST * simplifyAST(DdNode * const f, PabloBlock &block);
     52    PabloAST * makeCoverAST(DdNode * const f, PabloBlock &block);
    5353private:
    5454    DdNode * Zero() const;
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_simplifier.cpp

    r4699 r4736  
    228228                    }
    229229                }
    230             }
    231             // If an AND, OR or XOR instruction has two Advance instructions as inputs and neither Advance
    232             // has another user and both shift their input by the same amount, we can perform the AND, OR
    233             // or XOR on the inputs to the Advances and remove one of the Advance statements.
    234             else if (LLVM_UNLIKELY(isa<Advance>(stmt->getOperand(1)) && isa<Advance>(stmt->getOperand(0)))) {
     230            } else if (LLVM_UNLIKELY(isa<Advance>(stmt->getOperand(1)) && isa<Advance>(stmt->getOperand(0)))) {
     231                // If an AND, OR or XOR instruction has two Advance instructions as inputs and neither Advance
     232                // has another user and both shift their input by the same amount, we can perform the AND, OR
     233                // or XOR on the inputs to the Advances and remove one of the Advance statements.
     234
    235235                Advance * const a0 = cast<Advance>(stmt->getOperand(0));
    236236                Advance * const a1 = cast<Advance>(stmt->getOperand(1));
     
    252252                    default: break;
    253253                }
    254             }
    255             else if (LLVM_UNLIKELY(isa<MatchStar>(stmt->getOperand(1)) && isa<MatchStar>(stmt->getOperand(0))) && isa<Or>(stmt)) {
    256 
    257 
    258             }
     254            } else if (LLVM_UNLIKELY(isa<MatchStar>(stmt->getOperand(1)) && isa<MatchStar>(stmt->getOperand(0))) && isa<Or>(stmt)) {
     255
     256
     257            } /*else if (LLVM_UNLIKELY(isa<Or>(stmt) && isa<And>(stmt->getOperand(0)) && isa<And>(stmt->getOperand(1)))) {
     258
     259                // If we have an OR(AND(A,B),AND(NOT(A),C)) statement and neither of the inner operands are used elsewhere, we can
     260                // promote the Or to a Sel statement.
     261
     262                And * const a0 = cast<And>(stmt->getOperand(0));
     263                And * const a1 = cast<And>(stmt->getOperand(1));
     264
     265                if (LLVM_UNLIKELY(a0->getNumUses() == 1 && a1->getNumUses() == 1)) {
     266
     267                    bool neg[4] = { false, false, false, false };
     268
     269                    for (unsigned i = 0; i != 2; ++i) {
     270                        if (isa<Not>(a0->getOperand(i))) {
     271                            PabloAST * i0 = cast<Not>(a0->getOperand(i))->getOperand(0);
     272                            for (unsigned j = 0; j != 2; ++j) {
     273                                if (a0->getOperand(j) == i0) {
     274                                    neg[i + j * 2] = true;
     275                                }
     276                            }
     277                        }
     278                    }
     279
     280
     281
     282
     283
     284
     285
     286
     287
     288                }
     289
     290            }*/
    259291        }
    260292        stmt = stmt->getNextNode();
Note: See TracChangeset for help on using the changeset viewer.