Welcome,
Guest
. Please
login
or
register
.
Did you miss your
activation email
?
1 Hour
1 Day
1 Week
1 Month
Forever
Login with username, password and session length
Home
About
Team
Rules
Stats
Status
Sitemap
IRC
Server Map
Bots
Control Panel
Omninet
Efnet
Rules
Downloads
Forum
News
Our Projects
Major Community Projects
Recent...
Unread
Replies
Recent
Tools
Online Axe Tilemap Editor
TI83 Plus ASM File Unsquisher
Z80 Conversion Tools
IES TI File Editor
Free RAM areas
Comprehensive Getkeyr table
URL Shortener
Help
Contact Us
Change Request
Report Issue/Bug
Team
Articles
Members
View the memberlist
Search For Members
Buddies
Login
Register
Omnimaga
»
Forum
»
General Discussion
»
Technology and Development
»
Computer Projects and Ideas
»
haroldbot (theorem prover / solver)
« previous
next »
Print
Pages: [
1
]
2
Go Down
Author
Topic: haroldbot (theorem prover / solver) (Read 4638 times)
0 Members and 1 Guest are viewing this topic.
harold
LV5
Advanced (Next: 300)
Posts: 226
Rating: +41/3
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 32bit 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 nonboolean expression. You can make any expression nonboolean by surrounding it with parentheses. For nonconstant 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 "timeout 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 subexpressions. For example: "haroldbot: let m = x >> 31 in abs(x) == (x + m) ^ m"
Builtin 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 preallocated array, the time that takes depends on the speed of the client.
The proofs it finds (if any), are made using the fairly bruteforce 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
»
Logged
+4/0 karm for this message
Blog about bitmath:
bitmath.blogspot.nl
Check the
haroldbot thread
for the supported commands and syntax.
You can use haroldbot from
this website
.
Xeda112358
Xombie. I am it.
Coder Of Tomorrow
LV12
Extreme Poster (Next: 5000)
Posts: 4372
Rating: +691/6
meow :3
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
Logged
My pastebin

Pokémon Amber

Grammer Programming Language

BatLib Library

Jade Simulator

Zeda's Hex Opcodes

FileSyst Library

CopyProg

TPROG

GroupRead

Lbl Read/Write

Z80 Floating Point Routines
harold
LV5
Advanced (Next: 300)
Posts: 226
Rating: +41/3
Re: haroldbot (theorem prover / solver)
«
Reply #2 on:
April 05, 2013, 01:28:51 pm »
haroldbot now also accepts a single = for equality.
Logged
Blog about bitmath:
bitmath.blogspot.nl
Check the
haroldbot thread
for the supported commands and syntax.
You can use haroldbot from
this website
.
Sorunome
Fox Fox Fox Fox Fox Fox Fox!
Support Staff
LV13
Extreme Addict (Next: 9001)
Posts: 7905
Rating: +371/13
Derpy Hooves
Re: haroldbot (theorem prover / solver)
«
Reply #3 on:
April 06, 2013, 02:46:03 pm »
wow, this is pretty amazing
Logged
+1/0 karm for this message
THE GAME
Also, check out
my website
If OmnomIRC is screwed up, blame me!
Click here to give me an internet!
harold
LV5
Advanced (Next: 300)
Posts: 226
Rating: +41/3
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
»
Logged
Blog about bitmath:
bitmath.blogspot.nl
Check the
haroldbot thread
for the supported commands and syntax.
You can use haroldbot from
this website
.
xlibman
Now active at https://codewalr.us
CoT Emeritus
LV15
Omnimagician (Next: )
Posts: 55806
Rating: +3148/232
CodeWalrus founder & retired Omnimaga founder
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.
Also will we be able to use it from OmnomIRC in the future?
Logged
In case you are wondering where I went, I am still active in the TI community, but I left Omni back in 2015 for
various
reasons
. I might come back one day, depending of certain circumstances, but my new online home (despite me being Omnimaga founder in 2001) is now CodeWalrus (
https://codewalr.us
). Sorry for the inconveniences.
Bandcamp

Reverbnation

Facebook

Youtube

Twitter
Retired
Omnimaga
admin (200111) and editor (201214)
harold
LV5
Advanced (Next: 300)
Posts: 226
Rating: +41/3
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?
Logged
Blog about bitmath:
bitmath.blogspot.nl
Check the
haroldbot thread
for the supported commands and syntax.
You can use haroldbot from
this website
.
Sorunome
Fox Fox Fox Fox Fox Fox Fox!
Support Staff
LV13
Extreme Addict (Next: 9001)
Posts: 7905
Rating: +371/13
Derpy Hooves
Re: haroldbot (theorem prover / solver)
«
Reply #7 on:
April 07, 2013, 01:55:24 pm »
Here it works from OmnomIRC
Logged
+1/0 karm for this message
THE GAME
Also, check out
my website
If OmnomIRC is screwed up, blame me!
Click here to give me an internet!
xlibman
Now active at https://codewalr.us
CoT Emeritus
LV15
Omnimagician (Next: )
Posts: 55806
Rating: +3148/232
CodeWalrus founder & retired Omnimaga founder
Re: haroldbot (theorem prover / solver)
«
Reply #8 on:
April 08, 2013, 01:23:10 am »
Quote from: harold on April 07, 2013, 12:28:33 pm
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
Logged
In case you are wondering where I went, I am still active in the TI community, but I left Omni back in 2015 for
various
reasons
. I might come back one day, depending of certain circumstances, but my new online home (despite me being Omnimaga founder in 2001) is now CodeWalrus (
https://codewalr.us
). Sorry for the inconveniences.
Bandcamp

Reverbnation

Facebook

Youtube

Twitter
Retired
Omnimaga
admin (200111) and editor (201214)
harold
LV5
Advanced (Next: 300)
Posts: 226
Rating: +41/3
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
Logged
Blog about bitmath:
bitmath.blogspot.nl
Check the
haroldbot thread
for the supported commands and syntax.
You can use haroldbot from
this website
.
harold
LV5
Advanced (Next: 300)
Posts: 226
Rating: +41/3
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
»
Logged
Blog about bitmath:
bitmath.blogspot.nl
Check the
haroldbot thread
for the supported commands and syntax.
You can use haroldbot from
this website
.
Sorunome
Fox Fox Fox Fox Fox Fox Fox!
Support Staff
LV13
Extreme Addict (Next: 9001)
Posts: 7905
Rating: +371/13
Derpy Hooves
Re: haroldbot (theorem prover / solver)
«
Reply #11 on:
April 29, 2013, 06:52:31 pm »
This bot is just getting so awesome, nice work!
Logged
+1/0 karm for this message
THE GAME
Also, check out
my website
If OmnomIRC is screwed up, blame me!
Click here to give me an internet!
harold
LV5
Advanced (Next: 300)
Posts: 226
Rating: +41/3
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".
Logged
Blog about bitmath:
bitmath.blogspot.nl
Check the
haroldbot thread
for the supported commands and syntax.
You can use haroldbot from
this website
.
harold
LV5
Advanced (Next: 300)
Posts: 226
Rating: +41/3
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]")
Logged
Blog about bitmath:
bitmath.blogspot.nl
Check the
haroldbot thread
for the supported commands and syntax.
You can use haroldbot from
this website
.
harold
LV5
Advanced (Next: 300)
Posts: 226
Rating: +41/3
Re: haroldbot (theorem prover / solver)
«
Reply #14 on:
August 05, 2013, 03:28:26 pm »
Small update: added ternary operator.
Logged
Blog about bitmath:
bitmath.blogspot.nl
Check the
haroldbot thread
for the supported commands and syntax.
You can use haroldbot from
this website
.
Print
Pages: [
1
]
2
Go Up
« previous
next »
Omnimaga
»
Forum
»
General Discussion
»
Technology and Development
»
Computer Projects and Ideas
»
haroldbot (theorem prover / solver)