❌

Normal view

There are new articles available, click to refresh the page.
Before yesterdaysecret club

Improving MBA Deobfuscation using Equality Saturation

8 August 2022 at 23:00

This blog post will first give a brief overview of obfuscation based on Mixed-Boolean-Arithmetic (MBA), how it has historically been attacked and what are the known limitations. The main focus will then shift to an extension of the oracle-based synthesis approach, detailing how combining program synthesis with the equality saturation technique produces significantly more simplification opportunities. Finally, a set of examples spanning from different MBA categories over unsolved limitations up to future work ideas will hopefully serve as food for thoughts to the reader. Across the post, references to existing research are provided to delve into additional details and deepen the understanding of the topics.

Mixed-Boolean-Arithmetic Obfuscation

Mixed-Boolean-Arithmetic Obfuscation is a technique which represents an expression to be concealed in a semantically equivalent, but syntactically more complex form. For example, the expression x + y, can be rewritten as (x ^ y) + 2 * (x & y), effectively making its behaviour harder to comprehend.

Commonly, such MBAs can be found in advanced malware samples and real-world DRM systems, belonging to the strongest-known code obfuscation techniques. However, in recent years, various attacks have been developed; the next section will provide a brief overview of their strengths and limitations.

Common Attacks and Shortcomings

Several attacks have been published since the release of the original papers on Mixed-Boolean-Arithmetic Obfuscation 1, 2. While initial tools, like SSPAM, simplified MBAs via pattern matching, more sophisticated approaches rely on algebraic simplifications, machine learning or program synthesis. As of late, some methods also cleverly abuse intrinsic properties of certain sub-classes of MBAs.

Algebraic Attacks

Arybo makes use of the bit-blasting technique to convert a word-level expression into a bit-level representation—where each bit of the output is independently computed—and proceeds with applying boolean algebraic simplifications to obtain a shrinked version of the input expression. While extremely powerful, the idea falls short when the bit-blasting step has to handle big symbolic multiplications. Another issue is related to the fact that a human analyst may expect an easier-to-read word-level expression as output, while this may not be the case when processing instruction sequences with non-trivial semantics.

Worth mentioning are the ad-hoc algebraic attacks on the permutation polynomial MBA expressions devised by Ninon Eyrolles 3 and Biondi et al. 4. While attractive, the scope of both approaches is limited to the deobfuscation of a constant and is strongly dependent on the MBA generation process.

Stochastic Program Synthesis

Approaches like Stoke, Syntia and its extension Xyntia are based on methods which are known as stochastic program synthesis: They handle the expression simplification as a stochastic optimization problem. Their idea is to represent the obfuscated program as a vector of I/O pairs and learn an expression which has the same I/O behaviour. To achieve this, these approaches use a grammar to generate and mutate small expressions and combine this with a cost function which guides the search towards expressions with the same behaviour.

While stochastic synthesis works well to simplify semantically easy expressions, it has a hard time in finding more complex ones. Since these approaches also cannot simplify sub-expressions in an MBA, they are not successful in some of the semantically more complex cases that can be found in the wild.

Synthesis-based Expression Simplification

As a consequence, new methods have been introduced which re-use some program synthesis concepts, while also being able to simplify partial expressions. These methods can be described as synthesis-based expression simplification and have been introduced by Robin David et al. as QSynthesis. The open source projects QSynthesis and msynth are representatives of this technique.

Once a symbolic execution of the MBA is performed, the techniques represent the MBA as an abstract syntax tree (AST). Then, using a precomputed database (so-called oracle) which maps I/O behaviours to expressions, a divide-and-conquer strategy is adopted: The I/O behaviour of each sub-expression is evaluated and, when possible, sub-expressions are replaced by shorter representations from the database.

These approaches are the most generic to date. However, processing a unique representation of the MBA expression, they often miss synthesis opportunities that would otherwise lead to better results. A common example are sub-expressions that, if combined, would cancel out, but are too far away in the AST to be discovered by the technique.

Drill&Join

Drill&Join is a lesser known approach which strives to achieve exact inductive program synthesis of Boolean expressions. It has been repurposed by Biondi et al. to weaken opaque predicates protected via MBA obfuscation.

As with Arybo, the attack is particularly suitable if the expression needs to be processed by an SMT solver; however, also in this case, a bit-level output may not be appealing to a human analyst. Another major limitation mentioned in the paper is related to the improper support for expressions behaving as a point function (e.g. mathematical functions that show a certain behaviour for exactly one specific input).

MBA-Blast

MBA-Blast, and soon after MBA-Solver, provided the community with the first fully algebraic attack abusing properties of the main theorem to build linear MBA expressions. The authors devised a process to normalize the input MBA expression and are able to shrink them via basic algebraic simplifications.

The approach, while in its infancy, proved how reusing knowledge of the problem can be extremely effective; extensions to it are to be expected. The major limitation is to be found in the lack of support of expressions that cannot be trivially converted from word-level to bit-level, such as non-linear or polynomial MBAs.

Souper

Souper is a synthesizing superoptimizer for LLVM-IR that provides an implementation of exhaustive synthesis and CounterExample-Guided Inductive Synthesis (CEGIS). Worth noting are the attempts to synthesize big constants either via harvesting from the original expression or employing the CEGIS component to materialize them. Its current major limitation is the scalability on semantically complex instruction sequences.

NeuReduce

NeuReduce is a string-to-string method based on neural networks to automatically learn and reduce complex MBA expressions. A strong limitation of the approach is its inability to generalize to MBA expressions which are built using rewriting rules not part of the training set. In real-world scenarios, the used rewriting rules would also be hard to collect.

QSynthesis Limitations and Improvements

In the remaining parts of this post, we’ll delve into known QSynthesis limitations and explore ways to tackle them. We will especially take advantage of the fact that, having full access to the AST of the expression, enables the combination of information coming from both the syntactical and semantical worlds. Hence, the expression to simplify is assumed to be available to the attacker in the form of an assembly or intermediate representation.

QSynthesis Example

The following images, adapted from the original publication, exemplify the step-by-step exploration and synthesis procedure used by QSynthesis. Even though the updated version presented at Black Hat 2021 provides an improved exploration strategy, the main simplification steps are the same and their understanding is fundamental to grasp further extensions.

In the offline phase of the attack, the so-called oracle is computed using a grammar with simple constants, symbolic variables and n-ary operations:

  1. A set of M concrete values associated to the symbolic variables is randomly generated;
  2. Expressions of increasing complexity are obtained from the grammar, their I/O behaviour is calculated and the output vector, of size N, is mapped to an hash;
  3. Each hash and expression tuple is saved in the oracle, preserving the smallest expression in case a collision is found (e.g. the expressions A, A & A, A | A are equivalent).

The explanation of the online phase of the attack, assuming the availability of the precomputed oracle, follows. Furthermore, a top-down bottom-up placeholder-based exploration strategy is assumed to be driving the identification of the synthesizable sub-expressions.

In the next image, the sub-tree highlighted in red is deemed synthesizable by the oracle and associated to the smaller expression (A + B). An intermediate variable (V1) is created and substituted in the AST in place of all the sub-trees identical to the one that just got synthesized.

QSynthesis 0

In the left image, the now updated AST—with the placeholder nodes highlighted in blue—turns also out to be synthesizable, matching the behaviour of the smaller expression (A ^ V1). Once again, an intermediate variable (V2) is created and replaced in the AST. The right image shows the updated AST, which cannot be simplified any further.

QSynthesis 1 QSynthesis 2

The following images represent the intermediate variables (V1, V2) generated after a successful sub-tree synthesis and their simplified expansions, highlighted in green.

QSynthesis 3 QSynthesis 4

Starting from the fully updated AST—just containing the V2 node—we can expand the intermediate variables in reverse order, obtaining the fully synthesized AST depicted below.

QSynthesis 5

The official publications explain the two phases in greater details, so we highly suggest checking them out to gather a better understanding of the idea.

Locality Issues

The reliance on a unique syntactical representation of the input expression raises some less documented—but nonetheless important—shortcomings, which are here referred to as locality issues. For example, when an expression contains a large chain of additions, it may happen that the AST exploration algorithm completely misses valid synthesis opportunities, as some useful nodes are too far apart in the tree. Unluckily, the problem is not limited to addition chains; in fact, all operations with commutativity and associativity properties are affected.

This limitation becomes more apparent when handling MBAs where the terms replaced by more complex linear combinations are interleaved with each other or when a polynomial encoding is involved, scattering related nodes all over the obfuscated expression.

For example, consider the AST of the following expression (5*(A ^ B)) + (A & B), where the red/blue nodes represent the left/right addition operands.

AST 0

After applying the rewriting rules (x^y) = (~x|y)+(x&~y)-~(x^y) and (x&y) = (x|y)-(~x&y)-(x&~y), we obtain the following updated AST, which is easily handled by QSynthesis. In fact, the strictly related sub-trees—of the same colour—are locally next to each other, readily synthesizable by the oracle. The red/blue nodes now represent the obfuscated left/right addition operands, while the white nodes represent a chain of additions.

AST 1

Shuffling the terms which are part of the chain of additions, we reduce the synthesis opportunities, hindering the QSynthesis exploration algorithm to produce the best solution; in the end, we obtain only a partial simplification. This is due to the fact that now the strictly related sub-trees are not in local vicinity anymore.

AST 2

Constants Support

The original publication ignored the problem of synthesizing constants altogether and the idea of deriving them with an SMT solver was deemed too time consuming. However, the updated version mentions how some concrete values can be obtained preprocessing the expression with SymPy or by inserting simple constants during the oracle generation process.

The current open-source implementation details the possibility to synthesize nodes yielding a single constant; even though, the authors do not elaborate any further on the improvements due to the inclusion of concrete values in the database.

Attacks Combination

Some of the attacks mentioned in the previous chapter are orthogonal to QSynthesis, meaning that existing research can be successfully combined without loss of generality:

  • MBA-Blast can be used to simplify linear sub-expressions before proceeding with the oracle-based synthesis, enabling better support to non-linear or polynomial MBAs;
  • CEGIS can be used to synthesize sub-expressions that do not match the precomputed oracle and may possibly contain constants.

Before describing how another technique from the program analysis world, namely Equality Saturation, paves the way to even more powerful attacks, we demonstrate what a combined approach for constant synthesis may look like.

Templated Constants Synthesis

What follows is an attempt at combining oracle-based synthesis and CEGIS to increase the chance of simplifying a sub-expression involving constants.

As previously mentioned, Souper relies on CEGIS to infer valid concrete values: It generates a templated query containing symbolic placeholders where the constants should fit and proceeds with asking for a solution to the SMT solver. Therefore, we need to obtain the same template using our only source of information: the observed I/O behaviour. The idea has been divided in an offline phase, taking place just once, and an online phase, taking place every time a sub-expression does not match the main oracle.

Offline phase:

  1. An ad-hoc oracle of size 8 bits, involving three variables and two constants in the range [0-255] is computed;
  2. Expressions evaluating to the same oracle key are filtered to remove semantical duplicates and added to the same bucket;
  3. The constants in the entries are replaced by symbolic placeholders and remaining duplicates are removed;
  4. The entries in each bucket, now referred to as templates, are saved in ascending size order.

Online phase:

  1. The I/O behavior of the sub-expression is truncated to 8 bits to compute a new oracle key used to query the ad-hoc oracle;
  2. If a match is found, the list of templates in the bucket is iterated and used to query the SMT solver attempting to derive full bitwidth constants;
  3. In case of success, the symbolic placeholder(s) in the candidate template are replaced by the constant(s) and the node is considered to be synthesized.

The high-level idea is to drive a full bitwidth sub-expression synthesis with truncated bitwidth behaviours. As expected, limitations arise when the behaviours are not representative enough, leading to the iteration of hundred of possibly invalid templates.

A New Ingredient: Equality Saturation

Equality saturation is an optimization technique proposed by Tate et al. in 2009, and it relies on the e-graph data structure designed by Gregory Nelson in his PhD thesis in 1980. Recently, Willsey et al. released an improved equality saturation implementation called egg, whose resources have been used as a base for this proof of concept.

Historically, it has been used as a first-class synthesis technique, enabling improvements in projects involving: 3D CAD programs, floating point or algebra expressions. In this post, we will see how also MBA expressions can be dramatically simplified, if we combine equality saturation with oracle-based synthesis.

Building Blocks

From an implementation perspective, an e-graph is a data structure used to represent a congruence relation over a set of expressions. It is made of equivalence classes (e-classes), which, in turn, contain equivalent nodes (e-nodes). Some similarities can be found between an AST node and an e-node; in fact, each e-node represents an operator or a value. However, its children, when present, are references to e-classes and not to other e-nodes. Each e-node is unique; if some sub-expressions of an AST are identical, they will end up being the same e-node. This guarantees a compact and efficient representation.

The following image depicts a simple e-graph populated with the expression (A * B) + (A * C).

Step 0

  • The circles (e0 to e5) represent the e-classes, which, in the initial state of the e-graph, have a unique edge connected to the single e-node part of an equivalence class. Additional edges from e-classes to e-nodes will be added once new equalities are discovered.
  • The rectangles (ADD, MUL, A, B, C) represent the e-nodes, which can be divided in values (A, B, C) and operators (ADD, MUL). Each child of an operator is connected to an e-class by an edge.
  • The A value, appearing twice in the expression, has been converted into a single e-node part of a single e-class (e1), following the aforementioned compact representation.
  • The e5 e-class can referred to as the head of the e-graph, effectively representing the topmost node in the expression’s AST.

An in-depth explanation about the inner workings of equality saturation and the e-graph structure can be found in the egg’s official documentation.

Why Do We Need Equality Saturation?

At this point, the careful reader may have guessed that the main goal, for MBA deobfuscation, would be for us to have the possibility to explore a large number—potentially hundred of thousands—of equivalent representations of the input expression and be able to locate the one best suiting the oracle-based synthesis attack. Thankfully, an e-graph will let us represent a huge number of semantical equivalence relations between syntactically different expressions.

Equality saturation can add information to an e-graph using a technique called term-rewriting. The process consists in syntactically matching parts of an expression and transforming them into equivalent ones. This is usually achieved in two steps: the matching and rewriting phase. The matching phase, that uses pattern matching to identify sub-expressions for which equivalent representations are known; the rewriting phase, that generates new representations for the matched sub-expressions.

Unluckily, term-rewriting is by design a destructive technique, as any information about the original expression is lost as soon as the rewrite to the new expression is done. This raises issues if multiple rewrites are possible for the same matched sub-expression, as only one of those must be selected to proceed. Projects like SSPAM or LLVM’s peephole optimizer rely on heuristics to find the best rewriting candidate, minimizing some cost function. However, this opens the door to another problem, known as phase-ordering; this problem deals with the question of what happens when applying some rewrites in different orders. Given the rewriting rules R0 and R1, it could be that applying R0 before R1 leads to a worse result compared to applying R1 before R0; there’s no easy way to solve the problem (in fact, this problem is NP-complete).

The ideal solution would be able to apply all possible rewrites at the same time, preserving the intermediate equivalent representations of the starting expression and deciding at the end which candidate is the best. No need to look any further, as this is exactly what equality saturation does.

Cost Computation and Candidate Extraction

The last part of the equality saturation process consists in the cost computation and extraction of the best representation of the input expression. As for the stochastic synthesis, the cost computation plays an important role in driving the selection of the useful candidate sub-expressions. Depending on the goal, the cost function could be prioritizing the selection of smaller or faster nodes, even though—for the rest of the post—the logic will be to select the smallest AST nodes, basically optimizing towards shorter expressions. Once the costs have been computed, the extraction phase visits the needed e-classes in the e-graph, selecting the best possible representation of the input expression.

As a bonus, computing the cost after each iteration gives visibility on the quality of the process; if the e-graph grows at a too fast pace, computing the costs offers an opportunity to extract the best candidate expression and start a new equality saturation from scratch. This is usually referred to as a full e-graph reset.

Equality Saturation Example

The images below represent a step-by-step equality saturation execution applied to the expression (B + A) - B, in an attempt to simplify it. A and B are names given to complex sub-expressions that cannot be synthesized. The following rewriting rules are being applied at each iteration:

  • (x + (-x)) => 0
  • (x + y) => (y + x)
  • (x - y) => (x + (-y))
  • (x + (y + z)) => ((x + y) + z)

This is the state of the e-graph right after the insertion of the expression to process.

Step 0

These are intermediate states of the e-graph where all the rules have been applied against the e-nodes present in the previous state of the e-graph, leading to the addition of new equalities. On the left image we can observe how the e-class e2 is representing the equivalence between the expressions (B + A) and (A + B), thanks to the second rule, and how the e-class e6 is representing the equivalence between the expressions (B + A) - B, (A + B) - B, (B + A) + (-B) and (A + B) + (-B), thanks to the combination of the second and third rules. On the right image we can instead observe how the e6 e-class turned into the e7 e-class with the addition of the equivalent representations (-B) + (B + A) and (-B) + (A + B), again thanks to the second rule.

Step 1 Step 2

This can be considered the final state of the e-graph, even though it isn’t fully saturated (no more rewrites are possible), as it provides enough knowledge for the program synthesis to be fully effective on the input expression.

Step 3

In the final step, the e-classes and e-nodes which are part of the simplified expression (0 + A) are highlighted. As expected, an e-class (e8) represents the knowledge that ((-B) + B) is equivalent to 0.

QSynthesis Extension

In the upcoming paragraphs, we take advantage of the equality saturation properties to overcome the MBA deobfuscation limitations highlighted in the previous section. First, we focus on increasing the synthesis opportunities. After attempting to extend the support to the constants synthesis, we finally repurpose the runtime information to enhance the saturation loop.

Expression Morphing

As learned thus far, the input expression may not be in the most amenable form to guarantee good synthesis opportunities; therefore, it is important to find a way to morph it accordingly and make sure its semantical correctness is preserved.

Relying on equality saturation, the expression can be inserted in an e-graph and transformed to obtain an increasing amount of syntactically different but semantically equivalent representations, with the hope that at least one of them will be more synthesizable than it originally was. The good news is that, given an e-graph preserves all the intermediate information, at any given time the best possible candidate expression can be extracted from the e-graph, meaning that, employing this approach, the obtainable result is never going to be worse compared to avoiding it.

Given the nature of an MBA expression is strongly related to the properties of the involved arithmetic (add, sub, mul, neg) and logical (and, or, xor, not) operations, the minimal set of selected rewriting rules are commutativity, associativity and distributivity. To these, a set of equality and normalization rules have been added (e.g. rewriting neg into not, pushing not to the leaves of the expression). The list of rewriting rules currently employed by the proof of concept can be found in the Appendix.

The following example shows how the application of three rewriting rules (commutativity, associativity and not normalization) turns an expression which cannot be synthesized by an oracle using two variables into one which can be synthesized.

Simplified with a two variables oracle and using three rules
python3 synth.py
eclasses #: 11
Input (cost = 16): (~(((x+y)+(~(((x+y)+x)+y)))+(-z)))
====================================================================================================
eclasses #: 16
Synthesized (cost = 5): ((x+y)+z)
====================================================================================================

Constants Harvesting

Constant synthesis is a well known hard problem, although, using the aforementioned rewriting rules, a set of constants not originally present in the obfuscated expression starts appearing in the e-graph. Obviously, some are generated through the simple negation rules, but others are obtained with the repeated application of a non-trivial combination of rewriting rules that, moving some sub-expressions next to each other, lead to new synthesis opportunities.

As expected, this positive side effect turned out to be insufficient in most cases, so a further attempt to use the new information to improve the synthesis at runtime has been done. After each matching phase, the e-graph is updated with the discovered equalities, making it possible to identify all the e-classes of unit cost representing a constant. At this point the constants can be used to compute a smaller ad-hoc runtime oracle, available from the next synthesis iteration.

During the experiments the runtime oracle has been built with a single operation involving one variable and one constant. Assuming K harvested constants, an oracle with N binary operations and M input samples, K×N×M output samples need to be computed to obtain K×N new oracle entries. The oracle computation time is usually negligible, as the amount of harvested constants is contained compared to the total amount of possible constants in the bitwidth of the input expression.

The following examples show the same obfuscated expression simplified using different options. First, using CEGIS with the support of the constants oracle, which leads to the solution in one iteration. Then, via constants harvesting using the runtime oracle, taking five iterations. Finally, with the default rewriting rules, that in nine iterations lead to a simplified version of the original expression, but not to the best possible representation. Depending on the expression under analysis, the CEGIS option may be overkill and too slow, while standard rewriting rules or constants harvesting could be the right choice.

Simplified via constants oracle (CEGIS)
python3 synth.py --use-constants-oracle
eclasses #: 84
Input (cost = 1979): ((((((((((((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c))-((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x1)))+((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c)))*0x67)+0xd)*0x2d)+(((((((((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c))-((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x1)))+((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c)))*0x67)+0xd)*(-0x52))|0x22)*(-0x1b)))+(-0x3e))-(-0x9))*(-0x13))&(-0x1))
====================================================================================================
eclasses #: 163
Synthesized (cost = 3): (x^0x5c)
====================================================================================================
Simplified via runtime oracle (harvesting)
python3 synth.py --use-constants-harvest
eclasses #: 84
Input (cost = 1979): ((((((((((((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c))-((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x1)))+((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c)))*0x67)+0xd)*0x2d)+(((((((((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c))-((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x1)))+((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c)))*0x67)+0xd)*(-0x52))|0x22)*(-0x1b)))+(-0x3e))-(-0x9))*(-0x13))&(-0x1))
====================================================================================================
eclasses #: 132
Synthesized (cost = 473): ((((((((((((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e)&0x94)-((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e))+(((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e)&0x94))*0x67)+0xd)*0x2d)+((((((((((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e)&0x94)-((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e))+(((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e)&0x94))*0x67)+0xd)*0xae)|0x22)*0xe5))+0xc2)-0xf7)*0xed)
====================================================================================================
eclasses #: 257
Synthesized (cost = 51): ((((((((((((x^0x26)&0x94)*0x67)*0xae)+(-(x^0x26)))*0x67)+0xd)*0x2d)+((((((((((x^0x26)&0x94)*0x67)*0xae)+(-(x^0x26)))*0x67)+0xd)*0xae)|0x22)*0xe5))+0xc2)-0xf7)*0xed)
====================================================================================================
eclasses #: 687
Synthesized (cost = 5): ((x^0x26)^0x7a)
====================================================================================================
eclasses #: 3473
Synthesized (cost = 5): ((x^0x26)^0x7a)
====================================================================================================
eclasses #: 50943
Synthesized (cost = 3): (0x5c^x)
e-graph reset done.
====================================================================================================
Simplified via default term rewriting
python3 synth.py
eclasses #: 84
Input (cost = 1979): ((((((((((((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c))-((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x1)))+((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c)))*0x67)+0xd)*0x2d)+(((((((((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c))-((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x1)))+((((((((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x3a)+(-0x51))&(-0xc))+(((((((((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*0x56)+0x24)&0x46)*0x4b)+(((((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))+(((-((((((x*(-0x1b))+(-0x9))*(-0x13))+(-0x2a))+(((((x*(-0x1b))+(-0x9))*0x26)+0x55)&(-0x2)))*0x2))+(-0x1))&(-0x2)))*0x3)+0x4d)*(-0x19)))+0x76)*0x63))+0x2e)&(-0x6c)))*0x67)+0xd)*(-0x52))|0x22)*(-0x1b)))+(-0x3e))-(-0x9))*(-0x13))&(-0x1))
====================================================================================================
eclasses #: 132
Synthesized (cost = 473): ((((((((((((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e)&0x94)-((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e))+(((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e)&0x94))*0x67)+0xd)*0x2d)+((((((((((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e)&0x94)-((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e))+(((((((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x3a)+0xaf)&0xf4)+((((((x+x)&0x46)*0x4b)+(((((((x+0xab)+0xd6)+((~x)+(~x)))+(x+x))*0x3)+0x4d)*0xe7))+0x76)*0x63))+0x2e)&0x94))*0x67)+0xd)*0xae)|0x22)*0xe5))+0xc2)-0xf7)*0xed)
====================================================================================================
eclasses #: 252
Synthesized (cost = 219): (((((((((((((((((((((x+x)&0x46)*0x4b)*0x3a)+((0x2*(~(-x)))+0xde))+0xbc)+0xaf)&0xf4)+((((x+x)&0x46)+(((((0x7f+x)*0x3)+0x4d)*0xe7)*0x63))+0xa2))+0x2e)&0x94)*0x67)*0xae)+(-((((((((((x+x)&0x46)*0x4b)*0x3a)+((0x2*(~(-x)))+0xde))+0xbc)+0xaf)&0xf4)+((((x+x)&0x46)+(((((0x7f+x)*0x3)+0x4d)*0xe7)*0x63))+0xa2))+0x2e)))*0x67)+0xd)*0x2d)+(((((((((((((((((((x+x)&0x46)*0x4b)*0x3a)+((0x2*(~(-x)))+0xde))+0xbc)+0xaf)&0xf4)+((((x+x)&0x46)+(((((0x7f+x)*0x3)+0x4d)*0xe7)*0x63))+0xa2))+0x2e)&0x94)*0x67)*0xae)+(-((((((((((x+x)&0x46)*0x4b)*0x3a)+((0x2*(~(-x)))+0xde))+0xbc)+0xaf)&0xf4)+((((x+x)&0x46)+(((((0x7f+x)*0x3)+0x4d)*0xe7)*0x63))+0xa2))+0x2e)))*0x67)+0xd)*0xae)|0x22)*0xe5))+0xc2)-0xf7)*0xed)
====================================================================================================
eclasses #: 650
Synthesized (cost = 181): ((((0xb+(0x1b*((0x2*((((((((0xf1+(0xb5*(0x7f+x)))+(((x+x)&0x46)*0x4b))*0x3a)+0xaf)&0xf4)+(((0xf1+(0xb5*(0x7f+x)))*0x63)+((x+x)&0x46)))+0x2e)&0x94))+(0xd2-((((((0xf1+(0xb5*(0x7f+x)))+(((x+x)&0x46)*0x4b))*0x3a)+0xaf)&0xf4)+(((0xf1+(0xb5*(0x7f+x)))*0x63)+((x+x)&0x46)))))))*0xed)+(((0x2*((0x2*((((((((0xf1+(0xb5*(0x7f+x)))+(((x+x)&0x46)*0x4b))*0x3a)+0xaf)&0xf4)+(((0xf1+(0xb5*(0x7f+x)))*0x63)+((x+x)&0x46)))+0x2e)&0x94))+(0xd2-((((((0xf1+(0xb5*(0x7f+x)))+(((x+x)&0x46)*0x4b))*0x3a)+0xaf)&0xf4)+(((0xf1+(0xb5*(0x7f+x)))*0x63)+((x+x)&0x46))))))+0xd6)|0x22))+0x55)
====================================================================================================
eclasses #: 3256
Synthesized (cost = 14): (((((x+x)&0x46)+(~(x+0xed)))+0x1)+0x49)
====================================================================================================
eclasses #: 48747
Synthesized (cost = 11): ((((x+x)&0x46)+(0x80-x))+0xdc)
e-graph reset done.
====================================================================================================
eclasses #: 17
Synthesized (cost = 11): ((((x+x)&0x46)+(0x80-x))+0xdc)
====================================================================================================
eclasses #: 28
Synthesized (cost = 11): ((((x+x)&0x46)+(0x80-x))+0xdc)
====================================================================================================
eclasses #: 51
Synthesized (cost = 10): ((0x5c+(-x))+((x+x)&0x46))
====================================================================================================
eclasses #: 87
Synthesized (cost = 9): ((0x5c+((x+x)&0x46))-x)
====================================================================================================

Incremental Learning

Investigating the idea of reducing the amount of wasted information led to a concept resembling an incremental learning technique. In fact, during the synthesis phase, new knowledge is normally generated and discarded, while we could instead put it to good use. This new information can be divided into:

  • Coming from a sub-expression that can be synthesized, namely: the computed oracle key, the processed e-class and its simplified representation;
  • Coming from a sub-expression that cannot be synthesized, namely: the computed oracle key, that turned out to be missing from the oracle, and the processed e-class.

Both cases provide valuable knowledge that can be inserted into the e-graph, incrementally improving the results:

  • In the former case, the synthesized representation of the node can be inserted into the e-graph, obtaining a new e-class to be merged with the original e-class. This will provide the e-graph with the best representation for that e-class and additional e-nodes to be e-matched, potentially leading to more synthesis opportunities;
  • In the latter case, all the e-classes that resulted into the computation of the same oracle key can be merged into a single e-class, reducing the total amount of e-classes and enforcing a best representation to be used during the extraction phase.

The following example shows how repurposing the runtime information leads to a smaller result with fewer e-classes in less iterations.

With incremental learning
python3 synth.py
eclasses #: 18
Input (cost = 29): (((((((x&y)*0x3)-(x|y))-(~(x|y)))-(((~x)&y)*0x2))-(~y))-(x|(~y)))
====================================================================================================
eclasses #: 23
Synthesized (cost = 29): (((((((x&y)*0x3)-(x|y))-(~(x|y)))-(((~x)&y)*0x2))-(~y))-(x|(~y)))
====================================================================================================
eclasses #: 27
Synthesized (cost = 29): (((((((x&y)*0x3)-(x|y))-(~(x|y)))-(((~x)&y)*0x2))-(~y))-(x|(~y)))
====================================================================================================
eclasses #: 48
Synthesized (cost = 20): (((-((~x)+(x^y)))+(((x&y)*0x3)+0x1))-(x|(~y)))
====================================================================================================
eclasses #: 108
Synthesized (cost = 18): (((-(((~x)&y)-0x1))+(((x&y)*0x3)+0x1))-(~y))
====================================================================================================
eclasses #: 294
Synthesized (cost = 13): ((((x&y)+0x2)+((x&y)*0x3))+0x1)
====================================================================================================
eclasses #: 947
Synthesized (cost = 11): (((x&y)+0x3)+((x&y)*0x3))
====================================================================================================
eclasses #: 5786
Synthesized (cost = 7): ((0x4*(x&y))+0x3)
====================================================================================================
Without incremental learning
python3 synth.py
eclasses #: 18
Input (cost = 29): (((((((x&y)*0x3)-(x|y))-(~(x|y)))-(((~x)&y)*0x2))-(~y))-(x|(~y)))
====================================================================================================
eclasses #: 23
Synthesized (cost = 29): (((((((x&y)*0x3)-(x|y))-(~(x|y)))-(((~x)&y)*0x2))-(~y))-(x|(~y)))
====================================================================================================
eclasses #: 30
Synthesized (cost = 29): (((((((x&y)*0x3)-(x|y))-(~(x|y)))-(((~x)&y)*0x2))-(~y))-(x|(~y)))
====================================================================================================
eclasses #: 50
Synthesized (cost = 20): (((-((~x)+(x^y)))+(0x1+((x&y)*0x3)))-(x|(~y)))
====================================================================================================
eclasses #: 112
Synthesized (cost = 18): (((-((~x)+(x|y)))+(0x1+((x&y)*0x3)))-(~y))
====================================================================================================
eclasses #: 364
Synthesized (cost = 15): (((-(~(x&y)))+(0x1+((x&y)*0x3)))+0x1)
====================================================================================================
eclasses #: 1354
Synthesized (cost = 13): (((x&y)+(0x2+((x&y)*0x3)))+0x1)
====================================================================================================
eclasses #: 6358
Synthesized (cost = 11): ((x&y)+(0x3+((x&y)*0x3)))
====================================================================================================

Expression Preprocessing

There are cases in which preprocessing the input expression may increase the probability of achieving good synthesis results. In the proof of concept, two preprocessing steps have been included: First, a simplified implementation of MBA-Blast to shrink and normalize linear sub-expressions; then, a pass which converts multiplications by a small constant into sequences of additions, increasing the chance for the associativity rewriting to match synthesizable sub-expressions.

MBA-Blast Normalization

The open-source implementation of MBA-Blast currently does not not handle the processing of linear sub-expressions in non-linear or polynomial input forms. Further, it also does not implement the common sub-expression elimination idea proposed in the original publication. In our proof of concept, the input expression is turned into an AST with detection of common sub-expressions, enabling a transparent handling of the linear parts of a non-linear or polynomial input and attempting a layered elimination of common terms.

The base selection plays an important role in how effective the algebraic simplifications will be and if the layered elimination will be possible at all. In fact, it is currently unknown if there is an optimal way to pick the base given the expression’s properties. Therefore three default basis are provided: TINY (small terms preferred), HUGE (variables and-ed together) and HARD (hardcoded handpicked base).

Multiplication Explosion

This preprocessing step is an attempt to increase the amount of commutativity and associativity rewriting opportunities, hoping for some of those to cancel out sub-terms or turn them into synthesizable nodes. The explosion is currently being limited to small multiplicative constants. Usually this is fine, as the selected coefficients for in-the-wild MBA expressions are small, even though nothing would exclude the artificial usage of big coefficients, ruling this step out altogether.

Evaluation

The following tests showcase linear, non-linear and polynomial MBA expressions obtained from NeuReduce, MBA-Obfuscator, QSynthesis and own implementations of the first (rewriting) and third (encoding) theorems from the original Zhou et al. publications. Additionally, the selected expressions are only partially handled by the standard QSynthesis implementation.

Linear MBA with one 8 bits variable and one 8 bits constant
python3 synth.py --use-constants-harvest
eclasses #: 10
Input (cost = 13): (((x|0x10)-((~x)&0x10))-(x&(-0x11)))
====================================================================================================
eclasses #: 14
Synthesized (cost = 5): (x-(x&0xef))
====================================================================================================
eclasses #: 22
Synthesized (cost = 3): (x&0x10)
====================================================================================================
Linear MBA with five 8 bits variables
python3 synth.py
eclasses #: 47
Input (cost = 75): ((((((((((((-((x^y)*0x4))-((~y)|(~z)))+(((~x)|(~y))*0x4))-((x|((~y)&z))*0x5))+(((~x)&(y|z))*0x3))+(x*0x7))-((((~x)|y)|z)*0x2))-((x^y)|(~z)))+(a&(~b)))-(~(a|b)))+((~a)|b))+0x2)
====================================================================================================
eclasses #: 64
Synthesized (cost = 24): (((a-((~((-(y^z))-(x&(y^z))))-(a^b)))+((~a)|b))+0x2)
====================================================================================================
eclasses #: 93
Synthesized (cost = 24): (((a-((~((-(y^z))-(x&(y^z))))-(a^b)))+((~a)|b))+0x2)
====================================================================================================
eclasses #: 175
Synthesized (cost = 19): (((0xff+((-(y^z))-(x&(y^z))))-(~(a|b)))+0x2)
====================================================================================================
eclasses #: 501
Synthesized (cost = 16): ((((a|b)-(y^z))+(-(x&(y^z))))+0x2)
====================================================================================================
Non-Linear MBA with four 8 bits variables
python3 synth.py --use-mba-blast-before --mba-blast-logic=2
Original: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((-((((z&(x^y))&(~w))|((x|(y|z))&w))*-0xfa))-((((z^(x|(y|z)))&(~w))|(((x&(~y))|(y^z))&w))*0x1))+(((((~(x^y))&(~(x^z)))&(~w))|(((x&z)^(~(x^(y&z))))&w))*0x7))+((((~(y&(~z)))&(~w))|((~(x^((~y)&z)))&w))*0x1))+((x&(y&(z&w)))*0x7))+((x&(y&((~z)&w)))*0x8))+((x&((~y)&((~z)&w)))*0x8))+(((~x)&(y&(z&w)))*0x5))-(((~x)&(y&((~z)&w)))*0x1))-(((~x)&((~y)&((~z)&w)))*0x8))-((~(x|(y|(z|w))))*0x8))-((~(x|(y|((~z)|w))))*0x1))+((~(x|((~y)|(z|w))))*0x1))+((~(x|((~y)|((~z)|w))))*0x5))+((~((~x)|(y|(z|w))))*0x1))+((~((~x)|(y|((~z)|w))))*0x6))+((~((~x)|((~y)|(z|w))))*0x2))-((~((~x)|((~y)|((~z)|w))))*0x7))&y)^(~(((((((((((((((((((-((((z&(x^y))&(~w))|((x|(y|z))&w))*-0xfa))-((((z^(x|(y|z)))&(~w))|(((x&(~y))|(y^z))&w))*0x1))+(((((~(x^y))&(~(x^z)))&(~w))|(((x&z)^(~(x^(y&z))))&w))*0x7))+((((~(y&(~z)))&(~w))|((~(x^((~y)&z)))&w))*0x1))+((x&(y&(z&w)))*0x7))+((x&(y&((~z)&w)))*0x8))+((x&((~y)&((~z)&w)))*0x8))+(((~x)&(y&(z&w)))*0x5))-(((~x)&(y&((~z)&w)))*0x1))-(((~x)&((~y)&((~z)&w)))*0x8))-((~(x|(y|(z|w))))*0x8))-((~(x|(y|((~z)|w))))*0x1))+((~(x|((~y)|(z|w))))*0x1))+((~(x|((~y)|((~z)|w))))*0x5))+((~((~x)|(y|(z|w))))*0x1))+((~((~x)|(y|((~z)|w))))*0x6))+((~((~x)|((~y)|(z|w))))*0x2))-((~((~x)|((~y)|((~z)|w))))*0x7))^((~y)|z))))&(~w))|((z^(~(((((((((((((((((((-((((z&(x^y))&(~w))|((x|(y|z))&w))*-0xfa))-((((z^(x|(y|z)))&(~w))|(((x&(~y))|(y^z))&w))*0x1))+(((((~(x^y))&(~(x^z)))&(~w))|(((x&z)^(~(x^(y&z))))&w))*0x7))+((((~(y&(~z)))&(~w))|((~(x^((~y)&z)))&w))*0x1))+((x&(y&(z&w)))*0x7))+((x&(y&((~z)&w)))*0x8))+((x&((~y)&((~z)&w)))*0x8))+(((~x)&(y&(z&w)))*0x5))-(((~x)&(y&((~z)&w)))*0x1))-(((~x)&((~y)&((~z)&w)))*0x8))-((~(x|(y|(z|w))))*0x8))-((~(x|(y|((~z)|w))))*0x1))+((~(x|((~y)|(z|w))))*0x1))+((~(x|((~y)|((~z)|w))))*0x5))+((~((~x)|(y|(z|w))))*0x1))+((~((~x)|(y|((~z)|w))))*0x6))+((~((~x)|((~y)|(z|w))))*0x2))-((~((~x)|((~y)|((~z)|w))))*0x7))|(y&z))))&w))*0x3)+((((y^(~(x&(y&z))))&(~w))|(((x|y)&(~(x^(y^z))))&w))*0x1))-((((y^(~(x&(y&z))))&(~w))|((~(y^z))&w))*0x1))+((((z^(~(x&((~y)|z))))&(~w))|((x&(~z))&w))*0x1))-(((((x&y)|(~(y|z)))&(~w))|(((x&y)|(~(x^(y^z))))&w))*0x3))+((((z&(~(x&y)))&(~w))|((x&y)&w))*0x4))-(((((~(x^y))&(~(x^z)))&(~w))|(((x|y)&(x^(y^z)))&w))*0x1))+((((z^(~(x&((~y)&z))))&(~w))|((y^(x&((~y)|z)))&w))*0x2))-((((x&((~y)|z))&(~w))|(((x&(~y))|(~(y^z)))&w))*0xb))-(((((~(x|y))|(~(x^(y^z))))&(~w))|((~((~x)&(y^z)))&w))*0xb))+(((((x&y)|(y^z))&(~w))|((~(x^((~y)&z)))&w))*0x1))-(((((x&(~y))|(~(y^z)))&(~w))|(((x&z)^(~(x^(y&z))))&w))*0x3))+(((((~(x^y))&(~(x^z)))&(~w))|(((x&z)|(y&(~z)))&w))*0x5))-((((y^(x|(y^z)))&(~w))|(((~(x^y))|(x^z))&w))*0x1))+((((z^(~(x|((~y)&z))))&(~w))|((y^(x|((~y)|z)))&w))*0x2))+((((y|(~(x|(~z))))&(~w))|(((~x)|(y^z))&w))*0xb))-(((((x&(~y))|(y^z))&(~w))|((y&(~(x&(~z))))&w))*0x1))-(((((~(x&y))&(~(x^(y^z))))&(~w))|((z^(x|((~y)&z)))&w))*0x5))+((((y^(~(x&((~y)&z))))&(~w))|((z^(x|y))&w))*0x7))-(((((y&(~z))^((~x)|(y^z)))&(~w))|(((~y)&(~(x^z)))&w))*0x6))+((((z^(x&(~y)))&(~w))|((z^(x&y))&w))*0x1))+((((x|(~z))&(~w))|((x^(y|z))&w))*0x5))+((((~(x&(y|z)))&(~w))|((z&(~(x&y)))&w))*0x1))+((((y^(~((~x)&(y^z))))&(~w))|((y^(~(x&(~z))))&w))*0xb))+((((~(y&z))&(~w))|((x&(y^z))&w))*0x1))-(((((x&y)^(x^((~y)|z)))&(~w))|((x|((~y)|z))&w))*0x6))+(((((~(x&(~y)))&(y^z))&(~w))|((z^((~x)|(y|z)))&w))*0x1))+((((~(x&(~y)))&(~w))|((y^((~x)|(y^z)))&w))*0x1))+(((((~z)&(~(x^y)))&(~w))|((y^(~(x&(y&z))))&w))*0x5))-((((z^(x|(~y)))&(~w))|(((x&y)|(y^z))&w))*0x1))+(((((~y)&(x^z))&(~w))|((~(x|(~z)))&w))*0xb))-(((((~(x&y))&(x^(y^z)))&(~w))|(((x&y)^(y|(~z)))&w))*0x2))+((((y^(~(x|((~y)&z))))&(~w))|((z^(~(x&((~y)|z))))&w))*0x1))-(((((x&z)^(~(x^((~y)&z))))&(~w))|((~(y|z))&w))*0x2))-(((((x&y)|(~(y^z)))&(~w))|(((~y)&(~(x^z)))&w))*0x1))-((((~(x&(y^z)))&(~w))|((~(x&((~y)|z)))&w))*0x6))+((((x&y)&(~w))|(((~y)|(x^z))&w))*0x3))-(((((~x)|((~y)&z))&(~w))|(((~(x|y))|(y^z))&w))*0x7))+((((~(x|(y^z)))&(~w))|((x|(~z))&w))*0x1))-((((~(x|y))&(~w))|((z^(~((~x)&((~y)&z))))&w))*0x1))-((((z^(x|((~y)|z)))&(~w))|(((x|(~y))&(~(x^(y^z))))&w))*0x7))-((((x&(y|z))&(~w))|((z&(~(x&(~y))))&w))*0x3))+((((x^z)&(~w))|(((x&y)|(~(x^(y^z))))&w))*0x1))-((((~(y^z))&(~w))|(((y&z)^(~((~x)&(y^z))))&w))*0x1))+((((~(y|z))&(~w))|(((x^y)|(x^z))&w))*0x3))-((((x&(y|z))&(~w))|((y^(x|(y|z)))&w))*0x2))-(((((x|(~y))&(~(x^(y^z))))&(~w))|(((~(x|(~y)))|(~(y^z)))&w))*0x1))+((((x|(~z))&(~w))|((y^(x|((~y)|z)))&w))*0xb))+(((((~(x&(~y)))&(~(y^z)))&(~w))|((y^(~(x&(y&z))))&w))*0x2))+((((z^(~(x|y)))&(~w))|(((y&(~z))^((~x)|(y^z)))&w))*0x2))-((((~(x^y))&(~w))|(((~z)&(~(x^y)))&w))*0x6))-((((y^(~((~x)&(y|z))))&(~w))|((~(x|y))&w))*0x1))+((((x|(y&z))&(~w))|(((~(x&y))&(x^(y^z)))&w))*0x3))-((((z^(~((~x)&((~y)&z))))&(~w))|(((y&(~z))^(x|(y^z)))&w))*0xb))-((((z^(~(x|y)))&(~w))|((y^(x&(y|z)))&w))*0x7))+((((z|(~(x^y)))&(~w))|((z^((~x)|((~y)&z)))&w))*0x2))+(((((x|y)&(x^(y^z)))&(~w))|((z|(x&(~y)))&w))*0x1))+((((z&(~(x^y)))&(~w))|(((x&z)^(~(x^((~y)&z))))&w))*0x1))-(((((x&(~y))|(y^z))&(~w))|((~y)&w))*0x6))+((((y^(~(x|(y&z))))&(~w))|(((y&(~z))^((~x)|(y^z)))&w))*0x4))-((((~((~x)|((~y)|z)))&(~w))|((z&(x^y))&w))*0x5))-((((x^(y^z))&(~w))|((x&(~y))&w))*0x2))+(((((~(x|(~y)))|(~(x^(y^z))))&(~w))|(y&w))*0x2))-((((x|(y&z))&(~w))|((z^(~((~x)&((~y)|z))))&w))*0x1))-((((x&(~y))&(~w))|((z^(~(x|((~y)&z))))&w))*0x2))+((((z^(x&(y|z)))&(~w))|((z^((~x)|((~y)|z)))&w))*0x7))+(((((~x)|((~y)|z))&(~w))|((~(x|(y|z)))&w))*0x4))+((((y^(~(x|(y&z))))&(~w))|((~(x^((~y)&z)))&w))*0x2))+((((y^(~(x&(~z))))&(~w))|((y^((~x)&(y^z)))&w))*0x1))+((((z^(~(x&y)))&(~w))|(((x^y)|(x^z))&w))*0x1))+(((((x|(~y))&(x^(y^z)))&(~w))|((~(x&(~z)))&w))*0x5))-((((y^(x&((~y)|z)))&(~w))|((y^(x&((~y)|z)))&w))*0x2))+(((((x&y)^(~(x^(y&z))))&(~w))|((~(x&(~z)))&w))*0x1))-((((z&(x^y))&(~w))|(((x|y)&(y^z))&w))*0x3))-((((y|(~(x^z)))&(~w))|((~(x^((~y)|z)))&w))*0x2))-((((y^((~x)&(y|z)))&(~w))|(((~z)&(x^y))&w))*0x7))-((((~(x^(y&z)))&(~w))|((z|(~(x^y)))&w))*0x6))+(((((x&(~y))|(~(y^z)))&(~w))|((y^(~((~x)|((~y)&z))))&w))*0x1))+(((((~y)&(~(x^z)))&(~w))|((x&((~y)|z))&w))*0xb))-(((((y&z)^(~(x&(y^z))))&(~w))|(((~(x|y))|(y^z))&w))*0x1))+(((((x&z)|(y&(~z)))&(~w))|((z^((~x)&((~y)|z)))&w))*0x1))-((((~((~x)&((~y)|z)))&(~w))|(((~(x|y))|(~(y^z)))&w))*0x2))-((((y^((~x)|((~y)&z)))&(~w))|((~((~x)|((~y)|z)))&w))*0x1))+((~(x|(y|(z|w))))*0x8))-((~(x|((~y)|(z|w))))*0x7))-((~((~x)|(y|(z|w))))*0x7))+((~((~x)|((~y)|(z|w))))*0x7))+((~(x|(y|((~z)|w))))*0xd))+((~(x|((~y)|((~z)|w))))*0x15))+((~((~x)|(y|((~z)|w))))*0xa))+((~((~x)|((~y)|((~z)|w))))*0x6))+(((~x)&((~y)&((~z)&w)))*0xc))-(((~x)&(y&((~z)&w)))*0x1d))+((x&((~y)&((~z)&w)))*0xc))+((x&(y&((~z)&w)))*0xc))-(((~x)&((~y)&(z&w)))*0x20))+(((~x)&(y&(z&w)))*0xe))+((x&((~y)&(z&w)))*0xc))+((((((((((((((((((((-((((z&(x^y))&(~w))|((x|(y|z))&w))*-0xfa))-((((z^(x|(y|z)))&(~w))|(((x&(~y))|(y^z))&w))*0x1))+(((((~(x^y))&(~(x^z)))&(~w))|(((x&z)^(~(x^(y&z))))&w))*0x7))+((((~(y&(~z)))&(~w))|((~(x^((~y)&z)))&w))*0x1))+((x&(y&(z&w)))*0x7))+((x&(y&((~z)&w)))*0x8))+((x&((~y)&((~z)&w)))*0x8))+(((~x)&(y&(z&w)))*0x5))-(((~x)&(y&((~z)&w)))*0x1))-(((~x)&((~y)&((~z)&w)))*0x8))-((~(x|(y|(z|w))))*0x8))-((~(x|(y|((~z)|w))))*0x1))+((~(x|((~y)|(z|w))))*0x1))+((~(x|((~y)|((~z)|w))))*0x5))+((~((~x)|(y|(z|w))))*0x1))+((~((~x)|(y|((~z)|w))))*0x6))+((~((~x)|((~y)|(z|w))))*0x2))-((~((~x)|((~y)|((~z)|w))))*0x7))&(y&(z&w)))*0xf))
MBA-Blast: (((((((((((((((~w)&x)&y)&z)*0x4)+((((w&(~x))&y)&z)*0x4))+(((((~w)&(~x))&y)&z)*0x4))+(((w&x)&(~y))&z))+((((~w)&(~x))&(~y))&z))+(((w&x)&y)&(~z)))+(((((~w)&x)&y)&(~z))*0x4))+(((w&(~x))&y)&(~z)))+(((((~w)&(~x))&y)&(~z))*0x3))+(((w&(~x))&(~y))&(~z)))+((((~w)&(~x))&(~y))&(~z)))
eclasses #: 47
Input (cost = 120): (((((((((((((((~w)&x)&y)&z)*0x4)+((((w&(~x))&y)&z)*0x4))+(((((~w)&(~x))&y)&z)*0x4))+(((w&x)&(~y))&z))+((((~w)&(~x))&(~y))&z))+(((w&x)&y)&(~z)))+(((((~w)&x)&y)&(~z))*0x4))+(((w&(~x))&y)&(~z)))+(((((~w)&(~x))&y)&(~z))*0x3))+(((w&(~x))&(~y))&(~z)))+((((~w)&(~x))&(~y))&(~z)))
====================================================================================================
eclasses #: 52
Synthesized (cost = 113): (((((((((((((((~w)&x)&y)&z)*0x4)+((((w&(~x))&y)&z)*0x4))+((((~(w|x))&y)&z)*0x4))+(((w&x)&(~y))&z))+((~(w|(x|y)))&z))+(((w&x)&y)&(~z)))+(((((~w)&x)&y)&(~z))*0x4))+(((w&(~x))&y)&(~z)))+((((~(w|x))&y)&(~z))*0x3))+(((w&(~x))&(~y))&(~z)))+(~((w|x)|(y|z))))
====================================================================================================
eclasses #: 102
Synthesized (cost = 92): (((((((((~(w^x))&(z-(y&z)))+((0x4*((y&z)&(w^x)))+((((~(w|x))&y)&z)*0x4)))+(((w&x)&y)&(~z)))+(((((~w)&x)&y)&(~z))*0x4))+(((w&(~x))&y)&(~z)))+(((~(w|(x|z)))&y)*0x3))+(((~(x|y))&w)&(~z)))+(~((w|x)|(y|z))))
====================================================================================================
eclasses #: 194
Synthesized (cost = 79): (((((((((w&x)&(y^z))+(0x4*((z&y)-((w&x)&(z&y)))))+((~(w|(x|y)))&z))+((((~(w|z))&x)&y)*0x4))+(((~(x|z))&w)&y))+(((~(w|(x|z)))&y)*0x3))+((~(x|(y|z)))&w))+(~((w|x)|(y|z))))
====================================================================================================
eclasses #: 457
Synthesized (cost = 64): ((((~((w|x)|(y|z)))+((~((y|z)|x))&w))+((((~(w|(x|z)))&y)*0x3)+(((y&(~(w|z)))&x)*0x4)))+(((y^z)&((~w)^(x|y)))+(0x4*((z&y)-((w&x)&(z&y))))))
====================================================================================================
eclasses #: 1462
Synthesized (cost = 46): (((((~(x|y))^((y^z)&w))+(0x4*((z&y)-((w&x)&(z&y)))))+(((~(w|(x|z)))&y)*0x3))+(((y&(~(w|z)))&x)*0x4))
====================================================================================================
eclasses #: 2377
Synthesized (cost = 35): (((((~(w|(x|z)))&y)*0x3)+((~(x|y))^((y^z)&w)))+(0x4*((y&(x|z))-((w&x)&y))))
====================================================================================================
Non-Linear MBA with two 8 bits variables and one 8 bits constant
python3 synth.py
eclasses #: 30
Input (cost = 55): ((~(((-(~((~((-(((~((y^(y+(-0x2)))&0x1))^(--0xff))+(-y)))+0x48))&((~(((-(((~((y^(y+(-0x2)))&0x1))^(--0xff))+(-y)))+0x48)|0x2))^0x2))))+(-z))+(-0x2)))+(-0x1))
====================================================================================================
eclasses #: 39
Synthesized (cost = 22): ((~(((-(~((~(y+0x48))&((~((y+0x48)|0x2))^0x2))))-z)+(-0x2)))+(-0x1))
====================================================================================================
eclasses #: 70
Synthesized (cost = 21): ((~(((-((y+0x48)|(~((~((y+0x48)|0x2))^0x2))))-z)+0xfe))+0xff)
====================================================================================================
eclasses #: 137
Synthesized (cost = 16): (-((-(~((0xb7-y)&(((0xb7-y)&0xfd)^0x2))))-z))
====================================================================================================
eclasses #: 319
Synthesized (cost = 16): (~((~z)-(~((0xb7-y)&(((0xb7-y)&0xfd)^0x2)))))
====================================================================================================
eclasses #: 804
Synthesized (cost = 14): (z+(~((0xb7-y)&(((0xb7-y)&0xfd)^0x2))))
====================================================================================================
eclasses #: 1907
Synthesized (cost = 14): (z+(~((0xb7-y)&(((0xb7-y)&0xfd)^0x2))))
====================================================================================================
eclasses #: 7293
Synthesized (cost = 5): ((0x48+y)+z)
====================================================================================================
Non-Linear MBA with two 8 bits variables and two 8 bits materialized constants
python3 synth.py
eclasses #: 18
Input (cost = 29): (((((((x&y)*0x3)-(x|y))-(~(x|y)))-(((~x)&y)*0x2))-(~y))-(x|(~y)))
====================================================================================================
eclasses #: 23
Synthesized (cost = 29): (((((((x&y)*0x3)-(x|y))-(~(x|y)))-(((~x)&y)*0x2))-(~y))-(x|(~y)))
====================================================================================================
eclasses #: 28
Synthesized (cost = 29): (((((((x&y)*0x3)-(x|y))-(~(x|y)))-(((~x)&y)*0x2))-(~y))-(x|(~y)))
====================================================================================================
eclasses #: 50
Synthesized (cost = 20): (((-((~x)+(x^y)))+(0x1+((x&y)*0x3)))-(x|(~y)))
====================================================================================================
eclasses #: 125
Synthesized (cost = 18): (((-((~x)+(x|y)))+(0x1+((x&y)*0x3)))-(~y))
====================================================================================================
eclasses #: 499
Synthesized (cost = 15): (((-(~(x&y)))+(0x1+((x&y)*0x3)))+0x1)
====================================================================================================
eclasses #: 2163
Synthesized (cost = 13): ((((x&y)+0x2)+((x&y)*0x3))+0x1)
====================================================================================================
eclasses #: 17036
Synthesized (cost = 11): ((0x3+(x&y))+((x&y)*0x3))
====================================================================================================
eclasses #: 255439
Synthesized (cost = 7): (0x3+(0x4*(x&y)))
e-graph reset done.
====================================================================================================
Polynomial MBA (MBA-Obfuscator) with three 8 bits variables
python3 synth.py --use-mba-blast-before --mba-blast-logic=1
Original: ((((((((((((((((z^((~x)&(y|z)))*0x8)*(x&y))-(((z^((~x)&(y|z)))*0x18)*(x&(~y))))+(((z^((~x)&(y|z)))*0x4)*(~(x|y))))-(((z^((~x)&(y|z)))*0x14)*(~(x|(~y)))))-(((~(x&(y&z)))*0x1e)*(x&y)))-(((~(x&(y&z)))*0xc)*(x&(~y))))+(((~(x&(y&z)))*0x24)*(x|y)))-(((~(x&(y&z)))*0x6)*(~(x^y))))+(((~(x&(y&z)))*0x9)*(~(x|y))))-(((~(x&(y&z)))*0xf)*(~(x|(~y)))))+(((z^((~x)&(y|z)))*0x1c)*(x^y)))-(((z^((~x)&(y|z)))*0x4)*y))-(((~(x&(y&z)))*0x15)*(x^y)))+(((~(x&(y&z)))*0x3)*y))
MBA-Blast: ((~(x&(~x)))*((((((y*0x4)-((x&y)*0x4))+((x&z)*0x4))-((y&z)*0x4))+((x&y)&z))+((~(x&(~x)))*0x3)))
eclasses #: 23
Input (cost = 41): ((~(x&(~x)))*((((((y*0x4)-((x&y)*0x4))+((x&z)*0x4))-((y&z)*0x4))+((x&y)&z))+((~(x&(~x)))*0x3)))
====================================================================================================
eclasses #: 27
Synthesized (cost = 31): (0xff*((((((y*0x4)-((x&y)*0x4))+((x&z)*0x4))-((y&z)*0x4))+((x&y)&z))+0xfd))
====================================================================================================
eclasses #: 40
Synthesized (cost = 28): (-(((((0x4*(y-(x&y)))+((x&z)*0x4))-((y&z)*0x4))+((x&y)&z))+0xfd))
====================================================================================================
eclasses #: 79
Synthesized (cost = 26): (-((((0x4*((y-(x&y))+(x&z)))-((y&z)*0x4))+((x&y)&z))+0xfd))
====================================================================================================
eclasses #: 209
Synthesized (cost = 17): (0x3-((0x4*((x^y)&(y^z)))+((x&y)&z)))
====================================================================================================
eclasses #: 827
Synthesized (cost = 17): ((0x3-((x&y)&z))-(0x4*((x^y)&(y^z))))
====================================================================================================
eclasses #: 8319
Synthesized (cost = 17): ((0x3-((x&y)&z))-(0x4*((x^y)&(y^z))))
====================================================================================================
Polynomial MBA (normal, 3rd degree) with three 8 bits variables
python3 synth.py
eclasses #: 44
Input (cost = 825): ((((((((((((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*(-0x58))+((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*0x68))+(((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*(-0x6d)))+0x26)*((((((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*(-0x58))+((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*0x68))+(((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*(-0x6d)))+0x26))*((((((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*(-0x58))+((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*0x68))+(((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*(-0x6d)))+0x26))*0x18)+((((((((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*(-0x58))+((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*0x68))+(((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*(-0x6d)))+0x26)*((((((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*(-0x58))+((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*0x68))+(((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*(-0x6d)))+0x26))*(-0x28)))+(((((((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*(-0x58))+((((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3))))*0x68))+(((z*0x7)^(((x&z)*0x2)+(((z+(-y))*(x|y))*0x3)))*(-0x6d)))+0x26)*0x5b))+(-0x22))
====================================================================================================
eclasses #: 57
Synthesized (cost = 775): ((((((((((((((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3))))*((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3))))*(-0x58))+((((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3))))*0x68))+(((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3)))*(-0x6d)))+0x26)*((((((((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3))))*((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3))))*(-0x58))+((((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3))))*0x68))+(((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3)))*(-0x6d)))+0x26))*((((((((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3))))*((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3))))*(-0x58))+((((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3)))*((z*0x7)^(((x&z)*0x2)+(((z-y)*(x|y))*0x3))))*