Add :exhaust #94
Comments
|
Indeed. And also note that Cryptol-1 did this "in-parallel." That is, instead of testing one-by-one, you test 64 inputs (assuming you're on a 64 bit machine) in one go. The code is in there in the old repo, but I could be bribed with a sufficient number of beers should it be necessary to explain the obvious magic in detail. |
|
Pssst. @LeventErkok ... want beer on Wednesday? |
|
@TomMD: That might be a possibility.. I'll watch the beers list communication tomorrow! I think I jumped the gun there a bit with the parallel-exhaust comment. Now that I think about it, the parallel execution was done by first generating an AIG, and then interpreting that in parallel, by taking advantage of the fact that all you need to interpret an AIG is the AND operation and the NOT operation, both of which easily parallelize. So, if you have 10 bits of inputs, instead of running from 0 to 1023, you keep 10 64-bit machine words, and then use each bit to represent the next possible value of one of the inputs. That way you can test all those values in parallel, as the underlying machine can do 64-bit AND and 64-bit NOT in one machine instruction. I hope that's clear, if not we can talk about it later. (You can do this in Haskell using Of course, translating to AIG also has the advantage of getting rid of all the interpretative overhead associated with interpreting the Cryptol IR; which really pays off as But of course, I don't think Cryptol-2 has the AIG-generation capabilities of Cryptol-1, so this option may not be available to you directly. On the other hand, I bet @weaversa would love this, as it would open the door to talking to ABC directly as well: Once you have the internal AIG's generated, it's rather a simple matter to hook it up to ABC, at least using the file-system. |
Previously, if one command was a prefix of another command, that would lead to an ambiguous lookup from the command trie. Now there are two ways to look up: one works like previously, which is good for tab-completion, and the other will only return one result if there is an exact match. This means we can now have multiple forms of each command, so we can explicitly have short forms like :e -> :edit that won't be changed just based on what names we give to future commands. This closes #90, and also #94 which was blocked on this due to :exhaust and :edit conflicting.
|
Forgot to close this back on 95bb27b |
A la Cryptol 1, we should have an exhaustive checking mode.
The text was updated successfully, but these errors were encountered: