Changeset 5119
 Timestamp:
 Aug 8, 2016, 4:00:32 PM (3 years ago)
 Location:
 icGREP/icgrepdevel/icgrep/pablo/optimizers
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

icGREP/icgrepdevel/icgrep/pablo/optimizers/pablo_automultiplexing.cpp
r5113 r5119 22 22 using namespace boost::numeric::ublas; 23 23 24 /// Interesting test cases:25 /// ./icgrep c multiplexing '[\p{Lm}\p{Meetei_Mayek}]' disableifhierarchystrategy26 27 /// ./icgrep c multiplexing '\p{Imperial_Aramaic}(?<!\p{Sm})' disableifhierarchystrategy28 29 30 24 static cl::OptionCategory MultiplexingOptions("Multiplexing Optimization Options", "These options control the Pablo Multiplexing optimization pass."); 31 25 … … 42 36 #undef INITIAL_SEED_VALUE 43 37 44 static cl::opt<unsigned> SetLimit("multiplexingsetlimit", cl::init(std::numeric_limits<unsigned>::max()),45 cl::desc("maximum s ize of anycandidate set."),38 static cl::opt<unsigned> WindowSize("multiplexingwindowsize", cl::init(100), 39 cl::desc("maximum sequence distance to consider for candidate set."), 46 40 cl::cat(MultiplexingOptions)); 47 41 48 static cl::opt<unsigned> SelectionLimit("multiplexingselectionlimit", 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("multiplexingwindowsize", 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("multiplexingsamples", 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 multiplexingsetlimit)."),66 clEnumVal(WorkingSet, "choose multiplexing sets that share common input values."),67 clEnumValEnd),68 cl::init(Greedy),69 cl::cat(MultiplexingOptions));70 42 71 43 namespace pablo { 44 45 Z3_bool maxsat(Z3_context ctx, Z3_solver solver, std::vector<Z3_ast> & soft); 72 46 73 47 using TypeId = PabloAST::ClassTypeId; … … 79 53 bool MultiplexingPass::optimize(PabloFunction & function) { 80 54 81 #ifndef NDEBUG82 55 PabloVerifier::verify(function, "premultiplexing"); 83 #endif 56 57 errs() << "PREMULTIPLEXING\n==============================================\n"; 58 PabloPrinter::print(function, errs()); 84 59 85 60 Z3_config cfg = Z3_mk_config(); … … 96 71 Z3_del_context(ctx); 97 72 98 #ifndef NDEBUG99 73 PabloVerifier::verify(function, "postmultiplexing"); 100 #endif101 74 102 75 Simplifier::optimize(function); 76 77 errs() << "POSTMULTIPLEXING\n==============================================\n"; 78 PabloPrinter::print(function, errs()); 103 79 104 80 return true; … … 164 140 **  */ 165 141 void MultiplexingPass::multiplex(PabloBlock * const block, Statement * const begin, Statement * const end) { 166 if (generateCandidateSets( )) {142 if (generateCandidateSets(begin, end)) { 167 143 selectMultiplexSetsGreedy(); 168 144 eliminateSubsetConstraints(); … … 176 152 inline bool MultiplexingPass::equals(Z3_ast a, Z3_ast b) { 177 153 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? 179 155 Z3_inc_ref(mContext, test); 180 156 Z3_solver_assert(mContext, mSolver, test); … … 257 233 **  */ 258 234 inline Z3_ast MultiplexingPass::characterize(Advance * const adv, Z3_ast Ik) { 259 const auto k = m AdvanceNegatedVariable.size();235 const auto k = mNegatedAdvance.size(); 260 236 261 237 assert (adv); … … 293 269 } 294 270 unconstrained[i] = true; 295 296 271 } else if (equals(Ii, IiIk)) { 297 272 // If Ii = Ii â© Ik then Ii â Ik. Record this in the subset graph with the arc (i, k). … … 306 281 } 307 282 unconstrained[i] = true; 308 309 283 } else if (equals(Ik, IiIk)) { 310 284 // If Ik = Ii â© Ik then Ik â Ii. Record this in the subset graph with the arc (k, i). … … 318 292 unconstrained[i] = true; 319 293 } 320 321 294 Z3_dec_ref(mContext, IiIk); 322 295 Z3_solver_pop(mContext, mSolver, 1); … … 350 323 Z3_ast Ai = Z3_mk_and(mContext, 2, conj); 351 324 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); 353 326 Ai0 = Ai; 354 327 assert (get(mConstraintGraph[i]) == Ai); 355 328 356 vars[m++] = m AdvanceNegatedVariable[i];357 358 continue; // note: if these Advances are n'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. 359 332 } 360 333 add_edge(i, k, mConstraintGraph); 361 334 } 362 335 // To minimize the number of BDD computations, we store the negated variable instead of negating it each time. 363 m AdvanceNegatedVariable.emplace_back(Nk);336 mNegatedAdvance.emplace_back(Nk); 364 337 Z3_ast Ak = Z3_mk_and(mContext, m, vars); 365 338 if (LLVM_UNLIKELY(Ak != Ak0)) { … … 385 358 } 386 359 387 for (Z3_ast var : m AdvanceNegatedVariable) {360 for (Z3_ast var : mNegatedAdvance) { 388 361 Z3_dec_ref(mContext, var); 389 362 } 390 m AdvanceNegatedVariable.clear();363 mNegatedAdvance.clear(); 391 364 392 365 // Scan through and count all the advances and statements ... … … 454 427 455 428 mSubsetGraph = SubsetGraph(advances); 456 m AdvanceNegatedVariable.reserve(advances);429 mNegatedAdvance.reserve(advances); 457 430 458 431 return last; 432 } 433 434 435 /**  * 436 * @brief generateCandidateSets 437 **  */ 438 bool 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_m1 âš Â¬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 **  */ 535 void 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 nonterminal!"); 564 } 565 } 566 Z3_model_dec_ref(ctx, m); 567 } 568 Z3_solver_pop(ctx, solver, 1); 459 569 } 460 570 … … 465 575 static inline bool is_power_of_2(const size_t n) { 466 576 return ((n & (n  1)) == 0); 467 }468 469 /**  *470 * @brief generateCandidateSets471 **  */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 S489 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 choose540 *541 * Compute n choose k542 **  */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 select562 *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 updateCandidateSet580 **  */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 set603 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 addCandidateSet626 * @param S an independent set627 **  */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 samples645 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 }652 577 } 653 578 … … 689 614 degree_t r = degree(t, mCandidateGraph); 690 615 if (LLVM_LIKELY(r >= 3)) { // if this set has at least 3 elements. 691 r *= r;692 616 if (w < r) { 693 617 u = t; … … 738 662 } 739 663 #endif 740 }741 742 /**  *743 * @brief selectMultiplexSetsWorkingSet744 **  */745 void MultiplexingPass::selectMultiplexSetsWorkingSet() {746 747 // The inputs to each Advance must be different; otherwise the SimplificationPass would consider all but748 // one of the Advances redundant. However, if the input is short lived, we can ignore it in favour of its749 // 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 754 664 } 755 665 … … 802 712 803 713 ///**  * 804 // * Fu & Malik procedure for MaxSAT. This procedure is based on unsat core extraction and the atmostone constraint. 714 // * Topologically sort the sequence of instructions whilst trying to adhere as best as possible to the original 715 // * program sequence. 805 716 // **  */ 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]; 810 727 // 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; 813 745 // } 814 746 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); 817 799 // } 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 softconstraints 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 826 848 // 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!"); 839 860 // } 840 861 // } 841 862 // } 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 atmostone 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!"); 859 864 // return false; 860 865 //} … … 864 869 * @brief addWithHardConstraints 865 870 **  */ 866 Z3_ast addWithHardConstraints(Z3_context ctx, Z3_solver solver, PabloBlock * const block, Statement * stmt, flat_map<Statement *, Z3_ast> & M) {871 Z3_ast addWithHardConstraints(Z3_context ctx, Z3_solver solver, PabloBlock * const block, Statement * const stmt, flat_map<Statement *, Z3_ast> & M) { 867 872 assert (M.count(stmt) == 0 && stmt>getParent() == block); 868 873 // 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)))); 871 878 for (unsigned i = 0; i != stmt>getNumOperands(); ++i) { 872 879 PabloAST * const op = stmt>getOperand(i); … … 874 881 const auto f = M.find(cast<Statement>(op)); 875 882 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)); 878 884 } 879 885 } … … 881 887 M.emplace(stmt, node); 882 888 return node; 883 884 889 } 885 890 … … 937 942 assert (!end  isa<If>(end)  isa<While>(end)); 938 943 939 Statement * const ip = begin>getPrevNode(); // save our insertion point prior to modifying the AST940 941 944 Z3_config cfg = Z3_mk_config(); 942 //Z3_set_param_value(cfg, "MODEL", "true");945 Z3_set_param_value(cfg, "MODEL", "true"); 943 946 Z3_context ctx = Z3_mk_context(cfg); 944 947 Z3_del_config(cfg); 945 948 Z3_solver solver = Z3_mk_solver(ctx); 949 Z3_solver_inc_ref(ctx, solver); 946 950 947 951 const auto first_set = num_vertices(mConstraintGraph); 948 952 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 constraints962 // 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());982 953 983 954 for (auto idx = first_set; idx != last_set; ++idx) { … … 988 959 PabloAST * muxed[m]; 989 960 PabloAST * muxed_n[m]; 961 990 962 // The multiplex set graph is a DAG with edges denoting the set relationships of our independent sets. 991 963 unsigned i = 0; 992 964 for (const auto u : make_iterator_range(adjacent_vertices(idx, mCandidateGraph))) { 993 965 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])))); 996 969 ++i; 997 970 } 998 971 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 999 1014 circular_buffer<PabloAST *> Q(n); 1000 1015 1001 1016 /// Perform ntom Multiplexing 1002 for (size_t j = 0; j != m; ++j) { 1017 for (size_t j = 0; j != m; ++j) { 1003 1018 std::ostringstream prefix; 1004 1019 prefix << "mux" << n << "to" << m << '.' << (j); … … 1049 1064 assert (M.count(input[i]) == 0); 1050 1065 } 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); 1078 1104 Z3_del_context(ctx); 1079 1105 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 ntom 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 mton 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 //} 1089 1264 1090 1265 /**  * … … 1140 1315 inline Z3_ast MultiplexingPass::make(const PabloAST * const expr) { 1141 1316 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)); 1152 1318 Z3_inc_ref(mContext, node); 1153 1319 return add(expr, node); … … 1176 1342 1177 1343 1344 inline 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 1349 inline 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 1354 inline 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 */ 1375 void 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 */ 1392 unsigned 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 */ 1415 inline 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 */ 1422 void 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 */ 1448 void 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 atmostone constraint. 1466 **  */ 1467 Z3_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 softconstraints 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 1178 1528 } // end of namespace pablo 
icGREP/icgrepdevel/icgrep/pablo/optimizers/pablo_automultiplexing.hpp
r5113 r5119 28 28 using CharacterizationMap = llvm::DenseMap<const PabloAST *, CharacterizationRef>; 29 29 30 using ConstraintGraph = boost::adjacency_matrix<boost:: directedS, Advance *>;30 using ConstraintGraph = boost::adjacency_matrix<boost::undirectedS, Advance *>; 31 31 using ConstraintVertex = ConstraintGraph::vertex_descriptor; 32 32 using Constraints = std::vector<ConstraintVertex>; … … 36 36 using IntDistribution = std::uniform_int_distribution<RNG::result_type>; 37 37 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>; 39 39 using Candidates = std::vector<CandidateGraph::vertex_descriptor>; 40 40 … … 66 66 void multiplex(PabloBlock * const block, Statement * const begin, Statement * const end); 67 67 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); 72 70 73 71 void selectMultiplexSetsGreedy(); 74 void selectMultiplexSetsWorkingSet();75 72 76 73 void eliminateSubsetConstraints(); … … 97 94 ConstraintGraph mConstraintGraph; 98 95 99 AdvanceVariable m AdvanceNegatedVariable;96 AdvanceVariable mNegatedAdvance; 100 97 SubsetGraph mSubsetGraph; 101 98 CandidateGraph mCandidateGraph;
Note: See TracChangeset
for help on using the changeset viewer.