Ignore:
Timestamp:
Aug 8, 2016, 4:00:32 PM (3 years ago)
Author:
nmedfort
Message:

Work on multiplexing using a fixed window.

Location:
icGREP/icgrep-devel/icgrep/pablo/optimizers
Files:
2 edited

Legend:

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

    r5113 r5119  
    2222using namespace boost::numeric::ublas;
    2323
    24 /// Interesting test cases:
    25 /// ./icgrep -c -multiplexing '[\p{Lm}\p{Meetei_Mayek}]' -disable-if-hierarchy-strategy
    26 
    27 /// ./icgrep -c -multiplexing '\p{Imperial_Aramaic}(?<!\p{Sm})' -disable-if-hierarchy-strategy
    28 
    29 
    3024static cl::OptionCategory MultiplexingOptions("Multiplexing Optimization Options", "These options control the Pablo Multiplexing optimization pass.");
    3125
     
    4236#undef INITIAL_SEED_VALUE
    4337
    44 static cl::opt<unsigned> SetLimit("multiplexing-set-limit", cl::init(std::numeric_limits<unsigned>::max()),
    45                                         cl::desc("maximum size of any candidate set."),
     38static cl::opt<unsigned> WindowSize("multiplexing-window-size", cl::init(100),
     39                                        cl::desc("maximum sequence distance to consider for candidate set."),
    4640                                        cl::cat(MultiplexingOptions));
    4741
    48 static cl::opt<unsigned> SelectionLimit("multiplexing-selection-limit", cl::init(100),
    49                                         cl::desc("maximum number of selections from any partial candidate set."),
    50                                         cl::cat(MultiplexingOptions));
    51 
    52 static cl::opt<unsigned> WindowSize("multiplexing-window-size", cl::init(1),
    53                                         cl::desc("maximum depth difference for computing mutual exclusion of Advance nodes."),
    54                                         cl::cat(MultiplexingOptions));
    55 
    56 static cl::opt<unsigned> Samples("multiplexing-samples", cl::init(1),
    57                                  cl::desc("number of times the Advance constraint graph is sampled to find multiplexing opportunities."),
    58                                  cl::cat(MultiplexingOptions));
    59 
    60 
    61 enum SelectionStrategy {Greedy, WorkingSet};
    62 
    63 static cl::opt<SelectionStrategy> Strategy(cl::desc("Choose set selection strategy:"),
    64                                              cl::values(
    65                                              clEnumVal(Greedy, "choose the largest multiplexing sets possible (w.r.t. the multiplexing-set-limit)."),
    66                                              clEnumVal(WorkingSet, "choose multiplexing sets that share common input values."),
    67                                              clEnumValEnd),
    68                                            cl::init(Greedy),
    69                                            cl::cat(MultiplexingOptions));
    7042
    7143namespace pablo {
     44
     45Z3_bool maxsat(Z3_context ctx, Z3_solver solver, std::vector<Z3_ast> & soft);
    7246
    7347using TypeId = PabloAST::ClassTypeId;
     
    7953bool MultiplexingPass::optimize(PabloFunction & function) {
    8054
    81     #ifndef NDEBUG
    8255    PabloVerifier::verify(function, "pre-multiplexing");
    83     #endif
     56
     57    errs() << "PRE-MULTIPLEXING\n==============================================\n";
     58    PabloPrinter::print(function, errs());
    8459
    8560    Z3_config cfg = Z3_mk_config();
     
    9671    Z3_del_context(ctx);
    9772
    98     #ifndef NDEBUG
    9973    PabloVerifier::verify(function, "post-multiplexing");
    100     #endif
    10174
    10275    Simplifier::optimize(function);
     76
     77    errs() << "POST-MULTIPLEXING\n==============================================\n";
     78    PabloPrinter::print(function, errs());
    10379
    10480    return true;
     
    164140 ** ------------------------------------------------------------------------------------------------------------- */
    165141void MultiplexingPass::multiplex(PabloBlock * const block, Statement * const begin, Statement * const end) {
    166     if (generateCandidateSets()) {
     142    if (generateCandidateSets(begin, end)) {
    167143        selectMultiplexSetsGreedy();
    168144        eliminateSubsetConstraints();
     
    176152inline bool MultiplexingPass::equals(Z3_ast a, Z3_ast b) {
    177153    Z3_solver_push(mContext, mSolver);
    178     Z3_ast test = Z3_mk_eq(mContext, a, b);
     154    Z3_ast test = Z3_mk_eq(mContext, a, b); // try using check assumption instead?
    179155    Z3_inc_ref(mContext, test);
    180156    Z3_solver_assert(mContext, mSolver, test);
     
    257233 ** ------------------------------------------------------------------------------------------------------------- */
    258234inline Z3_ast MultiplexingPass::characterize(Advance * const adv, Z3_ast Ik) {
    259     const auto k = mAdvanceNegatedVariable.size();
     235    const auto k = mNegatedAdvance.size();
    260236
    261237    assert (adv);
     
    293269                }
    294270                unconstrained[i] = true;
    295 
    296271            } else if (equals(Ii, IiIk)) {
    297272                // If Ii = Ii ∩ Ik then Ii ⊆ Ik. Record this in the subset graph with the arc (i, k).
     
    306281                }
    307282                unconstrained[i] = true;
    308 
    309283            } else if (equals(Ik, IiIk)) {
    310284                // If Ik = Ii ∩ Ik then Ik ⊆ Ii. Record this in the subset graph with the arc (k, i).
     
    318292                unconstrained[i] = true;
    319293            }
    320 
    321294            Z3_dec_ref(mContext, IiIk);
    322295            Z3_solver_pop(mContext, mSolver, 1);
     
    350323            Z3_ast Ai = Z3_mk_and(mContext, 2, conj);
    351324            Z3_inc_ref(mContext, Ai);
    352             Z3_dec_ref(mContext, Ai0); // if this doesn't work, we'll have to scan from the output variables.
     325            Z3_dec_ref(mContext, Ai0);
    353326            Ai0 = Ai;
    354327            assert (get(mConstraintGraph[i]) == Ai);
    355328
    356             vars[m++] = mAdvanceNegatedVariable[i];
    357 
    358             continue; // note: if these Advances aren't transtively independent, an edge will still exist.
     329            vars[m++] = mNegatedAdvance[i];
     330
     331            continue; // note: if these Advances are transitively dependent, an edge will still exist.
    359332        }
    360333        add_edge(i, k, mConstraintGraph);
    361334    }
    362335    // To minimize the number of BDD computations, we store the negated variable instead of negating it each time.
    363     mAdvanceNegatedVariable.emplace_back(Nk);
     336    mNegatedAdvance.emplace_back(Nk);
    364337    Z3_ast Ak = Z3_mk_and(mContext, m, vars);
    365338    if (LLVM_UNLIKELY(Ak != Ak0)) {
     
    385358    }
    386359
    387     for (Z3_ast var : mAdvanceNegatedVariable) {
     360    for (Z3_ast var : mNegatedAdvance) {
    388361        Z3_dec_ref(mContext, var);
    389362    }
    390     mAdvanceNegatedVariable.clear();
     363    mNegatedAdvance.clear();
    391364
    392365    // Scan through and count all the advances and statements ...
     
    454427
    455428    mSubsetGraph = SubsetGraph(advances);
    456     mAdvanceNegatedVariable.reserve(advances);
     429    mNegatedAdvance.reserve(advances);
    457430
    458431    return last;
     432}
     433
     434
     435/** ------------------------------------------------------------------------------------------------------------- *
     436 * @brief generateCandidateSets
     437 ** ------------------------------------------------------------------------------------------------------------- */
     438bool MultiplexingPass::generateCandidateSets(Statement * const begin, Statement * const end) {
     439
     440    const auto n = mNegatedAdvance.size();
     441    if (LLVM_UNLIKELY(n < 3)) {
     442        return false;
     443    }
     444    assert (num_vertices(mConstraintGraph) == n);
     445
     446    // The naive way to handle this would be to compute a DNF formula consisting of the
     447    // powerset of all independent (candidate) sets of G, assign a weight to each, and
     448    // try to maximally satisfy the clauses. However, this would be extremely costly to
     449    // compute let alone solve as we could easily generate O(2^100) clauses for a complex
     450    // problem. Further the vast majority of clauses would be false in the end.
     451
     452    // Moreover, for every set that can Advance is contained in would need a unique
     453    // variable and selector. In other words:
     454
     455    // Suppose Advance A has a selector variable I. If I is true, then A must be in ONE set.
     456    // Assume A could be in m sets. To enforce this, there are m(m - 1)/2 clauses:
     457
     458    //   (¬A_1 √ ¬A_2 √ ¬I), (¬A_1 √ ¬A_3 √ ¬I), ..., (¬A_m-1 √ ¬A_m √ ¬I)
     459
     460    // m here is be equivalent to number of independent sets in the constraint graph G
     461    // that contains A.
     462
     463    // If two sets have a DEPENDENCY constraint between them, it will introduce a cyclic
     464    // relationship even if those sets are legal on their own. Thus we'd also need need
     465    // hard constraints between all constrained variables related to the pair of Advances.
     466
     467    // Instead, we only try to solve for one set at a time. This eliminate the need for
     468    // the above constraints and computing m but this process to be closer to a simple
     469    // greedy search.
     470
     471    // We do want to weight whether to include or exclude an item in a set but what should
     472    // this be? The weight must be related to the elements already in the set. If our goal
     473    // is to balance the perturbation of the AST with the reduction in # of Advances, the
     474    // cost of inclusion / exclusion could be proportional to the # of instructions that
     475    // it increases / decreases the span by --- but how many statements is an Advance worth?
     476
     477    // What if instead we maintain a queue of advances and discard any that are outside of
     478    // the current window?
     479
     480    mCandidateGraph = CandidateGraph(n);
     481
     482    Z3_config cfg = Z3_mk_config();
     483    Z3_set_param_value(cfg, "MODEL", "true");
     484    Z3_context ctx = Z3_mk_context(cfg);
     485    Z3_del_config(cfg);
     486    Z3_solver solver = Z3_mk_solver(ctx);
     487    Z3_solver_inc_ref(ctx, solver);
     488    std::vector<Z3_ast> N(n);
     489    for (unsigned i = 0; i < n; ++i) {
     490        N[i] = Z3_mk_fresh_const(ctx, nullptr, Z3_mk_bool_sort(ctx)); assert (N[i]);
     491    }
     492    std::vector<std::pair<unsigned, unsigned>> S;
     493    S.reserve(n);
     494
     495    unsigned line = 0;
     496    unsigned i = 0;
     497    for (Statement * stmt = begin; stmt != end; stmt = stmt->getNextNode()) {
     498        if (LLVM_UNLIKELY(isa<Advance>(stmt))) {
     499            assert (S.empty() || line > std::get<0>(S.back()));
     500            assert (cast<Advance>(stmt) == mConstraintGraph[i]);
     501            if (S.size() > 0 && (line - std::get<0>(S.front())) > WindowSize) {
     502                // try to compute a maximal set for this given set of Advances
     503                if (S.size() > 2) {
     504                    generateCandidateSets(ctx, solver, S, N);
     505                }
     506                // erase any that preceed our window
     507                for (auto i = S.begin();;) {
     508                    if (++i == S.end() || (line - std::get<0>(*i)) <= WindowSize) {
     509                        S.erase(S.begin(), i);
     510                        break;
     511                    }
     512                }
     513            }
     514            for (unsigned j : make_iterator_range(adjacent_vertices(i, mConstraintGraph))) {
     515                Z3_ast disj[2] = { Z3_mk_not(ctx, N[j]), Z3_mk_not(ctx, N[i]) };
     516                Z3_solver_assert(ctx, solver, Z3_mk_or(ctx, 2, disj));
     517            }
     518            S.emplace_back(line, i++);
     519        }
     520        ++line;
     521    }
     522    if (S.size() > 2) {
     523        generateCandidateSets(ctx, solver, S, N);
     524    }
     525
     526    Z3_solver_dec_ref(ctx, solver);
     527    Z3_del_context(ctx);
     528
     529    return num_vertices(mCandidateGraph) > n;
     530}
     531
     532/** ------------------------------------------------------------------------------------------------------------- *
     533 * @brief generateCandidateSets
     534 ** ------------------------------------------------------------------------------------------------------------- */
     535void MultiplexingPass::generateCandidateSets(Z3_context ctx, Z3_solver solver, const std::vector<std::pair<unsigned, unsigned>> & S, const std::vector<Z3_ast> & N) {
     536    assert (S.size() > 2);
     537    assert (std::get<0>(S.front()) < std::get<0>(S.back()));
     538    assert ((std::get<0>(S.back()) - std::get<0>(S.front())) <= WindowSize);
     539    Z3_solver_push(ctx, solver);
     540    const auto n = N.size();
     541    std::vector<Z3_ast> assumptions(S.size());
     542    for (unsigned i = 0, j = 0; i < n; ++i) {
     543        if (LLVM_UNLIKELY(j < S.size() && std::get<1>(S[j]) == i)) { // in our window range
     544            assumptions[j++] = N[i];
     545        } else {
     546            Z3_solver_assert(ctx, solver, Z3_mk_not(ctx, N[i]));
     547        }
     548    }
     549    if (maxsat(ctx, solver, assumptions) != Z3_L_FALSE) {
     550        Z3_model m = Z3_solver_get_model(ctx, solver);
     551        Z3_model_inc_ref(ctx, m);
     552        const auto k = add_vertex(mCandidateGraph); assert(k >= N.size());
     553        Z3_ast TRUE = Z3_mk_true(ctx);
     554        Z3_ast FALSE = Z3_mk_false(ctx);
     555        for (const auto i : S) {
     556            Z3_ast value;
     557            if (LLVM_UNLIKELY(Z3_model_eval(ctx, m, N[std::get<1>(i)], 1, &value) != Z3_TRUE)) {
     558                throw std::runtime_error("Unexpected Z3 error when attempting to obtain value from constraint model!");
     559            }
     560            if (value == TRUE) {
     561                add_edge(std::get<1>(i), k, mCandidateGraph);
     562            } else if (LLVM_UNLIKELY(value != FALSE)) {
     563                throw std::runtime_error("Unexpected Z3 error constraint model value is a non-terminal!");
     564            }
     565        }
     566        Z3_model_dec_ref(ctx, m);
     567    }
     568    Z3_solver_pop(ctx, solver, 1);
    459569}
    460570
     
    465575static inline bool is_power_of_2(const size_t n) {
    466576    return ((n & (n - 1)) == 0);
    467 }
    468 
    469 /** ------------------------------------------------------------------------------------------------------------- *
    470  * @brief generateCandidateSets
    471  ** ------------------------------------------------------------------------------------------------------------- */
    472 bool MultiplexingPass::generateCandidateSets() {
    473 
    474     const auto n = mAdvanceNegatedVariable.size();
    475     if (n < 3) {
    476         return false;
    477     }
    478     assert (num_vertices(mConstraintGraph) == n);
    479 
    480     Constraints S;
    481 
    482     ConstraintGraph::degree_size_type D[n];
    483 
    484     mCandidateGraph = CandidateGraph(n);
    485 
    486     for (unsigned r = Samples; r; --r) {
    487 
    488         // Push all source nodes into the (initial) independent set S
    489         for (const auto v : make_iterator_range(vertices(mConstraintGraph))) {
    490             const auto d = in_degree(v, mConstraintGraph);
    491             D[v] = d;
    492             if (d == 0) {
    493                 S.push_back(v);
    494             }
    495         }
    496 
    497         auto remaining = num_vertices(mConstraintGraph) - S.size();
    498 
    499         for (;;) {
    500             assert (S.size() > 0);
    501             addCandidateSet(S);
    502             if (LLVM_UNLIKELY(remaining == 0)) {
    503                 break;
    504             }
    505             for (;;) {
    506                 assert (S.size() > 0);
    507                 // Randomly choose a vertex in S and discard it.
    508                 const auto i = S.begin() + IntDistribution(0, S.size() - 1)(mRNG);
    509                 assert (i != S.end());
    510                 const auto u = *i;
    511                 S.erase(i);
    512                 bool checkCandidate = false;
    513                 for (auto e : make_iterator_range(out_edges(u, mConstraintGraph))) {
    514                     const auto v = target(e, mConstraintGraph);
    515                     assert ("Constraint set degree subtraction error!" && (D[v] != 0));
    516                     if ((--D[v]) == 0) {
    517                         assert ("Error v is already in S!" && std::count(S.begin(), S.end(), v) == 0);
    518                         S.push_back(v);
    519                         assert (remaining != 0);
    520                         --remaining;
    521                         if (LLVM_LIKELY(S.size() >= 3)) {
    522                             checkCandidate = true;
    523                         }
    524                     }
    525                 }
    526                 if (checkCandidate || LLVM_UNLIKELY(remaining == 0)) {
    527                     break;
    528                 }
    529             }
    530         }
    531 
    532         S.clear();
    533     }
    534 
    535     return num_vertices(mCandidateGraph) > num_vertices(mConstraintGraph);
    536 }
    537 
    538 /** ------------------------------------------------------------------------------------------------------------- *
    539  * @brief choose
    540  *
    541  * Compute n choose k
    542  ** ------------------------------------------------------------------------------------------------------------- */
    543 __attribute__ ((const)) inline unsigned long choose(const unsigned n, const unsigned k) {
    544     if (n < k)
    545         return 0;
    546     if (n == k || k == 0)
    547         return 1;
    548     unsigned long delta = k;
    549     unsigned long max = n - k;
    550     if (delta < max) {
    551         std::swap(delta, max);
    552     }
    553     unsigned long result = delta + 1;
    554     for (unsigned i = 2; i <= max; ++i) {
    555         result = (result * (delta + i)) / i;
    556     }
    557     return result;
    558 }
    559 
    560 /** ------------------------------------------------------------------------------------------------------------- *
    561  * @brief select
    562  *
    563  * James McCaffrey's algorithm for "Generating the mth Lexicographical Element of a Mathematical Combination"
    564  ** ------------------------------------------------------------------------------------------------------------- */
    565 void MultiplexingPass::selectCandidateSet(const unsigned n, const unsigned k, const unsigned m, const Constraints & S, ConstraintVertex * const element) {
    566     unsigned long a = n;
    567     unsigned long b = k;
    568     unsigned long x = (choose(n, k) - 1) - m;
    569     for (unsigned i = 0; i != k; ++i) {
    570         unsigned long y = 0;
    571         while ((y = choose(--a, b)) > x);
    572         x = x - y;
    573         b = b - 1;
    574         element[i] = S[(n - 1) - a];
    575     }
    576 }
    577 
    578 /** ------------------------------------------------------------------------------------------------------------- *
    579  * @brief updateCandidateSet
    580  ** ------------------------------------------------------------------------------------------------------------- */
    581 void MultiplexingPass::updateCandidateSet(ConstraintVertex * const begin, ConstraintVertex * const end) {
    582 
    583     using Vertex = CandidateGraph::vertex_descriptor;
    584 
    585     const auto n = num_vertices(mConstraintGraph);
    586     const auto m = num_vertices(mCandidateGraph);
    587     const auto d = end - begin;
    588 
    589     std::sort(begin, end);
    590 
    591     Vertex u = 0;
    592 
    593     for (Vertex i = n; i != m; ++i) {
    594 
    595         if (LLVM_UNLIKELY(degree(i, mCandidateGraph) == 0)) {
    596             u = i;
    597             continue;
    598         }
    599 
    600         const auto adj = adjacent_vertices(i, mCandidateGraph);
    601         if (degree(i, mCandidateGraph) < d) {
    602             // set_i can only be a subset of the new set
    603             if (LLVM_UNLIKELY(std::includes(begin, end, adj.first, adj.second))) {
    604                 clear_vertex(i, mCandidateGraph);
    605                 u = i;
    606             }
    607         } else if (LLVM_UNLIKELY(std::includes(adj.first, adj.second, begin, end))) {
    608             // the new set is a subset of set_i; discard it.
    609             return;
    610         }
    611 
    612     }
    613 
    614     if (LLVM_LIKELY(u == 0)) { // n must be at least 3 so u is 0 if and only if we're not reusing a set vertex.
    615         u = add_vertex(mCandidateGraph);
    616     }
    617 
    618     for (ConstraintVertex * i = begin; i != end; ++i) {
    619         add_edge(u, *i, mCandidateGraph);
    620     }
    621 
    622 }
    623 
    624 /** ------------------------------------------------------------------------------------------------------------- *
    625  * @brief addCandidateSet
    626  * @param S an independent set
    627  ** ------------------------------------------------------------------------------------------------------------- */
    628 inline void MultiplexingPass::addCandidateSet(const Constraints & S) {
    629     if (S.size() >= 3) {
    630         const unsigned setLimit = SetLimit;
    631         if (S.size() <= setLimit) {
    632             ConstraintVertex E[S.size()];
    633             std::copy(S.cbegin(), S.cend(), E);
    634             updateCandidateSet(E, E + S.size());
    635         } else {
    636             assert (setLimit > 0);
    637             ConstraintVertex E[setLimit];
    638             const auto max = choose(S.size(), setLimit);
    639             if (LLVM_UNLIKELY(max <= SelectionLimit)) {
    640                 for (unsigned i = 0; i != max; ++i) {
    641                     selectCandidateSet(S.size(), setLimit, i, S, E);
    642                     updateCandidateSet(E, E + setLimit);
    643                 }
    644             } else { // take m random samples
    645                 for (unsigned i = 0; i != SelectionLimit; ++i) {
    646                     selectCandidateSet(S.size(), setLimit, mRNG() % max, S, E);
    647                     updateCandidateSet(E, E + setLimit);
    648                 }
    649             }
    650         }
    651     }
    652577}
    653578
     
    689614            degree_t r = degree(t, mCandidateGraph);
    690615            if (LLVM_LIKELY(r >= 3)) { // if this set has at least 3 elements.
    691                 r *= r;
    692616                if (w < r) {
    693617                    u = t;
     
    738662    }
    739663    #endif
    740 }
    741 
    742 /** ------------------------------------------------------------------------------------------------------------- *
    743  * @brief selectMultiplexSetsWorkingSet
    744  ** ------------------------------------------------------------------------------------------------------------- */
    745 void MultiplexingPass::selectMultiplexSetsWorkingSet() {
    746 
    747     // The inputs to each Advance must be different; otherwise the SimplificationPass would consider all but
    748     // one of the Advances redundant. However, if the input is short lived, we can ignore it in favour of its
    749     // operands, which *may* be shared amongst more than one of the Advances (or may be short lived themselves,
    750     // in which we can consider their operands instead.) Ideally, if we can keep the set of live values small,
    751     // we may be able to reduce register pressure.
    752 
    753 
    754664}
    755665
     
    802712
    803713///** ------------------------------------------------------------------------------------------------------------- *
    804 // * Fu & Malik procedure for MaxSAT. This procedure is based on unsat core extraction and the at-most-one constraint.
     714// * Topologically sort the sequence of instructions whilst trying to adhere as best as possible to the original
     715// * program sequence.
    805716// ** ------------------------------------------------------------------------------------------------------------- */
    806 //inline bool fu_malik_maxsat_step(Z3_context ctx, Z3_solver s, const std::vector<Z3_ast> & soft)
    807 //{
    808 //    // create assumptions
    809 //    const auto n = soft.size();
     717//inline bool topologicalSort(Z3_context ctx, Z3_solver solver, const std::vector<Z3_ast> & nodes, const int limit) {
     718//    const auto n = nodes.size();
     719//    if (LLVM_UNLIKELY(n == 0)) {
     720//        return true;
     721//    }
     722//    if (LLVM_UNLIKELY(Z3_solver_check(ctx, solver) == Z3_L_FALSE)) {
     723//        return false;
     724//    }
     725
     726//    Z3_ast aux_vars[n];
    810727//    Z3_ast assumptions[n];
    811 //    for (size_t i = 0; i < n; ++i) {
    812 //        assumptions[i] = Z3_mk_not(ctx, soft[i]);
     728//    Z3_ast ordering[n];
     729//    int increments[n];
     730
     731//    Z3_sort boolTy = Z3_mk_bool_sort(ctx);
     732//    Z3_sort intTy = Z3_mk_int_sort(ctx);
     733//    Z3_ast one = Z3_mk_int(ctx, 1, intTy);
     734
     735//    for (unsigned i = 0; i < n; ++i) {
     736//        aux_vars[i] = Z3_mk_fresh_const(ctx, nullptr, boolTy);
     737//        assumptions[i] = Z3_mk_not(ctx, aux_vars[i]);
     738//        Z3_ast num = one;
     739//        if (i > 0) {
     740//            Z3_ast prior_plus_one[2] = { nodes[i - 1], one };
     741//            num = Z3_mk_add(ctx, 2, prior_plus_one);
     742//        }
     743//        ordering[i] = Z3_mk_eq(ctx, nodes[i], num);
     744//        increments[i] = 1;
    813745//    }
    814746
    815 //    if (Z3_solver_check_assumptions(ctx, s, n, assumptions) != Z3_L_FALSE) {
    816 //        return true; // done
     747//    unsigned unsat = 0;
     748
     749//    for (;;) {
     750//        Z3_solver_push(ctx, solver);
     751//        for (unsigned i = 0; i < n; ++i) {
     752//            Z3_ast constraint[2] = {ordering[i], aux_vars[i]};
     753//            Z3_solver_assert(ctx, solver, Z3_mk_or(ctx, 2, constraint));
     754//        }
     755//        if (LLVM_UNLIKELY(Z3_solver_check_assumptions(ctx, solver, n, assumptions) != Z3_L_FALSE)) {
     756//            errs() << " SATISFIABLE!  (" << unsat << " of " << n << ")\n";
     757//            return true; // done
     758//        }
     759//        Z3_ast_vector core = Z3_solver_get_unsat_core(ctx, solver); assert (core);
     760//        unsigned m = Z3_ast_vector_size(ctx, core); assert (m > 0);
     761
     762//        errs() << " UNSATISFIABLE " << m << "  (" << unsat << " of " << n <<")\n";
     763
     764//        for (unsigned j = 0; j < m; j++) {
     765//            // check whether assumption[i] is in the core or not
     766//            bool not_found = true;
     767//            for (unsigned i = 0; i < n; i++) {
     768//                if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) {
     769
     770//                    const auto k = increments[i];
     771
     772//                    errs() << " -- " << i << " @k=" << k << "\n";
     773
     774//                    if (k < limit) {
     775//                        Z3_ast gap = Z3_mk_int(ctx, 1UL << k, intTy);
     776//                        Z3_ast num = gap;
     777//                        if (LLVM_LIKELY(i > 0)) {
     778//                            Z3_ast prior_plus_gap[2] = { nodes[i - 1], gap };
     779//                            num = Z3_mk_add(ctx, 2, prior_plus_gap);
     780//                        }
     781//                        Z3_dec_ref(ctx, ordering[i]);
     782//                        ordering[i] = Z3_mk_le(ctx, num, nodes[i]);
     783//                    } else if (k == limit && i > 0) {
     784//                        ordering[i] = Z3_mk_le(ctx, nodes[i - 1], nodes[i]);
     785//                    } else {
     786//                        assumptions[i] = aux_vars[i]; // <- trivially satisfiable
     787//                        ++unsat;
     788//                    }
     789//                    increments[i] = k + 1;
     790//                    not_found = false;
     791//                    break;
     792//                }
     793//            }
     794//            if (LLVM_UNLIKELY(not_found)) {
     795//                throw std::runtime_error("Unexpected Z3 failure when attempting to locate unsatisfiable ordering constraint!");
     796//            }
     797//        }
     798//        Z3_solver_pop(ctx, solver, 1);
    817799//    }
    818 
    819 //    const auto core = Z3_solver_get_unsat_core(ctx, s);
    820 //    const auto m = Z3_ast_vector_size(ctx, core);
    821 //    Z3_ast block_vars[m];
    822 //    unsigned k = 0;
    823 //    // update soft-constraints and aux_vars
    824 //    for (unsigned i = 0; i < num_soft_cnstrs; i++) {
    825 //        // check whether assumption[i] is in the core or not
     800//    llvm_unreachable("maxsat wrongly reported this being unsatisfiable despite being able to satisfy the hard constraints!");
     801//    return false;
     802//}
     803
     804///** ------------------------------------------------------------------------------------------------------------- *
     805// * Topologically sort the sequence of instructions whilst trying to adhere as best as possible to the original
     806// * program sequence.
     807// ** ------------------------------------------------------------------------------------------------------------- */
     808//inline bool topologicalSort(Z3_context ctx, Z3_solver solver, const std::vector<Z3_ast> & nodes, const int limit) {
     809//    const auto n = nodes.size();
     810//    if (LLVM_UNLIKELY(n == 0)) {
     811//        return true;
     812//    }
     813//    if (LLVM_UNLIKELY(Z3_solver_check(ctx, solver) == Z3_L_FALSE)) {
     814//        return false;
     815//    }
     816
     817//    Z3_ast aux_vars[n];
     818//    Z3_ast assumptions[n];
     819
     820//    Z3_sort boolTy = Z3_mk_bool_sort(ctx);
     821//    Z3_ast one = Z3_mk_int(ctx, 1, Z3_mk_int_sort(ctx));
     822
     823//    for (unsigned i = 0; i < n; ++i) {
     824//        aux_vars[i] = Z3_mk_fresh_const(ctx, nullptr, boolTy);
     825//        assumptions[i] = Z3_mk_not(ctx, aux_vars[i]);
     826//        Z3_ast num = one;
     827//        if (i > 0) {
     828//            Z3_ast prior_plus_one[2] = { nodes[i - 1], one };
     829//            num = Z3_mk_add(ctx, 2, prior_plus_one);
     830//        }
     831//        Z3_ast ordering = Z3_mk_eq(ctx, nodes[i], num);
     832//        Z3_ast constraint[2] = {ordering, aux_vars[i]};
     833//        Z3_solver_assert(ctx, solver, Z3_mk_or(ctx, 2, constraint));
     834//    }
     835
     836//    for (unsigned k = 0; k < n; ) {
     837//        if (LLVM_UNLIKELY(Z3_solver_check_assumptions(ctx, solver, n, assumptions) != Z3_L_FALSE)) {
     838//            errs() << " SATISFIABLE!\n";
     839//            return true; // done
     840//        }
     841//        Z3_ast_vector core = Z3_solver_get_unsat_core(ctx, solver); assert (core);
     842//        unsigned m = Z3_ast_vector_size(ctx, core); assert (m > 0);
     843
     844//        k += m;
     845
     846//        errs() << " UNSATISFIABLE " << m << " (" << k << ")\n";
     847
    826848//        for (unsigned j = 0; j < m; j++) {
    827 //            if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) {
    828 //                // assumption[i] is in the unsat core... so soft_cnstrs[i] is in the unsat core
    829 //                Z3_ast block_var   = Z3_mk_fresh_const(ctx, nullptr, Z3_mk_bool_sort(ctx));
    830 //                Z3_ast new_aux_var = Z3_mk_fresh_const(ctx, nullptr, Z3_mk_bool_sort(ctx));
    831 //                soft_cnstrs[i]     = mk_binary_or(ctx, soft_cnstrs[i], block_var);
    832 //                aux_vars[i]        = new_aux_var;
    833 //                block_vars[k]      = block_var;
    834 //                k++;
    835 //                // Add new constraint containing the block variable.
    836 //                // Note that we are using the new auxiliary variable to be able to use it as an assumption.
    837 //                Z3_solver_assert(ctx, s, mk_binary_or(ctx, soft_cnstrs[i], new_aux_var));
    838 //                break;
     849//            // check whether assumption[i] is in the core or not
     850//            bool not_found = true;
     851//            for (unsigned i = 0; i < n; i++) {
     852//                if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) {
     853//                    assumptions[i] = aux_vars[i];
     854//                    not_found = false;
     855//                    break;
     856//                }
     857//            }
     858//            if (LLVM_UNLIKELY(not_found)) {
     859//                throw std::runtime_error("Unexpected Z3 failure when attempting to locate unsatisfiable ordering constraint!");
    839860//            }
    840861//        }
    841862//    }
    842 
    843 
    844 //    assert_at_most_one(ctx, s, k, block_vars);
    845 //    return 0; // not done.
    846 
    847 //}
    848 
    849 ///** ------------------------------------------------------------------------------------------------------------- *
    850 // * Fu & Malik procedure for MaxSAT. This procedure is based on unsat core extraction and the at-most-one constraint.
    851 // ** ------------------------------------------------------------------------------------------------------------- */
    852 //inline bool fu_malik_maxsat(Z3_context ctx, Z3_solver s, const std::vector<Z3_ast> & soft) {
    853 //    assert(Z3_solver_check(ctx, s) != Z3_L_FALSE);
    854 //    for (size_t k = 0; k < soft.size(); ++k) {
    855 //        if (fu_malik_maxsat_step(ctx, s, soft)) {
    856 //            return true;
    857 //        }
    858 //    }
     863//    llvm_unreachable("maxsat wrongly reported this being unsatisfiable despite being able to satisfy the hard constraints!");
    859864//    return false;
    860865//}
     
    864869 * @brief addWithHardConstraints
    865870 ** ------------------------------------------------------------------------------------------------------------- */
    866 Z3_ast addWithHardConstraints(Z3_context ctx, Z3_solver solver, PabloBlock * const block, Statement * stmt, flat_map<Statement *, Z3_ast> & M) {
     871Z3_ast addWithHardConstraints(Z3_context ctx, Z3_solver solver, PabloBlock * const block, Statement * const stmt, flat_map<Statement *, Z3_ast> & M) {
    867872    assert (M.count(stmt) == 0 && stmt->getParent() == block);
    868873    // compute the hard dependency constraints
    869     Z3_symbol symbol = Z3_mk_string_symbol(ctx, stmt->getName()->value().data()); assert (symbol);
    870     Z3_ast node = Z3_mk_const(ctx, symbol, Z3_mk_int_sort(ctx)); assert (node);
     874    Z3_ast node = Z3_mk_fresh_const(ctx, nullptr, Z3_mk_int_sort(ctx)); assert (node);
     875    // we want all numbers to be positive so that the soft assertion that the first statement ought to stay at the first location
     876    // whenever possible isn't satisfied by making preceeding numbers negative.
     877    Z3_solver_assert(ctx, solver, Z3_mk_gt(ctx, node, Z3_mk_int(ctx, 0, Z3_mk_int_sort(ctx))));
    871878    for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
    872879        PabloAST * const op = stmt->getOperand(i);
     
    874881            const auto f = M.find(cast<Statement>(op));
    875882            if (f != M.end()) {
    876                 Z3_ast depedency = Z3_mk_lt(ctx, f->second, node);
    877                 Z3_solver_assert(ctx, solver, depedency);
     883                Z3_solver_assert(ctx, solver, Z3_mk_lt(ctx, f->second, node));
    878884            }
    879885        }
     
    881887    M.emplace(stmt, node);
    882888    return node;
    883 
    884889}
    885890
     
    937942    assert (!end || isa<If>(end) || isa<While>(end));
    938943
    939     Statement * const ip = begin->getPrevNode(); // save our insertion point prior to modifying the AST
    940 
    941944    Z3_config cfg = Z3_mk_config();
    942     // Z3_set_param_value(cfg, "MODEL", "true");
     945    Z3_set_param_value(cfg, "MODEL", "true");
    943946    Z3_context ctx = Z3_mk_context(cfg);
    944947    Z3_del_config(cfg);
    945948    Z3_solver solver = Z3_mk_solver(ctx);
     949    Z3_solver_inc_ref(ctx, solver);
    946950
    947951    const auto first_set = num_vertices(mConstraintGraph);
    948952    const auto last_set = num_vertices(mCandidateGraph);
    949 
    950     // Compute the hard and soft constraints for any part of the AST that we are not intending to modify.
    951     flat_map<Statement *, Z3_ast> M;
    952 
    953 //    Z3_ast prior = nullptr;
    954 
    955 //    Z3_ast one = Z3_mk_int(ctx, 1, Z3_mk_int_sort(ctx));
    956 
    957 //    std::vector<Z3_ast> soft; // call check_with_assumptions!!!
    958 
    959     for (Statement * stmt = begin; stmt != end; stmt = stmt->getNextNode()) {
    960         Z3_ast node = addWithHardConstraints(ctx, solver, block, stmt, M);
    961 //        // add in the soft ordering constraints
    962 //        if (prior) {
    963 //            Z3_ast constraint[2];
    964 //            if (gap) {
    965 //                constraint[0] = Z3_mk_lt(ctx, prior, node);
    966 //                gap = false;
    967 //            } else {
    968 //                Z3_ast prior_plus_one[2] = { prior, one };
    969 //                Z3_ast num = Z3_mk_add(ctx, 2, prior_plus_one);
    970 //                constraint[0] = Z3_mk_eq(ctx, node, num);
    971 //            }
    972 //            Z3_ast ordering = Z3_mk_fresh_const(ctx, nullptr, Z3_mk_bool_sort(ctx));
    973 //            constraint[1] = ordering;
    974 //            Z3_solver_assert(ctx, solver, Z3_mk_or(ctx, 2, constraint));
    975 //            soft.push_back(ordering);
    976 //        }
    977 //        prior = node;
    978     }
    979 
    980 
    981     block->setInsertPoint(block->back());
    982953
    983954    for (auto idx = first_set; idx != last_set; ++idx) {
     
    988959            PabloAST * muxed[m];
    989960            PabloAST * muxed_n[m];
     961
    990962            // The multiplex set graph is a DAG with edges denoting the set relationships of our independent sets.
    991963            unsigned i = 0;
    992964            for (const auto u : make_iterator_range(adjacent_vertices(idx, mCandidateGraph))) {
    993965                input[i] = mConstraintGraph[u];
    994                 assert ("Algorithm failure! not all inputs are in the same block!" && (input[i]->getParent() == block));
    995                 assert ("Algorithm failure! not all inputs advance by the same amount!" && (input[i]->getOperand(1) == input[0]->getOperand(1)));
     966                assert ("Not all inputs are in the same block!" && (input[i]->getParent() == block));
     967                assert ("Not all inputs advance by the same amount!" && (input[i]->getOperand(1) == input[0]->getOperand(1)));
     968                assert ("Inputs are not in sequential order!" && (i == 0 || (i > 0 && dominates(input[i - 1], input[i]))));
    996969                ++i;
    997970            }
    998971
     972            Statement * const A1 = input[0];
     973            Statement * const An = input[n - 1]->getNextNode();
     974
     975            Statement * const ip = A1->getPrevNode(); // save our insertion point prior to modifying the AST
     976
     977            Z3_solver_push(ctx, solver);
     978
     979            // Compute the hard and soft constraints for any part of the AST that we are not intending to modify.
     980            flat_map<Statement *, Z3_ast> M;
     981
     982            Z3_ast prior = nullptr;
     983            Z3_ast one = Z3_mk_int(ctx, 1, Z3_mk_int_sort(ctx));
     984            std::vector<Z3_ast> ordering;
     985//            std::vector<Z3_ast> nodes;
     986
     987            for (Statement * stmt = A1; stmt != An; stmt = stmt->getNextNode()) { assert (stmt != ip);
     988                Z3_ast node = addWithHardConstraints(ctx, solver, block, stmt, M);
     989                // compute the soft ordering constraints
     990                Z3_ast num = one;
     991                if (prior) {
     992                    Z3_ast prior_plus_one[2] = { prior, one };
     993                    num = Z3_mk_add(ctx, 2, prior_plus_one);
     994                }
     995                ordering.push_back(Z3_mk_eq(ctx, node, num));
     996                if (prior) {
     997                    ordering.push_back(Z3_mk_lt(ctx, prior, node));
     998                }
     999
     1000
     1001//                for (Z3_ast prior : nodes) {
     1002//                    Z3_solver_assert(ctx, solver, Z3_mk_not(ctx, Z3_mk_eq(ctx, prior, node)));
     1003//                }
     1004 //               nodes.push_back(node);
     1005
     1006
     1007                prior = node;
     1008            }
     1009
     1010            // assert (nodes.size() <= WindowSize);
     1011
     1012            block->setInsertPoint(block->back()); // <- necessary for domination check!
     1013
    9991014            circular_buffer<PabloAST *> Q(n);
    10001015
    10011016            /// Perform n-to-m Multiplexing
    1002             for (size_t j = 0; j != m; ++j) {               
     1017            for (size_t j = 0; j != m; ++j) {
    10031018                std::ostringstream prefix;
    10041019                prefix << "mux" << n << "to" << m << '.' << (j);
     
    10491064                assert (M.count(input[i]) == 0);
    10501065            }
    1051         }
    1052     }
    1053 
    1054     assert (M.count(ip) == 0);
    1055 
    1056     if (LLVM_UNLIKELY(Z3_solver_check(ctx, solver) == Z3_L_FALSE)) {
    1057         throw std::runtime_error("Unexpected Z3 failure when attempting to topologically sort the AST!");
    1058     }
    1059 
    1060     Z3_model m = Z3_solver_get_model(ctx, solver);
    1061     Z3_model_inc_ref(ctx, m);
    1062 
    1063     std::vector<std::pair<long long int, Statement *>> Q;
    1064 
    1065     for (const auto i : M) {
    1066         Z3_ast value;
    1067         if (Z3_model_eval(ctx, m, std::get<1>(i), Z3_L_TRUE, &value) != Z3_L_TRUE) {
    1068             throw std::runtime_error("Unexpected Z3 error when attempting to obtain value from model!");
    1069         }
    1070         long long int line;
    1071         if (Z3_get_numeral_int64(ctx, value, &line) != Z3_L_TRUE) {
    1072             throw std::runtime_error("Unexpected Z3 error when attempting to convert model value to integer!");
    1073         }
    1074         Q.emplace_back(line, std::get<0>(i));
    1075     }
    1076 
    1077     Z3_model_dec_ref(ctx, m);
     1066
     1067            assert (M.count(ip) == 0);
     1068
     1069            if (LLVM_UNLIKELY(maxsat(ctx, solver, ordering) != Z3_L_TRUE)) {
     1070                throw std::runtime_error("Unexpected Z3 failure when attempting to topologically sort the AST!");
     1071            }
     1072
     1073            Z3_model model = Z3_solver_get_model(ctx, solver);
     1074            Z3_model_inc_ref(ctx, model);
     1075
     1076            std::vector<std::pair<long long int, Statement *>> I;
     1077
     1078            for (const auto i : M) {
     1079                Z3_ast value;
     1080                if (LLVM_UNLIKELY(Z3_model_eval(ctx, model, std::get<1>(i), Z3_L_TRUE, &value) != Z3_L_TRUE)) {
     1081                    throw std::runtime_error("Unexpected Z3 error when attempting to obtain value from model!");
     1082                }
     1083                long long int line;
     1084                if (LLVM_UNLIKELY(Z3_get_numeral_int64(ctx, value, &line) != Z3_L_TRUE)) {
     1085                    throw std::runtime_error("Unexpected Z3 error when attempting to convert model value to integer!");
     1086                }
     1087                I.emplace_back(line, std::get<0>(i));
     1088            }
     1089
     1090            Z3_model_dec_ref(ctx, model);
     1091
     1092            std::sort(I.begin(), I.end());
     1093
     1094            block->setInsertPoint(ip);
     1095            for (auto i : I) {
     1096                block->insert(std::get<1>(i));
     1097            }
     1098
     1099            Z3_solver_pop(ctx, solver, 1);
     1100        }
     1101    }
     1102
     1103    Z3_solver_dec_ref(ctx, solver);
    10781104    Z3_del_context(ctx);
    10791105
    1080     std::sort(Q.begin(), Q.end());
    1081 
    1082     block->setInsertPoint(ip);
    1083     for (auto i : Q) {
    1084         block->insert(std::get<1>(i));
    1085     }
    1086 
    1087 
    1088 }
     1106}
     1107
     1108///** ------------------------------------------------------------------------------------------------------------- *
     1109// * @brief multiplexSelectedSets
     1110// ** ------------------------------------------------------------------------------------------------------------- */
     1111//inline void MultiplexingPass::multiplexSelectedSets(PabloBlock * const block, Statement * const begin, Statement * const end) {
     1112
     1113//    assert ("begin cannot be null!" && begin);
     1114//    assert (begin->getParent() == block);
     1115//    assert (!end || end->getParent() == block);
     1116//    assert (!end || isa<If>(end) || isa<While>(end));
     1117
     1118//    Statement * const ip = begin->getPrevNode(); // save our insertion point prior to modifying the AST
     1119
     1120//    Z3_config cfg = Z3_mk_config();
     1121//    Z3_set_param_value(cfg, "MODEL", "true");
     1122//    Z3_context ctx = Z3_mk_context(cfg);
     1123//    Z3_del_config(cfg);
     1124//    Z3_solver solver = Z3_mk_solver(ctx);
     1125//    Z3_solver_inc_ref(ctx, solver);
     1126
     1127//    const auto first_set = num_vertices(mConstraintGraph);
     1128//    const auto last_set = num_vertices(mCandidateGraph);
     1129
     1130//    // Compute the hard and soft constraints for any part of the AST that we are not intending to modify.
     1131//    flat_map<Statement *, Z3_ast> M;
     1132
     1133//    Z3_ast prior = nullptr;
     1134//    Z3_ast one = Z3_mk_int(ctx, 1, Z3_mk_int_sort(ctx));
     1135//    std::vector<Z3_ast> ordering;
     1136
     1137//    for (Statement * stmt = begin; stmt != end; stmt = stmt->getNextNode()) { assert (stmt != ip);
     1138//        Z3_ast node = addWithHardConstraints(ctx, solver, block, stmt, M);
     1139//        // compute the soft ordering constraints
     1140//        Z3_ast num = one;
     1141//        if (prior) {
     1142//            Z3_ast prior_plus_one[2] = { prior, one };
     1143//            num = Z3_mk_add(ctx, 2, prior_plus_one);
     1144//        }
     1145//        ordering.push_back(Z3_mk_eq(ctx, node, num));
     1146//        prior = node;
     1147//    }
     1148
     1149//    block->setInsertPoint(block->back()); // <- necessary for domination check!
     1150
     1151//    errs() << "---------------------------------------------\n";
     1152
     1153//    for (auto idx = first_set; idx != last_set; ++idx) {
     1154//        const size_t n = degree(idx, mCandidateGraph);
     1155//        if (n) {
     1156//            const size_t m = log2_plus_one(n); assert (n > 2 && m < n);
     1157//            Advance * input[n];
     1158//            PabloAST * muxed[m];
     1159//            PabloAST * muxed_n[m];
     1160
     1161//            errs() << n << " -> " << m << "\n";
     1162
     1163//            // The multiplex set graph is a DAG with edges denoting the set relationships of our independent sets.
     1164//            unsigned i = 0;
     1165//            for (const auto u : make_iterator_range(adjacent_vertices(idx, mCandidateGraph))) {
     1166//                input[i] = mConstraintGraph[u];
     1167//                assert ("Not all inputs are in the same block!" && (input[i]->getParent() == block));
     1168//                assert ("Not all inputs advance by the same amount!" && (input[i]->getOperand(1) == input[0]->getOperand(1)));
     1169//                ++i;
     1170//            }
     1171
     1172//            circular_buffer<PabloAST *> Q(n);
     1173
     1174//            /// Perform n-to-m Multiplexing
     1175//            for (size_t j = 0; j != m; ++j) {
     1176//                std::ostringstream prefix;
     1177//                prefix << "mux" << n << "to" << m << '.' << (j);
     1178//                assert (Q.empty());
     1179//                for (size_t i = 0; i != n; ++i) {
     1180//                    if (((i + 1) & (1UL << j)) != 0) {
     1181//                        Q.push_back(input[i]->getOperand(0));
     1182//                    }
     1183//                }
     1184//                while (Q.size() > 1) {
     1185//                    PabloAST * a = Q.front(); Q.pop_front();
     1186//                    PabloAST * b = Q.front(); Q.pop_front();
     1187//                    PabloAST * expr = block->createOr(a, b);
     1188//                    addWithHardConstraints(ctx, solver, block, expr, M, ip);
     1189//                    Q.push_back(expr);
     1190//                }
     1191//                PabloAST * const muxing = Q.front(); Q.clear();
     1192//                muxed[j] = block->createAdvance(muxing, input[0]->getOperand(1), prefix.str());
     1193//                addWithHardConstraints(ctx, solver, block, muxed[j], M, ip);
     1194//                muxed_n[j] = block->createNot(muxed[j]);
     1195//                addWithHardConstraints(ctx, solver, block, muxed_n[j], M, ip);
     1196//            }
     1197
     1198//            /// Perform m-to-n Demultiplexing
     1199//            for (size_t i = 0; i != n; ++i) {
     1200//                // Construct the demuxed values and replaces all the users of the original advances with them.
     1201//                assert (Q.empty());
     1202//                for (size_t j = 0; j != m; ++j) {
     1203//                    Q.push_back((((i + 1) & (1UL << j)) != 0) ? muxed[j] : muxed_n[j]);
     1204//                }
     1205//                Z3_ast replacement = nullptr;
     1206//                while (Q.size() > 1) {
     1207//                    PabloAST * const a = Q.front(); Q.pop_front();
     1208//                    PabloAST * const b = Q.front(); Q.pop_front();
     1209//                    PabloAST * expr = block->createAnd(a, b);
     1210//                    replacement = addWithHardConstraints(ctx, solver, block, expr, M, ip);
     1211//                    Q.push_back(expr);
     1212//                }
     1213//                assert (replacement);
     1214//                PabloAST * const demuxed = Q.front(); Q.clear();
     1215
     1216//                const auto f = M.find(input[i]);
     1217//                assert (f != M.end());
     1218//                Z3_solver_assert(ctx, solver, Z3_mk_eq(ctx, f->second, replacement));
     1219//                M.erase(f);
     1220
     1221//                input[i]->replaceWith(demuxed);
     1222//                assert (M.count(input[i]) == 0);
     1223//            }
     1224//        }
     1225//    }
     1226
     1227//    assert (M.count(ip) == 0);
     1228
     1229//    // if (LLVM_UNLIKELY(maxsat(ctx, solver, ordering) == Z3_L_FALSE)) {
     1230//    if (LLVM_UNLIKELY(Z3_solver_check(ctx, solver) != Z3_L_TRUE)) {
     1231//        throw std::runtime_error("Unexpected Z3 failure when attempting to topologically sort the AST!");
     1232//    }
     1233
     1234//    Z3_model m = Z3_solver_get_model(ctx, solver);
     1235//    Z3_model_inc_ref(ctx, m);
     1236
     1237//    std::vector<std::pair<long long int, Statement *>> Q;
     1238
     1239//    errs() << "-----------------------------------------------------------\n";
     1240
     1241//    for (const auto i : M) {
     1242//        Z3_ast value;
     1243//        if (Z3_model_eval(ctx, m, std::get<1>(i), Z3_L_TRUE, &value) != Z3_L_TRUE) {
     1244//            throw std::runtime_error("Unexpected Z3 error when attempting to obtain value from model!");
     1245//        }
     1246//        long long int line;
     1247//        if (Z3_get_numeral_int64(ctx, value, &line) != Z3_L_TRUE) {
     1248//            throw std::runtime_error("Unexpected Z3 error when attempting to convert model value to integer!");
     1249//        }
     1250//        Q.emplace_back(line, std::get<0>(i));
     1251//    }
     1252
     1253//    Z3_model_dec_ref(ctx, m);
     1254//    Z3_solver_dec_ref(ctx, solver);
     1255//    Z3_del_context(ctx);
     1256
     1257//    std::sort(Q.begin(), Q.end());
     1258
     1259//    block->setInsertPoint(ip);
     1260//    for (auto i : Q) {
     1261//        block->insert(std::get<1>(i));
     1262//    }
     1263//}
    10891264
    10901265/** ------------------------------------------------------------------------------------------------------------- *
     
    11401315inline Z3_ast MultiplexingPass::make(const PabloAST * const expr) {
    11411316    assert (expr);
    1142     Z3_sort ty = Z3_mk_bool_sort(mContext);
    1143     const String * name = nullptr;
    1144     if (LLVM_LIKELY(isa<Statement>(expr))) {
    1145         name = cast<Statement>(expr)->getName();
    1146     } else if (LLVM_UNLIKELY(isa<Var>(expr))) {
    1147         name = cast<Var>(expr)->getName();
    1148     }
    1149     assert (name);
    1150     Z3_symbol s = Z3_mk_string_symbol(mContext, name->value().data());
    1151     Z3_ast node = Z3_mk_const(mContext, s, ty);
     1317    Z3_ast node = Z3_mk_fresh_const(mContext, nullptr, Z3_mk_bool_sort(mContext));
    11521318    Z3_inc_ref(mContext, node);
    11531319    return add(expr, node);
     
    11761342
    11771343
     1344inline Z3_ast mk_binary_or(Z3_context ctx, Z3_ast in_1, Z3_ast in_2) {
     1345    Z3_ast args[2] = { in_1, in_2 };
     1346    return Z3_mk_or(ctx, 2, args);
     1347}
     1348
     1349inline Z3_ast mk_ternary_or(Z3_context ctx, Z3_ast in_1, Z3_ast in_2, Z3_ast in_3) {
     1350    Z3_ast args[3] = { in_1, in_2, in_3 };
     1351    return Z3_mk_or(ctx, 3, args);
     1352}
     1353
     1354inline Z3_ast mk_binary_and(Z3_context ctx, Z3_ast in_1, Z3_ast in_2) {
     1355    Z3_ast args[2] = { in_1, in_2 };
     1356    return Z3_mk_and(ctx, 2, args);
     1357}
     1358
     1359///**
     1360//   \brief Create a full adder with inputs \c in_1, \c in_2 and \c cin.
     1361//   The output of the full adder is stored in \c out, and the carry in \c c_out.
     1362//*/
     1363//inline std::pair<Z3_ast, Z3_ast> mk_full_adder(Z3_context ctx, Z3_ast in_1, Z3_ast in_2, Z3_ast cin) {
     1364//    Z3_ast out = Z3_mk_xor(ctx, Z3_mk_xor(ctx, in_1, in_2), cin);
     1365//    Z3_ast cout = mk_ternary_or(ctx, mk_binary_and(ctx, in_1, in_2), mk_binary_and(ctx, in_1, cin), mk_binary_and(ctx, in_2, cin));
     1366//    return std::make_pair(out, cout);
     1367//}
     1368
     1369/**
     1370   \brief Create an adder for inputs of size \c num_bits.
     1371   The arguments \c in1 and \c in2 are arrays of bits of size \c num_bits.
     1372
     1373   \remark \c result must be an array of size \c num_bits + 1.
     1374*/
     1375void mk_adder(Z3_context ctx, const unsigned num_bits, Z3_ast * in_1, Z3_ast * in_2, Z3_ast * result) {
     1376    Z3_ast cin = Z3_mk_false(ctx);
     1377    for (unsigned i = 0; i < num_bits; i++) {
     1378        result[i] = Z3_mk_xor(ctx, Z3_mk_xor(ctx, in_1[i], in_2[i]), cin);
     1379        cin = mk_ternary_or(ctx, mk_binary_and(ctx, in_1[i], in_2[i]), mk_binary_and(ctx, in_1[i], cin), mk_binary_and(ctx, in_2[i], cin));
     1380    }
     1381    result[num_bits] = cin;
     1382}
     1383
     1384/**
     1385   \brief Given \c num_ins "numbers" of size \c num_bits stored in \c in.
     1386   Create floor(num_ins/2) adder circuits. Each circuit is adding two consecutive "numbers".
     1387   The numbers are stored one after the next in the array \c in.
     1388   That is, the array \c in has size num_bits * num_ins.
     1389   Return an array of bits containing \c ceil(num_ins/2) numbers of size \c (num_bits + 1).
     1390   If num_ins/2 is not an integer, then the last "number" in the output, is the last "number" in \c in with an appended "zero".
     1391*/
     1392unsigned mk_adder_pairs(Z3_context ctx, const unsigned num_bits, const unsigned num_ins, Z3_ast * in, Z3_ast * out) {
     1393    unsigned out_num_bits = num_bits + 1;
     1394    Z3_ast * _in          = in;
     1395    Z3_ast * _out         = out;
     1396    unsigned out_num_ins  = (num_ins % 2 == 0) ? (num_ins / 2) : (num_ins / 2) + 1;
     1397    for (unsigned i = 0; i < num_ins / 2; i++) {
     1398        mk_adder(ctx, num_bits, _in, _in + num_bits, _out);
     1399        _in  += num_bits;
     1400        _in  += num_bits;
     1401        _out += out_num_bits;
     1402    }
     1403    if (num_ins % 2 != 0) {
     1404        for (unsigned i = 0; i < num_bits; i++) {
     1405            _out[i] = _in[i];
     1406        }
     1407        _out[num_bits] = Z3_mk_false(ctx);
     1408    }
     1409    return out_num_ins;
     1410}
     1411
     1412/**
     1413   \brief Return the \c idx bit of \c val.
     1414*/
     1415inline bool get_bit(unsigned val, unsigned idx) {
     1416    return (val & (1U << (idx & 31))) != 0;
     1417}
     1418
     1419/**
     1420   \brief Given an integer val encoded in n bits (boolean variables), assert the constraint that val <= k.
     1421*/
     1422void assert_le_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * val)
     1423{
     1424    Z3_ast i1, i2;
     1425    Z3_ast not_val = Z3_mk_not(ctx, val[0]);
     1426    assert (get_bit(1, 0));
     1427    Z3_ast out = Z3_mk_true(ctx);
     1428    for (unsigned i = 1; i < n; i++) {
     1429        not_val = Z3_mk_not(ctx, val[i]);
     1430        if (get_bit(1, i)) {
     1431            i1 = not_val;
     1432            i2 = out;
     1433        }
     1434        else {
     1435            i1 = Z3_mk_false(ctx);
     1436            i2 = Z3_mk_false(ctx);
     1437        }
     1438        out = mk_ternary_or(ctx, i1, i2, mk_binary_and(ctx, not_val, out));
     1439    }
     1440    Z3_solver_assert(ctx, s, out);
     1441}
     1442
     1443/**
     1444   \brief Create a counter circuit to count the number of "ones" in lits.
     1445   The function returns an array of bits (i.e. boolean expressions) containing the output of the circuit.
     1446   The size of the array is stored in out_sz.
     1447*/
     1448void mk_counter_circuit(Z3_context ctx, Z3_solver solver, unsigned n, Z3_ast * lits) {
     1449    unsigned k = 1;
     1450    assert (n != 0);
     1451    Z3_ast aux_array_1[n + 1];
     1452    Z3_ast aux_array_2[n + 1];
     1453    Z3_ast * aux_1 = aux_array_1;
     1454    Z3_ast * aux_2 = aux_array_2;
     1455    std::memcpy(aux_1, lits, sizeof(Z3_ast) * n);
     1456    while (n > 1) {
     1457        assert (aux_1 != aux_2);
     1458        n = mk_adder_pairs(ctx, k++, n, aux_1, aux_2);
     1459        std::swap(aux_1, aux_2);
     1460    }
     1461    assert_le_one(ctx, solver, k, aux_1);
     1462}
     1463
     1464/** ------------------------------------------------------------------------------------------------------------- *
     1465 * Fu & Malik procedure for MaxSAT. This procedure is based on unsat core extraction and the at-most-one constraint.
     1466 ** ------------------------------------------------------------------------------------------------------------- */
     1467Z3_bool maxsat(Z3_context ctx, Z3_solver solver, std::vector<Z3_ast> & soft) {
     1468    if (LLVM_UNLIKELY(Z3_solver_check(ctx, solver) == Z3_L_FALSE)) {
     1469        return Z3_L_FALSE;
     1470    }
     1471    if (LLVM_UNLIKELY(soft.empty())) {
     1472        return true;
     1473    }
     1474
     1475    const auto n = soft.size();
     1476    const auto ty = Z3_mk_bool_sort(ctx);
     1477    Z3_ast aux_vars[n];
     1478    Z3_ast assumptions[n];
     1479
     1480    for (unsigned i = 0; i < n; ++i) {
     1481        aux_vars[i] = Z3_mk_fresh_const(ctx, nullptr, ty);
     1482        Z3_solver_assert(ctx, solver, mk_binary_or(ctx, soft[i], aux_vars[i]));
     1483    }
     1484
     1485    for (;;) {
     1486        // create assumptions
     1487        for (unsigned i = 0; i < n; i++) {
     1488            // Recall that we asserted (soft_cnstrs[i] \/ aux_vars[i])
     1489            // So using (NOT aux_vars[i]) as an assumption we are actually forcing the soft_cnstrs[i] to be considered.
     1490            assumptions[i] = Z3_mk_not(ctx, aux_vars[i]);
     1491        }
     1492        if (Z3_solver_check_assumptions(ctx, solver, n, assumptions) != Z3_L_FALSE) {
     1493            return Z3_L_TRUE; // done
     1494        } else {
     1495            Z3_ast_vector core = Z3_solver_get_unsat_core(ctx, solver);
     1496            unsigned m = Z3_ast_vector_size(ctx, core);
     1497            Z3_ast block_vars[m];
     1498            unsigned k = 0;
     1499            // update soft-constraints and aux_vars
     1500            for (unsigned i = 0; i < n; i++) {
     1501                // check whether assumption[i] is in the core or not
     1502                for (unsigned j = 0; j < m; j++) {
     1503                    if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) {
     1504                        // assumption[i] is in the unsat core... so soft_cnstrs[i] is in the unsat core
     1505                        Z3_ast block_var = Z3_mk_fresh_const(ctx, nullptr, ty);
     1506                        Z3_ast new_aux_var = Z3_mk_fresh_const(ctx, nullptr, ty);
     1507                        soft[i] = mk_binary_or(ctx, soft[i], block_var);
     1508                        aux_vars[i] = new_aux_var;
     1509                        block_vars[k] = block_var;
     1510                        ++k;
     1511                        // Add new constraint containing the block variable.
     1512                        // Note that we are using the new auxiliary variable to be able to use it as an assumption.
     1513                        Z3_solver_assert(ctx, solver, mk_binary_or(ctx, soft[i], new_aux_var) );
     1514                        break;
     1515                    }
     1516                }
     1517
     1518            }
     1519            if (k > 1) {
     1520                mk_counter_circuit(ctx, solver, k, block_vars);
     1521            }
     1522        }
     1523    }
     1524    llvm_unreachable("unreachable");
     1525    return Z3_L_FALSE;
     1526}
     1527
    11781528} // end of namespace pablo
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_automultiplexing.hpp

    r5113 r5119  
    2828    using CharacterizationMap = llvm::DenseMap<const PabloAST *, CharacterizationRef>;
    2929
    30     using ConstraintGraph = boost::adjacency_matrix<boost::directedS, Advance *>;
     30    using ConstraintGraph = boost::adjacency_matrix<boost::undirectedS, Advance *>;
    3131    using ConstraintVertex = ConstraintGraph::vertex_descriptor;
    3232    using Constraints = std::vector<ConstraintVertex>;
     
    3636    using IntDistribution = std::uniform_int_distribution<RNG::result_type>;
    3737
    38     using CandidateGraph = boost::adjacency_list<boost::hash_setS, boost::vecS, boost::undirectedS>;
     38    using CandidateGraph = boost::adjacency_list<boost::setS, boost::vecS, boost::undirectedS>;
    3939    using Candidates = std::vector<CandidateGraph::vertex_descriptor>;
    4040
     
    6666    void multiplex(PabloBlock * const block, Statement * const begin, Statement * const end);
    6767
    68     bool generateCandidateSets();
    69     void addCandidateSet(const Constraints & S);
    70     void updateCandidateSet(ConstraintVertex * const begin, ConstraintVertex * const end);
    71     void selectCandidateSet(const unsigned n, const unsigned k, const unsigned m, const Constraints & S, ConstraintVertex * const element);
     68    bool generateCandidateSets(Statement * const begin, Statement * const end);
     69    void generateCandidateSets(Z3_context ctx, Z3_solver solver, const std::vector<std::pair<unsigned, unsigned>> & S, const std::vector<Z3_ast> & N);
    7270
    7371    void selectMultiplexSetsGreedy();
    74     void selectMultiplexSetsWorkingSet();
    7572
    7673    void eliminateSubsetConstraints();
     
    9794    ConstraintGraph             mConstraintGraph;
    9895
    99     AdvanceVariable             mAdvanceNegatedVariable;
     96    AdvanceVariable             mNegatedAdvance;
    10097    SubsetGraph                 mSubsetGraph;
    10198    CandidateGraph              mCandidateGraph;
Note: See TracChangeset for help on using the changeset viewer.