## Examples

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

## Notes

Tip: a saved copy of this page works offline.

== binds less strongly than bitwise operators.

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

The BDD structural matcher has not been fully ported yet.

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.

## List of available functions

• min = min_u, min_s
• max = max_u, max_s
• addus, addss, subus, subss (un)signed saturating addition and subtraction
• avg_up unsigned average, rounded up
• 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