Author Topic: haroldbot (theorem prover / solver)  (Read 21717 times)

0 Members and 1 Guest are viewing this topic.

Offline harold

  • LV5 Advanced (Next: 300)
  • *****
  • Posts: 226
  • Rating: +41/-3
    • View Profile
haroldbot (theorem prover / solver)
« on: April 05, 2013, 12:40:19 pm »
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.
« Last Edit: February 18, 2017, 12:45:31 pm by harold »
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

Offline Xeda112358

  • they/them
  • Moderator
  • LV12 Extreme Poster (Next: 5000)
  • ************
  • Posts: 4704
  • Rating: +719/-6
  • Calc-u-lator, do doo doo do do do.
    • View Profile
Re: haroldbot (theorem prover / solver)
« Reply #1 on: April 05, 2013, 01:07:35 pm »
I tested it; I had fun. I just keep forgetting to use * and == even though I know I am supposed to :P

Offline harold

  • LV5 Advanced (Next: 300)
  • *****
  • Posts: 226
  • Rating: +41/-3
    • View Profile
Re: haroldbot (theorem prover / solver)
« Reply #2 on: April 05, 2013, 01:28:51 pm »
haroldbot now also accepts a single = for equality.
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

Offline Sorunome

  • Fox Fox Fox Fox Fox Fox Fox!
  • Support Staff
  • LV13 Extreme Addict (Next: 9001)
  • *************
  • Posts: 7920
  • Rating: +374/-13
  • Derpy Hooves
    • View Profile
    • My website! (You might lose the game)
Re: haroldbot (theorem prover / solver)
« Reply #3 on: April 06, 2013, 02:46:03 pm »
wow, this is pretty amazing O.O

THE GAME
Also, check out my website
If OmnomIRC is screwed up, blame me!
Click here to give me an internet!

Offline harold

  • LV5 Advanced (Next: 300)
  • *****
  • Posts: 226
  • Rating: +41/-3
    • View Profile
Re: haroldbot (theorem prover / solver)
« Reply #4 on: April 07, 2013, 11:16:22 am »
I added showing up to 4 results to "solve" mode, as well as showing the total number of solutions.
« Last Edit: April 07, 2013, 11:16:31 am by harold »
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

Offline DJ Omnimaga

  • Clacualters are teh gr33t
  • CoT Emeritus
  • LV15 Omnimagician (Next: --)
  • *
  • Posts: 55941
  • Rating: +3154/-232
  • CodeWalrus founder & retired Omnimaga founder
    • View Profile
    • Dream of Omnimaga Music
Re: haroldbot (theorem prover / solver)
« Reply #5 on: April 07, 2013, 12:21:01 pm »
Awesome, this will be useful to cheat on tests. Just kidding I might need it from time to time. :P

Also will we be able to use it from OmnomIRC in the future?

Offline harold

  • LV5 Advanced (Next: 300)
  • *****
  • Posts: 226
  • Rating: +41/-3
    • View Profile
Re: haroldbot (theorem prover / solver)
« Reply #6 on: April 07, 2013, 12:28:33 pm »
Wait, in the future? Isn't that possible right now?
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

Offline Sorunome

  • Fox Fox Fox Fox Fox Fox Fox!
  • Support Staff
  • LV13 Extreme Addict (Next: 9001)
  • *************
  • Posts: 7920
  • Rating: +374/-13
  • Derpy Hooves
    • View Profile
    • My website! (You might lose the game)
Re: haroldbot (theorem prover / solver)
« Reply #7 on: April 07, 2013, 01:55:24 pm »
Here it works from OmnomIRC :)

THE GAME
Also, check out my website
If OmnomIRC is screwed up, blame me!
Click here to give me an internet!

Offline DJ Omnimaga

  • Clacualters are teh gr33t
  • CoT Emeritus
  • LV15 Omnimagician (Next: --)
  • *
  • Posts: 55941
  • Rating: +3154/-232
  • CodeWalrus founder & retired Omnimaga founder
    • View Profile
    • Dream of Omnimaga Music
Re: haroldbot (theorem prover / solver)
« Reply #8 on: April 08, 2013, 01:23:10 am »
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 :P

Offline harold

  • LV5 Advanced (Next: 300)
  • *****
  • Posts: 226
  • Rating: +41/-3
    • View Profile
Re: haroldbot (theorem prover / solver)
« Reply #9 on: April 08, 2013, 01:25:36 am »
Actually, for the first couple of hours, it only worked with OmnomIRC :)
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

Offline harold

  • LV5 Advanced (Next: 300)
  • *****
  • Posts: 226
  • Rating: +41/-3
    • View Profile
Re: haroldbot (theorem prover / solver)
« Reply #10 on: April 28, 2013, 03:22:45 pm »
Update: added abs, changed >> to signed, added >>> as unsigned shift, solved a big bug in quantified solve mode
This new version is now online.
« Last Edit: April 28, 2013, 03:41:20 pm by harold »
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

Offline Sorunome

  • Fox Fox Fox Fox Fox Fox Fox!
  • Support Staff
  • LV13 Extreme Addict (Next: 9001)
  • *************
  • Posts: 7920
  • Rating: +374/-13
  • Derpy Hooves
    • View Profile
    • My website! (You might lose the game)
Re: haroldbot (theorem prover / solver)
« Reply #11 on: April 29, 2013, 06:52:31 pm »
This bot is just getting so awesome, nice work! :D

THE GAME
Also, check out my website
If OmnomIRC is screwed up, blame me!
Click here to give me an internet!

Offline harold

  • LV5 Advanced (Next: 300)
  • *****
  • Posts: 226
  • Rating: +41/-3
    • View Profile
Re: haroldbot (theorem prover / solver)
« Reply #12 on: May 18, 2013, 07:41:46 am »
Update: everything is now signed. You can go back to unsigned with the keyword "unsigned".
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

Offline harold

  • LV5 Advanced (Next: 300)
  • *****
  • Posts: 226
  • Rating: +41/-3
    • View Profile
Re: haroldbot (theorem prover / solver)
« Reply #13 on: June 07, 2013, 07:12:32 pm »
Update: !!changed the meaning of >>>!! added some functions, added a fallback to a SAT solver, and improved the detection of simple expressions (ie when you say "haroldbot: a + b" it should say "[a + b]" instead of "[solution not constant]")
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

Offline harold

  • LV5 Advanced (Next: 300)
  • *****
  • Posts: 226
  • Rating: +41/-3
    • View Profile
Re: haroldbot (theorem prover / solver)
« Reply #14 on: August 05, 2013, 03:28:26 pm »
Small update: added ternary operator.
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.