Ignore:
Timestamp:
Sep 14, 2016, 2:56:54 PM (3 years ago)
Author:
nmedfort
Message:

Work on multiplexing and distribution passes + a few AST modification bug fixes.

File:
1 edited

Legend:

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

    r5152 r5156  
    1414#include <llvm/Support/CommandLine.h>
    1515#include "maxsat.hpp"
     16
     17//  noif-dist-mult-dist-50 \p{Cham}(?<!\p{Mc})
    1618
    1719using namespace boost;
     
    273275    Z3_context ctx = Z3_mk_context(cfg);
    274276    Z3_del_config(cfg);
    275     Z3_solver solver = Z3_mk_solver(ctx);
    276     Z3_solver_inc_ref(ctx, solver);
    277 
    278     BooleanReassociationPass brp(ctx, solver, function);
     277
     278    Z3_params params = Z3_mk_params(ctx);
     279    Z3_params_inc_ref(ctx, params);
     280    Z3_params_set_bool(ctx, params, Z3_mk_string_symbol(ctx, "pull_cheap_ite"), true);
     281    Z3_params_set_bool(ctx, params, Z3_mk_string_symbol(ctx, "local_ctx"), true);
     282
     283    Z3_tactic ctx_solver_simplify = Z3_mk_tactic(ctx, "ctx-solver-simplify");
     284    Z3_tactic_inc_ref(ctx, ctx_solver_simplify);
     285
     286    BooleanReassociationPass brp(ctx, params, ctx_solver_simplify, function);
    279287    brp.processScopes(function);
    280288
    281     Z3_solver_dec_ref(ctx, solver);
     289    Z3_params_dec_ref(ctx, params);
     290    Z3_tactic_dec_ref(ctx, ctx_solver_simplify);
    282291    Z3_del_context(ctx);
     292
     293    PabloVerifier::verify(function, "post-reassociation");
    283294
    284295    Simplifier::optimize(function);
     
    308319 ** ------------------------------------------------------------------------------------------------------------- */
    309320void BooleanReassociationPass::processScopes(PabloBlock * const block, CharacterizationMap & map) {
    310     Z3_solver_push(mContext, mSolver);
    311321    for (Statement * stmt = block->front(); stmt; ) {
    312322        if (LLVM_UNLIKELY(isa<If>(stmt))) {
     
    335345            stmt = characterize(stmt, map);
    336346        }
    337     }
     347    }   
    338348    distributeScope(block, map);
    339     Z3_solver_pop(mContext, mSolver, 1);
    340349}
    341350
     
    385394        return stmt->getNextNode();
    386395    }
    387     node = Z3_simplify(mContext, node); assert (node);
     396    node = simplify(node); assert (node);
    388397    PabloAST * const replacement = map.findKey(node);
    389398    if (LLVM_LIKELY(replacement == nullptr)) {
     
    399408 * @brief processScope
    400409 ** ------------------------------------------------------------------------------------------------------------- */
    401 inline void BooleanReassociationPass::distributeScope(PabloBlock * const block, CharacterizationMap & map) {
     410inline void BooleanReassociationPass::distributeScope(PabloBlock * const block, CharacterizationMap & C) {
    402411    Graph G;
    403412    try {
    404         transformAST(block, map, G);
     413        mBlock = block;
     414        transformAST(C, G);
    405415    } catch (std::runtime_error err) {
    406         printGraph(G, "G");
     416        printGraph(G, "E");
     417        throw err;
     418    } catch (std::exception err) {
     419        printGraph(G, "E");
    407420        throw err;
    408421    }
     
    415428 * are "flattened" (i.e., allowed to have any number of inputs.)
    416429 ** ------------------------------------------------------------------------------------------------------------- */
    417 void BooleanReassociationPass::transformAST(PabloBlock * const block, CharacterizationMap & C, Graph & G) {
     430void BooleanReassociationPass::transformAST(CharacterizationMap & C, Graph & G) {
     431
    418432    StatementMap S;
     433
    419434    // Compute the base def-use graph ...
    420     for (Statement * stmt : *block) {
     435    for (Statement * stmt : *mBlock) {
    421436
    422437        const Vertex u = makeVertex(stmt->getClassTypeId(), stmt, S, G, C.get(stmt));
     
    433448                const Vertex v = makeVertex(TypeId::Var, def, C, S, G);
    434449                add_edge(def, u, v, G);
    435                 resolveNestedUsages(block, def, v, C, S, G, stmt);
     450                resolveNestedUsages(def, v, C, S, G, stmt);
    436451            }
    437452        } else if (LLVM_UNLIKELY(isa<While>(stmt))) {
     
    447462                remove_edge(v, u, G);
    448463                add_edge(var, u, v, G);
    449                 resolveNestedUsages(block, var, v, C, S, G, stmt);
    450             }
    451         } else {           
    452             resolveNestedUsages(block, stmt, u, C, S, G, stmt);
    453         }
    454     }
    455 
    456     if (redistributeGraph(C, S, G)) {
     464                resolveNestedUsages(var, v, C, S, G, stmt);
     465            }
     466        } else {
     467            resolveNestedUsages(stmt, u, C, S, G, stmt);
     468        }
     469    }
     470
     471//    printGraph(G, "G");
     472
     473    VertexMap M;
     474    if (redistributeGraph(C, M, G)) {
    457475        factorGraph(G);
    458         rewriteAST(block, G);
     476
     477//        printGraph(G, "H");
     478
     479        rewriteAST(C, M, G);
    459480        mModified = true;
    460481    }
     
    465486 * @brief resolveNestedUsages
    466487 ** ------------------------------------------------------------------------------------------------------------- */
    467 void BooleanReassociationPass::resolveNestedUsages(PabloBlock * const block, PabloAST * const expr, const Vertex u,
     488void BooleanReassociationPass::resolveNestedUsages(PabloAST * const expr, const Vertex u,
    468489                                                   CharacterizationMap & C, StatementMap & S, Graph & G,
    469490                                                   const Statement * const ignoreIfThis) const {
     
    472493        if (LLVM_LIKELY(user != expr && isa<Statement>(user))) {
    473494            PabloBlock * parent = cast<Statement>(user)->getParent(); assert (parent);
    474             if (LLVM_UNLIKELY(parent != block)) {
     495            if (LLVM_UNLIKELY(parent != mBlock)) {
    475496                for (;;) {
    476                     if (parent->getParent() == block) {
     497                    if (parent->getParent() == mBlock) {
    477498                        Statement * const branch = parent->getBranch();
    478499                        if (LLVM_UNLIKELY(branch != ignoreIfThis)) {
     
    757778 * Apply the distribution law to reduce computations whenever possible.
    758779 ** ------------------------------------------------------------------------------------------------------------- */
    759 bool BooleanReassociationPass::redistributeGraph(CharacterizationMap & C, StatementMap & M, Graph & G) const {
     780bool BooleanReassociationPass::redistributeGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const {
    760781
    761782    bool modified = false;
     
    763784    DistributionGraph H;
    764785
    765     contractGraph(M, G);
     786    contractGraph(G);
    766787
    767788    for (;;) {
     
    829850            H.clear();
    830851
    831             contractGraph(M, G);
     852            contractGraph(G);
    832853        }
    833854
    834855        // Although exceptionally unlikely, it's possible that if we can reduce the graph, we could
    835856        // further simplify it. Restart the process if and only if we succeed.
    836         if (LLVM_UNLIKELY(reduceGraph(C, M, G))) {
    837             if (LLVM_UNLIKELY(contractGraph(M, G))) {
     857        if (reduceGraph(C, M, G)) {
     858            if (LLVM_UNLIKELY(contractGraph(G))) {
    838859                H.clear();
    839860                continue;
     
    865886
    866887/** ------------------------------------------------------------------------------------------------------------- *
     888 * @brief unique_source
     889 ** ------------------------------------------------------------------------------------------------------------- */
     890inline bool has_unique_source(const Vertex u, const Graph & G) {
     891    if (in_degree(u, G) > 0) {
     892        graph_traits<Graph>::in_edge_iterator i, end;
     893        std::tie(i, end) = in_edges(u, G);
     894        const Vertex v = source(*i, G);
     895        while (++i != end) {
     896            if (source(*i, G) != v) {
     897                return false;
     898            }
     899        }
     900        return true;
     901    }
     902    return false;
     903}
     904
     905/** ------------------------------------------------------------------------------------------------------------- *
     906 * @brief unique_target
     907 ** ------------------------------------------------------------------------------------------------------------- */
     908inline bool has_unique_target(const Vertex u, const Graph & G) {
     909    if (out_degree(u, G) > 0) {
     910        graph_traits<Graph>::out_edge_iterator i, end;
     911        std::tie(i, end) = out_edges(u, G);
     912        const Vertex v = target(*i, G);
     913        while (++i != end) {
     914            if (target(*i, G) != v) {
     915                return false;
     916            }
     917        }
     918        return true;
     919    }
     920    return false;
     921}
     922
     923
     924/** ------------------------------------------------------------------------------------------------------------- *
    867925 * @brief contractGraph
    868926 ** ------------------------------------------------------------------------------------------------------------- */
    869 bool BooleanReassociationPass::contractGraph(StatementMap & M, Graph & G) const {
     927bool BooleanReassociationPass::contractGraph(Graph & G) const {
    870928
    871929    bool contracted = false;
     
    881939        } else if (LLVM_LIKELY(out_degree(u, G) > 0)) {
    882940            if (isAssociative(G[u])) {
    883                 if (LLVM_UNLIKELY(in_degree(u, G) == 1)) {
     941                if (LLVM_UNLIKELY(has_unique_source(u, G))) {
    884942                    // We have a redundant node here that'll simply end up being a duplicate
    885943                    // of the input value. Remove it and add any of its outgoing edges to its
     
    888946                    const Vertex v = source(ei, G);
    889947                    for (auto ej : make_iterator_range(out_edges(u, G))) {
    890                         const Vertex w = target(ej, G);
    891                         add_edge(G[ei], v, w, G);
    892                     }
    893                     removeVertex(u, M, G);
     948                        add_edge(G[ej], v, target(ej, G), G);
     949                    }
     950//                    if (LLVM_UNLIKELY(getValue(G[v]) == nullptr && getValue(G[u]) != nullptr)) {
     951//                        getValue(G[v]) = getValue(G[u]);
     952//                    }
     953                    removeVertex(u, G);
    894954                    contracted = true;
    895                 } else if (LLVM_UNLIKELY(out_degree(u, G) == 1)) {
     955                } else if (LLVM_UNLIKELY(has_unique_target(u, G))) {
    896956                    // Otherwise if we have a single user, we have a similar case as above but
    897957                    // we can only merge this vertex into the outgoing instruction if they are
     
    901961                    if (LLVM_UNLIKELY(getType(G[v]) == getType(G[u]))) {
    902962                        for (auto ej : make_iterator_range(in_edges(u, G))) {
    903                             add_edge(G[ei], source(ej, G), v, G);
     963                            add_edge(G[ej], source(ej, G), v, G);
    904964                        }
    905                         removeVertex(u, M, G);
     965                        if (LLVM_UNLIKELY(getValue(G[v]) == nullptr && getValue(G[u]) != nullptr)) {
     966                            getValue(G[v]) = getValue(G[u]);
     967                        }
     968                        removeVertex(u, G);
    906969                        contracted = true;
    907                     }                   
     970                    }
    908971                }
    909972            }
    910973        } else if (LLVM_UNLIKELY(isNonEscaping(G[u]))) {
    911             removeVertex(u, M, G);
     974            removeVertex(u, G);
    912975            contracted = true;
    913976        }
     
    933996 * @brief reduceGraph
    934997 ** ------------------------------------------------------------------------------------------------------------- */
    935 bool BooleanReassociationPass::reduceGraph(CharacterizationMap & C, StatementMap & S, Graph & G) const {
     998bool BooleanReassociationPass::reduceVertex(const Vertex u, CharacterizationMap & C, VertexMap & M, Graph & G, const bool use_expensive_simplification) const {
    936999
    9371000    bool reduced = false;
    9381001
    939     VertexMap M;
     1002    assert (isReducible(G[u]));
     1003
     1004    Z3_ast node = getDefinition(G[u]);
     1005    if (isAssociative(G[u])) {
     1006        const TypeId typeId = getType(G[u]);
     1007        if (node == nullptr) {
     1008            const auto n = in_degree(u, G); assert (n > 1);
     1009            Z3_ast operands[n];
     1010            unsigned i = 0;
     1011            for (auto e : make_iterator_range(in_edges(u, G))) {
     1012                const Vertex v = source(e, G);
     1013                assert (getDefinition(G[v]));
     1014                operands[i++] = getDefinition(G[v]);
     1015            }
     1016            switch (typeId) {
     1017                case TypeId::And:
     1018                    node = Z3_mk_and(mContext, n, operands);
     1019                    break;
     1020                case TypeId::Or:
     1021                    node = Z3_mk_or(mContext, n, operands);
     1022                    break;
     1023                case TypeId::Xor:
     1024                    node = Z3_mk_xor(mContext, operands[0], operands[1]);
     1025                    for (unsigned i = 2; LLVM_UNLIKELY(i < n); ++i) {
     1026                        node = Z3_mk_xor(mContext, node, operands[i]);
     1027                    }
     1028                    break;
     1029                default: llvm_unreachable("unexpected type id");
     1030            }
     1031            assert (node);
     1032            getDefinition(G[u]) = node;
     1033        }
     1034
     1035        graph_traits<Graph>::in_edge_iterator begin, end;
     1036restart:if (in_degree(u, G) > 1) {
     1037            std::tie(begin, end) = in_edges(u, G);
     1038            for (auto i = begin; ++i != end; ) {
     1039                const auto v = source(*i, G);
     1040                for (auto j = begin; j != i; ++j) {
     1041                    const auto w = source(*j, G);
     1042                    Z3_ast operands[2] = { getDefinition(G[v]), getDefinition(G[w]) };
     1043                    Z3_ast test = nullptr;
     1044                    switch (typeId) {
     1045                        case TypeId::And:
     1046                            test = Z3_mk_and(mContext, 2, operands); break;
     1047                        case TypeId::Or:
     1048                            test = Z3_mk_or(mContext, 2, operands); break;
     1049                        case TypeId::Xor:
     1050                            test = Z3_mk_xor(mContext, operands[0], operands[1]); break;
     1051                        default:
     1052                            llvm_unreachable("impossible type id");
     1053                    }
     1054                    assert (test);
     1055                    test = simplify(test, use_expensive_simplification);
     1056
     1057                    bool replacement = false;
     1058                    Vertex x = 0;
     1059                    const auto f = M.find(test);
     1060                    if (LLVM_UNLIKELY(f != M.end())) {
     1061                        x = f->second;
     1062                        assert (getDefinition(G[x]) == test);
     1063                        replacement = true;
     1064                    } else {
     1065                        PabloAST * const factor = C.findKey(test);
     1066                        if (LLVM_UNLIKELY(!inCurrentBlock(factor, mBlock))) {
     1067                            x = makeVertex(TypeId::Var, factor, G, test);
     1068                            M.emplace(test, x);
     1069                            replacement = true;
     1070                        }
     1071                    }
     1072
     1073                    if (LLVM_UNLIKELY(replacement)) {
     1074
     1075                        // note: unless both edges carry an Pablo AST replacement value, they will converge into a single edge.
     1076                        PabloAST * const r1 = G[*i];
     1077                        PabloAST * const r2 = G[*j];
     1078
     1079                        remove_edge(*i, G);
     1080                        remove_edge(*j, G);
     1081
     1082                        if (LLVM_UNLIKELY(r1 && r2)) {
     1083                            add_edge(r1, x, u, G);
     1084                            add_edge(r2, x, u, G);
     1085                        } else {
     1086                            add_edge(r1 ? r1 : r2, x, u, G);
     1087                        }
     1088
     1089                        reduced = true;
     1090                        goto restart;
     1091                    }
     1092                }
     1093            }
     1094        }
     1095    }
     1096
     1097    if (LLVM_UNLIKELY(node == nullptr)) {
     1098        throw std::runtime_error("No Z3 characterization for vertex " + std::to_string(u));
     1099    }
     1100
     1101    auto f = M.find(node);
     1102    if (LLVM_LIKELY(f == M.end())) {
     1103        M.emplace(node, u);
     1104    } else if (isAssociative(G[u])) {
     1105        const Vertex v = f->second;
     1106        for (auto e : make_iterator_range(out_edges(u, G))) {
     1107            add_edge(G[e], v, target(e, G), G);
     1108        }
     1109        removeVertex(u, G);
     1110        reduced = true;
     1111    }
     1112
     1113    return reduced;
     1114}
     1115
     1116/** ------------------------------------------------------------------------------------------------------------- *
     1117 * @brief reduceGraph
     1118 ** ------------------------------------------------------------------------------------------------------------- */
     1119bool BooleanReassociationPass::reduceGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const {
     1120
     1121    bool reduced = false;
     1122
    9401123    circular_buffer<Vertex> ordering(num_vertices(G));
    9411124
    9421125    topological_sort(G, std::front_inserter(ordering)); // topological ordering
     1126
     1127    M.clear();
    9431128
    9441129    // first contract the graph
    9451130    for (const Vertex u : ordering) {
    9461131        if (isReducible(G[u])) {
    947             Z3_ast & node = getDefinition(G[u]);
    948             if (isAssociative(G[u])) {
    949                 const TypeId typeId = getType(G[u]);
    950                 if (node == nullptr) {
    951                     const auto n = in_degree(u, G); assert (n > 1);
    952                     Z3_ast operands[n];
    953                     unsigned i = 0;
    954                     for (auto e : make_iterator_range(in_edges(u, G))) {
    955                         const Vertex v = source(e, G);
    956                         assert (getDefinition(G[v]));
    957                         operands[i++] = getDefinition(G[v]);
    958                     }
    959                     switch (typeId) {
    960                         case TypeId::And:
    961                             node = Z3_mk_and(mContext, n, operands);
    962                             break;
    963                         case TypeId::Or:
    964                             node = Z3_mk_or(mContext, n, operands);
    965                             break;
    966                         case TypeId::Xor:
    967                             node = Z3_mk_xor(mContext, operands[0], operands[1]);
    968                             for (unsigned i = 2; LLVM_UNLIKELY(i < n); ++i) {
    969                                 node = Z3_mk_xor(mContext, node, operands[i]);
    970                             }
    971                             break;
    972                         default: llvm_unreachable("unexpected type id");
    973                     }
    974 
    975                     assert (node);
    976                     node = Z3_simplify(mContext, node);
    977                 }
    978                 graph_traits<Graph>::in_edge_iterator begin, end;
    979 restart:        if (in_degree(u, G) > 1) {
    980                     std::tie(begin, end) = in_edges(u, G);
    981                     for (auto i = begin; ++i != end; ) {
    982                         const auto v = source(*i, G);
    983                         for (auto j = begin; j != i; ++j) {
    984                             const auto w = source(*j, G);
    985                             Z3_ast operands[2] = { getDefinition(G[v]), getDefinition(G[w]) };
    986                             assert (operands[0]);
    987                             assert (operands[1]);
    988                             Z3_ast test = nullptr;
    989                             switch (typeId) {
    990                                 case TypeId::And:
    991                                     test = Z3_mk_and(mContext, 2, operands); break;
    992                                 case TypeId::Or:
    993                                     test = Z3_mk_or(mContext, 2, operands); break;
    994                                 case TypeId::Xor:
    995                                     test = Z3_mk_xor(mContext, operands[0], operands[1]); break;
    996                                 default:
    997                                     llvm_unreachable("impossible type id");
    998                             }
    999                             assert (test);
    1000                             test = Z3_simplify(mContext, test);
    1001                             PabloAST * const factor = C.findKey(test);
    1002                             if (LLVM_UNLIKELY(factor != nullptr)) {
    1003                                 const Vertex a = makeVertex(TypeId::Var, factor, S, G, test);
    1004                                 // note: unless both edges carry an Pablo AST replacement value, they will converge into a single edge.
    1005                                 PabloAST * const r1 = G[*i];
    1006                                 PabloAST * const r2 = G[*j];
    1007 
    1008                                 remove_edge(*i, G);
    1009                                 remove_edge(*j, G);
    1010 
    1011                                 if (LLVM_UNLIKELY(r1 && r2)) {
    1012                                     add_edge(r1, a, u, G);
    1013                                     add_edge(r2, a, u, G);
    1014                                 } else {
    1015                                     add_edge(r1 ? r1 : r2, a, u, G);
    1016                                 }
    1017 
    1018 //                                errs() << " -- subsituting (" << a << ',' << u << ")=" << Z3_ast_to_string(mContext, test)
    1019 //                                       << " for (" << v << ',' << u << ")=" << Z3_ast_to_string(mContext, getDefinition(G[v]));
    1020 
    1021 //                                switch (typeId) {
    1022 //                                    case TypeId::And:
    1023 //                                        errs() << " ∧ "; break;
    1024 //                                    case TypeId::Or:
    1025 //                                        errs() << " √ ";  break;
    1026 //                                    case TypeId::Xor:
    1027 //                                        errs() << " ⊕ ";  break;
    1028 //                                    default:
    1029 //                                        llvm_unreachable("impossible type id");
    1030 //                                }
    1031 
    1032 //                                errs() << "(" << w << ',' << u << ")=" << Z3_ast_to_string(mContext, getDefinition(G[w]))
    1033 //                                       << "\n";
    1034 
    1035                                 reduced = true;
    1036                                 goto restart;
    1037                             }
    1038                         }
    1039                     }
    1040                 }
    1041             }
    1042 
    1043             if (LLVM_UNLIKELY(node == nullptr)) {
    1044                 throw std::runtime_error("No Z3 characterization for vertex " + std::to_string(u));
    1045             }
    1046 
    1047             auto f = M.find(node);
    1048             if (LLVM_LIKELY(f == M.end())) {
    1049                 M.emplace(node, u);
    1050             } else if (isAssociative(G[u])) {
    1051                 const Vertex v = f->second;
    1052 
    1053 //                errs() << " -- subsituting " << u << ":=\n" << Z3_ast_to_string(mContext, getDefinition(G[u]))
    1054 //                       << "\n for " << v << ":=\n" << Z3_ast_to_string(mContext, getDefinition(G[v])) << "\n";
    1055 
    1056                 for (auto e : make_iterator_range(out_edges(u, G))) {
    1057                     add_edge(G[e], v, target(e, G), G);
    1058                 }
    1059                 removeVertex(u, S, G);
     1132            if (reduceVertex(u, C, M, G, false)) {
    10601133                reduced = true;
    10611134            }
     
    10781151    bool modified = false;
    10791152
    1080     for (auto i = factors.begin(); ++i != factors.end(); ) {
    1081         assert (getType(G[*i]) == typeId);
    1082         for (auto ei : make_iterator_range(in_edges(*i, G))) {
     1153    for (unsigned i = 1; i < factors.size(); ++i) {
     1154        assert (getType(G[factors[i]]) == typeId);
     1155        for (auto ei : make_iterator_range(in_edges(factors[i], G))) {
    10831156            I.push_back(source(ei, G));
    10841157        }
    10851158        std::sort(I.begin(), I.end());
    1086         for (auto j = factors.begin(); j != i; ++j) {
    1087             for (auto ej : make_iterator_range(in_edges(*j, G))) {
     1159        for (unsigned j = 0; j < i; ++j) {
     1160            for (auto ej : make_iterator_range(in_edges(factors[j], G))) {
    10881161                J.push_back(source(ej, G));
    10891162            }
     
    10951168            const auto n = K.size();
    10961169            if (n > 1) {
    1097                 Vertex a = *i;
    1098                 Vertex b = *j;
     1170                Vertex a = factors[i];
     1171                Vertex b = factors[j];
    10991172                if (LLVM_UNLIKELY(in_degree(a, G) == n || in_degree(b, G) == n)) {
    11001173                    if (in_degree(a, G) != n) {
     
    11651238 * @brief rewriteAST
    11661239 ** ------------------------------------------------------------------------------------------------------------- */
    1167 void BooleanReassociationPass::rewriteAST(PabloBlock * const block, Graph & G) {
     1240bool BooleanReassociationPass::rewriteAST(CharacterizationMap & C, VertexMap & M, Graph & G) {
    11681241
    11691242    using line_t = long long int;
     
    11721245
    11731246    Z3_config cfg = Z3_mk_config();
    1174     Z3_set_param_value(cfg, "MODEL", "true");
     1247    Z3_set_param_value(cfg, "model", "true");
    11751248    Z3_context ctx = Z3_mk_context(cfg);
    11761249    Z3_del_config(cfg);
     
    11801253    std::vector<Z3_ast> mapping(num_vertices(G), nullptr);
    11811254
    1182     flat_map<PabloAST *, Z3_ast> M;
     1255    flat_map<PabloAST *, Z3_ast> V;
    11831256
    11841257    // Generate the variables
     
    11891262        const auto var = Z3_mk_fresh_const(ctx, nullptr, ty);
    11901263        Z3_ast constraint = nullptr;
    1191         if (in_degree(u, G) == 0) {
    1192             constraint = Z3_mk_eq(ctx, var, ZERO);
    1193         } else {
     1264        if (in_degree(u, G) > 0) {
    11941265            constraint = Z3_mk_gt(ctx, var, ZERO);
    1195         }
    1196         Z3_solver_assert(ctx, solver, constraint);
    1197 
     1266            Z3_solver_assert(ctx, solver, constraint);
     1267        }       
    11981268        PabloAST * const expr = getValue(G[u]);
    1199         if (expr) {
    1200             const bool added = M.emplace(expr, var).second;
    1201             assert ("G contains duplicate vertices for the same statement!" && added);
     1269        if (inCurrentBlock(expr, mBlock)) {
     1270            V.emplace(expr, var);
    12021271        }
    12031272        mapping[u] = var;
     
    12151284    // Compute the soft ordering constraints
    12161285    std::vector<Z3_ast> ordering(0);
    1217     ordering.reserve(2 * M.size() - 1);
     1286    ordering.reserve(V.size() - 1);
    12181287
    12191288    Z3_ast prior = nullptr;
    12201289    unsigned gap = 1;
    1221     for (Statement * stmt : *block) {
    1222         auto f = M.find(stmt);
    1223         if (f != M.end()) {
     1290    for (Statement * stmt : *mBlock) {
     1291        auto f = V.find(stmt);
     1292        if (f != V.end()) {
    12241293            Z3_ast const node = f->second;
    12251294            if (prior) {
    1226                 ordering.push_back(Z3_mk_lt(ctx, prior, node));
     1295//                ordering.push_back(Z3_mk_lt(ctx, prior, node)); // increases the cost by 6 - 10x
    12271296                Z3_ast ops[2] = { node, prior };
    12281297                ordering.push_back(Z3_mk_le(ctx, Z3_mk_sub(ctx, 2, ops), Z3_mk_int(ctx, gap, ty)));
    12291298            } else {
    12301299                ordering.push_back(Z3_mk_eq(ctx, node, Z3_mk_int(ctx, gap, ty)));
    1231 
    12321300            }
    12331301            prior = node;
     
    12701338    std::sort(S.begin(), S.end(), [&L](const Vertex u, const Vertex v){ return L[u] < L[v]; });
    12711339
    1272     block->setInsertPoint(nullptr);
     1340    mBlock->setInsertPoint(nullptr);
    12731341
    12741342    std::vector<Vertex> T;
     
    12881356            }
    12891357
    1290             Statement * ip = block->getInsertPoint();
    1291             ip = ip ? ip->getNextNode() : block->front();
     1358            Statement * ip = mBlock->getInsertPoint();
     1359            ip = ip ? ip->getNextNode() : mBlock->front();
    12921360
    12931361            const auto typeId = getType(G[u]);
    12941362
    1295             T.reserve(in_degree(u, G));
    1296             for (const auto e : make_iterator_range(in_edges(u, G))) {
    1297                 T.push_back(source(e, G));
    1298             }
    1299 
    1300             // Then sort them by their line position (noting any incoming value will either be 0 or MAX_INT)
    1301             std::sort(T.begin(), T.end(), [&L](const Vertex u, const Vertex v){ return L[u] < L[v]; });
    1302             if (LoadEarly) {
    1303                 block->setInsertPoint(nullptr);
    1304             }
    1305 
    1306             circular_buffer<PabloAST *> Q(2); // in_degree(u, G));
    1307             for (auto u : T) {
    1308                 PabloAST * expr = getValue(G[u]);
    1309                 if (LLVM_UNLIKELY(expr == nullptr)) {
    1310                     throw std::runtime_error("Vertex " + std::to_string(u) + " does not have an expression!");
    1311                 }
    1312                 Q.push_back(expr);
    1313                 if (Q.size() > 1) {
    1314 
    1315                     PabloAST * e1 = Q.front(); Q.pop_front();
    1316                     PabloAST * e2 = Q.front(); Q.pop_front();
    1317 
    1318                     if (in_degree(u, G) > 0) {
    1319                         if (LLVM_UNLIKELY(!dominates(e1, e2))) {
    1320                             std::string tmp;
    1321                             raw_string_ostream out(tmp);
    1322                             out << "e1: ";
    1323                             PabloPrinter::print(e1, out);
    1324                             out << " does not dominate e2: ";
    1325                             PabloPrinter::print(e2, out);
    1326                             throw std::runtime_error(out.str());
     1363            PabloAST * expr = nullptr;
     1364
     1365            for (;;) {
     1366
     1367                T.reserve(in_degree(u, G));
     1368                for (const auto e : make_iterator_range(in_edges(u, G))) {
     1369                    T.push_back(source(e, G));
     1370                }
     1371
     1372                // Then sort them by their line position (noting any incoming value will either be 0 or MAX_INT)
     1373                std::sort(T.begin(), T.end(), [&L](const Vertex u, const Vertex v){ return L[u] < L[v]; });
     1374
     1375                if (LoadEarly) {
     1376                    mBlock->setInsertPoint(nullptr);
     1377                }
     1378
     1379                bool done = true;
     1380
     1381                PabloAST * join = nullptr;
     1382
     1383                for (auto v : T) {
     1384                    expr = getValue(G[v]);
     1385                    if (LLVM_UNLIKELY(expr == nullptr)) {
     1386                        throw std::runtime_error("Vertex " + std::to_string(v) + " does not have an expression!");
     1387                    }
     1388                    if (join) {
     1389
     1390                        if (in_degree(v, G) > 0) {
     1391
     1392                            assert (L[v] > 0 && L[v] < MAX_INT);
     1393
     1394                            Statement * dom = cast<Statement>(expr);
     1395                            for (;;) {
     1396                                PabloBlock * const parent = dom->getParent();
     1397                                if (parent == mBlock) {
     1398                                    break;
     1399                                }
     1400                                dom = parent->getBranch(); assert(dom);
     1401                            }
     1402                            mBlock->setInsertPoint(dom);
     1403
     1404                            assert (dominates(join, expr));
     1405                            assert (dominates(expr, ip));
     1406                            assert (dominates(dom, ip));
    13271407                        }
    1328                         assert (dominates(e1, e2));
    1329                         assert (dominates(e2, ip));
    1330                         Statement * dom = cast<Statement>(expr);
    1331                         for (;;) {
    1332                             PabloBlock * const parent = dom->getParent();
    1333                             if (parent == block) {
    1334                                 block->setInsertPoint(dom);
     1408
     1409                        Statement * const currIP = mBlock->getInsertPoint();
     1410
     1411                        switch (typeId) {
     1412                            case TypeId::And:
     1413                                expr = mBlock->createAnd(join, expr); break;
     1414                            case TypeId::Or:
     1415                                expr = mBlock->createOr(join, expr); break;
     1416                            case TypeId::Xor:
     1417                                expr = mBlock->createXor(join, expr); break;
     1418                            default:
     1419                                llvm_unreachable("Invalid TypeId!");
     1420                        }
     1421
     1422                        // If the insertion point hasn't "moved" then we didn't make a new statement
     1423                        // and thus must have unexpectidly reused a prior statement (or Var.)
     1424                        if (LLVM_UNLIKELY(currIP == mBlock->getInsertPoint())) {
     1425                            if (LLVM_LIKELY(reduceVertex(u, C, M, G, true))) {
     1426                                done = false;
    13351427                                break;
    13361428                            }
    1337                             dom = parent->getBranch(); assert(dom);
     1429                            throw std::runtime_error("Unable to reduce vertex " + std::to_string(u));
    13381430                        }
    1339                         assert (dominates(dom, ip));
    1340                     }
    1341 
    1342                     switch (typeId) {
    1343                         case TypeId::And:
    1344                             expr = block->createAnd(e1, e2); break;
    1345                         case TypeId::Or:
    1346                             expr = block->createOr(e1, e2); break;
    1347                         case TypeId::Xor:
    1348                             expr = block->createXor(e1, e2); break;
    1349                         default: break;
    1350                     }
    1351                     Q.push_front(expr);
    1352                 }
    1353             }
    1354 
    1355             assert (Q.size() == 1);
    1356 
    1357             T.clear();
    1358 
    1359             block->setInsertPoint(ip->getPrevNode());
    1360 
    1361             PabloAST * const replacement = Q.front(); assert (replacement);
     1431                    }
     1432                    join = expr;
     1433                }
     1434
     1435                T.clear();
     1436
     1437                if (done) {
     1438                    break;
     1439                }
     1440            }
     1441
     1442
     1443            PabloAST * const replacement = expr; assert (replacement);
     1444
     1445            mBlock->setInsertPoint(ip->getPrevNode());
     1446
    13621447            for (auto e : make_iterator_range(out_edges(u, G))) {
    13631448                if (G[e]) {
     
    13721457
    13731458        assert (stmt);
    1374         assert (inCurrentBlock(stmt, block));
    13751459
    13761460        if (LLVM_UNLIKELY(isa<If>(stmt) || isa<While>(stmt))) {
     
    13821466        }
    13831467
    1384         block->insert(cast<Statement>(stmt));
     1468        mBlock->insert(cast<Statement>(stmt));
    13851469        L[u] = count++; // update the line count with the actual one.
    13861470    }
     
    13891473    Z3_del_context(ctx);
    13901474
    1391     Statement * const end = block->getInsertPoint(); assert (end);
     1475    Statement * const end = mBlock->getInsertPoint(); assert (end);
    13921476    for (;;) {
    13931477        Statement * const next = end->getNextNode();
     
    13951479            break;
    13961480        }
     1481
     1482        #ifndef NDEBUG
     1483        for (PabloAST * user : next->users()) {
     1484            if (isa<Statement>(user) && dominates(user, next)) {
     1485                std::string tmp;
     1486                raw_string_ostream out(tmp);
     1487                out << "Erasing ";
     1488                PabloPrinter::print(next, out);
     1489                out << " erroneously modifies live statement ";
     1490                PabloPrinter::print(cast<Statement>(user), out);
     1491                throw std::runtime_error(out.str());
     1492            }
     1493        }
     1494        #endif
    13971495        next->eraseFromParent(true);
    13981496    }
    13991497
    14001498    #ifndef NDEBUG
    1401     PabloVerifier::verify(mFunction, "post-reassociation");
     1499    PabloVerifier::verify(mFunction, "mid-reassociation");
    14021500    #endif
    14031501
     1502    return true;
    14041503}
    14051504
     
    14821581
    14831582/** ------------------------------------------------------------------------------------------------------------- *
     1583 * @brief simplify
     1584 ** ------------------------------------------------------------------------------------------------------------- */
     1585Z3_ast BooleanReassociationPass::simplify(Z3_ast node, bool use_expensive_minimization) const {
     1586
     1587    assert (node);
     1588
     1589    node = Z3_simplify_ex(mContext, node, mParams);
     1590
     1591    if (use_expensive_minimization) {
     1592
     1593        Z3_goal g = Z3_mk_goal(mContext, true, false, false);
     1594        Z3_goal_inc_ref(mContext, g);
     1595
     1596        Z3_goal_assert(mContext, g, node);
     1597
     1598        Z3_apply_result r = Z3_tactic_apply(mContext, mTactic, g);
     1599        Z3_apply_result_inc_ref(mContext, r);
     1600
     1601        assert (Z3_apply_result_get_num_subgoals(mContext, r) == 1);
     1602
     1603        Z3_goal h = Z3_apply_result_get_subgoal(mContext, r, 0);
     1604        Z3_goal_inc_ref(mContext, h);
     1605
     1606        const unsigned n = Z3_goal_size(mContext, h);
     1607
     1608        if (n == 1) {
     1609            node = Z3_goal_formula(mContext, h, 0);
     1610        } else if (n > 1) {
     1611            Z3_ast operands[n];
     1612            for (unsigned i = 0; i < n; ++i) {
     1613                operands[i] = Z3_goal_formula(mContext, h, i);
     1614            }
     1615            node = Z3_mk_and(mContext, n, operands);
     1616        }
     1617        Z3_goal_dec_ref(mContext, h);
     1618    }
     1619    return node;
     1620}
     1621
     1622/** ------------------------------------------------------------------------------------------------------------- *
    14841623 * @brief add
    14851624 ** ------------------------------------------------------------------------------------------------------------- */
     
    15261665 * @brief constructor
    15271666 ** ------------------------------------------------------------------------------------------------------------- */
    1528 inline BooleanReassociationPass::BooleanReassociationPass(Z3_context ctx, Z3_solver solver, PabloFunction & f)
     1667inline BooleanReassociationPass::BooleanReassociationPass(Z3_context ctx, Z3_params params, Z3_tactic tactic, PabloFunction & f)
    15291668: mContext(ctx)
    1530 , mSolver(solver)
     1669, mParams(params)
     1670, mTactic(tactic)
    15311671, mFunction(f)
    15321672, mModified(false) {
Note: See TracChangeset for help on using the changeset viewer.