haroldbot (development name: TheoremBot) was an IRC bot (now only a website) that proves theorems, solves equations, and can even calculate. All in the 32-bit bitvector domain (if that means nothing to you, take that to mean "it calculates with unsigned ints, not natural numbers or real numbers or anything like that).

Warning: the interpretation of >> has changed between versions, it is and was an unsigned shift in the current and the first version, but a signed shift in some versions in between.
Warning: the interpretation of >>> has changed between versions, it is now a rotate.
Warning: in version 5d, theorem proving mode has become much more sensitive to divisions by zero, so sensitive that if there's any possibility of division by zero it will freak out. I'll try to do something about that at some point.

How to use it
There are three basic modes.

• The "solve" mode. Just type in any boolean expression. haroldbot will try to solve it, and give (if applicable) cases of inputs that make it true, false, or result in a divby0. If an expression is always true, haroldbot will search for a proof. Example: "x * 3 == 1" or "x + y == y + x"
• The calculation/simplification mode. Used for any non-boolean expression. You can make any expression non-boolean by surrounding it with parentheses. For non-constant results, only some inputs result in anything interesting (if the resulting BDD can be matched against a known pattern). Example: "1+2+3+4^15" or "a | a"

note: haroldbot tries to answer you regardless of what else you put in a message as long as it has the string haroldbot: in it. If it doesn't answer, usually that means you asked something it didn't like.
note: sometime it will say something like "time-out while counting solutions". That means the BDD approach didn't work out and it had to switch to the SAT solver - don't worry if you don't know what that means, it's the implication of that that's important: it will not find try to find "nice" results, it will find just any old result. Quantified mode does not fall back to the SAT solver (yet?).

Signedness
Values in haroldbot have no signedness, instead the operations have signedness. All operators and functions are unsigned by default, append s (operators) or _s (functions) to get the signed version, if there is one.

Expression syntax
Operator precedence and associativity are almost the same as in C, but not quite. Notably the comparisons have a lower precedence than bitwise operations (but still higher than boolean operations). Here is a list of available operators and their gotcha's, in order of precedence (groups of equal precedence not shown)

• ~ bitwise NOT, aka 1's complement.
• - unary minus, aka 2's complement.
• * multiplication. haroldbot doesn't really like multiplication, especially not if neither of the two operands is a constant. Computation tends to be slow (using the SAT solver fallback) or even time out and give no result.
• /, /u, /s division. The warning about multiplication also applies to division. Note that "0x80000000 / -1" in signed mode doesn't "error", as it usually would.
• %, %u, %s remainder, aka modulo (in the unsigned case). Signed remainder has the sign of the dividend. The warning about multiplication also applies to remainder.
• + addition.
• - subtraction.
• << left shift. haroldbot doesn't like shifts where the right operand isn't a constant, but you can sometimes get away with it. It's not as bad as multiplication.
• >>, >>u, >>s signed right shift in signed mode, unsigned right shift in unsigned mode. The warning about shifts also applies to signed right shift.
• & bitwise AND.
• ^ bitwise XOR.
• | bitwise OR.
• ==, !=, <, <u, <s, >, >u, >s, <=, <=u, <=s, >=, >=u, >=s signed or unsigned comparisons. '=' is not a comparison. Comparisons give a mask of all 1's or all 0's instead of being a boolean true or false.
• => implies. implemented as (~a | b) == -1.
• && boolean AND.
• || boolean OR.
• ?: actually a bitwise mux, acts like the usual ternary operator if the condition can only be 0 or -1 (for example, if the condition is a boolean expression).
• let name = expression in expression used to give names to things. Useful to factor out common sub-expressions. For example: "haroldbot: let m = x >> 31 in abs(x) == (x + m) ^ m"

Built-in functions:

• min(a, b) takes the signed or unsigned minimum of a and b.
• min_s(a, b) takes the signed minimum of a and b.
• min_u(a, b) takes the unsigned minimum of a and b.
• max(a, b) takes the signed or unsigned maximum of a and b.
• max_s(a, b) takes the signed maximum of a and b.
• max_u(a, b) takes the unsigned maximum of a and b.
• popcnt(a) the population count aka hamming weight (number of 1 bits) of a.
• nlz(a) number of leading 0's in a.
• ntz(a) number of trailing 0's in a.
• reverse(a) reverses the bits in a.
• abs(a) takes the absolute value of a where a is interpreted as signed (otherwise it would do nothing).

How it works
It builds an array of 32 binary decision diagram's of the input (one for each bit), and does some fairly standard operations on them (quantified solve mode uses universal quantification over all the variables that you didn't mention, which is a bit rare). There's no magic. If you want to learn more about BDD's, you can read the draft of Knuth's Chapter 7.1.4.
When that fails (that is, there are more than about a hundred thousand nodes in the BDD), it switches to a SAT solver. It switches when the BDDs get too big to fit in their pre-allocated array, the time that takes depends on the speed of the client.

The proofs it finds (if any), are made using the fairly brute-force approach of taking both "ends" of the proof and applying rewrite rules until they meet in the middle. This process is guided somewhat by selecting candidate expressions to rewrite based on their "weight", the weight is a combination of how many steps away it is from the original expression and, crucially, how complicated the expression is. It's an empirical observation that it's usually not necessary to have expressions in a proof that are a lot more complicated than the most complicated "end" of the proof. Of course this does not always hold, so this optimization makes it slower to find some proofs, while making it faster to find typical proofs. A second important component is two forms of hashing. One form that helps to match expressions that are overall structurally equal (all explored expressions are put into hash sets using this type of hash, to make it fast to detect when the two expanding clouds of expressions meet). That hash the usual "combination of hashes of child nodes and this node". The other hash is one that helps to match rewrite rules to expressions, it considers only a node and its immediate children. Rewrite rules are put in bins according to which hashes they would match onto, when rewriting this is used to only attempt to match a rule pattern to an expression if it has a decent chance of actually matching.


I'm open to requests, but BDDs are no silver bullet and will not solve everything, and the SAT solver fallback tends to be really slow (through no fault of its own, it's just that it automatically only gets to deal with hard problems - everything easy is solved by the BDDs). For example multiplication, division and remainder, are just fundamentally hard to deal with. It's also not really a good framework for simplification, but you can use theorem proving mode to test if your own simplification is correct.

haroldbot now also accepts a single = for equality.

I added showing up to 4 results to "solve" mode, as well as showing the total number of solutions.

Wait, in the future? Isn't that possible right now?

Wait, in the future? Isn't that possible right now?

Ah I didn't know it was implemented already. Many bots creators tend to forget OmnomIRC at first, so I tend to ask if it will be planned

Update: added abs, changed >> to signed, added >>> as unsigned shift, solved a big bug in quantified solve mode
This new version is now online.

Update: everything is now signed. You can go back to unsigned with the keyword "unsigned".

Small update: added ternary operator.