Just do some math

`1000 + 15 & -16`

Find out whether two expressions are equivalent

`let x = a + b in (x < a) == (x < max(a, b))`

*Prove* that two expressions are equivalent

`a ^ ((a ^ b) & mask) == (a & ~mask) | (b & mask)`

Find when two expressions are equal and when they are not

`x == -x`

Quantify some variables away to find values that always work

`forall x: -x == (x ^ m) - m`

Tip: a saved copy of this page works offline.

See the table of operators below for operator precedence.

Comparisons result in 0 (false) or -1 (true).

Finding proofs can be slow and often nothing is found at all.

SAT fallback now exists, using MiniSat compiled with Emscripten. This is brand new so expect bugs (not due to MiniSat, but for example I don't entirely trust my circuit builder and circuit-to-SAT converter). haroldbot should now give up early on (some) multiplications that would create a gigantic BDD.

In general, there *are* many bugs.

Since everything happens client-side, I don't get automatic bug reports. Please open an issue or contact me (eg via email, Mastodon @harold@mastodon.gamedev.place or twitter @HaroldAptroot).

Overview of how haroldbot works.

`min = min_u, min_s``max = max_u, max_s``ror, rol`bitwise rotate`addus, addss, subus, subss`(un)signed saturating addition and subtraction`avg, avg_up`unsigned average, rounded down or up respectively`ternlog``popcnt``abs``nlz`(alias`lzcnt`) number of leading zeroes`ntz`(alias`tzcnt`) number of trailing zeroes`reverse`bit-reversal`grev`generalized bit-reversal (2 arguments)`hmul = hmul_u, hmul_s`high half of product`blsi, blsr, blsmsk, tzmsk`BMI operations`bzhi, pdep, pext`BMI2 operations`clmul`carryless multiplication`grevmul`it's grevmul, whatever that is

Precedence | Operator | Description |
---|---|---|

1 | let ... in ... | "let" expression |

2 | ~ |
bitwise complement |

- | negation | |

3 | * | multiplication |

/ /u | unsigned division | |

/s | signed division | |

/e | Euclidean division | |

/p | unsigned division but division by zero yields zero | |

% %u | unsigned remainder | |

%s | signed remainder | |

%e | Euclidean remainder | |

4 | + | addition |

- | subtraction | |

5 | << | shift left |

>> >>u | shift right (logical) | |

>>s | shift right (arithmetic) | |

6 | & | bitwise AND |

7 | ^ | bitwise XOR |

8 | | | bitwise OR |

9 | == | compare equal |

!= | compare not equal | |

< <u | compare unsigned less than | |

<s | compare signed less than | |

> >u | compare unsigned greater than | |

>s | compare signed greater than | |

<= <=u | compare unsigned less than or equal | |

<=s | compare signed less than or equal | |

>= >=u | compare unsigned greater than or equal | |

>=s | compare signed greater than or equal | |

10 | && | Boolean AND, implicitly converts integer operands to Boolean |

11 | || | Boolean OR, implicitly converts integer operands to Boolean |

12 | => | Boolean implication, implicitly converts integer operands to Boolean |

13 | ... ? ... : ... | Ternary operator if the condition is a Boolean, otherwise bitwise MUX |