oracleTable.cpp

//! \file
/*
**  Copyright (C) - Triton
**
**  This program is under the terms of the Apache License 2.0.
*/

#include <array>
#include <deque>
#include <map>

#include <triton/astEnums.hpp>
#include <triton/oracleEntry.hpp>



namespace triton {
  namespace engines {
    namespace synthesis {
      namespace oracles {

        //! The oracle table for unary operators. Each entry is a UnaryEntry object.
        /*! \brief Entry: <bits> <x value> <result> <operator> */
        std::map<triton::ast::ast_e, std::array<UnaryEntry, 40>> unopTable = {
          /* bvneg synthesis */
          {
            triton::ast::BVNEG_NODE, {
              UnaryEntry(8, 0x84, 0x7c), UnaryEntry(16, 0xf231, 0x0dcf), UnaryEntry(32, 0xdea0368a, 0x215fc976), UnaryEntry(64, 0x5ebb7410a9076a77, 0xa1448bef56f89589),
              UnaryEntry(8, 0xb1, 0x4f), UnaryEntry(16, 0x908a, 0x6f76), UnaryEntry(32, 0x5a3a5b2f, 0xa5c5a4d1), UnaryEntry(64, 0x16cae2f7e7d3fc97, 0xe9351d08182c0369),
              UnaryEntry(8, 0x31, 0xcf), UnaryEntry(16, 0x7eba, 0x8146), UnaryEntry(32, 0x4450a330, 0xbbaf5cd0), UnaryEntry(64, 0x6eb5594872f62607, 0x914aa6b78d09d9f9),
              UnaryEntry(8, 0x24, 0xdc), UnaryEntry(16, 0x0f3a, 0xf0c6), UnaryEntry(32, 0x5f849c9c, 0xa07b6364), UnaryEntry(64, 0x523c7aa7ea140cf6, 0xadc3855815ebf30a),
              UnaryEntry(8, 0x7a, 0x86), UnaryEntry(16, 0x6f5e, 0x90a2), UnaryEntry(32, 0x3eda78a1, 0xc125875f), UnaryEntry(64, 0xe2b22250f677c90a, 0x1d4dddaf098836f6),
              UnaryEntry(8, 0xfb, 0x05), UnaryEntry(16, 0xeaf3, 0x150d), UnaryEntry(32, 0xf606f29e, 0x09f90d62), UnaryEntry(64, 0xc25139f6c56e2b1a, 0x3daec6093a91d4e6),
              UnaryEntry(8, 0xdf, 0x21), UnaryEntry(16, 0xf446, 0x0bba), UnaryEntry(32, 0xb3152d26, 0x4cead2da), UnaryEntry(64, 0xa6a5c5db99af6292, 0x595a3a2466509d6e),
              UnaryEntry(8, 0x90, 0x70), UnaryEntry(16, 0xbe65, 0x419b), UnaryEntry(32, 0x6875f40f, 0x978a0bf1), UnaryEntry(64, 0xb32040a2bc375160, 0x4cdfbf5d43c8aea0),
              UnaryEntry(8, 0xf5, 0x0b), UnaryEntry(16, 0xfc94, 0x036c), UnaryEntry(32, 0x43937e0a, 0xbc6c81f6), UnaryEntry(64, 0xf088f5479deb9f86, 0x0f770ab86214607a),
              UnaryEntry(8, 0x82, 0x7e), UnaryEntry(16, 0xfd23, 0x02dd), UnaryEntry(32, 0xa78178e3, 0x587e871d), UnaryEntry(64, 0x9070b8c2438a7d2d, 0x6f8f473dbc7582d3),
            }
          },
          /* bvnot synthesis */
          {
            triton::ast::BVNOT_NODE, {
              UnaryEntry(8, 0xbf, 0x40), UnaryEntry(16, 0xa534, 0x5acb), UnaryEntry(32, 0xe615f7a1, 0x19ea085e), UnaryEntry(64, 0x7e2d19f3e35fa723, 0x81d2e60c1ca058dc),
              UnaryEntry(8, 0x07, 0xf8), UnaryEntry(16, 0xcbfb, 0x3404), UnaryEntry(32, 0xf0033666, 0x0ffcc999), UnaryEntry(64, 0x74b2231ce11018aa, 0x8b4ddce31eefe755),
              UnaryEntry(8, 0xad, 0x52), UnaryEntry(16, 0x952a, 0x6ad5), UnaryEntry(32, 0x4b6a154b, 0xb495eab4), UnaryEntry(64, 0x1e6a1f352e994b3d, 0xe195e0cad166b4c2),
              UnaryEntry(8, 0x37, 0xc8), UnaryEntry(16, 0x8ae7, 0x7518), UnaryEntry(32, 0x4cda9ed4, 0xb325612b), UnaryEntry(64, 0xc8512c92c9727132, 0x37aed36d368d8ecd),
              UnaryEntry(8, 0x86, 0x79), UnaryEntry(16, 0xbb3c, 0x44c3), UnaryEntry(32, 0x18d1e778, 0xe72e1887), UnaryEntry(64, 0xbeba68945a58db0e, 0x4145976ba5a724f1),
              UnaryEntry(8, 0xb1, 0x4e), UnaryEntry(16, 0x872e, 0x78d1), UnaryEntry(32, 0x25718016, 0xda8e7fe9), UnaryEntry(64, 0x423a32a97ea6daf7, 0xbdc5cd5681592508),
              UnaryEntry(8, 0x5d, 0xa2), UnaryEntry(16, 0x82fe, 0x7d01), UnaryEntry(32, 0xb9b70129, 0x4648fed6), UnaryEntry(64, 0xa349cf97698b719b, 0x5cb6306896748e64),
              UnaryEntry(8, 0x30, 0xcf), UnaryEntry(16, 0x9694, 0x696b), UnaryEntry(32, 0x5fa761a9, 0xa0589e56), UnaryEntry(64, 0x5cddd977d5a8990e, 0xa32226882a5766f1),
              UnaryEntry(8, 0x17, 0xe8), UnaryEntry(16, 0x3d85, 0xc27a), UnaryEntry(32, 0x7f90f323, 0x806f0cdc), UnaryEntry(64, 0xcb1e51195c5cd301, 0x34e1aee6a3a32cfe),
              UnaryEntry(8, 0x94, 0x6b), UnaryEntry(16, 0xf83f, 0x07c0), UnaryEntry(32, 0x0edc448e, 0xf123bb71), UnaryEntry(64, 0x5e1415d881b3c360, 0xa1ebea277e4c3c9f),
            }
          },
          /* bswap synthesis */
          {
            triton::ast::BSWAP_NODE, {
              UnaryEntry(8, 0x27, 0x27), UnaryEntry(16, 0xcb3e, 0x3ecb), UnaryEntry(32, 0xff2fd55f, 0x5fd52fff), UnaryEntry(64, 0xa88db124f3f781ac, 0xac81f7f324b18da8),
              UnaryEntry(8, 0x51, 0x51), UnaryEntry(16, 0x5b4f, 0x4f5b), UnaryEntry(32, 0xbf2b3aa8, 0xa83a2bbf), UnaryEntry(64, 0x1e505703753e938c, 0x8c933e750357501e),
              UnaryEntry(8, 0x9c, 0x9c), UnaryEntry(16, 0x7432, 0x3274), UnaryEntry(32, 0xa3dfc3f8, 0xf8c3dfa3), UnaryEntry(64, 0xe56f7ec839cac245, 0x45c2ca39c87e6fe5),
              UnaryEntry(8, 0xa1, 0xa1), UnaryEntry(16, 0x9b5c, 0x5c9b), UnaryEntry(32, 0x31899f06, 0x069f8931), UnaryEntry(64, 0x1043e5a76ee28a0b, 0x0b8ae26ea7e54310),
              UnaryEntry(8, 0xbd, 0xbd), UnaryEntry(16, 0x3752, 0x5237), UnaryEntry(32, 0x2e91aa5e, 0x5eaa912e), UnaryEntry(64, 0x18491fc165c2e982, 0x82e9c265c11f4918),
              UnaryEntry(8, 0xb2, 0xb2), UnaryEntry(16, 0x569e, 0x9e56), UnaryEntry(32, 0x04e142dd, 0xdd42e104), UnaryEntry(64, 0xcf8d996c9e669774, 0x7497669e6c998dcf),
              UnaryEntry(8, 0x5f, 0x5f), UnaryEntry(16, 0x6bf3, 0xf36b), UnaryEntry(32, 0x67bce895, 0x95e8bc67), UnaryEntry(64, 0xae03b5679bc74ec8, 0xc84ec79b67b503ae),
              UnaryEntry(8, 0x5f, 0x5f), UnaryEntry(16, 0xf654, 0x54f6), UnaryEntry(32, 0xe000a10b, 0x0ba100e0), UnaryEntry(64, 0xcf6cadb6fc9ba591, 0x91a59bfcb6ad6ccf),
              UnaryEntry(8, 0xe5, 0xe5), UnaryEntry(16, 0x0593, 0x9305), UnaryEntry(32, 0x8e67df26, 0x26df678e), UnaryEntry(64, 0xda908c7dc0afaace, 0xceaaafc07d8c90da),
              UnaryEntry(8, 0xea, 0xea), UnaryEntry(16, 0xc035, 0x35c0), UnaryEntry(32, 0x25438920, 0x20894325), UnaryEntry(64, 0xfe8b2d171004f9e1, 0xe1f90410172d8bfe),
            }
          },
        };


        //! The oracle table for binary operators. Each entry is a BinaryEntry object.
        /*! \brief Entry: <bits> <x value> <y value> <result> <operator> */
        std::map<triton::ast::ast_e, std::array<BinaryEntry, 40>> binopTable = {
          /* bvadd synthesis */
          {
            triton::ast::BVADD_NODE, {
              BinaryEntry(8, 0x2a, 0x21, 0x4b), BinaryEntry(16, 0xf7c6, 0xa071, 0x9837), BinaryEntry(32, 0x21cf24bb, 0x928b1c0c, 0xb45a40c7), BinaryEntry(64, 0x2b770af9386bf896, 0x088426db5a2d6527, 0x33fb31d492995dbd),
              BinaryEntry(8, 0x6e, 0x33, 0xa1), BinaryEntry(16, 0x400a, 0x419c, 0x81a6), BinaryEntry(32, 0xdf7cba6c, 0x8f4b81be, 0x6ec83c2a), BinaryEntry(64, 0xcdc86e0594a07ef6, 0x9134f30afb218ec7, 0x5efd61108fc20dbd),
              BinaryEntry(8, 0xf8, 0x7f, 0x77), BinaryEntry(16, 0xcfd6, 0xee27, 0xbdfd), BinaryEntry(32, 0x7caa704b, 0x83c1f886, 0x006c68d1), BinaryEntry(64, 0x702afe18034a476a, 0x052daa255ecc76bc, 0x7558a83d6216be26),
              BinaryEntry(8, 0x56, 0x6d, 0xc3), BinaryEntry(16, 0xe17f, 0x3a59, 0x1bd8), BinaryEntry(32, 0x0e4d2d01, 0x611ac4e7, 0x6f67f1e8), BinaryEntry(64, 0x2fae54a6bc40ea5b, 0x0fcb9e3f309025c5, 0x3f79f2e5ecd11020),
              BinaryEntry(8, 0xb9, 0xd2, 0x8b), BinaryEntry(16, 0xfddc, 0x7319, 0x70f5), BinaryEntry(32, 0x177bcd65, 0x3f010d62, 0x567cdac7), BinaryEntry(64, 0x6fb11b935f9aae69, 0x8fd0c575be50e5ae, 0xff81e1091deb9417),
              BinaryEntry(8, 0x47, 0x02, 0x49), BinaryEntry(16, 0x091f, 0xd2b9, 0xdbd8), BinaryEntry(32, 0x96e4d147, 0xb36174b2, 0x4a4645f9), BinaryEntry(64, 0xdeccc2958f0127ff, 0xc35a846ae4563870, 0xa22747007357606f),
              BinaryEntry(8, 0xfc, 0x7e, 0x7a), BinaryEntry(16, 0xfb24, 0xe45c, 0xdf80), BinaryEntry(32, 0x6d67c2b5, 0x8c26e4cf, 0xf98ea784), BinaryEntry(64, 0x6fe70127efad1a04, 0x1afc9543e7e5d960, 0x8ae3966bd792f364),
              BinaryEntry(8, 0x75, 0xd7, 0x4c), BinaryEntry(16, 0x209d, 0x8aa8, 0xab45), BinaryEntry(32, 0xc784d851, 0x2d0b3d67, 0xf49015b8), BinaryEntry(64, 0x4aad31129617209d, 0xd53de47dd51a05c1, 0x1feb15906b31265e),
              BinaryEntry(8, 0x62, 0xbc, 0x1e), BinaryEntry(16, 0x9de8, 0xf61e, 0x9406), BinaryEntry(32, 0x03650979, 0x61fd65af, 0x65626f28), BinaryEntry(64, 0xf91d6f62b4d8d216, 0x1a24d7edcd3c29d9, 0x134247508214fbef),
              BinaryEntry(8, 0x1f, 0xe6, 0x05), BinaryEntry(16, 0x92b4, 0x23f8, 0xb6ac), BinaryEntry(32, 0x83ebae14, 0xe91c1970, 0x6d07c784), BinaryEntry(64, 0x31e1e94e9a3b0296, 0xe64d9b88986f516f, 0x182f84d732aa5405),
            }
          },
          /* bvand synthesis */
          {
            triton::ast::BVAND_NODE, {
              BinaryEntry(8, 0x41, 0x56, 0x40), BinaryEntry(16, 0x2f2d, 0x6343, 0x2301), BinaryEntry(32, 0x2683960f, 0x44198cc7, 0x04018407), BinaryEntry(64, 0x775697891b1bc1ed, 0x9d9c8274e6a8d54f, 0x151482000208c14d),
              BinaryEntry(8, 0x8c, 0x7d, 0x0c), BinaryEntry(16, 0xfabf, 0x251e, 0x201e), BinaryEntry(32, 0x8717c7e2, 0x0eacd9c8, 0x0604c1c0), BinaryEntry(64, 0xe961866f1744589d, 0x1579a57539690e1b, 0x0161846511400819),
              BinaryEntry(8, 0x3e, 0x96, 0x16), BinaryEntry(16, 0xf64a, 0xfdfc, 0xf448), BinaryEntry(32, 0x6e7275f0, 0x4a746452, 0x4a706450), BinaryEntry(64, 0x25b33c982504da01, 0x6c14d1e146f051f6, 0x2410108004005000),
              BinaryEntry(8, 0x12, 0xfc, 0x10), BinaryEntry(16, 0x55e6, 0xd397, 0x5186), BinaryEntry(32, 0x78cc0ac9, 0xe0fff1df, 0x60cc00c9), BinaryEntry(64, 0x37eb86e7dc325e59, 0x836f18c7dd73cadb, 0x036b00c7dc324a59),
              BinaryEntry(8, 0xbf, 0x42, 0x02), BinaryEntry(16, 0x3b40, 0x6b0c, 0x2b00), BinaryEntry(32, 0x770516b3, 0xaca49ff0, 0x240416b0), BinaryEntry(64, 0x623bb77ffa92c305, 0x0d8d39ecdf75c8f7, 0x0009316cda10c005),
              BinaryEntry(8, 0xfa, 0x5c, 0x58), BinaryEntry(16, 0x6d47, 0x5658, 0x4440), BinaryEntry(32, 0x56defbdc, 0xb25bcca8, 0x125ac888), BinaryEntry(64, 0xcb96ee2b95884779, 0x71c6aea15cfee3da, 0x4186ae2114884358),
              BinaryEntry(8, 0xde, 0xdb, 0xda), BinaryEntry(16, 0xb539, 0xb566, 0xb520), BinaryEntry(32, 0xe5bf3331, 0xd4baef67, 0xc4ba2321), BinaryEntry(64, 0xa613e8bf3b2b7424, 0x1c7a459fa6bd97e8, 0x0412409f22291420),
              BinaryEntry(8, 0x71, 0xdb, 0x51), BinaryEntry(16, 0x560f, 0xb7ce, 0x160e), BinaryEntry(32, 0x82ab1b76, 0x81adb128, 0x80a91120), BinaryEntry(64, 0x00081a318bae99c4, 0xfffe33817cc13f29, 0x0008120108801900),
              BinaryEntry(8, 0x91, 0xa5, 0x81), BinaryEntry(16, 0x7470, 0x21c3, 0x2040), BinaryEntry(32, 0x8fdac274, 0x3c262a67, 0x0c020264), BinaryEntry(64, 0x3e0e94dab0ea3ab9, 0x62ecd72f3bf4cc33, 0x220c940a30e00831),
              BinaryEntry(8, 0x92, 0x18, 0x10), BinaryEntry(16, 0xa3a0, 0xc540, 0x8100), BinaryEntry(32, 0xa01a2abe, 0xc2e8709e, 0x8008209e), BinaryEntry(64, 0x1095087eac2f0f7c, 0x45f8782be2092282, 0x0090082aa0090200),
            }
          },
          /* bvmul synthesis */
          {
            triton::ast::BVMUL_NODE, {
              BinaryEntry(8, 0xe6, 0x59, 0xf6), BinaryEntry(16, 0xc449, 0x493c, 0xd21c), BinaryEntry(32, 0xb7801c01, 0x15239bf6, 0xcf3283f6), BinaryEntry(64, 0x75fef9b741b28f26, 0xa92ed6125c644f8e, 0x3abbbaca1e102114),
              BinaryEntry(8, 0x9a, 0xa8, 0x10), BinaryEntry(16, 0xab08, 0xd202, 0xe610), BinaryEntry(32, 0x063bf86a, 0xecab0d7d, 0xbdb3adc2), BinaryEntry(64, 0x722cfb8a7f1d58ad, 0xa12d93a527a9b6e9, 0x38cf48cf73f5b375),
              BinaryEntry(8, 0x13, 0x09, 0xab), BinaryEntry(16, 0x6598, 0xa942, 0x8930), BinaryEntry(32, 0x04f690aa, 0x3fa04a85, 0x1a2a4c52), BinaryEntry(64, 0x093fec4daa861116, 0xf0ace022b3e1b013, 0xb03c11b33a0864a2),
              BinaryEntry(8, 0x06, 0x31, 0x26), BinaryEntry(16, 0xa519, 0x859b, 0xf323), BinaryEntry(32, 0x90d07d98, 0x59e2ab5e, 0x28a2a5d0), BinaryEntry(64, 0x71c981dfbcdc3516, 0x3ac42c5b6747556c, 0x8f6ab5595da0b348),
              BinaryEntry(8, 0x2c, 0xe6, 0x88), BinaryEntry(16, 0xeb08, 0xf8c4, 0xb220), BinaryEntry(32, 0x00221248, 0x874b8879, 0x7ce8e408), BinaryEntry(64, 0xd9b72a9640035d88, 0x526271c7459d3964, 0x0e64fdefc58bd120),
              BinaryEntry(8, 0x78, 0xd1, 0xf8), BinaryEntry(16, 0xae3a, 0xcb5c, 0x9ad8), BinaryEntry(32, 0x2429f997, 0xf18c939d, 0xeda3c69b), BinaryEntry(64, 0xdfaccf1fcaa06a45, 0x2a311e48a717cd36, 0x5c20f91bc222ab8e),
              BinaryEntry(8, 0xb2, 0x35, 0xda), BinaryEntry(16, 0x7cf0, 0x9b83, 0x3ed0), BinaryEntry(32, 0x07ae4034, 0xb20ea0da, 0x1d5b2c48), BinaryEntry(64, 0x75e4132155ad122d, 0x87c049d1030a4462, 0x82ed393b01d6e93a),
              BinaryEntry(8, 0x32, 0xa7, 0x9e), BinaryEntry(16, 0x015c, 0x46f4, 0x73b0), BinaryEntry(32, 0x3de6b960, 0x931681ec, 0x625c4480), BinaryEntry(64, 0x7f7c443dc0c03e68, 0xc17252cf5f8e1403, 0x9a51a7ab7cd0db38),
              BinaryEntry(8, 0x4c, 0xf3, 0x24), BinaryEntry(16, 0xf18f, 0xac92, 0xd78e), BinaryEntry(32, 0xef803d1b, 0x30bbb52a, 0xa8f71d6e), BinaryEntry(64, 0x90d4819e98184e8e, 0x82580a34a3950e5b, 0x7b9840b38795b07a),
              BinaryEntry(8, 0xb7, 0xa2, 0xce), BinaryEntry(16, 0x68dd, 0x693d, 0xa1a9), BinaryEntry(32, 0xd1ced77d, 0x1dde70fa, 0x69ab2012), BinaryEntry(64, 0x443c83b1204c3365, 0xc90dac7bd0f3edab, 0x25fc11d4f759d577),
            }
          },
          /* bvnand synthesis */
          {
            triton::ast::BVNAND_NODE, {
              BinaryEntry(8, 0x9b, 0xb3, 0x6c), BinaryEntry(16, 0x51e7, 0x086c, 0xff9b), BinaryEntry(32, 0xac6d2e6e, 0x09728fae, 0xf79ff1d1), BinaryEntry(64, 0x31191b8fb5bd591e, 0x8661e0859745ed44, 0xfffeff7a6afab6fb),
              BinaryEntry(8, 0x8d, 0x3c, 0xf3), BinaryEntry(16, 0x24c3, 0xbc0f, 0xdbfc), BinaryEntry(32, 0x8a53cb9e, 0xcc9b9d82, 0x77ec767d), BinaryEntry(64, 0x20cdb8d30b2c872e, 0x1a79c25b6eea591f, 0xffb67facf5d7fef1),
              BinaryEntry(8, 0x80, 0xae, 0x7f), BinaryEntry(16, 0x980e, 0xde0b, 0x67f5), BinaryEntry(32, 0x0644dec0, 0x705aeb74, 0xffbf35bf), BinaryEntry(64, 0x0eda7d4dcf18af58, 0x5fe1d5bafdbbe797, 0xf13faaf732e758ef),
              BinaryEntry(8, 0xa0, 0x6e, 0xdf), BinaryEntry(16, 0x5615, 0x2aaa, 0xfdff), BinaryEntry(32, 0x67f62a9c, 0x0341c815, 0xfcbff7eb), BinaryEntry(64, 0x913c934e582f15df, 0x6c570e5b794242d8, 0xffebfdb5a7fdff27),
              BinaryEntry(8, 0x10, 0xd4, 0xef), BinaryEntry(16, 0x339d, 0xef67, 0xdcfa), BinaryEntry(32, 0x031ce808, 0x7e120f37, 0xfdeff7ff), BinaryEntry(64, 0x5738c5e01df45f9c, 0xd9046fa4c6f3a7b4, 0xaeffba5ffb0ff86b),
              BinaryEntry(8, 0x68, 0x28, 0xd7), BinaryEntry(16, 0xbcb1, 0xffbd, 0x434e), BinaryEntry(32, 0x2990b69d, 0x96a52a58, 0xff7fdde7), BinaryEntry(64, 0xcb7323439a04064c, 0x4a9bb3d1f45c0c95, 0xb5ecdcbe6ffbfbfb),
              BinaryEntry(8, 0x87, 0xe3, 0x7c), BinaryEntry(16, 0xf61c, 0x368b, 0xc9f7), BinaryEntry(32, 0xa4806508, 0x861ebb50, 0x7bffdeff), BinaryEntry(64, 0x812f65ef1a2c74af, 0xa57c1979296da2cb, 0x7ed3fe96f7d3df74),
              BinaryEntry(8, 0x82, 0x09, 0xff), BinaryEntry(16, 0x9fbe, 0x5b33, 0xe4cd), BinaryEntry(32, 0x9f5919ac, 0x3554d3c0, 0xeaafee7f), BinaryEntry(64, 0x8ac559764a83d87f, 0x4867c1b7603be9c9, 0xf7babec9bffc37b6),
              BinaryEntry(8, 0x3a, 0x5b, 0xe5), BinaryEntry(16, 0xf90c, 0x844f, 0x7ff3), BinaryEntry(32, 0xf3eaf858, 0xd394436b, 0x2c7fbfb7), BinaryEntry(64, 0x52f4e32aa0a500c4, 0xd7e2bf074a9185e0, 0xad1f5cfdff7eff3f),
              BinaryEntry(8, 0x1d, 0x86, 0xfb), BinaryEntry(16, 0x635b, 0xcc8b, 0xbff4), BinaryEntry(32, 0x7c2d23fc, 0xa064cbf7, 0xdfdbfc0b), BinaryEntry(64, 0x26c8a45fe769bbb7, 0xc05b02e87671b11a, 0xffb7ffb7999e4eed),
            }
          },
          /* bvnor synthesis */
          {
            triton::ast::BVNOR_NODE, {
              BinaryEntry(8, 0x92, 0xf1, 0x0c), BinaryEntry(16, 0xc675, 0x2401, 0x198a), BinaryEntry(32, 0x8493e564, 0x45948ddf, 0x3a681200), BinaryEntry(64, 0x94369fb29c1aa344, 0x10959136f158dc36, 0x6b48604902a50089),
              BinaryEntry(8, 0xb6, 0xc4, 0x09), BinaryEntry(16, 0xaa95, 0xca92, 0x1568), BinaryEntry(32, 0x0db77e10, 0x764c5d35, 0x800080ca), BinaryEntry(64, 0x26c6cf26d38fc16a, 0xeb9db352b62218fb, 0x1020008908502604),
              BinaryEntry(8, 0xd2, 0x7e, 0x01), BinaryEntry(16, 0xbca1, 0x7ec3, 0x011c), BinaryEntry(32, 0x2f79a53a, 0xc1bca911, 0x100252c4), BinaryEntry(64, 0x9133f773268cbf47, 0x117ece3e0a587c5d, 0x6e800080d12300a0),
              BinaryEntry(8, 0x64, 0x0b, 0x90), BinaryEntry(16, 0x6643, 0x076c, 0x9890), BinaryEntry(32, 0x5eb63fdb, 0x1ee94f28, 0xa1008004), BinaryEntry(64, 0x2121c94afd84446a, 0x2b057f07d5beef4d, 0xd4da00b002411090),
              BinaryEntry(8, 0x4e, 0x38, 0x81), BinaryEntry(16, 0x0e3b, 0x22a4, 0xd140), BinaryEntry(32, 0xd9b6ab9f, 0xfdb61360, 0x02494400), BinaryEntry(64, 0x0846f97151398c3e, 0x860968f8bab42aaa, 0x71b0060604425141),
              BinaryEntry(8, 0xc6, 0xe3, 0x18), BinaryEntry(16, 0xfa2c, 0xae40, 0x0193), BinaryEntry(32, 0x1dc43cdb, 0xe5a9b9fe, 0x02124200), BinaryEntry(64, 0x2120a60aeb56eb5e, 0xe7435e08a51d7c30, 0x189c01f510a00081),
              BinaryEntry(8, 0x29, 0x55, 0x82), BinaryEntry(16, 0xd4e0, 0x4c30, 0x230f), BinaryEntry(32, 0x83a0a9e1, 0xd2a207af, 0x2c5d5010), BinaryEntry(64, 0xd15711aa49e9f0a8, 0xd00621a2bc22a774, 0x2ea8ce5502140803),
              BinaryEntry(8, 0x8a, 0x65, 0x10), BinaryEntry(16, 0xb1f2, 0xc9af, 0x0600), BinaryEntry(32, 0x300a3a70, 0x2eb026a6, 0xc145c109), BinaryEntry(64, 0xfd06aa2bea7123fc, 0xb1ee6eecf6b7ee72, 0x0211111001081001),
              BinaryEntry(8, 0x02, 0x10, 0xed), BinaryEntry(16, 0x293d, 0xa0ca, 0x5600), BinaryEntry(32, 0x6d4747a0, 0x38eebb60, 0x8210001f), BinaryEntry(64, 0x2c3a4673228b5bd4, 0x9fe8a1af1ecfecf5, 0x40051800c130000a),
              BinaryEntry(8, 0xb0, 0x18, 0x47), BinaryEntry(16, 0x840e, 0x10b5, 0x6b40), BinaryEntry(32, 0x4e468c83, 0xa811c03a, 0x11a83344), BinaryEntry(64, 0x271b90da8422dcd7, 0x173dda34fddd50a2, 0xc8c0250102002308),
            }
          },
          /* bvor synthesis */
          {
            triton::ast::BVOR_NODE, {
              BinaryEntry(8, 0xa9, 0x0f, 0xaf), BinaryEntry(16, 0x401c, 0x6101, 0x611d), BinaryEntry(32, 0x9988499a, 0x14c70dde, 0x9dcf4dde), BinaryEntry(64, 0xf0b21f4ebcca4f91, 0x02afafba29c90548, 0xf2bfbffebdcb4fd9),
              BinaryEntry(8, 0x54, 0xa7, 0xf7), BinaryEntry(16, 0x0801, 0x85ad, 0x8dad), BinaryEntry(32, 0x043e41a3, 0xfb1f395f, 0xff3f79ff), BinaryEntry(64, 0xac04b729896ae417, 0x21a82322d873e344, 0xadacb72bd97be757),
              BinaryEntry(8, 0xc9, 0x70, 0xf9), BinaryEntry(16, 0x19de, 0x1cb0, 0x1dfe), BinaryEntry(32, 0x01532e2f, 0x1f8d8b7a, 0x1fdfaf7f), BinaryEntry(64, 0x6cb3c7d25a4e8e46, 0x494b0b9795b381d2, 0x6dfbcfd7dfff8fd6),
              BinaryEntry(8, 0xd3, 0xa8, 0xfb), BinaryEntry(16, 0x9467, 0x6cda, 0xfcff), BinaryEntry(32, 0xd553cdc5, 0xbb0cbc6d, 0xff5ffded), BinaryEntry(64, 0xd0b3c262ac968367, 0x585a9e0d0c1e143a, 0xd8fbde6fac9e977f),
              BinaryEntry(8, 0x39, 0x7d, 0x7d), BinaryEntry(16, 0x689e, 0x66d5, 0x6edf), BinaryEntry(32, 0x6c66f1a5, 0xb13523bb, 0xfd77f3bf), BinaryEntry(64, 0xf7484193f4f4d43d, 0x859eb81a198b205e, 0xf7def99bfdfff47f),
              BinaryEntry(8, 0xb2, 0x1a, 0xba), BinaryEntry(16, 0xd771, 0xb697, 0xf7f7), BinaryEntry(32, 0x5eecade5, 0xea0a06ac, 0xfeeeafed), BinaryEntry(64, 0xef09d7da651f08e7, 0x7f73ef2d401d0e73, 0xff7bffff651f0ef7),
              BinaryEntry(8, 0x46, 0x60, 0x66), BinaryEntry(16, 0xa827, 0x2540, 0xad67), BinaryEntry(32, 0x79cfae1e, 0x844992a9, 0xfdcfbebf), BinaryEntry(64, 0xb25bb85d26ec7359, 0x4e4accfc5a45ce76, 0xfe5bfcfd7eedff7f),
              BinaryEntry(8, 0x36, 0x32, 0x36), BinaryEntry(16, 0x8e7d, 0x0260, 0x8e7d), BinaryEntry(32, 0x78aa3415, 0xeb0dbcb9, 0xfbafbcbd), BinaryEntry(64, 0xaf14dd9c58dbaa48, 0x647f240c7a25bb37, 0xef7ffd9c7affbb7f),
              BinaryEntry(8, 0x11, 0x6d, 0x7d), BinaryEntry(16, 0x3f31, 0xd2ef, 0xffff), BinaryEntry(32, 0x7ca6a35a, 0xfde03bbf, 0xfde6bbff), BinaryEntry(64, 0xa7759db91346a3a3, 0x3e379bca6c2bed4f, 0xbf779ffb7f6fefef),
              BinaryEntry(8, 0x8f, 0x20, 0xaf), BinaryEntry(16, 0xacdc, 0xabf5, 0xaffd), BinaryEntry(32, 0x82727599, 0xf629a089, 0xf67bf599), BinaryEntry(64, 0xc3037dbb9d3dfd78, 0x0347e7c8019999e3, 0xc347fffb9dbdfdfb),
            }
          },
          /* bvrol synthesis */
          {
            triton::ast::BVROL_NODE, {
              BinaryEntry(8, 0xeb, 0x33, 0x5f), BinaryEntry(16, 0xdfae, 0xdca3, 0xfd76), BinaryEntry(32, 0x60fa061c, 0x5c4cab20, 0x60fa061c), BinaryEntry(64, 0x95f5eaaefb6a61cc, 0xa398742d4fa33209, 0xebd55df6d4c3992b),
              BinaryEntry(8, 0xe6, 0x0c, 0x6e), BinaryEntry(16, 0xd5a6, 0x2c25, 0xb4da), BinaryEntry(32, 0x3c134127, 0x6cf4f38d, 0x6824e782), BinaryEntry(64, 0x0e6ec9caae30e059, 0x4eab62ebda7fbe5b, 0x55718702c873764e),
              BinaryEntry(8, 0xb6, 0xf8, 0xb6), BinaryEntry(16, 0x0371, 0x29f6, 0xdc40), BinaryEntry(32, 0x24ecb909, 0x01b253c9, 0xd9721249), BinaryEntry(64, 0x915e5664e9e45ad2, 0xaae6d1ec39efae80, 0x915e5664e9e45ad2),
              BinaryEntry(8, 0xfd, 0x14, 0xdf), BinaryEntry(16, 0x5c26, 0x7a38, 0x265c), BinaryEntry(32, 0xf0a1b439, 0xcaf2222f, 0xda1cf850), BinaryEntry(64, 0x41b9ddbe9243ae07, 0x18d13c4e3b8f5bec, 0x3ae0741b9ddbe924),
              BinaryEntry(8, 0x2d, 0x41, 0x5a), BinaryEntry(16, 0x75b2, 0x9577, 0xd93a), BinaryEntry(32, 0x5c8f90e5, 0xc6854743, 0xe47c872a), BinaryEntry(64, 0xbf13900a937a166a, 0x347c72e1ca0b89aa, 0xe859aafc4e402a4d),
              BinaryEntry(8, 0x6c, 0x23, 0x63), BinaryEntry(16, 0x9fc3, 0xc18b, 0x1cfe), BinaryEntry(32, 0xebdb539d, 0xf9031da5, 0x7b6a73bd), BinaryEntry(64, 0x6de6684e8fdfc37b, 0x5f0f5a3b22b84f69, 0xbf86f6dbccd09d1f),
              BinaryEntry(8, 0x2a, 0x74, 0xa2), BinaryEntry(16, 0xc819, 0xff77, 0x0ce4), BinaryEntry(32, 0xce57baf7, 0x427e1b0c, 0x7baf7ce5), BinaryEntry(64, 0x2bcdf3d6c1fafb20, 0xc797c1405929fa9f, 0x60fd7d9015e6f9eb),
              BinaryEntry(8, 0x4d, 0xc2, 0x35), BinaryEntry(16, 0xd236, 0x02f4, 0x236d), BinaryEntry(32, 0x2c4c8dc3, 0xc2adc5c5, 0x8991b865), BinaryEntry(64, 0x646daec9992de182, 0x5cefe50573257c0d, 0xb5d93325bc304c8d),
              BinaryEntry(8, 0xc9, 0xa7, 0xe4), BinaryEntry(16, 0x124a, 0x7759, 0x9424), BinaryEntry(32, 0x3efa9b3e, 0xa0e5d00e, 0xa6cf8fbe), BinaryEntry(64, 0x7a09b3fb46d3a6fb, 0xfbf878ae7d6c1858, 0xfb46d3a6fb7a09b3),
              BinaryEntry(8, 0xe6, 0x40, 0xe6), BinaryEntry(16, 0x295c, 0xe433, 0x4ae1), BinaryEntry(32, 0x1948df3d, 0x6bced321, 0x3291be7a), BinaryEntry(64, 0x449a0a274cdff5bc, 0xd1b83681b2f04189, 0x34144e99bfeb7889),
            }
          },
          /* bvror synthesis */
          {
            triton::ast::BVROR_NODE, {
              BinaryEntry(8, 0x0d, 0xe0, 0x0d), BinaryEntry(16, 0x22ae, 0x4aef, 0x455c), BinaryEntry(32, 0x3c1c1862, 0xc76f2414, 0xc18623c1), BinaryEntry(64, 0xee87ac50704100ad, 0x687376f0dd11a4aa, 0x141c10402b7ba1eb),
              BinaryEntry(8, 0x74, 0xf9, 0x3a), BinaryEntry(16, 0x1756, 0x7c07, 0xac2e), BinaryEntry(32, 0xce5cd993, 0xe1c106f8, 0x5cd993ce), BinaryEntry(64, 0x1a98090ffa6d7028, 0x791be9ecbe6966ab, 0x21ff4dae05035301),
              BinaryEntry(8, 0xbd, 0x76, 0xf6), BinaryEntry(16, 0xa6b3, 0x22e1, 0xd359), BinaryEntry(32, 0xa357e227, 0x5fe6727e, 0x8d5f889e), BinaryEntry(64, 0xa509c49e8b47b441, 0xdb8f28381c99fa5f, 0x168f68834a13893d),
              BinaryEntry(8, 0x7c, 0xf0, 0x7c), BinaryEntry(16, 0x783a, 0x174f, 0xf074), BinaryEntry(32, 0xcffa1c3c, 0xe617e931, 0x0e1e67fd), BinaryEntry(64, 0xe014ad2538b45cd4, 0x45f4a77fae42cf9b, 0x168b9a9c0295a4a7),
              BinaryEntry(8, 0xeb, 0x3e, 0xaf), BinaryEntry(16, 0xbc1d, 0x5a2f, 0x783b), BinaryEntry(32, 0xeaac6515, 0x081b10ed, 0x28af5563), BinaryEntry(64, 0x7f38f034a90096f3, 0xf77effd95e509ded, 0x81a54804b79bf9c7),
              BinaryEntry(8, 0xb8, 0x64, 0x8b), BinaryEntry(16, 0x95f0, 0xa8ad, 0xaf84), BinaryEntry(32, 0xe7da54f1, 0x50d64c1b, 0xfb4a9e3c), BinaryEntry(64, 0x32565a1679361aeb, 0x45531bf4f7d83d89, 0x75992b2d0b3c9b0d),
              BinaryEntry(8, 0x67, 0x35, 0x3b), BinaryEntry(16, 0x85f4, 0xfee8, 0xf485), BinaryEntry(32, 0xb14d004b, 0x72177746, 0x2ec53401), BinaryEntry(64, 0x7a6d5da9fa663963, 0xbcf569753c6a8768, 0xa9fa6639637a6d5d),
              BinaryEntry(8, 0x2e, 0x0f, 0x5c), BinaryEntry(16, 0x905f, 0x68db, 0x0bf2), BinaryEntry(32, 0x75c5939b, 0x288253da, 0x7164e6dd), BinaryEntry(64, 0x5e90160e2533ce12, 0x6a7483e49581e3d8, 0x33ce125e90160e25),
              BinaryEntry(8, 0x3f, 0x43, 0xe7), BinaryEntry(16, 0xb177, 0x2f8e, 0xc5de), BinaryEntry(32, 0x7264df88, 0xe40e4d04, 0x87264df8), BinaryEntry(64, 0xc8fab790634be52c, 0xc238f0c83bba89f9, 0x7d5bc831a5f29664),
              BinaryEntry(8, 0x79, 0x0c, 0x97), BinaryEntry(16, 0x262c, 0x46b9, 0x1613), BinaryEntry(32, 0x8d751692, 0xe06fd325, 0x946ba8b4), BinaryEntry(64, 0x142986818ec6c940, 0x1aa9db8b17ca55e9, 0x40c76364a00a14c3),
            }
          },
          /* bvsdiv synthesis */
          {
            triton::ast::BVSDIV_NODE, {
              BinaryEntry(8, 0xd8, 0x01, 0xd8), BinaryEntry(16, 0x5747, 0x0001, 0x5747), BinaryEntry(32, 0x46777f14, 0x00000001, 0x46777f14), BinaryEntry(64, 0xfe17019d9e1c49ff, 0x0000000000000001, 0xfe17019d9e1c49ff),
              BinaryEntry(8, 0x17, 0x02, 0x0b), BinaryEntry(16, 0xad3c, 0x0002, 0xd69e), BinaryEntry(32, 0x05d03cc5, 0x00000002, 0x02e81e62), BinaryEntry(64, 0xc033c6d707e4d2d8, 0x0000000000000002, 0xe019e36b83f2696c),
              BinaryEntry(8, 0xb3, 0x04, 0xed), BinaryEntry(16, 0x337d, 0x0004, 0x0cdf), BinaryEntry(32, 0x1b4e2976, 0x00000004, 0x06d38a5d), BinaryEntry(64, 0x50ed242891bf7414, 0x0000000000000004, 0x143b490a246fdd05),
              BinaryEntry(8, 0x8e, 0x08, 0xf2), BinaryEntry(16, 0x21fe, 0x0008, 0x043f), BinaryEntry(32, 0xdfeb0388, 0x00000008, 0xfbfd6071), BinaryEntry(64, 0xdf7b6572e1f657b6, 0x0000000000000008, 0xfbef6cae5c3ecaf7),
              BinaryEntry(8, 0x15, 0x10, 0x01), BinaryEntry(16, 0x318a, 0x0010, 0x0318), BinaryEntry(32, 0xe87a0a7d, 0x00000010, 0xfe87a0a8), BinaryEntry(64, 0xe4c477c010dea2b6, 0x0000000000000010, 0xfe4c477c010dea2c),
              BinaryEntry(8, 0x81, 0x20, 0xfd), BinaryEntry(16, 0x0f8e, 0x0020, 0x007c), BinaryEntry(32, 0x72fb784d, 0x00000020, 0x0397dbc2), BinaryEntry(64, 0x9211647d63ac6245, 0x0000000000000020, 0xfc908b23eb1d6313),
              BinaryEntry(8, 0x6b, 0x40, 0x01), BinaryEntry(16, 0x6cbc, 0x0040, 0x01b2), BinaryEntry(32, 0xb459e5df, 0x00000040, 0xfed16798), BinaryEntry(64, 0xe390a1f1569e862f, 0x0000000000000040, 0xff8e4287c55a7a19),
              BinaryEntry(8, 0xcc, 0x01, 0xcc), BinaryEntry(16, 0xe62a, 0x0080, 0xffcd), BinaryEntry(32, 0x680c41fc, 0x00000080, 0x00d01883), BinaryEntry(64, 0x37a8c4d713046aa3, 0x0000000000000080, 0x006f5189ae2608d5),
              BinaryEntry(8, 0x7a, 0x02, 0x3d), BinaryEntry(16, 0x017c, 0x0100, 0x0001), BinaryEntry(32, 0xff8c832e, 0x00000100, 0xffff8c84), BinaryEntry(64, 0x568b049560be2287, 0x0000000000000100, 0x00568b049560be22),
              BinaryEntry(8, 0xf3, 0x04, 0xfd), BinaryEntry(16, 0x475b, 0x0200, 0x0023), BinaryEntry(32, 0x3fab4cb8, 0x00000200, 0x001fd5a6), BinaryEntry(64, 0x462ef4ee422aa042, 0x0000000000000200, 0x0023177a77211550),
            }
          },
          /* bvsmod synthesis */
          {
            triton::ast::BVSMOD_NODE, {
              BinaryEntry(8, 0xac, 0x72, 0x1e), BinaryEntry(16, 0xbb9d, 0xbc2f, 0xff6e), BinaryEntry(32, 0xea116f35, 0x3e858c53, 0x2896fb88), BinaryEntry(64, 0xc3c2fe790413c2ae, 0x7ed3cdb688a76db1, 0x4296cc2f8cbb305f),
              BinaryEntry(8, 0xb7, 0xda, 0xdd), BinaryEntry(16, 0x4ea3, 0xbdba, 0xca17), BinaryEntry(32, 0xde972172, 0xe4a23cee, 0xf9f4e484), BinaryEntry(64, 0x630eca4993410f3b, 0x65fc800f2fc802c1, 0x630eca4993410f3b),
              BinaryEntry(8, 0x54, 0x88, 0xdc), BinaryEntry(16, 0x8f93, 0x12f3, 0x0145), BinaryEntry(32, 0x456c7b00, 0x3c29060f, 0x094374f1), BinaryEntry(64, 0xe6fb134c6fb47e85, 0x199a2edf5b09c88c, 0x0095422bcabe4711),
              BinaryEntry(8, 0x56, 0x66, 0x56), BinaryEntry(16, 0xc682, 0x6f5d, 0x35df), BinaryEntry(32, 0x6b42eae5, 0x2789b27e, 0x1c2f85e9), BinaryEntry(64, 0xf4ea1335001225aa, 0x14f2f028ce262435, 0x09dd035dce3849df),
              BinaryEntry(8, 0x7f, 0x10, 0x0f), BinaryEntry(16, 0x5107, 0xb129, 0xb359), BinaryEntry(32, 0x96d6cdb5, 0xea4022cd, 0xedd64281), BinaryEntry(64, 0xcdb53a194460d851, 0x0da5740ad179a7ad, 0x044b0a448a477705),
              BinaryEntry(8, 0xfa, 0xb8, 0xfa), BinaryEntry(16, 0x7f71, 0xf0ba, 0xf5fb), BinaryEntry(32, 0x271e13a2, 0xafaf695e, 0xd6cd7d00), BinaryEntry(64, 0x3ca8db238f7d4f9a, 0xfbf2a9e3b39e53f1, 0xffe0cf7b15c43ab9),
              BinaryEntry(8, 0x0e, 0xfd, 0xff), BinaryEntry(16, 0x43db, 0xa1ef, 0xe5ca), BinaryEntry(32, 0x3d1daa66, 0xcf634bdb, 0xdbe4421c), BinaryEntry(64, 0x47d32a3d420c7231, 0x2c10544901c27c84, 0x1bc2d5f44049f5ad),
              BinaryEntry(8, 0xb7, 0x44, 0x3f), BinaryEntry(16, 0x383a, 0xe57b, 0xe8ab), BinaryEntry(32, 0xe008b7a1, 0xd5900802, 0xe008b7a1), BinaryEntry(64, 0x9f22647164ce6cf0, 0x1151567117f0c757, 0x070a6b17f47318fa),
              BinaryEntry(8, 0x96, 0xe6, 0xfe), BinaryEntry(16, 0xa57d, 0x81b5, 0xa57d), BinaryEntry(32, 0xbd2d2111, 0x9cfe6f3d, 0xbd2d2111), BinaryEntry(64, 0x80fa5f0264ad9bed, 0xe58c3d25f0a18503, 0xeac96a6aa22787e1),
              BinaryEntry(8, 0x10, 0x6a, 0x10), BinaryEntry(16, 0x362b, 0x7ac8, 0x362b), BinaryEntry(32, 0xe4103987, 0xd5c77119, 0xe4103987), BinaryEntry(64, 0x25d4f6587dc9524e, 0x08870faf49d4e6be, 0x03b8b79b5675b756),
            }
          },
          /* bvsrem synthesis */
          {
            triton::ast::BVSREM_NODE, {
              BinaryEntry(8, 0x59, 0xa9, 0x02), BinaryEntry(16, 0xbf0b, 0xf62e, 0xf9f7), BinaryEntry(32, 0x5bb42f8a, 0xd45f818c, 0x047332a2), BinaryEntry(64, 0xc765db09a3665e24, 0xf7a516e6126fb9e6, 0xf98751a534c802c0),
              BinaryEntry(8, 0x12, 0x16, 0x12), BinaryEntry(16, 0xccd0, 0x31d3, 0xfea3), BinaryEntry(32, 0x11290ca3, 0x310379f6, 0x11290ca3), BinaryEntry(64, 0xd5ffbb578e1bf42c, 0x943fbddf148b6003, 0xd5ffbb578e1bf42c),
              BinaryEntry(8, 0x9b, 0x58, 0xf3), BinaryEntry(16, 0x102d, 0x165f, 0x102d), BinaryEntry(32, 0x1c7ba0ff, 0xfaf6bd01, 0x034d5204), BinaryEntry(64, 0x253549b26bf1a97a, 0x2b4027571772af79, 0x253549b26bf1a97a),
              BinaryEntry(8, 0xb0, 0x2d, 0xdd), BinaryEntry(16, 0x25ee, 0x123e, 0x0172), BinaryEntry(32, 0xdb2f6682, 0xd95e2a73, 0xdb2f6682), BinaryEntry(64, 0xa602a81dbefa2941, 0xd9f80a35638d01f6, 0xf21293b2f7e02555),
              BinaryEntry(8, 0xa9, 0xd5, 0xff), BinaryEntry(16, 0x9c31, 0xced4, 0xfe89), BinaryEntry(32, 0x03301b60, 0xf631d05d, 0x03301b60), BinaryEntry(64, 0x80ff4bb5594c04a0, 0x2ea269b5712922b8, 0xde441f203b9e4a10),
              BinaryEntry(8, 0x87, 0x84, 0x87), BinaryEntry(16, 0x1608, 0xeebe, 0x04c6), BinaryEntry(32, 0x2b1d5827, 0xfad21cd0, 0x01ae3ea7), BinaryEntry(64, 0x2d19d418594efc6f, 0xfa8378fb7255f3b6, 0x01359bf3ebfe9a1f),
              BinaryEntry(8, 0xf2, 0xd1, 0xf2), BinaryEntry(16, 0x9392, 0x28a5, 0xe4dc), BinaryEntry(32, 0xd90a01f5, 0x6e95f49b, 0xd90a01f5), BinaryEntry(64, 0x9072cd86d104515c, 0xdec3a2f86662a6a9, 0xf427e49d9ddc5d61),
              BinaryEntry(8, 0x02, 0xf9, 0x02), BinaryEntry(16, 0x1fc9, 0x6036, 0x1fc9), BinaryEntry(32, 0xc40da616, 0x3792bb7a, 0xfba06190), BinaryEntry(64, 0x3f0ed987c72db747, 0x05c56e7f28337e50, 0x05588890352ac827),
              BinaryEntry(8, 0x78, 0xef, 0x01), BinaryEntry(16, 0x7290, 0x9b3a, 0x0dca), BinaryEntry(32, 0xe2a2bdb9, 0x5144f034, 0xe2a2bdb9), BinaryEntry(64, 0xcdf25524307a93de, 0x27e4b886fad709e5, 0xf5d70dab2b519dc3),
              BinaryEntry(8, 0xa3, 0xf1, 0xfd), BinaryEntry(16, 0x84ae, 0x2f5a, 0xe362), BinaryEntry(32, 0x6fa3564c, 0xe037d9b2, 0x104ae362), BinaryEntry(64, 0x06dde445d9fdc5ea, 0x02aa4f6cc9b7ae28, 0x0189456c468e699a),
            }
          },
          /* bvsub synthesis */
          {
            triton::ast::BVSUB_NODE, {
              BinaryEntry(8, 0xab, 0x0d, 0x9e), BinaryEntry(16, 0x3e04, 0xfa06, 0x43fe), BinaryEntry(32, 0x9e311a8b, 0xfb870346, 0xa2aa1745), BinaryEntry(64, 0x1098061e49e0a3f8, 0xcee8b5272b2b2c00, 0x41af50f71eb577f8),
              BinaryEntry(8, 0x38, 0x50, 0xe8), BinaryEntry(16, 0x865b, 0x1356, 0x7305), BinaryEntry(32, 0x4ad3fde4, 0xd46b181f, 0x7668e5c5), BinaryEntry(64, 0x5079105c0dedd5c3, 0xb93cd4f0977dde2b, 0x973c3b6b766ff798),
              BinaryEntry(8, 0xaf, 0x60, 0x4f), BinaryEntry(16, 0xec28, 0x04a2, 0xe786), BinaryEntry(32, 0x3a250637, 0x4fb84592, 0xea6cc0a5), BinaryEntry(64, 0xfc2206514781af56, 0x374a72919ac91f4a, 0xc4d793bfacb8900c),
              BinaryEntry(8, 0x66, 0xce, 0x98), BinaryEntry(16, 0x072c, 0x78bf, 0x8e6d), BinaryEntry(32, 0x48df8ed9, 0x5b983f29, 0xed474fb0), BinaryEntry(64, 0xc0c7d7e485c99896, 0x3af2ad393470d6e3, 0x85d52aab5158c1b3),
              BinaryEntry(8, 0xf6, 0x89, 0x6d), BinaryEntry(16, 0x4f41, 0x3416, 0x1b2b), BinaryEntry(32, 0x80a7ab88, 0x2d9a2422, 0x530d8766), BinaryEntry(64, 0xa46a75820c6fb0fc, 0x8fcceef94230b1d5, 0x149d8688ca3eff27),
              BinaryEntry(8, 0xde, 0x0e, 0xd0), BinaryEntry(16, 0x8c17, 0xe2f8, 0xa91f), BinaryEntry(32, 0x8ece98ae, 0x5a67d7f8, 0x3466c0b6), BinaryEntry(64, 0xa99a835805979a4a, 0xe2a1b2b2e39a663b, 0xc6f8d0a521fd340f),
              BinaryEntry(8, 0x75, 0x9b, 0xda), BinaryEntry(16, 0x372a, 0x61f7, 0xd533), BinaryEntry(32, 0xe2a32226, 0xb09115b8, 0x32120c6e), BinaryEntry(64, 0xebe48760d3b25fe9, 0xb8a3a059bb4e56f5, 0x3340e707186408f4),
              BinaryEntry(8, 0x84, 0x2a, 0x5a), BinaryEntry(16, 0xae2a, 0x46b0, 0x677a), BinaryEntry(32, 0xb61e116b, 0xfe947e9a, 0xb78992d1), BinaryEntry(64, 0xd08768a5df3b07dd, 0x3344e82e7c8fb3c8, 0x9d42807762ab5415),
              BinaryEntry(8, 0x4a, 0xe1, 0x69), BinaryEntry(16, 0xc6f0, 0x1b8a, 0xab66), BinaryEntry(32, 0x432c147a, 0x23648d2b, 0x1fc7874f), BinaryEntry(64, 0x7a60cd9ece8b510f, 0x3908cb24ab994d8d, 0x4158027a22f20382),
              BinaryEntry(8, 0xee, 0x15, 0xd9), BinaryEntry(16, 0x7e69, 0x3aee, 0x437b), BinaryEntry(32, 0xff52c7a3, 0xc23e22d4, 0x3d14a4cf), BinaryEntry(64, 0x7a63a41f13c831a8, 0xc98f17d5ee703184, 0xb0d48c4925580024),
            }
          },
          /* bvudiv synthesis */
          {
            triton::ast::BVUDIV_NODE, {
              BinaryEntry(8, 0x5d, 0x01, 0x5d), BinaryEntry(16, 0xada8, 0x0001, 0xada8), BinaryEntry(32, 0xaf76da01, 0x00000001, 0xaf76da01), BinaryEntry(64, 0x8da3672293da95a0, 0x0000000000000001, 0x8da3672293da95a0),
              BinaryEntry(8, 0x3d, 0x02, 0x1e), BinaryEntry(16, 0x4d03, 0x0002, 0x2681), BinaryEntry(32, 0xda9d67d9, 0x00000002, 0x6d4eb3ec), BinaryEntry(64, 0x048405db82440ba2, 0x0000000000000002, 0x024202edc12205d1),
              BinaryEntry(8, 0x38, 0x04, 0x0e), BinaryEntry(16, 0xb60a, 0x0004, 0x2d82), BinaryEntry(32, 0x5620383c, 0x00000004, 0x15880e0f), BinaryEntry(64, 0x0dd9306942e45b97, 0x0000000000000004, 0x03764c1a50b916e5),
              BinaryEntry(8, 0x41, 0x08, 0x08), BinaryEntry(16, 0x9c1c, 0x0008, 0x1383), BinaryEntry(32, 0x2c8319e9, 0x00000008, 0x0590633d), BinaryEntry(64, 0x08bedaccbc6c75be, 0x0000000000000008, 0x0117db59978d8eb7),
              BinaryEntry(8, 0x1d, 0x10, 0x01), BinaryEntry(16, 0x0f91, 0x0010, 0x00f9), BinaryEntry(32, 0x311762fe, 0x00000010, 0x0311762f), BinaryEntry(64, 0xfe15b2306b926366, 0x0000000000000010, 0x0fe15b2306b92636),
              BinaryEntry(8, 0x80, 0x20, 0x04), BinaryEntry(16, 0x0418, 0x0020, 0x0020), BinaryEntry(32, 0x7ab70791, 0x00000020, 0x03d5b83c), BinaryEntry(64, 0x3cc553fd58555cf3, 0x0000000000000020, 0x01e62a9feac2aae7),
              BinaryEntry(8, 0xc8, 0x40, 0x03), BinaryEntry(16, 0x4ef5, 0x0040, 0x013b), BinaryEntry(32, 0x3ab85989, 0x00000040, 0x00eae166), BinaryEntry(64, 0x1d330a710e65643c, 0x0000000000000040, 0x0074cc29c4399590),
              BinaryEntry(8, 0xf2, 0x01, 0xf2), BinaryEntry(16, 0x3681, 0x0080, 0x006d), BinaryEntry(32, 0xcad8118c, 0x00000080, 0x0195b023), BinaryEntry(64, 0x3d2524d98d53e09b, 0x0000000000000080, 0x007a4a49b31aa7c1),
              BinaryEntry(8, 0xe0, 0x02, 0x70), BinaryEntry(16, 0xb5ea, 0x0100, 0x00b5), BinaryEntry(32, 0xec422548, 0x00000100, 0x00ec4225), BinaryEntry(64, 0x2205dd33c11ec30e, 0x0000000000000100, 0x002205dd33c11ec3),
              BinaryEntry(8, 0xea, 0x04, 0x3a), BinaryEntry(16, 0x94bd, 0x0200, 0x004a), BinaryEntry(32, 0x4356da7b, 0x00000200, 0x0021ab6d), BinaryEntry(64, 0x83f2c987f12ef36c, 0x0000000000000200, 0x0041f964c3f89779),
            }
          },
          /* bvurem synthesis */
          {
            triton::ast::BVUREM_NODE, {
              BinaryEntry(8, 0x95, 0xaa, 0x95), BinaryEntry(16, 0xc09e, 0xd941, 0xc09e), BinaryEntry(32, 0x1b8d5434, 0x78a4c013, 0x1b8d5434), BinaryEntry(64, 0xbe704f49a47019e6, 0x1c1d426adfa831b1, 0x15c0c0c8667eefc0),
              BinaryEntry(8, 0x30, 0x93, 0x30), BinaryEntry(16, 0x230d, 0x1662, 0x0cab), BinaryEntry(32, 0xfec61cce, 0x7d000ea3, 0x04c5ff88), BinaryEntry(64, 0xe8a6cb521eb42e18, 0x214f0c2dbbc2abfc, 0x20cc823fb8242630),
              BinaryEntry(8, 0x02, 0xb0, 0x02), BinaryEntry(16, 0x51c4, 0x6e79, 0x51c4), BinaryEntry(32, 0xf31d575a, 0xb7b132b7, 0x3b6c24a3), BinaryEntry(64, 0xc75e76a4b3a70416, 0xe6c459b52980e9c1, 0xc75e76a4b3a70416),
              BinaryEntry(8, 0x73, 0x39, 0x01), BinaryEntry(16, 0x7861, 0x1cf1, 0x049d), BinaryEntry(32, 0x14d6ed03, 0x006c8d49, 0x000fe20a), BinaryEntry(64, 0x75e945cfb796c4ad, 0x40a33eca981f8438, 0x354607051f774075),
              BinaryEntry(8, 0xb1, 0x97, 0x1a), BinaryEntry(16, 0x21f2, 0xbb1f, 0x21f2), BinaryEntry(32, 0x7c6e3d14, 0x134b106e, 0x08abda80), BinaryEntry(64, 0x50329b8e71789098, 0x9af7139d6c4be4cf, 0x50329b8e71789098),
              BinaryEntry(8, 0xa2, 0xbb, 0xa2), BinaryEntry(16, 0x845e, 0xfe90, 0x845e), BinaryEntry(32, 0xb23485c7, 0xc8a83eed, 0xb23485c7), BinaryEntry(64, 0xbfa61e5a1ce78fe2, 0x12d5fb32749bd119, 0x034a4e618ed164e8),
              BinaryEntry(8, 0xf5, 0x67, 0x27), BinaryEntry(16, 0x844a, 0x6bfc, 0x184e), BinaryEntry(32, 0x1f23f1af, 0x412a4c65, 0x1f23f1af), BinaryEntry(64, 0xf803d16c59ee4a08, 0xec88733070c5db4d, 0x0b7b5e3be9286ebb),
              BinaryEntry(8, 0x51, 0x63, 0x51), BinaryEntry(16, 0x607d, 0x2b5f, 0x09bf), BinaryEntry(32, 0x4954eb58, 0x13c65b32, 0x0e01d9c2), BinaryEntry(64, 0xfd6fe042414fd618, 0x42da760428805d43, 0x34e07e35c7cebe4f),
              BinaryEntry(8, 0x96, 0x6c, 0x2a), BinaryEntry(16, 0x170a, 0x853f, 0x170a), BinaryEntry(32, 0x4efd0ae6, 0x76563c35, 0x4efd0ae6), BinaryEntry(64, 0xf18c4e717cdb5876, 0x083821d70c364514, 0x033079151ab58532),
              BinaryEntry(8, 0x97, 0xeb, 0x97), BinaryEntry(16, 0x95d0, 0xdd9d, 0x95d0), BinaryEntry(32, 0x95cb48a9, 0x1223ca81, 0x04acf4a1), BinaryEntry(64, 0xb274df8664c3dfd4, 0x2f91986927f05735, 0x23c0164aecf2da35),
            }
          },
          /* bvxnor synthesis */
          {
            triton::ast::BVXNOR_NODE, {
              BinaryEntry(8, 0x07, 0xdd, 0x25), BinaryEntry(16, 0xa1ec, 0x7f21, 0x2132), BinaryEntry(32, 0x05601358, 0x837bda03, 0x79e436a4), BinaryEntry(64, 0x8af45257cf2a0ce7, 0xc456ab65a00733f8, 0xb15d06cd90d2c0e0),
              BinaryEntry(8, 0x59, 0x63, 0xc5), BinaryEntry(16, 0xe113, 0x55cf, 0x4b23), BinaryEntry(32, 0x21a1e372, 0xbc6d2148, 0x62333dc5), BinaryEntry(64, 0xe573378bfad38fd9, 0xd00d15aa94e76296, 0xca81ddde91cb12b0),
              BinaryEntry(8, 0x25, 0x27, 0xfd), BinaryEntry(16, 0xebb7, 0xaa49, 0xbe01), BinaryEntry(32, 0x0b553cbd, 0x08f8f650, 0xfc523512), BinaryEntry(64, 0x8db777183f1a913d, 0x978ed9b8c892ddcd, 0xe5c6515f0877b30f),
              BinaryEntry(8, 0xd3, 0x19, 0x35), BinaryEntry(16, 0x12ac, 0x8455, 0x6906), BinaryEntry(32, 0xa4d836c7, 0x57c0ff70, 0x0ce73648), BinaryEntry(64, 0x9aa04c0e19377b1c, 0x1c3e3f066300abde, 0x79618cf785c82f3d),
              BinaryEntry(8, 0xb0, 0xe7, 0xa8), BinaryEntry(16, 0xb57c, 0x28c1, 0x6242), BinaryEntry(32, 0x522be1c5, 0x9727aaab, 0x3af3b491), BinaryEntry(64, 0x3933ce62876faa3c, 0xec833f6b3169744b, 0x2a4f0ef649f92188),
              BinaryEntry(8, 0xc6, 0x0b, 0x32), BinaryEntry(16, 0xfdf0, 0x484a, 0x4a45), BinaryEntry(32, 0x6f7425e1, 0xb0c9cb35, 0x2042112b), BinaryEntry(64, 0x0ec13d3603e6a8ad, 0x9f03df60189f4764, 0x6e3d1da9e4861036),
              BinaryEntry(8, 0x23, 0x78, 0xa4), BinaryEntry(16, 0xbc7e, 0xdf08, 0x9c89), BinaryEntry(32, 0x77f1731a, 0xfb8b2f6a, 0x7385a38f), BinaryEntry(64, 0xcd997c6f6798450a, 0xb19f9bf4762606f0, 0x83f91864ee41bc05),
              BinaryEntry(8, 0xc7, 0x12, 0x2a), BinaryEntry(16, 0x2ffb, 0x0191, 0xd195), BinaryEntry(32, 0xce6d7b89, 0x60f2f340, 0x51607736), BinaryEntry(64, 0x6e9aa65f8dd34b4c, 0x7da5a0964e4fe1db, 0xecc0f9363c635568),
              BinaryEntry(8, 0x6f, 0xca, 0x5a), BinaryEntry(16, 0x4acb, 0x91f3, 0x24c7), BinaryEntry(32, 0x991863ad, 0xbf47e4c7, 0xd9a07895), BinaryEntry(64, 0x8775921f83ac7480, 0xa8bd34b595e7651f, 0xd0375955e9b4ee60),
              BinaryEntry(8, 0x80, 0x87, 0xf8), BinaryEntry(16, 0xcac5, 0x687a, 0x5d40), BinaryEntry(32, 0xc79d31f9, 0xab52ff2c, 0x9330312a), BinaryEntry(64, 0xedef4939098835f1, 0x90c6de16bd4128e9, 0x82d668d04b36e2e7),
            }
          },
          /* bvxor synthesis */
          {
            triton::ast::BVXOR_NODE, {
              BinaryEntry(8, 0x62, 0x33, 0x51), BinaryEntry(16, 0xe886, 0xb487, 0x5c01), BinaryEntry(32, 0x8db56e47, 0xe6db1f16, 0x6b6e7151), BinaryEntry(64, 0xb445ff9ed877fba2, 0x1b0f35f5d4ff8309, 0xaf4aca6b0c8878ab),
              BinaryEntry(8, 0x8c, 0x18, 0x94), BinaryEntry(16, 0x1581, 0x48b1, 0x5d30), BinaryEntry(32, 0xc2314683, 0x7d952884, 0xbfa46e07), BinaryEntry(64, 0xca344e6c2ce05406, 0x1da7c5bb9c479c61, 0xd7938bd7b0a7c867),
              BinaryEntry(8, 0x28, 0xfc, 0xd4), BinaryEntry(16, 0xe08d, 0x2629, 0xc6a4), BinaryEntry(32, 0x4d49b521, 0xb4f82452, 0xf9b19173), BinaryEntry(64, 0x836cfdce083ec840, 0xe4c05531b5bb3fd9, 0x67aca8ffbd85f799),
              BinaryEntry(8, 0xd4, 0x7d, 0xa9), BinaryEntry(16, 0x0262, 0x428a, 0x40e8), BinaryEntry(32, 0x66e796f1, 0x5a5875e1, 0x3cbfe310), BinaryEntry(64, 0x19df757ef6bd5eca, 0x89cfa8de22e52a28, 0x9010dda0d45874e2),
              BinaryEntry(8, 0x21, 0xe1, 0xc0), BinaryEntry(16, 0xcda0, 0x484e, 0x85ee), BinaryEntry(32, 0x9de59d4a, 0x3d522cb9, 0xa0b7b1f3), BinaryEntry(64, 0xa7e66415b3009893, 0x1106ecd4169c6d38, 0xb6e088c1a59cf5ab),
              BinaryEntry(8, 0xda, 0xbd, 0x67), BinaryEntry(16, 0x26c3, 0xa09f, 0x865c), BinaryEntry(32, 0x40aed338, 0xe1ac878e, 0xa10254b6), BinaryEntry(64, 0x49e46348edd4a9e8, 0x720ee4f551dc8ba1, 0x3bea87bdbc082249),
              BinaryEntry(8, 0xbc, 0xfc, 0x40), BinaryEntry(16, 0x28f6, 0x448e, 0x6c78), BinaryEntry(32, 0x1b5fa7d5, 0xa418aabf, 0xbf470d6a), BinaryEntry(64, 0x37157f43f42847f2, 0x907f4bf711843442, 0xa76a34b4e5ac73b0),
              BinaryEntry(8, 0x71, 0xc7, 0xb6), BinaryEntry(16, 0xe588, 0xeab9, 0x0f31), BinaryEntry(32, 0x40a3c544, 0x47c2ecce, 0x0761298a), BinaryEntry(64, 0xb8af526f544d959e, 0xfc74f1f52e46539b, 0x44dba39a7a0bc605),
              BinaryEntry(8, 0x73, 0x6c, 0x1f), BinaryEntry(16, 0x7b2c, 0x7e6b, 0x0547), BinaryEntry(32, 0xae998b82, 0xaa3531b3, 0x04acba31), BinaryEntry(64, 0xbdc34828860b1540, 0x93b7ac38f4dae21d, 0x2e74e41072d1f75d),
              BinaryEntry(8, 0x92, 0x73, 0xe1), BinaryEntry(16, 0xd8ad, 0x588d, 0x8020), BinaryEntry(32, 0xdbd7bcb8, 0x77464840, 0xac91f4f8), BinaryEntry(64, 0x16b093609bf704a6, 0xa67d16782e7bb079, 0xb0cd8518b58cb4df),
            }
          },
        };

      }; /* oracles namespace */
    }; /* synthesis namespace */
  }; /* engines namespace */
}; /* triton namespace */