1. C++ / Говнокод #18139

    +142

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    15. 15
    16. 16
    17. 17
    18. 18
    19. 19
    20. 20
    21. 21
    22. 22
    23. 23
    24. 24
    25. 25
    26. 26
    27. 27
    28. 28
    29. 29
    30. 30
    31. 31
    32. 32
    33. 33
    34. 34
    35. 35
    36. 36
    37. 37
    38. 38
    39. 39
    40. 40
    41. 41
    42. 42
    43. 43
    44. 44
    45. 45
    46. 46
    47. 47
    48. 48
    49. 49
    50. 50
    51. 51
    52. 52
    53. 53
    54. 54
    55. 55
    56. 56
    57. 57
    58. 58
    59. 59
    60. 60
    61. 61
    62. 62
    63. 63
    64. 64
    65. 65
    66. 66
    67. 67
    68. 68
    69. 69
    70. 70
    71. 71
    72. 72
    73. 73
    74. 74
    75. 75
    76. 76
    77. 77
    78. 78
    79. 79
    80. 80
    81. 81
    82. 82
    83. 83
    84. 84
    85. 85
    86. 86
    87. 87
    88. 88
    typedef enum {
        INIT1=0, INIT2,  INIT3,  INIT4,  INIT5,  INIT6,  INITN,
        BIND1,   BIND2,  BIND3,  BIND4,  BIND5,  BIND6,  BINDN,
        YIELD1,  YIELD2, YIELD3, YIELD4, YIELD5, YIELD6, YIELDN, 
        COMPARE, CHECK, FILTER, CFILTER, PFILTER, CHOOSE, NOOP, CONTINUE,
        GET_ENODE, 
        GET_CGR1, GET_CGR2, GET_CGR3, GET_CGR4, GET_CGR5, GET_CGR6, GET_CGRN,
        IS_CGR
    } opcode;
...
...
...



        switch (m_pc->m_opcode) {
        case INIT1:
            m_app          = m_registers[0];
            if (m_app->get_num_args() != 1)
                goto backtrack;
            m_registers[1] = m_app->get_arg(0);
            m_pc = m_pc->m_next;
            goto main_loop;
            
        case INIT2:
            m_app          = m_registers[0];
            if (m_app->get_num_args() != 2)
                goto backtrack;
            m_registers[1] = m_app->get_arg(0);
            m_registers[2] = m_app->get_arg(1);
            m_pc = m_pc->m_next;
            goto main_loop;
            
        case INIT3:
            m_app          = m_registers[0];
            if (m_app->get_num_args() != 3)
                goto backtrack;
            m_registers[1] = m_app->get_arg(0);
            m_registers[2] = m_app->get_arg(1);
            m_registers[3] = m_app->get_arg(2);
            m_pc = m_pc->m_next;
            goto main_loop;
            
        case INIT4:
            m_app          = m_registers[0];
            if (m_app->get_num_args() != 4)
                goto backtrack;
            m_registers[1] = m_app->get_arg(0);
            m_registers[2] = m_app->get_arg(1);
            m_registers[3] = m_app->get_arg(2);
            m_registers[4] = m_app->get_arg(3);
            m_pc = m_pc->m_next;
            goto main_loop;
            
        case INIT5:
            m_app          = m_registers[0]; 
            if (m_app->get_num_args() != 5)
                goto backtrack;
            m_registers[1] = m_app->get_arg(0);
            m_registers[2] = m_app->get_arg(1);
            m_registers[3] = m_app->get_arg(2);
            m_registers[4] = m_app->get_arg(3);
            m_registers[5] = m_app->get_arg(4);
            m_pc = m_pc->m_next;
            goto main_loop;
            
        case INIT6: 
            m_app          = m_registers[0];
            if (m_app->get_num_args() != 6)
                goto backtrack;
            m_registers[1] = m_app->get_arg(0);
            m_registers[2] = m_app->get_arg(1);
            m_registers[3] = m_app->get_arg(2);
            m_registers[4] = m_app->get_arg(3);
            m_registers[5] = m_app->get_arg(4);
            m_registers[6] = m_app->get_arg(5);
            m_pc = m_pc->m_next;
            goto main_loop;
            
        case INITN:
            m_app      = m_registers[0];
            m_num_args = m_app->get_num_args();
            if (m_num_args != static_cast<const initn *>(m_pc)->m_num_args)
                goto backtrack;
            for (unsigned i = 0; i < m_num_args; i++)
                m_registers[i+1] = m_app->get_arg(i);
            m_pc = m_pc->m_next;
            goto main_loop;

    Из изходников STM-солвера Z3
    https://github.com/Z3Prover/z3/blob/master/src/smt/mam.cpp#L2298
    Почему нельзя было оставить только вариант INITN? Цикл отбирает так много ресурсов?

    Запостил: j123123, 10 Мая 2015

    Комментарии (2) RSS

    • ava Dummy00001 10.05.2015 14:23 # 0

      > Z3 is a theorem prover from Microsoft Research.

      вы ожидали чего-то лучшего? :)
      Ответить

    • ava roman-kashitsyn 10.05.2015 15:24 # +1

      Ну может померяли, и оказалось, что так быстрее на типичных инпутах.
      Ответить

    Добавить комментарий